author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 13612 | 55d32e76ef4e |
child 22808 | a7daa74e2980 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: Reduction.thy |
1048 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Ole Rasmussen |
1048 | 4 |
Copyright 1995 University of Cambridge |
5 |
Logic Image: ZF |
|
6 |
*) |
|
7 |
||
16417 | 8 |
theory Reduction imports Residuals begin |
12593 | 9 |
|
10 |
(**** Lambda-terms ****) |
|
1048 | 11 |
|
12 |
consts |
|
12593 | 13 |
lambda :: "i" |
14 |
unmark :: "i=>i" |
|
15 |
Apl :: "[i,i]=>i" |
|
1048 | 16 |
|
17 |
translations |
|
12593 | 18 |
"Apl(n,m)" == "App(0,n,m)" |
19 |
||
20 |
inductive |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
21 |
domains "lambda" <= redexes |
12593 | 22 |
intros |
23 |
Lambda_Var: " n \<in> nat ==> Var(n) \<in> lambda" |
|
24 |
Lambda_Fun: " u \<in> lambda ==> Fun(u) \<in> lambda" |
|
25 |
Lambda_App: "[|u \<in> lambda; v \<in> lambda|] ==> Apl(u,v) \<in> lambda" |
|
26 |
type_intros redexes.intros bool_typechecks |
|
27 |
||
28 |
declare lambda.intros [intro] |
|
29 |
||
30 |
primrec |
|
31 |
"unmark(Var(n)) = Var(n)" |
|
32 |
"unmark(Fun(u)) = Fun(unmark(u))" |
|
33 |
"unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))" |
|
34 |
||
35 |
||
36 |
declare lambda.intros [simp] |
|
37 |
declare lambda.dom_subset [THEN subsetD, simp, intro] |
|
38 |
||
39 |
||
40 |
(* ------------------------------------------------------------------------- *) |
|
41 |
(* unmark lemmas *) |
|
42 |
(* ------------------------------------------------------------------------- *) |
|
43 |
||
44 |
lemma unmark_type [intro, simp]: |
|
45 |
"u \<in> redexes ==> unmark(u) \<in> lambda" |
|
46 |
by (erule redexes.induct, simp_all) |
|
47 |
||
48 |
lemma lambda_unmark: "u \<in> lambda ==> unmark(u) = u" |
|
49 |
by (erule lambda.induct, simp_all) |
|
50 |
||
51 |
||
52 |
(* ------------------------------------------------------------------------- *) |
|
53 |
(* lift and subst preserve lambda *) |
|
54 |
(* ------------------------------------------------------------------------- *) |
|
55 |
||
56 |
lemma liftL_type [rule_format]: |
|
57 |
"v \<in> lambda ==> \<forall>k \<in> nat. lift_rec(v,k) \<in> lambda" |
|
58 |
by (erule lambda.induct, simp_all add: lift_rec_Var) |
|
59 |
||
60 |
lemma substL_type [rule_format, simp]: |
|
61 |
"v \<in> lambda ==> \<forall>n \<in> nat. \<forall>u \<in> lambda. subst_rec(u,v,n) \<in> lambda" |
|
62 |
by (erule lambda.induct, simp_all add: liftL_type subst_Var) |
|
63 |
||
64 |
||
65 |
(* ------------------------------------------------------------------------- *) |
|
66 |
(* type-rule for reduction definitions *) |
|
67 |
(* ------------------------------------------------------------------------- *) |
|
68 |
||
69 |
lemmas red_typechecks = substL_type nat_typechecks lambda.intros |
|
70 |
bool_typechecks |
|
71 |
||
72 |
consts |
|
73 |
Sred1 :: "i" |
|
74 |
Sred :: "i" |
|
75 |
Spar_red1 :: "i" |
|
76 |
Spar_red :: "i" |
|
77 |
"-1->" :: "[i,i]=>o" (infixl 50) |
|
78 |
"--->" :: "[i,i]=>o" (infixl 50) |
|
79 |
"=1=>" :: "[i,i]=>o" (infixl 50) |
|
80 |
"===>" :: "[i,i]=>o" (infixl 50) |
|
81 |
||
82 |
translations |
|
83 |
"a -1-> b" == "<a,b> \<in> Sred1" |
|
84 |
"a ---> b" == "<a,b> \<in> Sred" |
|
85 |
"a =1=> b" == "<a,b> \<in> Spar_red1" |
|
86 |
"a ===> b" == "<a,b> \<in> Spar_red" |
|
1048 | 87 |
|
88 |
||
89 |
inductive |
|
90 |
domains "Sred1" <= "lambda*lambda" |
|
12593 | 91 |
intros |
92 |
beta: "[|m \<in> lambda; n \<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m" |
|
93 |
rfun: "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)" |
|
94 |
apl_l: "[|m2 \<in> lambda; m1 -1-> n1|] ==> Apl(m1,m2) -1-> Apl(n1,m2)" |
|
95 |
apl_r: "[|m1 \<in> lambda; m2 -1-> n2|] ==> Apl(m1,m2) -1-> Apl(m1,n2)" |
|
96 |
type_intros red_typechecks |
|
97 |
||
98 |
declare Sred1.intros [intro, simp] |
|
1048 | 99 |
|
100 |
inductive |
|
101 |
domains "Sred" <= "lambda*lambda" |
|
12593 | 102 |
intros |
103 |
one_step: "m-1->n ==> m--->n" |
|
104 |
refl: "m \<in> lambda==>m --->m" |
|
105 |
trans: "[|m--->n; n--->p|] ==>m--->p" |
|
106 |
type_intros Sred1.dom_subset [THEN subsetD] red_typechecks |
|
107 |
||
108 |
declare Sred.one_step [intro, simp] |
|
109 |
declare Sred.refl [intro, simp] |
|
1048 | 110 |
|
111 |
inductive |
|
112 |
domains "Spar_red1" <= "lambda*lambda" |
|
12593 | 113 |
intros |
114 |
beta: "[|m =1=> m'; n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'" |
|
115 |
rvar: "n \<in> nat ==> Var(n) =1=> Var(n)" |
|
116 |
rfun: "m =1=> m' ==> Fun(m) =1=> Fun(m')" |
|
117 |
rapl: "[|m =1=> m'; n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')" |
|
118 |
type_intros red_typechecks |
|
119 |
||
120 |
declare Spar_red1.intros [intro, simp] |
|
121 |
||
122 |
inductive |
|
123 |
domains "Spar_red" <= "lambda*lambda" |
|
124 |
intros |
|
125 |
one_step: "m =1=> n ==> m ===> n" |
|
126 |
trans: "[|m===>n; n===>p|] ==> m===>p" |
|
127 |
type_intros Spar_red1.dom_subset [THEN subsetD] red_typechecks |
|
128 |
||
129 |
declare Spar_red.one_step [intro, simp] |
|
130 |
||
131 |
||
132 |
||
133 |
(* ------------------------------------------------------------------------- *) |
|
134 |
(* Setting up rule lists for reduction *) |
|
135 |
(* ------------------------------------------------------------------------- *) |
|
136 |
||
137 |
lemmas red1D1 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD1] |
|
138 |
lemmas red1D2 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD2] |
|
139 |
lemmas redD1 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD1] |
|
140 |
lemmas redD2 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD2] |
|
141 |
||
142 |
lemmas par_red1D1 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD1] |
|
143 |
lemmas par_red1D2 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD2] |
|
144 |
lemmas par_redD1 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD1] |
|
145 |
lemmas par_redD2 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD2] |
|
146 |
||
147 |
declare bool_typechecks [intro] |
|
148 |
||
149 |
inductive_cases [elim!]: "Fun(t) =1=> Fun(u)" |
|
150 |
||
151 |
||
152 |
||
153 |
(* ------------------------------------------------------------------------- *) |
|
154 |
(* Lemmas for reduction *) |
|
155 |
(* ------------------------------------------------------------------------- *) |
|
156 |
||
157 |
lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)" |
|
158 |
apply (erule Sred.induct) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
159 |
apply (rule_tac [3] Sred.trans, simp_all) |
12593 | 160 |
done |
161 |
||
162 |
lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)" |
|
163 |
apply (erule Sred.induct) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
164 |
apply (rule_tac [3] Sred.trans, simp_all) |
12593 | 165 |
done |
166 |
||
167 |
lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')" |
|
168 |
apply (erule Sred.induct) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
169 |
apply (rule_tac [3] Sred.trans, simp_all) |
12593 | 170 |
done |
171 |
||
172 |
lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')" |
|
173 |
apply (rule_tac n = "Apl (m',n) " in Sred.trans) |
|
174 |
apply (simp_all add: red_Apll red_Aplr) |
|
175 |
done |
|
1048 | 176 |
|
12593 | 177 |
lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==> |
178 |
Apl(Fun(m),n)---> n'/m'" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12593
diff
changeset
|
179 |
apply (rule_tac n = "Apl (Fun (m'),n') " in Sred.trans) |
12593 | 180 |
apply (simp_all add: red_Apl red_Fun) |
181 |
done |
|
182 |
||
183 |
||
184 |
(* ------------------------------------------------------------------------- *) |
|
185 |
(* Lemmas for parallel reduction *) |
|
186 |
(* ------------------------------------------------------------------------- *) |
|
187 |
||
188 |
||
189 |
lemma refl_par_red1: "m \<in> lambda==> m =1=> m" |
|
190 |
by (erule lambda.induct, simp_all) |
|
191 |
||
192 |
lemma red1_par_red1: "m-1->n ==> m=1=>n" |
|
193 |
by (erule Sred1.induct, simp_all add: refl_par_red1) |
|
194 |
||
195 |
lemma red_par_red: "m--->n ==> m===>n" |
|
196 |
apply (erule Sred.induct) |
|
197 |
apply (rule_tac [3] Spar_red.trans) |
|
198 |
apply (simp_all add: refl_par_red1 red1_par_red1) |
|
199 |
done |
|
200 |
||
201 |
lemma par_red_red: "m===>n ==> m--->n" |
|
202 |
apply (erule Spar_red.induct) |
|
203 |
apply (erule Spar_red1.induct) |
|
204 |
apply (rule_tac [5] Sred.trans) |
|
205 |
apply (simp_all add: red_Fun red_beta red_Apl) |
|
206 |
done |
|
207 |
||
1048 | 208 |
|
12593 | 209 |
(* ------------------------------------------------------------------------- *) |
210 |
(* Simulation *) |
|
211 |
(* ------------------------------------------------------------------------- *) |
|
212 |
||
213 |
lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m~v & regular(v)" |
|
214 |
by (erule Spar_red1.induct, force+) |
|
215 |
||
216 |
||
217 |
(* ------------------------------------------------------------------------- *) |
|
218 |
(* commuting of unmark and subst *) |
|
219 |
(* ------------------------------------------------------------------------- *) |
|
220 |
||
221 |
lemma unmmark_lift_rec: |
|
222 |
"u \<in> redexes ==> \<forall>k \<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)" |
|
223 |
by (erule redexes.induct, simp_all add: lift_rec_Var) |
|
224 |
||
225 |
lemma unmmark_subst_rec: |
|
226 |
"v \<in> redexes ==> \<forall>k \<in> nat. \<forall>u \<in> redexes. |
|
227 |
unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)" |
|
228 |
by (erule redexes.induct, simp_all add: unmmark_lift_rec subst_Var) |
|
229 |
||
230 |
||
231 |
(* ------------------------------------------------------------------------- *) |
|
232 |
(* Completeness *) |
|
233 |
(* ------------------------------------------------------------------------- *) |
|
234 |
||
235 |
lemma completeness_l [rule_format]: |
|
236 |
"u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)" |
|
237 |
apply (erule Scomp.induct) |
|
238 |
apply (auto simp add: unmmark_subst_rec) |
|
239 |
done |
|
240 |
||
241 |
lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)" |
|
242 |
by (drule completeness_l, simp_all add: lambda_unmark) |
|
1048 | 243 |
|
244 |
end |
|
245 |