src/ZF/IMP/Com.thy

HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
constructor ";" now yields a low precedence; the reduction relations are
now more like infixes.

(*  Title: 	ZF/IMP/Com.thy
    ID:         $Id$
    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
    Copyright   1994 TUM

Arithmetic expressions, Boolean expressions, Commands

And their Operational semantics
*)

Com = Univ + "Datatype" +

(** Arithmetic expressions **)
consts  loc  :: "i"
        aexp :: "i"

datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
  "aexp" = N ("n: nat")
         | X ("x: loc")
         | Op1 ("f: nat -> nat", "a : aexp")
         | Op2 ("f: (nat*nat) -> nat", "a0 : aexp", "a1 : aexp")


(** Evaluation of arithmetic expressions **)
consts  evala    :: "i"
       "@evala"  :: "[i,i,i] => o"		("<_,_>/ -a-> _"  [0,0,50] 50)
translations
    "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
inductive
  domains "evala" <= "aexp * (loc -> nat) * nat"
  intrs 
    N   "[| n:nat ; sigma:loc->nat |] ==> <N(n),sigma> -a-> n"
    X  	"[| x:loc;  sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x"
    Op1 "[| <e,sigma> -a-> n;  f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n"
    Op2 "[| <e0,sigma> -a-> n0;  <e1,sigma>  -a-> n1; f: (nat*nat) -> nat |] \
\           ==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>"

  type_intrs "aexp.intrs@[apply_funtype]"


(** Boolean expressions **)
consts  bexp :: "i"

datatype <= "univ(aexp Un ((nat*nat)->bool) )"
  "bexp" = true
         | false
         | ROp  ("f: (nat*nat)->bool", "a0 : aexp", "a1 : aexp")
         | noti ("b : bexp")
         | andi ("b0 : bexp", "b1 : bexp")	(infixl 60)
         | ori  ("b0 : bexp", "b1 : bexp")	(infixl 60)


(** Evaluation of boolean expressions **)
consts evalb	:: "i"	
       "@evalb" :: "[i,i,i] => o"		("<_,_>/ -b-> _" [0,0,50] 50)

translations
    "<be,sig> -b-> b" == "<be,sig,b> : evalb"

inductive
  domains "evalb" <= "bexp * (loc -> nat) * bool"
  intrs (*avoid clash with ML constructors true, false*)
    tru   "[| sigma:loc -> nat |] ==> <true,sigma> -b-> 1"
    fls   "[| sigma:loc -> nat |] ==> <false,sigma> -b-> 0"
    ROp   "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] \
\	   ==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> "
    noti  "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)"
    andi  "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
\          ==> <b0 andi b1,sigma> -b-> (w0 and w1)"
    ori   "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
\	    ==> <b0 ori b1,sigma> -b-> (w0 or w1)"

  type_intrs "bexp.intrs @   \
\	      [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
  type_elims "[make_elim(evala.dom_subset RS subsetD)]"


(** Commands **)
consts  com :: "i"

datatype <= "univ(loc Un aexp Un bexp)"
  "com" = skip
        | ":="  ("x:loc", "a:aexp")		(infixl 60)
        | semic ("c0:com", "c1:com")		("_; _"  [60, 60] 10)
	| while ("b:bexp", "c:com")		("while _ do _"  60)
	| ifc   ("b:bexp", "c0:com", "c1:com")	("ifc _ then _ else _"  60)
  type_intrs "aexp.intrs"

(*Constructor ";" has low precedence to avoid syntactic ambiguities
  with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)

(** Execution of commands **)
consts  evalc    :: "i"
        "@evalc" :: "[i,i,i] => o"   		("<_,_>/ -c-> _" [0,0,50] 50)
	"assign" :: "[i,i,i] => i"   		("_[_'/_]"       [95,0,0] 95)

translations
       "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"

rules 
	assign_def	"sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"

inductive
  domains "evalc" <= "com * (loc -> nat) * (loc -> nat)"
  intrs
    skip    "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"

    assign  "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \
\            <x := a,sigma> -c-> sigma[m/x]"

    semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \
\            <c0 ; c1, sigma> -c-> sigma1"

    ifc1     "[| b:bexp; c1:com; sigma:loc->nat;   \
\		 <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
\             <ifc b then c0 else c1, sigma> -c-> sigma1"

    ifc0     "[| b:bexp; c0:com; sigma:loc->nat;   \
\		 <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \
\             <ifc b then c0 else c1, sigma> -c-> sigma1"

    while0   "[| c: com; <b, sigma> -b-> 0 |] ==> \
\             <while b do c,sigma> -c-> sigma "

    while1   "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \
\                <while b do c, sigma2> -c-> sigma1 |] ==> \
\             <while b do c, sigma> -c-> sigma1 "

  con_defs   "[assign_def]"
  type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
  type_elims "[make_elim(evala.dom_subset RS subsetD),   \
\	      make_elim(evalb.dom_subset RS subsetD) ]"

end