author | wenzelm |
Thu, 03 Jan 2019 21:15:52 +0100 | |
changeset 69587 | 53982d5ec0bb |
parent 65449 | c82e63b11b8b |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/IMP/Com.thy |
40945 | 2 |
Author: Heiko Loetzbeyer and Robert Sandner, TU München |
12610 | 3 |
*) |
482 | 4 |
|
60770 | 5 |
section \<open>Arithmetic expressions, boolean expressions, commands\<close> |
482 | 6 |
|
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
60770
diff
changeset
|
7 |
theory Com imports ZF begin |
511 | 8 |
|
12610 | 9 |
|
60770 | 10 |
subsection \<open>Arithmetic expressions\<close> |
511 | 11 |
|
12610 | 12 |
consts |
13 |
loc :: i |
|
14 |
aexp :: i |
|
15 |
||
16 |
datatype \<subseteq> "univ(loc \<union> (nat -> nat) \<union> ((nat \<times> nat) -> nat))" |
|
17 |
aexp = N ("n \<in> nat") |
|
18 |
| X ("x \<in> loc") |
|
19 |
| Op1 ("f \<in> nat -> nat", "a \<in> aexp") |
|
20 |
| Op2 ("f \<in> (nat \<times> nat) -> nat", "a0 \<in> aexp", "a1 \<in> aexp") |
|
511 | 21 |
|
22 |
||
12610 | 23 |
consts evala :: i |
35068 | 24 |
|
25 |
abbreviation |
|
69587 | 26 |
evala_syntax :: "[i, i] => o" (infixl \<open>-a->\<close> 50) |
35068 | 27 |
where "p -a-> n == <p,n> \<in> evala" |
12610 | 28 |
|
511 | 29 |
inductive |
12610 | 30 |
domains "evala" \<subseteq> "(aexp \<times> (loc -> nat)) \<times> nat" |
31 |
intros |
|
12606 | 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" |
|
12610 | 35 |
Op2: "[| <e0,sigma> -a-> n0; <e1,sigma> -a-> n1; f \<in> (nat\<times>nat) -> nat |] |
12606 | 36 |
==> <Op2(f,e0,e1),sigma> -a-> f`<n0,n1>" |
37 |
type_intros aexp.intros apply_funtype |
|
511 | 38 |
|
39 |
||
60770 | 40 |
subsection \<open>Boolean expressions\<close> |
12610 | 41 |
|
42 |
consts bexp :: i |
|
511 | 43 |
|
12610 | 44 |
datatype \<subseteq> "univ(aexp \<union> ((nat \<times> nat)->bool))" |
45 |
bexp = true |
|
46 |
| false |
|
47 |
| ROp ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp") |
|
48 |
| noti ("b \<in> bexp") |
|
69587 | 49 |
| andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl \<open>andi\<close> 60) |
50 |
| ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl \<open>ori\<close> 60) |
|
511 | 51 |
|
52 |
||
12610 | 53 |
consts evalb :: i |
35068 | 54 |
|
55 |
abbreviation |
|
69587 | 56 |
evalb_syntax :: "[i,i] => o" (infixl \<open>-b->\<close> 50) |
35068 | 57 |
where "p -b-> b == <p,b> \<in> evalb" |
511 | 58 |
|
59 |
inductive |
|
12610 | 60 |
domains "evalb" \<subseteq> "(bexp \<times> (loc -> nat)) \<times> bool" |
61 |
intros |
|
62 |
true: "[| sigma \<in> loc -> nat |] ==> <true,sigma> -b-> 1" |
|
63 |
false: "[| sigma \<in> loc -> nat |] ==> <false,sigma> -b-> 0" |
|
64 |
ROp: "[| <a0,sigma> -a-> n0; <a1,sigma> -a-> n1; f \<in> (nat*nat)->bool |] |
|
1478 | 65 |
==> <ROp(f,a0,a1),sigma> -b-> f`<n0,n1> " |
12606 | 66 |
noti: "[| <b,sigma> -b-> w |] ==> <noti(b),sigma> -b-> not(w)" |
12610 | 67 |
andi: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] |
1155 | 68 |
==> <b0 andi b1,sigma> -b-> (w0 and w1)" |
12610 | 69 |
ori: "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] |
1478 | 70 |
==> <b0 ori b1,sigma> -b-> (w0 or w1)" |
12610 | 71 |
type_intros bexp.intros |
12606 | 72 |
apply_funtype and_type or_type bool_1I bool_0I not_type |
73 |
type_elims evala.dom_subset [THEN subsetD, elim_format] |
|
511 | 74 |
|
75 |
||
60770 | 76 |
subsection \<open>Commands\<close> |
511 | 77 |
|
12610 | 78 |
consts com :: i |
79 |
datatype com = |
|
69587 | 80 |
skip (\<open>\<SKIP>\<close> []) |
81 |
| assignment ("x \<in> loc", "a \<in> aexp") (infixl \<open>\<ASSN>\<close> 60) |
|
82 |
| semicolon ("c0 \<in> com", "c1 \<in> com") (\<open>_\<SEQ> _\<close> [60, 60] 10) |
|
83 |
| while ("b \<in> bexp", "c \<in> com") (\<open>\<WHILE> _ \<DO> _\<close> 60) |
|
84 |
| "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") (\<open>\<IF> _ \<THEN> _ \<ELSE> _\<close> 60) |
|
511 | 85 |
|
86 |
||
12610 | 87 |
consts evalc :: i |
35068 | 88 |
|
89 |
abbreviation |
|
69587 | 90 |
evalc_syntax :: "[i, i] => o" (infixl \<open>-c->\<close> 50) |
35068 | 91 |
where "p -c-> s == <p,s> \<in> evalc" |
511 | 92 |
|
93 |
inductive |
|
12610 | 94 |
domains "evalc" \<subseteq> "(com \<times> (loc -> nat)) \<times> (loc -> nat)" |
12606 | 95 |
intros |
12610 | 96 |
skip: "[| sigma \<in> loc -> nat |] ==> <\<SKIP>,sigma> -c-> sigma" |
12606 | 97 |
|
12610 | 98 |
assign: "[| m \<in> nat; x \<in> loc; <a,sigma> -a-> m |] |
99 |
==> <x \<ASSN> a,sigma> -c-> sigma(x:=m)" |
|
511 | 100 |
|
12610 | 101 |
semi: "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] |
102 |
==> <c0\<SEQ> c1, sigma> -c-> sigma1" |
|
12606 | 103 |
|
12610 | 104 |
if1: "[| b \<in> bexp; c1 \<in> com; sigma \<in> loc->nat; |
105 |
<b,sigma> -b-> 1; <c0,sigma> -c-> sigma1 |] |
|
106 |
==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1" |
|
511 | 107 |
|
12610 | 108 |
if0: "[| b \<in> bexp; c0 \<in> com; sigma \<in> loc->nat; |
109 |
<b,sigma> -b-> 0; <c1,sigma> -c-> sigma1 |] |
|
110 |
==> <\<IF> b \<THEN> c0 \<ELSE> c1, sigma> -c-> sigma1" |
|
12606 | 111 |
|
12610 | 112 |
while0: "[| c \<in> com; <b, sigma> -b-> 0 |] |
113 |
==> <\<WHILE> b \<DO> c,sigma> -c-> sigma" |
|
511 | 114 |
|
12610 | 115 |
while1: "[| c \<in> com; <b,sigma> -b-> 1; <c,sigma> -c-> sigma2; |
116 |
<\<WHILE> b \<DO> c, sigma2> -c-> sigma1 |] |
|
117 |
==> <\<WHILE> b \<DO> c, sigma> -c-> sigma1" |
|
12606 | 118 |
|
119 |
type_intros com.intros update_type |
|
120 |
type_elims evala.dom_subset [THEN subsetD, elim_format] |
|
121 |
evalb.dom_subset [THEN subsetD, elim_format] |
|
122 |
||
123 |
||
60770 | 124 |
subsection \<open>Misc lemmas\<close> |
511 | 125 |
|
12610 | 126 |
lemmas evala_1 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1] |
127 |
and evala_2 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2] |
|
128 |
and evala_3 [simp] = evala.dom_subset [THEN subsetD, THEN SigmaD2] |
|
511 | 129 |
|
12610 | 130 |
lemmas evalb_1 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1] |
131 |
and evalb_2 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2] |
|
132 |
and evalb_3 [simp] = evalb.dom_subset [THEN subsetD, THEN SigmaD2] |
|
511 | 133 |
|
12610 | 134 |
lemmas evalc_1 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD1] |
135 |
and evalc_2 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD1, THEN SigmaD2] |
|
136 |
and evalc_3 [simp] = evalc.dom_subset [THEN subsetD, THEN SigmaD2] |
|
511 | 137 |
|
12610 | 138 |
inductive_cases |
139 |
evala_N_E [elim!]: "<N(n),sigma> -a-> i" |
|
140 |
and evala_X_E [elim!]: "<X(x),sigma> -a-> i" |
|
141 |
and evala_Op1_E [elim!]: "<Op1(f,e),sigma> -a-> i" |
|
142 |
and evala_Op2_E [elim!]: "<Op2(f,a1,a2),sigma> -a-> i" |
|
511 | 143 |
|
144 |
end |