src/HOL/Hoare_Parallel/RG_Syntax.thy
changeset 35107 bdca9f765ee4
parent 34940 3e80eab831a1
child 35113 1a0c129bb2e0
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy	Thu Feb 11 09:14:34 2010 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy	Thu Feb 11 13:54:53 2010 +0100
     1.3 @@ -4,10 +4,13 @@
     1.4  imports RG_Hoare Quote_Antiquote
     1.5  begin
     1.6  
     1.7 +abbreviation Skip :: "'a com"  ("SKIP")
     1.8 +  where "SKIP \<equiv> Basic id"
     1.9 +
    1.10 +notation Seq  ("(_;;/ _)" [60,61] 60)
    1.11 +
    1.12  syntax
    1.13    "_Assign"    :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"                     ("(\<acute>_ :=/ _)" [70, 65] 61)
    1.14 -  "_skip"      :: "'a com"                                  ("SKIP")
    1.15 -  "_Seq"       :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"              ("(_;;/ _)" [60,61] 60)
    1.16    "_Cond"      :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"   ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)
    1.17    "_Cond2"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0IF _ THEN _ FI)" [0,0] 56)
    1.18    "_While"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0WHILE _ /DO _ /OD)"  [0, 0] 61)
    1.19 @@ -16,9 +19,7 @@
    1.20    "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
    1.21  
    1.22  translations
    1.23 -  "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>"
    1.24 -  "SKIP" \<rightleftharpoons> "Basic id"
    1.25 -  "c1;; c2" \<rightleftharpoons> "Seq c1 c2"
    1.26 +  "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
    1.27    "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    1.28    "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
    1.29    "WHILE b DO c OD" \<rightharpoonup> "While .{b}. c"
    1.30 @@ -52,8 +53,8 @@
    1.31    "_after"  :: "id \<Rightarrow> 'a" ("\<ordfeminine>_")
    1.32   
    1.33  translations
    1.34 -  "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>fst"
    1.35 -  "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>snd"
    1.36 +  "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>CONST fst"
    1.37 +  "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>CONST snd"
    1.38  
    1.39  print_translation {*
    1.40    let
    1.41 @@ -63,7 +64,7 @@
    1.42  
    1.43      val assert_tr' = quote_tr' (Syntax.const "_Assert");
    1.44  
    1.45 -    fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
    1.46 +    fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
    1.47            quote_tr' (Syntax.const name) (t :: ts)
    1.48        | bexp_tr' _ _ = raise Match;
    1.49  
    1.50 @@ -78,8 +79,10 @@
    1.51        | update_name_tr' (Const x) = Const (upd_tr' x)
    1.52        | update_name_tr' _ = raise Match;
    1.53  
    1.54 -    fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match
    1.55 -      | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match
    1.56 +    fun K_tr' (Abs (_, _, t)) =
    1.57 +          if null (loose_bnos t) then t else raise Match
    1.58 +      | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
    1.59 +          if null (loose_bnos t) then t else raise Match
    1.60        | K_tr' _ = raise Match;
    1.61  
    1.62      fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
    1.63 @@ -87,8 +90,10 @@
    1.64              (Abs (x, dummyT, K_tr' k) :: ts)
    1.65        | assign_tr' _ = raise Match;
    1.66    in
    1.67 -    [("Collect", assert_tr'), ("Basic", assign_tr'),
    1.68 -      ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
    1.69 +   [(@{const_syntax Collect}, assert_tr'),
    1.70 +    (@{const_syntax Basic}, assign_tr'),
    1.71 +    (@{const_syntax Cond}, bexp_tr' "_Cond"),
    1.72 +    (@{const_syntax While}, bexp_tr' "_While_inv")]
    1.73    end
    1.74  *}
    1.75