*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rule induction question*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 29 Sep 2014 20:51:39 +0200*In-reply-to*: <5428B234.5090600@illinois.edu>*References*: <5428B234.5090600@illinois.edu>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

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 >

**Follow-Ups**:**Re: [isabelle] rule induction question***From:*Amarin Phaosawasdi

**References**:**[isabelle] rule induction question***From:*Amarin Phaosawasdi

- Previous by Date: Re: [isabelle] Problems with code-datatype
- Next by Date: [isabelle] 2 year postdoc on formal security at Swansea University (Markus Roggenbach)
- Previous by Thread: [isabelle] rule induction question
- Next by Thread: Re: [isabelle] rule induction question
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list