--- a/src/ZF/IMP/Com.thy Mon Aug 08 16:45:08 1994 +0200
+++ b/src/ZF/IMP/Com.thy Fri Aug 12 10:20:07 1994 +0200
@@ -3,7 +3,126 @@
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
-Dummy theory merely recording dependence
+Arithmetic expressions, Boolean expressions, Commands
+
+And their Operational semantics
*)
-Com = Bexp
+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-> _")
+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-> _")
+
+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)
+ | ";" ("c0:com", "c1:com") (infixl 60)
+ | while ("b:bexp", "c:com") ("while _ do _" 60)
+ | ifc ("b:bexp", "c0:com", "c1:com") ("ifc _ then _ else _" 60)
+ type_intrs "aexp.intrs"
+
+
+(** Execution of commands **)
+consts evalc :: "i"
+ "@evalc" :: "[i,i,i] => o" ("<_,_>/ -c-> _")
+ "assign" :: "[i,i,i] => i" ("_[_'/_]" [900,0,0] 900)
+
+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 "[| c1: com; <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \
+\ <ifc b then c0 else c1, sigma> -c-> sigma1"
+
+ ifc0 "[| c0 : com; <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