Re: [isabelle] rule induction question



Dear Amarin,

That is a nice little puzzle. I had not tried it before and needed some time to
find a solution (see below). The fine structure of the proofs remains obscure
and you may want to spell it out yourself. The main point is however not that
difficult: the lemma lem did not drop out of thin air but comes directly from
looking at the subgoal in the WhileTrue case. On the techical side it is
important to write the induction in the given form because the proposition you
induct on contains other subterms than just variables.

There may be other slicker ways of proving your goal but I could not see how to
complete your original attempt.

Tobias

lemma lem:
  "⟦ (WHILE b DO (c;; IF b THEN c ELSE SKIP),s2) ⇒ s3; bval b s1; (c,s1) ⇒ s2 ⟧
   ⟹ (WHILE b DO (c;; IF b THEN c ELSE SKIP),s1) ⇒ s3"
apply(induction "WHILE b DO (c;; IF b THEN c ELSE SKIP)" s2 s3
  arbitrary: s1 rule: big_step_induct)
 apply auto
done

lemma "(WHILE b DO c,s) ⇒ t ⟹ (WHILE b DO (c;; IF b THEN c ELSE SKIP),s) ⇒ t"
proof(induction "WHILE b DO c" s t rule: big_step_induct)
  case WhileFalse thus ?case by blast
next
  case WhileTrue thus ?case using lem by blast
qed


On 29/09/2014 03:13, Amarin Phaosawasdi wrote:
> 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.