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