--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Thu Feb 11 09:14:34 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Thu Feb 11 13:54:53 2010 +0100
@@ -5,18 +5,25 @@
text{* Syntax for commands and for assertions and boolean expressions in
commands @{text com} and annotated commands @{text ann_com}. *}
+abbreviation Skip :: "'a com" ("SKIP" 63)
+ where "SKIP \<equiv> Basic id"
+
+abbreviation AnnSkip :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63)
+ where "r SKIP \<equiv> AnnBasic r id"
+
+notation
+ Seq ("_,,/ _" [55, 56] 55) and
+ AnnSeq ("_;;/ _" [60,61] 60)
+
syntax
"_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61)
"_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61)
translations
- "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
- "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
+ "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
+ "r \<acute>x := a" \<rightharpoonup> "CONST AnnBasic r \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
syntax
- "_AnnSkip" :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63)
- "_AnnSeq" :: "'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" ("_;;/ _" [60,61] 60)
-
"_AnnCond1" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com"
("_ //IF _ /THEN _ /ELSE _ /FI" [90,0,0,0] 61)
"_AnnCond2" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com"
@@ -28,8 +35,6 @@
"_AnnAtom" :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a ann_com" ("_//\<langle>_\<rangle>" [90,0] 61)
"_AnnWait" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com" ("_//WAIT _ END" [90,0] 61)
- "_Skip" :: "'a com" ("SKIP" 63)
- "_Seq" :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("_,,/ _" [55, 56] 55)
"_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
"_Cond2" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("IF _ THEN _ FI" [0,0] 56)
@@ -39,20 +44,15 @@
("(0WHILE _ //DO _ /OD)" [0, 0] 61)
translations
- "SKIP" \<rightleftharpoons> "Basic id"
- "c_1,, c_2" \<rightleftharpoons> "Seq c_1 c_2"
-
- "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
+ "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
"IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
"WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c"
"WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
- "r SKIP" \<rightleftharpoons> "AnnBasic r id"
- "c_1;; c_2" \<rightleftharpoons> "AnnSeq c_1 c_2"
- "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "AnnCond1 r .{b}. c1 c2"
- "r IF b THEN c FI" \<rightharpoonup> "AnnCond2 r .{b}. c"
- "r WHILE b INV i DO c OD" \<rightharpoonup> "AnnWhile r .{b}. i c"
- "r AWAIT b THEN c END" \<rightharpoonup> "AnnAwait r .{b}. c"
+ "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST AnnCond1 r .{b}. c1 c2"
+ "r IF b THEN c FI" \<rightharpoonup> "CONST AnnCond2 r .{b}. c"
+ "r WHILE b INV i DO c OD" \<rightharpoonup> "CONST AnnWhile r .{b}. i c"
+ "r AWAIT b THEN c END" \<rightharpoonup> "CONST AnnAwait r .{b}. c"
"r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT True THEN c END"
"r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END"
@@ -68,11 +68,11 @@
("SCHEME [_ \<le> _ < _] _// _" [0,0,0,60, 90] 57)
translations
- "_prg c q" \<rightleftharpoons> "[(Some c, q)]"
- "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps"
- "_PAR ps" \<rightleftharpoons> "Parallel ps"
+ "_prg c q" \<rightleftharpoons> "[(CONST Some c, q)]"
+ "_prgs c q ps" \<rightleftharpoons> "(CONST Some c, q) # ps"
+ "_PAR ps" \<rightleftharpoons> "CONST Parallel ps"
- "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]"
+ "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (CONST Some c, q)) [j..<k]"
print_translation {*
let
@@ -86,11 +86,11 @@
val assert_tr' = quote_tr' (Syntax.const "_Assert");
- fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
+ fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
quote_tr' (Syntax.const name) (t :: ts)
| bexp_tr' _ _ = raise Match;
- fun annbexp_tr' name (r :: (Const ("Collect", _) $ t) :: ts) =
+ fun annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) =
annquote_tr' (Syntax.const name) (r :: t :: ts)
| annbexp_tr' _ _ = raise Match;
@@ -105,8 +105,10 @@
| update_name_tr' (Const x) = Const (upd_tr' x)
| update_name_tr' _ = raise Match;
- fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
- | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
+ fun K_tr' (Abs (_, _, t)) =
+ if null (loose_bnos t) then t else raise Match
+ | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
+ if null (loose_bnos t) then t else raise Match
| K_tr' _ = raise Match;
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
@@ -119,22 +121,26 @@
(Abs (x, dummyT, K_tr' k) :: ts)
| annassign_tr' _ = raise Match;
- fun Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1 ) $ t2) $ Const ("Nil",_))] =
- (Syntax.const "_prg" $ t1 $ t2)
- | Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1) $ t2) $ ts)] =
- (Syntax.const "_prgs" $ t1 $ t2 $ Parallel_PAR [ts])
+ fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $
+ (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $
+ Const (@{const_syntax Nil}, _))] = Syntax.const "_prg" $ t1 $ t2
+ | Parallel_PAR [(Const (@{const_syntax Cons}, _) $
+ (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some}, _) $ t1) $ t2) $ ts)] =
+ Syntax.const "_prgs" $ t1 $ t2 $ Parallel_PAR [ts]
| Parallel_PAR _ = raise Match;
-fun Parallel_tr' ts = Syntax.const "_PAR" $ Parallel_PAR ts;
+ fun Parallel_tr' ts = Syntax.const "_PAR" $ Parallel_PAR ts;
in
- [("Collect", assert_tr'), ("Basic", assign_tr'),
- ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv"),
- ("AnnBasic", annassign_tr'),
- ("AnnWhile", annbexp_tr' "_AnnWhile"), ("AnnAwait", annbexp_tr' "_AnnAwait"),
- ("AnnCond1", annbexp_tr' "_AnnCond1"), ("AnnCond2", annbexp_tr' "_AnnCond2")]
-
- end
-
+ [(@{const_syntax Collect}, assert_tr'),
+ (@{const_syntax Basic}, assign_tr'),
+ (@{const_syntax Cond}, bexp_tr' "_Cond"),
+ (@{const_syntax While}, bexp_tr' "_While_inv"),
+ (@{const_syntax AnnBasic}, annassign_tr'),
+ (@{const_syntax AnnWhile}, annbexp_tr' "_AnnWhile"),
+ (@{const_syntax AnnAwait}, annbexp_tr' "_AnnAwait"),
+ (@{const_syntax AnnCond1}, annbexp_tr' "_AnnCond1"),
+ (@{const_syntax AnnCond2}, annbexp_tr' "_AnnCond2")]
+ end;
*}
end
\ No newline at end of file