[isabelle] rule induction question



Hi all,

I've been using the book Concrete Semantics (http://www21.in.tum.de/~nipkow/Concrete-Semantics/) as a tutorial.

Currently, I'm trying to prove the following.
"⟦(WHILE b DO c,s)⇒t⟧⟹(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"

In other words, I want to prove that I can unroll the loop and end up in the same final state.

At some point in the proof, I'm in a "subtree" (also another WHILE loop) of the original WHILE b DO c. I want to be able to apply the induction hypothesis and get an unrolled loop for that subtree.

I looked at some examples of rule induction on the web and in the Programming and Proving book. I tried structuring the proofs that way and also used cases, but am still stuck.

The version of the theory that I'm sending here uses "proof -". It helps me being explicit what I'm trying to do since I'm new to Isabelle.

I've laid out the whole proof and skipped the parts where I needed the induction hypothesis with "sorry".

Would anybody mind taking a look, please?

The code is below. I've marked the places that I need help with "(* NEED INDUCTION HYPOTHESIS *)".

Thank you,
Amarin

========================
Semantics.thy
========================
theory Semantics imports Main begin

type_synonym vname = string
type_synonym val = int
type_synonym state = "vname ⇒ val"

datatype aexp = N int | V vname
fun aval :: "aexp ⇒ state ⇒ val" where
"aval (N n) s = n" |
"aval (V x) s = s x"

datatype bexp = Bc bool
fun bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) s = v"

datatype
  com = SKIP
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
      | Seq    com  com         ("_;;/ _"  [60, 61] 60)
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)

inductive
  big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
Skip: "(SKIP,s) ⇒ s" |
Assign: "(x ::= a,s) ⇒ s(x := aval a s)" |
Seq: "⟦ (c1,s1) ⇒ s2;  (c2,s2) ⇒ s3 ⟧ ⟹ (c1;;c2, s1) ⇒ s3" |
IfTrue: "⟦ bval b s;  (c1,s) ⇒ t ⟧ ⟹ (IF b THEN c1 ELSE c2, s) ⇒ t" |
IfFalse: "⟦ ¬bval b s;  (c2,s) ⇒ t ⟧ ⟹ (IF b THEN c1 ELSE c2, s) ⇒ t" |
WhileFalse: "⟦¬bval b s⟧ ⟹ (WHILE b DO c,s) ⇒ s" |
WhileTrue: "⟦ bval b s1;  (c,s1) ⇒ s2;  (WHILE b DO c,s2) ⇒ s3 ⟧
  ⟹ (WHILE b DO c, s1) ⇒ s3"

declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
inductive_cases SkipE[elim!]: "(SKIP,s) ⇒ t"
inductive_cases AssignE[elim!]: "(x ::= a,s) ⇒ t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1) ⇒ s3"
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) ⇒ t"
inductive_cases WhileE[elim]: "(WHILE b DO c,s) ⇒ t"

theorem big_step_determ: "⟦ (c,s) ⇒ t; (c,s) ⇒ u ⟧ ⟹ u = t"
  by (induction arbitrary: u as3 rule: big_step_induct) blast+

lemma unroll_while:
"⟦(WHILE b DO c,s)⇒t⟧⟹(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"
proof -
  fix b s c t
  assume assms: "(WHILE b DO c,s)⇒t"
  let ?thesis = "(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"
  {
    assume true1: "bval b s"
obtain i where i1:"(c,s)⇒i" and i2:"(WHILE b DO c,i)⇒t" using assms true1 by auto
    {
      assume true2: "bval b i"
obtain i' where i3:"(c,i)⇒i'" and i4:"(WHILE b DO c,i')⇒t" using i2 true2 by auto have body:"(c;;IF b THEN c ELSE SKIP,s) ⇒ i'" using i1 i3 true2 by auto
      have loop:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),i') ⇒ t" using i4
        sorry (* NEED INDUCTION HYPOTHESIS *)
      have ?thesis using body loop true1 by auto
    } moreover
    {
      assume false2: "¬bval b i"
      have body:"(c;;IF b THEN c ELSE SKIP,s) ⇒ i" using i1 false2 by auto
      have loop:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),i) ⇒ t" using i2
        sorry (* NEED INDUCTION HYPOTHESIS *)
      have ?thesis using body loop true1 by auto
    }
    ultimately have "(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t" by metis
  } moreover {
    assume false1: "¬bval b s"
    have final1:"(WHILE b DO c,s)⇒s" using false1 by auto
have final2:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒s" using false1 by auto
    have eq:"s=t" using assms final1 big_step_determ by auto
    have ?thesis using final2 eq by auto
  } ultimately show ?thesis by metis
qed

end




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.