*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] rule induction question*From*: Amarin Phaosawasdi <phaosaw2 at illinois.edu>*Date*: Sun, 28 Sep 2014 20:13:24 -0500*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.1

Hi all,

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"

Would anybody mind taking a look, please?

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"

{ assume true2: "bval b i"

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 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:*Tobias Nipkow

- Previous by Date: Re: [isabelle] nested multiset ordering?
- Next by Date: [isabelle] Vocabulary question: is the real name of HOL, λHOL?
- Previous by Thread: Re: [isabelle] nested multiset ordering?
- 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