# HG changeset patch # User nipkow # Date 1368771592 -7200 # Node ID bc01725d79182d7940057dd5863d6ce66d6bb268 # Parent 90cd3c53a887ceed96ec00c3c97cd2e0d8bfb89e replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/ACom.thy --- 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 \ 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 \ 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 \ 'a) \ com \ '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 \ '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 \ 'b) \ 'a acom \ '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 \ (EX C1 C2. C = C1;C2 & strip C1 = c1 & strip C2 = c2)" + "strip C = c1;;c2 \ (EX C1 C2. C = C1;;C2 & strip C1 = c1 & strip C2 = c2)" by (cases C) simp_all lemma strip_eq_If: diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int0.thy --- 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 \ top_on_acom C2 X)" + "top_on_acom (C1;;C2) X = (top_on_acom C1 X \ top_on_acom C2 X)" "top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X = (top_on_opt P1 X \ top_on_acom C1 X \ top_on_opt P2 X \ top_on_acom C2 X \ top_on_opt Q X)" "top_on_acom ({I} WHILE b DO {P} C {Q}) X = diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int1.thy --- 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 \ top_on_acom C2 X)" + "top_on_acom (C1;;C2) X = (top_on_acom C1 X \ top_on_acom C2 X)" "top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X = (top_on_opt P1 X \ top_on_acom C1 X \ top_on_opt P2 X \ top_on_acom C2 X \ top_on_opt Q X)" "top_on_acom ({I} WHILE b DO {P} C {Q}) X = diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int1_parity.thy --- 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 \) ^^ i) (bot c)" diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy --- 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 \ 'a astate \ '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) \ (AI c2 S)" | "AI (WHILE b DO c) S = pfp (AI c) S" diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy --- 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)" diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy --- 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 \ 'a st \ '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) \ (AI c2 S)" | "AI (WHILE b DO c) S = pfp (AI c) S" diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy --- 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 \ bot | Up S \ 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) \ AI c2 (bfilter b False S)" | "AI (WHILE b DO c) S = diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy --- 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)" diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy --- 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 \'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 \ 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 \ com \ '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 \ '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 \ 'b) \ 'a acom \ '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' \ - (\c1 c2. c = c1;c2 \ map_acom f c1 = c1' \ map_acom f c2 = c2')" + "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 lemma map_acom_If: @@ -97,7 +97,7 @@ by (cases c) simp_all lemma strip_eq_Seq: - "strip c = c1;c2 \ (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)" + "strip c = c1;;c2 \ (EX d1 d2. c = d1;;d2 & strip d1 = c1 & strip d2 = c2)" by (cases c) simp_all lemma strip_eq_If: diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_ITP/Abs_Int0_ITP.thy --- 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 \ 'a acom \ bool" where "le_acom (SKIP {S}) (SKIP {S'}) = (S \ S')" | "le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \ e=e' \ S \ S')" | -"le_acom (c1;c2) (c1';c2') = (le_acom c1 c1' \ le_acom c2 c2')" | +"le_acom (c1;;c2) (c1';;c2') = (le_acom c1 c1' \ le_acom c2 c2')" | "le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) = (b=b' \ le_acom c1 c1' \ le_acom c2 c2' \ S \ S')" | "le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) = @@ -85,7 +85,7 @@ lemma [simp]: "x ::= e {S} \ c \ (\S'. c = x ::= e {S'} \ S \ S')" by (cases c) auto -lemma [simp]: "c1;c2 \ c \ (\c1' c2'. c = c1';c2' \ c1 \ c1' \ c2 \ c2')" +lemma [simp]: "c1;;c2 \ c \ (\c1' c2'. c = c1';;c2' \ c1 \ c1' \ c2 \ c2')" by (cases c) auto lemma [simp]: "IF b THEN c1 ELSE c2 {S} \ c \ @@ -263,7 +263,7 @@ "step' S (SKIP {P}) = (SKIP {S})" | "step' S (x ::= e {P}) = x ::= e {case S of None \ None | Some S \ 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 \ post c2}" | "step' S ({Inv} WHILE b DO c {P}) = diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy --- 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 \ None | Some S \ 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 \ post c2})" | diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy --- 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 \ ^^1) (anno None test2_parity))" diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy --- 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 \ None | Some S \ 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 \ post c2})" | diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy --- 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 \ 'a \ 'a) \ 'a acom \ 'a acom \ '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}) = diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy --- 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 \ 'a acom \ bool" where "(SKIP {S}) \ (SKIP {S'}) = (S \ S')" | "(x ::= e {S}) \ (x' ::= e' {S'}) = (x=x' \ e=e' \ S \ S')" | -"(c1;c2) \ (c1';c2') = (c1 \ c1' \ c2 \ c2')" | +"(c1;;c2) \ (c1';;c2') = (c1 \ c1' \ c2 \ c2')" | "(IF b THEN c1 ELSE c2 {S}) \ (IF b' THEN c1' ELSE c2' {S'}) = (b=b' \ c1 \ c1' \ c2 \ c2' \ S \ S')" | "({Inv} WHILE b DO c {P}) \ ({Inv'} WHILE b' DO c' {P'}) = @@ -30,7 +30,7 @@ lemma Assign_le: "x ::= e {S} \ c \ (\S'. c = x ::= e {S'} \ S \ S')" by (cases c) auto -lemma Seq_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 \ @@ -64,12 +64,12 @@ end fun sub\<^isub>1 :: "'a acom \ '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 \ '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 \ '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. \ bval b s} c2 {post c1 \ post c2}" | diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Abs_Int_Tests.thy --- 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 diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Big_Step.thy --- 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) \ s" | Assign: "(x ::= a,s) \ s(x := aval a s)" | 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" | + (c\<^isub>1;;c\<^isub>2, s\<^isub>1) \ s\<^isub>3" | IfTrue: "\ bval b s; (c\<^isub>1,s) \ t \ \ (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \ t" | @@ -24,7 +24,7 @@ text_raw{*}%endsnip*} text_raw{*\snip{BigStepEx}{1}{2}{% *} -schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \ ?t" +schematic_lemma ex: "(''x'' ::= N 5;; ''y'' ::= V ''x'', s) \ ?t" apply(rule Seq) apply(rule Assign) apply simp @@ -89,7 +89,7 @@ inductive_cases AssignE[elim!]: "(x ::= a,s) \ t" thm AssignE -inductive_cases SeqE[elim!]: "(c1;c2,s1) \ s3" +inductive_cases SeqE[elim!]: "(c1;;c2,s1) \ s3" thm SeqE inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \ t" thm IfE @@ -143,7 +143,7 @@ transformation on programs: *} lemma unfold_while: - "(WHILE b DO c) \ (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \ ?iw") + "(WHILE b DO c) \ (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \ ?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) \ 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 Seq) + hence "(c;; ?w, s) \ t" by (rule Seq) -- "then the whole @{text IF}" with `bval b s` have "(?iw, s) \ 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) \ t` have "(c; ?w, s) \ t" by auto + with `(?iw, s) \ t` have "(c;; ?w, s) \ t" by auto -- "and for this, only the Seq-rule is applicable:" then obtain s' where "(c, s) \ s'" and "(?w, s') \ t" by auto @@ -203,7 +203,7 @@ prove many such facts automatically. *} lemma while_unfold: - "(WHILE b DO c) \ (IF b THEN c; WHILE b DO c ELSE SKIP)" + "(WHILE b DO c) \ (IF b THEN c;; WHILE b DO c ELSE SKIP)" by blast lemma triv_if: diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Collecting.thy --- 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 \ post C2}" | @@ -69,7 +69,7 @@ lemma Assign_le[simp]: "x ::= e {S} \ c \ (\S'. c = x ::= e {S'} \ S \ S')" by (cases c) (auto simp:less_eq_acom_def anno_def) -lemma Seq_le[simp]: "C1;C2 \ C \ (\C1' C2'. C = C1';C2' \ C1 \ C1' \ C2 \ C2')" +lemma Seq_le[simp]: "C1;;C2 \ C \ (\C1' C2'. C = C1';;C2' \ C1 \ C1' \ C2 \ C2')" apply (cases C) apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2) done diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Com.thy --- 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) diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Compiler.thy --- 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 \ 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)" | diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Def_Init.thy --- 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 \ com \ vname set \ bool" where Skip: "D A SKIP A" | Assign: "vars a \ A \ D A (x ::= a) (insert x A)" | -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" | +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" @@ -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'" diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Def_Init_Big.thy --- 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) \ 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))" | -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" | +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 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Def_Init_Small.thy --- 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 \ (x ::= a, s) \ (SKIP, s(x := Some i))" | -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')" | +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)" | -While: "(WHILE b DO c,s) \ (IF b THEN c; WHILE b DO c ELSE SKIP,s)" +While: "(WHILE b DO c,s) \ (IF b THEN c;; WHILE b DO c ELSE SKIP,s)" lemmas small_step_induct = small_step.induct[split_format(complete)] diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Def_Init_Sound_Small.thy --- 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 \ 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 \ 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 diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Denotation.thy --- 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 \ 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) \ C c1 \ bval b s} \ {(s,t). (s,t) \ C c2 \ \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) diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Finite_Reachable.thy --- 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) \(n) (c', t) \ - (\c1' m. c' = c1'; c2 \ (c1, s) \(m) (c1', t) \ m \ n) \ +lemma Seq_stepsnD: "(c1;; c2, s) \(n) (c', t) \ + (\c1' m. c' = c1';; c2 \ (c1, s) \(m) (c1', t) \ m \ n) \ (\s2 m1 m2. (c1,s) \(m1) (SKIP,s2) \ (c2, s2) \(m2) (c', t) \ 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) \ (c12', s')" + from Suc.prems obtain s' c12' where "(c1;;c2, s) \ (c12', s')" and n: "(c12',s') \(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) \ (c1', s'')" - hence n': "(c1';c2,s') \(n) (c',t)" using n by auto + fix c1' s'' assume 1: "(c12', s') = (c1';; c2, s'')" "(c1, s) \ (c1', s'')" + hence n': "(c1';;c2,s') \(n) (c',t)" using n by auto from Suc.IH[OF n'] show ?case proof - assume "\c1'' m. c' = c1''; c2 \ (c1', s') \(m) (c1'', t) \ m \ n" + assume "\c1'' m. c' = c1'';; c2 \ (c1', s') \(m) (c1'', t) \ m \ n" (is "\ a b. ?P a b") then obtain c1'' m where 2: "?P c1'' m" by blast - hence "c' = c1'';c2 \ (c1, s) \(Suc m) (c1'',t) \ Suc m \ Suc n" + hence "c' = c1'';;c2 \ (c1, s) \(Suc m) (c1'',t) \ Suc m \ Suc n" using 1 by auto thus ?case by blast next @@ -80,13 +80,13 @@ qed qed -corollary Seq_starD: "(c1; c2, s) \* (c', t) \ - (\c1'. c' = c1'; c2 \ (c1, s) \* (c1', t)) \ +corollary Seq_starD: "(c1;; c2, s) \* (c', t) \ + (\c1'. c' = c1';; c2 \ (c1, s) \* (c1', t)) \ (\s2. (c1,s) \* (SKIP,s2) \ (c2, s2) \* (c', t))" by(metis Seq_stepsnD star_if_stepsn stepsn_if_star) -lemma reachable_Seq: "reachable (c1;c2) \ - (\c1'. c1';c2) ` reachable c1 \ reachable c2" +lemma reachable_Seq: "reachable (c1;;c2) \ + (\c1'. c1';;c2) ` reachable c1 \ reachable c2" by(auto simp: reachable_def image_def dest!: Seq_starD) @@ -100,8 +100,8 @@ lemma While_stepsnD: "(WHILE b DO c, s) \(n) (c2,t) \ - c2 \ {WHILE b DO c, IF b THEN c ; WHILE b DO c ELSE SKIP, SKIP} - \ (\c1. c2 = c1 ; WHILE b DO c \ (\ s1 s2. (c,s1) \* (c1,s2)))" + c2 \ {WHILE b DO c, IF b THEN c ;; WHILE b DO c ELSE SKIP, SKIP} + \ (\c1. c2 = c1 ;; WHILE b DO c \ (\ s1 s2. (c,s1) \* (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) \(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) \(n3) (c2,t)" by auto + assume "(iw', s') = (c;; WHILE b DO c, s)" + with n3 have "(c;;?w, s) \(n3) (c2,t)" by auto from Seq_stepsnD[OF this] show ?thesis proof - assume "\c1' m. c2 = c1'; ?w \ (c,s) \(m) (c1', t) \ m \ n3" + assume "\c1' m. c2 = c1';; ?w \ (c,s) \(m) (c1', t) \ m \ n3" thus ?thesis by (metis star_if_stepsn) next assume "\s2 m1 m2. (c, s) \(m1) (SKIP, s2) \ @@ -144,8 +144,8 @@ qed lemma reachable_While: "reachable (WHILE b DO c) \ - {WHILE b DO c, IF b THEN c ; WHILE b DO c ELSE SKIP, SKIP} \ - (\c'. c' ; WHILE b DO c) ` reachable c" + {WHILE b DO c, IF b THEN c ;; WHILE b DO c ELSE SKIP, SKIP} \ + (\c'. c' ;; WHILE b DO c) ` reachable c" apply(auto simp: reachable_def image_def) by (metis While_stepsnD insertE singletonE stepsn_if_star) diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Fold.thy --- 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 \ vname set" where "lnames SKIP = {}" | "lnames (x ::= a) = {x}" | -"lnames (c1; c2) = lnames c1 \ lnames c2" | +"lnames (c1;; c2) = lnames c1 \ lnames c2" | "lnames (IF b THEN c1 ELSE c2) = lnames c1 \ 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 \ t(x \ k) | _ \ 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 \ t(x \ k) | _ \ 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 \ bdefs c1 t | Bc False \ 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 \ fold' c1 t | Bc False \ fold' c2 t diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Hoare.thy --- 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: "\ {\s. P(s[a/x])} x::=a {P}" | Seq: "\ \ {P} c\<^isub>1 {Q}; \ {Q} c\<^isub>2 {R} \ - \ \ {P} c\<^isub>1;c\<^isub>2 {R}" | + \ \ {P} c\<^isub>1;;c\<^isub>2 {R}" | If: "\