renamed Semi to Seq
authornipkow
Sat Apr 28 07:38:22 2012 +0200 (2012-04-28)
changeset 47818151d137f1095
parent 47817 5d2d63f4363e
child 47819 d402ac2288b8
renamed Semi to Seq
src/HOL/IMP/ACom.thy
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int2.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy
src/HOL/IMP/Big_Step.thy
src/HOL/IMP/C_like.thy
src/HOL/IMP/Collecting.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Comp_Rev.thy
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Def_Ass.thy
src/HOL/IMP/Def_Ass_Big.thy
src/HOL/IMP/Def_Ass_Small.thy
src/HOL/IMP/Def_Ass_Sound_Big.thy
src/HOL/IMP/Def_Ass_Sound_Small.thy
src/HOL/IMP/Fold.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/HoareT.thy
src/HOL/IMP/Hoare_Examples.thy
src/HOL/IMP/Hoare_Sound_Complete.thy
src/HOL/IMP/Live.thy
src/HOL/IMP/Live_True.thy
src/HOL/IMP/OO.thy
src/HOL/IMP/Procs.thy
src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
src/HOL/IMP/Procs_Stat_Vars_Stat.thy
src/HOL/IMP/Sec_Typing.thy
src/HOL/IMP/Sec_TypingT.thy
src/HOL/IMP/Sem_Equiv.thy
src/HOL/IMP/Small_Step.thy
src/HOL/IMP/Types.thy
src/HOL/IMP/VC.thy
     1.1 --- a/src/HOL/IMP/ACom.thy	Fri Apr 27 23:17:58 2012 +0200
     1.2 +++ b/src/HOL/IMP/ACom.thy	Sat Apr 28 07:38:22 2012 +0200
     1.3 @@ -10,12 +10,12 @@
     1.4  subsection "Annotated Commands"
     1.5  
     1.6  datatype 'a acom =
     1.7 -  SKIP   'a                           ("SKIP {_}" 61) |
     1.8 -  Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
     1.9 -  Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
    1.10 -  If     bexp "('a acom)" "('a acom)" 'a
    1.11 +  SKIP 'a                           ("SKIP {_}" 61) |
    1.12 +  Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
    1.13 +  Seq "('a acom)" "('a acom)"       ("_;//_"  [60, 61] 60) |
    1.14 +  If bexp "('a acom)" "('a acom)" 'a
    1.15      ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
    1.16 -  While  'a bexp "('a acom)" 'a
    1.17 +  While 'a bexp "('a acom)" 'a
    1.18      ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
    1.19  
    1.20  fun post :: "'a acom \<Rightarrow>'a" where
    1.21 @@ -72,7 +72,7 @@
    1.22   "map_acom f c = x ::= e {S'} \<longleftrightarrow> (\<exists>S. c = x::=e {S} \<and> S' = f S)"
    1.23  by (cases c) auto
    1.24  
    1.25 -lemma map_acom_Semi:
    1.26 +lemma map_acom_Seq:
    1.27   "map_acom f c = c1';c2' \<longleftrightarrow>
    1.28   (\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')"
    1.29  by (cases c) auto
    1.30 @@ -99,7 +99,7 @@
    1.31    "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})"
    1.32  by (cases c) simp_all
    1.33  
    1.34 -lemma strip_eq_Semi:
    1.35 +lemma strip_eq_Seq:
    1.36    "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
    1.37  by (cases c) simp_all
    1.38  
    1.39 @@ -119,7 +119,7 @@
    1.40  
    1.41  lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
    1.42  apply(induct C2 arbitrary: C1)
    1.43 -apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Semi strip_eq_If strip_eq_While)
    1.44 +apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Seq strip_eq_If strip_eq_While)
    1.45  done
    1.46  
    1.47  lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
     2.1 --- a/src/HOL/IMP/Abs_Int0.thy	Fri Apr 27 23:17:58 2012 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Sat Apr 28 07:38:22 2012 +0200
     2.3 @@ -332,7 +332,7 @@
     2.4      by (fastforce simp: Assign_le  map_acom_Assign intro: aval'_sound in_gamma_update
     2.5        split: option.splits del:subsetD)
     2.6  next
     2.7 -  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
     2.8 +  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     2.9      by (metis le_post post_map_acom)
    2.10  next
    2.11    case (If b C1 C2 P)
     3.1 --- a/src/HOL/IMP/Abs_Int1.thy	Fri Apr 27 23:17:58 2012 +0200
     3.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Sat Apr 28 07:38:22 2012 +0200
     3.3 @@ -96,7 +96,7 @@
     3.4      by(fastforce simp: Assign_le map_acom_Assign wt_st_def
     3.5          intro: aval'_sound in_gamma_update split: option.splits)
     3.6  next
     3.7 -  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
     3.8 +  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     3.9      by (metis le_post post_map_acom wt_post)
    3.10  next
    3.11    case (If b C1 C2 P)
     4.1 --- a/src/HOL/IMP/Abs_Int2.thy	Fri Apr 27 23:17:58 2012 +0200
     4.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Sat Apr 28 07:38:22 2012 +0200
     4.3 @@ -189,7 +189,7 @@
     4.4      by (fastforce simp: Assign_le map_acom_Assign wt_option_def wt_st_def
     4.5          intro: aval'_sound in_gamma_update  split: option.splits del:subsetD)
     4.6  next
     4.7 -  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
     4.8 +  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     4.9      by (metis le_post post_map_acom wt_post)
    4.10  next
    4.11    case (If b C1 C2 P)
     5.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy	Fri Apr 27 23:17:58 2012 +0200
     5.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy	Sat Apr 28 07:38:22 2012 +0200
     5.3 @@ -44,7 +44,7 @@
     5.4    case Assign thus ?case
     5.5      by (auto simp: lookup_update aval'_sound)
     5.6  next
     5.7 -  case Semi thus ?case by auto
     5.8 +  case Seq thus ?case by auto
     5.9  next
    5.10    case If thus ?case
    5.11      by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
     6.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Fri Apr 27 23:17:58 2012 +0200
     6.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy	Sat Apr 28 07:38:22 2012 +0200
     6.3 @@ -160,7 +160,7 @@
     6.4  next
     6.5    case Assign thus ?case by (auto simp: aval'_sound)
     6.6  next
     6.7 -  case Semi thus ?case by auto
     6.8 +  case Seq thus ?case by auto
     6.9  next
    6.10    case If thus ?case by(auto simp: in_rep_join)
    6.11  next
     7.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Fri Apr 27 23:17:58 2012 +0200
     7.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Sat Apr 28 07:38:22 2012 +0200
     7.3 @@ -187,7 +187,7 @@
     7.4    case Assign thus ?case
     7.5      by (auto simp: lookup_update aval'_sound)
     7.6  next
     7.7 -  case Semi thus ?case by fastforce
     7.8 +  case Seq thus ?case by fastforce
     7.9  next
    7.10    case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
    7.11  next
     8.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Fri Apr 27 23:17:58 2012 +0200
     8.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy	Sat Apr 28 07:38:22 2012 +0200
     8.3 @@ -324,7 +324,7 @@
     8.4      by (fastforce simp: Assign_le  map_acom_Assign intro: aval'_sound in_gamma_update
     8.5        split: option.splits del:subsetD)
     8.6  next
     8.7 -  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
     8.8 +  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     8.9      by (metis le_post post_map_acom)
    8.10  next
    8.11    case (If b c1 c2 P)
     9.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Fri Apr 27 23:17:58 2012 +0200
     9.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy	Sat Apr 28 07:38:22 2012 +0200
     9.3 @@ -66,7 +66,7 @@
     9.4      by (fastforce simp: Assign_le  map_acom_Assign intro: aval'_sound in_gamma_update
     9.5        split: option.splits del:subsetD)
     9.6  next
     9.7 -  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
     9.8 +  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
     9.9      by (metis le_post post_map_acom)
    9.10  next
    9.11    case (If b c1 c2 P)
    10.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Fri Apr 27 23:17:58 2012 +0200
    10.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Sat Apr 28 07:38:22 2012 +0200
    10.3 @@ -202,7 +202,7 @@
    10.4      by (fastforce simp: Assign_le  map_acom_Assign intro: aval'_sound in_gamma_update
    10.5        split: option.splits del:subsetD)
    10.6  next
    10.7 -  case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
    10.8 +  case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq)
    10.9      by (metis le_post post_map_acom)
   10.10  next
   10.11    case (If b cs1 cs2 P)
    11.1 --- a/src/HOL/IMP/Big_Step.thy	Fri Apr 27 23:17:58 2012 +0200
    11.2 +++ b/src/HOL/IMP/Big_Step.thy	Sat Apr 28 07:38:22 2012 +0200
    11.3 @@ -10,7 +10,7 @@
    11.4  where
    11.5  Skip:    "(SKIP,s) \<Rightarrow> s" |
    11.6  Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
    11.7 -Semi:    "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
    11.8 +Seq:     "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2;  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
    11.9            (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   11.10  
   11.11  IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
   11.12 @@ -25,7 +25,7 @@
   11.13  
   11.14  text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEx}{% *}
   11.15  schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
   11.16 -apply(rule Semi)
   11.17 +apply(rule Seq)
   11.18  apply(rule Assign)
   11.19  apply simp
   11.20  apply(rule Assign)
   11.21 @@ -89,8 +89,8 @@
   11.22  
   11.23  inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
   11.24  thm AssignE
   11.25 -inductive_cases SemiE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
   11.26 -thm SemiE
   11.27 +inductive_cases SeqE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
   11.28 +thm SeqE
   11.29  inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
   11.30  thm IfE
   11.31  
   11.32 @@ -162,7 +162,7 @@
   11.33          "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
   11.34        -- "now we can build a derivation tree for the @{text IF}"
   11.35        -- "first, the body of the True-branch:"
   11.36 -      hence "(c; ?w, s) \<Rightarrow> t" by (rule Semi)
   11.37 +      hence "(c; ?w, s) \<Rightarrow> t" by (rule Seq)
   11.38        -- "then the whole @{text IF}"
   11.39        with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue)
   11.40      }
   11.41 @@ -184,7 +184,7 @@
   11.42      -- {* then this time only the @{text IfTrue} rule can have be used *}
   11.43      { assume "bval b s"
   11.44        with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto
   11.45 -      -- "and for this, only the Semi-rule is applicable:"
   11.46 +      -- "and for this, only the Seq-rule is applicable:"
   11.47        then obtain s' where
   11.48          "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
   11.49        -- "with this information, we can build a derivation tree for the @{text WHILE}"
    12.1 --- a/src/HOL/IMP/C_like.thy	Fri Apr 27 23:17:58 2012 +0200
    12.2 +++ b/src/HOL/IMP/C_like.thy	Sat Apr 28 07:38:22 2012 +0200
    12.3 @@ -24,7 +24,7 @@
    12.4    com = SKIP 
    12.5        | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
    12.6        | New    aexp aexp
    12.7 -      | Semi   com  com          ("_;/ _"  [60, 61] 60)
    12.8 +      | Seq    com  com          ("_;/ _"  [60, 61] 60)
    12.9        | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
   12.10        | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
   12.11  
   12.12 @@ -34,7 +34,7 @@
   12.13  Skip:    "(SKIP,sn) \<Rightarrow> sn" |
   12.14  Assign:  "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" |
   12.15  New:     "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)"  |
   12.16 -Semi:    "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2;  (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
   12.17 +Seq:    "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2;  (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
   12.18            (c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3" |
   12.19  
   12.20  IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
    13.1 --- a/src/HOL/IMP/Collecting.thy	Fri Apr 27 23:17:58 2012 +0200
    13.2 +++ b/src/HOL/IMP/Collecting.thy	Sat Apr 28 07:38:22 2012 +0200
    13.3 @@ -30,7 +30,7 @@
    13.4  lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
    13.5  by (cases c) auto
    13.6  
    13.7 -lemma Semi_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
    13.8 +lemma Seq_le: "c1;c2 \<le> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<le> c1' \<and> c2 \<le> c2')"
    13.9  by (cases c) auto
   13.10  
   13.11  lemma If_le: "IF b THEN c1 ELSE c2 {S} \<le> c \<longleftrightarrow>
   13.12 @@ -52,7 +52,7 @@
   13.13  next
   13.14    case goal3 thus ?case
   13.15    apply(induct x y arbitrary: z rule: less_eq_acom.induct)
   13.16 -  apply (auto intro: le_trans simp: SKIP_le Assign_le Semi_le If_le While_le)
   13.17 +  apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le)
   13.18    done
   13.19  next
   13.20    case goal4 thus ?case
   13.21 @@ -94,7 +94,7 @@
   13.22    case goal1
   13.23    have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
   13.24    proof(induction a arbitrary: A)
   13.25 -    case Semi from Semi.prems show ?case by(force intro!: Semi.IH)
   13.26 +    case Seq from Seq.prems show ?case by(force intro!: Seq.IH)
   13.27    next
   13.28      case If from If.prems show ?case by(force intro!: If.IH)
   13.29    next
   13.30 @@ -109,8 +109,8 @@
   13.31    next
   13.32      case Assign thus ?case by (force simp:Assign_le)
   13.33    next
   13.34 -    case Semi from Semi.prems show ?case
   13.35 -      by (force intro!: Semi.IH simp:Semi_le)
   13.36 +    case Seq from Seq.prems show ?case
   13.37 +      by (force intro!: Seq.IH simp:Seq_le)
   13.38    next
   13.39      case If from If.prems show ?case by (force simp: If_le intro!: If.IH)
   13.40    next
   13.41 @@ -121,8 +121,8 @@
   13.42    case goal3
   13.43    have "strip(lift Inter i A) = i"
   13.44    proof(induction i arbitrary: A)
   13.45 -    case Semi from Semi.prems show ?case
   13.46 -      by (fastforce simp: strip_eq_Semi subset_iff intro!: Semi.IH)
   13.47 +    case Seq from Seq.prems show ?case
   13.48 +      by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH)
   13.49    next
   13.50      case If from If.prems show ?case
   13.51        by (fastforce intro!: If.IH simp: strip_eq_If)
    14.1 --- a/src/HOL/IMP/Com.thy	Fri Apr 27 23:17:58 2012 +0200
    14.2 +++ b/src/HOL/IMP/Com.thy	Sat Apr 28 07:38:22 2012 +0200
    14.3 @@ -5,7 +5,7 @@
    14.4  datatype
    14.5    com = SKIP 
    14.6        | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
    14.7 -      | Semi   com  com         ("_;/ _"  [60, 61] 60)
    14.8 +      | Seq    com  com         ("_;/ _"  [60, 61] 60)
    14.9        | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
   14.10        | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
   14.11  
    15.1 --- a/src/HOL/IMP/Comp_Rev.thy	Fri Apr 27 23:17:58 2012 +0200
    15.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Sat Apr 28 07:38:22 2012 +0200
    15.3 @@ -224,10 +224,10 @@
    15.4  next
    15.5    case Assign thus ?case by simp
    15.6  next
    15.7 -  case (Semi c1 c2)
    15.8 -  from Semi.prems
    15.9 +  case (Seq c1 c2)
   15.10 +  from Seq.prems
   15.11    show ?case 
   15.12 -    by (fastforce dest: Semi.IH [THEN subsetD])
   15.13 +    by (fastforce dest: Seq.IH [THEN subsetD])
   15.14  next
   15.15    case (If b c1 c2)
   15.16    from If.prems
   15.17 @@ -492,7 +492,7 @@
   15.18    thus ?case
   15.19      by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
   15.20  next
   15.21 -  case (Semi c1 c2)
   15.22 +  case (Seq c1 c2)
   15.23    thus ?case by (fastforce dest!: exec_n_split_full)
   15.24  next
   15.25    case (If b c1 c2)
    16.1 --- a/src/HOL/IMP/Compiler.thy	Fri Apr 27 23:17:58 2012 +0200
    16.2 +++ b/src/HOL/IMP/Compiler.thy	Sat Apr 28 07:38:22 2012 +0200
    16.3 @@ -259,13 +259,13 @@
    16.4    case (Assign x a s)
    16.5    show ?case by (fastforce simp:fun_upd_def cong: if_cong)
    16.6  next
    16.7 -  case (Semi c1 s1 s2 c2 s3)
    16.8 +  case (Seq c1 s1 s2 c2 s3)
    16.9    let ?cc1 = "ccomp c1"  let ?cc2 = "ccomp c2"
   16.10    have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
   16.11 -    using Semi.IH(1) by fastforce
   16.12 +    using Seq.IH(1) by fastforce
   16.13    moreover
   16.14    have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
   16.15 -    using Semi.IH(2) by fastforce
   16.16 +    using Seq.IH(2) by fastforce
   16.17    ultimately show ?case by simp (blast intro: exec_trans)
   16.18  next
   16.19    case (WhileTrue b s1 c s2 s3)
    17.1 --- a/src/HOL/IMP/Def_Ass.thy	Fri Apr 27 23:17:58 2012 +0200
    17.2 +++ b/src/HOL/IMP/Def_Ass.thy	Sat Apr 28 07:38:22 2012 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  inductive D :: "vname set \<Rightarrow> com \<Rightarrow> vname set \<Rightarrow> bool" where
    17.5  Skip: "D A SKIP A" |
    17.6  Assign: "vars a \<subseteq> A \<Longrightarrow> D A (x ::= a) (insert x A)" |
    17.7 -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" |
    17.8 +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" |
    17.9  If: "\<lbrakk> vars b \<subseteq> A;  D A c\<^isub>1 A\<^isub>1;  D A c\<^isub>2 A\<^isub>2 \<rbrakk> \<Longrightarrow>
   17.10    D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" |
   17.11  While: "\<lbrakk> vars b \<subseteq> A;  D A c A' \<rbrakk> \<Longrightarrow> D A (WHILE b DO c) A"
    18.1 --- a/src/HOL/IMP/Def_Ass_Big.thy	Fri Apr 27 23:17:58 2012 +0200
    18.2 +++ b/src/HOL/IMP/Def_Ass_Big.thy	Sat Apr 28 07:38:22 2012 +0200
    18.3 @@ -12,7 +12,7 @@
    18.4  Skip: "(SKIP,s) \<Rightarrow> s" |
    18.5  AssignNone: "aval a s = None \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> None" |
    18.6  Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, Some s) \<Rightarrow> Some(s(x := Some i))" |
    18.7 -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" |
    18.8 +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" |
    18.9  
   18.10  IfNone:  "bval b s = None \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \<Rightarrow> None" |
   18.11  IfTrue:  "\<lbrakk> bval b s = Some True;  (c\<^isub>1,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow>
    19.1 --- a/src/HOL/IMP/Def_Ass_Small.thy	Fri Apr 27 23:17:58 2012 +0200
    19.2 +++ b/src/HOL/IMP/Def_Ass_Small.thy	Sat Apr 28 07:38:22 2012 +0200
    19.3 @@ -10,8 +10,8 @@
    19.4  where
    19.5  Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
    19.6  
    19.7 -Semi1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
    19.8 -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')" |
    19.9 +Seq1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
   19.10 +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')" |
   19.11  
   19.12  IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
   19.13  IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
    20.1 --- a/src/HOL/IMP/Def_Ass_Sound_Big.thy	Fri Apr 27 23:17:58 2012 +0200
    20.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy	Sat Apr 28 07:38:22 2012 +0200
    20.3 @@ -16,7 +16,7 @@
    20.4    case AssignNone thus ?case
    20.5      by auto (metis aval_Some option.simps(3) subset_trans)
    20.6  next
    20.7 -  case Semi thus ?case by auto metis
    20.8 +  case Seq thus ?case by auto metis
    20.9  next
   20.10    case IfTrue thus ?case by auto blast
   20.11  next
    21.1 --- a/src/HOL/IMP/Def_Ass_Sound_Small.thy	Fri Apr 27 23:17:58 2012 +0200
    21.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy	Sat Apr 28 07:38:22 2012 +0200
    21.3 @@ -18,7 +18,7 @@
    21.4  
    21.5  lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
    21.6  proof (induction c arbitrary: A A' M)
    21.7 -  case Semi thus ?case by auto (metis D.intros(3))
    21.8 +  case Seq thus ?case by auto (metis D.intros(3))
    21.9  next
   21.10    case (If b c1 c2)
   21.11    then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
   21.12 @@ -40,10 +40,10 @@
   21.13    moreover
   21.14    then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
   21.15    ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"
   21.16 -    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)
   21.17 +    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)
   21.18    thus ?case by (metis D_incr `A = dom s`)
   21.19  next
   21.20 -  case Semi2 thus ?case by auto (metis D_mono D.intros(3))
   21.21 +  case Seq2 thus ?case by auto (metis D_mono D.intros(3))
   21.22  qed (auto intro: D.intros)
   21.23  
   21.24  theorem D_sound:
    22.1 --- a/src/HOL/IMP/Fold.thy	Fri Apr 27 23:17:58 2012 +0200
    22.2 +++ b/src/HOL/IMP/Fold.thy	Sat Apr 28 07:38:22 2012 +0200
    22.3 @@ -82,13 +82,13 @@
    22.4  lemma defs_restrict:
    22.5    "defs c t |` (- lnames c) = t |` (- lnames c)"
    22.6  proof (induction c arbitrary: t)
    22.7 -  case (Semi c1 c2)
    22.8 +  case (Seq c1 c2)
    22.9    hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
   22.10      by simp
   22.11    hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
   22.12           t |` (- lnames c1) |` (-lnames c2)" by simp
   22.13    moreover
   22.14 -  from Semi
   22.15 +  from Seq
   22.16    have "defs c2 (defs c1 t) |` (- lnames c2) = 
   22.17          defs c1 t |` (- lnames c2)"
   22.18      by simp
   22.19 @@ -121,9 +121,9 @@
   22.20    thus ?case
   22.21      by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
   22.22  next
   22.23 -  case (Semi c1 s1 s2 c2 s3)
   22.24 -  have "approx (defs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
   22.25 -  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi.IH(2))
   22.26 +  case (Seq c1 s1 s2 c2 s3)
   22.27 +  have "approx (defs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems])
   22.28 +  hence "approx (defs c2 (defs c1 t)) s3" by (rule Seq.IH(2))
   22.29    thus ?case by simp
   22.30  next
   22.31    case (IfTrue b s c1 s')
   22.32 @@ -155,15 +155,15 @@
   22.33    case Assign
   22.34    thus ?case by (clarsimp simp: approx_def)
   22.35  next
   22.36 -  case (Semi c1 s1 s2 c2 s3)
   22.37 +  case (Seq c1 s1 s2 c2 s3)
   22.38    hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" 
   22.39      by (simp add: Int_commute)
   22.40    hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
   22.41 -    by (rule Semi)
   22.42 +    by (rule Seq)
   22.43    hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
   22.44      by (simp add: Int_commute)
   22.45    hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
   22.46 -    by (rule Semi)
   22.47 +    by (rule Seq)
   22.48    thus ?case by simp
   22.49  next
   22.50    case (IfTrue b s c1 s' c2)
   22.51 @@ -196,8 +196,8 @@
   22.52    case Assign
   22.53    show ?case by (simp add: equiv_up_to_def)
   22.54  next
   22.55 -  case Semi 
   22.56 -  thus ?case by (auto intro!: equiv_up_to_semi)
   22.57 +  case Seq 
   22.58 +  thus ?case by (auto intro!: equiv_up_to_seq)
   22.59  next
   22.60    case If
   22.61    thus ?case by (auto intro!: equiv_up_to_if_weak)
   22.62 @@ -293,13 +293,13 @@
   22.63  lemma bdefs_restrict:
   22.64    "bdefs c t |` (- lnames c) = t |` (- lnames c)"
   22.65  proof (induction c arbitrary: t)
   22.66 -  case (Semi c1 c2)
   22.67 +  case (Seq c1 c2)
   22.68    hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
   22.69      by simp
   22.70    hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
   22.71           t |` (- lnames c1) |` (-lnames c2)" by simp
   22.72    moreover
   22.73 -  from Semi
   22.74 +  from Seq
   22.75    have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = 
   22.76          bdefs c1 t |` (- lnames c2)"
   22.77      by simp
   22.78 @@ -334,9 +334,9 @@
   22.79    thus ?case
   22.80      by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
   22.81  next
   22.82 -  case (Semi c1 s1 s2 c2 s3)
   22.83 -  have "approx (bdefs c1 t) s2" by (rule Semi.IH(1)[OF Semi.prems])
   22.84 -  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi.IH(2))
   22.85 +  case (Seq c1 s1 s2 c2 s3)
   22.86 +  have "approx (bdefs c1 t) s2" by (rule Seq.IH(1)[OF Seq.prems])
   22.87 +  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Seq.IH(2))
   22.88    thus ?case by simp
   22.89  next
   22.90    case (IfTrue b s c1 s')
   22.91 @@ -377,8 +377,8 @@
   22.92    case Assign
   22.93    thus ?case by (simp add: equiv_up_to_def)
   22.94  next
   22.95 -  case Semi
   22.96 -  thus ?case by (auto intro!: equiv_up_to_semi)           
   22.97 +  case Seq
   22.98 +  thus ?case by (auto intro!: equiv_up_to_seq)           
   22.99  next
  22.100    case (If b c1 c2)
  22.101    hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> 
    23.1 --- a/src/HOL/IMP/Hoare.thy	Fri Apr 27 23:17:58 2012 +0200
    23.2 +++ b/src/HOL/IMP/Hoare.thy	Sat Apr 28 07:38:22 2012 +0200
    23.3 @@ -19,8 +19,8 @@
    23.4  
    23.5  Assign:  "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}"  |
    23.6  
    23.7 -Semi: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q};  \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
    23.8 -       \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}"  |
    23.9 +Seq: "\<lbrakk> \<turnstile> {P} c\<^isub>1 {Q};  \<turnstile> {Q} c\<^isub>2 {R} \<rbrakk>
   23.10 +      \<Longrightarrow> \<turnstile> {P} c\<^isub>1;c\<^isub>2 {R}"  |
   23.11  
   23.12  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>
   23.13       \<Longrightarrow> \<turnstile> {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  |
   23.14 @@ -31,9 +31,9 @@
   23.15  conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q};  \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
   23.16          \<Longrightarrow> \<turnstile> {P'} c {Q'}"
   23.17  
   23.18 -lemmas [simp] = hoare.Skip hoare.Assign hoare.Semi If
   23.19 +lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If
   23.20  
   23.21 -lemmas [intro!] = hoare.Skip hoare.Assign hoare.Semi hoare.If
   23.22 +lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If
   23.23  
   23.24  lemma strengthen_pre:
   23.25    "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s;  \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
    24.1 --- a/src/HOL/IMP/HoareT.thy	Fri Apr 27 23:17:58 2012 +0200
    24.2 +++ b/src/HOL/IMP/HoareT.thy	Sat Apr 28 07:38:22 2012 +0200
    24.3 @@ -20,7 +20,7 @@
    24.4  where
    24.5  Skip:  "\<turnstile>\<^sub>t {P} SKIP {P}" |
    24.6  Assign:  "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" |
    24.7 -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}" |
    24.8 +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}" |
    24.9  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>
   24.10    \<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" |
   24.11  While:
   24.12 @@ -57,19 +57,19 @@
   24.13    DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
   24.14  
   24.15  lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}"
   24.16 -apply(rule Semi)
   24.17 +apply(rule Seq)
   24.18  prefer 2
   24.19  apply(rule While'
   24.20    [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"
   24.21     and f = "\<lambda>s. nat (n - s ''y'')"])
   24.22 -apply(rule Semi)
   24.23 +apply(rule Seq)
   24.24  prefer 2
   24.25  apply(rule Assign)
   24.26  apply(rule Assign')
   24.27  apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
   24.28  apply clarsimp
   24.29  apply fastforce
   24.30 -apply(rule Semi)
   24.31 +apply(rule Seq)
   24.32  prefer 2
   24.33  apply(rule Assign)
   24.34  apply(rule Assign')
   24.35 @@ -182,7 +182,7 @@
   24.36  next
   24.37    case Assign show ?case by simp (blast intro:hoaret.Assign)
   24.38  next
   24.39 -  case Semi thus ?case by simp (blast intro:hoaret.Semi)
   24.40 +  case Seq thus ?case by simp (blast intro:hoaret.Seq)
   24.41  next
   24.42    case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)
   24.43  next
    25.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Fri Apr 27 23:17:58 2012 +0200
    25.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Sat Apr 28 07:38:22 2012 +0200
    25.3 @@ -51,17 +51,17 @@
    25.4  pulling back the postcondition towards the precondition. *}
    25.5  
    25.6  lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
    25.7 -apply(rule hoare.Semi)
    25.8 +apply(rule hoare.Seq)
    25.9  prefer 2
   25.10  apply(rule While'
   25.11    [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"])
   25.12 -apply(rule Semi)
   25.13 +apply(rule Seq)
   25.14  prefer 2
   25.15  apply(rule Assign)
   25.16  apply(rule Assign')
   25.17  apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps)
   25.18  apply(fastforce)
   25.19 -apply(rule Semi)
   25.20 +apply(rule Seq)
   25.21  prefer 2
   25.22  apply(rule Assign)
   25.23  apply(rule Assign')
    26.1 --- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Fri Apr 27 23:17:58 2012 +0200
    26.2 +++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Sat Apr 28 07:38:22 2012 +0200
    26.3 @@ -35,7 +35,7 @@
    26.4  lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
    26.5  by (rule ext) (auto simp: wp_def)
    26.6  
    26.7 -lemma wp_Semi[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
    26.8 +lemma wp_Seq[simp]: "wp (c\<^isub>1;c\<^isub>2) Q = wp c\<^isub>1 (wp c\<^isub>2 Q)"
    26.9  by (rule ext) (auto simp: wp_def)
   26.10  
   26.11  lemma wp_If[simp]:
   26.12 @@ -60,7 +60,7 @@
   26.13  
   26.14  lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
   26.15  proof(induction c arbitrary: Q)
   26.16 -  case Semi thus ?case by(auto intro: Semi)
   26.17 +  case Seq thus ?case by(auto intro: Seq)
   26.18  next
   26.19    case (If b c1 c2)
   26.20    let ?If = "IF b THEN c1 ELSE c2"
    27.1 --- a/src/HOL/IMP/Live.thy	Fri Apr 27 23:17:58 2012 +0200
    27.2 +++ b/src/HOL/IMP/Live.thy	Sat Apr 28 07:38:22 2012 +0200
    27.3 @@ -54,11 +54,11 @@
    27.4    case Assign then show ?case
    27.5      by (auto simp: ball_Un)
    27.6  next
    27.7 -  case (Semi c1 s1 s2 c2 s3 X t1)
    27.8 -  from Semi.IH(1) Semi.prems obtain t2 where
    27.9 +  case (Seq c1 s1 s2 c2 s3 X t1)
   27.10 +  from Seq.IH(1) Seq.prems obtain t2 where
   27.11      t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
   27.12      by simp blast
   27.13 -  from Semi.IH(2)[OF s2t2] obtain t3 where
   27.14 +  from Seq.IH(2)[OF s2t2] obtain t3 where
   27.15      t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   27.16      by auto
   27.17    show ?case using t12 t23 s3t3 by auto
   27.18 @@ -118,11 +118,11 @@
   27.19    case Assign then show ?case
   27.20      by (auto simp: ball_Un)
   27.21  next
   27.22 -  case (Semi c1 s1 s2 c2 s3 X t1)
   27.23 -  from Semi.IH(1) Semi.prems obtain t2 where
   27.24 +  case (Seq c1 s1 s2 c2 s3 X t1)
   27.25 +  from Seq.IH(1) Seq.prems obtain t2 where
   27.26      t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
   27.27      by simp blast
   27.28 -  from Semi.IH(2)[OF s2t2] obtain t3 where
   27.29 +  from Seq.IH(2)[OF s2t2] obtain t3 where
   27.30      t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   27.31      by auto
   27.32    show ?case using t12 t23 s3t3 by auto
   27.33 @@ -172,7 +172,7 @@
   27.34  lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
   27.35  by (cases c) auto
   27.36  
   27.37 -lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
   27.38 +lemma Seq_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
   27.39    (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))"
   27.40  by (cases c) auto
   27.41  
   27.42 @@ -194,11 +194,11 @@
   27.43    case Assign then show ?case
   27.44      by (auto simp: ball_Un)
   27.45  next
   27.46 -  case (Semi bc1 s1 s2 bc2 s3 c X t1)
   27.47 +  case (Seq bc1 s1 s2 bc2 s3 c X t1)
   27.48    then obtain c1 c2 where c: "c = c1;c2"
   27.49      and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
   27.50 -  note IH = Semi.hyps(2,4)
   27.51 -  from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
   27.52 +  note IH = Seq.hyps(2,4)
   27.53 +  from IH(1)[OF bc1, of t1] Seq.prems c obtain t2 where
   27.54      t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
   27.55    from IH(2)[OF bc2 s2t2] obtain t3 where
   27.56      t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
    28.1 --- a/src/HOL/IMP/Live_True.thy	Fri Apr 27 23:17:58 2012 +0200
    28.2 +++ b/src/HOL/IMP/Live_True.thy	Sat Apr 28 07:38:22 2012 +0200
    28.3 @@ -49,11 +49,11 @@
    28.4    case Assign then show ?case
    28.5      by (auto simp: ball_Un)
    28.6  next
    28.7 -  case (Semi c1 s1 s2 c2 s3 X t1)
    28.8 -  from Semi.IH(1) Semi.prems obtain t2 where
    28.9 +  case (Seq c1 s1 s2 c2 s3 X t1)
   28.10 +  from Seq.IH(1) Seq.prems obtain t2 where
   28.11      t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
   28.12      by simp blast
   28.13 -  from Semi.IH(2)[OF s2t2] obtain t3 where
   28.14 +  from Seq.IH(2)[OF s2t2] obtain t3 where
   28.15      t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
   28.16      by auto
   28.17    show ?case using t12 t23 s3t3 by auto
    29.1 --- a/src/HOL/IMP/OO.thy	Fri Apr 27 23:17:58 2012 +0200
    29.2 +++ b/src/HOL/IMP/OO.thy	Sat Apr 28 07:38:22 2012 +0200
    29.3 @@ -22,7 +22,7 @@
    29.4    Vassign string exp       ("(_ ::=/ _)" [1000,61] 62) |
    29.5    Fassign exp string exp   ("(_\<bullet>_ ::=/ _)" [63,0,62] 62) |
    29.6    Mcall exp string exp     ("(_\<bullet>/_<_>)" [63,0,0] 63) |
    29.7 -  Semi exp exp             ("_;/ _" [61,60] 60) |
    29.8 +  Seq exp exp              ("_;/ _" [61,60] 60) |
    29.9    If bexp exp exp          ("IF _/ THEN (2_)/ ELSE (2_)" [0,0,61] 61)
   29.10  and bexp = B bool | Not bexp | And bexp bexp | Eq exp exp
   29.11  
   29.12 @@ -56,7 +56,7 @@
   29.13     me \<turnstile> (me m,ve,sn\<^isub>3) \<Rightarrow> (r,ve',sn\<^isub>4) \<rbrakk>
   29.14    \<Longrightarrow>
   29.15   me \<turnstile> (oe\<bullet>m<pe>,c\<^isub>1) \<Rightarrow> (r,ve\<^isub>3,sn\<^isub>4)" |
   29.16 -Semi:
   29.17 +Seq:
   29.18  "\<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>
   29.19   me \<turnstile> (e\<^isub>1; e\<^isub>2,c\<^isub>1) \<Rightarrow> c\<^isub>3" |
   29.20  IfTrue:
    30.1 --- a/src/HOL/IMP/Procs.thy	Fri Apr 27 23:17:58 2012 +0200
    30.2 +++ b/src/HOL/IMP/Procs.thy	Sat Apr 28 07:38:22 2012 +0200
    30.3 @@ -9,7 +9,7 @@
    30.4  datatype
    30.5    com = SKIP 
    30.6        | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
    30.7 -      | Semi   com  com          ("_;/ _"  [60, 61] 60)
    30.8 +      | Seq    com  com          ("_;/ _"  [60, 61] 60)
    30.9        | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
   30.10        | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
   30.11        | Var    vname com        ("(1{VAR _;;/ _})")
    31.1 --- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Fri Apr 27 23:17:58 2012 +0200
    31.2 +++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Sat Apr 28 07:38:22 2012 +0200
    31.3 @@ -10,7 +10,7 @@
    31.4  where
    31.5  Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
    31.6  Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
    31.7 -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>
    31.8 +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>
    31.9            pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   31.10  
   31.11  IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
    32.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Fri Apr 27 23:17:58 2012 +0200
    32.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Sat Apr 28 07:38:22 2012 +0200
    32.3 @@ -10,7 +10,7 @@
    32.4  where
    32.5  Skip:    "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
    32.6  Assign:  "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
    32.7 -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>
    32.8 +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>
    32.9            pe \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   32.10  
   32.11  IfTrue:  "\<lbrakk> bval b s;  pe \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
    33.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Fri Apr 27 23:17:58 2012 +0200
    33.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Sat Apr 28 07:38:22 2012 +0200
    33.3 @@ -17,7 +17,7 @@
    33.4  where
    33.5  Skip:    "e \<turnstile> (SKIP,s) \<Rightarrow> s" |
    33.6  Assign:  "(pe,ve,f) \<turnstile> (x ::= a,s) \<Rightarrow> s(ve x := aval a (s o ve))" |
    33.7 -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>
    33.8 +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>
    33.9            e \<turnstile> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
   33.10  
   33.11  IfTrue:  "\<lbrakk> bval b (s \<circ> venv e);  e \<turnstile> (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
    34.1 --- a/src/HOL/IMP/Sec_Typing.thy	Fri Apr 27 23:17:58 2012 +0200
    34.2 +++ b/src/HOL/IMP/Sec_Typing.thy	Sat Apr 28 07:38:22 2012 +0200
    34.3 @@ -10,7 +10,7 @@
    34.4    "l \<turnstile> SKIP" |
    34.5  Assign:
    34.6    "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
    34.7 -Semi:
    34.8 +Seq:
    34.9    "\<lbrakk> l \<turnstile> c\<^isub>1;  l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
   34.10  If:
   34.11    "\<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" |
   34.12 @@ -44,7 +44,7 @@
   34.13  next
   34.14    case Assign thus ?case by auto
   34.15  next
   34.16 -  case Semi thus ?case by auto
   34.17 +  case Seq thus ?case by auto
   34.18  next
   34.19    case (IfTrue b s c1)
   34.20    hence "max (sec_bexp b) l \<turnstile> c1" by auto
   34.21 @@ -85,7 +85,7 @@
   34.22      thus "s y = t y" using `s = t (\<le> l)` by simp
   34.23    qed
   34.24  next
   34.25 -  case Semi thus ?case by blast
   34.26 +  case Seq thus ?case by blast
   34.27  next
   34.28    case (IfTrue b s c1 s' c2)
   34.29    have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems(2) by auto
   34.30 @@ -186,7 +186,7 @@
   34.31    "l \<turnstile>' SKIP" |
   34.32  Assign':
   34.33    "\<lbrakk> sec x \<ge> sec_aexp a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
   34.34 -Semi':
   34.35 +Seq':
   34.36    "\<lbrakk> l \<turnstile>' c\<^isub>1;  l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
   34.37  If':
   34.38    "\<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" |
   34.39 @@ -199,7 +199,7 @@
   34.40  apply(induction rule: sec_type.induct)
   34.41  apply (metis Skip')
   34.42  apply (metis Assign')
   34.43 -apply (metis Semi')
   34.44 +apply (metis Seq')
   34.45  apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
   34.46  by (metis less_or_eq_imp_le min_max.sup_absorb1 min_max.sup_absorb2 nat_le_linear While' anti_mono')
   34.47  
   34.48 @@ -208,7 +208,7 @@
   34.49  apply(induction rule: sec_type'.induct)
   34.50  apply (metis Skip)
   34.51  apply (metis Assign)
   34.52 -apply (metis Semi)
   34.53 +apply (metis Seq)
   34.54  apply (metis min_max.sup_absorb2 If)
   34.55  apply (metis min_max.sup_absorb2 While)
   34.56  by (metis anti_mono)
   34.57 @@ -220,7 +220,7 @@
   34.58    "\<turnstile> SKIP : l" |
   34.59  Assign2:
   34.60    "sec x \<ge> sec_aexp a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
   34.61 -Semi2:
   34.62 +Seq2:
   34.63    "\<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 " |
   34.64  If2:
   34.65    "\<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>
   34.66 @@ -233,7 +233,7 @@
   34.67  apply(induction rule: sec_type2.induct)
   34.68  apply (metis Skip')
   34.69  apply (metis Assign' eq_imp_le)
   34.70 -apply (metis Semi' anti_mono' min_max.inf.commute min_max.inf_le2)
   34.71 +apply (metis Seq' anti_mono' min_max.inf.commute min_max.inf_le2)
   34.72  apply (metis If' anti_mono' min_max.inf_absorb2 min_max.le_iff_inf nat_le_linear)
   34.73  by (metis While')
   34.74  
   34.75 @@ -241,7 +241,7 @@
   34.76  apply(induction rule: sec_type'.induct)
   34.77  apply (metis Skip2 le_refl)
   34.78  apply (metis Assign2)
   34.79 -apply (metis Semi2 min_max.inf_greatest)
   34.80 +apply (metis Seq2 min_max.inf_greatest)
   34.81  apply (metis If2 inf_greatest inf_nat_def le_trans)
   34.82  apply (metis While2 le_trans)
   34.83  by (metis le_trans)
    35.1 --- a/src/HOL/IMP/Sec_TypingT.thy	Fri Apr 27 23:17:58 2012 +0200
    35.2 +++ b/src/HOL/IMP/Sec_TypingT.thy	Sat Apr 28 07:38:22 2012 +0200
    35.3 @@ -8,7 +8,7 @@
    35.4    "l \<turnstile> SKIP"  |
    35.5  Assign:
    35.6    "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a"  |
    35.7 -Semi:
    35.8 +Seq:
    35.9    "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2"  |
   35.10  If:
   35.11    "\<lbrakk> max (sec_bexp b) l \<turnstile> c\<^isub>1;  max (sec_bexp b) l \<turnstile> c\<^isub>2 \<rbrakk>
   35.12 @@ -37,7 +37,7 @@
   35.13  next
   35.14    case Assign thus ?case by auto
   35.15  next
   35.16 -  case Semi thus ?case by auto
   35.17 +  case Seq thus ?case by auto
   35.18  next
   35.19    case (IfTrue b s c1)
   35.20    hence "max (sec_bexp b) l \<turnstile> c1" by auto
   35.21 @@ -60,7 +60,7 @@
   35.22  apply(induction arbitrary: s rule: sec_type.induct)
   35.23  apply (metis big_step.Skip)
   35.24  apply (metis big_step.Assign)
   35.25 -apply (metis big_step.Semi)
   35.26 +apply (metis big_step.Seq)
   35.27  apply (metis IfFalse IfTrue le0 le_antisym le_maxI2)
   35.28  apply simp
   35.29  done
   35.30 @@ -86,7 +86,7 @@
   35.31    qed
   35.32    ultimately show ?case by blast
   35.33  next
   35.34 -  case Semi thus ?case by blast
   35.35 +  case Seq thus ?case by blast
   35.36  next
   35.37    case (IfTrue b s c1 s' c2)
   35.38    have "sec_bexp b \<turnstile> c1" "sec_bexp b \<turnstile> c2" using IfTrue.prems by auto
   35.39 @@ -175,7 +175,7 @@
   35.40    "l \<turnstile>' SKIP"  |
   35.41  Assign':
   35.42    "\<lbrakk> sec x \<ge> sec_aexp a;  sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a"  |
   35.43 -Semi':
   35.44 +Seq':
   35.45    "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2"  |
   35.46  If':
   35.47    "\<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"  |
   35.48 @@ -188,7 +188,7 @@
   35.49  apply(induction rule: sec_type.induct)
   35.50  apply (metis Skip')
   35.51  apply (metis Assign')
   35.52 -apply (metis Semi')
   35.53 +apply (metis Seq')
   35.54  apply (metis min_max.inf_sup_ord(3) min_max.sup_absorb2 nat_le_linear If' anti_mono')
   35.55  by (metis While')
   35.56  
   35.57 @@ -197,7 +197,7 @@
   35.58  apply(induction rule: sec_type'.induct)
   35.59  apply (metis Skip)
   35.60  apply (metis Assign)
   35.61 -apply (metis Semi)
   35.62 +apply (metis Seq)
   35.63  apply (metis min_max.sup_absorb2 If)
   35.64  apply (metis While)
   35.65  by (metis anti_mono)
    36.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Fri Apr 27 23:17:58 2012 +0200
    36.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Sat Apr 28 07:38:22 2012 +0200
    36.3 @@ -70,7 +70,7 @@
    36.4    by (rule equiv_up_to_hoare)
    36.5  
    36.6  
    36.7 -lemma equiv_up_to_semi:
    36.8 +lemma equiv_up_to_seq:
    36.9    "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
   36.10    P \<Turnstile> (c; d) \<sim> (c'; d')"
   36.11    by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
    37.1 --- a/src/HOL/IMP/Small_Step.thy	Fri Apr 27 23:17:58 2012 +0200
    37.2 +++ b/src/HOL/IMP/Small_Step.thy	Sat Apr 28 07:38:22 2012 +0200
    37.3 @@ -10,8 +10,8 @@
    37.4  where
    37.5  Assign:  "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" |
    37.6  
    37.7 -Semi1:   "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
    37.8 -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')" |
    37.9 +Seq1:    "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
   37.10 +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')" |
   37.11  
   37.12  IfTrue:  "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
   37.13  IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
   37.14 @@ -54,8 +54,8 @@
   37.15  thm SkipE
   37.16  inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
   37.17  thm AssignE
   37.18 -inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct"
   37.19 -thm SemiE
   37.20 +inductive_cases SeqE[elim]: "(c1;c2,s) \<rightarrow> ct"
   37.21 +thm SeqE
   37.22  inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct"
   37.23  inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct"
   37.24  
   37.25 @@ -70,18 +70,18 @@
   37.26  
   37.27  subsection "Equivalence with big-step semantics"
   37.28  
   37.29 -lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
   37.30 +lemma star_seq2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')"
   37.31  proof(induction rule: star_induct)
   37.32    case refl thus ?case by simp
   37.33  next
   37.34    case step
   37.35 -  thus ?case by (metis Semi2 star.step)
   37.36 +  thus ?case by (metis Seq2 star.step)
   37.37  qed
   37.38  
   37.39 -lemma semi_comp:
   37.40 +lemma seq_comp:
   37.41    "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
   37.42     \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
   37.43 -by(blast intro: star.step star_semi2 star_trans)
   37.44 +by(blast intro: star.step star_seq2 star_trans)
   37.45  
   37.46  text{* The following proof corresponds to one on the board where one would
   37.47  show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. *}
   37.48 @@ -95,7 +95,7 @@
   37.49  next
   37.50    fix c1 c2 s1 s2 s3
   37.51    assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)"
   37.52 -  thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp)
   37.53 +  thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule seq_comp)
   37.54  next
   37.55    fix s::state and b c0 c1 t
   37.56    assume "bval b s"
   37.57 @@ -126,7 +126,7 @@
   37.58    assume b: "bval b s"
   37.59    have "(?w,s) \<rightarrow> (?if, s)" by blast
   37.60    moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b)
   37.61 -  moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w])
   37.62 +  moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule seq_comp[OF c w])
   37.63    ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps)
   37.64  qed
   37.65  
   37.66 @@ -137,7 +137,7 @@
   37.67  next
   37.68    case Assign show ?case by blast
   37.69  next
   37.70 -  case Semi thus ?case by (blast intro: semi_comp)
   37.71 +  case Seq thus ?case by (blast intro: seq_comp)
   37.72  next
   37.73    case IfTrue thus ?case by (blast intro: star.step)
   37.74  next
   37.75 @@ -148,7 +148,7 @@
   37.76  next
   37.77    case WhileTrue
   37.78    thus ?case
   37.79 -    by(metis While semi_comp small_step.IfTrue star.step[of small_step])
   37.80 +    by(metis While seq_comp small_step.IfTrue star.step[of small_step])
   37.81  qed
   37.82  
   37.83  lemma small1_big_continue:
    38.1 --- a/src/HOL/IMP/Types.thy	Fri Apr 27 23:17:58 2012 +0200
    38.2 +++ b/src/HOL/IMP/Types.thy	Sat Apr 28 07:38:22 2012 +0200
    38.3 @@ -41,8 +41,8 @@
    38.4  
    38.5  datatype
    38.6    com = SKIP 
    38.7 -      | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
    38.8 -      | Semi   com  com          ("_; _"  [60, 61] 60)
    38.9 +      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
   38.10 +      | Seq    com  com         ("_; _"  [60, 61] 60)
   38.11        | If     bexp com com     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
   38.12        | While  bexp com         ("WHILE _ DO _"  [0, 61] 61)
   38.13  
   38.14 @@ -54,8 +54,8 @@
   38.15  where
   38.16  Assign:  "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
   38.17  
   38.18 -Semi1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
   38.19 -Semi2:   "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" |
   38.20 +Seq1:   "(SKIP;c,s) \<rightarrow> (c,s)" |
   38.21 +Seq2:   "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" |
   38.22  
   38.23  IfTrue:  "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
   38.24  IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
   38.25 @@ -93,7 +93,7 @@
   38.26  inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
   38.27  Skip_ty: "\<Gamma> \<turnstile> SKIP" |
   38.28  Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
   38.29 -Semi_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
   38.30 +Seq_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
   38.31  If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
   38.32  While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
   38.33  
   38.34 @@ -164,7 +164,7 @@
   38.35    case Assign_ty 
   38.36    thus ?case by (metis Assign aprogress)
   38.37  next
   38.38 -  case Semi_ty thus ?case by simp (metis Semi1 Semi2)
   38.39 +  case Seq_ty thus ?case by simp (metis Seq1 Seq2)
   38.40  next
   38.41    case (If_ty \<Gamma> b c1 c2)
   38.42    then obtain bv where "tbval b s bv" by (metis bprogress)
    39.1 --- a/src/HOL/IMP/VC.thy	Fri Apr 27 23:17:58 2012 +0200
    39.2 +++ b/src/HOL/IMP/VC.thy	Sat Apr 28 07:38:22 2012 +0200
    39.3 @@ -10,7 +10,7 @@
    39.4  datatype acom =
    39.5    ASKIP |
    39.6    Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
    39.7 -  Asemi   acom acom      ("_;/ _"  [60, 61] 60) |
    39.8 +  Aseq   acom acom       ("_;/ _"  [60, 61] 60) |
    39.9    Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
   39.10    Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
   39.11  
   39.12 @@ -19,7 +19,7 @@
   39.13  fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
   39.14  "pre ASKIP Q = Q" |
   39.15  "pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
   39.16 -"pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
   39.17 +"pre (Aseq c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
   39.18  "pre (Aif b c\<^isub>1 c\<^isub>2) Q =
   39.19    (\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
   39.20         (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
   39.21 @@ -30,7 +30,7 @@
   39.22  fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
   39.23  "vc ASKIP Q = (\<lambda>s. True)" |
   39.24  "vc (Aassign x a) Q = (\<lambda>s. True)" |
   39.25 -"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)" |
   39.26 +"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)" |
   39.27  "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)" |
   39.28  "vc (Awhile I b c) Q =
   39.29    (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
   39.30 @@ -42,7 +42,7 @@
   39.31  fun strip :: "acom \<Rightarrow> com" where
   39.32  "strip ASKIP = SKIP" |
   39.33  "strip (Aassign x a) = (x::=a)" |
   39.34 -"strip (Asemi c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
   39.35 +"strip (Aseq c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)" |
   39.36  "strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
   39.37  "strip (Awhile I b c) = (WHILE b DO strip c)"
   39.38  
   39.39 @@ -73,13 +73,13 @@
   39.40  lemma pre_mono:
   39.41    "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
   39.42  proof (induction c arbitrary: P P' s)
   39.43 -  case Asemi thus ?case by simp metis
   39.44 +  case Aseq thus ?case by simp metis
   39.45  qed simp_all
   39.46  
   39.47  lemma vc_mono:
   39.48    "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
   39.49  proof(induction c arbitrary: P P')
   39.50 -  case Asemi thus ?case by simp (metis pre_mono)
   39.51 +  case Aseq thus ?case by simp (metis pre_mono)
   39.52  qed simp_all
   39.53  
   39.54  lemma vc_complete:
   39.55 @@ -94,12 +94,12 @@
   39.56    show ?case (is "\<exists>ac. ?C ac")
   39.57    proof show "?C(Aassign x a)" by simp qed
   39.58  next
   39.59 -  case (Semi P c1 Q c2 R)
   39.60 -  from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
   39.61 -  from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   39.62 +  case (Seq P c1 Q c2 R)
   39.63 +  from Seq.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
   39.64 +  from Seq.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   39.65    show ?case (is "\<exists>ac. ?C ac")
   39.66    proof
   39.67 -    show "?C(Asemi ac1 ac2)"
   39.68 +    show "?C(Aseq ac1 ac2)"
   39.69        using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
   39.70    qed
   39.71  next
   39.72 @@ -127,7 +127,7 @@
   39.73  fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
   39.74  "vcpre ASKIP Q = (\<lambda>s. True, Q)" |
   39.75  "vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
   39.76 -"vcpre (Asemi c\<^isub>1 c\<^isub>2) Q =
   39.77 +"vcpre (Aseq c\<^isub>1 c\<^isub>2) Q =
   39.78    (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
   39.79         (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 wp\<^isub>2
   39.80     in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" |