3 Author: Ole Rasmussen |
3 Author: Ole Rasmussen |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 Logic Image: ZF |
5 Logic Image: ZF |
6 *) |
6 *) |
7 |
7 |
8 Reduction = Terms+ |
8 theory Reduction = Residuals: |
|
9 |
|
10 (**** Lambda-terms ****) |
9 |
11 |
10 consts |
12 consts |
11 Sred1, Sred, Spar_red1,Spar_red :: i |
13 lambda :: "i" |
12 "-1->","--->","=1=>", "===>" :: [i,i]=>o (infixl 50) |
14 unmark :: "i=>i" |
|
15 Apl :: "[i,i]=>i" |
13 |
16 |
14 translations |
17 translations |
15 "a -1-> b" == "<a,b>:Sred1" |
18 "Apl(n,m)" == "App(0,n,m)" |
16 "a ---> b" == "<a,b>:Sred" |
19 |
17 "a =1=> b" == "<a,b>:Spar_red1" |
20 inductive |
18 "a ===> b" == "<a,b>:Spar_red" |
21 domains "lambda" <= "redexes" |
|
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" |
19 |
87 |
20 |
88 |
21 inductive |
89 inductive |
22 domains "Sred1" <= "lambda*lambda" |
90 domains "Sred1" <= "lambda*lambda" |
23 intrs |
91 intros |
24 beta "[|m \\<in> lambda; n \\<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m" |
92 beta: "[|m \<in> lambda; n \<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m" |
25 rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)" |
93 rfun: "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)" |
26 apl_l "[|m2 \\<in> lambda; m1 -1-> n1|] ==> |
94 apl_l: "[|m2 \<in> lambda; m1 -1-> n1|] ==> Apl(m1,m2) -1-> Apl(n1,m2)" |
27 Apl(m1,m2) -1-> Apl(n1,m2)" |
95 apl_r: "[|m1 \<in> lambda; m2 -1-> n2|] ==> Apl(m1,m2) -1-> Apl(m1,n2)" |
28 apl_r "[|m1 \\<in> lambda; m2 -1-> n2|] ==> |
96 type_intros red_typechecks |
29 Apl(m1,m2) -1-> Apl(m1,n2)" |
97 |
30 type_intrs "red_typechecks" |
98 declare Sred1.intros [intro, simp] |
31 |
99 |
32 inductive |
100 inductive |
33 domains "Sred" <= "lambda*lambda" |
101 domains "Sred" <= "lambda*lambda" |
34 intrs |
102 intros |
35 one_step "[|m-1->n|] ==> m--->n" |
103 one_step: "m-1->n ==> m--->n" |
36 refl "m \\<in> lambda==>m --->m" |
104 refl: "m \<in> lambda==>m --->m" |
37 trans "[|m--->n; n--->p|]==>m--->p" |
105 trans: "[|m--->n; n--->p|] ==>m--->p" |
38 type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks" |
106 type_intros Sred1.dom_subset [THEN subsetD] red_typechecks |
|
107 |
|
108 declare Sred.one_step [intro, simp] |
|
109 declare Sred.refl [intro, simp] |
39 |
110 |
40 inductive |
111 inductive |
41 domains "Spar_red1" <= "lambda*lambda" |
112 domains "Spar_red1" <= "lambda*lambda" |
42 intrs |
113 intros |
43 beta "[|m =1=> m'; |
114 beta: "[|m =1=> m'; n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'" |
44 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'" |
115 rvar: "n \<in> nat ==> Var(n) =1=> Var(n)" |
45 rvar "n \\<in> nat==> Var(n) =1=> Var(n)" |
116 rfun: "m =1=> m' ==> Fun(m) =1=> Fun(m')" |
46 rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')" |
117 rapl: "[|m =1=> m'; n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')" |
47 rapl "[|m =1=> m'; |
118 type_intros red_typechecks |
48 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')" |
119 |
49 type_intrs "red_typechecks" |
120 declare Spar_red1.intros [intro, simp] |
50 |
121 |
51 inductive |
122 inductive |
52 domains "Spar_red" <= "lambda*lambda" |
123 domains "Spar_red" <= "lambda*lambda" |
53 intrs |
124 intros |
54 one_step "[|m =1=> n|] ==> m ===> n" |
125 one_step: "m =1=> n ==> m ===> n" |
55 trans "[|m===>n; n===>p|]==>m===>p" |
126 trans: "[|m===>n; n===>p|] ==> m===>p" |
56 type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks" |
127 type_intros Spar_red1.dom_subset [THEN subsetD] red_typechecks |
57 |
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) |
|
159 apply (rule_tac [3] Sred.trans) |
|
160 apply simp_all |
|
161 done |
|
162 |
|
163 lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)" |
|
164 apply (erule Sred.induct) |
|
165 apply (rule_tac [3] Sred.trans) |
|
166 apply simp_all |
|
167 done |
|
168 |
|
169 lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')" |
|
170 apply (erule Sred.induct) |
|
171 apply (rule_tac [3] Sred.trans) |
|
172 apply simp_all |
|
173 done |
|
174 |
|
175 lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')" |
|
176 apply (rule_tac n = "Apl (m',n) " in Sred.trans) |
|
177 apply (simp_all add: red_Apll red_Aplr) |
|
178 done |
|
179 |
|
180 lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==> |
|
181 Apl(Fun(m),n)---> n'/m'" |
|
182 apply (rule_tac n = "Apl (Fun (m') ,n') " in Sred.trans) |
|
183 apply (simp_all add: red_Apl red_Fun) |
|
184 done |
|
185 |
|
186 |
|
187 (* ------------------------------------------------------------------------- *) |
|
188 (* Lemmas for parallel reduction *) |
|
189 (* ------------------------------------------------------------------------- *) |
|
190 |
|
191 |
|
192 lemma refl_par_red1: "m \<in> lambda==> m =1=> m" |
|
193 by (erule lambda.induct, simp_all) |
|
194 |
|
195 lemma red1_par_red1: "m-1->n ==> m=1=>n" |
|
196 by (erule Sred1.induct, simp_all add: refl_par_red1) |
|
197 |
|
198 lemma red_par_red: "m--->n ==> m===>n" |
|
199 apply (erule Sred.induct) |
|
200 apply (rule_tac [3] Spar_red.trans) |
|
201 apply (simp_all add: refl_par_red1 red1_par_red1) |
|
202 done |
|
203 |
|
204 lemma par_red_red: "m===>n ==> m--->n" |
|
205 apply (erule Spar_red.induct) |
|
206 apply (erule Spar_red1.induct) |
|
207 apply (rule_tac [5] Sred.trans) |
|
208 apply (simp_all add: red_Fun red_beta red_Apl) |
|
209 done |
|
210 |
|
211 |
|
212 (* ------------------------------------------------------------------------- *) |
|
213 (* Simulation *) |
|
214 (* ------------------------------------------------------------------------- *) |
|
215 |
|
216 lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m~v & regular(v)" |
|
217 by (erule Spar_red1.induct, force+) |
|
218 |
|
219 |
|
220 (* ------------------------------------------------------------------------- *) |
|
221 (* commuting of unmark and subst *) |
|
222 (* ------------------------------------------------------------------------- *) |
|
223 |
|
224 lemma unmmark_lift_rec: |
|
225 "u \<in> redexes ==> \<forall>k \<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)" |
|
226 by (erule redexes.induct, simp_all add: lift_rec_Var) |
|
227 |
|
228 lemma unmmark_subst_rec: |
|
229 "v \<in> redexes ==> \<forall>k \<in> nat. \<forall>u \<in> redexes. |
|
230 unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)" |
|
231 by (erule redexes.induct, simp_all add: unmmark_lift_rec subst_Var) |
|
232 |
|
233 |
|
234 (* ------------------------------------------------------------------------- *) |
|
235 (* Completeness *) |
|
236 (* ------------------------------------------------------------------------- *) |
|
237 |
|
238 lemma completeness_l [rule_format]: |
|
239 "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)" |
|
240 apply (erule Scomp.induct) |
|
241 apply (auto simp add: unmmark_subst_rec) |
|
242 apply (drule_tac psi = "Fun (?u) =1=> ?w" in asm_rl) |
|
243 apply auto |
|
244 done |
|
245 |
|
246 lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)" |
|
247 by (drule completeness_l, simp_all add: lambda_unmark) |
58 |
248 |
59 end |
249 end |
60 |
250 |