--- a/src/HOL/IMP/Def_Init_Big.thy Wed Jul 24 13:03:53 2013 +0200
+++ b/src/HOL/IMP/Def_Init_Big.thy Wed Jul 24 22:54:47 2013 +0200
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Def_Init_Big
-imports Com Def_Init_Exp
+imports Def_Init_Exp Def_Init
begin
subsection "Initialization-Sensitive Big Step Semantics"
@@ -29,4 +29,40 @@
lemmas big_step_induct = big_step.induct[split_format(complete)]
+
+subsection "Soundness wrt Big Steps"
+
+text{* Note the special form of the induction because one of the arguments
+of the inductive predicate is not a variable but the term @{term"Some s"}: *}
+
+theorem Sound:
+ "\<lbrakk> (c,Some s) \<Rightarrow> s'; D A c A'; A \<subseteq> dom s \<rbrakk>
+ \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
+proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
+ case AssignNone thus ?case
+ by auto (metis aval_Some option.simps(3) subset_trans)
+next
+ case Seq thus ?case by auto metis
+next
+ case IfTrue thus ?case by auto blast
+next
+ case IfFalse thus ?case by auto blast
+next
+ case IfNone thus ?case
+ by auto (metis bval_Some option.simps(3) order_trans)
+next
+ case WhileNone thus ?case
+ by auto (metis bval_Some option.simps(3) order_trans)
+next
+ case (WhileTrue b s c s' s'')
+ from `D A (WHILE b DO c) A'` obtain A' where "D A c A'" by blast
+ then obtain t' where "s' = Some t'" "A \<subseteq> dom t'"
+ by (metis D_incr WhileTrue(3,7) subset_trans)
+ from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case .
+qed auto
+
+corollary sound: "\<lbrakk> D (dom s) c A'; (c,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> s' \<noteq> None"
+by (metis Sound not_Some_eq subset_refl)
+
end
+
--- a/src/HOL/IMP/Def_Init_Small.thy Wed Jul 24 13:03:53 2013 +0200
+++ b/src/HOL/IMP/Def_Init_Small.thy Wed Jul 24 22:54:47 2013 +0200
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Def_Init_Small
-imports Star Com Def_Init_Exp
+imports Star Def_Init_Exp Def_Init
begin
subsection "Initialization-Sensitive Small Step Semantics"
@@ -24,4 +24,55 @@
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
where "x \<rightarrow>* y == star small_step x y"
+
+subsection "Soundness wrt Small Steps"
+
+theorem progress:
+ "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
+proof (induction c arbitrary: s A')
+ case Assign thus ?case by auto (metis aval_Some small_step.Assign)
+next
+ case (If b c1 c2)
+ then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
+ then show ?case
+ by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
+qed (fastforce intro: small_step.intros)+
+
+lemma D_mono: "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
+proof (induction c arbitrary: A A' M)
+ case Seq thus ?case by auto (metis D.intros(3))
+next
+ case (If b c1 c2)
+ then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
+ by auto
+ with If.IH `A \<subseteq> A'` obtain M1' M2'
+ where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
+ hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
+ using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
+ thus ?case by metis
+next
+ case While thus ?case by auto (metis D.intros(5) subset_trans)
+qed (auto intro: D.intros)
+
+theorem D_preservation:
+ "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
+proof (induction arbitrary: A rule: small_step_induct)
+ case (While b c s)
+ then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
+ moreover
+ then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
+ ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
+ by (metis D.If[OF `vars b \<subseteq> dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
+ thus ?case by (metis D_incr `A = dom s`)
+next
+ case Seq2 thus ?case by auto (metis D_mono D.intros(3))
+qed (auto intro: D.intros)
+
+theorem D_sound:
+ "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A'
+ \<Longrightarrow> (\<exists>cs''. (c',s') \<rightarrow> cs'') \<or> c' = SKIP"
+apply(induction arbitrary: A' rule:star_induct)
+apply (metis progress)
+by (metis D_preservation)
+
end
--- a/src/HOL/IMP/Def_Init_Sound_Big.thy Wed Jul 24 13:03:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Def_Init_Sound_Big
-imports Def_Init Def_Init_Big
-begin
-
-subsection "Soundness wrt Big Steps"
-
-text{* Note the special form of the induction because one of the arguments
-of the inductive predicate is not a variable but the term @{term"Some s"}: *}
-
-theorem Sound:
- "\<lbrakk> (c,Some s) \<Rightarrow> s'; D A c A'; A \<subseteq> dom s \<rbrakk>
- \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
-proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
- case AssignNone thus ?case
- by auto (metis aval_Some option.simps(3) subset_trans)
-next
- case Seq thus ?case by auto metis
-next
- case IfTrue thus ?case by auto blast
-next
- case IfFalse thus ?case by auto blast
-next
- case IfNone thus ?case
- by auto (metis bval_Some option.simps(3) order_trans)
-next
- case WhileNone thus ?case
- by auto (metis bval_Some option.simps(3) order_trans)
-next
- case (WhileTrue b s c s' s'')
- from `D A (WHILE b DO c) A'` obtain A' where "D A c A'" by blast
- then obtain t' where "s' = Some t'" "A \<subseteq> dom t'"
- by (metis D_incr WhileTrue(3,7) subset_trans)
- from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case .
-qed auto
-
-corollary sound: "\<lbrakk> D (dom s) c A'; (c,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> s' \<noteq> None"
-by (metis Sound not_Some_eq subset_refl)
-
-end
--- a/src/HOL/IMP/Def_Init_Sound_Small.thy Wed Jul 24 13:03:53 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Def_Init_Sound_Small
-imports Def_Init Def_Init_Small
-begin
-
-subsection "Soundness wrt Small Steps"
-
-theorem progress:
- "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> EX cs'. (c,s) \<rightarrow> cs'"
-proof (induction c arbitrary: s A')
- case Assign thus ?case by auto (metis aval_Some small_step.Assign)
-next
- case (If b c1 c2)
- then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
- then show ?case
- by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
-qed (fastforce intro: small_step.intros)+
-
-lemma D_mono: "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
-proof (induction c arbitrary: A A' M)
- case Seq thus ?case by auto (metis D.intros(3))
-next
- case (If b c1 c2)
- then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
- by auto
- with If.IH `A \<subseteq> A'` obtain M1' M2'
- where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
- hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
- using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
- thus ?case by metis
-next
- case While thus ?case by auto (metis D.intros(5) subset_trans)
-qed (auto intro: D.intros)
-
-theorem D_preservation:
- "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
-proof (induction arbitrary: A rule: small_step_induct)
- case (While b c s)
- then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
- moreover
- then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
- ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
- by (metis D.If[OF `vars b \<subseteq> dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
- thus ?case by (metis D_incr `A = dom s`)
-next
- case Seq2 thus ?case by auto (metis D_mono D.intros(3))
-qed (auto intro: D.intros)
-
-theorem D_sound:
- "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A'
- \<Longrightarrow> (\<exists>cs''. (c',s') \<rightarrow> cs'') \<or> c' = SKIP"
-apply(induction arbitrary: A' rule:star_induct)
-apply (metis progress)
-by (metis D_preservation)
-
-end
--- a/src/HOL/ROOT Wed Jul 24 13:03:53 2013 +0200
+++ b/src/HOL/ROOT Wed Jul 24 22:54:47 2013 +0200
@@ -125,8 +125,9 @@
Poly_Types
Sec_Typing
Sec_TypingT
- Def_Init_Sound_Big
- Def_Init_Sound_Small
+ Def_Init_Big
+ Def_Init_Small
+ Fold
Live
Live_True
Hoare_Examples
@@ -147,7 +148,6 @@
Procs_Stat_Vars_Stat
C_like
OO
- Fold
files "document/root.bib" "document/root.tex"
session "HOL-IMPP" in IMPP = HOL +