Re: [isabelle] rule induction question



Dear Tobias,

This helped tremendously. I spelled the proof out and it made perfect sense.

Thank you,
Amarin

On 09/29/2014 01:51 PM, Tobias Nipkow wrote:
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.