src/ZF/IMP/Com.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 1534 e8de1db81559
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/IMP/Com.thy
     2     ID:         $Id$
     3     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     4     Copyright   1994 TUM
     5 
     6 Arithmetic expressions, Boolean expressions, Commands
     7 
     8 And their Operational semantics
     9 *)
    10 
    11 Com = Datatype +
    12 
    13 (** Arithmetic expressions **)
    14 consts  loc  :: i
    15         aexp :: i
    16 
    17 datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
    18   "aexp" = N ("n: nat")
    19          | X ("x: loc")
    20          | Op1 ("f: nat -> nat", "a : aexp")
    21          | Op2 ("f: (nat*nat) -> nat", "a0 : aexp", "a1 : aexp")
    22 
    23 
    24 (** Evaluation of arithmetic expressions **)
    25 consts  evala    :: i
    26        "@evala"  :: [i,i,i] => o                ("<_,_>/ -a-> _"  [0,0,50] 50)
    27 translations
    28     "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
    29 inductive
    30   domains "evala" <= "aexp * (loc -> nat) * nat"
    31   intrs 
    32     N   "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
    33     X   "[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
    34     Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
    35     Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] 
    36            ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"
    37 
    38   type_intrs "aexp.intrs@[apply_funtype]"
    39 
    40 
    41 (** Boolean expressions **)
    42 consts  bexp :: i
    43 
    44 datatype <= "univ(aexp Un ((nat*nat)->bool) )"
    45   "bexp" = true
    46          | false
    47          | ROp  ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
    48          | noti ("b : bexp")
    49          | andi ("b0 : bexp", "b1 : bexp")      (infixl 60)
    50          | ori  ("b0 : bexp", "b1 : bexp")      (infixl 60)
    51 
    52 
    53 (** Evaluation of boolean expressions **)
    54 consts evalb    :: i    
    55        "@evalb" :: [i,i,i] => o         ("<_,_>/ -b-> _" [0,0,50] 50)
    56 
    57 translations
    58     "<be,sig> -b-> b" == "<be,sig,b> : evalb"
    59 
    60 inductive
    61   domains "evalb" <= "bexp * (loc -> nat) * bool"
    62   intrs (*avoid clash with ML constructors true, false*)
    63     tru   "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
    64     fls   "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
    65     ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] 
    66            ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
    67     noti  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
    68     andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
    69           ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
    70     ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] 
    71             ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
    72 
    73   type_intrs "bexp.intrs @   
    74               [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
    75   type_elims "[make_elim(evala.dom_subset RS subsetD)]"
    76 
    77 
    78 (** Commands **)
    79 consts  com :: i
    80 
    81 datatype <= "univ(loc Un aexp Un bexp)"
    82   "com" = skip
    83         | ":="  ("x:loc", "a:aexp")             (infixl 60)
    84         | semic ("c0:com", "c1:com")            ("_; _"  [60, 60] 10)
    85         | while ("b:bexp", "c:com")             ("while _ do _"  60)
    86         | ifc   ("b:bexp", "c0:com", "c1:com")  ("ifc _ then _ else _"  60)
    87 
    88 (*Constructor ";" has low precedence to avoid syntactic ambiguities
    89   with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)
    90 
    91 (** Execution of commands **)
    92 consts  evalc    :: i
    93         "@evalc" :: [i,i,i] => o                ("<_,_>/ -c-> _" [0,0,50] 50)
    94         "assign" :: [i,i,i] => i                ("_[_'/_]"       [95,0,0] 95)
    95 
    96 translations
    97        "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
    98 
    99 defs 
   100         assign_def      "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
   101 
   102 inductive
   103   domains "evalc" <= "com * (loc -> nat) * (loc -> nat)"
   104   intrs
   105     skip    "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"
   106 
   107     assign  "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> 
   108             <x := a,sigma> -c-> sigma[m/x]"
   109 
   110     semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> 
   111             <c0 ; c1, sigma> -c-> sigma1"
   112 
   113     ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   
   114                  <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> 
   115              <ifc b then c0 else c1, sigma> -c-> sigma1"
   116 
   117     ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   
   118                  <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> 
   119              <ifc b then c0 else c1, sigma> -c-> sigma1"
   120 
   121     while0   "[| c: com; <b, sigma> -b-> 0 |] ==> 
   122              <while b do c,sigma> -c-> sigma "
   123 
   124     while1   "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; 
   125                 <while b do c, sigma2> -c-> sigma1 |] ==> 
   126              <while b do c, sigma> -c-> sigma1 "
   127 
   128   con_defs   "[assign_def]"
   129   type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
   130   type_elims "[make_elim(evala.dom_subset RS subsetD),   
   131               make_elim(evalb.dom_subset RS subsetD) ]"
   132 
   133 end