# HG changeset patch
# User nipkow
# Date 1353568993 -3600
# Node ID 4fc4237488abaddd65ca7f760651631140663917
# Parent  a29be9d067d2d0db40d96137fc90ab458a15ff8f
tuned names

diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Ass.thy
--- a/src/HOL/IMP/Def_Ass.thy	Wed Nov 21 21:08:20 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-theory Def_Ass imports Vars Com
-begin
-
-subsection "Definite Assignment Analysis"
-
-inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
-Skip: "D A SKIP A" |
-Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
-Seq: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |
-If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^isub>1 A\<^isub>1;  D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
-  D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
-While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
-
-inductive_cases [elim!]:
-"D A SKIP A'"
-"D A (x ::= a) A'"
-"D A (c1;c2) A'"
-"D A (IF b THEN c1 ELSE c2) A'"
-"D A (WHILE b DO c) A'"
-
-lemma D_incr: 
-  "D A c A' \<Longrightarrow> A \<subseteq> A'"
-by (induct rule: D.induct) auto
-
-end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Ass_Big.thy
--- a/src/HOL/IMP/Def_Ass_Big.thy	Wed Nov 21 21:08:20 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Def_Ass_Big imports Com Def_Ass_Exp
-begin
-
-subsection "Initialization-Sensitive Big Step Semantics"
-
-inductive
-  big_step :: "(com \<times> state option) \<Rightarrow> state option \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
-where
-None: "(c,None) \<Rightarrow> None" |
-Skip: "(SKIP,s) \<Rightarrow> s" |
-AssignNone: "aval a s = None \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> None" |
-Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> Some(s(x := Some i))" |
-Seq:    "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s\<^isub>1) \<Rightarrow> s\<^isub>3" |
-
-IfNone:  "bval b s = None \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> None" |
-IfTrue:  "\<lbrakk> bval b s = Some True;  (c\<^isub>1,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
-  (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> s'" |
-IfFalse: "\<lbrakk> bval b s = Some False;  (c\<^isub>2,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
-  (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> s'" |
-
-WhileNone: "bval b s = None \<Longrightarrow> (WHILE b DO c,Some s) \<Rightarrow> None" |
-WhileFalse: "bval b s = Some False \<Longrightarrow> (WHILE b DO c,Some s) \<Rightarrow> Some s" |
-WhileTrue:
-  "\<lbrakk> bval b s = Some True;  (c,Some s) \<Rightarrow> s';  (WHILE b DO c,s') \<Rightarrow> s'' \<rbrakk> \<Longrightarrow>
-  (WHILE b DO c,Some s) \<Rightarrow> s''"
-
-lemmas big_step_induct = big_step.induct[split_format(complete)]
-
-end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Ass_Exp.thy
--- a/src/HOL/IMP/Def_Ass_Exp.thy	Wed Nov 21 21:08:20 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Def_Ass_Exp imports Vars
-begin
-
-subsection "Initialization-Sensitive Expressions Evaluation"
-
-type_synonym state = "vname \<Rightarrow> val option"
-
-
-fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where
-"aval (N i) s = Some i" |
-"aval (V x) s = s x" |
-"aval (Plus a\<^isub>1 a\<^isub>2) s =
-  (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
-     (Some i\<^isub>1,Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1+i\<^isub>2) | _ \<Rightarrow> None)"
-
-
-fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
-"bval (Bc v) s = Some v" |
-"bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" |
-"bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of
-  (Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2) | _ \<Rightarrow> None)" |
-"bval (Less a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
- (Some i\<^isub>1, Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1 < i\<^isub>2) | _ \<Rightarrow> None)"
-
-
-lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i"
-by (induct a) auto
-
-lemma bval_Some: "vars b \<subseteq> dom s \<Longrightarrow> \<exists> bv. bval b s = Some bv"
-by (induct b) (auto dest!: aval_Some)
-
-end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Ass_Small.thy
--- a/src/HOL/IMP/Def_Ass_Small.thy	Wed Nov 21 21:08:20 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Def_Ass_Small imports Star Com Def_Ass_Exp
-begin
-
-subsection "Initialization-Sensitive Small Step Semantics"
-
-inductive
-  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
-where
-Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
-
-Seq1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
-Seq2:   "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" |
-
-IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
-IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
-
-While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
-
-lemmas small_step_induct = small_step.induct[split_format(complete)]
-
-abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
-where "x \<rightarrow>* y == star small_step x y"
-
-end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Ass_Sound_Big.thy
--- a/src/HOL/IMP/Def_Ass_Sound_Big.thy	Wed Nov 21 21:08:20 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Def_Ass_Sound_Big imports Def_Ass Def_Ass_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
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Ass_Sound_Small.thy
--- a/src/HOL/IMP/Def_Ass_Sound_Small.thy	Wed Nov 21 21:08:20 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Def_Ass_Sound_Small imports Def_Ass Def_Ass_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> c' \<noteq> SKIP
-   \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
-apply(induction arbitrary: A' rule:star_induct)
-apply (metis progress)
-by (metis D_preservation)
-
-end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Init.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Init.thy	Thu Nov 22 08:23:13 2012 +0100
@@ -0,0 +1,26 @@
+theory Def_Init
+imports Vars Com
+begin
+
+subsection "Definite Initialization Analysis"
+
+inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
+Skip: "D A SKIP A" |
+Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
+Seq: "\<lbrakk> D A\<^isub>1 c\<^isub>1 A\<^isub>2;  D A\<^isub>2 c\<^isub>2 A\<^isub>3 \<rbrakk> \<Longrightarrow> D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" |
+If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^isub>1 A\<^isub>1;  D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
+  D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
+While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
+
+inductive_cases [elim!]:
+"D A SKIP A'"
+"D A (x ::= a) A'"
+"D A (c1;c2) A'"
+"D A (IF b THEN c1 ELSE c2) A'"
+"D A (WHILE b DO c) A'"
+
+lemma D_incr: 
+  "D A c A' \<Longrightarrow> A \<subseteq> A'"
+by (induct rule: D.induct) auto
+
+end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Init_Big.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Init_Big.thy	Thu Nov 22 08:23:13 2012 +0100
@@ -0,0 +1,32 @@
+(* Author: Tobias Nipkow *)
+
+theory Def_Init_Big
+imports Com Def_Init_Exp
+begin
+
+subsection "Initialization-Sensitive Big Step Semantics"
+
+inductive
+  big_step :: "(com \<times> state option) \<Rightarrow> state option \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
+where
+None: "(c,None) \<Rightarrow> None" |
+Skip: "(SKIP,s) \<Rightarrow> s" |
+AssignNone: "aval a s = None \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> None" |
+Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> Some(s(x := Some i))" |
+Seq:    "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2 \<Longrightarrow> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s\<^isub>1) \<Rightarrow> s\<^isub>3" |
+
+IfNone:  "bval b s = None \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> None" |
+IfTrue:  "\<lbrakk> bval b s = Some True;  (c\<^isub>1,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
+  (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> s'" |
+IfFalse: "\<lbrakk> bval b s = Some False;  (c\<^isub>2,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
+  (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> s'" |
+
+WhileNone: "bval b s = None \<Longrightarrow> (WHILE b DO c,Some s) \<Rightarrow> None" |
+WhileFalse: "bval b s = Some False \<Longrightarrow> (WHILE b DO c,Some s) \<Rightarrow> Some s" |
+WhileTrue:
+  "\<lbrakk> bval b s = Some True;  (c,Some s) \<Rightarrow> s';  (WHILE b DO c,s') \<Rightarrow> s'' \<rbrakk> \<Longrightarrow>
+  (WHILE b DO c,Some s) \<Rightarrow> s''"
+
+lemmas big_step_induct = big_step.induct[split_format(complete)]
+
+end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Init_Exp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Init_Exp.thy	Thu Nov 22 08:23:13 2012 +0100
@@ -0,0 +1,35 @@
+(* Author: Tobias Nipkow *)
+
+theory Def_Init_Exp
+imports Vars
+begin
+
+subsection "Initialization-Sensitive Expressions Evaluation"
+
+type_synonym state = "vname \<Rightarrow> val option"
+
+
+fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val option" where
+"aval (N i) s = Some i" |
+"aval (V x) s = s x" |
+"aval (Plus a\<^isub>1 a\<^isub>2) s =
+  (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
+     (Some i\<^isub>1,Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1+i\<^isub>2) | _ \<Rightarrow> None)"
+
+
+fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
+"bval (Bc v) s = Some v" |
+"bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" |
+"bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of
+  (Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2) | _ \<Rightarrow> None)" |
+"bval (Less a\<^isub>1 a\<^isub>2) s = (case (aval a\<^isub>1 s, aval a\<^isub>2 s) of
+ (Some i\<^isub>1, Some i\<^isub>2) \<Rightarrow> Some(i\<^isub>1 < i\<^isub>2) | _ \<Rightarrow> None)"
+
+
+lemma aval_Some: "vars a \<subseteq> dom s \<Longrightarrow> \<exists> i. aval a s = Some i"
+by (induct a) auto
+
+lemma bval_Some: "vars b \<subseteq> dom s \<Longrightarrow> \<exists> bv. bval b s = Some bv"
+by (induct b) (auto dest!: aval_Some)
+
+end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Init_Small.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Init_Small.thy	Thu Nov 22 08:23:13 2012 +0100
@@ -0,0 +1,27 @@
+(* Author: Tobias Nipkow *)
+
+theory Def_Init_Small
+imports Star Com Def_Init_Exp
+begin
+
+subsection "Initialization-Sensitive Small Step Semantics"
+
+inductive
+  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
+where
+Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
+
+Seq1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
+Seq2:   "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" |
+
+IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
+IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
+
+While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+
+lemmas small_step_induct = small_step.induct[split_format(complete)]
+
+abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
+where "x \<rightarrow>* y == star small_step x y"
+
+end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Init_Sound_Big.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Init_Sound_Big.thy	Thu Nov 22 08:23:13 2012 +0100
@@ -0,0 +1,41 @@
+(* 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
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/IMP/Def_Init_Sound_Small.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Def_Init_Sound_Small.thy	Thu Nov 22 08:23:13 2012 +0100
@@ -0,0 +1,57 @@
+(* 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> c' \<noteq> SKIP
+   \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
+apply(induction arbitrary: A' rule:star_induct)
+apply (metis progress)
+by (metis D_preservation)
+
+end
diff -r a29be9d067d2 -r 4fc4237488ab src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Nov 21 21:08:20 2012 +0100
+++ b/src/HOL/ROOT	Thu Nov 22 08:23:13 2012 +0100
@@ -98,8 +98,8 @@
     Poly_Types
     Sec_Typing
     Sec_TypingT
-    Def_Ass_Sound_Big
-    Def_Ass_Sound_Small
+    Def_Init_Sound_Big
+    Def_Init_Sound_Small
     Live
     Live_True
     Hoare_Examples