# HG changeset patch # User nipkow # Date 1335591502 -7200 # Node ID 151d137f1095e2100f58cdfabdaa15c978cf362b # Parent 5d2d63f4363ed557fb0dd704fd0d3a7893ddba10 renamed Semi to Seq diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/ACom.thy --- 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 \'a" where @@ -72,7 +72,7 @@ "map_acom f c = x ::= e {S'} \ (\S. c = x::=e {S} \ S' = f S)" by (cases c) auto -lemma map_acom_Semi: +lemma map_acom_Seq: "map_acom f c = c1';c2' \ (\c1 c2. c = c1;c2 \ map_acom f c1 = c1' \ map_acom f c2 = c2')" by (cases c) auto @@ -99,7 +99,7 @@ "strip c = x::=e \ (EX P. c = x::=e {P})" by (cases c) simp_all -lemma strip_eq_Semi: +lemma strip_eq_Seq: "strip c = c1;c2 \ (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 \ 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] diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int0.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int1.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int2.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy --- 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 diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy --- 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 diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Big_Step.thy --- 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) \ s" | Assign: "(x ::= a,s) \ s(x := aval a s)" | -Semi: "\ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ +Seq: "\ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ (c\<^isub>1;c\<^isub>2, s\<^isub>1) \ s\<^isub>3" | IfTrue: "\ bval b s; (c\<^isub>1,s) \ t \ \ @@ -25,7 +25,7 @@ text_raw{*\begin{isaverbatimwrite}\newcommand{\BigStepEx}{% *} schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \ ?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) \ t" thm AssignE -inductive_cases SemiE[elim!]: "(c1;c2,s1) \ s3" -thm SemiE +inductive_cases SeqE[elim!]: "(c1;c2,s1) \ s3" +thm SeqE inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ t" thm IfE @@ -162,7 +162,7 @@ "(c, s) \ s'" and "(?w, s') \ 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) \ t" by (rule Semi) + hence "(c; ?w, s) \ t" by (rule Seq) -- "then the whole @{text IF}" with `bval b s` have "(?iw, s) \ 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) \ t` have "(c; ?w, s) \ 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) \ s'" and "(?w, s') \ t" by auto -- "with this information, we can build a derivation tree for the @{text WHILE}" diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/C_like.thy --- 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) \ sn" | Assign: "(lhs ::= a,s,n) \ (s(aval lhs s := aval a s),n)" | New: "(New lhs a,s,n) \ (s(aval lhs s := n), n+aval a s)" | -Semi: "\ (c\<^isub>1,sn\<^isub>1) \ sn\<^isub>2; (c\<^isub>2,sn\<^isub>2) \ sn\<^isub>3 \ \ +Seq: "\ (c\<^isub>1,sn\<^isub>1) \ sn\<^isub>2; (c\<^isub>2,sn\<^isub>2) \ sn\<^isub>3 \ \ (c\<^isub>1;c\<^isub>2, sn\<^isub>1) \ sn\<^isub>3" | IfTrue: "\ bval b s; (c\<^isub>1,s,n) \ tn \ \ diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Collecting.thy --- 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} \ c \ (\S'. c = x ::= e {S'} \ S \ S')" by (cases c) auto -lemma Semi_le: "c1;c2 \ c \ (\c1' c2'. c = c1';c2' \ c1 \ c1' \ c2 \ c2')" +lemma Seq_le: "c1;c2 \ c \ (\c1' c2'. c = c1';c2' \ c1 \ c1' \ c2 \ c2')" by (cases c) auto lemma If_le: "IF b THEN c1 ELSE c2 {S} \ c \ @@ -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 \ lift Inter (strip a) A \ 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Com.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Comp_Rev.thy --- 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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Compiler.thy --- 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 \ (0,s1,stk) \* (isize ?cc1,s2,stk)" - using Semi.IH(1) by fastforce + using Seq.IH(1) by fastforce moreover have "?cc1 @ ?cc2 \ (isize ?cc1,s2,stk) \* (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) diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Def_Ass.thy --- 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 \ com \ vname set \ bool" where Skip: "D A SKIP A" | Assign: "vars a \ A \ D A (x ::= a) (insert x A)" | -Semi: "\ D A\<^isub>1 c\<^isub>1 A\<^isub>2; D A\<^isub>2 c\<^isub>2 A\<^isub>3 \ \ D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" | +Seq: "\ D A\<^isub>1 c\<^isub>1 A\<^isub>2; D A\<^isub>2 c\<^isub>2 A\<^isub>3 \ \ D A\<^isub>1 (c\<^isub>1; c\<^isub>2) A\<^isub>3" | If: "\ vars b \ A; D A c\<^isub>1 A\<^isub>1; D A c\<^isub>2 A\<^isub>2 \ \ D A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) (A\<^isub>1 Int A\<^isub>2)" | While: "\ vars b \ A; D A c A' \ \ D A (WHILE b DO c) A" diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Def_Ass_Big.thy --- 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) \ s" | AssignNone: "aval a s = None \ (x ::= a, Some s) \ None" | Assign: "aval a s = Some i \ (x ::= a, Some s) \ Some(s(x := Some i))" | -Semi: "(c\<^isub>1,s\<^isub>1) \ s\<^isub>2 \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ (c\<^isub>1;c\<^isub>2,s\<^isub>1) \ s\<^isub>3" | +Seq: "(c\<^isub>1,s\<^isub>1) \ s\<^isub>2 \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ (c\<^isub>1;c\<^isub>2,s\<^isub>1) \ s\<^isub>3" | IfNone: "bval b s = None \ (IF b THEN c\<^isub>1 ELSE c\<^isub>2,Some s) \ None" | IfTrue: "\ bval b s = Some True; (c\<^isub>1,Some s) \ s' \ \ diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Def_Ass_Small.thy --- 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 \ (x ::= a, s) \ (SKIP, s(x := Some i))" | -Semi1: "(SKIP;c,s) \ (c,s)" | -Semi2: "(c\<^isub>1,s) \ (c\<^isub>1',s') \ (c\<^isub>1;c\<^isub>2,s) \ (c\<^isub>1';c\<^isub>2,s')" | +Seq1: "(SKIP;c,s) \ (c,s)" | +Seq2: "(c\<^isub>1,s) \ (c\<^isub>1',s') \ (c\<^isub>1;c\<^isub>2,s) \ (c\<^isub>1';c\<^isub>2,s')" | IfTrue: "bval b s = Some True \ (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \ (c\<^isub>1,s)" | IfFalse: "bval b s = Some False \ (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \ (c\<^isub>2,s)" | diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Def_Ass_Sound_Big.thy --- 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 diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Def_Ass_Sound_Small.thy --- 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 \ A \ A' \ 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 \ A" "D A c1 M1" "D A c2 M2" "M = M1 \ 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 \ 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 \ 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: diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Fold.thy --- 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 \ IF b THEN c1 ELSE c2 \ diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Hoare.thy --- 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: "\ {\s. P(s[a/x])} x::=a {P}" | -Semi: "\ \ {P} c\<^isub>1 {Q}; \ {Q} c\<^isub>2 {R} \ - \ \ {P} c\<^isub>1;c\<^isub>2 {R}" | +Seq: "\ \ {P} c\<^isub>1 {Q}; \ {Q} c\<^isub>2 {R} \ + \ \ {P} c\<^isub>1;c\<^isub>2 {R}" | If: "\ \ {\s. P s \ bval b s} c\<^isub>1 {Q}; \ {\s. P s \ \ bval b s} c\<^isub>2 {Q} \ \ \ {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}" | @@ -31,9 +31,9 @@ conseq: "\ \s. P' s \ P s; \ {P} c {Q}; \s. Q s \ Q' s \ \ \ {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: "\ \s. P' s \ P s; \ {P} c {Q} \ \ \ {P'} c {Q}" diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/HoareT.thy --- 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: "\\<^sub>t {P} SKIP {P}" | Assign: "\\<^sub>t {\s. P(s[a/x])} x::=a {P}" | -Semi: "\ \\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \ \ \\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}" | +Seq: "\ \\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \ \ \\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}" | If: "\ \\<^sub>t {\s. P s \ bval b s} c\<^isub>1 {Q}; \\<^sub>t {\s. P s \ \ bval b s} c\<^isub>2 {Q} \ \ \\<^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 "\\<^sub>t {\s. 0 \ n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\s. s ''x'' = \{1..n}}" -apply(rule Semi) +apply(rule Seq) prefer 2 apply(rule While' [where P = "\s. s ''x'' = \ {1..s ''y''} \ 0 \ s ''y'' \ s ''y'' \ n" and f = "\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 diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Hoare_Examples.thy --- 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 "\ {\s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\s. s ''x'' = \ {1 .. n}}" -apply(rule hoare.Semi) +apply(rule hoare.Seq) prefer 2 apply(rule While' [where P = "\s. s ''x'' = \ {1..s ''y''} \ 0 \ s ''y'' \ s ''y'' \ 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') diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Hoare_Sound_Complete.thy --- 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 = (\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: "\ {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" diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Live.thy --- 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) \ 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) \ 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) \ 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) \ 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 \ c = x::=a & x : X" by (cases c) auto -lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \ +lemma Seq_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \ (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) \ t2" and s2t2: "s2 = t2 on L c2 X" by auto from IH(2)[OF bc2 s2t2] obtain t3 where t23: "(c2, t2) \ t3" and s3t3: "s3 = t3 on X" diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Live_True.thy --- 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) \ 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) \ t3" and s3t3: "s3 = t3 on X" by auto show ?case using t12 t23 s3t3 by auto diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/OO.thy --- 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 ("(_\_ ::=/ _)" [63,0,62] 62) | Mcall exp string exp ("(_\/_<_>)" [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 \ (me m,ve,sn\<^isub>3) \ (r,ve',sn\<^isub>4) \ \ me \ (oe\m,c\<^isub>1) \ (r,ve\<^isub>3,sn\<^isub>4)" | -Semi: +Seq: "\ me \ (e\<^isub>1,c\<^isub>1) \ (r,c\<^isub>2); me \ (e\<^isub>2,c\<^isub>2) \ c\<^isub>3 \ \ me \ (e\<^isub>1; e\<^isub>2,c\<^isub>1) \ c\<^isub>3" | IfTrue: diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Procs.thy --- 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 _;;/ _})") diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy --- 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 \ (SKIP,s) \ s" | Assign: "pe \ (x ::= a,s) \ s(x := aval a s)" | -Semi: "\ pe \ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; pe \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ +Seq: "\ pe \ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; pe \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ pe \ (c\<^isub>1;c\<^isub>2, s\<^isub>1) \ s\<^isub>3" | IfTrue: "\ bval b s; pe \ (c\<^isub>1,s) \ t \ \ diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Procs_Stat_Vars_Dyn.thy --- 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 \ (SKIP,s) \ s" | Assign: "pe \ (x ::= a,s) \ s(x := aval a s)" | -Semi: "\ pe \ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; pe \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ +Seq: "\ pe \ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; pe \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ pe \ (c\<^isub>1;c\<^isub>2, s\<^isub>1) \ s\<^isub>3" | IfTrue: "\ bval b s; pe \ (c\<^isub>1,s) \ t \ \ diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Procs_Stat_Vars_Stat.thy --- 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 \ (SKIP,s) \ s" | Assign: "(pe,ve,f) \ (x ::= a,s) \ s(ve x := aval a (s o ve))" | -Semi: "\ e \ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; e \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ +Seq: "\ e \ (c\<^isub>1,s\<^isub>1) \ s\<^isub>2; e \ (c\<^isub>2,s\<^isub>2) \ s\<^isub>3 \ \ e \ (c\<^isub>1;c\<^isub>2, s\<^isub>1) \ s\<^isub>3" | IfTrue: "\ bval b (s \ venv e); e \ (c\<^isub>1,s) \ t \ \ diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Sec_Typing.thy --- 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 \ SKIP" | Assign: "\ sec x \ sec_aexp a; sec x \ l \ \ l \ x ::= a" | -Semi: +Seq: "\ l \ c\<^isub>1; l \ c\<^isub>2 \ \ l \ c\<^isub>1;c\<^isub>2" | If: "\ max (sec_bexp b) l \ c\<^isub>1; max (sec_bexp b) l \ c\<^isub>2 \ \ l \ 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 \ c1" by auto @@ -85,7 +85,7 @@ thus "s y = t y" using `s = t (\ 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 \ c1" "sec_bexp b \ c2" using IfTrue.prems(2) by auto @@ -186,7 +186,7 @@ "l \' SKIP" | Assign': "\ sec x \ sec_aexp a; sec x \ l \ \ l \' x ::= a" | -Semi': +Seq': "\ l \' c\<^isub>1; l \' c\<^isub>2 \ \ l \' c\<^isub>1;c\<^isub>2" | If': "\ sec_bexp b \ l; l \' c\<^isub>1; l \' c\<^isub>2 \ \ l \' 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 @@ "\ SKIP : l" | Assign2: "sec x \ sec_aexp a \ \ x ::= a : sec x" | -Semi2: +Seq2: "\ \ c\<^isub>1 : l\<^isub>1; \ c\<^isub>2 : l\<^isub>2 \ \ \ c\<^isub>1;c\<^isub>2 : min l\<^isub>1 l\<^isub>2 " | If2: "\