# IRC log for #isabelle, 2016-08-25

All times shown according to UTC.

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 int-e popinman322: That's a bit vague. is there a stronger statement that you can show by induction?
17:38 popinman322 int-e: 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 int-e 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 int-e well, it's provable and not too hard.
17:46 int-e (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 int-e well, the "a" is removed... it's the first element of the list.
17:48 popinman322 int-e, I'm sorry. I'm still too new to this. Thank you.
17:50 int-e if you apply auto to that goal, the equation that stands out to me is "  | "isPal2 [x] = True""
17:51 int-e sorry, is "rev x @ [b, a] = a # b # x"
17:55 int-e 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