--- a/src/HOL/IMP/Compiler0.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(* Title: HOL/IMP/Compiler0.thy
- Author: Tobias Nipkow, TUM
- Copyright 1996 TUM
-
-This is an early version of the compiler, where the abstract machine
-has an explicit pc. This turned out to be awkward, and a second
-development was started. See Machines.thy and Compiler.thy.
-*)
-
-header "A Simple Compiler"
-
-theory Compiler0 imports Natural begin
-
-subsection "An abstract, simplistic machine"
-
-text {* There are only three instructions: *}
-datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
-
-text {* We describe execution of programs in the machine by
- an operational (small step) semantics:
-*}
-
-inductive_set
- stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set"
- and stepa1' :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
- ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50)
- for P :: "instr list"
-where
- "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : stepa1 P"
-| ASIN[simp]:
- "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>"
-| JMPFT[simp,intro]:
- "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>"
-| JMPFF[simp,intro]:
- "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>"
-| JMPB[simp]:
- "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>"
-
-abbreviation
- stepa :: "[instr list,state,nat,state,nat] \<Rightarrow> bool"
- ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) where
- "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^*)"
-
-abbreviation
- stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
- ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50) where
- "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : (stepa1 P ^^ i)"
-
-subsection "The compiler"
-
-primrec compile :: "com \<Rightarrow> instr list" where
-"compile \<SKIP> = []" |
-"compile (x:==a) = [ASIN x a]" |
-"compile (c1;c2) = compile c1 @ compile c2" |
-"compile (\<IF> b \<THEN> c1 \<ELSE> c2) =
- [JMPF b (length(compile c1) + 2)] @ compile c1 @
- [JMPF (%x. False) (length(compile c2)+1)] @ compile c2" |
-"compile (\<WHILE> b \<DO> c) = [JMPF b (length(compile c) + 2)] @ compile c @
- [JMPB (length(compile c)+1)]"
-
-declare nth_append[simp]
-
-subsection "Context lifting lemmas"
-
-text {*
- Some lemmas for lifting an execution into a prefix and suffix
- of instructions; only needed for the first proof.
-*}
-lemma app_right_1:
- assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
- shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
- using assms
- by induct auto
-
-lemma app_left_1:
- assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
- shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -1\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
- using assms
- by induct auto
-
-declare rtrancl_induct2 [induct set: rtrancl]
-
-lemma app_right:
- assumes "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
- shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
- using assms
-proof induct
- show "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1,i1\<rangle>" by simp
-next
- fix s1' i1' s2 i2
- assume "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s1',i1'\<rangle>"
- and "is1 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
- thus "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
- by (blast intro: app_right_1 rtrancl_trans)
-qed
-
-lemma app_left:
- assumes "is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
- shows "is1 @ is2 \<turnstile> \<langle>s1,size is1+i1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
-using assms
-proof induct
- show "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1,length is1 + i1\<rangle>" by simp
-next
- fix s1' i1' s2 i2
- assume "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s1',length is1 + i1'\<rangle>"
- and "is2 \<turnstile> \<langle>s1',i1'\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
- thus "is1 @ is2 \<turnstile> \<langle>s1,length is1 + i1\<rangle> -*\<rightarrow> \<langle>s2,length is1 + i2\<rangle>"
- by (blast intro: app_left_1 rtrancl_trans)
-qed
-
-lemma app_left2:
- "\<lbrakk> is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
- is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
- by (simp add: app_left)
-
-lemma app1_left:
- assumes "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
- shows "instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
-proof -
- from app_left [OF assms, of "[instr]"]
- show ?thesis by simp
-qed
-
-subsection "Compiler correctness"
-
-declare rtrancl_into_rtrancl[trans]
- converse_rtrancl_into_rtrancl[trans]
- rtrancl_trans[trans]
-
-text {*
- The first proof; The statement is very intuitive,
- but application of induction hypothesis requires the above lifting lemmas
-*}
-theorem
- assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
- shows "compile c \<turnstile> \<langle>s,0\<rangle> -*\<rightarrow> \<langle>t,length(compile c)\<rangle>" (is "?P c s t")
- using assms
-proof induct
- show "\<And>s. ?P \<SKIP> s s" by simp
-next
- show "\<And>a s x. ?P (x :== a) s (s[x\<mapsto> a s])" by force
-next
- fix c0 c1 s0 s1 s2
- assume "?P c0 s0 s1"
- hence "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)\<rangle>"
- by (rule app_right)
- moreover assume "?P c1 s1 s2"
- hence "compile c0 @ compile c1 \<turnstile> \<langle>s1,length(compile c0)\<rangle> -*\<rightarrow>
- \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
- proof -
- show "\<And>is1 is2 s1 s2 i2.
- is2 \<turnstile> \<langle>s1,0\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
- is1 @ is2 \<turnstile> \<langle>s1,size is1\<rangle> -*\<rightarrow> \<langle>s2,size is1+i2\<rangle>"
- using app_left[of _ 0] by simp
- qed
- ultimately have "compile c0 @ compile c1 \<turnstile> \<langle>s0,0\<rangle> -*\<rightarrow>
- \<langle>s2,length(compile c0)+length(compile c1)\<rangle>"
- by (rule rtrancl_trans)
- thus "?P (c0; c1) s0 s2" by simp
-next
- fix b c0 c1 s0 s1
- let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
- assume "b s0" and IH: "?P c0 s0 s1"
- hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
- also from IH
- have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c0)+1\<rangle>"
- by(auto intro:app1_left app_right)
- also have "?comp \<turnstile> \<langle>s1,length(compile c0)+1\<rangle> -1\<rightarrow> \<langle>s1,length ?comp\<rangle>"
- by(auto)
- finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
-next
- fix b c0 c1 s0 s1
- let ?comp = "compile(\<IF> b \<THEN> c0 \<ELSE> c1)"
- assume "\<not>b s0" and IH: "?P c1 s0 s1"
- hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,length(compile c0) + 2\<rangle>" by auto
- also from IH
- have "?comp \<turnstile> \<langle>s0,length(compile c0)+2\<rangle> -*\<rightarrow> \<langle>s1,length ?comp\<rangle>"
- by (force intro!: app_left2 app1_left)
- finally show "?P (\<IF> b \<THEN> c0 \<ELSE> c1) s0 s1" .
-next
- fix b c and s::state
- assume "\<not>b s"
- thus "?P (\<WHILE> b \<DO> c) s s" by force
-next
- fix b c and s0::state and s1 s2
- let ?comp = "compile(\<WHILE> b \<DO> c)"
- assume "b s0" and
- IHc: "?P c s0 s1" and IHw: "?P (\<WHILE> b \<DO> c) s1 s2"
- hence "?comp \<turnstile> \<langle>s0,0\<rangle> -1\<rightarrow> \<langle>s0,1\<rangle>" by auto
- also from IHc
- have "?comp \<turnstile> \<langle>s0,1\<rangle> -*\<rightarrow> \<langle>s1,length(compile c)+1\<rangle>"
- by (auto intro: app1_left app_right)
- also have "?comp \<turnstile> \<langle>s1,length(compile c)+1\<rangle> -1\<rightarrow> \<langle>s1,0\<rangle>" by simp
- also note IHw
- finally show "?P (\<WHILE> b \<DO> c) s0 s2".
-qed
-
-text {*
- Second proof; statement is generalized to cater for prefixes and suffixes;
- needs none of the lifting lemmas, but instantiations of pre/suffix.
- *}
-(*
-theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-shows "\<And>a z. a@compile c@z \<turnstile> \<langle>s,size a\<rangle> -*\<rightarrow> \<langle>t,size a + size(compile c)\<rangle>"
- (is "\<And>a z. ?P c s t a z")
-proof -
- from A show "\<And>a z. ?thesis a z"
- proof induct
- case Skip thus ?case by simp
- next
- case Assign thus ?case by (force intro!: ASIN)
- next
- fix c1 c2 s s' s'' a z
- assume IH1: "\<And>a z. ?P c1 s s' a z" and IH2: "\<And>a z. ?P c2 s' s'' a z"
- from IH1 IH2[of "a@compile c1"]
- show "?P (c1;c2) s s'' a z"
- by(simp add:add_assoc[THEN sym])(blast intro:rtrancl_trans)
- next
-(* at this point I gave up converting to structured proofs *)
-(* \<IF> b \<THEN> c0 \<ELSE> c1; case b is true *)
- apply(intro strip)
- (* instantiate assumption sufficiently for later: *)
- apply(erule_tac x = "a@[?I]" in allE)
- apply(simp)
- (* execute JMPF: *)
- apply(rule converse_rtrancl_into_rtrancl)
- apply(force intro!: JMPFT)
- (* execute compile c0: *)
- apply(rule rtrancl_trans)
- apply(erule allE)
- apply assumption
- (* execute JMPF: *)
- apply(rule r_into_rtrancl)
- apply(force intro!: JMPFF)
-(* end of case b is true *)
- apply(intro strip)
- apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
- apply(simp add:add_assoc)
- apply(rule converse_rtrancl_into_rtrancl)
- apply(force intro!: JMPFF)
- apply(blast)
- apply(force intro: JMPFF)
-apply(intro strip)
-apply(erule_tac x = "a@[?I]" in allE)
-apply(erule_tac x = a in allE)
-apply(simp)
-apply(rule converse_rtrancl_into_rtrancl)
- apply(force intro!: JMPFT)
-apply(rule rtrancl_trans)
- apply(erule allE)
- apply assumption
-apply(rule converse_rtrancl_into_rtrancl)
- apply(force intro!: JMPB)
-apply(simp)
-done
-*)
-text {* Missing: the other direction! I did much of it, and although
-the main lemma is very similar to the one in the new development, the
-lemmas surrounding it seemed much more complicated. In the end I gave
-up. *}
-
-end
--- a/src/HOL/IMP/Examples.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-(* Title: HOL/IMP/Examples.thy
- Author: David von Oheimb, TUM
-*)
-
-header "Examples"
-
-theory Examples imports Natural begin
-
-definition
- factorial :: "loc => loc => com" where
- "factorial a b = (b :== (%s. 1);
- \<WHILE> (%s. s a ~= 0) \<DO>
- (b :== (%s. s b * s a); a :== (%s. s a - 1)))"
-
-declare update_def [simp]
-
-subsection "An example due to Tony Hoare"
-
-lemma lemma1:
- assumes 1: "!x. P x \<longrightarrow> Q x"
- and 2: "\<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t"
- shows "w = While P c \<Longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
- using 2 apply induct
- using 1 apply auto
- done
-
-lemma lemma2 [rule_format (no_asm)]:
- "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>
- !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
-apply (erule evalc.induct)
-apply (simp_all (no_asm_simp))
-apply blast
-apply (case_tac "P s")
-apply auto
-done
-
-lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
- (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
- by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
-
-
-subsection "Factorial"
-
-lemma factorial_3: "a~=b ==>
- \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
- by (simp add: factorial_def)
-
-text {* the same in single step mode: *}
-lemmas [simp del] = evalc_cases
-lemma "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
-apply (unfold factorial_def)
-apply (frule not_sym)
-apply (rule evalc.intros)
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply simp
-apply (rule evalc.intros)
-apply simp
-done
-
-end
--- a/src/HOL/IMP/Expr.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-(* Title: HOL/IMP/Expr.thy
- Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
-*)
-
-header "Expressions"
-
-theory Expr imports Main begin
-
-text {*
- Arithmetic expressions and Boolean expressions.
- Not used in the rest of the language, but included for completeness.
-*}
-
-subsection "Arithmetic expressions"
-typedecl loc
-
-type_synonym state = "loc => nat"
-
-datatype
- aexp = N nat
- | X loc
- | Op1 "nat => nat" aexp
- | Op2 "nat => nat => nat" aexp aexp
-
-subsection "Evaluation of arithmetic expressions"
-
-inductive
- evala :: "[aexp*state,nat] => bool" (infixl "-a->" 50)
-where
- N: "(N(n),s) -a-> n"
-| X: "(X(x),s) -a-> s(x)"
-| Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
-| Op2: "[| (e0,s) -a-> n0; (e1,s) -a-> n1 |]
- ==> (Op2 f e0 e1,s) -a-> f n0 n1"
-
-lemmas [intro] = N X Op1 Op2
-
-
-subsection "Boolean expressions"
-
-datatype
- bexp = true
- | false
- | ROp "nat => nat => bool" aexp aexp
- | noti bexp
- | andi bexp bexp (infixl "andi" 60)
- | ori bexp bexp (infixl "ori" 60)
-
-subsection "Evaluation of boolean expressions"
-
-inductive
- evalb :: "[bexp*state,bool] => bool" (infixl "-b->" 50)
- -- "avoid clash with ML constructors true, false"
-where
- tru: "(true,s) -b-> True"
-| fls: "(false,s) -b-> False"
-| ROp: "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |]
- ==> (ROp f a0 a1,s) -b-> f n0 n1"
-| noti: "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
-| andi: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
- ==> (b0 andi b1,s) -b-> (w0 & w1)"
-| ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
- ==> (b0 ori b1,s) -b-> (w0 | w1)"
-
-lemmas [intro] = tru fls ROp noti andi ori
-
-subsection "Denotational semantics of arithmetic and boolean expressions"
-
-primrec A :: "aexp => state => nat"
-where
- "A(N(n)) = (%s. n)"
-| "A(X(x)) = (%s. s(x))"
-| "A(Op1 f a) = (%s. f(A a s))"
-| "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-
-primrec B :: "bexp => state => bool"
-where
- "B(true) = (%s. True)"
-| "B(false) = (%s. False)"
-| "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-| "B(noti(b)) = (%s. ~(B b s))"
-| "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
-| "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
-
-inductive_simps
- evala_simps [simp]:
- "(N(n),s) -a-> n'"
- "(X(x),sigma) -a-> i"
- "(Op1 f e,sigma) -a-> i"
- "(Op2 f a1 a2,sigma) -a-> i"
- "((true,sigma) -b-> w)"
- "((false,sigma) -b-> w)"
- "((ROp f a0 a1,sigma) -b-> w)"
- "((noti(b),sigma) -b-> w)"
- "((b0 andi b1,sigma) -b-> w)"
- "((b0 ori b1,sigma) -b-> w)"
-
-
-lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
- by (induct a arbitrary: n) auto
-
-lemma bexp_iff:
- "((b,s) -b-> w) = (B b s = w)"
- by (induct b arbitrary: w) (auto simp add: aexp_iff)
-
-end
--- a/src/HOL/IMP/Hoare.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(* Title: HOL/IMP/Hoare.thy
- Author: Tobias Nipkow
-*)
-
-header "Inductive Definition of Hoare Logic"
-
-theory Hoare imports Natural begin
-
-type_synonym assn = "state => bool"
-
-inductive
- hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
-where
- skip: "|- {P}\<SKIP>{P}"
-| ass: "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
-| semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
-| If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
- |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
-| While: "|- {%s. P s & b s} c {P} ==>
- |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
-| conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
- |- {P'}c{Q'}"
-
-lemma strengthen_pre: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
-by (blast intro: conseq)
-
-lemma weaken_post: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
-by (blast intro: conseq)
-
-lemma While':
-assumes "|- {%s. P s & b s} c {P}" and "ALL s. P s & \<not> b s \<longrightarrow> Q s"
-shows "|- {P} \<WHILE> b \<DO> c {Q}"
-by(rule weaken_post[OF While[OF assms(1)] assms(2)])
-
-
-lemmas [simp] = skip ass semi If
-
-lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
-
-end
--- a/src/HOL/IMP/Hoare_Den.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,133 +0,0 @@
-(* Title: HOL/IMP/Hoare_Den.thy
- Author: Tobias Nipkow
-*)
-
-header "Soundness and Completeness wrt Denotational Semantics"
-
-theory Hoare_Den imports Hoare Denotation begin
-
-definition
- hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
- "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)"
-
-
-lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
-proof(induct rule: hoare.induct)
- case (While P b c)
- { fix s t
- let ?G = "Gamma b (C c)"
- assume "(s,t) \<in> lfp ?G"
- hence "P s \<longrightarrow> P t \<and> \<not> b t"
- proof(rule lfp_induct2)
- show "mono ?G" by(rule Gamma_mono)
- next
- fix s t assume "(s,t) \<in> ?G (lfp ?G \<inter> {(s,t). P s \<longrightarrow> P t \<and> \<not> b t})"
- thus "P s \<longrightarrow> P t \<and> \<not> b t" using While.hyps
- by(auto simp: hoare_valid_def Gamma_def)
- qed
- }
- thus ?case by(simp add:hoare_valid_def)
-qed (auto simp: hoare_valid_def)
-
-
-definition
- wp :: "com => assn => assn" where
- "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)"
-
-lemma wp_SKIP: "wp \<SKIP> Q = Q"
-by (simp add: wp_def)
-
-lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
-by (simp add: wp_def)
-
-lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_If:
- "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_While_If:
- "wp (\<WHILE> b \<DO> c) Q s =
- wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
-by(simp only: wp_def C_While_If)
-
-(*Not suitable for rewriting: LOOPS!*)
-lemma wp_While_if:
- "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
-by(simp add:wp_While_If wp_If wp_SKIP)
-
-lemma wp_While_True: "b s ==>
- wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
-by(simp add: wp_While_if)
-
-lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
-by(simp add: wp_While_if)
-
-lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
-
-lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
- (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
-apply (simp (no_asm))
-apply (rule iffI)
- apply (rule weak_coinduct)
- apply (erule CollectI)
- apply safe
- apply simp
- apply simp
-apply (simp add: wp_def Gamma_def)
-apply (intro strip)
-apply (rule mp)
- prefer 2 apply (assumption)
-apply (erule lfp_induct2)
-apply (fast intro!: monoI)
-apply (subst gfp_unfold)
- apply (fast intro!: monoI)
-apply fast
-done
-
-declare C_while [simp del]
-
-lemma wp_is_pre: "|- {wp c Q} c {Q}"
-proof(induct c arbitrary: Q)
- case SKIP show ?case by auto
-next
- case Assign show ?case by auto
-next
- case Semi thus ?case by auto
-next
- case (Cond b c1 c2)
- let ?If = "IF b THEN c1 ELSE c2"
- show ?case
- proof(rule If)
- show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
- proof(rule strengthen_pre[OF _ Cond(1)])
- show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
- qed
- show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
- proof(rule strengthen_pre[OF _ Cond(2)])
- show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
- qed
- qed
-next
- case (While b c)
- let ?w = "WHILE b DO c"
- show ?case
- proof(rule While')
- show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
- proof(rule strengthen_pre[OF _ While(1)])
- show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
- qed
- show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
- qed
-qed
-
-lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
-proof(rule conseq)
- show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
- by (auto simp: hoare_valid_def wp_def)
- show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
- show "\<forall>s. Q s \<longrightarrow> Q s" by auto
-qed
-
-end
--- a/src/HOL/IMP/Hoare_Op.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-(* Title: HOL/IMP/Hoare_Op.thy
- Author: Tobias Nipkow
-*)
-
-header "Soundness and Completeness wrt Operational Semantics"
-
-theory Hoare_Op imports Hoare begin
-
-definition
- hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
- "|= {P}c{Q} = (!s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> P s --> Q t)"
-
-lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
-proof(induct rule: hoare.induct)
- case (While P b c)
- { fix s t
- assume "\<langle>WHILE b DO c,s\<rangle> \<longrightarrow>\<^sub>c t"
- hence "P s \<longrightarrow> P t \<and> \<not> b t"
- proof(induct "WHILE b DO c" s t)
- case WhileFalse thus ?case by blast
- next
- case WhileTrue thus ?case
- using While(2) unfolding hoare_valid_def by blast
- qed
-
- }
- thus ?case unfolding hoare_valid_def by blast
-qed (auto simp: hoare_valid_def)
-
-definition
- wp :: "com => assn => assn" where
- "wp c Q = (%s. !t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t --> Q t)"
-
-lemma wp_SKIP: "wp \<SKIP> Q = Q"
-by (simp add: wp_def)
-
-lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
-by (simp add: wp_def)
-
-lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_If:
- "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
-by (rule ext) (auto simp: wp_def)
-
-lemma wp_While_If:
- "wp (\<WHILE> b \<DO> c) Q s =
- wp (IF b THEN c;\<WHILE> b \<DO> c ELSE SKIP) Q s"
-unfolding wp_def by (metis equivD1 equivD2 unfold_while)
-
-lemma wp_While_True: "b s ==>
- wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
-by(simp add: wp_While_If wp_If wp_SKIP)
-
-lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
-by(simp add: wp_While_If wp_If wp_SKIP)
-
-lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
-
-lemma wp_is_pre: "|- {wp c Q} c {Q}"
-proof(induct c arbitrary: Q)
- case SKIP show ?case by auto
-next
- case Assign show ?case by auto
-next
- case Semi thus ?case by(auto intro: semi)
-next
- case (Cond b c1 c2)
- let ?If = "IF b THEN c1 ELSE c2"
- show ?case
- proof(rule If)
- show "|- {\<lambda>s. wp ?If Q s \<and> b s} c1 {Q}"
- proof(rule strengthen_pre[OF _ Cond(1)])
- show "\<forall>s. wp ?If Q s \<and> b s \<longrightarrow> wp c1 Q s" by auto
- qed
- show "|- {\<lambda>s. wp ?If Q s \<and> \<not> b s} c2 {Q}"
- proof(rule strengthen_pre[OF _ Cond(2)])
- show "\<forall>s. wp ?If Q s \<and> \<not> b s \<longrightarrow> wp c2 Q s" by auto
- qed
- qed
-next
- case (While b c)
- let ?w = "WHILE b DO c"
- have "|- {wp ?w Q} ?w {\<lambda>s. wp ?w Q s \<and> \<not> b s}"
- proof(rule hoare.While)
- show "|- {\<lambda>s. wp ?w Q s \<and> b s} c {wp ?w Q}"
- proof(rule strengthen_pre[OF _ While(1)])
- show "\<forall>s. wp ?w Q s \<and> b s \<longrightarrow> wp c (wp ?w Q) s" by auto
- qed
- qed
- thus ?case
- proof(rule weaken_post)
- show "\<forall>s. wp ?w Q s \<and> \<not> b s \<longrightarrow> Q s" by auto
- qed
-qed
-
-lemma hoare_relative_complete: assumes "|= {P}c{Q}" shows "|- {P}c{Q}"
-proof(rule strengthen_pre)
- show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
- by (auto simp: hoare_valid_def wp_def)
- show "|- {wp c Q} c {Q}" by(rule wp_is_pre)
-qed
-
-end
--- a/src/HOL/IMP/Live.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,212 +0,0 @@
-theory Live imports Natural
-begin
-
-text{* Which variables/locations does an expression depend on?
-Any set of variables that completely determine the value of the expression,
-in the worst case all locations: *}
-
-consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set"
-specification (Dep)
-dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> e s = e t"
-by(rule_tac x="%x. UNIV" in exI)(simp add: fun_eq_iff[symmetric])
-
-text{* The following definition of @{const Dep} looks very tempting
-@{prop"Dep e = {a. EX s t. (ALL x. x\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"}
-but does not work in case @{text e} depends on an infinite set of variables.
-For example, if @{term"e s"} tests if @{text s} is 0 at infinitely many locations. Then @{term"Dep e"} incorrectly yields the empty set!
-
-If we had a concrete representation of expressions, we would simply write
-a recursive free-variables function.
-*}
-
-primrec L :: "com \<Rightarrow> loc set \<Rightarrow> loc set" where
-"L SKIP A = A" |
-"L (x :== e) A = A-{x} \<union> Dep e" |
-"L (c1; c2) A = (L c1 \<circ> L c2) A" |
-"L (IF b THEN c1 ELSE c2) A = Dep b \<union> L c1 A \<union> L c2 A" |
-"L (WHILE b DO c) A = Dep b \<union> A \<union> L c A"
-
-primrec "kill" :: "com \<Rightarrow> loc set" where
-"kill SKIP = {}" |
-"kill (x :== e) = {x}" |
-"kill (c1; c2) = kill c1 \<union> kill c2" |
-"kill (IF b THEN c1 ELSE c2) = Dep b \<union> kill c1 \<inter> kill c2" |
-"kill (WHILE b DO c) = {}"
-
-primrec gen :: "com \<Rightarrow> loc set" where
-"gen SKIP = {}" |
-"gen (x :== e) = Dep e" |
-"gen (c1; c2) = gen c1 \<union> (gen c2-kill c1)" |
-"gen (IF b THEN c1 ELSE c2) = Dep b \<union> gen c1 \<union> gen c2" |
-"gen (WHILE b DO c) = Dep b \<union> gen c"
-
-lemma L_gen_kill: "L c A = gen c \<union> (A - kill c)"
-by(induct c arbitrary:A) auto
-
-lemma L_idemp: "L c (L c A) \<subseteq> L c A"
-by(fastsimp simp add:L_gen_kill)
-
-theorem L_sound: "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
- \<forall>x\<in>A. s' x = t' x"
-proof (induct c arbitrary: A s t s' t')
- case SKIP then show ?case by auto
-next
- case (Assign x e) then show ?case
- by (auto simp:update_def ball_Un dest!: dep_on)
-next
- case (Semi c1 c2)
- from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
- by auto
- from Semi(5) obtain t'' where t1: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>c2,t''\<rangle> \<longrightarrow>\<^sub>c t'"
- by auto
- show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
-next
- case (Cond b c1 c2)
- show ?case
- proof cases
- assume "b s"
- hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
- have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
- hence t: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
- show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
- next
- assume "\<not> b s"
- hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
- have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
- hence t: "\<langle>c2,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
- show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
- qed
-next
- case (While b c) note IH = this
- { fix cw
- have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>cw,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
- \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
- proof (induct arbitrary: t A pred:evalc)
- case WhileFalse
- have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
- then have "t' = t" using WhileFalse by auto
- then show ?case using WhileFalse by auto
- next
- case (WhileTrue _ s _ s'' s')
- have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
- have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
- then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
- using WhileTrue(6,7) by auto
- have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
- using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(6,8)
- by (auto simp:L_gen_kill)
- then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
- then show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
- qed auto }
--- "a terser version"
- { let ?w = "While b c"
- have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>?w,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
- \<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
- proof (induct ?w s s' arbitrary: t A pred:evalc)
- case WhileFalse
- have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
- then have "t' = t" using WhileFalse by auto
- then show ?case using WhileFalse by simp
- next
- case (WhileTrue s s'' s')
- have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
- then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'"
- using WhileTrue(6,7) by auto
- have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
- using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(7)
- by (auto simp:L_gen_kill)
- then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
- then show ?case using WhileTrue(5) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
- qed }
- from this[OF IH(3) IH(4,2)] show ?case by metis
-qed
-
-
-primrec bury :: "com \<Rightarrow> loc set \<Rightarrow> com" where
-"bury SKIP _ = SKIP" |
-"bury (x :== e) A = (if x:A then x:== e else SKIP)" |
-"bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" |
-"bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" |
-"bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \<union> A \<union> L c A))"
-
-theorem bury_sound:
- "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury c A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
- \<forall>x\<in>A. s' x = t' x"
-proof (induct c arbitrary: A s t s' t')
- case SKIP then show ?case by auto
-next
- case (Assign x e) then show ?case
- by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on)
-next
- case (Semi c1 c2)
- from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'"
- by auto
- from Semi(5) obtain t'' where t1: "\<langle>bury c1 (L c2 A),t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>bury c2 A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
- by auto
- show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp
-next
- case (Cond b c1 c2)
- show ?case
- proof cases
- assume "b s"
- hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp
- have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
- hence t: "\<langle>bury c1 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
- show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp
- next
- assume "\<not> b s"
- hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto
- have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on)
- hence t: "\<langle>bury c2 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto
- show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp
- qed
-next
- case (While b c) note IH = this
- { fix cw
- have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>bury cw A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
- \<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
- proof (induct arbitrary: t A pred:evalc)
- case WhileFalse
- have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
- then have "t' = t" using WhileFalse by auto
- then show ?case using WhileFalse by auto
- next
- case (WhileTrue _ s _ s'' s')
- have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp
- have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
- then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
- and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
- using WhileTrue(6,7) by auto
- have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
- using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8)
- by (auto simp:L_gen_kill)
- moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
- ultimately show ?case
- using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
- qed auto }
- { let ?w = "While b c"
- have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury ?w A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow>
- \<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x"
- proof (induct ?w s s' arbitrary: t A pred:evalc)
- case WhileFalse
- have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on)
- then have "t' = t" using WhileFalse by auto
- then show ?case using WhileFalse by simp
- next
- case (WhileTrue s s'' s')
- have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on)
- then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''"
- and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'"
- using WhileTrue(6,7) by auto
- have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x"
- using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(7)
- by (auto simp:L_gen_kill)
- then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto
- then show ?case
- using WhileTrue(5) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis
- qed }
- from this[OF IH(3) IH(4,2)] show ?case by metis
-qed
-
-
-end
\ No newline at end of file
--- a/src/HOL/IMP/Machines.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-theory Machines
-imports Natural
-begin
-
-lemma converse_in_rel_pow_eq:
- "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
-apply(rule iffI)
- apply(blast elim:rel_pow_E2)
-apply (auto simp: rel_pow_commute[symmetric])
-done
-
-subsection "Instructions"
-
-text {* There are only three instructions: *}
-datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat
-
-type_synonym instrs = "instr list"
-
-subsection "M0 with PC"
-
-inductive_set
- exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
- and exec01' :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
- ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
- for P :: "instr list"
-where
- "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)"
-| SET: "\<lbrakk> n<size P; P!n = SET x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>"
-| JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>"
-| JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk>
- \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>"
-| JMPB: "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>"
-
-abbreviation
- exec0s :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
- ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) where
- "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^*"
-
-abbreviation
- exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
- ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) where
- "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^^n"
-
-subsection "M0 with lists"
-
-text {* We describe execution of programs in the machine by
- an operational (small step) semantics:
-*}
-
-type_synonym config = "instrs \<times> instrs \<times> state"
-
-
-inductive_set
- stepa1 :: "(config \<times> config)set"
- and stepa1' :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
- ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
-where
- "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : stepa1"
-| "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>"
-| "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>"
-| "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk>
- \<Longrightarrow> \<langle>JMPF b i # p, q, s\<rangle> -1\<rightarrow> \<langle>drop i p, rev(take i p) @ JMPF b i # q, s\<rangle>"
-| "i \<le> size q
- \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>"
-
-abbreviation
- stepa :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool"
- ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where
- "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^*)"
-
-abbreviation
- stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
- ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where
- "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^^i)"
-
-inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1"
-
-lemma exec_simp[simp]:
- "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of
- SET x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q |
- JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q
- else n \<le> size p \<and> p' = drop n p \<and> q' = rev(take n p) @ i # q) |
- JMPB n \<Rightarrow> n \<le> size q \<and> t=s \<and> p' = rev(take n q) @ i # p \<and> q' = drop n q)"
-apply(rule iffI)
-defer
-apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm)
-apply(erule execE)
-apply(simp_all)
-done
-
-lemma execn_simp[simp]:
-"(\<langle>i#p,q,s\<rangle> -n\<rightarrow> \<langle>p'',q'',u\<rangle>) =
- (n=0 \<and> p'' = i#p \<and> q'' = q \<and> u = s \<or>
- ((\<exists>m p' q' t. n = Suc m \<and>
- \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -m\<rightarrow> \<langle>p'',q'',u\<rangle>)))"
-by(subst converse_in_rel_pow_eq, simp)
-
-
-lemma exec_star_simp[simp]: "(\<langle>i#p,q,s\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>) =
- (p'' = i#p & q''=q & u=s |
- (\<exists>p' q' t. \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>))"
-apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp)
-apply(blast)
-done
-
-declare nth_append[simp]
-
-lemma rev_revD: "rev xs = rev ys \<Longrightarrow> xs = ys"
-by simp
-
-lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)"
-apply(rule iffI)
- apply(rule rev_revD, simp)
-apply fastsimp
-done
-
-lemma direction1:
- "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow>
- rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>"
-apply(induct set: stepa1)
- apply(simp add:exec01.SET)
- apply(fastsimp intro:exec01.JMPFT)
- apply simp
- apply(rule exec01.JMPFF)
- apply simp
- apply fastsimp
- apply simp
- apply simp
- apply simp
-apply(fastsimp simp add:exec01.JMPB)
-done
-
-(*
-lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
-apply(induct xs)
- apply simp_all
-apply(case_tac i)
-apply simp_all
-done
-
-lemma rev_drop: "\<And>i. rev (drop i xs) = take (length xs - i) (rev xs)"
-apply(induct xs)
- apply simp_all
-apply(case_tac i)
-apply simp_all
-done
-*)
-
-lemma direction2:
- "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
- rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
- rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>"
-apply(induct arbitrary: p q p' q' set: exec01)
- apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
- apply(drule sym)
- apply simp
- apply(rule rev_revD)
- apply simp
- apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
- apply(drule sym)
- apply simp
- apply(rule rev_revD)
- apply simp
- apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+
- apply(drule sym)
- apply simp
- apply(rule rev_revD)
- apply simp
-apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
-apply(drule sym)
-apply(simp add:rev_take)
-apply(rule rev_revD)
-apply(simp add:rev_drop)
-done
-
-
-theorem M_eqiv:
-"(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) =
- (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)"
- by (blast dest: direction1 direction2)
-
-end
--- a/src/HOL/IMP/Natural.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,354 +0,0 @@
-(* Title: HOL/IMP/Natural.thy
- Author: Tobias Nipkow & Robert Sandner, TUM
- Isar Version: Gerwin Klein, 2001; additional proofs by Lawrence Paulson
- Copyright 1996 TUM
-*)
-
-header "Natural Semantics of Commands"
-
-theory Natural imports Com begin
-
-subsection "Execution of commands"
-
-text {*
- We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
- in state @{text s}, terminates in state @{text s'}}. Formally,
- @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
- @{text "(c,s,s')"} is part of the relation @{text evalc}}:
-*}
-
-definition
- update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900) where
- "update = fun_upd"
-
-notation (xsymbols)
- update ("_/[_ \<mapsto> /_]" [900,0,0] 900)
-
-text {* Disable conflicting syntax from HOL Map theory. *}
-
-no_syntax
- "_maplet" :: "['a, 'a] => maplet" ("_ /|->/ _")
- "_maplets" :: "['a, 'a] => maplet" ("_ /[|->]/ _")
- "" :: "maplet => maplets" ("_")
- "_Maplets" :: "[maplet, maplets] => maplets" ("_,/ _")
- "_MapUpd" :: "['a ~=> 'b, maplets] => 'a ~=> 'b" ("_/'(_')" [900,0]900)
- "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])")
-
-text {*
- The big-step execution relation @{text evalc} is defined inductively:
-*}
-inductive
- evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
-where
- Skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
-| Assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
-
-| Semi: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-| IfTrue: "b s \<Longrightarrow> \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-| IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-| WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
-| WhileTrue: "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
- \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
-
-text {*
-The induction principle induced by this definition looks like this:
-
-@{thm [display] evalc.induct [no_vars]}
-
-
-(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
- meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
-*}
-
-text {*
- The rules of @{text evalc} are syntax directed, i.e.~for each
- syntactic category there is always only one rule applicable. That
- means we can use the rules in both directions. This property is called rule inversion.
-*}
-inductive_cases skipE [elim!]: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
-inductive_cases semiE [elim!]: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-inductive_cases assignE [elim!]: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
-inductive_cases ifE [elim!]: "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-inductive_cases whileE [elim]: "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-text {* The next proofs are all trivial by rule inversion.
-*}
-
-inductive_simps
- skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'"
- and assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s'"
- and semi: "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
-
-lemma ifTrue:
- "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
- by auto
-
-lemma ifFalse:
- "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'"
- by auto
-
-lemma whileFalse:
- "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
- by auto
-
-lemma whileTrue:
- "b s \<Longrightarrow>
- \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
- (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
- by auto
-
-text "Again, Isabelle may use these rules in automatic proofs:"
-lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
-
-subsection "Equivalence of statements"
-
-text {*
- We call two statements @{text c} and @{text c'} equivalent wrt.~the
- big-step semantics when \emph{@{text c} started in @{text s} terminates
- in @{text s'} iff @{text c'} started in the same @{text s} also terminates
- in the same @{text s'}}. Formally:
-*}
-definition
- equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _" [56, 56] 55) where
- "c \<sim> c' = (\<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s')"
-
-text {*
- Proof rules telling Isabelle to unfold the definition
- if there is something to be proved about equivalent
- statements: *}
-lemma equivI [intro!]:
- "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
- by (unfold equiv_c_def) blast
-
-lemma equivD1:
- "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
- by (unfold equiv_c_def) blast
-
-lemma equivD2:
- "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'"
- by (unfold equiv_c_def) blast
-
-text {*
- As an example, we show that loop unfolding is an equivalence
- transformation on programs:
-*}
-lemma unfold_while:
- "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
-proof -
- -- "to show the equivalence, we look at the derivation tree for"
- -- "each side and from that construct a derivation tree for the other side"
- { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
- -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
- -- "then both statements do nothing:"
- hence "\<not>b s \<Longrightarrow> s = s'" by blast
- hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- moreover
- -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
- -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
- { assume b: "b s"
- with w obtain s'' where
- "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
- -- "now we can build a derivation tree for the @{text \<IF>}"
- -- "first, the body of the True-branch:"
- hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi)
- -- "then the whole @{text \<IF>}"
- with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
- }
- ultimately
- -- "both cases together give us what we want:"
- have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- }
- moreover
- -- "now the other direction:"
- { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
- -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
- -- "of the @{text \<IF>} is executed, and both statements do nothing:"
- hence "\<not>b s \<Longrightarrow> s = s'" by blast
- hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- moreover
- -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
- -- {* then this time only the @{text IfTrue} rule can have be used *}
- { assume b: "b s"
- with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
- -- "and for this, only the Semi-rule is applicable:"
- then obtain s'' where
- "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
- -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
- with b
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
- }
- ultimately
- -- "both cases together again give us what we want:"
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- }
- ultimately
- show ?thesis by blast
-qed
-
-text {*
- Happily, such lengthy proofs are seldom necessary. Isabelle can prove many such facts automatically.
-*}
-
-lemma
- "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
-by blast
-
-lemma triv_if:
- "(\<IF> b \<THEN> c \<ELSE> c) \<sim> c"
-by blast
-
-lemma commute_if:
- "(\<IF> b1 \<THEN> (\<IF> b2 \<THEN> c11 \<ELSE> c12) \<ELSE> c2)
- \<sim>
- (\<IF> b2 \<THEN> (\<IF> b1 \<THEN> c11 \<ELSE> c2) \<ELSE> (\<IF> b1 \<THEN> c12 \<ELSE> c2))"
-by blast
-
-lemma while_equiv:
- "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<sim> c' \<Longrightarrow> (c0 = \<WHILE> b \<DO> c) \<Longrightarrow> \<langle>\<WHILE> b \<DO> c', s\<rangle> \<longrightarrow>\<^sub>c u"
-by (induct rule: evalc.induct) (auto simp add: equiv_c_def)
-
-lemma equiv_while:
- "c \<sim> c' \<Longrightarrow> (\<WHILE> b \<DO> c) \<sim> (\<WHILE> b \<DO> c')"
-by (simp add: equiv_c_def) (metis equiv_c_def while_equiv)
-
-
-text {*
- Program equivalence is an equivalence relation.
-*}
-
-lemma equiv_refl:
- "c \<sim> c"
-by blast
-
-lemma equiv_sym:
- "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c1"
-by (auto simp add: equiv_c_def)
-
-lemma equiv_trans:
- "c1 \<sim> c2 \<Longrightarrow> c2 \<sim> c3 \<Longrightarrow> c1 \<sim> c3"
-by (auto simp add: equiv_c_def)
-
-text {*
- Program constructions preserve equivalence.
-*}
-
-lemma equiv_semi:
- "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (c1; c2) \<sim> (c1'; c2')"
-by (force simp add: equiv_c_def)
-
-lemma equiv_if:
- "c1 \<sim> c1' \<Longrightarrow> c2 \<sim> c2' \<Longrightarrow> (\<IF> b \<THEN> c1 \<ELSE> c2) \<sim> (\<IF> b \<THEN> c1' \<ELSE> c2')"
-by (force simp add: equiv_c_def)
-
-lemma while_never: "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> c \<noteq> \<WHILE> (\<lambda>s. True) \<DO> c1"
-apply (induct rule: evalc.induct)
-apply auto
-done
-
-lemma equiv_while_True:
- "(\<WHILE> (\<lambda>s. True) \<DO> c1) \<sim> (\<WHILE> (\<lambda>s. True) \<DO> c2)"
-by (blast dest: while_never)
-
-
-subsection "Execution is deterministic"
-
-text {*
-This proof is automatic.
-*}
-theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = t"
-by (induct arbitrary: u rule: evalc.induct) blast+
-
-
-text {*
-The following proof presents all the details:
-*}
-theorem com_det:
- assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
- shows "u = t"
- using assms
-proof (induct arbitrary: u set: evalc)
- fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s" by blast
-next
- fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s[x \<mapsto> a s]" by blast
-next
- fix c0 c1 s s1 s2 u
- assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
- assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
- assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
- then obtain s' where
- c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
- c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
- by auto
-
- from c0 IH0 have "s'=s2" by blast
- with c1 IH1 show "u=s1" by blast
-next
- fix b c0 c1 s s1 u
- assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
- assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
- hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
- with IH show "u = s1" by blast
-next
- fix b c0 c1 s s1 u
- assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
- assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
- hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by blast
- with IH show "u = s1" by blast
-next
- fix b c s u
- assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s" by blast
-next
- fix b c s s1 s2 u
- assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
- assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
- assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
- then obtain s' where
- c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
- w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
- by auto
-
- from c "IH\<^sub>c" have "s' = s2" by blast
- with w "IH\<^sub>w" show "u = s1" by blast
-qed
-
-
-text {*
- This is the proof as you might present it in a lecture. The remaining
- cases are simple enough to be proved automatically:
-*}
-theorem
- assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" and "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u"
- shows "u = t"
- using assms
-proof (induct arbitrary: u)
- -- "the simple @{text \<SKIP>} case for demonstration:"
- fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s" by blast
-next
- -- "and the only really interesting case, @{text \<WHILE>}:"
- fix b c s s1 s2 u
- assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
- assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
-
- assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
- then obtain s' where
- c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
- w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
- by auto
-
- from c "IH\<^sub>c" have "s' = s2" by blast
- with w "IH\<^sub>w" show "u = s1" by blast
-qed blast+ -- "prove the rest automatically"
-
-end
--- a/src/HOL/IMP/Transition.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,644 +0,0 @@
-(* Title: HOL/IMP/Transition.thy
- Author: Tobias Nipkow & Robert Sandner, TUM
- Isar Version: Gerwin Klein, 2001
- Copyright 1996 TUM
-*)
-
-header "Transition Semantics of Commands"
-
-theory Transition imports Natural begin
-
-subsection "The transition relation"
-
-text {*
- We formalize the transition semantics as in \cite{Nielson}. This
- makes some of the rules a bit more intuitive, but also requires
- some more (internal) formal overhead.
-
- Since configurations that have terminated are written without
- a statement, the transition relation is not
- @{typ "((com \<times> state) \<times> (com \<times> state)) set"}
- but instead:
- @{typ "((com option \<times> state) \<times> (com option \<times> state)) set"}
-
- Some syntactic sugar that we will use to hide the
- @{text option} part in configurations:
-*}
-abbreviation
- angle :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") where
- "<c,s> == (Some c, s)"
-abbreviation
- angle2 :: "state \<Rightarrow> com option \<times> state" ("<_>") where
- "<s> == (None, s)"
-
-notation (xsymbols)
- angle ("\<langle>_,_\<rangle>") and
- angle2 ("\<langle>_\<rangle>")
-
-notation (HTML output)
- angle ("\<langle>_,_\<rangle>") and
- angle2 ("\<langle>_\<rangle>")
-
-text {*
- Now, finally, we are set to write down the rules for our small step semantics:
-*}
-inductive_set
- evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
- and evalc1' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
- ("_ \<longrightarrow>\<^sub>1 _" [60,60] 61)
-where
- "cs \<longrightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1"
-| Skip: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"
-| Assign: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
-
-| Semi1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
-| Semi2: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0',s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0';c1,s'\<rangle>"
-
-| IfTrue: "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>"
-| IfFalse: "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c2,s\<rangle>"
-
-| While: "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s\<rangle>"
-
-lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs"
-
-text {*
- More syntactic sugar for the transition relation, and its
- iteration.
-*}
-abbreviation
- evalcn :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
- ("_ -_\<rightarrow>\<^sub>1 _" [60,60,60] 60) where
- "cs -n\<rightarrow>\<^sub>1 cs' == (cs,cs') \<in> evalc1^^n"
-
-abbreviation
- evalc' :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
- ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [60,60] 60) where
- "cs \<longrightarrow>\<^sub>1\<^sup>* cs' == (cs,cs') \<in> evalc1^*"
-
-(*<*)
-declare rel_pow_Suc_E2 [elim!]
-(*>*)
-
-text {*
- As for the big step semantics you can read these rules in a
- syntax directed way:
-*}
-lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)"
- by (induct y, rule, cases set: evalc1, auto)
-
-lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
- by (induct y, rule, cases set: evalc1, auto)
-
-lemma Cond_1:
- "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y = ((b s \<longrightarrow> y = \<langle>c1, s\<rangle>) \<and> (\<not>b s \<longrightarrow> y = \<langle>c2, s\<rangle>))"
- by (induct y, rule, cases set: evalc1, auto)
-
-lemma While_1:
- "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s\<rangle>)"
- by (induct y, rule, cases set: evalc1, auto)
-
-lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
-
-
-subsection "Examples"
-
-lemma
- "s x = 0 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x \<mapsto> 1]\<rangle>"
- (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
-proof -
- let ?c = "x:== \<lambda>s. s x+1"
- let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
- assume [simp]: "s x = 0"
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" ..
- also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
- also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1) simp
- also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
- also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
- also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
- finally show ?thesis ..
-qed
-
-lemma
- "s x = 2 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> (x:== \<lambda>s. s x+1), s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'"
- (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
-proof -
- let ?c = "x:== \<lambda>s. s x+1"
- let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
- assume [simp]: "s x = 2"
- note update_def [simp]
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" ..
- also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
- also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1) simp
- also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
- also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
- also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1) simp
- also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
- also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
- also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1) simp
- oops
-
-subsection "Basic properties"
-
-text {*
- There are no \emph{stuck} programs:
-*}
-lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
-proof (induct c)
- -- "case Semi:"
- fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y"
- then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
- then obtain c1' s' where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<or> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1',s'\<rangle>"
- by (cases y, cases "fst y") auto
- thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
-next
- -- "case If:"
- fix b c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" and "\<exists>y. \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>1 y"
- thus "\<exists>y. \<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y" by (cases "b s") auto
-qed auto -- "the rest is trivial"
-
-text {*
- If a configuration does not contain a statement, the program
- has terminated and there is no next configuration:
-*}
-lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P"
- by (induct y, auto elim: evalc1.cases)
-
-lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>"
- by (induct set: rtrancl) auto
-
-(*<*)
-(* FIXME: relpow.simps don't work *)
-lemmas [simp del] = relpow.simps
-lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R ^^ 0 = Id" by (simp add: relpow.simps)
-lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R ^^ Suc 0 = R" by (simp add: relpow.simps)
-
-(*>*)
-lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
- by (cases n) auto
-
-lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1"
- by (cases n) auto
-
-subsection "Equivalence to natural semantics (after Nielson and Nielson)"
-
-text {*
- We first need two lemmas about semicolon statements:
- decomposition and composition.
-*}
-lemma semiD:
- "\<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
- \<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> n = i+j"
-proof (induct n arbitrary: c1 c2 s s'')
- case 0
- then show ?case by simp
-next
- case (Suc n)
-
- from `\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
- obtain co s''' where
- 1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s''')" and
- n: "(co, s''') -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
- by auto
-
- from 1
- show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j"
- (is "\<exists>i j s'. ?Q i j s'")
- proof (cases set: evalc1)
- case Semi1
- from `co = Some c2` and `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'''\<rangle>` and 1 n
- have "?Q 1 n s'''" by simp
- thus ?thesis by blast
- next
- case (Semi2 c1')
- note c1 = `\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'''\<rangle>`
- with `co = Some (c1'; c2)` and n
- have "\<langle>c1'; c2, s'''\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
- with Suc.hyps obtain i j s0 where
- c1': "\<langle>c1',s'''\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
- c2: "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
- i: "n = i+j"
- by fast
-
- from c1 c1'
- have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto intro: rel_pow_Suc_I2)
- with c2 i
- have "?Q (i+1) j s0" by simp
- thus ?thesis by blast
- qed
-qed
-
-
-lemma semiI:
- "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof (induct n arbitrary: c0 s s'')
- case 0
- from `\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
- have False by simp
- thus ?case ..
-next
- case (Suc n)
- note c0 = `\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
- note c1 = `\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
- note IH = `\<And>c0 s s''.
- \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>`
- from c0 obtain y where
- 1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
- from 1 obtain c0' s0' where
- "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>"
- by (cases y, cases "fst y") auto
- moreover
- { assume y: "y = \<langle>s0'\<rangle>"
- with n have "s'' = s0'" by simp
- with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast
- with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
- }
- moreover
- { assume y: "y = \<langle>c0', s0'\<rangle>"
- with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
- with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
- moreover
- from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast
- hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast
- ultimately
- have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
- }
- ultimately
- show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
-qed
-
-text {*
- The easy direction of the equivalence proof:
-*}
-lemma evalc_imp_evalc1:
- assumes "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- shows "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- using assms
-proof induct
- fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
-next
- fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
-next
- fix c0 c1 s s'' s'
- assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
- then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
- moreover
- assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- ultimately
- show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
-next
- fix s::state and b c0 c1 s'
- assume "b s"
- hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
- also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
-next
- fix s::state and b c0 c1 s'
- assume "\<not>b s"
- hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
- also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
-next
- fix b c and s::state
- assume b: "\<not>b s"
- let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
- have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
- also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
- also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
- finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
-next
- fix b c s s'' s'
- let ?w = "\<WHILE> b \<DO> c"
- let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
- assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
- assume b: "b s"
- have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
- also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
- also
- from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
- with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
- finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
-qed
-
-text {*
- Finally, the equivalence theorem:
-*}
-theorem evalc_equiv_evalc1:
- "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof
- assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- then show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
-next
- assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
- moreover
- have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- proof (induct arbitrary: c s s' rule: less_induct)
- fix n
- assume IH: "\<And>m c s s'. m < n \<Longrightarrow> \<langle>c,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- fix c s s'
- assume c: "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
- then obtain m where n: "n = Suc m" by (cases n) auto
- with c obtain y where
- c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
- show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- proof (cases c)
- case SKIP
- with c n show ?thesis by auto
- next
- case Assign
- with c n show ?thesis by auto
- next
- fix c1 c2 assume semi: "c = (c1; c2)"
- with c obtain i j s'' where
- c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
- c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
- ij: "n = i+j"
- by (blast dest: semiD)
- from c1 c2 obtain
- "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
- with ij obtain
- i: "i < n" and j: "j < n" by simp
- from IH i c1
- have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" .
- moreover
- from IH j c2
- have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" .
- moreover
- note semi
- ultimately
- show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- next
- fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
- { assume True: "b s = True"
- with If c n
- have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
- with n IH
- have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- with If True
- have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- }
- moreover
- { assume False: "b s = False"
- with If c n
- have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
- with n IH
- have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- with If False
- have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- }
- ultimately
- show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
- next
- fix b c' assume w: "c = \<WHILE> b \<DO> c'"
- with c n
- have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
- (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
- with n IH
- have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
- moreover note unfold_while [of b c']
- -- {* @{thm unfold_while [of b c']} *}
- ultimately
- have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
- with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
- qed
- qed
- ultimately
- show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
-qed
-
-
-subsection "Winskel's Proof"
-
-declare rel_pow_0_E [elim!]
-
-text {*
- Winskel's small step rules are a bit different \cite{Winskel};
- we introduce their equivalents as derived rules:
-*}
-lemma whileFalse1 [intro]:
- "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>")
-proof -
- assume "\<not>b s"
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
- also from `\<not>b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
- also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
- finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
-qed
-
-lemma whileTrue1 [intro]:
- "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>"
- (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
-proof -
- assume "b s"
- have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
- also from `b s` have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
- finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
-qed
-
-inductive_cases evalc1_SEs:
- "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
- "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
- "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
- "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
- "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-
-inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 (co, s')"
-
-declare evalc1_SEs [elim!]
-
-lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
-apply (induct set: evalc)
-
--- SKIP
-apply blast
-
--- ASSIGN
-apply fast
-
--- SEMI
-apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
-
--- IF
-apply (fast intro: converse_rtrancl_into_rtrancl)
-apply (fast intro: converse_rtrancl_into_rtrancl)
-
--- WHILE
-apply blast
-apply (blast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
-
-done
-
-
-lemma lemma2:
- "\<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<Longrightarrow> \<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n"
-apply (induct n arbitrary: c d s u)
- -- "case n = 0"
- apply fastsimp
--- "induction step"
-apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
- elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
-done
-
-lemma evalc1_impl_evalc:
- "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct c arbitrary: s t)
-apply (safe dest!: rtrancl_imp_UN_rel_pow)
-
--- SKIP
-apply (simp add: SKIP_n)
-
--- ASSIGN
-apply (fastsimp elim: rel_pow_E2)
-
--- SEMI
-apply (fast dest!: rel_pow_imp_rtrancl lemma2)
-
--- IF
-apply (erule rel_pow_E2)
-apply simp
-apply (fast dest!: rel_pow_imp_rtrancl)
-
--- "WHILE, induction on the length of the computation"
-apply (rename_tac b c s t n)
-apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
-apply (rule_tac x = "s" in spec)
-apply (induct_tac n rule: nat_less_induct)
-apply (intro strip)
-apply (erule rel_pow_E2)
- apply simp
-apply (simp only: split_paired_all)
-apply (erule evalc1_E)
-
-apply simp
-apply (case_tac "b x")
- -- WhileTrue
- apply (erule rel_pow_E2)
- apply simp
- apply (clarify dest!: lemma2)
- apply atomize
- apply (erule allE, erule allE, erule impE, assumption)
- apply (erule_tac x=mb in allE, erule impE, fastsimp)
- apply blast
--- WhileFalse
-apply (erule rel_pow_E2)
- apply simp
-apply (simp add: SKIP_n)
-done
-
-
-text {* proof of the equivalence of evalc and evalc1 *}
-lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
- by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
-
-
-subsection "A proof without n"
-
-text {*
- The inductions are a bit awkward to write in this section,
- because @{text None} as result statement in the small step
- semantics doesn't have a direct counterpart in the big step
- semantics.
-
- Winskel's small step rule set (using the @{text "\<SKIP>"} statement
- to indicate termination) is better suited for this proof.
-*}
-
-lemma my_lemma1:
- assumes "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>"
- and "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
- shows "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
-proof -
- -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
- from assms
- have "\<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
- apply (induct rule: converse_rtrancl_induct2)
- apply simp
- apply (rename_tac c s')
- apply simp
- apply (rule conjI)
- apply fast
- apply clarify
- apply (case_tac c)
- apply (auto intro: converse_rtrancl_into_rtrancl)
- done
- then show ?thesis by simp
-qed
-
-lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
-apply (induct set: evalc)
-
--- SKIP
-apply fast
-
--- ASSIGN
-apply fast
-
--- SEMI
-apply (fast intro: my_lemma1)
-
--- IF
-apply (fast intro: converse_rtrancl_into_rtrancl)
-apply (fast intro: converse_rtrancl_into_rtrancl)
-
--- WHILE
-apply fast
-apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
-
-done
-
-text {*
- The opposite direction is based on a Coq proof done by Ranan Fraer and
- Yves Bertot. The following sketch is from an email by Ranan Fraer.
-
-\begin{verbatim}
-First we've broke it into 2 lemmas:
-
-Lemma 1
-((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
-
-This is a quick one, dealing with the cases skip, assignment
-and while_false.
-
-Lemma 2
-((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
- =>
-<c,s> -c-> t
-
-This is proved by rule induction on the -*-> relation
-and the induction step makes use of a third lemma:
-
-Lemma 3
-((c,s) --> (c',s')) /\ <c',s'> -c'-> t
- =>
-<c,s> -c-> t
-
-This captures the essence of the proof, as it shows that <c',s'>
-behaves as the continuation of <c,s> with respect to the natural
-semantics.
-The proof of Lemma 3 goes by rule induction on the --> relation,
-dealing with the cases sequence1, sequence2, if_true, if_false and
-while_true. In particular in the case (sequence1) we make use again
-of Lemma 1.
-\end{verbatim}
-*}
-
-inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
-
-lemma FB_lemma3:
- "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
- \<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
- by (induct arbitrary: t set: evalc1)
- (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
-
-lemma FB_lemma2:
- "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
- \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
- apply (induct rule: converse_rtrancl_induct2, force)
- apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
- done
-
-lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
- by (fastsimp dest: FB_lemma2)
-
-end
--- a/src/HOL/IMP/VC.thy Wed Jun 01 21:35:34 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,137 +0,0 @@
-(* Title: HOL/IMP/VC.thy
- Author: Tobias Nipkow
-
-acom: annotated commands
-vc: verification-conditions
-awp: weakest (liberal) precondition
-*)
-
-header "Verification Conditions"
-
-theory VC imports Hoare_Op begin
-
-datatype acom = Askip
- | Aass loc aexp
- | Asemi acom acom
- | Aif bexp acom acom
- | Awhile bexp assn acom
-
-primrec awp :: "acom => assn => assn"
-where
- "awp Askip Q = Q"
-| "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
-| "awp (Asemi c d) Q = awp c (awp d Q)"
-| "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
-| "awp (Awhile b I c) Q = I"
-
-primrec vc :: "acom => assn => assn"
-where
- "vc Askip Q = (\<lambda>s. True)"
-| "vc (Aass x a) Q = (\<lambda>s. True)"
-| "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
-| "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
-| "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
- (I s & b s --> awp c I s) & vc c I s)"
-
-primrec astrip :: "acom => com"
-where
- "astrip Askip = SKIP"
-| "astrip (Aass x a) = (x:==a)"
-| "astrip (Asemi c d) = (astrip c;astrip d)"
-| "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
-| "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
-
-(* simultaneous computation of vc and awp: *)
-primrec vcawp :: "acom => assn => assn \<times> assn"
-where
- "vcawp Askip Q = (\<lambda>s. True, Q)"
-| "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
-| "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
- (vcc,wpc) = vcawp c wpd
- in (\<lambda>s. vcc s & vcd s, wpc))"
-| "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
- (vcc,wpc) = vcawp c Q
- in (\<lambda>s. vcc s & vcd s,
- \<lambda>s.(b s --> wpc s) & (~b s --> wpd s)))"
-| "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
- in (\<lambda>s. (I s & ~b s --> Q s) &
- (I s & b s --> wpc s) & vcc s, I))"
-
-(*
-Soundness and completeness of vc
-*)
-
-declare hoare.conseq [intro]
-
-
-lemma vc_sound: "(ALL s. vc c Q s) \<Longrightarrow> |- {awp c Q} astrip c {Q}"
-proof(induct c arbitrary: Q)
- case (Awhile b I c)
- show ?case
- proof(simp, rule While')
- from `\<forall>s. vc (Awhile b I c) Q s`
- have vc: "ALL s. vc c I s" and IQ: "ALL s. I s \<and> \<not> b s \<longrightarrow> Q s" and
- awp: "ALL s. I s & b s --> awp c I s" by simp_all
- from vc have "|- {awp c I} astrip c {I}" using Awhile.hyps by blast
- with awp show "|- {\<lambda>s. I s \<and> b s} astrip c {I}"
- by(rule strengthen_pre)
- show "\<forall>s. I s \<and> \<not> b s \<longrightarrow> Q s" by(rule IQ)
- qed
-qed auto
-
-
-lemma awp_mono:
- "(!s. P s --> Q s) ==> awp c P s ==> awp c Q s"
-proof (induct c arbitrary: P Q s)
- case Asemi thus ?case by simp metis
-qed simp_all
-
-lemma vc_mono:
- "(!s. P s --> Q s) ==> vc c P s ==> vc c Q s"
-proof(induct c arbitrary: P Q)
- case Asemi thus ?case by simp (metis awp_mono)
-qed simp_all
-
-lemma vc_complete: assumes der: "|- {P}c{Q}"
- shows "(\<exists>ac. astrip ac = c & (\<forall>s. vc ac Q s) & (\<forall>s. P s --> awp ac Q s))"
- (is "? ac. ?Eq P c Q ac")
-using der
-proof induct
- case skip
- show ?case (is "? ac. ?C ac")
- proof show "?C Askip" by simp qed
-next
- case (ass P x a)
- show ?case (is "? ac. ?C ac")
- proof show "?C(Aass x a)" by simp qed
-next
- case (semi P c1 Q c2 R)
- from semi.hyps obtain ac1 where ih1: "?Eq P c1 Q ac1" by fast
- from semi.hyps obtain ac2 where ih2: "?Eq Q c2 R ac2" by fast
- show ?case (is "? ac. ?C ac")
- proof
- show "?C(Asemi ac1 ac2)"
- using ih1 ih2 by simp (fast elim!: awp_mono vc_mono)
- qed
-next
- case (If P b c1 Q c2)
- from If.hyps obtain ac1 where ih1: "?Eq (%s. P s & b s) c1 Q ac1" by fast
- from If.hyps obtain ac2 where ih2: "?Eq (%s. P s & ~b s) c2 Q ac2" by fast
- show ?case (is "? ac. ?C ac")
- proof
- show "?C(Aif b ac1 ac2)"
- using ih1 ih2 by simp
- qed
-next
- case (While P b c)
- from While.hyps obtain ac where ih: "?Eq (%s. P s & b s) c P ac" by fast
- show ?case (is "? ac. ?C ac")
- proof show "?C(Awhile b P ac)" using ih by simp qed
-next
- case conseq thus ?case by(fast elim!: awp_mono vc_mono)
-qed
-
-lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
- by (induct c arbitrary: Q) (simp_all add: Let_def)
-
-end
--- a/src/HOL/IsaMakefile Wed Jun 01 21:35:34 2011 +0200
+++ b/src/HOL/IsaMakefile Wed Jun 01 21:50:49 2011 +0200
@@ -525,9 +525,9 @@
HOL-IMP: HOL $(LOG)/HOL-IMP.gz
-$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy \
- IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
- IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy \
+$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
+ IMP/Big_Step.thy IMP/Com.thy IMP/Compiler.thy IMP/Denotation.thy \
+ IMP/Small_Step.thy IMP/Star.thy \
IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP