# IRC log for #isabelle, 2015-11-21

All times shown according to UTC.

Time Nick Message
01:42 barrucadu I've got this proof I've been working on down to one missing component, which feels like I'm doing the induction wrong: https://gist.github.com/barrucadu/b5fc0b3f440b354cca34 (see the "sorry")
01:43 barrucadu There's also a sledgehammer-generated proof I don't really understand the complexity of
01:43 barrucadu Hopefully this'll be the last question for a while…
01:52 int-e barrucadu: without trying to understand that in full detail: should the  proof (induct trace)  be a  proof (induct trace arbitrary: por)? Right now the induction hypothesis fixes `por` to the original one.
01:54 barrucadu int-e: Possibly, let me try
01:57 int-e you'll then have to use Cons(2) instead of assms(1)
02:01 barrucadu Everything but the 'have "por_well_formed newPor"' works, still not sure how to approach that :(
02:04 int-e a first step would be  unfolding `newPor = grow_por p xs` apply (intro Cons(1)) ... but then you'll have to show that  trace_por_agree xs p  and I'm not sure that actually holds.
02:18 ThreeOfE1ght joined #isabelle
03:10 barrucadu Hmm, I'll stare at this some more in the morning. Thaqnks for the suggestion.
08:24 ski joined #isabelle
09:34 ThreeOfE1ght barrucadu: I haven't looked at your proof in detail, but the first thing I noticed: why don't you do "proof (induction por trace rule: grow_por.induct)"?
09:35 ThreeOfE1ght When doing induction over a function definition, it is usually a good idea to use the induction rule of the function package
09:35 ThreeOfE1ght because that follows the definition of the function precisely
09:40 int-e Ah I should've seen that... that's what I get for not really thinking about what's supposed to be proved.
09:52 ThreeOfE1ght well your approach would probably also have worked, but only with the "arbitrary:" that int-e suggested