author | lcp |
Mon, 24 Oct 1994 10:34:28 +0100 | |
changeset 653 | 6eeff82979df |
parent 518 | 4530c45370b4 |
child 658 | 368aa02631d8 |
permissions | -rw-r--r-- |
482 | 1 |
(* Title: ZF/IMP/Com.thy |
2 |
ID: $Id$ |
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 |
Copyright 1994 TUM |
|
5 |
||
511 | 6 |
Arithmetic expressions, Boolean expressions, Commands |
7 |
||
8 |
And their Operational semantics |
|
482 | 9 |
*) |
10 |
||
511 | 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" |
|
653
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
26 |
"@evala" :: "[i,i,i] => o" ("<_,_>/ -a-> _" [0,0,50] 50) |
511 | 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" |
|
653
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
55 |
"@evalb" :: "[i,i,i] => o" ("<_,_>/ -b-> _" [0,0,50] 50) |
511 | 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 |
||
514 | 73 |
type_intrs "bexp.intrs @ \ |
74 |
\ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]" |
|
511 | 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) |
|
653
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
84 |
| semic ("c0:com", "c1:com") ("_; _" [60, 60] 10) |
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
85 |
| while ("b:bexp", "c:com") ("while _ do _" 60) |
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
86 |
| ifc ("b:bexp", "c0:com", "c1:com") ("ifc _ then _ else _" 60) |
511 | 87 |
type_intrs "aexp.intrs" |
88 |
||
653
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
89 |
(*Constructor ";" has low precedence to avoid syntactic ambiguities |
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
90 |
with [| m: nat; x: loc; ... |] ==> ... It usually will need parentheses.*) |
511 | 91 |
|
92 |
(** Execution of commands **) |
|
93 |
consts evalc :: "i" |
|
653
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
94 |
"@evalc" :: "[i,i,i] => o" ("<_,_>/ -c-> _" [0,0,50] 50) |
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
95 |
"assign" :: "[i,i,i] => i" ("_[_'/_]" [95,0,0] 95) |
511 | 96 |
|
97 |
translations |
|
98 |
"<ce,sig> -c-> s" == "<ce,sig,s> : evalc" |
|
99 |
||
100 |
rules |
|
101 |
assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)" |
|
102 |
||
103 |
inductive |
|
104 |
domains "evalc" <= "com * (loc -> nat) * (loc -> nat)" |
|
105 |
intrs |
|
106 |
skip "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma" |
|
107 |
||
108 |
assign "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> \ |
|
109 |
\ <x := a,sigma> -c-> sigma[m/x]" |
|
110 |
||
111 |
semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> \ |
|
112 |
\ <c0 ; c1, sigma> -c-> sigma1" |
|
113 |
||
518 | 114 |
ifc1 "[| b:bexp; c1:com; sigma:loc->nat; \ |
115 |
\ <b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> \ |
|
511 | 116 |
\ <ifc b then c0 else c1, sigma> -c-> sigma1" |
117 |
||
518 | 118 |
ifc0 "[| b:bexp; c0:com; sigma:loc->nat; \ |
119 |
\ <b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> \ |
|
511 | 120 |
\ <ifc b then c0 else c1, sigma> -c-> sigma1" |
121 |
||
122 |
while0 "[| c: com; <b, sigma> -b-> 0 |] ==> \ |
|
123 |
\ <while b do c,sigma> -c-> sigma " |
|
124 |
||
125 |
while1 "[| c : com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; \ |
|
126 |
\ <while b do c, sigma2> -c-> sigma1 |] ==> \ |
|
127 |
\ <while b do c, sigma> -c-> sigma1 " |
|
128 |
||
129 |
con_defs "[assign_def]" |
|
130 |
type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]" |
|
514 | 131 |
type_elims "[make_elim(evala.dom_subset RS subsetD), \ |
132 |
\ make_elim(evalb.dom_subset RS subsetD) ]" |
|
511 | 133 |
|
134 |
end |