--- a/src/HOL/IMP/Compiler0.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Compiler0.thy Thu Dec 08 20:15:50 2005 +0100
@@ -47,7 +47,7 @@
"_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool"
("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50)
-translations
+translations
"P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P"
"P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)"
"P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^i)"
@@ -80,69 +80,64 @@
subsection "Context lifting lemmas"
-text {*
+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 A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
+ 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>"
-proof -
- from A show ?thesis
- by induct force+
-qed
+ using prems
+ by induct auto
lemma app_left_1:
- assumes A: "is2 \<turnstile> \<langle>s1,i1\<rangle> -1\<rightarrow> \<langle>s2,i2\<rangle>"
+ 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>"
-proof -
- from A show ?thesis
- by induct force+
-qed
+ using prems
+ by induct auto
declare rtrancl_induct2 [induct set: rtrancl]
lemma app_right:
-assumes A: "is1 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-shows "is1 @ is2 \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle>"
-proof -
- from A show ?thesis
- 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>"
- "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
+ 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 prems
+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 A: "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>"
-proof -
- from A show ?thesis
- 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>"
- "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
+ 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 prems
+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)
+ is1 @ is2 \<turnstile> \<langle>s1,j1\<rangle> -*\<rightarrow> \<langle>s2,j2\<rangle>"
+ by (simp add: app_left)
lemma app1_left:
- "is \<turnstile> \<langle>s1,i1\<rangle> -*\<rightarrow> \<langle>s2,i2\<rangle> \<Longrightarrow>
- instr # is \<turnstile> \<langle>s1,Suc i1\<rangle> -*\<rightarrow> \<langle>s2,Suc i2\<rangle>"
- by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
+ 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 prems, of "[instr]"]
+ show ?thesis by simp
+qed
subsection "Compiler correctness"
@@ -154,69 +149,68 @@
The first proof; The statement is very intuitive,
but application of induction hypothesis requires the above lifting lemmas
*}
-theorem assumes A: "\<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")
-proof -
- from A show ?thesis
- 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".
+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 prems
+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 {*
--- a/src/HOL/IMP/Denotation.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Denotation.thy Thu Dec 08 20:15:50 2005 +0100
@@ -12,9 +12,9 @@
constdefs
Gamma :: "[bexp,com_den] => (com_den => com_den)"
- "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
+ "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
{(s,t). s=t \<and> \<not>b s})"
-
+
consts
C :: "com => com_den"
@@ -33,7 +33,7 @@
by (unfold Gamma_def mono_def) fast
lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
-apply (simp (no_asm))
+apply simp
apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*}
apply (simp add: Gamma_def)
done
@@ -42,7 +42,7 @@
lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
(* start with rule induction *)
-apply (erule evalc.induct)
+apply (induct set: evalc)
apply auto
(* while *)
apply (unfold Gamma_def)
@@ -54,15 +54,14 @@
(* Denotational Semantics implies Operational Semantics *)
-lemma com2 [rule_format]: "\<forall>s t. (s,t)\<in>C(c) \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct_tac "c")
+lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+apply (induct c fixing: s t)
-apply (simp_all (no_asm_use))
+apply simp_all
apply fast
apply fast
(* while *)
-apply (intro strip)
apply (erule lfp_induct [OF _ Gamma_mono])
apply (unfold Gamma_def)
apply fast
@@ -72,7 +71,6 @@
(**** Proof of Equivalence ****)
lemma denotational_is_natural: "(s,t) \<in> C(c) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
-apply (fast elim: com2 dest: com1)
-done
+ by (fast elim: com2 dest: com1)
end
--- a/src/HOL/IMP/Examples.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Examples.thy Thu Dec 08 20:15:50 2005 +0100
@@ -8,7 +8,7 @@
theory Examples imports Natural begin
-constdefs
+constdefs
factorial :: "loc => loc => com"
"factorial a b == b :== (%s. 1);
\<WHILE> (%s. s a ~= 0) \<DO>
@@ -18,16 +18,16 @@
subsection "An example due to Tony Hoare"
-lemma lemma1 [rule_format (no_asm)]:
- "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
- !c. 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"
-apply (erule evalc.induct)
-apply auto
-done
+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 |] ==>
+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))
@@ -36,19 +36,16 @@
apply auto
done
-
-lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
+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)"
-apply (unfold factorial_def)
-apply simp
-done
+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
@@ -82,5 +79,5 @@
apply (rule evalc.intros)
apply simp
done
-
+
end
--- a/src/HOL/IMP/Expr.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Expr.thy Thu Dec 08 20:15:50 2005 +0100
@@ -134,12 +134,11 @@
by (rule,cases set: evalb) auto
-lemma aexp_iff:
- "!!n. ((a,s) -a-> n) = (A a s = n)"
- by (induct a) auto
+lemma aexp_iff: "((a,s) -a-> n) = (A a s = n)"
+ by (induct a fixing: n) auto
lemma bexp_iff:
- "!!w. ((b,s) -b-> w) = (B b s = w)"
- by (induct b) (auto simp add: aexp_iff)
+ "((b,s) -b-> w) = (B b s = w)"
+ by (induct b fixing: w) (auto simp add: aexp_iff)
end
--- a/src/HOL/IMP/Hoare.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Hoare.thy Thu Dec 08 20:15:50 2005 +0100
@@ -32,7 +32,7 @@
constdefs wp :: "com => assn => assn"
"wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
-(*
+(*
Soundness (and part of) relative completeness of Hoare rules
wrt denotational semantics
*)
@@ -52,7 +52,7 @@
lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
apply (unfold hoare_valid_def)
-apply (erule hoare.induct)
+apply (induct set: hoare)
apply (simp_all (no_asm_simp))
apply fast
apply fast
@@ -80,7 +80,7 @@
apply fast
done
-lemma wp_If:
+lemma wp_If:
"wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
apply (unfold wp_def)
apply (simp (no_asm))
@@ -88,7 +88,7 @@
apply fast
done
-lemma wp_While_True:
+lemma wp_While_True:
"b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
apply (unfold wp_def)
apply (subst C_While_If)
@@ -104,12 +104,11 @@
lemmas [simp] = wp_SKIP wp_Ass wp_Semi wp_If wp_While_True wp_While_False
(*Not suitable for rewriting: LOOPS!*)
-lemma wp_While_if:
+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)"
-apply (simp (no_asm))
-done
+ by simp
-lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
+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)
@@ -131,18 +130,17 @@
declare C_while [simp del]
-lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
+lemmas [intro!] = hoare.skip hoare.ass hoare.semi hoare.If
-lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
-apply (induct_tac "c")
+lemma wp_is_pre: "|- {wp c Q} c {Q}"
+apply (induct c fixing: Q)
apply (simp_all (no_asm))
apply fast+
apply (blast intro: hoare_conseq1)
-apply safe
apply (rule hoare_conseq2)
apply (rule hoare.While)
apply (rule hoare_conseq1)
- prefer 2 apply (fast)
+ prefer 2 apply fast
apply safe
apply simp
apply simp
--- a/src/HOL/IMP/Machines.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Machines.thy Thu Dec 08 20:15:50 2005 +0100
@@ -1,28 +1,31 @@
+
+(* $Id$ *)
+
theory Machines imports Natural begin
lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
-by(fast intro:rtrancl.intros elim:rtranclE)
+ by (fast intro: rtrancl.intros elim: rtranclE)
lemma converse_rtrancl_eq: "R^* = Id \<union> (R^* O R)"
-by(subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
+ by (subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
lemmas converse_rel_powE = rel_pow_E2
lemma R_O_Rn_commute: "R O R^n = R^n O R"
-by(induct_tac n, simp, simp add: O_assoc[symmetric])
+ by (induct n) (simp, simp add: O_assoc [symmetric])
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))"
+ "((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:converse_rel_powE)
apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
done
lemma rel_pow_plus: "R^(m+n) = R^n O R^m"
-by(induct n, simp, simp add:O_assoc)
+ by (induct n) (simp, simp add: O_assoc)
lemma rel_pow_plusI: "\<lbrakk> (x,y) \<in> R^m; (y,z) \<in> R^n \<rbrakk> \<Longrightarrow> (x,z) \<in> R^(m+n)"
-by(simp add:rel_pow_plus rel_compI)
+ by (simp add: rel_pow_plus rel_compI)
subsection "Instructions"
@@ -33,7 +36,7 @@
subsection "M0 with PC"
-consts exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
+consts exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set"
syntax
"_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool"
("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50)
@@ -58,7 +61,7 @@
"_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool"
("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50)
-translations
+translations
"p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)"
"p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*"
"p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^n"
@@ -97,7 +100,7 @@
"_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool"
("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50)
-translations
+translations
"\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : stepa1"
"\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^*)"
"\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^i)"
@@ -156,7 +159,7 @@
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(erule stepa1.induct)
+apply(induct set: stepa1)
apply(simp add:exec01.SET)
apply(fastsimp intro:exec01.JMPFT)
apply simp
@@ -187,9 +190,9 @@
*)
lemma direction2:
"rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
- \<forall>p q p' q'. rpq = rev p @ q & sp = size p & sp' = size p' \<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(erule exec01.induct)
+apply(induct fixing: p q p' q' set: exec01)
apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj)
apply(drule sym)
apply simp
@@ -216,6 +219,6 @@
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(fast dest:direction1 direction2)
+ by (blast dest: direction1 direction2)
end
--- a/src/HOL/IMP/Natural.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Natural.thy Thu Dec 08 20:15:50 2005 +0100
@@ -11,7 +11,7 @@
subsection "Execution of commands"
-consts evalc :: "(com \<times> state \<times> state) set"
+consts evalc :: "(com \<times> state \<times> state) set"
syntax "_evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
syntax (xsymbols)
@@ -21,7 +21,7 @@
"_evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
text {*
- We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
+ 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}}:
@@ -39,7 +39,7 @@
The big-step execution relation @{text evalc} is defined inductively:
*}
inductive evalc
- intros
+ intros
Skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
Assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
@@ -49,7 +49,7 @@
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'
+ 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"
@@ -60,7 +60,7 @@
@{thm [display] evalc.induct [no_vars]}
-(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
+(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
*}
@@ -70,35 +70,35 @@
syntactic category there is always only one rule applicable. That
means we can use the rules in both directions. The proofs for this
are all the same: one direction is trivial, the other one is shown
- by using the @{text evalc} rules backwards:
+ by using the @{text evalc} rules backwards:
*}
-lemma skip:
+lemma skip:
"\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
by (rule, erule evalc.elims) auto
-lemma assign:
- "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
+lemma assign:
+ "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
by (rule, erule evalc.elims) auto
-lemma semi:
+lemma semi:
"\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
by (rule, erule evalc.elims) auto
-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'"
+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 (rule, erule evalc.elims) auto
-lemma ifFalse:
+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 (rule, erule evalc.elims) auto
-lemma whileFalse:
+lemma whileFalse:
"\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
- by (rule, erule evalc.elims) auto
+ by (rule, erule evalc.elims) auto
-lemma whileTrue:
- "b s \<Longrightarrow>
- \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
+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 (rule, erule evalc.elims) auto
@@ -112,7 +112,7 @@
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:
-*}
+*}
constdefs
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
"c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
@@ -120,7 +120,7 @@
text {*
Proof rules telling Isabelle to unfold the definition
if there is something to be proved about equivalent
- statements: *}
+ 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
@@ -141,7 +141,7 @@
"(\<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"
+ -- "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:"
@@ -159,8 +159,8 @@
-- "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:"
+ ultimately
+ -- "both cases together give us what we want:"
have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
}
moreover
@@ -180,9 +180,9 @@
"\<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)
+ have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
}
- ultimately
+ ultimately
-- "both cases together again give us what we want:"
have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
}
@@ -196,91 +196,89 @@
text {*
The following proof presents all the details:
*}
-theorem com_det: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t"
-proof clarify -- "transform the goal into canonical form"
- assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
- thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t"
- proof (induct set: evalc)
- fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s" by simp
- next
- fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s[x \<mapsto> a s]" by simp
- 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"
+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 prems
+proof (induct fixing: u set: evalc)
+ fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
+ thus "u = s" by simp
+next
+ fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
+ thus "u = s[x \<mapsto> a s]" by simp
+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
+ 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
+ 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"
+ 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 simp
- 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 "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 simp
+ 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 simp
- 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 simp
- 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
+ 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 simp
+ 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 simp
+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
+ 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 "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t"
-proof clarify
- assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
- thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t"
- proof (induct set: evalc)
- -- "the simple @{text \<SKIP>} case for demonstration:"
- fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
- thus "u = s" by simp
- 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
+ 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 prems
+proof (induct fixing: u)
+ -- "the simple @{text \<SKIP>} case for demonstration:"
+ fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
+ thus "u = s" by simp
+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 (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
-qed
+ by auto
+
+ from c "IH\<^sub>c" have "s' = s2" by blast
+ with w "IH\<^sub>w" show "u = s1" by blast
+qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
end
--- a/src/HOL/IMP/Transition.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/Transition.thy Thu Dec 08 20:15:50 2005 +0100
@@ -15,16 +15,16 @@
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
+
+ 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:
*}
consts evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
text {*
- Some syntactic sugar that we will use to hide the
+ Some syntactic sugar that we will use to hide the
@{text option} part in configurations:
*}
syntax
@@ -65,21 +65,21 @@
translations
"cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
- "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n"
- "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*"
+ "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n"
+ "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*"
- -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"},
+ -- {* Isabelle/HOL converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"},
so we also include: *}
- "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"
+ "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"
"cs0 -n\<rightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^n"
- "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*"
+ "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*"
text {*
Now, finally, we are set to write down the rules for our small step semantics:
*}
inductive evalc1
intros
- Skip: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"
+ 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>"
@@ -96,42 +96,40 @@
(* fixme: move to Relation_Power.thy *)
lemma rel_pow_Suc_E2 [elim!]:
"[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
- by (drule rel_pow_Suc_D2) blast
+ by (blast dest: rel_pow_Suc_D2)
lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
-proof -
- assume "p \<in> R\<^sup>*"
- moreover obtain x y where p: "p = (x,y)" by (cases p)
- ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
- hence "\<exists>n. (x,y) \<in> R^n"
+proof (induct p)
+ fix x y
+ assume "(x, y) \<in> R\<^sup>*"
+ thus "\<exists>n. (x, y) \<in> R^n"
proof induct
- fix a have "(a,a) \<in> R^0" by simp
- thus "\<exists>n. (a,a) \<in> R ^ n" ..
+ fix a have "(a, a) \<in> R^0" by simp
+ thus "\<exists>n. (a, a) \<in> R ^ n" ..
next
- fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
- then obtain n where "(a,b) \<in> R^n" ..
- moreover assume "(b,c) \<in> R"
- ultimately have "(a,c) \<in> R^(Suc n)" by auto
- thus "\<exists>n. (a,c) \<in> R^n" ..
+ fix a b c assume "\<exists>n. (a, b) \<in> R ^ n"
+ then obtain n where "(a, b) \<in> R^n" ..
+ moreover assume "(b, c) \<in> R"
+ ultimately have "(a, c) \<in> R^(Suc n)" by auto
+ thus "\<exists>n. (a, c) \<in> R^n" ..
qed
- with p show ?thesis by hypsubst
-qed
-(*>*)
+qed
+(*>*)
text {*
- As for the big step semantics you can read these rules in a
+ 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 (rule, cases set: evalc1, auto)
+lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)"
+ by (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 (rule, cases set: evalc1, auto)
-lemma Cond_1:
+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 (rule, cases set: evalc1, auto)
-lemma While_1:
+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 (rule, cases set: evalc1, auto)
@@ -140,7 +138,7 @@
subsection "Examples"
-lemma
+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 -
@@ -148,45 +146,45 @@
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>?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
+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>"
+ 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>?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>?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)
+ 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 {*
+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"
+ 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)
+ by (cases y, cases "fst y") auto
thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
next
-- "case If:"
@@ -198,22 +196,22 @@
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"
+lemma stuck [elim!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1 y \<Longrightarrow> P"
by (auto elim: evalc1.elims)
-lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>"
- by (erule rtrancl_induct) auto
+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 *)
+(* FIXME: relpow.simps don't work *)
lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
-lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
+lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
lemmas [simp del] = relpow.simps
(*>*)
lemma evalc1_None_0 [simp, dest!]: "\<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"
+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)"
@@ -223,72 +221,70 @@
decomposition and composition.
*}
lemma semiD:
- "\<And>c1 c2 s s''. \<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
+ "\<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"
- (is "PROP ?P n")
-proof (induct n)
- show "PROP ?P 0" by simp
+proof (induct n fixing: c1 c2 s s'')
+ case 0
+ then show ?case by simp
next
- fix n assume IH: "PROP ?P n"
- show "PROP ?P (Suc n)"
- proof -
- fix c1 c2 s s''
- assume "\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
- then obtain y where
+ case (Suc n)
+
+ from `\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>`
+ obtain y where
1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 y" and
n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
- by blast
+ by blast
- 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
- then obtain s' where
+ 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
+ then obtain s' where
"y = \<langle>c2, s'\<rangle>" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
- by auto
- with 1 n have "?Q 1 n s'" by simp
- thus ?thesis by blast
- next
- case Semi2
- then obtain c1' s' where
+ by auto
+ with 1 n have "?Q 1 n s'" by simp
+ thus ?thesis by blast
+ next
+ case Semi2
+ then obtain c1' s' where
y: "y = \<langle>c1'; c2, s'\<rangle>" and
c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
- by auto
- with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
- with IH obtain i j s0 where
+ by auto
+ with 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 auto -- "the remaining cases cannot occur"
- qed
+ 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 auto -- "the remaining cases cannot occur"
qed
-lemma semiI:
- "\<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>"
-proof (induct n)
- fix c0 s s'' assume "\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
- hence False by simp
- thus "?thesis c0 s s''" ..
+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 fixing: 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
- fix c0 s s'' n
- assume c0: "\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
- assume c1: "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- assume 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
+ 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)
+ "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
@@ -312,57 +308,55 @@
text {*
The easy direction of the equivalence proof:
*}
-lemma evalc_imp_evalc1:
- "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
-proof -
- assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- thus "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
- 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
+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 prems
+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 {*
@@ -373,42 +367,42 @@
proof
assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
-next
+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 "\<And>c s s'. \<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
- proof (induct rule: nat_less_induct)
+ have "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ proof (induct fixing: c s s' rule: less_induct)
fix n
- assume IH: "\<forall>m. m < n \<longrightarrow> (\<forall>c s s'. \<langle>c, s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s')"
+ 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
+ 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'"
+ show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
proof (cases c)
case SKIP
with c n show ?thesis by auto
- next
+ 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"
+ 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
+ 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 c1 i IH
- have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" by blast
+ from IH i c1
+ have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" .
moreover
- from c2 j IH
- have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+ from IH j c2
+ have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" .
moreover
note semi
ultimately
@@ -417,33 +411,33 @@
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
+ 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 simp
+ have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
}
moreover
{ assume False: "b s = False"
with If c n
- have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
+ 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 simp
+ have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
}
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
+ 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
+ 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
@@ -458,11 +452,11 @@
declare rel_pow_0_E [elim!]
text {*
- Winskel's small step rules are a bit different \cite{Winskel};
+ 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>")
+ "\<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>" ..
@@ -472,7 +466,7 @@
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>"
+ "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"
@@ -481,8 +475,8 @@
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 t"
+inductive_cases evalc1_SEs:
+ "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t"
"\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 t"
"\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
"\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
@@ -493,53 +487,53 @@
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 (erule evalc.induct)
+apply (induct set: evalc)
--- SKIP
+-- SKIP
apply blast
--- ASSIGN
+-- ASSIGN
apply fast
--- SEMI
+-- SEMI
apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
--- IF
+-- IF
apply (fast intro: converse_rtrancl_into_rtrancl)
apply (fast intro: converse_rtrancl_into_rtrancl)
--- WHILE
+-- WHILE
apply fast
apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
done
-lemma lemma2 [rule_format (no_asm)]:
- "\<forall>c d s u. \<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_tac "n")
+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 fixing: c d s u)
-- "case n = 0"
apply fastsimp
-- "induction step"
-apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
+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 [rule_format (no_asm)]:
- "\<forall>s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
-apply (induct_tac "c")
+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 fixing: s t)
apply (safe dest!: rtrancl_imp_UN_rel_pow)
-- SKIP
apply (simp add: SKIP_n)
--- ASSIGN
+-- ASSIGN
apply (fastsimp elim: rel_pow_E2)
-- SEMI
apply (fast dest!: rel_pow_imp_rtrancl lemma2)
--- IF
+-- IF
apply (erule rel_pow_E2)
apply simp
apply (fast dest!: rel_pow_imp_rtrancl)
@@ -548,7 +542,7 @@
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 (induct_tac n rule: nat_less_induct)
apply (intro strip)
apply (erule rel_pow_E2)
apply simp
@@ -560,10 +554,11 @@
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
+-- WhileFalse
apply (erule rel_pow_E2)
apply simp
apply (simp add: SKIP_n)
@@ -572,8 +567,7 @@
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)"
-apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
-done
+ by (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
subsection "A proof without n"
@@ -582,49 +576,50 @@
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.
+ semantics.
Winskel's small step rule set (using the @{text "\<SKIP>"} statement
to indicate termination) is better suited for this proof.
*}
-lemma my_lemma1 [rule_format (no_asm)]:
- "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<Longrightarrow> \<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
+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"} *}
- have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<longrightarrow>
- \<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
- apply (erule converse_rtrancl_induct2)
+ from prems
+ 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 fast
apply clarify
apply (case_tac c)
apply (auto intro: converse_rtrancl_into_rtrancl)
done
- moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
- ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
+ 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 (erule evalc.induct)
+apply (induct set: evalc)
--- SKIP
+-- SKIP
apply fast
-- ASSIGN
apply fast
--- SEMI
+-- SEMI
apply (fast intro: my_lemma1)
-- IF
apply (fast intro: converse_rtrancl_into_rtrancl)
-apply (fast intro: converse_rtrancl_into_rtrancl)
+apply (fast intro: converse_rtrancl_into_rtrancl)
--- WHILE
+-- WHILE
apply fast
apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
@@ -645,18 +640,18 @@
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:
+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'>
+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,
@@ -668,24 +663,22 @@
inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
-lemma FB_lemma3 [rule_format]:
- "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow>
- (\<forall>t. \<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 (erule evalc1.induct)
- apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
- done
+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 fixing: t set: evalc1)
+ (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
-lemma FB_lemma2 [rule_format]:
- "(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 (erule converse_rtrancl_induct2)
+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)
apply simp
apply clarsimp
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"
- apply (fastsimp dest: FB_lemma2)
- done
+ by (fastsimp dest: FB_lemma2)
end
--- a/src/HOL/IMP/VC.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/IMP/VC.thy Thu Dec 08 20:15:50 2005 +0100
@@ -28,14 +28,14 @@
"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 (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 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 (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)"
@@ -69,49 +69,50 @@
lemma l: "!s. P s --> P s" by fast
-lemma vc_sound: "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
-apply (induct_tac "c")
+lemma vc_sound: "(!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
+apply (induct c fixing: Q)
apply (simp_all (no_asm))
apply fast
apply fast
apply fast
(* if *)
+ apply atomize
apply (tactic "Deepen_tac 4 1")
(* while *)
-apply (intro allI impI)
+apply atomize
+apply (intro allI impI)
apply (rule conseq)
apply (rule l)
apply (rule While)
defer
apply fast
-apply (rule_tac P="awp acom fun2" in conseq)
+apply (rule_tac P="awp c fun2" in conseq)
apply fast
apply fast
apply fast
done
-lemma awp_mono [rule_format (no_asm)]:
+lemma awp_mono [rule_format (no_asm)]:
"!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
-apply (induct_tac "c")
+apply (induct c)
apply (simp_all (no_asm_simp))
apply (rule allI, rule allI, rule impI)
apply (erule allE, erule allE, erule mp)
apply (erule allE, erule allE, erule mp, assumption)
done
-
-lemma vc_mono [rule_format (no_asm)]:
+lemma vc_mono [rule_format (no_asm)]:
"!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
-apply (induct_tac "c")
+apply (induct c)
apply (simp_all (no_asm_simp))
apply safe
-apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
+apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
prefer 2 apply assumption
apply (fast elim: awp_mono)
done
lemma vc_complete: assumes der: "|- {P}c{Q}"
- shows "(? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
+ 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
@@ -149,9 +150,7 @@
case conseq thus ?case by(fast elim!: awp_mono vc_mono)
qed
-lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
-apply (induct_tac "c")
-apply (simp_all (no_asm_simp) add: Let_def)
-done
+lemma vcawp_vc_awp: "vcawp c Q = (vc c Q, awp c Q)"
+ by (induct c fixing: Q) (simp_all add: Let_def)
end
--- a/src/HOL/Library/Quotient.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Library/Quotient.thy Thu Dec 08 20:15:50 2005 +0100
@@ -163,15 +163,13 @@
*}
theorem quot_cond_function:
- "(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==>
- (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
- ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
- P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
- (is "PROP ?eq ==> PROP ?cong ==> _ ==> _")
+ assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
+ and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
+ ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
+ and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
+ shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
proof -
- assume cong: "PROP ?cong"
- assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
- hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
+ from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
also have "... = g a b"
proof (rule cong)
show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" ..
@@ -185,18 +183,16 @@
qed
theorem quot_function:
- "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
- (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==>
- f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
-proof -
- case rule_context from this TrueI
- show ?thesis by (rule quot_cond_function)
-qed
+ assumes "!!X Y. f X Y == g (pick X) (pick Y)"
+ and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
+ shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
+ using prems and TrueI
+ by (rule quot_cond_function)
theorem quot_function':
"(!!X Y. f X Y == g (pick X) (pick Y)) ==>
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
- by (rule quot_function) (simp only: quot_equality)+
+ by (rule quot_function) (simp_all only: quot_equality)
end
--- a/src/HOL/Library/While_Combinator.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Library/While_Combinator.thy Thu Dec 08 20:15:50 2005 +0100
@@ -67,8 +67,9 @@
hide const while_aux
-lemma def_while_unfold: assumes fdef: "f == while test do"
- shows "f x = (if test x then f(do x) else x)"
+lemma def_while_unfold:
+ assumes fdef: "f == while test do"
+ shows "f x = (if test x then f(do x) else x)"
proof -
have "f x = while test do x" using fdef by simp
also have "\<dots> = (if test x then while test do (do x) else x)"
@@ -82,22 +83,16 @@
The proof rule for @{term while}, where @{term P} is the invariant.
*}
-theorem while_rule_lemma[rule_format]:
- "[| !!s. P s ==> b s ==> P (c s);
- !!s. P s ==> \<not> b s ==> Q s;
- wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
- P s --> Q (while b c s)"
-proof -
- case rule_context
- assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
- show ?thesis
- apply (induct s rule: wf [THEN wf_induct])
- apply simp
- apply clarify
- apply (subst while_unfold)
- apply (simp add: rule_context)
- done
-qed
+theorem while_rule_lemma:
+ assumes invariant: "!!s. P s ==> b s ==> P (c s)"
+ and terminate: "!!s. P s ==> \<not> b s ==> Q s"
+ and wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
+ shows "P s \<Longrightarrow> Q (while b c s)"
+ apply (induct s rule: wf [THEN wf_induct])
+ apply simp
+ apply (subst while_unfold)
+ apply (simp add: invariant terminate)
+ done
theorem while_rule:
"[| P s;
@@ -148,7 +143,7 @@
back into equality. *}
lemma seteq: "(A = B) = ((!a : A. a:B) & (!b:B. b:A))"
-by blast
+ by blast
theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
P {0, 4, 2}"
--- a/src/HOL/MicroJava/BV/Err.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy Thu Dec 08 20:15:50 2005 +0100
@@ -257,15 +257,14 @@
done
lemma OK_plus_OK_eq_Err_conv [simp]:
- "\<lbrakk> x:A; y:A; semilat(err A, le r, fe) \<rbrakk> \<Longrightarrow>
- ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+ assumes "x:A" and "y:A" and "semilat(err A, le r, fe)"
+ shows "((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
proof -
have plus_le_conv3: "\<And>A x y z f r.
\<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk>
\<Longrightarrow> x <=_r z \<and> y <=_r z"
by (rule semilat.plus_le_conv [THEN iffD1])
- case rule_context
- thus ?thesis
+ from prems show ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
--- a/src/HOL/MicroJava/BV/Kildall.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Thu Dec 08 20:15:50 2005 +0100
@@ -159,9 +159,9 @@
done
lemma (in semilat) merges_pres_le_ub:
-shows "\<lbrakk> set ts <= A; set ss <= A;
- \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; ss <=[r] ts \<rbrakk>
- \<Longrightarrow> merges f ps ss <=[r] ts"
+ assumes "set ts <= A" and "set ss <= A"
+ and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts"
+ shows "merges f ps ss <=[r] ts"
proof -
{ fix t ts ps
have
@@ -182,8 +182,7 @@
done
} note this [dest]
- case rule_context
- thus ?thesis by blast
+ from prems show ?thesis by blast
qed
--- a/src/HOL/MicroJava/BV/Product.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy Thu Dec 08 20:15:50 2005 +0100
@@ -72,15 +72,15 @@
lemma plus_eq_Err_conv [simp]:
- "\<lbrakk> x:A; y:A; semilat(err A, Err.le r, lift2 f) \<rbrakk>
- \<Longrightarrow> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+ assumes "x:A" and "y:A"
+ and "semilat(err A, Err.le r, lift2 f)"
+ shows "(x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
proof -
have plus_le_conv2:
"\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
by (rule semilat.plus_le_conv [THEN iffD1])
- case rule_context
- thus ?thesis
+ from prems show ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
--- a/src/HOL/Product_Type.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Product_Type.thy Thu Dec 08 20:15:50 2005 +0100
@@ -223,14 +223,13 @@
done
lemma Pair_inject:
- "(a, b) = (a', b') ==> (a = a' ==> b = b' ==> R) ==> R"
-proof -
- case rule_context [unfolded Pair_def]
- show ?thesis
- apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE])
- apply (rule rule_context ProdI)+
- .
-qed
+ assumes "(a, b) = (a', b')"
+ and "a = a' ==> b = b' ==> R"
+ shows R
+ apply (insert prems [unfolded Pair_def])
+ apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE])
+ apply (assumption | rule ProdI)+
+ done
lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')"
by (blast elim!: Pair_inject)
@@ -507,11 +506,11 @@
lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
by (simp only: split_tupled_all, simp)
-lemma mem_splitE: "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"
-proof -
- case rule_context [unfolded split_def]
- show ?thesis by (rule rule_context surjective_pairing)+
-qed
+lemma mem_splitE:
+ assumes major: "z: split c p"
+ and cases: "!!x y. [| p = (x,y); z: c x y |] ==> Q"
+ shows Q
+ by (rule major [unfolded split_def] cases surjective_pairing)+
declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
@@ -533,15 +532,14 @@
*}
lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
-by (rule ext, fast)
+ by (rule ext) fast
lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
-by (rule ext, fast)
+ by (rule ext) fast
lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
-- {* Allows simplifications of nested splits in case of independent predicates. *}
- apply (rule ext, blast)
- done
+ by (rule ext) blast
(* Do NOT make this a simp rule as it
a) only helps in special situations
@@ -549,7 +547,7 @@
*)
lemma split_comp_eq:
"(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))"
-by (rule ext, auto)
+ by (rule ext) auto
lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
by blast
@@ -595,20 +593,15 @@
done
lemma prod_fun_imageE [elim!]:
- "[| c: (prod_fun f g)`r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P
- |] ==> P"
-proof -
- case rule_context
- assume major: "c: (prod_fun f g)`r"
- show ?thesis
- apply (rule major [THEN imageE])
- apply (rule_tac p = x in PairE)
- apply (rule rule_context)
- prefer 2
- apply blast
- apply (blast intro: prod_fun)
- done
-qed
+ assumes major: "c: (prod_fun f g)`r"
+ and cases: "!!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P"
+ shows P
+ apply (rule major [THEN imageE])
+ apply (rule_tac p = x in PairE)
+ apply (rule cases)
+ apply (blast intro: prod_fun)
+ apply blast
+ done
constdefs
@@ -619,10 +612,10 @@
"upd_snd f == prod_fun id f"
lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)"
-by (simp add: upd_fst_def)
+ by (simp add: upd_fst_def)
lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)"
-by (simp add: upd_snd_def)
+ by (simp add: upd_snd_def)
text {*
\bigskip Disjoint union of a family of sets -- Sigma.
@@ -644,10 +637,10 @@
*}
lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
-by blast
+ by blast
lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
-by blast
+ by blast
lemma SigmaE2:
"[| (a, b) : Sigma A B;
@@ -658,7 +651,7 @@
lemma Sigma_cong:
"\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
\<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
-by auto
+ by auto
lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
by blast
--- a/src/HOL/Real/Rational.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Real/Rational.thy Thu Dec 08 20:15:50 2005 +0100
@@ -332,16 +332,13 @@
qed
theorem rat_function:
- "(!!q r. f q r == g (fraction_of q) (fraction_of r)) ==>
- (!!a b a' b' c d c' d'.
+ assumes "!!q r. f q r == g (fraction_of q) (fraction_of r)"
+ and "!!a b a' b' c d c' d'.
\<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor> ==>
b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0 ==>
- g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==>
- f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
-proof -
- case rule_context from this TrueI
- show ?thesis by (rule rat_cond_function)
-qed
+ g (fract a b) (fract c d) = g (fract a' b') (fract c' d')"
+ shows "f (Fract a b) (Fract c d) = g (fract a b) (fract c d)"
+ using prems and TrueI by (rule rat_cond_function)
subsubsection {* Standard operations on rational numbers *}
--- a/src/HOL/Transitive_Closure.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Transitive_Closure.thy Thu Dec 08 20:15:50 2005 +0100
@@ -81,7 +81,7 @@
lemmas rtrancl_induct2 =
rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
consumes 1, case_names refl step]
-
+
lemma trans_rtrancl: "trans(r^*)"
-- {* transitivity of transitive closure!! -- by induction *}
proof (rule transI)
@@ -94,21 +94,17 @@
lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
lemma rtranclE:
- "[| (a::'a,b) : r^*; (a = b) ==> P;
- !!y.[| (a,y) : r^*; (y,b) : r |] ==> P
- |] ==> P"
+ assumes major: "(a::'a,b) : r^*"
+ and cases: "(a = b) ==> P"
+ "!!y. [| (a,y) : r^*; (y,b) : r |] ==> P"
+ shows P
-- {* elimination of @{text rtrancl} -- by induction on a special formula *}
-proof -
- assume major: "(a::'a,b) : r^*"
- case rule_context
- show ?thesis
- apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
- apply (rule_tac [2] major [THEN rtrancl_induct])
- prefer 2 apply (blast!)
- prefer 2 apply (blast!)
- apply (erule asm_rl exE disjE conjE prems)+
- done
-qed
+ apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
+ apply (rule_tac [2] major [THEN rtrancl_induct])
+ prefer 2 apply blast
+ prefer 2 apply blast
+ apply (erule asm_rl exE disjE conjE cases)+
+ done
lemma converse_rtrancl_into_rtrancl:
"(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
@@ -187,21 +183,16 @@
consumes 1, case_names refl step]
lemma converse_rtranclE:
- "[| (x,z):r^*;
- x=z ==> P;
- !!y. [| (x,y):r; (y,z):r^* |] ==> P
- |] ==> P"
-proof -
- assume major: "(x,z):r^*"
- case rule_context
- show ?thesis
- apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
- apply (rule_tac [2] major [THEN converse_rtrancl_induct])
- prefer 2 apply iprover
- prefer 2 apply iprover
- apply (erule asm_rl exE disjE conjE prems)+
- done
-qed
+ assumes major: "(x,z):r^*"
+ and cases: "x=z ==> P"
+ "!!y. [| (x,y):r; (y,z):r^* |] ==> P"
+ shows P
+ apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
+ apply (rule_tac [2] major [THEN converse_rtrancl_induct])
+ prefer 2 apply iprover
+ prefer 2 apply iprover
+ apply (erule asm_rl exE disjE conjE cases)+
+ done
ML_setup {*
bind_thm ("converse_rtranclE2", split_rule
@@ -258,17 +249,12 @@
qed
lemma trancl_trans_induct:
- "[| (x,y) : r^+;
- !!x y. (x,y) : r ==> P x y;
- !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z
- |] ==> P x y"
+ assumes major: "(x,y) : r^+"
+ and cases: "!!x y. (x,y) : r ==> P x y"
+ "!!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z"
+ shows "P x y"
-- {* Another induction rule for trancl, incorporating transitivity *}
-proof -
- assume major: "(x,y) : r^+"
- case rule_context
- show ?thesis
- by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
-qed
+ by (iprover intro: r_into_trancl major [THEN trancl_induct] cases)
inductive_cases tranclE: "(a, b) : r^+"
@@ -279,9 +265,9 @@
-- {* Transitivity of @{term "r^+"} *}
proof (rule transI)
fix x y z
- assume "(x, y) \<in> r^+"
+ assume xy: "(x, y) \<in> r^+"
assume "(y, z) \<in> r^+"
- thus "(x, z) \<in> r^+" by induct (iprover!)+
+ thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+
qed
lemmas trancl_trans = trans_trancl [THEN transD, standard]
@@ -323,19 +309,15 @@
intro!: trancl_converseI trancl_converseD)
lemma converse_trancl_induct:
- "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y);
- !!y z.[| (y,z) : r; (z,b) : r^+; P(z) |] ==> P(y) |]
- ==> P(a)"
-proof -
- assume major: "(a,b) : r^+"
- case rule_context
- show ?thesis
- apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
- apply (rule prems)
- apply (erule converseD)
- apply (blast intro: prems dest!: trancl_converseD)
- done
-qed
+ assumes major: "(a,b) : r^+"
+ and cases: "!!y. (y,b) : r ==> P(y)"
+ "!!y z.[| (y,z) : r; (z,b) : r^+; P(z) |] ==> P(y)"
+ shows "P a"
+ apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
+ apply (rule cases)
+ apply (erule converseD)
+ apply (blast intro: prems dest!: trancl_converseD)
+ done
lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
apply (erule converse_trancl_induct, auto)
@@ -343,15 +325,14 @@
done
lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
-by(blast elim: tranclE dest: trancl_into_rtrancl)
+ by (blast elim: tranclE dest: trancl_into_rtrancl)
lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
by (blast dest: r_into_trancl)
lemma trancl_subset_Sigma_aux:
"(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
- apply (erule rtrancl_induct, auto)
- done
+ by (induct rule: rtrancl_induct) auto
lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
apply (rule subsetI)
@@ -477,16 +458,16 @@
val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
val rtrancl_trans = thm "rtrancl_trans";
- fun decomp (Trueprop $ t) =
- let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
- let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
- | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
- | decr r = (r,"r");
- val (rel,r) = decr rel;
- in SOME (a,b,rel,r) end
- | dec _ = NONE
+ fun decomp (Trueprop $ t) =
+ let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
+ let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
+ | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
+ | decr r = (r,"r");
+ val (rel,r) = decr rel;
+ in SOME (a,b,rel,r) end
+ | dec _ = NONE
in dec t end;
-
+
end); (* struct *)
change_simpset (fn ss => ss
@@ -499,7 +480,7 @@
method_setup trancl =
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trancl_tac)) *}
- {* simple transitivity reasoner *}
+ {* simple transitivity reasoner *}
method_setup rtrancl =
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (rtrancl_tac)) *}
{* simple transitivity reasoner *}
--- a/src/HOL/Unix/Unix.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/HOL/Unix/Unix.thy Thu Dec 08 20:15:50 2005 +0100
@@ -255,16 +255,16 @@
lookup root path = Some file"
by (simp add: access_def split: option.splits if_splits)
-lemma access_update_other: "path' \<parallel> path \<Longrightarrow>
- access (update path' opt root) path uid perms = access root path uid perms"
+lemma access_update_other:
+ assumes parallel: "path' \<parallel> path"
+ shows "access (update path' opt root) path uid perms = access root path uid perms"
proof -
- assume "path' \<parallel> path"
- then obtain y z xs ys zs where
+ from parallel obtain y z xs ys zs where
"y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
by (blast dest: parallel_decomp)
- hence "lookup (update path' opt root) path = lookup root path"
+ then have "lookup (update path' opt root) path = lookup root path"
by (blast intro: lookup_update_other)
- thus ?thesis by (simp only: access_def)
+ then show ?thesis by (simp only: access_def)
qed
@@ -437,36 +437,35 @@
relation.
*}
-theorem transition_uniq: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root \<midarrow>x\<rightarrow> root'' \<Longrightarrow> root' = root''"
-proof -
- assume root: "root \<midarrow>x\<rightarrow> root'"
- assume "root \<midarrow>x\<rightarrow> root''"
- thus "root' = root''"
- proof cases
- case read
- with root show ?thesis by cases auto
- next
- case write
- with root show ?thesis by cases auto
- next
- case chmod
- with root show ?thesis by cases auto
- next
- case creat
- with root show ?thesis by cases auto
- next
- case unlink
- with root show ?thesis by cases auto
- next
- case mkdir
- with root show ?thesis by cases auto
- next
- case rmdir
- with root show ?thesis by cases auto
- next
- case readdir
- with root show ?thesis by cases fastsimp+
- qed
+theorem transition_uniq:
+ assumes root': "root \<midarrow>x\<rightarrow> root'"
+ and root'': "root \<midarrow>x\<rightarrow> root''"
+ shows "root' = root''"
+ using root''
+proof cases
+ case read
+ with root' show ?thesis by cases auto
+next
+ case write
+ with root' show ?thesis by cases auto
+next
+ case chmod
+ with root' show ?thesis by cases auto
+next
+ case creat
+ with root' show ?thesis by cases auto
+next
+ case unlink
+ with root' show ?thesis by cases auto
+next
+ case mkdir
+ with root' show ?thesis by cases auto
+next
+ case rmdir
+ with root' show ?thesis by cases auto
+next
+ case readdir
+ with root' show ?thesis by cases fastsimp+
qed
text {*
@@ -476,24 +475,20 @@
*}
theorem transition_type_safe:
- "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
- \<Longrightarrow> \<exists>att dir. root' = Env att dir"
-proof -
- assume tr: "root \<midarrow>x\<rightarrow> root'"
- assume inv: "\<exists>att dir. root = Env att dir"
- show ?thesis
- proof (cases "path_of x")
- case Nil
- with tr inv show ?thesis
- by cases (auto simp add: access_def split: if_splits)
- next
- case Cons
- from tr obtain opt where
- "root' = root \<or> root' = update (path_of x) opt root"
- by cases auto
- with inv Cons show ?thesis
- by (auto simp add: update_eq split: list.splits)
- qed
+ assumes tr: "root \<midarrow>x\<rightarrow> root'"
+ and inv: "\<exists>att dir. root = Env att dir"
+ shows "\<exists>att dir. root' = Env att dir"
+proof (cases "path_of x")
+ case Nil
+ with tr inv show ?thesis
+ by cases (auto simp add: access_def split: if_splits)
+next
+ case Cons
+ from tr obtain opt where
+ "root' = root \<or> root' = update (path_of x) opt root"
+ by cases auto
+ with inv Cons show ?thesis
+ by (auto simp add: update_eq split: list.splits)
qed
text {*
@@ -539,21 +534,21 @@
lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')"
proof
assume "root =[]\<Rightarrow> root'"
- thus "root = root'" by cases simp_all
+ then show "root = root'" by cases simp_all
next
assume "root = root'"
- thus "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)
+ then show "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)
qed
lemma transitions_cons_eq:
"root =(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root'')"
proof
assume "root =(x # xs)\<Rightarrow> root''"
- thus "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
+ then show "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
by cases auto
next
assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
- thus "root =(x # xs)\<Rightarrow> root''"
+ then show "root =(x # xs)\<Rightarrow> root''"
by (blast intro: transitions.cons)
qed
@@ -568,13 +563,13 @@
by (simp add: transitions_nil_eq)
lemma transitions_consD:
- "root =(x # xs)\<Rightarrow> root'' \<Longrightarrow> root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root''"
+ assumes list: "root =(x # xs)\<Rightarrow> root''"
+ and hd: "root \<midarrow>x\<rightarrow> root'"
+ shows "root' =xs\<Rightarrow> root''"
proof -
- assume "root =(x # xs)\<Rightarrow> root''"
- then obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"
+ from list obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"
by cases simp_all
- assume "root \<midarrow>x\<rightarrow> root'"
- with r' have "r' = root'" by (rule transition_uniq)
+ from r' hd have "r' = root'" by (rule transition_uniq)
with root'' show "root' =xs\<Rightarrow> root''" by simp
qed
@@ -586,26 +581,20 @@
*}
lemma transitions_invariant:
- "(\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r') \<Longrightarrow>
- root =xs\<Rightarrow> root' \<Longrightarrow> Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
-proof -
- assume r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
- assume "root =xs\<Rightarrow> root'"
- thus "Q root \<Longrightarrow> (\<forall>x \<in> set xs. P x) \<Longrightarrow> Q root'" (is "PROP ?P root xs root'")
- proof (induct root xs root')
- fix root assume "Q root"
- thus "Q root" .
- next
- fix root root' root'' and x xs
- assume root': "root \<midarrow>x\<rightarrow> root'"
- assume hyp: "PROP ?P root' xs root''"
- assume Q: "Q root"
- assume P: "\<forall>x \<in> set (x # xs). P x"
- hence "P x" by simp
- with root' Q have Q': "Q root'" by (rule r)
- from P have "\<forall>x \<in> set xs. P x" by simp
- with Q' show "Q root''" by (rule hyp)
- qed
+ assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
+ and trans: "root =xs\<Rightarrow> root'"
+ shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
+ using trans
+proof induct
+ case nil
+ show ?case by assumption
+next
+ case (cons root root' root'' x xs)
+ note P = `\<forall>x \<in> set (x # xs). P x`
+ then have "P x" by simp
+ with `root \<midarrow>x\<rightarrow> root'` and `Q root` have Q': "Q root'" by (rule r)
+ from P have "\<forall>x \<in> set xs. P x" by simp
+ with Q' show "Q root''" by (rule cons.hyps)
qed
text {*
@@ -675,31 +664,23 @@
executed we may destruct it backwardly into individual transitions.
*}
-lemma can_exec_snocD: "\<And>root. can_exec root (xs @ [y])
+lemma can_exec_snocD: "can_exec root (xs @ [y])
\<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''"
- (is "PROP ?P xs" is "\<And>root. ?A root xs \<Longrightarrow> ?C root xs")
-proof (induct xs)
- fix root
- {
- assume "?A root []"
- thus "?C root []"
- by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
- next
- fix x xs
- assume hyp: "PROP ?P xs"
- assume asm: "?A root (x # xs)"
- show "?C root (x # xs)"
- proof -
- from asm obtain r root'' where x: "root \<midarrow>x\<rightarrow> r" and
- xs_y: "r =(xs @ [y])\<Rightarrow> root''"
- by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
- from xs_y hyp obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
- by (unfold can_exec_def) blast
- from x xs have "root =(x # xs)\<Rightarrow> root'"
- by (rule transitions.cons)
- with y show ?thesis by blast
- qed
- }
+proof (induct xs fixing: root)
+ case Nil
+ then show ?case
+ by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
+next
+ case (Cons x xs)
+ from `can_exec root ((x # xs) @ [y])` obtain r root'' where
+ x: "root \<midarrow>x\<rightarrow> r" and
+ xs_y: "r =(xs @ [y])\<Rightarrow> root''"
+ by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
+ from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
+ by (unfold can_exec_def) blast
+ from x xs have "root =(x # xs)\<Rightarrow> root'"
+ by (rule transitions.cons)
+ with y show ?case by blast
qed
@@ -803,16 +784,12 @@
*}
theorem general_procedure:
- "(\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False) \<Longrightarrow>
- (\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root) \<Longrightarrow>
- (\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r') \<Longrightarrow>
- init users =bs\<Rightarrow> root \<Longrightarrow>
- \<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))"
+ assumes cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"
+ and init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"
+ and preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
+ and init_result: "init users =bs\<Rightarrow> root"
+ shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))"
proof -
- assume cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"
- assume init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"
- assume preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
- assume init_result: "init users =bs\<Rightarrow> root"
{
fix xs
assume Ps: "\<forall>x \<in> set xs. P x"
@@ -825,7 +802,7 @@
by (rule transitions_invariant)
from this y have False by (rule cannot_y)
}
- thus ?thesis by blast
+ then show ?thesis by blast
qed
text {*
@@ -930,38 +907,36 @@
we just have to inspect rather special cases.
*}
-lemma (in invariant)
- cannot_rmdir: "invariant root bogus_path \<Longrightarrow>
- root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root' \<Longrightarrow> False"
+lemma (in invariant) cannot_rmdir:
+ assumes inv: "invariant root bogus_path"
+ and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
+ shows False
proof -
- assume "invariant root bogus_path"
- then obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
+ from inv obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
by (unfold invariant_def) blast
moreover
- assume "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
- then obtain att where
+ from rmdir obtain att where
"access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"
by cases auto
- hence "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
+ then have "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
by (simp only: access_empty_lookup lookup_append_some) simp
ultimately show False by (simp add: bogus_path_def)
qed
lemma (in invariant)
- init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path"
-proof -
- note eval = facts access_def init_def
- case rule_context thus ?thesis
- apply (unfold bogus_def bogus_path_def)
- apply (drule transitions_consD, rule transition.intros,
+ assumes init: "init users =bogus\<Rightarrow> root"
+ notes eval = facts access_def init_def
+ shows init_invariant: "invariant root bogus_path"
+ using init
+ apply (unfold bogus_def bogus_path_def)
+ apply (drule transitions_consD, rule transition.intros,
(force simp add: eval)+, (simp add: eval)?)+
- -- "evaluate all operations"
- apply (drule transitions_nilD)
- -- "reach final result"
- apply (simp add: invariant_def eval)
- -- "check the invariant"
- done
-qed
+ -- "evaluate all operations"
+ apply (drule transitions_nilD)
+ -- "reach final result"
+ apply (simp add: invariant_def eval)
+ -- "check the invariant"
+ done
text {*
\medskip At last we are left with the main effort to show that the
@@ -971,14 +946,12 @@
required here.
*}
-lemma (in invariant)
- preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow>
- invariant root path \<Longrightarrow> uid_of x = user\<^isub>1 \<Longrightarrow> invariant root' path"
+lemma (in invariant) preserve_invariant:
+ assumes tr: "root \<midarrow>x\<rightarrow> root'"
+ and inv: "invariant root path"
+ and uid: "uid_of x = user\<^isub>1"
+ shows "invariant root' path"
proof -
- assume tr: "root \<midarrow>x\<rightarrow> root'"
- assume inv: "invariant root path"
- assume uid: "uid_of x = user\<^isub>1"
-
from inv obtain att dir where
inv1: "access root path user\<^isub>1 {} = Some (Env att dir)" and
inv2: "dir \<noteq> empty" and
@@ -1019,7 +992,7 @@
with tr uid inv2 inv3 lookup changed path and user\<^isub>1_not_root
have False
by cases (auto simp add: access_empty_lookup dest: access_some_lookup)
- thus ?thesis ..
+ then show ?thesis ..
next
fix z zs assume ys: "ys = z # zs"
have "lookup root' path = lookup root path"
@@ -1085,7 +1058,7 @@
have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
lookup root ((path @ [y]) @ us) \<noteq> None"
by cases (auto dest: access_some_lookup)
- thus ?thesis by (blast dest!: lookup_some_append)
+ then show ?thesis by (blast dest!: lookup_some_append)
qed
finally show ?thesis .
qed
--- a/src/ZF/Induct/Brouwer.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/ZF/Induct/Brouwer.thy Thu Dec 08 20:15:50 2005 +0100
@@ -22,24 +22,20 @@
by (fast intro!: brouwer.intros [unfolded brouwer.con_defs]
elim: brouwer.cases [unfolded brouwer.con_defs])
-lemma brouwer_induct2:
- "[| b \<in> brouwer;
- P(Zero);
- !!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b));
- !!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i)
- |] ==> P(Lim(h))
- |] ==> P(b)"
+lemma brouwer_induct2 [consumes 1, case_names Zero Suc Lim]:
+ assumes b: "b \<in> brouwer"
+ and cases:
+ "P(Zero)"
+ "!!b. [| b \<in> brouwer; P(b) |] ==> P(Suc(b))"
+ "!!h. [| h \<in> nat -> brouwer; \<forall>i \<in> nat. P(h`i) |] ==> P(Lim(h))"
+ shows "P(b)"
-- {* A nicer induction rule than the standard one. *}
-proof -
- case rule_context
- assume "b \<in> brouwer"
- thus ?thesis
- apply induct
- apply (assumption | rule rule_context)+
+ using b
+ apply induct
+ apply (assumption | rule cases)+
apply (fast elim: fun_weaken_type)
apply (fast dest: apply_type)
done
-qed
subsection {* The Martin-Löf wellordering type *}
@@ -58,22 +54,17 @@
elim: Well.cases [unfolded Well.con_defs])
-lemma Well_induct2:
- "[| w \<in> Well(A, B);
- !!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y)
- |] ==> P(Sup(a,f))
- |] ==> P(w)"
+lemma Well_induct2 [consumes 1, case_names step]:
+ assumes w: "w \<in> Well(A, B)"
+ and step: "!!a f. [| a \<in> A; f \<in> B(a) -> Well(A,B); \<forall>y \<in> B(a). P(f`y) |] ==> P(Sup(a,f))"
+ shows "P(w)"
-- {* A nicer induction rule than the standard one. *}
-proof -
- case rule_context
- assume "w \<in> Well(A, B)"
- thus ?thesis
- apply induct
- apply (assumption | rule rule_context)+
- apply (fast elim: fun_weaken_type)
- apply (fast dest: apply_type)
- done
-qed
+ using w
+ apply induct
+ apply (assumption | rule step)+
+ apply (fast elim: fun_weaken_type)
+ apply (fast dest: apply_type)
+ done
lemma Well_bool_unfold: "Well(bool, \<lambda>x. x) = 1 + (1 -> Well(bool, \<lambda>x. x))"
-- {* In fact it's isomorphic to @{text nat}, but we need a recursion operator *}
--- a/src/ZF/Induct/Ntree.thy Thu Dec 08 20:15:41 2005 +0100
+++ b/src/ZF/Induct/Ntree.thy Thu Dec 08 20:15:50 2005 +0100
@@ -49,42 +49,36 @@
by (blast intro: ntree.intros [unfolded ntree.con_defs]
elim: ntree.cases [unfolded ntree.con_defs])
-lemma ntree_induct [induct set: ntree]:
- "[| t \<in> ntree(A);
- !!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); \<forall>i \<in> n. P(h`i)
- |] ==> P(Branch(x,h))
- |] ==> P(t)"
+lemma ntree_induct [consumes 1, case_names Branch, induct set: ntree]:
+ assumes t: "t \<in> ntree(A)"
+ and step: "!!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); \<forall>i \<in> n. P(h`i)
+ |] ==> P(Branch(x,h))"
+ shows "P(t)"
-- {* A nicer induction rule than the standard one. *}
-proof -
- case rule_context
- assume "t \<in> ntree(A)"
- thus ?thesis
- apply induct
- apply (erule UN_E)
- apply (assumption | rule rule_context)+
- apply (fast elim: fun_weaken_type)
- apply (fast dest: apply_type)
- done
-qed
+ using t
+ apply induct
+ apply (erule UN_E)
+ apply (assumption | rule step)+
+ apply (fast elim: fun_weaken_type)
+ apply (fast dest: apply_type)
+ done
-lemma ntree_induct_eqn:
- "[| t \<in> ntree(A); f \<in> ntree(A)->B; g \<in> ntree(A)->B;
- !!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); f O h = g O h |] ==>
- f ` Branch(x,h) = g ` Branch(x,h)
- |] ==> f`t=g`t"
+lemma ntree_induct_eqn [consumes 1]:
+ assumes t: "t \<in> ntree(A)"
+ and f: "f \<in> ntree(A)->B"
+ and g: "g \<in> ntree(A)->B"
+ and step: "!!x n h. [| x \<in> A; n \<in> nat; h \<in> n -> ntree(A); f O h = g O h |] ==>
+ f ` Branch(x,h) = g ` Branch(x,h)"
+ shows "f`t=g`t"
-- {* Induction on @{term "ntree(A)"} to prove an equation *}
-proof -
- case rule_context
- assume "t \<in> ntree(A)"
- thus ?thesis
- apply induct
- apply (assumption | rule rule_context)+
- apply (insert rule_context)
- apply (rule fun_extension)
- apply (assumption | rule comp_fun)+
- apply (simp add: comp_fun_apply)
+ using t
+ apply induct
+ apply (assumption | rule step)+
+ apply (insert f g)
+ apply (rule fun_extension)
+ apply (assumption | rule comp_fun)+
+ apply (simp add: comp_fun_apply)
done
-qed
text {*
\medskip Lemmas to justify using @{text Ntree} in other recursive
@@ -127,9 +121,8 @@
by (simp add: ntree_copy_def ntree_rec_Branch)
lemma ntree_copy_is_ident: "z \<in> ntree(A) ==> ntree_copy(z) = z"
- apply (induct_tac z)
- apply (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
- done
+ by (induct z set: ntree)
+ (auto simp add: domain_of_fun Pi_Collect_iff fun_is_function)
text {*
@@ -140,25 +133,21 @@
by (fast intro!: maptree.intros [unfolded maptree.con_defs]
elim: maptree.cases [unfolded maptree.con_defs])
-lemma maptree_induct [induct set: maptree]:
- "[| t \<in> maptree(A);
- !!x n h. [| x \<in> A; h \<in> maptree(A) -||> maptree(A);
+lemma maptree_induct [consumes 1, induct set: maptree]:
+ assumes t: "t \<in> maptree(A)"
+ and step: "!!x n h. [| x \<in> A; h \<in> maptree(A) -||> maptree(A);
\<forall>y \<in> field(h). P(y)
- |] ==> P(Sons(x,h))
- |] ==> P(t)"
+ |] ==> P(Sons(x,h))"
+ shows "P(t)"
-- {* A nicer induction rule than the standard one. *}
-proof -
- case rule_context
- assume "t \<in> maptree(A)"
- thus ?thesis
- apply induct
- apply (assumption | rule rule_context)+
- apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD])
- apply (drule FiniteFun.dom_subset [THEN subsetD])
- apply (drule Fin.dom_subset [THEN subsetD])
- apply fast
- done
-qed
+ using t
+ apply induct
+ apply (assumption | rule step)+
+ apply (erule Collect_subset [THEN FiniteFun_mono1, THEN subsetD])
+ apply (drule FiniteFun.dom_subset [THEN subsetD])
+ apply (drule Fin.dom_subset [THEN subsetD])
+ apply fast
+ done
text {*
@@ -169,22 +158,18 @@
by (fast intro!: maptree2.intros [unfolded maptree2.con_defs]
elim: maptree2.cases [unfolded maptree2.con_defs])
-lemma maptree2_induct [induct set: maptree2]:
- "[| t \<in> maptree2(A, B);
- !!x n h. [| x \<in> A; h \<in> B -||> maptree2(A,B); \<forall>y \<in> range(h). P(y)
- |] ==> P(Sons2(x,h))
- |] ==> P(t)"
-proof -
- case rule_context
- assume "t \<in> maptree2(A, B)"
- thus ?thesis
- apply induct
- apply (assumption | rule rule_context)+
- apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD])
- apply (drule FiniteFun.dom_subset [THEN subsetD])
- apply (drule Fin.dom_subset [THEN subsetD])
- apply fast
- done
-qed
+lemma maptree2_induct [consumes 1, induct set: maptree2]:
+ assumes t: "t \<in> maptree2(A, B)"
+ and step: "!!x n h. [| x \<in> A; h \<in> B -||> maptree2(A,B); \<forall>y \<in> range(h). P(y)
+ |] ==> P(Sons2(x,h))"
+ shows "P(t)"
+ using t
+ apply induct
+ apply (assumption | rule step)+
+ apply (erule FiniteFun_mono [OF subset_refl Collect_subset, THEN subsetD])
+ apply (drule FiniteFun.dom_subset [THEN subsetD])
+ apply (drule Fin.dom_subset [THEN subsetD])
+ apply fast
+ done
end