Time 
Nick 
Message 
02:47 

ilbot3 joined #isabelle 
02:47 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
04:28 
spacekitteh 
okay so 
04:28 
spacekitteh 
i have a string set 
04:28 
spacekitteh 
how can i map each element of the set to a unique integer? 
04:29 
spacekitteh 
i.e. memory_location "index" {"index", "sum"} = 1 
04:29 
spacekitteh 
i.e. memory_location "sum" {"index", "sum"} = 2 
04:29 
spacekitteh 
etc 
06:21 

larsrh_ joined #isabelle 
08:45 
ThreeOfEight 
spacekitteh: oh dear 
08:45 
ThreeOfEight 
it's always problematic to take something that is inherently unordered (a set) and impose some kind of order on it 
08:46 
ThreeOfEight 
you can always work with "SOME", but then that will not be executable 
08:46 
ThreeOfEight 
if it's strings, they are a linear order, so you can probably use "sorted_list_of_set" 
08:46 
ThreeOfEight 
and then use the index of the element in that list as the index (e.g. using the List_Index AFP entry) 
08:48 
ThreeOfEight 
or, if you want to do it more directly, write something like "index x = card {y∈A. y < x}" (where A is the set of strings and x is the string to be indexed) 
08:48 
ThreeOfEight 
so you define the index of a string to be the number of strings in the set that are smaller than it 
08:48 
ThreeOfEight 
not sure if that is the best way to do it 
09:17 
larsrh 
"sorted_list_of_set" is alright, but there's not a lot of library around it 
10:00 
ThreeOfEight 
Frankly, you might want to overthink working with sets in the first place 
10:01 
ThreeOfEight 
It is often tempting to do something with sets and then impose some order on them later on, but I don't think that's a good idea 
10:32 
spacekitteh 
i plan on using some different orderings 
10:32 
spacekitteh 
e.g. alphabetical, cachecoherent, etc 
10:32 
spacekitteh 
er cache locality 
10:32 
larsrh 
Where in HOL can I find the theorem that a function 'a set => 'a can't be injective? 
11:34 
ammbauer 
using the same case_names in different induction rules shouldn't be a problem, right? 
11:42 
inte 
larsrh: Cantors_paradox is the key: lemma "¬ inj (f :: 'a set ⇒ 'a)" by (metis Cantors_paradox Pow_UNIV inj_imp_surj_inv) 
12:06 
larsrh 
ammbauer: nope, not a problem 
12:06 
larsrh 
inte: thanks 
13:07 

dmiles_afk joined #isabelle 
14:00 

tokenrove joined #isabelle 
18:20 

mal``` joined #isabelle 