# IRC log for #isabelle, 2016-01-20

All times shown according to UTC.

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, cache-coherent, 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 int-e 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 int-e: thanks
13:07 dmiles_afk joined #isabelle
14:00 tokenrove joined #isabelle
18:20 mal``` joined #isabelle