Time 
Nick 
Message 
01:47 

ilbot3 joined #isabelle 
01: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/ 
05:29 

dmiles joined #isabelle 
10:28 

silver joined #isabelle 
12:21 

aindilis2 joined #isabelle 
14:40 

ski joined #isabelle 
17:35 
popinman322 
Is there a way to set up a custom induction hypothesis? I'm trying to prove two palindrome definitions equivalent and the normal list induction hypothesis isn't enough. 
17:36 
popinman322 
Also, how do you label individual cases when all you have are (numerical) indices? 
17:36 
inte 
popinman322: That's a bit vague. is there a stronger statement that you can show by induction? 
17:38 
popinman322 
inte: this is what I have: http://pastebin.com/t2CT6uMb 
17:39 
popinman322 
The problem is that induction over the list argument gives me an induction hypothesis that makes it impossible to prove the Cons case 
17:40 
popinman322 
"x = a_ # x_" IH: "isPal1 x_ = isPal2 x_" 
17:40 
popinman322 
... or, at least, it'd be incredibly awkward 
17:41 
inte 
hmm, is there a reason this won't go through: proof (induct rule: isPal2.induct) case 3 thus ?case sorry qed auto 
17:43 
popinman322 
That results in the same issue 
17:43 
popinman322 
Possibly 
17:44 
popinman322 
... I can work with that. 
17:44 
popinman322 
It's still awkward. Probably because I didn't express isPal2 that well. 
17:46 
inte 
well, it's provable and not too hard. 
17:46 
inte 
(it's often a good idea to do induction on function definitions) 
17:47 
popinman322 
The third induction case for isPal2 says nothing about the equality of "last (v # va)" and "a" 
17:48 
popinman322 
So split into cases over the equality? 
17:48 
inte 
well, the "a" is removed... it's the first element of the list. 
17:48 
popinman322 
inte, I'm sorry. I'm still too new to this. Thank you. 
17:50 
inte 
if you apply auto to that goal, the equation that stands out to me is "  "isPal2 [x] = True"" 
17:51 
inte 
sorry, is "rev x @ [b, a] = a # b # x" 
17:55 
inte 
And Isabelle needs help with matching the rev x with the a # ... part, splitting off the last element of the x. Which is the same as splitting off the first element of "rev x", so I tried apply (cases "rev x"), which slightly amazingly did the trick (auto can solve the remaining goals) 
22:34 

silver_ joined #isabelle 