Time 
Nick 
Message 
00:29 

ilbot3 joined #isabelle 
00:29 

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/ 
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/ 
03:25 
tautologico 
I want to prove an equality f x = g y where both f and g are defined functions. trying to use "by simp" unfolds the left side but not the right side. and the result is a big term that I don't want to write explicitly. how can I prove this? 
08:41 
ThreeOfEight 
tautologico: that is impossible to answer without more context 
09:43 
tautologico 
I (re)defined natural numbers with S and Z constructors, a multiplication function (mult) and factorial. I want to prove factorial 5 = mult 12 10 (where 5 = (S (S (S (S (S Z))))) and so on) 
10:08 
ThreeOfEight 
tautologico: well show me your code 
10:08 
ThreeOfEight 
put it in a paste bin or something 
10:09 
ThreeOfEight 
(if it's a university assignment or something like that, use a private paste bin, /msg the link to me and delete it afterwards) 
10:10 
ThreeOfEight 
but from what you have told me so far, I wonder how you defined "5", "12", and "10" 
10:10 
ThreeOfEight 
and my guess would be that you would have to unfold those definitions 
13:09 
tautologico 
it's not an assignment :) 
13:10 
tautologico 
I'm translating parts of the "Software Foundations" book (uses Coq) to Isabelle/HOL, as an exercise 
13:14 
tautologico 
the relevant parts are in this gist: https://gist.github.com/tautologico/59fe0d68c4616e9ecb55 
13:26 
ThreeOfEight 
tautologico: oh that's easy 
13:26 
ThreeOfEight 
you just have to unfold the definitions of ten/twelve 
13:26 
ThreeOfEight 
e.g. "unfolding ten_def twelve_def by simp" 
13:26 
ThreeOfEight 
or "by (simp add: ten_def twelve_def)" 
13:27 
ThreeOfEight 
note that this proof will fail, because both your ten and your twelve are actually nines 
13:28 
tautologico 
that's right 
13:28 
tautologico 
it works, thank you :) 
13:29 
tautologico 
the original book uses a submodule when defining the naturals, and later closes the submodule so the rest of the code uses the standard nat type in Coq, so it can use number literals in this part 
13:42 
ThreeOfEight 
well if you really want to do this sort of thing, you should prove that your natural numbers form a semiring 
13:42 
ThreeOfEight 
http://downthetypehole.de/paste/GNbfdVQL 
13:42 
ThreeOfEight 
then you can use numeral syntax for them out of the box 
13:43 
ThreeOfEight 
I left out all the instance proofs (i.e. the semiring axioms for nat), but those are pretty straightforward 
13:44 
ThreeOfEight 
adding the eval_nat_numeral I proved in there to the simp set automatically converts numerals to the corresponding "S (S (S Z)))" notation 
13:44 
ThreeOfEight 
as shown in the example 
13:45 
ThreeOfEight 
(numerals are stored in LSBF binary internally) 
14:20 
tautologico 
that's good to know 
14:20 
tautologico 
I think if I define my nats inside a local context or "experiment" (I saw something like this in the manual) I can mirror the structure of the original text 