src/HOL/Hoare/Hoare.thy
author berghofe
Tue, 25 Jun 1996 13:11:29 +0200
changeset 1824 44254696843a
parent 1558 9c6ebfab4e05
child 2239 8f9007a2f165
permissions -rw-r--r--
Changed argument order of nat_rec.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
     1
(*  Title:      HOL/Hoare/Hoare.thy
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
     3
    Author:     Norbert Galm & Tobias Nipkow
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TUM
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     5
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     6
Sugared semantic embedding of Hoare logic.
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     7
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     8
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     9
Hoare = Arith +
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    10
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    11
types
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    12
  'a prog                       (* program syntax *)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    13
  pvar = nat                    (* encoding of program variables ( < 26! ) *)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    14
  'a state = pvar => 'a         (* program state *)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    15
  'a exp = 'a state => 'a       (* denotation of expressions *)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    16
  'a bexp = 'a state => bool    (* denotation of boolean expressions *)
1384
007ad29ce6ca removed quotes from types section
clasohm
parents: 1374
diff changeset
    17
  'a com = 'a state => 'a state => bool (* denotation of programs *)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    18
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    19
syntax
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    20
  "@Skip"       :: 'a prog                              ("SKIP")
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    21
  "@Assign"     :: [id, 'a] => 'a prog          ("_ := _")
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    22
  "@Seq"        :: ['a prog, 'a prog] => 'a prog        ("_;//_" [0,1000] 999)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    23
  "@If"         :: [bool, 'a prog, 'a prog] => 'a prog
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    24
                   ("IF _//THEN//  (_)//ELSE//  (_)//END")
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    25
  "@While"      :: [bool, bool, 'a prog] => 'a prog
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    26
                   ("WHILE _//DO {_}//  (_)//END")
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    27
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    28
  "@Spec"       :: [bool, 'a prog, bool] => bool        ("{_}//_//{_}")
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    29
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    30
constdefs
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    31
  (* denotational semantics *)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    32
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    33
  Skip          :: 'a com
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    34
  "Skip s s' == (s=s')"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    35
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    36
  Assign        :: [pvar, 'a exp] => 'a com
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    37
  "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    38
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    39
  Seq           :: ['a com, 'a com] => 'a com
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    40
  "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    41
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    42
  Cond          :: ['a bexp, 'a com, 'a com] => 'a com
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    43
  "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    44
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    45
  While         :: ['a bexp, 'a bexp, 'a com] => 'a com
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    46
  "While b inv c s s' == ? n. Iter n b c s s'"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    47
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    48
  Iter          :: [nat, 'a bexp, 'a com] => 'a com
1824
44254696843a Changed argument order of nat_rec.
berghofe
parents: 1558
diff changeset
    49
  "Iter n b c == nat_rec (%s s'.~b(s) & (s=s'))
44254696843a Changed argument order of nat_rec.
berghofe
parents: 1558
diff changeset
    50
             (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s') n"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    51
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    52
  Spec          :: ['a bexp, 'a com, 'a bexp] => bool
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1476
diff changeset
    53
  "Spec p c q == !s s'. c s s' --> p s --> q s'"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    54
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    55
end
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    56
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    57
ML
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    58
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    59
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    60
(*** term manipulation ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    61
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    62
(* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante,
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    63
   freie Var., scheme-Variable oder als Name fuer eine Lambda-Abstraktion vorkommt *)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    64
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    65
fun name_in_term (name,Const (s,t))     =(name=s)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    66
  | name_in_term (name,Free (s,t))      =(name=s)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    67
  | name_in_term (name,Var ((s,i),t))   =(name=s ^ makestring i)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    68
  | name_in_term (name,Abs (s,t,trm))   =(name=s) orelse (name_in_term (name,trm))
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    69
  | name_in_term (name,trm1 $ trm2)     =(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    70
  | name_in_term (_,_)                  =false;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    71
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    72
(* variant_name:string (name:string,trm:term) liefert einen von name abgewandelten Namen (durch Anhaengen
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    73
   von genuegend vielen "_"), der nicht in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    74
   auch Namen von scheme-Variablen und von Lambda-Abstraktionen in trm *)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    75
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    76
fun variant_name (name,trm)     =if name_in_term (name,trm)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    77
                                        then variant_name (name ^ "_",trm)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    78
                                        else name;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    79
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    80
(* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    81
trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    82
wurden *)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    83
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    84
fun subst_term (von,nach,Abs (s,t,trm)) =if von=Abs (s,t,trm)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    85
                                                then nach
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    86
                                                else Abs (s,t,subst_term (von,nach,trm))
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    87
  | subst_term (von,nach,trm1 $ trm2)   =if von=trm1 $ trm2
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    88
                                                then nach
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    89
                                                else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    90
  | subst_term (von,nach,trm)           =if von=trm
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    91
                                                then nach
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    92
                                                else trm;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    93
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    94
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    95
(* Translation between program vars ("a" - "z") and their encoding as
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    96
   natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    97
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
    98
fun is_pvarID s = size s=1 andalso "a"<=s andalso s<="z";
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    99
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   100
fun pvarID2pvar s =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   101
  let fun rest2pvar (i,arg) =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   102
            if i=0 then arg else rest2pvar(i-1, Syntax.const "Suc" $ arg)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   103
  in rest2pvar(ord s - ord "a", Syntax.const "0") end;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   104
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   105
fun pvar2pvarID trm     =
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   106
        let
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   107
                fun rest2pvarID (Const("0",_),i)                =chr (i + ord "a")
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   108
                  | rest2pvarID (Const("Suc",_) $ trm,i)        =rest2pvarID (trm,i+1)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   109
        in
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   110
                rest2pvarID (trm,0)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   111
        end;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   112
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   113
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   114
(*** parse translations: syntax -> semantics ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   115
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   116
(* term_tr:term (name:string,trm:term) ersetzt in trm alle freien Variablen, die eine pvarID
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   117
   darstellen, durch name $ pvarID2pvar(pvarID). Beispiel:
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   118
   bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   119
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   120
fun term_tr (name,Free (s,t)) = if is_pvarID s
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   121
                                then Syntax.free name $ pvarID2pvar s
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   122
                                else Free (s,t)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   123
  | term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm))
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   124
  | term_tr (name,trm1 $ trm2)  = term_tr (name,trm1) $ term_tr (name,trm2)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   125
  | term_tr (name,trm) = trm;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   126
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   127
fun bool_tr B =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   128
  let val name = variant_name("s",B)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   129
  in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,B))) end;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   130
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   131
fun exp_tr E =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   132
  let val name = variant_name("s",E)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   133
  in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   134
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   135
fun prog_tr (Const ("@Skip",_)) = Syntax.const "Skip"
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   136
  | prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   137
      if is_pvarID V
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   138
      then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   139
      else error("Not a valid program variable: " ^ quote V)
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   140
  | prog_tr (Const ("@Seq",_) $ C $ C') =
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   141
      Syntax.const "Seq" $ prog_tr C $ prog_tr C'
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   142
  | prog_tr (Const ("@If",_) $ B $ C $ C') =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   143
      Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C'
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   144
  | prog_tr (Const ("@While",_) $ B $ INV $ C) =
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   145
      Syntax.const "While" $ bool_tr B $ bool_tr INV $ prog_tr C;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   146
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   147
fun spec_tr [P,C,Q] = Syntax.const "Spec" $ bool_tr P $ prog_tr C $ bool_tr Q;
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   148
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   149
val parse_translation = [("@Spec",spec_tr)];
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   150
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   151
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   152
(*** print translations: semantics -> syntax ***)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   153
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   154
(* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   155
   entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   156
        bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   157
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   158
fun term_tr' (name,Free (s,t) $ trm)    =if name=s
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   159
                                                then Syntax.free (pvar2pvarID trm)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   160
                                                else Free (s,t) $ term_tr' (name,trm)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   161
  | term_tr' (name,Abs (s,t,trm))       =Abs (s,t,term_tr' (name,trm))
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   162
  | term_tr' (name,trm1 $ trm2)         =term_tr' (name,trm1) $ term_tr' (name,trm2)
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   163
  | term_tr' (name,trm)                 =trm;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   164
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   165
fun bexp_tr' (Abs(_,_,b))       =term_tr' (variant_abs ("s",dummyT,b));
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   166
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   167
fun exp_tr' (Abs(_,_,e))        =term_tr' (variant_abs ("s",dummyT,e));
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   168
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   169
fun com_tr' (Const ("Skip",_))                  =Syntax.const "@Skip"
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   170
  | com_tr' (Const ("Assign",_) $ v $ e)                =Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   171
  | com_tr' (Const ("Seq",_) $ c $ c')          =Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   172
  | com_tr' (Const ("Cond",_) $ b $ c $ c')             =Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   173
  | com_tr' (Const ("While",_) $ b $ inv $ c)   =Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   174
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   175
fun spec_tr' [p,c,q]            =Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
   176
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1384
diff changeset
   177
val print_translation   =[("Spec",spec_tr')];