author | paulson |
Thu, 09 May 1996 11:45:53 +0200 | |
changeset 1741 | 8b3de497b49d |
parent 1534 | e8de1db81559 |
child 6047 | f2e0938ba38d |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/IMP/Com.thy |
482 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM |
482 | 4 |
Copyright 1994 TUM |
5 |
||
511 | 6 |
Arithmetic expressions, Boolean expressions, Commands |
7 |
||
8 |
And their Operational semantics |
|
482 | 9 |
*) |
10 |
||
810 | 11 |
Com = Datatype + |
511 | 12 |
|
13 |
(** Arithmetic expressions **) |
|
1401 | 14 |
consts loc :: i |
15 |
aexp :: i |
|
511 | 16 |
|
17 |
datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )" |
|
18 |
"aexp" = N ("n: nat") |
|
19 |
| X ("x: loc") |
|
1534 | 20 |
| Op1 ("f : nat -> nat", "a : aexp") |
21 |
| Op2 ("f : (nat*nat) -> nat", "a0 : aexp", "a1 : aexp") |
|
511 | 22 |
|
23 |
||
24 |
(** Evaluation of arithmetic expressions **) |
|
1401 | 25 |
consts evala :: i |
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
26 |
"-a->" :: [i,i] => o (infixl 50) |
511 | 27 |
translations |
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
28 |
"p -a-> n" == "<p,n> : evala" |
511 | 29 |
inductive |
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
30 |
domains "evala" <= "(aexp * (loc -> nat)) * nat" |
511 | 31 |
intrs |
1534 | 32 |
N "[| n:nat; sigma:loc->nat |] ==> <N(n),sigma> -a-> n" |
1478 | 33 |
X "[| x:loc; sigma:loc->nat |] ==> <X(x),sigma> -a-> sigma`x" |
511 | 34 |
Op1 "[| <e,sigma> -a-> n; f: nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n" |
1155 | 35 |
Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f: (nat*nat) -> nat |] |
36 |
==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>" |
|
511 | 37 |
|
38 |
type_intrs "aexp.intrs@[apply_funtype]" |
|
39 |
||
40 |
||
41 |
(** Boolean expressions **) |
|
1401 | 42 |
consts bexp :: i |
511 | 43 |
|
44 |
datatype <= "univ(aexp Un ((nat*nat)->bool) )" |
|
45 |
"bexp" = true |
|
46 |
| false |
|
1534 | 47 |
| ROp ("f : (nat*nat)->bool", "a0 : aexp", "a1 : aexp") |
511 | 48 |
| noti ("b : bexp") |
1478 | 49 |
| andi ("b0 : bexp", "b1 : bexp") (infixl 60) |
50 |
| ori ("b0 : bexp", "b1 : bexp") (infixl 60) |
|
511 | 51 |
|
52 |
||
53 |
(** Evaluation of boolean expressions **) |
|
1478 | 54 |
consts evalb :: i |
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
55 |
"-b->" :: [i,i] => o (infixl 50) |
511 | 56 |
|
57 |
translations |
|
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
58 |
"p -b-> b" == "<p,b> : evalb" |
511 | 59 |
|
60 |
inductive |
|
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
61 |
domains "evalb" <= "(bexp * (loc -> nat)) * bool" |
511 | 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" |
|
1155 | 65 |
ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f: (nat*nat)->bool |] |
1478 | 66 |
==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> " |
511 | 67 |
noti "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)" |
1155 | 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 |] |
|
1478 | 71 |
==> <b0 ori b1,sigma> -b-> (w0 or w1)" |
511 | 72 |
|
1155 | 73 |
type_intrs "bexp.intrs @ |
1478 | 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 **) |
|
1401 | 79 |
consts com :: i |
511 | 80 |
|
81 |
datatype <= "univ(loc Un aexp Un bexp)" |
|
82 |
"com" = skip |
|
1478 | 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) |
|
511 | 87 |
|
653
6eeff82979df
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
518
diff
changeset
|
88 |
(*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
|
89 |
with [| m: nat; x: loc; ... |] ==> ... It usually will need parentheses.*) |
511 | 90 |
|
91 |
(** Execution of commands **) |
|
1401 | 92 |
consts evalc :: i |
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
93 |
"-c->" :: [i,i] => o (infixl 50) |
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
94 |
"assign" :: [i,i,i] => i ("_[_'/_]" [95,0,0] 95) |
511 | 95 |
|
96 |
translations |
|
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
97 |
"p -c-> s" == "<p,s> : evalc" |
511 | 98 |
|
753 | 99 |
defs |
1478 | 100 |
assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)" |
511 | 101 |
|
102 |
inductive |
|
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
103 |
domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)" |
511 | 104 |
intrs |
105 |
skip "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma" |
|
106 |
||
1155 | 107 |
assign "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> |
108 |
<x := a,sigma> -c-> sigma[m/x]" |
|
511 | 109 |
|
1155 | 110 |
semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> |
111 |
<c0 ; c1, sigma> -c-> sigma1" |
|
511 | 112 |
|
1155 | 113 |
ifc1 "[| b:bexp; c1:com; sigma:loc->nat; |
1478 | 114 |
<b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> |
1155 | 115 |
<ifc b then c0 else c1, sigma> -c-> sigma1" |
511 | 116 |
|
1155 | 117 |
ifc0 "[| b:bexp; c0:com; sigma:loc->nat; |
1478 | 118 |
<b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> |
1155 | 119 |
<ifc b then c0 else c1, sigma> -c-> sigma1" |
511 | 120 |
|
1155 | 121 |
while0 "[| c: com; <b, sigma> -b-> 0 |] ==> |
122 |
<while b do c,sigma> -c-> sigma " |
|
511 | 123 |
|
1155 | 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 " |
|
511 | 127 |
|
128 |
con_defs "[assign_def]" |
|
129 |
type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]" |
|
1155 | 130 |
type_elims "[make_elim(evala.dom_subset RS subsetD), |
1478 | 131 |
make_elim(evalb.dom_subset RS subsetD) ]" |
511 | 132 |
|
133 |
end |