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 sledgehammergenerated proof I don't really understand the complexity of 
01:43 
barrucadu 
Hopefully this'll be the last question for a while… 
01:52 
inte 
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 
inte: Possibly, let me try 
01:57 
inte 
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 
inte 
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 
inte 
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 inte suggested 
10:07 
ThreeOfEight 
barrucadu: what exactly does your "trace_por_agree" function do? 
10:07 
ThreeOfEight 
it would be easier to prove things with it if you could formulate it with just 2 cases 
12:58 
barrucadu 
It's kind of doing two things at once, and I'm not sure it needs to do both those things… so I can throw away the singleton case and make the nil case be True 
13:41 
ThreeOfEight 
I tried to complete your proof but got very stuck at one point and couldn't really proceed because I had no idea what "trace_por_agree" actually does 
13:41 
ThreeOfEight 
keeping things separate and modular whenever possible is one of the things that tend to make one's life a lot easier in theorem proving 
13:42 
ThreeOfEight 
oh, and, by the way "obtain x where "x = …"" is kind of an antipattern 
13:42 
ThreeOfEight 
just write "def x ≡ "..."" 
13:42 
ThreeOfEight 
then you get a theorem called x_def to unfold the definition 
13:43 
ThreeOfEight 
and if you only want an input abbreviation without defining a new constant, you can also use "let ?x = "..."" 
17:48 

mbrcknl joined #isabelle 