1 (* Title: ZF/IMP/Com.thy |
1 (* Title: ZF/IMP/Com.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
4 Copyright 1994 TUM |
4 Copyright 1994 TUM |
5 |
5 |
6 Dummy theory merely recording dependence |
6 Arithmetic expressions, Boolean expressions, Commands |
|
7 |
|
8 And their Operational semantics |
7 *) |
9 *) |
8 |
10 |
9 Com = Bexp |
11 Com = Univ + "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-> _") |
|
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-> _") |
|
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 @ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]" |
|
74 type_elims "[make_elim(evala.dom_subset RS subsetD)]" |
|
75 |
|
76 |
|
77 (** Commands **) |
|
78 consts com :: "i" |
|
79 |
|
80 datatype <= "univ(loc Un aexp Un bexp)" |
|
81 "com" = skip |
|
82 | ":=" ("x:loc", "a:aexp") (infixl 60) |
|
83 | ";" ("c0:com", "c1:com") (infixl 60) |
|
84 | while ("b:bexp", "c:com") ("while _ do _" 60) |
|
85 | ifc ("b:bexp", "c0:com", "c1:com") ("ifc _ then _ else _" 60) |
|
86 type_intrs "aexp.intrs" |
|
87 |
|
88 |
|
89 (** Execution of commands **) |
|
90 consts evalc :: "i" |
|
91 "@evalc" :: "[i,i,i] => o" ("<_,_>/ -c-> _") |
|
92 "assign" :: "[i,i,i] => i" ("_[_'/_]" [900,0,0] 900) |
|
93 |
|
94 translations |
|
95 "<ce,sig> -c-> s" == "<ce,sig,s> : evalc" |
|
96 |
|
97 rules |
|
98 assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)" |
|
99 |
|
100 inductive |
|
101 domains "evalc" <= "com * (loc -> nat) * (loc -> nat)" |
|
102 intrs |
|
103 skip "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma" |
|
104 |
|
105 assign "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \ |
|
106 \ <x := a,sigma> -c-> sigma[m/x]" |
|
107 |
|
108 semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \ |
|
109 \ <c0 ; c1, sigma> -c-> sigma1" |
|
110 |
|
111 ifc1 "[| c1: com; <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \ |
|
112 \ <ifc b then c0 else c1, sigma> -c-> sigma1" |
|
113 |
|
114 ifc0 "[| c0 : com; <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \ |
|
115 \ <ifc b then c0 else c1, sigma> -c-> sigma1" |
|
116 |
|
117 while0 "[| c: com; <b, sigma> -b-> 0 |] ==> \ |
|
118 \ <while b do c,sigma> -c-> sigma " |
|
119 |
|
120 while1 "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \ |
|
121 \ <while b do c, sigma2> -c-> sigma1 |] ==> \ |
|
122 \ <while b do c, sigma> -c-> sigma1 " |
|
123 |
|
124 con_defs "[assign_def]" |
|
125 type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]" |
|
126 type_elims "[make_elim(evala.dom_subset RS subsetD), make_elim(evalb.dom_subset RS subsetD) ]" |
|
127 |
|
128 end |