--- a/src/HOL/IMP/ACom.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/ACom.thy Sat Apr 28 07:38:22 2012 +0200
@@ -10,12 +10,12 @@
subsection "Annotated Commands"
datatype 'a acom =
- SKIP 'a ("SKIP {_}" 61) |
- Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
- Semi "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) |
- If bexp "('a acom)" "('a acom)" 'a
+ SKIP 'a ("SKIP {_}" 61) |
+ Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
+ Seq "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) |
+ If bexp "('a acom)" "('a acom)" 'a
("(IF _/ THEN _/ ELSE _//{_})" [0, 0, 61, 0] 61) |
- While 'a bexp "('a acom)" 'a
+ While 'a bexp "('a acom)" 'a
("({_}//WHILE _/ DO (_)//{_})" [0, 0, 61, 0] 61)
fun post :: "'a acom \<Rightarrow>'a" where
@@ -72,7 +72,7 @@
"map_acom f c = x ::= e {S'} \<longleftrightarrow> (\<exists>S. c = x::=e {S} \<and> S' = f S)"
by (cases c) auto
-lemma map_acom_Semi:
+lemma map_acom_Seq:
"map_acom f c = c1';c2' \<longleftrightarrow>
(\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')"
by (cases c) auto
@@ -99,7 +99,7 @@
"strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
by (cases c) simp_all
-lemma strip_eq_Semi:
+lemma strip_eq_Seq:
"strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
by (cases c) simp_all
@@ -119,7 +119,7 @@
lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
apply(induct C2 arbitrary: C1)
-apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Semi strip_eq_If strip_eq_While)
+apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Seq strip_eq_If strip_eq_While)
done
lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
--- a/src/HOL/IMP/Abs_Int0.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Sat Apr 28 07:38:22 2012 +0200
@@ -332,7 +332,7 @@
by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update
split: option.splits del:subsetD)
next
- case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+ case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
by (metis le_post post_map_acom)
next
case (If b C1 C2 P)
--- a/src/HOL/IMP/Abs_Int1.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Sat Apr 28 07:38:22 2012 +0200
@@ -96,7 +96,7 @@
by(fastforce simp: Assign_le map_acom_Assign wt_st_def
intro: aval'_sound in_gamma_update split: option.splits)
next
- case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+ case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
by (metis le_post post_map_acom wt_post)
next
case (If b C1 C2 P)
--- a/src/HOL/IMP/Abs_Int2.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Sat Apr 28 07:38:22 2012 +0200
@@ -189,7 +189,7 @@
by (fastforce simp: Assign_le map_acom_Assign wt_option_def wt_st_def
intro: aval'_sound in_gamma_update split: option.splits del:subsetD)
next
- case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+ case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
by (metis le_post post_map_acom wt_post)
next
case (If b C1 C2 P)
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy Sat Apr 28 07:38:22 2012 +0200
@@ -44,7 +44,7 @@
case Assign thus ?case
by (auto simp: lookup_update aval'_sound)
next
- case Semi thus ?case by auto
+ case Seq thus ?case by auto
next
case If thus ?case
by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Sat Apr 28 07:38:22 2012 +0200
@@ -160,7 +160,7 @@
next
case Assign thus ?case by (auto simp: aval'_sound)
next
- case Semi thus ?case by auto
+ case Seq thus ?case by auto
next
case If thus ?case by(auto simp: in_rep_join)
next
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Sat Apr 28 07:38:22 2012 +0200
@@ -187,7 +187,7 @@
case Assign thus ?case
by (auto simp: lookup_update aval'_sound)
next
- case Semi thus ?case by fastforce
+ case Seq thus ?case by fastforce
next
case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
next
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Sat Apr 28 07:38:22 2012 +0200
@@ -324,7 +324,7 @@
by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update
split: option.splits del:subsetD)
next
- case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+ case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
by (metis le_post post_map_acom)
next
case (If b c1 c2 P)
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Sat Apr 28 07:38:22 2012 +0200
@@ -66,7 +66,7 @@
by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update
split: option.splits del:subsetD)
next
- case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+ case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
by (metis le_post post_map_acom)
next
case (If b c1 c2 P)
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Sat Apr 28 07:38:22 2012 +0200
@@ -202,7 +202,7 @@
by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update
split: option.splits del:subsetD)
next
- case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
+ case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
by (metis le_post post_map_acom)
next
case (If b cs1 cs2 P)
--- a/src/HOL/IMP/Big_Step.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Big_Step.thy Sat Apr 28 07:38:22 2012 +0200
@@ -10,7 +10,7 @@
where
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
-Semi: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+Seq: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
(c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
@@ -25,7 +25,7 @@
text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEx}{% *}
schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
-apply(rule Semi)
+apply(rule Seq)
apply(rule Assign)
apply simp
apply(rule Assign)
@@ -89,8 +89,8 @@
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
thm AssignE
-inductive_cases SemiE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
-thm SemiE
+inductive_cases SeqE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
+thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
thm IfE
@@ -162,7 +162,7 @@
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
-- "now we can build a derivation tree for the @{text IF}"
-- "first, the body of the True-branch:"
- hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)
+ hence "(c; ?w, s) \<Rightarrow> t" by (rule Seq)
-- "then the whole @{text IF}"
with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
}
@@ -184,7 +184,7 @@
-- {* then this time only the @{text IfTrue} rule can have be used *}
{ assume "bval b s"
with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
- -- "and for this, only the Semi-rule is applicable:"
+ -- "and for this, only the Seq-rule is applicable:"
then obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
-- "with this information, we can build a derivation tree for the @{text WHILE}"
--- a/src/HOL/IMP/C_like.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/C_like.thy Sat Apr 28 07:38:22 2012 +0200
@@ -24,7 +24,7 @@
com = SKIP
| Assign aexp aexp ("_ ::= _" [61, 61] 61)
| New aexp aexp
- | Semi com com ("_;/ _" [60, 61] 60)
+ | Seq com com ("_;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
@@ -34,7 +34,7 @@
Skip: "(SKIP,sn) \<Rightarrow> sn" |
Assign: "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" |
New: "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)" |
-Semi: "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2; (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
+Seq: "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2; (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
(c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3" |
IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
--- a/src/HOL/IMP/Collecting.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Collecting.thy Sat Apr 28 07:38:22 2012 +0200
@@ -30,7 +30,7 @@
lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
by (cases c) auto
-lemma Semi_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
+lemma Seq_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
by (cases c) auto
lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow>
@@ -52,7 +52,7 @@
next
case goal3 thus ?case
apply(induct x y arbitrary: z rule: less_eq_acom.induct)
- apply (auto intro: le_trans simp: SKIP_le Assign_le Semi_le If_le While_le)
+ apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le)
done
next
case goal4 thus ?case
@@ -94,7 +94,7 @@
case goal1
have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
proof(induction a arbitrary: A)
- case Semi from Semi.prems show ?case by(force intro!: Semi.IH)
+ case Seq from Seq.prems show ?case by(force intro!: Seq.IH)
next
case If from If.prems show ?case by(force intro!: If.IH)
next
@@ -109,8 +109,8 @@
next
case Assign thus ?case by (force simp:Assign_le)
next
- case Semi from Semi.prems show ?case
- by (force intro!: Semi.IH simp:Semi_le)
+ case Seq from Seq.prems show ?case
+ by (force intro!: Seq.IH simp:Seq_le)
next
case If from If.prems show ?case by (force simp: If_le intro!: If.IH)
next
@@ -121,8 +121,8 @@
case goal3
have "strip(lift Inter i A) = i"
proof(induction i arbitrary: A)
- case Semi from Semi.prems show ?case
- by (fastforce simp: strip_eq_Semi subset_iff intro!: Semi.IH)
+ case Seq from Seq.prems show ?case
+ by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH)
next
case If from If.prems show ?case
by (fastforce intro!: If.IH simp: strip_eq_If)
--- a/src/HOL/IMP/Com.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Com.thy Sat Apr 28 07:38:22 2012 +0200
@@ -5,7 +5,7 @@
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
- | Semi com com ("_;/ _" [60, 61] 60)
+ | Seq com com ("_;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
--- a/src/HOL/IMP/Comp_Rev.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy Sat Apr 28 07:38:22 2012 +0200
@@ -224,10 +224,10 @@
next
case Assign thus ?case by simp
next
- case (Semi c1 c2)
- from Semi.prems
+ case (Seq c1 c2)
+ from Seq.prems
show ?case
- by (fastforce dest: Semi.IH [THEN subsetD])
+ by (fastforce dest: Seq.IH [THEN subsetD])
next
case (If b c1 c2)
from If.prems
@@ -492,7 +492,7 @@
thus ?case
by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
next
- case (Semi c1 c2)
+ case (Seq c1 c2)
thus ?case by (fastforce dest!: exec_n_split_full)
next
case (If b c1 c2)
--- a/src/HOL/IMP/Compiler.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Compiler.thy Sat Apr 28 07:38:22 2012 +0200
@@ -259,13 +259,13 @@
case (Assign x a s)
show ?case by (fastforce simp:fun_upd_def cong: if_cong)
next
- case (Semi c1 s1 s2 c2 s3)
+ case (Seq c1 s1 s2 c2 s3)
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
- using Semi.IH(1) by fastforce
+ using Seq.IH(1) by fastforce
moreover
have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
- using Semi.IH(2) by fastforce
+ using Seq.IH(2) by fastforce
ultimately show ?case by simp (blast intro: exec_trans)
next
case (WhileTrue b s1 c s2 s3)
--- a/src/HOL/IMP/Def_Ass.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Def_Ass.thy Sat Apr 28 07:38:22 2012 +0200
@@ -6,7 +6,7 @@
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)" |
-Semi: "\<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" |
+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"
--- a/src/HOL/IMP/Def_Ass_Big.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Def_Ass_Big.thy Sat Apr 28 07:38:22 2012 +0200
@@ -12,7 +12,7 @@
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))" |
-Semi: "(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" |
+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>
--- a/src/HOL/IMP/Def_Ass_Small.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Def_Ass_Small.thy Sat Apr 28 07:38:22 2012 +0200
@@ -10,8 +10,8 @@
where
Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
-Semi1: "(SKIP;c,s) \<rightarrow> (c,s)" |
-Semi2: "(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')" |
+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)" |
--- a/src/HOL/IMP/Def_Ass_Sound_Big.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy Sat Apr 28 07:38:22 2012 +0200
@@ -16,7 +16,7 @@
case AssignNone thus ?case
by auto (metis aval_Some option.simps(3) subset_trans)
next
- case Semi thus ?case by auto metis
+ case Seq thus ?case by auto metis
next
case IfTrue thus ?case by auto blast
next
--- a/src/HOL/IMP/Def_Ass_Sound_Small.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy Sat Apr 28 07:38:22 2012 +0200
@@ -18,7 +18,7 @@
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 Semi thus ?case by auto (metis D.intros(3))
+ 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"
@@ -40,10 +40,10 @@
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.Semi[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
+ 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 Semi2 thus ?case by auto (metis D_mono D.intros(3))
+ case Seq2 thus ?case by auto (metis D_mono D.intros(3))
qed (auto intro: D.intros)
theorem D_sound:
--- a/src/HOL/IMP/Fold.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Fold.thy Sat Apr 28 07:38:22 2012 +0200
@@ -82,13 +82,13 @@
lemma defs_restrict:
"defs c t |` (- lnames c) = t |` (- lnames c)"
proof (induction c arbitrary: t)
- case (Semi c1 c2)
+ case (Seq c1 c2)
hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"
by simp
hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
t |` (- lnames c1) |` (-lnames c2)" by simp
moreover
- from Semi
+ from Seq
have "defs c2 (defs c1 t) |` (- lnames c2) =
defs c1 t |` (- lnames c2)"
by simp
@@ -121,9 +121,9 @@
thus ?case
by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
next
- case (Semi c1 s1 s2 c2 s3)
- have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
- hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2))
+ case (Seq c1 s1 s2 c2 s3)
+ have "approx (defs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems])
+ hence "approx (defs c2 (defs c1 t)) s3" by (rule Seq.IH(2))
thus ?case by simp
next
case (IfTrue b s c1 s')
@@ -155,15 +155,15 @@
case Assign
thus ?case by (clarsimp simp: approx_def)
next
- case (Semi c1 s1 s2 c2 s3)
+ case (Seq c1 s1 s2 c2 s3)
hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1"
by (simp add: Int_commute)
hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
- by (rule Semi)
+ by (rule Seq)
hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
by (simp add: Int_commute)
hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
- by (rule Semi)
+ by (rule Seq)
thus ?case by simp
next
case (IfTrue b s c1 s' c2)
@@ -196,8 +196,8 @@
case Assign
show ?case by (simp add: equiv_up_to_def)
next
- case Semi
- thus ?case by (auto intro!: equiv_up_to_semi)
+ case Seq
+ thus ?case by (auto intro!: equiv_up_to_seq)
next
case If
thus ?case by (auto intro!: equiv_up_to_if_weak)
@@ -293,13 +293,13 @@
lemma bdefs_restrict:
"bdefs c t |` (- lnames c) = t |` (- lnames c)"
proof (induction c arbitrary: t)
- case (Semi c1 c2)
+ case (Seq c1 c2)
hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"
by simp
hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
t |` (- lnames c1) |` (-lnames c2)" by simp
moreover
- from Semi
+ from Seq
have "bdefs c2 (bdefs c1 t) |` (- lnames c2) =
bdefs c1 t |` (- lnames c2)"
by simp
@@ -334,9 +334,9 @@
thus ?case
by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
next
- case (Semi c1 s1 s2 c2 s3)
- have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
- hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2))
+ case (Seq c1 s1 s2 c2 s3)
+ have "approx (bdefs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems])
+ hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Seq.IH(2))
thus ?case by simp
next
case (IfTrue b s c1 s')
@@ -377,8 +377,8 @@
case Assign
thus ?case by (simp add: equiv_up_to_def)
next
- case Semi
- thus ?case by (auto intro!: equiv_up_to_semi)
+ case Seq
+ thus ?case by (auto intro!: equiv_up_to_seq)
next
case (If b c1 c2)
hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim>
--- a/src/HOL/IMP/Hoare.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Hoare.thy Sat Apr 28 07:38:22 2012 +0200
@@ -19,8 +19,8 @@
Assign: "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}" |
-Semi: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q}; \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
- \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}" |
+Seq: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q}; \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
+ \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}" |
If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
\<Longrightarrow> \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
@@ -31,9 +31,9 @@
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
\<Longrightarrow> \<turnstile> {P'} c {Q'}"
-lemmas [simp] = hoare.Skip hoare.Assign hoare.Semi If
+lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If
-lemmas [intro!] = hoare.Skip hoare.Assign hoare.Semi hoare.If
+lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If
lemma strengthen_pre:
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
--- a/src/HOL/IMP/HoareT.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/HoareT.thy Sat Apr 28 07:38:22 2012 +0200
@@ -20,7 +20,7 @@
where
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" |
Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" |
-Semi: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}" |
+Seq: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}" |
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk>
\<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
While:
@@ -57,19 +57,19 @@
DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}"
-apply(rule Semi)
+apply(rule Seq)
prefer 2
apply(rule While'
[where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"
and f = "\<lambda>s. nat (n - s ''y'')"])
-apply(rule Semi)
+apply(rule Seq)
prefer 2
apply(rule Assign)
apply(rule Assign')
apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
apply clarsimp
apply fastforce
-apply(rule Semi)
+apply(rule Seq)
prefer 2
apply(rule Assign)
apply(rule Assign')
@@ -182,7 +182,7 @@
next
case Assign show ?case by simp (blast intro:hoaret.Assign)
next
- case Semi thus ?case by simp (blast intro:hoaret.Semi)
+ case Seq thus ?case by simp (blast intro:hoaret.Seq)
next
case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)
next
--- a/src/HOL/IMP/Hoare_Examples.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy Sat Apr 28 07:38:22 2012 +0200
@@ -51,17 +51,17 @@
pulling back the postcondition towards the precondition. *}
lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
-apply(rule hoare.Semi)
+apply(rule hoare.Seq)
prefer 2
apply(rule While'
[where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"])
-apply(rule Semi)
+apply(rule Seq)
prefer 2
apply(rule Assign)
apply(rule Assign')
apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps)
apply(fastforce)
-apply(rule Semi)
+apply(rule Seq)
prefer 2
apply(rule Assign)
apply(rule Assign')
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Sat Apr 28 07:38:22 2012 +0200
@@ -35,7 +35,7 @@
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
by (rule ext) (auto simp: wp_def)
-lemma wp_Semi[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
+lemma wp_Seq[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
by (rule ext) (auto simp: wp_def)
lemma wp_If[simp]:
@@ -60,7 +60,7 @@
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
proof(induction c arbitrary: Q)
- case Semi thus ?case by(auto intro: Semi)
+ case Seq thus ?case by(auto intro: Seq)
next
case (If b c1 c2)
let ?If = "IF b THEN c1 ELSE c2"
--- a/src/HOL/IMP/Live.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Live.thy Sat Apr 28 07:38:22 2012 +0200
@@ -54,11 +54,11 @@
case Assign then show ?case
by (auto simp: ball_Un)
next
- case (Semi c1 s1 s2 c2 s3 X t1)
- from Semi.IH(1) Semi.prems obtain t2 where
+ case (Seq c1 s1 s2 c2 s3 X t1)
+ from Seq.IH(1) Seq.prems obtain t2 where
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
by simp blast
- from Semi.IH(2)[OF s2t2] obtain t3 where
+ from Seq.IH(2)[OF s2t2] obtain t3 where
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
by auto
show ?case using t12 t23 s3t3 by auto
@@ -118,11 +118,11 @@
case Assign then show ?case
by (auto simp: ball_Un)
next
- case (Semi c1 s1 s2 c2 s3 X t1)
- from Semi.IH(1) Semi.prems obtain t2 where
+ case (Seq c1 s1 s2 c2 s3 X t1)
+ from Seq.IH(1) Seq.prems obtain t2 where
t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
by simp blast
- from Semi.IH(2)[OF s2t2] obtain t3 where
+ from Seq.IH(2)[OF s2t2] obtain t3 where
t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
by auto
show ?case using t12 t23 s3t3 by auto
@@ -172,7 +172,7 @@
lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
by (cases c) auto
-lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
+lemma Seq_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
(EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
by (cases c) auto
@@ -194,11 +194,11 @@
case Assign then show ?case
by (auto simp: ball_Un)
next
- case (Semi bc1 s1 s2 bc2 s3 c X t1)
+ case (Seq bc1 s1 s2 bc2 s3 c X t1)
then obtain c1 c2 where c: "c = c1;c2"
and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
- note IH = Semi.hyps(2,4)
- from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
+ note IH = Seq.hyps(2,4)
+ from IH(1)[OF bc1, of t1] Seq.prems c obtain t2 where
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
from IH(2)[OF bc2 s2t2] obtain t3 where
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
--- a/src/HOL/IMP/Live_True.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Live_True.thy Sat Apr 28 07:38:22 2012 +0200
@@ -49,11 +49,11 @@
case Assign then show ?case
by (auto simp: ball_Un)
next
- case (Semi c1 s1 s2 c2 s3 X t1)
- from Semi.IH(1) Semi.prems obtain t2 where
+ case (Seq c1 s1 s2 c2 s3 X t1)
+ from Seq.IH(1) Seq.prems obtain t2 where
t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
by simp blast
- from Semi.IH(2)[OF s2t2] obtain t3 where
+ from Seq.IH(2)[OF s2t2] obtain t3 where
t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
by auto
show ?case using t12 t23 s3t3 by auto
--- a/src/HOL/IMP/OO.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/OO.thy Sat Apr 28 07:38:22 2012 +0200
@@ -22,7 +22,7 @@
Vassign string exp ("(_ ::=/ _)" [1000,61] 62) |
Fassign exp string exp ("(_\<bullet>_ ::=/ _)" [63,0,62] 62) |
Mcall exp string exp ("(_\<bullet>/_<_>)" [63,0,0] 63) |
- Semi exp exp ("_;/ _" [61,60] 60) |
+ Seq exp exp ("_;/ _" [61,60] 60) |
If bexp exp exp ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp
@@ -56,7 +56,7 @@
me \<turnstile> (me m,ve,sn\<^isub>3) \<Rightarrow> (r,ve',sn\<^isub>4) \<rbrakk>
\<Longrightarrow>
me \<turnstile> (oe\<bullet>m<pe>,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,sn\<^isub>4)" |
-Semi:
+Seq:
"\<lbrakk> me \<turnstile> (e\<^isub>1,c\<^isub>1) \<Rightarrow> (r,c\<^isub>2); me \<turnstile> (e\<^isub>2,c\<^isub>2) \<Rightarrow> c\<^isub>3 \<rbrakk> \<Longrightarrow>
me \<turnstile> (e\<^isub>1; e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
IfTrue:
--- a/src/HOL/IMP/Procs.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Procs.thy Sat Apr 28 07:38:22 2012 +0200
@@ -9,7 +9,7 @@
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
- | Semi com com ("_;/ _" [60, 61] 60)
+ | Seq com com ("_;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
| Var vname com ("(1{VAR _;;/ _})")
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Sat Apr 28 07:38:22 2012 +0200
@@ -10,7 +10,7 @@
where
Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
Assign: "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
-Semi: "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+Seq: "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
IfTrue: "\<lbrakk> bval b s; pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Sat Apr 28 07:38:22 2012 +0200
@@ -10,7 +10,7 @@
where
Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
Assign: "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
-Semi: "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+Seq: "\<lbrakk> pe \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; pe \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
IfTrue: "\<lbrakk> bval b s; pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Sat Apr 28 07:38:22 2012 +0200
@@ -17,7 +17,7 @@
where
Skip: "e \<turnstile> (SKIP,s) \<Rightarrow> s" |
Assign: "(pe,ve,f) \<turnstile> (x ::= a,s) \<Rightarrow> s(ve x := aval a (s o ve))" |
-Semi: "\<lbrakk> e \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; e \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
+Seq: "\<lbrakk> e \<turnstile> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; e \<turnstile> (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
e \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
IfTrue: "\<lbrakk> bval b (s \<circ> venv e); e \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
--- a/src/HOL/IMP/Sec_Typing.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Sec_Typing.thy Sat Apr 28 07:38:22 2012 +0200
@@ -10,7 +10,7 @@
"l \<turnstile> SKIP" |
Assign:
"\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
-Semi:
+Seq:
"\<lbrakk> l \<turnstile> c\<^isub>1; l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
If:
"\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1; max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
@@ -44,7 +44,7 @@
next
case Assign thus ?case by auto
next
- case Semi thus ?case by auto
+ case Seq thus ?case by auto
next
case (IfTrue b s c1)
hence "max (sec_bexp b) l \<turnstile> c1" by auto
@@ -85,7 +85,7 @@
thus "s y = t y" using `s = t (\<le> l)` by simp
qed
next
- case Semi thus ?case by blast
+ case Seq thus ?case by blast
next
case (IfTrue b s c1 s' c2)
have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems(2) by auto
@@ -186,7 +186,7 @@
"l \<turnstile>' SKIP" |
Assign':
"\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
-Semi':
+Seq':
"\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
If':
"\<lbrakk> sec_bexp b \<le> l; l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
@@ -199,7 +199,7 @@
apply(induction rule: sec_type.induct)
apply (metis Skip')
apply (metis Assign')
-apply (metis Semi')
+apply (metis Seq')
apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')
@@ -208,7 +208,7 @@
apply(induction rule: sec_type'.induct)
apply (metis Skip)
apply (metis Assign)
-apply (metis Semi)
+apply (metis Seq)
apply (metis min_max.sup_absorb2 If)
apply (metis min_max.sup_absorb2 While)
by (metis anti_mono)
@@ -220,7 +220,7 @@
"\<turnstile> SKIP : l" |
Assign2:
"sec x \<ge> sec_aexp a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
-Semi2:
+Seq2:
"\<lbrakk> \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk> \<Longrightarrow> \<turnstile> c\<^isub>1;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " |
If2:
"\<lbrakk> sec_bexp b \<le> min l\<^isub>1 l\<^isub>2; \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk>
@@ -233,7 +233,7 @@
apply(induction rule: sec_type2.induct)
apply (metis Skip')
apply (metis Assign' eq_imp_le)
-apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
+apply (metis Seq' anti_mono' min_max.inf.commute min_max.inf_le2)
apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
by (metis While')
@@ -241,7 +241,7 @@
apply(induction rule: sec_type'.induct)
apply (metis Skip2 le_refl)
apply (metis Assign2)
-apply (metis Semi2 min_max.inf_greatest)
+apply (metis Seq2 min_max.inf_greatest)
apply (metis If2 inf_greatest inf_nat_def le_trans)
apply (metis While2 le_trans)
by (metis le_trans)
--- a/src/HOL/IMP/Sec_TypingT.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Sec_TypingT.thy Sat Apr 28 07:38:22 2012 +0200
@@ -8,7 +8,7 @@
"l \<turnstile> SKIP" |
Assign:
"\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
-Semi:
+Seq:
"l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
If:
"\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1; max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk>
@@ -37,7 +37,7 @@
next
case Assign thus ?case by auto
next
- case Semi thus ?case by auto
+ case Seq thus ?case by auto
next
case (IfTrue b s c1)
hence "max (sec_bexp b) l \<turnstile> c1" by auto
@@ -60,7 +60,7 @@
apply(induction arbitrary: s rule: sec_type.induct)
apply (metis big_step.Skip)
apply (metis big_step.Assign)
-apply (metis big_step.Semi)
+apply (metis big_step.Seq)
apply (metis IfFalse IfTrue le0 le_antisym le_maxI2)
apply simp
done
@@ -86,7 +86,7 @@
qed
ultimately show ?case by blast
next
- case Semi thus ?case by blast
+ case Seq thus ?case by blast
next
case (IfTrue b s c1 s' c2)
have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto
@@ -175,7 +175,7 @@
"l \<turnstile>' SKIP" |
Assign':
"\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
-Semi':
+Seq':
"l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
If':
"\<lbrakk> sec_bexp b \<le> l; l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
@@ -188,7 +188,7 @@
apply(induction rule: sec_type.induct)
apply (metis Skip')
apply (metis Assign')
-apply (metis Semi')
+apply (metis Seq')
apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
by (metis While')
@@ -197,7 +197,7 @@
apply(induction rule: sec_type'.induct)
apply (metis Skip)
apply (metis Assign)
-apply (metis Semi)
+apply (metis Seq)
apply (metis min_max.sup_absorb2 If)
apply (metis While)
by (metis anti_mono)
--- a/src/HOL/IMP/Sem_Equiv.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy Sat Apr 28 07:38:22 2012 +0200
@@ -70,7 +70,7 @@
by (rule equiv_up_to_hoare)
-lemma equiv_up_to_semi:
+lemma equiv_up_to_seq:
"P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
P \<Turnstile> (c; d) \<sim> (c'; d')"
by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
--- a/src/HOL/IMP/Small_Step.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Small_Step.thy Sat Apr 28 07:38:22 2012 +0200
@@ -10,8 +10,8 @@
where
Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
-Semi1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
-Semi2: "(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')" |
+Seq1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,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 \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
@@ -54,8 +54,8 @@
thm SkipE
inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
thm AssignE
-inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct"
-thm SemiE
+inductive_cases SeqE[elim]: "(c1;c2,s) \<rightarrow> ct"
+thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"
inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct"
@@ -70,18 +70,18 @@
subsection "Equivalence with big-step semantics"
-lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
+lemma star_seq2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
proof(induction rule: star_induct)
case refl thus ?case by simp
next
case step
- thus ?case by (metis Semi2 star.step)
+ thus ?case by (metis Seq2 star.step)
qed
-lemma semi_comp:
+lemma seq_comp:
"\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
\<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
-by(blast intro: star.step star_semi2 star_trans)
+by(blast intro: star.step star_seq2 star_trans)
text{* The following proof corresponds to one on the board where one would
show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. *}
@@ -95,7 +95,7 @@
next
fix c1 c2 s1 s2 s3
assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)"
- thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp)
+ thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule seq_comp)
next
fix s::state and b c0 c1 t
assume "bval b s"
@@ -126,7 +126,7 @@
assume b: "bval b s"
have "(?w,s) \<rightarrow> (?if, s)" by blast
moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
- moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
+ moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule seq_comp[OF c w])
ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
qed
@@ -137,7 +137,7 @@
next
case Assign show ?case by blast
next
- case Semi thus ?case by (blast intro: semi_comp)
+ case Seq thus ?case by (blast intro: seq_comp)
next
case IfTrue thus ?case by (blast intro: star.step)
next
@@ -148,7 +148,7 @@
next
case WhileTrue
thus ?case
- by(metis While semi_comp small_step.IfTrue star.step[of small_step])
+ by(metis While seq_comp small_step.IfTrue star.step[of small_step])
qed
lemma small1_big_continue:
--- a/src/HOL/IMP/Types.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/Types.thy Sat Apr 28 07:38:22 2012 +0200
@@ -41,8 +41,8 @@
datatype
com = SKIP
- | Assign vname aexp ("_ ::= _" [1000, 61] 61)
- | Semi com com ("_; _" [60, 61] 60)
+ | Assign vname aexp ("_ ::= _" [1000, 61] 61)
+ | Seq com com ("_; _" [60, 61] 60)
| If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61)
| While bexp com ("WHILE _ DO _" [0, 61] 61)
@@ -54,8 +54,8 @@
where
Assign: "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
-Semi1: "(SKIP;c,s) \<rightarrow> (c,s)" |
-Semi2: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" |
+Seq1: "(SKIP;c,s) \<rightarrow> (c,s)" |
+Seq2: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" |
IfTrue: "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
@@ -93,7 +93,7 @@
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
Skip_ty: "\<Gamma> \<turnstile> SKIP" |
Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
-Semi_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
+Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
@@ -164,7 +164,7 @@
case Assign_ty
thus ?case by (metis Assign aprogress)
next
- case Semi_ty thus ?case by simp (metis Semi1 Semi2)
+ case Seq_ty thus ?case by simp (metis Seq1 Seq2)
next
case (If_ty \<Gamma> b c1 c2)
then obtain bv where "tbval b s bv" by (metis bprogress)
--- a/src/HOL/IMP/VC.thy Fri Apr 27 23:17:58 2012 +0200
+++ b/src/HOL/IMP/VC.thy Sat Apr 28 07:38:22 2012 +0200
@@ -10,7 +10,7 @@
datatype acom =
ASKIP |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) |
- Asemi acom acom ("_;/ _" [60, 61] 60) |
+ Aseq acom acom ("_;/ _" [60, 61] 60) |
Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
Awhile assn bexp acom ("({_}/ WHILE _/ DO _)" [0, 0, 61] 61)
@@ -19,7 +19,7 @@
fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
"pre ASKIP Q = Q" |
"pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
-"pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
+"pre (Aseq c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
"pre (Aif b c\<^isub>1 c\<^isub>2) Q =
(\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
(\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
@@ -30,7 +30,7 @@
fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
"vc ASKIP Q = (\<lambda>s. True)" |
"vc (Aassign x a) Q = (\<lambda>s. True)" |
-"vc (Asemi c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" |
+"vc (Aseq c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" |
"vc (Aif b c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" |
"vc (Awhile I b c) Q =
(\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
@@ -42,7 +42,7 @@
fun strip :: "acom \<Rightarrow> com" where
"strip ASKIP = SKIP" |
"strip (Aassign x a) = (x::=a)" |
-"strip (Asemi c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
+"strip (Aseq c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
"strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
"strip (Awhile I b c) = (WHILE b DO strip c)"
@@ -73,13 +73,13 @@
lemma pre_mono:
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
proof (induction c arbitrary: P P' s)
- case Asemi thus ?case by simp metis
+ case Aseq thus ?case by simp metis
qed simp_all
lemma vc_mono:
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
proof(induction c arbitrary: P P')
- case Asemi thus ?case by simp (metis pre_mono)
+ case Aseq thus ?case by simp (metis pre_mono)
qed simp_all
lemma vc_complete:
@@ -94,12 +94,12 @@
show ?case (is "\<exists>ac. ?C ac")
proof show "?C(Aassign x a)" by simp qed
next
- case (Semi P c1 Q c2 R)
- from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
- from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
+ case (Seq P c1 Q c2 R)
+ from Seq.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
+ from Seq.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
show ?case (is "\<exists>ac. ?C ac")
proof
- show "?C(Asemi ac1 ac2)"
+ show "?C(Aseq ac1 ac2)"
using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
qed
next
@@ -127,7 +127,7 @@
fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
"vcpre ASKIP Q = (\<lambda>s. True, Q)" |
"vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
-"vcpre (Asemi c\<^isub>1 c\<^isub>2) Q =
+"vcpre (Aseq c\<^isub>1 c\<^isub>2) Q =
(let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
(vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 wp\<^isub>2
in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" |