author | paulson |
Mon, 21 May 2001 14:52:04 +0200 | |
changeset 11320 | 56aa53caf333 |
parent 6112 | 5e4871c5136b |
child 12606 | cf1715a5f5ec |
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 |
||
6047
f2e0938ba38d
converted to use new primrec section and update operator
paulson
parents:
1741
diff
changeset
|
11 |
Com = Main + |
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) )" |
|
11320 | 18 |
"aexp" = N ("n \\<in> nat") |
19 |
| X ("x \\<in> loc") |
|
20 |
| Op1 ("f \\<in> nat -> nat", "a \\<in> aexp") |
|
21 |
| Op2 ("f \\<in> (nat*nat) -> nat", "a0 \\<in> aexp", "a1 \\<in> 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 |
11320 | 28 |
"p -a-> n" == "<p,n> \\<in> 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 |
11320 | 32 |
N "[| n \\<in> nat; sigma \\<in> loc->nat |] ==> <N(n),sigma> -a-> n" |
33 |
X "[| x \\<in> loc; sigma \\<in> loc->nat |] ==> <X(x),sigma> -a-> sigma`x" |
|
34 |
Op1 "[| <e,sigma> -a-> n; f \\<in> nat -> nat |] ==> <Op1(f,e),sigma> -a-> f`n" |
|
35 |
Op2 "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \\<in> (nat*nat) -> nat |] |
|
1155 | 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 |
|
11320 | 47 |
| ROp ("f \\<in> (nat*nat)->bool", "a0 \\<in> aexp", "a1 \\<in> aexp") |
48 |
| noti ("b \\<in> bexp") |
|
49 |
| andi ("b0 \\<in> bexp", "b1 \\<in> bexp") (infixl 60) |
|
50 |
| ori ("b0 \\<in> bexp", "b1 \\<in> 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 |
|
11320 | 58 |
"p -b-> b" == "<p,b> \\<in> 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*) |
11320 | 63 |
tru "[| sigma \\<in> loc -> nat |] ==> <true,sigma> -b-> 1" |
64 |
fls "[| sigma \\<in> loc -> nat |] ==> <false,sigma> -b-> 0" |
|
65 |
ROp "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \\<in> (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 |
|
6112 | 81 |
datatype |
511 | 82 |
"com" = skip |
11320 | 83 |
| asgt ("x \\<in> loc", "a \\<in> aexp") (infixl 60) |
84 |
| semic ("c0 \\<in> com", "c1 \\<in> com") ("_; _" [60, 60] 10) |
|
85 |
| while ("b \\<in> bexp", "c \\<in> com") ("while _ do _" 60) |
|
86 |
| ifc ("b \\<in> bexp", "c0 \\<in> com", "c1 \\<in> 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 |
11320 | 89 |
with [| m \\<in> nat; x \\<in> 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) |
511 | 94 |
|
95 |
translations |
|
11320 | 96 |
"p -c-> s" == "<p,s> \\<in> evalc" |
511 | 97 |
|
98 |
||
99 |
inductive |
|
1741
8b3de497b49d
Removed special syntax for -a-> and nested tuples to left
paulson
parents:
1534
diff
changeset
|
100 |
domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)" |
511 | 101 |
intrs |
11320 | 102 |
skip "[| sigma \\<in> loc -> nat |] ==> <skip,sigma> -c-> sigma" |
511 | 103 |
|
11320 | 104 |
assign "[| m \\<in> nat; x \\<in> loc; <a,sigma> -a-> m |] ==> |
6047
f2e0938ba38d
converted to use new primrec section and update operator
paulson
parents:
1741
diff
changeset
|
105 |
<x asgt a,sigma> -c-> sigma(x:=m)" |
511 | 106 |
|
1155 | 107 |
semi "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> |
108 |
<c0 ; c1, sigma> -c-> sigma1" |
|
511 | 109 |
|
11320 | 110 |
ifc1 "[| b \\<in> bexp; c1 \\<in> com; sigma \\<in> loc->nat; |
1478 | 111 |
<b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] ==> |
1155 | 112 |
<ifc b then c0 else c1, sigma> -c-> sigma1" |
511 | 113 |
|
11320 | 114 |
ifc0 "[| b \\<in> bexp; c0 \\<in> com; sigma \\<in> loc->nat; |
1478 | 115 |
<b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] ==> |
1155 | 116 |
<ifc b then c0 else c1, sigma> -c-> sigma1" |
511 | 117 |
|
11320 | 118 |
while0 "[| c \\<in> com; <b, sigma> -b-> 0 |] ==> |
1155 | 119 |
<while b do c,sigma> -c-> sigma " |
511 | 120 |
|
11320 | 121 |
while1 "[| c \\<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; |
1155 | 122 |
<while b do c, sigma2> -c-> sigma1 |] ==> |
123 |
<while b do c, sigma> -c-> sigma1 " |
|
511 | 124 |
|
6047
f2e0938ba38d
converted to use new primrec section and update operator
paulson
parents:
1741
diff
changeset
|
125 |
type_intrs "com.intrs @ [update_type]" |
1155 | 126 |
type_elims "[make_elim(evala.dom_subset RS subsetD), |
6047
f2e0938ba38d
converted to use new primrec section and update operator
paulson
parents:
1741
diff
changeset
|
127 |
make_elim(evalb.dom_subset RS subsetD) ]" |
511 | 128 |
|
129 |
end |