replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
--- a/src/HOL/IMP/ACom.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/ACom.thy Fri May 17 08:19:52 2013 +0200
@@ -9,7 +9,7 @@
datatype 'a acom =
SKIP 'a ("SKIP {_}" 61) |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
- Seq "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) |
+ Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) |
If bexp 'a "('a acom)" 'a "('a acom)" 'a
("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})" [0, 0, 0, 61, 0, 0] 61) |
While 'a bexp 'a "('a acom)" 'a
@@ -19,7 +19,7 @@
fun strip :: "'a acom \<Rightarrow> com" where
"strip (SKIP {P}) = com.SKIP" |
"strip (x ::= e {P}) = x ::= e" |
-"strip (C\<^isub>1;C\<^isub>2) = strip C\<^isub>1; strip C\<^isub>2" |
+"strip (C\<^isub>1;;C\<^isub>2) = strip C\<^isub>1;; strip C\<^isub>2" |
"strip (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {P}) =
IF b THEN strip C\<^isub>1 ELSE strip C\<^isub>2" |
"strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C"
@@ -29,7 +29,7 @@
fun asize :: "com \<Rightarrow> nat" where
"asize com.SKIP = 1" |
"asize (x ::= e) = 1" |
-"asize (C\<^isub>1;C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2" |
+"asize (C\<^isub>1;;C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2" |
"asize (IF b THEN C\<^isub>1 ELSE C\<^isub>2) = asize C\<^isub>1 + asize C\<^isub>2 + 3" |
"asize (WHILE b DO C) = asize C + 3"
text_raw{*}%endsnip*}
@@ -41,7 +41,7 @@
fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where
"annotate f com.SKIP = SKIP {f 0}" |
"annotate f (x ::= e) = x ::= e {f 0}" |
-"annotate f (c\<^isub>1;c\<^isub>2) = annotate f c\<^isub>1; annotate (shift f (asize c\<^isub>1)) c\<^isub>2" |
+"annotate f (c\<^isub>1;;c\<^isub>2) = annotate f c\<^isub>1;; annotate (shift f (asize c\<^isub>1)) c\<^isub>2" |
"annotate f (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
IF b THEN {f 0} annotate (shift f 1) c\<^isub>1
ELSE {f(asize c\<^isub>1 + 1)} annotate (shift f (asize c\<^isub>1 + 2)) c\<^isub>2
@@ -54,7 +54,7 @@
fun annos :: "'a acom \<Rightarrow> 'a list" where
"annos (SKIP {P}) = [P]" |
"annos (x ::= e {P}) = [P]" |
-"annos (C\<^isub>1;C\<^isub>2) = annos C\<^isub>1 @ annos C\<^isub>2" |
+"annos (C\<^isub>1;;C\<^isub>2) = annos C\<^isub>1 @ annos C\<^isub>2" |
"annos (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) =
P\<^isub>1 # annos C\<^isub>1 @ P\<^isub>2 # annos C\<^isub>2 @ [Q]" |
"annos ({I} WHILE b DO {P} C {Q}) = I # P # annos C @ [Q]"
@@ -70,7 +70,7 @@
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
"map_acom f (SKIP {P}) = SKIP {f P}" |
"map_acom f (x ::= e {P}) = x ::= e {f P}" |
-"map_acom f (C\<^isub>1;C\<^isub>2) = map_acom f C\<^isub>1; map_acom f C\<^isub>2" |
+"map_acom f (C\<^isub>1;;C\<^isub>2) = map_acom f C\<^isub>1;; map_acom f C\<^isub>2" |
"map_acom f (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) =
IF b THEN {f P\<^isub>1} map_acom f C\<^isub>1 ELSE {f P\<^isub>2} map_acom f C\<^isub>2
{f Q}" |
@@ -139,7 +139,7 @@
by (cases C) simp_all
lemma strip_eq_Seq:
- "strip C = c1;c2 \<longleftrightarrow> (EX C1 C2. C = C1;C2 & strip C1 = c1 & strip C2 = c2)"
+ "strip C = c1;;c2 \<longleftrightarrow> (EX C1 C2. C = C1;;C2 & strip C1 = c1 & strip C2 = c2)"
by (cases C) simp_all
lemma strip_eq_If:
--- a/src/HOL/IMP/Abs_Int0.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Fri May 17 08:19:52 2013 +0200
@@ -378,7 +378,7 @@
lemma top_on_acom_simps:
"top_on_acom (SKIP {Q}) X = top_on_opt Q X"
"top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
- "top_on_acom (C1;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
+ "top_on_acom (C1;;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
"top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
(top_on_opt P1 X \<and> top_on_acom C1 X \<and> top_on_opt P2 X \<and> top_on_acom C2 X \<and> top_on_opt Q X)"
"top_on_acom ({I} WHILE b DO {P} C {Q}) X =
--- a/src/HOL/IMP/Abs_Int1.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Fri May 17 08:19:52 2013 +0200
@@ -156,7 +156,7 @@
lemma top_on_acom_simps:
"top_on_acom (SKIP {Q}) X = top_on_opt Q X"
"top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
- "top_on_acom (C1;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
+ "top_on_acom (C1;;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
"top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
(top_on_opt P1 X \<and> top_on_acom C1 X \<and> top_on_opt P2 X \<and> top_on_acom C2 X \<and> top_on_opt Q X)"
"top_on_acom ({I} WHILE b DO {P} C {Q}) X =
--- a/src/HOL/IMP/Abs_Int1_parity.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Fri May 17 08:19:52 2013 +0200
@@ -133,12 +133,12 @@
subsubsection "Tests"
definition "test1_parity =
- ''x'' ::= N 1;
+ ''x'' ::= N 1;;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
value [code] "show_acom (the(AI_parity test1_parity))"
definition "test2_parity =
- ''x'' ::= N 1;
+ ''x'' ::= N 1;;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
definition "steps c i = ((step_parity \<top>) ^^ i) (bot c)"
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy Fri May 17 08:19:52 2013 +0200
@@ -33,7 +33,7 @@
fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
"AI SKIP S = S" |
"AI (x ::= a) S = update S x (aval' a S)" |
-"AI (c1;c2) S = AI c2 (AI c1 S)" |
+"AI (c1;;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
"AI (WHILE b DO c) S = pfp (AI c) S"
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri May 17 08:19:52 2013 +0200
@@ -68,8 +68,8 @@
text{* Straight line code: *}
definition "test1_const =
- ''y'' ::= N 7;
- ''z'' ::= Plus (V ''y'') (N 2);
+ ''y'' ::= N 7;;
+ ''z'' ::= Plus (V ''y'') (N 2);;
''y'' ::= Plus (V ''x'') (N 0)"
text{* Conditional: *}
@@ -78,27 +78,27 @@
text{* Conditional, test is ignored: *}
definition "test3_const =
- ''x'' ::= N 42;
+ ''x'' ::= N 42;;
IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
text{* While: *}
definition "test4_const =
- ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
+ ''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0"
text{* While, test is ignored: *}
definition "test5_const =
- ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+ ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
text{* Iteration is needed: *}
definition "test6_const =
- ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
- WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
+ ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 2;;
+ WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'')"
text{* More iteration would be needed: *}
definition "test7_const =
- ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
+ ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 0;; ''u'' ::= N 3;;
WHILE Less (V ''x'') (N 1)
- DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+ DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'';; ''z'' ::= V ''u'')"
value [code] "list (AI_const test1_const Top)"
value [code] "list (AI_const test2_const Top)"
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Fri May 17 08:19:52 2013 +0200
@@ -150,7 +150,7 @@
fun AI :: "com \<Rightarrow> 'a st \<Rightarrow> 'a st" where
"AI SKIP S = S" |
"AI (x ::= a) S = S(x := aval' a S)" |
-"AI (c1;c2) S = AI c2 (AI c1 S)" |
+"AI (c1;;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
"AI (WHILE b DO c) S = pfp (AI c) S"
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Fri May 17 08:19:52 2013 +0200
@@ -174,7 +174,7 @@
"AI SKIP S = S" |
"AI (x ::= a) S =
(case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
-"AI (c1;c2) S = AI c2 (AI c1 S)" |
+"AI (c1;;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S =
AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
"AI (WHILE b DO c) S =
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri May 17 08:19:52 2013 +0200
@@ -232,7 +232,7 @@
(Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
definition "test_ivl1 =
- ''y'' ::= N 7;
+ ''y'' ::= N 7;;
IF Less (V ''x'') (V ''y'')
THEN ''y'' ::= Plus (V ''y'') (V ''x'')
ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
@@ -245,25 +245,25 @@
value "list_up (AI_ivl test6_const Top)"
definition "test2_ivl =
- ''y'' ::= N 7;
+ ''y'' ::= N 7;;
WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
value [code] "list_up(AI_ivl test2_ivl Top)"
definition "test3_ivl =
- ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
+ ''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');;
WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
+ DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))"
value [code] "list_up(AI_ivl test3_ivl Top)"
definition "test4_ivl =
- ''x'' ::= N 0; ''y'' ::= N 0;
+ ''x'' ::= N 0;; ''y'' ::= N 0;;
WHILE Less (V ''x'') (N 1001)
- DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
+ DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
value [code] "list_up(AI_ivl test4_ivl Top)"
text{* Nontermination not detected: *}
definition "test5_ivl =
- ''x'' ::= N 0;
+ ''x'' ::= N 0;;
WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
value [code] "list_up(AI_ivl test5_ivl Top)"
--- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Fri May 17 08:19:52 2013 +0200
@@ -9,7 +9,7 @@
datatype 'a acom =
SKIP 'a ("SKIP {_}" 61) |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
- Seq "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) |
+ 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
@@ -18,21 +18,21 @@
fun post :: "'a acom \<Rightarrow>'a" where
"post (SKIP {P}) = P" |
"post (x ::= e {P}) = P" |
-"post (c1; c2) = post c2" |
+"post (c1;; c2) = post c2" |
"post (IF b THEN c1 ELSE c2 {P}) = P" |
"post ({Inv} WHILE b DO c {P}) = P"
fun strip :: "'a acom \<Rightarrow> com" where
"strip (SKIP {P}) = com.SKIP" |
"strip (x ::= e {P}) = (x ::= e)" |
-"strip (c1;c2) = (strip c1; strip c2)" |
+"strip (c1;;c2) = (strip c1;; strip c2)" |
"strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" |
"strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)"
fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
"anno a com.SKIP = SKIP {a}" |
"anno a (x ::= e) = (x ::= e {a})" |
-"anno a (c1;c2) = (anno a c1; anno a c2)" |
+"anno a (c1;;c2) = (anno a c1;; anno a c2)" |
"anno a (IF b THEN c1 ELSE c2) =
(IF b THEN anno a c1 ELSE anno a c2 {a})" |
"anno a (WHILE b DO c) =
@@ -41,14 +41,14 @@
fun annos :: "'a acom \<Rightarrow> 'a list" where
"annos (SKIP {a}) = [a]" |
"annos (x::=e {a}) = [a]" |
-"annos (C1;C2) = annos C1 @ annos C2" |
+"annos (C1;;C2) = annos C1 @ annos C2" |
"annos (IF b THEN C1 ELSE C2 {a}) = a # annos C1 @ annos C2" |
"annos ({i} WHILE b DO C {a}) = i # a # annos C"
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
"map_acom f (SKIP {P}) = SKIP {f P}" |
"map_acom f (x ::= e {P}) = (x ::= e {f P})" |
-"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
+"map_acom f (c1;;c2) = (map_acom f c1;; map_acom f c2)" |
"map_acom f (IF b THEN c1 ELSE c2 {P}) =
(IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" |
"map_acom f ({Inv} WHILE b DO c {P}) =
@@ -70,8 +70,8 @@
by (cases c) auto
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')"
+ "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
lemma map_acom_If:
@@ -97,7 +97,7 @@
by (cases c) simp_all
lemma strip_eq_Seq:
- "strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)"
+ "strip c = c1;;c2 \<longleftrightarrow> (EX d1 d2. c = d1;;d2 & strip d1 = c1 & strip d2 = c2)"
by (cases c) simp_all
lemma strip_eq_If:
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy Fri May 17 08:19:52 2013 +0200
@@ -72,7 +72,7 @@
fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
-"le_acom (c1;c2) (c1';c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" |
+"le_acom (c1;;c2) (c1';;c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" |
"le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) =
(b=b' \<and> le_acom c1 c1' \<and> le_acom c2 c2' \<and> S \<sqsubseteq> S')" |
"le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) =
@@ -85,7 +85,7 @@
lemma [simp]: "x ::= e {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<sqsubseteq> S')"
by (cases c) auto
-lemma [simp]: "c1;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')"
+lemma [simp]: "c1;;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';;c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')"
by (cases c) auto
lemma [simp]: "IF b THEN c1 ELSE c2 {S} \<sqsubseteq> c \<longleftrightarrow>
@@ -263,7 +263,7 @@
"step' S (SKIP {P}) = (SKIP {S})" |
"step' S (x ::= e {P}) =
x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" |
-"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
+"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" |
"step' S (IF b THEN c1 ELSE c2 {P}) =
IF b THEN step' S c1 ELSE step' S c2 {post c1 \<squnion> post c2}" |
"step' S ({Inv} WHILE b DO c {P}) =
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy Fri May 17 08:19:52 2013 +0200
@@ -33,7 +33,7 @@
"step' S (SKIP {P}) = (SKIP {S})" |
"step' S (x ::= e {P}) =
x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
-"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
+"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" |
"step' S (IF b THEN c1 ELSE c2 {P}) =
(let c1' = step' S c1; c2' = step' S c2
in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Fri May 17 08:19:52 2013 +0200
@@ -122,13 +122,13 @@
subsubsection "Tests"
definition "test1_parity =
- ''x'' ::= N 1;
+ ''x'' ::= N 1;;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
value "show_acom_opt (AI_parity test1_parity)"
definition "test2_parity =
- ''x'' ::= N 1;
+ ''x'' ::= N 1;;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
value "show_acom ((step_parity \<top> ^^1) (anno None test2_parity))"
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Fri May 17 08:19:52 2013 +0200
@@ -148,7 +148,7 @@
"step' S (SKIP {P}) = (SKIP {S})" |
"step' S (x ::= e {P}) =
x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" |
-"step' S (c1; c2) = step' S c1; step' (post c1) c2" |
+"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" |
"step' S (IF b THEN c1 ELSE c2 {P}) =
(let c1' = step' (bfilter b True S) c1; c2' = step' (bfilter b False S) c2
in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Fri May 17 08:19:52 2013 +0200
@@ -107,7 +107,7 @@
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
-"map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" |
+"map2_acom f (c1;;c2) (c1';;c2') = (map2_acom f c1 c1';; map2_acom f c2 c2')" |
"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) =
(IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" |
"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) =
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Fri May 17 08:19:52 2013 +0200
@@ -17,7 +17,7 @@
fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
"(SKIP {S}) \<le> (SKIP {S'}) = (S \<le> S')" |
"(x ::= e {S}) \<le> (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<le> S')" |
-"(c1;c2) \<le> (c1';c2') = (c1 \<le> c1' \<and> c2 \<le> c2')" |
+"(c1;;c2) \<le> (c1';;c2') = (c1 \<le> c1' \<and> c2 \<le> c2')" |
"(IF b THEN c1 ELSE c2 {S}) \<le> (IF b' THEN c1' ELSE c2' {S'}) =
(b=b' \<and> c1 \<le> c1' \<and> c2 \<le> c2' \<and> S \<le> S')" |
"({Inv} WHILE b DO c {P}) \<le> ({Inv'} WHILE b' DO c' {P'}) =
@@ -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 Seq_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>
@@ -64,12 +64,12 @@
end
fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where
-"sub\<^isub>1(c1;c2) = c1" |
+"sub\<^isub>1(c1;;c2) = c1" |
"sub\<^isub>1(IF b THEN c1 ELSE c2 {S}) = c1" |
"sub\<^isub>1({I} WHILE b DO c {P}) = c"
fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where
-"sub\<^isub>2(c1;c2) = c2" |
+"sub\<^isub>2(c1;;c2) = c2" |
"sub\<^isub>2(IF b THEN c1 ELSE c2 {S}) = c2"
fun invar :: "'a acom \<Rightarrow> 'a" where
@@ -79,8 +79,8 @@
where
"lift F com.SKIP M = (SKIP {F (post ` M)})" |
"lift F (x ::= a) M = (x ::= a {F (post ` M)})" |
-"lift F (c1;c2) M =
- lift F c1 (sub\<^isub>1 ` M); lift F c2 (sub\<^isub>2 ` M)" |
+"lift F (c1;;c2) M =
+ lift F c1 (sub\<^isub>1 ` M);; lift F c2 (sub\<^isub>2 ` M)" |
"lift F (IF b THEN c1 ELSE c2) M =
IF b THEN lift F c1 (sub\<^isub>1 ` M) ELSE lift F c2 (sub\<^isub>2 ` M)
{F (post ` M)}" |
@@ -142,7 +142,7 @@
"step S (SKIP {P}) = (SKIP {S})" |
"step S (x ::= e {P}) =
(x ::= e {{s'. EX s:S. s' = s(x := aval e s)}})" |
-"step S (c1; c2) = step S c1; step (post c1) c2" |
+"step S (c1;; c2) = step S c1;; step (post c1) c2" |
"step S (IF b THEN c1 ELSE c2 {P}) =
IF b THEN step {s:S. bval b s} c1 ELSE step {s:S. \<not> bval b s} c2
{post c1 \<union> post c2}" |
--- a/src/HOL/IMP/Abs_Int_Tests.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy Fri May 17 08:19:52 2013 +0200
@@ -8,8 +8,8 @@
text{* Straight line code: *}
definition "test1_const =
- ''y'' ::= N 7;
- ''z'' ::= Plus (V ''y'') (N 2);
+ ''y'' ::= N 7;;
+ ''z'' ::= Plus (V ''y'') (N 2);;
''y'' ::= Plus (V ''x'') (N 0)"
text{* Conditional: *}
@@ -18,26 +18,26 @@
text{* Conditional, test is relevant: *}
definition "test3_const =
- ''x'' ::= N 42;
+ ''x'' ::= N 42;;
IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
text{* While: *}
definition "test4_const =
- ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
+ ''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0"
text{* While, test is relevant: *}
definition "test5_const =
- ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
+ ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
text{* Iteration is needed: *}
definition "test6_const =
- ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
- WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
+ ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 2;;
+ WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'')"
text{* For intervals: *}
definition "test1_ivl =
- ''y'' ::= N 7;
+ ''y'' ::= N 7;;
IF Less (V ''x'') (V ''y'')
THEN ''y'' ::= Plus (V ''y'') (V ''x'')
ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
@@ -47,22 +47,22 @@
DO ''x'' ::= Plus (V ''x'') (N 1)"
definition "test3_ivl =
- ''x'' ::= N 7;
+ ''x'' ::= N 7;;
WHILE Less (V ''x'') (N 100)
DO ''x'' ::= Plus (V ''x'') (N 1)"
definition "test4_ivl =
- ''x'' ::= N 0; ''y'' ::= N 0;
+ ''x'' ::= N 0;; ''y'' ::= N 0;;
WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N 1))"
+ DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N 1))"
definition "test5_ivl =
- ''x'' ::= N 0; ''y'' ::= N 0;
+ ''x'' ::= N 0;; ''y'' ::= N 0;;
WHILE Less (V ''x'') (N 1000)
- DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
+ DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
definition "test6_ivl =
- ''x'' ::= N 0;
+ ''x'' ::= N 0;;
WHILE Less (N -1) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
end
--- a/src/HOL/IMP/Big_Step.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Big_Step.thy Fri May 17 08:19:52 2013 +0200
@@ -11,7 +11,7 @@
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
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" |
+ (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>
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
@@ -24,7 +24,7 @@
text_raw{*}%endsnip*}
text_raw{*\snip{BigStepEx}{1}{2}{% *}
-schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
+schematic_lemma ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \<Rightarrow> ?t"
apply(rule Seq)
apply(rule Assign)
apply simp
@@ -89,7 +89,7 @@
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
thm AssignE
-inductive_cases SeqE[elim!]: "(c1;c2,s1) \<Rightarrow> s3"
+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
@@ -143,7 +143,7 @@
transformation on programs:
*}
lemma unfold_while:
- "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
+ "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
proof -
-- "to show the equivalence, we look at the derivation tree for"
-- "each side and from that construct a derivation tree for the other side"
@@ -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 Seq)
+ 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)
}
@@ -183,7 +183,7 @@
-- "on the other hand, if @{text b} is @{text True} in state @{text s},"
-- {* 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
+ with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto
-- "and for this, only the Seq-rule is applicable:"
then obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
@@ -203,7 +203,7 @@
prove many such facts automatically. *}
lemma while_unfold:
- "(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)"
+ "(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)"
by blast
lemma triv_if:
--- a/src/HOL/IMP/Collecting.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Collecting.thy Fri May 17 08:19:52 2013 +0200
@@ -19,7 +19,7 @@
"Step S (SKIP {Q}) = (SKIP {S})" |
"Step S (x ::= e {Q}) =
x ::= e {f x e S}" |
-"Step S (C1; C2) = Step S C1; Step (post C1) C2" |
+"Step S (C1;; C2) = Step S C1;; Step (post C1) C2" |
"Step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
IF b THEN {g b S} Step P1 C1 ELSE {g (Not b) S} Step P2 C2
{post C1 \<squnion> post C2}" |
@@ -69,7 +69,7 @@
lemma Assign_le[simp]: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
by (cases c) (auto simp:less_eq_acom_def anno_def)
-lemma Seq_le[simp]: "C1;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
+lemma Seq_le[simp]: "C1;;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';;C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
apply (cases C)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done
--- a/src/HOL/IMP/Com.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Com.thy Fri May 17 08:19:52 2013 +0200
@@ -5,7 +5,7 @@
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
- | Seq 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/Compiler.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy Fri May 17 08:19:52 2013 +0200
@@ -209,7 +209,7 @@
fun ccomp :: "com \<Rightarrow> instr list" where
"ccomp SKIP = []" |
"ccomp (x ::= a) = acomp a @ [STORE x]" |
-"ccomp (c\<^isub>1;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
+"ccomp (c\<^isub>1;;c\<^isub>2) = ccomp c\<^isub>1 @ ccomp c\<^isub>2" |
"ccomp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) =
(let cc\<^isub>1 = ccomp c\<^isub>1; cc\<^isub>2 = ccomp c\<^isub>2; cb = bcomp b False (size cc\<^isub>1 + 1)
in cb @ cc\<^isub>1 @ JMP (size cc\<^isub>2) # cc\<^isub>2)" |
--- a/src/HOL/IMP/Def_Init.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Def_Init.thy Fri May 17 08:19:52 2013 +0200
@@ -7,7 +7,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)" |
-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" |
+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"
@@ -15,7 +15,7 @@
inductive_cases [elim!]:
"D A SKIP A'"
"D A (x ::= a) A'"
-"D A (c1;c2) A'"
+"D A (c1;;c2) A'"
"D A (IF b THEN c1 ELSE c2) A'"
"D A (WHILE b DO c) A'"
--- a/src/HOL/IMP/Def_Init_Big.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Def_Init_Big.thy Fri May 17 08:19:52 2013 +0200
@@ -13,7 +13,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))" |
-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" |
+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_Init_Small.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Def_Init_Small.thy Fri May 17 08:19:52 2013 +0200
@@ -11,13 +11,13 @@
where
Assign: "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |
-Seq1: "(SKIP;c,s) \<rightarrow> (c,s)" |
-Seq2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" |
+Seq1: "(SKIP;;c,s) \<rightarrow> (c,s)" |
+Seq2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';;c\<^isub>2,s')" |
IfTrue: "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" |
IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" |
-While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
lemmas small_step_induct = small_step.induct[split_format(complete)]
--- a/src/HOL/IMP/Def_Init_Sound_Small.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Def_Init_Sound_Small.thy Fri May 17 08:19:52 2013 +0200
@@ -40,7 +40,7 @@
then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
moreover
then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
- ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"
+ ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
by (metis D.If[OF `vars b \<subseteq> dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
thus ?case by (metis D_incr `A = dom s`)
next
--- a/src/HOL/IMP/Denotation.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Denotation.thy Fri May 17 08:19:52 2013 +0200
@@ -14,7 +14,7 @@
fun C :: "com \<Rightarrow> com_den" where
"C SKIP = Id" |
"C (x ::= a) = {(s,t). t = s(x := aval a s)}" |
-"C (c0;c1) = C(c0) O C(c1)" |
+"C (c0;;c1) = C(c0) O C(c1)" |
"C (IF b THEN c1 ELSE c2) = {(s,t). (s,t) \<in> C c1 \<and> bval b s} \<union>
{(s,t). (s,t) \<in> C c2 \<and> \<not>bval b s}" |
"C(WHILE b DO c) = lfp (Gamma b (C c))"
@@ -23,7 +23,7 @@
lemma Gamma_mono: "mono (Gamma b c)"
by (unfold Gamma_def mono_def) fast
-lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)"
+lemma C_While_If: "C(WHILE b DO c) = C(IF b THEN c;;WHILE b DO c ELSE SKIP)"
apply simp
apply (subst lfp_unfold [OF Gamma_mono]) --{*lhs only*}
apply (simp add: Gamma_def)
--- a/src/HOL/IMP/Finite_Reachable.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Finite_Reachable.thy Fri May 17 08:19:52 2013 +0200
@@ -43,14 +43,14 @@
by(auto simp: reachable_def dest:Assign_starD)
-lemma Seq_stepsnD: "(c1; c2, s) \<rightarrow>(n) (c', t) \<Longrightarrow>
- (\<exists>c1' m. c' = c1'; c2 \<and> (c1, s) \<rightarrow>(m) (c1', t) \<and> m \<le> n) \<or>
+lemma Seq_stepsnD: "(c1;; c2, s) \<rightarrow>(n) (c', t) \<Longrightarrow>
+ (\<exists>c1' m. c' = c1';; c2 \<and> (c1, s) \<rightarrow>(m) (c1', t) \<and> m \<le> n) \<or>
(\<exists>s2 m1 m2. (c1,s) \<rightarrow>(m1) (SKIP,s2) \<and> (c2, s2) \<rightarrow>(m2) (c', t) \<and> m1+m2 < n)"
proof(induction n arbitrary: c1 c2 s)
case 0 thus ?case by auto
next
case (Suc n)
- from Suc.prems obtain s' c12' where "(c1;c2, s) \<rightarrow> (c12', s')"
+ from Suc.prems obtain s' c12' where "(c1;;c2, s) \<rightarrow> (c12', s')"
and n: "(c12',s') \<rightarrow>(n) (c',t)" by auto
from this(1) show ?case
proof
@@ -59,14 +59,14 @@
using n by auto
thus ?case by blast
next
- fix c1' s'' assume 1: "(c12', s') = (c1'; c2, s'')" "(c1, s) \<rightarrow> (c1', s'')"
- hence n': "(c1';c2,s') \<rightarrow>(n) (c',t)" using n by auto
+ fix c1' s'' assume 1: "(c12', s') = (c1';; c2, s'')" "(c1, s) \<rightarrow> (c1', s'')"
+ hence n': "(c1';;c2,s') \<rightarrow>(n) (c',t)" using n by auto
from Suc.IH[OF n'] show ?case
proof
- assume "\<exists>c1'' m. c' = c1''; c2 \<and> (c1', s') \<rightarrow>(m) (c1'', t) \<and> m \<le> n"
+ assume "\<exists>c1'' m. c' = c1'';; c2 \<and> (c1', s') \<rightarrow>(m) (c1'', t) \<and> m \<le> n"
(is "\<exists> a b. ?P a b")
then obtain c1'' m where 2: "?P c1'' m" by blast
- hence "c' = c1'';c2 \<and> (c1, s) \<rightarrow>(Suc m) (c1'',t) \<and> Suc m \<le> Suc n"
+ hence "c' = c1'';;c2 \<and> (c1, s) \<rightarrow>(Suc m) (c1'',t) \<and> Suc m \<le> Suc n"
using 1 by auto
thus ?case by blast
next
@@ -80,13 +80,13 @@
qed
qed
-corollary Seq_starD: "(c1; c2, s) \<rightarrow>* (c', t) \<Longrightarrow>
- (\<exists>c1'. c' = c1'; c2 \<and> (c1, s) \<rightarrow>* (c1', t)) \<or>
+corollary Seq_starD: "(c1;; c2, s) \<rightarrow>* (c', t) \<Longrightarrow>
+ (\<exists>c1'. c' = c1';; c2 \<and> (c1, s) \<rightarrow>* (c1', t)) \<or>
(\<exists>s2. (c1,s) \<rightarrow>* (SKIP,s2) \<and> (c2, s2) \<rightarrow>* (c', t))"
by(metis Seq_stepsnD star_if_stepsn stepsn_if_star)
-lemma reachable_Seq: "reachable (c1;c2) \<subseteq>
- (\<lambda>c1'. c1';c2) ` reachable c1 \<union> reachable c2"
+lemma reachable_Seq: "reachable (c1;;c2) \<subseteq>
+ (\<lambda>c1'. c1';;c2) ` reachable c1 \<union> reachable c2"
by(auto simp: reachable_def image_def dest!: Seq_starD)
@@ -100,8 +100,8 @@
lemma While_stepsnD: "(WHILE b DO c, s) \<rightarrow>(n) (c2,t) \<Longrightarrow>
- c2 \<in> {WHILE b DO c, IF b THEN c ; WHILE b DO c ELSE SKIP, SKIP}
- \<or> (\<exists>c1. c2 = c1 ; WHILE b DO c \<and> (\<exists> s1 s2. (c,s1) \<rightarrow>* (c1,s2)))"
+ c2 \<in> {WHILE b DO c, IF b THEN c ;; WHILE b DO c ELSE SKIP, SKIP}
+ \<or> (\<exists>c1. c2 = c1 ;; WHILE b DO c \<and> (\<exists> s1 s2. (c,s1) \<rightarrow>* (c1,s2)))"
proof(induction n arbitrary: s rule: less_induct)
case (less n1)
show ?case
@@ -110,7 +110,7 @@
next
case (Suc n2)
let ?w = "WHILE b DO c"
- let ?iw = "IF b THEN c ; ?w ELSE SKIP"
+ let ?iw = "IF b THEN c ;; ?w ELSE SKIP"
from Suc less.prems have n2: "(?iw,s) \<rightarrow>(n2) (c2,t)" by(auto elim!: WhileE)
show ?thesis
proof(cases n2)
@@ -122,11 +122,11 @@
from this(1)
show ?thesis
proof
- assume "(iw', s') = (c; WHILE b DO c, s)"
- with n3 have "(c;?w, s) \<rightarrow>(n3) (c2,t)" by auto
+ assume "(iw', s') = (c;; WHILE b DO c, s)"
+ with n3 have "(c;;?w, s) \<rightarrow>(n3) (c2,t)" by auto
from Seq_stepsnD[OF this] show ?thesis
proof
- assume "\<exists>c1' m. c2 = c1'; ?w \<and> (c,s) \<rightarrow>(m) (c1', t) \<and> m \<le> n3"
+ assume "\<exists>c1' m. c2 = c1';; ?w \<and> (c,s) \<rightarrow>(m) (c1', t) \<and> m \<le> n3"
thus ?thesis by (metis star_if_stepsn)
next
assume "\<exists>s2 m1 m2. (c, s) \<rightarrow>(m1) (SKIP, s2) \<and>
@@ -144,8 +144,8 @@
qed
lemma reachable_While: "reachable (WHILE b DO c) \<subseteq>
- {WHILE b DO c, IF b THEN c ; WHILE b DO c ELSE SKIP, SKIP} \<union>
- (\<lambda>c'. c' ; WHILE b DO c) ` reachable c"
+ {WHILE b DO c, IF b THEN c ;; WHILE b DO c ELSE SKIP, SKIP} \<union>
+ (\<lambda>c'. c' ;; WHILE b DO c) ` reachable c"
apply(auto simp: reachable_def image_def)
by (metis While_stepsnD insertE singletonE stepsn_if_star)
--- a/src/HOL/IMP/Fold.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Fold.thy Fri May 17 08:19:52 2013 +0200
@@ -33,7 +33,7 @@
primrec lnames :: "com \<Rightarrow> vname set" where
"lnames SKIP = {}" |
"lnames (x ::= a) = {x}" |
-"lnames (c1; c2) = lnames c1 \<union> lnames c2" |
+"lnames (c1;; c2) = lnames c1 \<union> lnames c2" |
"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
"lnames (WHILE b DO c) = lnames c"
@@ -41,14 +41,14 @@
"defs SKIP t = t" |
"defs (x ::= a) t =
(case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
-"defs (c1;c2) t = (defs c2 o defs c1) t" |
+"defs (c1;;c2) t = (defs c2 o defs c1) t" |
"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
"defs (WHILE b DO c) t = t |` (-lnames c)"
primrec fold where
"fold SKIP _ = SKIP" |
"fold (x ::= a) t = (x ::= (afold a t))" |
-"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" |
+"fold (c1;;c2) t = (fold c1 t;; fold c2 (defs c1 t))" |
"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))"
@@ -259,7 +259,7 @@
"bdefs SKIP t = t" |
"bdefs (x ::= a) t =
(case afold a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
-"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
+"bdefs (c1;;c2) t = (bdefs c2 o bdefs c1) t" |
"bdefs (IF b THEN c1 ELSE c2) t = (case bfold b t of
Bc True \<Rightarrow> bdefs c1 t
| Bc False \<Rightarrow> bdefs c2 t
@@ -270,7 +270,7 @@
primrec fold' where
"fold' SKIP _ = SKIP" |
"fold' (x ::= a) t = (x ::= (afold a t))" |
-"fold' (c1;c2) t = (fold' c1 t; fold' c2 (bdefs c1 t))" |
+"fold' (c1;;c2) t = (fold' c1 t;; fold' c2 (bdefs c1 t))" |
"fold' (IF b THEN c1 ELSE c2) t = (case bfold b t of
Bc True \<Rightarrow> fold' c1 t
| Bc False \<Rightarrow> fold' c2 t
--- a/src/HOL/IMP/Hoare.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Hoare.thy Fri May 17 08:19:52 2013 +0200
@@ -20,7 +20,7 @@
Assign: "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}" |
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}" |
+ \<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}" |
--- a/src/HOL/IMP/HoareT.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/HoareT.thy Fri May 17 08:19:52 2013 +0200
@@ -22,7 +22,7 @@
where
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}" |
Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}" |
-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}" |
+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:
@@ -56,9 +56,9 @@
abbreviation "w n ==
WHILE Less (V ''y'') (N n)
- DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
+ 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}}"
+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 Seq)
prefer 2
apply(rule While'
@@ -112,7 +112,7 @@
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))"
by(auto intro!: ext simp: wpt_def)
-lemma [simp]: "wp\<^sub>t (c\<^isub>1;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"
+lemma [simp]: "wp\<^sub>t (c\<^isub>1;;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)"
unfolding wpt_def
apply(rule ext)
apply auto
--- a/src/HOL/IMP/Hoare_Examples.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy Fri May 17 08:19:52 2013 +0200
@@ -9,7 +9,7 @@
abbreviation "w n ==
WHILE Less (V ''y'') (N n)
- DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
+ DO ( ''y'' ::= Plus (V ''y'') (N 1);; ''x'' ::= Plus (V ''x'') (V ''y'') )"
text{* For this example we make use of some predefined functions. Function
@{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The
@@ -37,7 +37,7 @@
Now we prefix the loop with the necessary initialization: *}
lemma sum_via_bigstep:
-assumes "(''x'' ::= N 0; ''y'' ::= N 0; w n, s) \<Rightarrow> t"
+assumes "(''x'' ::= N 0;; ''y'' ::= N 0;; w n, s) \<Rightarrow> t"
shows "t ''x'' = \<Sum> {1 .. n}"
proof -
from assms have "(w n,s(''x'':=0,''y'':=0)) \<Rightarrow> t" by auto
@@ -50,7 +50,7 @@
text{* Note that we deal with sequences of commands from right to left,
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}}"
+lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0;; ''y'' ::= N 0;; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
apply(rule hoare.Seq)
prefer 2
apply(rule While'
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Fri May 17 08:19:52 2013 +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_Seq[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]:
@@ -45,11 +45,11 @@
lemma wp_While_If:
"wp (WHILE b DO c) Q s =
- wp (IF b THEN c;WHILE b DO c ELSE SKIP) Q s"
+ wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
unfolding wp_def by (metis unfold_while)
lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
- wp (WHILE b DO c) Q s = wp (c; WHILE b DO c) Q s"
+ wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s"
by(simp add: wp_While_If)
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
--- a/src/HOL/IMP/Live.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Live.thy Fri May 17 08:19:52 2013 +0200
@@ -10,25 +10,25 @@
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
"L SKIP X = X" |
"L (x ::= a) X = vars a \<union> (X - {x})" |
-"L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
+"L (c\<^isub>1;; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
"L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
-value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
+value "show (L (''y'' ::= V ''z'';; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
fun "kill" :: "com \<Rightarrow> vname set" where
"kill SKIP = {}" |
"kill (x ::= a) = {x}" |
-"kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
+"kill (c\<^isub>1;; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
"kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
"kill (WHILE b DO c) = {}"
fun gen :: "com \<Rightarrow> vname set" where
"gen SKIP = {}" |
"gen (x ::= a) = vars a" |
-"gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
+"gen (c\<^isub>1;; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
"gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
"gen (WHILE b DO c) = vars b \<union> gen c"
@@ -110,7 +110,7 @@
fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
"bury SKIP X = SKIP" |
"bury (x ::= a) X = (if x \<in> X then x ::= a else SKIP)" |
-"bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
+"bury (c\<^isub>1;; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X);; bury c\<^isub>2 X)" |
"bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
"bury (WHILE b DO c) X = WHILE b DO bury c (L (WHILE b DO c) X)"
@@ -182,8 +182,8 @@
lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
by (cases c) auto
-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))"
+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
lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
@@ -205,7 +205,7 @@
by (auto simp: ball_Un)
next
case (Seq bc1 s1 s2 bc2 s3 c X t1)
- then obtain c1 c2 where c: "c = c1;c2"
+ 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 = Seq.hyps(2,4)
from IH(1)[OF bc1, of t1] Seq.prems c obtain t2 where
--- a/src/HOL/IMP/Live_True.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Live_True.thy Fri May 17 08:19:52 2013 +0200
@@ -9,7 +9,7 @@
fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
"L SKIP X = X" |
"L (x ::= a) X = (if x \<in> X then vars a \<union> (X - {x}) else X)" |
-"L (c\<^isub>1; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
+"L (c\<^isub>1;; c\<^isub>2) X = L c\<^isub>1 (L c\<^isub>2 X)" |
"L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
"L (WHILE b DO c) X = lfp(\<lambda>Y. vars b \<union> X \<union> L c Y)"
@@ -154,7 +154,7 @@
text{* Sorry, this syntax is odd. *}
text{* A test: *}
-lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x''; ''x'' ::= V ''z''
+lemma "(let b = Less (N 0) (V ''y''); c = ''y'' ::= V ''x'';; ''x'' ::= V ''z''
in L (WHILE b DO c) {''y''}) = {''x'', ''y'', ''z''}"
by eval
@@ -173,12 +173,12 @@
fun Lb :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
"Lb SKIP X = X" |
"Lb (x ::= a) X = (if x \<in> X then X - {x} \<union> vars a else X)" |
-"Lb (c\<^isub>1; c\<^isub>2) X = (Lb c\<^isub>1 \<circ> Lb c\<^isub>2) X" |
+"Lb (c\<^isub>1;; c\<^isub>2) X = (Lb c\<^isub>1 \<circ> Lb c\<^isub>2) X" |
"Lb (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> Lb c\<^isub>1 X \<union> Lb c\<^isub>2 X" |
"Lb (WHILE b DO c) X = iter (\<lambda>A. vars b \<union> X \<union> Lb c A) 2 {} (vars b \<union> vars c \<union> X)"
text{* @{const Lb} (and @{const iter}) is not monotone! *}
-lemma "let w = WHILE Bc False DO (''x'' ::= V ''y''; ''z'' ::= V ''x'')
+lemma "let w = WHILE Bc False DO (''x'' ::= V ''y'';; ''z'' ::= V ''x'')
in \<not> (Lb w {''z''} \<subseteq> Lb w {''y'',''z''})"
by eval
--- a/src/HOL/IMP/Poly_Types.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Poly_Types.thy Fri May 17 08:19:52 2013 +0200
@@ -26,7 +26,7 @@
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>p" 50) where
"\<Gamma> \<turnstile>p SKIP" |
"\<Gamma> \<turnstile>p a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile>p x ::= a" |
-"\<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p c1;c2" |
+"\<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p c1;;c2" |
"\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p IF b THEN c1 ELSE c2" |
"\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c \<Longrightarrow> \<Gamma> \<turnstile>p WHILE b DO c"
--- a/src/HOL/IMP/Procs.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Procs.thy Fri May 17 08:19:52 2013 +0200
@@ -9,20 +9,20 @@
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
- | Seq 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 _;;/ _})")
- | Proc pname com com ("(1{PROC _ = _;;/ _})")
+ | Var vname com ("(1{VAR _;/ _})")
+ | Proc pname com com ("(1{PROC _ = _;/ _})")
| CALL pname
definition "test_com =
-{VAR ''x'';;
- {PROC ''p'' = ''x'' ::= N 1;;
- {PROC ''q'' = CALL ''p'';;
- {VAR ''x'';;
- ''x'' ::= N 2;
- {PROC ''p'' = ''x'' ::= N 3;;
- CALL ''q''; ''y'' ::= V ''x''}}}}}"
+{VAR ''x'';
+ {PROC ''p'' = ''x'' ::= N 1;
+ {PROC ''q'' = CALL ''p'';
+ {VAR ''x'';
+ ''x'' ::= N 2;;
+ {PROC ''p'' = ''x'' ::= N 3;
+ CALL ''q'';; ''y'' ::= V ''x''}}}}}"
end
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Fri May 17 08:19:52 2013 +0200
@@ -11,7 +11,7 @@
Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
Assign: "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
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" |
+ 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>
pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
@@ -23,11 +23,11 @@
"\<lbrakk> bval b s\<^isub>1; pe \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2; pe \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
pe \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
-Var: "pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(x := s x)" |
+Var: "pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({VAR x; c}, s) \<Rightarrow> t(x := s x)" |
Call: "pe \<turnstile> (pe p, s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
-Proc: "pe(p := cp) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
+Proc: "pe(p := cp) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp; c}, s) \<Rightarrow> t"
code_pred big_step .
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Fri May 17 08:19:52 2013 +0200
@@ -11,7 +11,7 @@
Skip: "pe \<turnstile> (SKIP,s) \<Rightarrow> s" |
Assign: "pe \<turnstile> (x ::= a,s) \<Rightarrow> s(x := aval a s)" |
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" |
+ 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>
pe \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
@@ -23,13 +23,13 @@
"\<lbrakk> bval b s\<^isub>1; pe \<turnstile> (c,s\<^isub>1) \<Rightarrow> s\<^isub>2; pe \<turnstile> (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow>
pe \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
-Var: "pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(x := s x)" |
+Var: "pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({VAR x; c}, s) \<Rightarrow> t(x := s x)" |
Call1: "(p,c)#pe \<turnstile> (c, s) \<Rightarrow> t \<Longrightarrow> (p,c)#pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
Call2: "\<lbrakk> p' \<noteq> p; pe \<turnstile> (CALL p, s) \<Rightarrow> t \<rbrakk> \<Longrightarrow>
(p',c)#pe \<turnstile> (CALL p, s) \<Rightarrow> t" |
-Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
+Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp; c}, s) \<Rightarrow> t"
code_pred big_step .
--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Fri May 17 08:19:52 2013 +0200
@@ -18,7 +18,7 @@
Skip: "e \<turnstile> (SKIP,s) \<Rightarrow> s" |
Assign: "(pe,ve,f) \<turnstile> (x ::= a,s) \<Rightarrow> s(ve x := aval a (s o ve))" |
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" |
+ 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>
e \<turnstile> (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" |
@@ -32,7 +32,7 @@
e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow>
- (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t" |
+ (pe,ve,f) \<turnstile> ({VAR x; c}, s) \<Rightarrow> t" |
Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t \<Longrightarrow>
((p,c,ve)#pe,ve',f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
@@ -40,7 +40,7 @@
((p',c,ve')#pe,ve,f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
Proc: "((p,cp,ve)#pe,ve,f) \<turnstile> (c,s) \<Rightarrow> t
- \<Longrightarrow> (pe,ve,f) \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t"
+ \<Longrightarrow> (pe,ve,f) \<turnstile> ({PROC p = cp; c}, s) \<Rightarrow> t"
code_pred big_step .
--- a/src/HOL/IMP/Sec_Typing.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Sec_Typing.thy Fri May 17 08:19:52 2013 +0200
@@ -11,7 +11,7 @@
Assign:
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
Seq:
- "\<lbrakk> l \<turnstile> c\<^isub>1; l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
+ "\<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 b) l \<turnstile> c\<^isub>1; max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
While:
@@ -24,7 +24,7 @@
value "2 \<turnstile> IF Less (V ''x1'') (V ''x'') THEN ''x1'' ::= N 0 ELSE SKIP"
inductive_cases [elim!]:
- "l \<turnstile> x ::= a" "l \<turnstile> c\<^isub>1;c\<^isub>2" "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" "l \<turnstile> WHILE b DO c"
+ "l \<turnstile> x ::= a" "l \<turnstile> c\<^isub>1;;c\<^isub>2" "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" "l \<turnstile> WHILE b DO c"
text{* An important property: anti-monotonicity. *}
@@ -187,7 +187,7 @@
Assign':
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
Seq':
- "\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
+ "\<lbrakk> l \<turnstile>' c\<^isub>1; l \<turnstile>' c\<^isub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' c\<^isub>1;;c\<^isub>2" |
If':
"\<lbrakk> sec 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" |
While':
@@ -221,7 +221,7 @@
Assign2:
"sec x \<ge> sec a \<Longrightarrow> \<turnstile> x ::= a : sec x" |
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 " |
+ "\<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 b \<le> min l\<^isub>1 l\<^isub>2; \<turnstile> c\<^isub>1 : l\<^isub>1; \<turnstile> c\<^isub>2 : l\<^isub>2 \<rbrakk>
\<Longrightarrow> \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2 : min l\<^isub>1 l\<^isub>2" |
--- a/src/HOL/IMP/Sec_TypingT.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Sec_TypingT.thy Fri May 17 08:19:52 2013 +0200
@@ -9,7 +9,7 @@
Assign:
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" |
Seq:
- "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;c\<^isub>2" |
+ "l \<turnstile> c\<^isub>1 \<Longrightarrow> l \<turnstile> c\<^isub>2 \<Longrightarrow> l \<turnstile> c\<^isub>1;;c\<^isub>2" |
If:
"\<lbrakk> max (sec b) l \<turnstile> c\<^isub>1; max (sec b) l \<turnstile> c\<^isub>2 \<rbrakk>
\<Longrightarrow> l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" |
@@ -19,7 +19,7 @@
code_pred (expected_modes: i => i => bool) sec_type .
inductive_cases [elim!]:
- "l \<turnstile> x ::= a" "l \<turnstile> c\<^isub>1;c\<^isub>2" "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" "l \<turnstile> WHILE b DO c"
+ "l \<turnstile> x ::= a" "l \<turnstile> c\<^isub>1;;c\<^isub>2" "l \<turnstile> IF b THEN c\<^isub>1 ELSE c\<^isub>2" "l \<turnstile> WHILE b DO c"
lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c"
@@ -176,7 +176,7 @@
Assign':
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" |
Seq':
- "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;c\<^isub>2" |
+ "l \<turnstile>' c\<^isub>1 \<Longrightarrow> l \<turnstile>' c\<^isub>2 \<Longrightarrow> l \<turnstile>' c\<^isub>1;;c\<^isub>2" |
If':
"\<lbrakk> sec 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" |
While':
--- a/src/HOL/IMP/Sem_Equiv.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy Fri May 17 08:19:52 2013 +0200
@@ -70,7 +70,7 @@
lemma equiv_up_to_seq:
"P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow>
(\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> Q s') \<Longrightarrow>
- P \<Turnstile> (c; d) \<sim> (c'; d')"
+ P \<Turnstile> (c;; d) \<sim> (c';; d')"
by (clarsimp simp: equiv_up_to_def) blast
lemma equiv_up_to_while_lemma:
--- a/src/HOL/IMP/Small_Step.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Small_Step.thy Fri May 17 08:19:52 2013 +0200
@@ -10,14 +10,14 @@
where
Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a 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')" |
+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)" |
While: "(WHILE b DO c,s) \<rightarrow>
- (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+ (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
text_raw{*}%endsnip*}
@@ -30,7 +30,7 @@
code_pred small_step .
values "{(c',map t [''x'',''y'',''z'']) |c' t.
- (''x'' ::= V ''z''; ''y'' ::= V ''x'',
+ (''x'' ::= V ''z'';; ''y'' ::= V ''x'',
<''x'' := 3, ''y'' := 7, ''z'' := 5>) \<rightarrow>* (c',t)}"
@@ -56,7 +56,7 @@
thm SkipE
inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct"
thm AssignE
-inductive_cases SeqE[elim]: "(c1;c2,s) \<rightarrow> ct"
+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"
@@ -72,7 +72,7 @@
subsection "Equivalence with big-step semantics"
-lemma star_seq2: "(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
@@ -82,7 +82,7 @@
lemma seq_comp:
"\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk>
- \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)"
+ \<Longrightarrow> (c1;;c2, s1) \<rightarrow>* (SKIP,s3)"
by(blast intro: star.step star_seq2 star_trans)
text{* The following proof corresponds to one on the board where one would
@@ -97,7 +97,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 seq_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"
@@ -115,20 +115,20 @@
next
fix b c and s::state
assume b: "\<not>bval b s"
- let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP"
+ let ?if = "IF b THEN c;; WHILE b DO c ELSE SKIP"
have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast
moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b)
ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by(metis star.refl star.step)
next
fix b c s s' t
let ?w = "WHILE b DO c"
- let ?if = "IF b THEN c; ?w ELSE SKIP"
+ let ?if = "IF b THEN c;; ?w ELSE SKIP"
assume w: "(?w,s') \<rightarrow>* (SKIP,t)"
assume c: "(c,s) \<rightarrow>* (SKIP,s')"
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 seq_comp[OF c w])
+ moreover have "(?if, s) \<rightarrow> (c;; ?w, s)" by (simp add: b)
+ 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
--- a/src/HOL/IMP/Types.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Types.thy Fri May 17 08:19:52 2013 +0200
@@ -44,7 +44,7 @@
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
- | Seq 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)
@@ -56,13 +56,13 @@
where
Assign: "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
-Seq1: "(SKIP;c,s) \<rightarrow> (c,s)" |
-Seq2: "(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)" |
-While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
+While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"
lemmas small_step_induct = small_step.induct[split_format(complete)]
@@ -95,12 +95,12 @@
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" |
-Seq_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"
inductive_cases [elim!]:
- "\<Gamma> \<turnstile> x ::= a" "\<Gamma> \<turnstile> c1;c2"
+ "\<Gamma> \<turnstile> x ::= a" "\<Gamma> \<turnstile> c1;;c2"
"\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
"\<Gamma> \<turnstile> WHILE b DO c"
--- a/src/HOL/IMP/VC.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/VC.thy Fri May 17 08:19:52 2013 +0200
@@ -10,7 +10,7 @@
datatype acom =
ASKIP |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) |
- Aseq 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)
@@ -42,7 +42,7 @@
fun strip :: "acom \<Rightarrow> com" where
"strip ASKIP = SKIP" |
"strip (Aassign x a) = (x::=a)" |
-"strip (Aseq 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)"
--- a/src/HOL/IMP/Vars.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Vars.thy Fri May 17 08:19:52 2013 +0200
@@ -72,9 +72,9 @@
begin
fun vars_com :: "com \<Rightarrow> vname set" where
-"vars com.SKIP = {}" |
+"vars SKIP = {}" |
"vars (x::=e) = {x} \<union> vars e" |
-"vars (c1;c2) = vars c1 \<union> vars c2" |
+"vars (c1;;c2) = vars c1 \<union> vars c2" |
"vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2" |
"vars (WHILE b DO c) = vars b \<union> vars c"