src/HOL/Hoare_Parallel/RG_Syntax.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42284 326f57825e1a
child 52143 36ffe23b25f8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13099
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13022
diff changeset
     1
header {* \section{Concrete Syntax} *}
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
15425
6356d2523f73 [ .. (] -> [ ..< ]
nipkow
parents: 13099
diff changeset
     3
theory RG_Syntax
6356d2523f73 [ .. (] -> [ ..< ]
nipkow
parents: 13099
diff changeset
     4
imports RG_Hoare Quote_Antiquote
6356d2523f73 [ .. (] -> [ ..< ]
nipkow
parents: 13099
diff changeset
     5
begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     6
35107
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
     7
abbreviation Skip :: "'a com"  ("SKIP")
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
     8
  where "SKIP \<equiv> Basic id"
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
     9
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
    10
notation Seq  ("(_;;/ _)" [60,61] 60)
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
    11
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
syntax
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    13
  "_Assign"    :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"                     ("(\<acute>_ :=/ _)" [70, 65] 61)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    14
  "_Cond"      :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"   ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    15
  "_Cond2"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0IF _ THEN _ FI)" [0,0] 56)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    16
  "_While"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0WHILE _ /DO _ /OD)"  [0, 0] 61)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    17
  "_Await"     :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"             ("(0AWAIT _ /THEN /_ /END)"  [0,0] 61)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
  "_Atom"      :: "'a com \<Rightarrow> 'a com"                        ("(\<langle>_\<rangle>)" 61)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    19
  "_Wait"      :: "'a bexp \<Rightarrow> 'a com"                       ("(0WAIT _ END)" 61)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    20
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    21
translations
35107
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
    22
  "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>"
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35107
diff changeset
    23
  "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    24
  "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35107
diff changeset
    25
  "WHILE b DO c OD" \<rightharpoonup> "CONST While .{b}. c"
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35107
diff changeset
    26
  "AWAIT b THEN c END" \<rightleftharpoons> "CONST Await .{b}. c"
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35107
diff changeset
    27
  "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    28
  "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    29
41229
d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents: 35145
diff changeset
    30
nonterminal prgs
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    31
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    32
syntax
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    33
  "_PAR"        :: "prgs \<Rightarrow> 'a"              ("COBEGIN//_//COEND" 60)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    34
  "_prg"        :: "'a \<Rightarrow> prgs"              ("_" 57)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    35
  "_prgs"       :: "['a, prgs] \<Rightarrow> prgs"      ("_//\<parallel>//_" [60,57] 57)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    36
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    37
translations
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    38
  "_prg a" \<rightharpoonup> "[a]"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    39
  "_prgs a ps" \<rightharpoonup> "a # ps"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    40
  "_PAR ps" \<rightharpoonup> "ps"
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    41
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    42
syntax
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    43
  "_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs"  ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    44
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    45
translations
34940
3e80eab831a1 explicit CONST in translations
haftmann
parents: 32621
diff changeset
    46
  "_prg_scheme j i k c" \<rightleftharpoons> "(CONST map (\<lambda>i. c) [j..<k])"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    47
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    48
text {* Translations for variables before and after a transition: *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    49
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    50
syntax 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    51
  "_before" :: "id \<Rightarrow> 'a" ("\<ordmasculine>_")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    52
  "_after"  :: "id \<Rightarrow> 'a" ("\<ordfeminine>_")
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    53
 
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    54
translations
35107
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
    55
  "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>CONST fst"
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
    56
  "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>CONST snd"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    57
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    58
print_translation {*
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    59
  let
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    60
    fun quote_tr' f (t :: ts) =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42086
diff changeset
    61
          Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    62
      | quote_tr' _ _ = raise Match;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    63
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35107
diff changeset
    64
    val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    65
35107
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
    66
    fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    67
          quote_tr' (Syntax.const name) (t :: ts)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    68
      | bexp_tr' _ _ = raise Match;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    69
25706
45d090186bbe accomodate to replacement of K_record by %x.c
schirmer
parents: 22759
diff changeset
    70
    fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42086
diff changeset
    71
          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42086
diff changeset
    72
            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    73
      | assign_tr' _ = raise Match;
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    74
  in
35107
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
    75
   [(@{const_syntax Collect}, assert_tr'),
bdca9f765ee4 modernized translations;
wenzelm
parents: 34940
diff changeset
    76
    (@{const_syntax Basic}, assign_tr'),
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35107
diff changeset
    77
    (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35107
diff changeset
    78
    (@{const_syntax While}, bexp_tr' @{syntax_const "_While"})]
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    79
  end
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    80
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    81
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    82
end