9284
|
1 |
(* Title: ZF/Resid/Substitution.thy
|
1048
|
2 |
ID: $Id$
|
1478
|
3 |
Author: Ole Rasmussen
|
1048
|
4 |
Copyright 1995 University of Cambridge
|
|
5 |
Logic Image: ZF
|
|
6 |
*)
|
|
7 |
|
12593
|
8 |
theory Substitution = Redex:
|
1048
|
9 |
|
|
10 |
consts
|
12593
|
11 |
lift_aux :: "i=>i"
|
|
12 |
lift :: "i=>i"
|
|
13 |
subst_aux :: "i=>i"
|
|
14 |
"'/" :: "[i,i]=>i" (infixl 70) (*subst*)
|
6046
|
15 |
|
|
16 |
constdefs
|
12593
|
17 |
lift_rec :: "[i,i]=> i"
|
6046
|
18 |
"lift_rec(r,k) == lift_aux(r)`k"
|
|
19 |
|
12593
|
20 |
subst_rec :: "[i,i,i]=> i" (**NOTE THE ARGUMENT ORDER BELOW**)
|
6046
|
21 |
"subst_rec(u,r,k) == subst_aux(r)`u`k"
|
|
22 |
|
1048
|
23 |
translations
|
|
24 |
"lift(r)" == "lift_rec(r,0)"
|
6046
|
25 |
"u/v" == "subst_rec(u,v,0)"
|
1048
|
26 |
|
6046
|
27 |
|
|
28 |
(** The clumsy _aux functions are required because other arguments vary
|
|
29 |
in the recursive calls ***)
|
|
30 |
|
|
31 |
primrec
|
12593
|
32 |
"lift_aux(Var(i)) = (\<lambda>k \<in> nat. if i<k then Var(i) else Var(succ(i)))"
|
6046
|
33 |
|
12593
|
34 |
"lift_aux(Fun(t)) = (\<lambda>k \<in> nat. Fun(lift_aux(t) ` succ(k)))"
|
6046
|
35 |
|
12593
|
36 |
"lift_aux(App(b,f,a)) = (\<lambda>k \<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
|
6046
|
37 |
|
1048
|
38 |
|
|
39 |
|
6046
|
40 |
primrec
|
|
41 |
"subst_aux(Var(i)) =
|
12593
|
42 |
(\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1)
|
6068
|
43 |
else if k=i then r else Var(i))"
|
6046
|
44 |
"subst_aux(Fun(t)) =
|
12593
|
45 |
(\<lambda>r \<in> redexes. \<lambda>k \<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
|
6046
|
46 |
|
|
47 |
"subst_aux(App(b,f,a)) =
|
12593
|
48 |
(\<lambda>r \<in> redexes. \<lambda>k \<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
|
|
49 |
|
|
50 |
|
|
51 |
(* ------------------------------------------------------------------------- *)
|
|
52 |
(* Arithmetic extensions *)
|
|
53 |
(* ------------------------------------------------------------------------- *)
|
|
54 |
|
|
55 |
lemma gt_not_eq: "p < n ==> n\<noteq>p"
|
|
56 |
by blast
|
|
57 |
|
|
58 |
lemma succ_pred [rule_format, simp]: "j \<in> nat ==> i < j --> succ(j #- 1) = j"
|
|
59 |
by (induct_tac "j", auto)
|
|
60 |
|
|
61 |
lemma lt_pred: "[|succ(x)<n; n \<in> nat|] ==> x < n #- 1 "
|
|
62 |
apply (rule succ_leE)
|
|
63 |
apply (simp add: succ_pred)
|
|
64 |
done
|
|
65 |
|
|
66 |
lemma gt_pred: "[|n < succ(x); p<n; n \<in> nat|] ==> n #- 1 < x "
|
|
67 |
apply (rule succ_leE)
|
|
68 |
apply (simp add: succ_pred)
|
|
69 |
done
|
|
70 |
|
|
71 |
|
|
72 |
declare not_lt_iff_le [simp] if_P [simp] if_not_P [simp]
|
|
73 |
|
|
74 |
|
|
75 |
(* ------------------------------------------------------------------------- *)
|
|
76 |
(* lift_rec equality rules *)
|
|
77 |
(* ------------------------------------------------------------------------- *)
|
|
78 |
lemma lift_rec_Var:
|
|
79 |
"n \<in> nat ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))"
|
|
80 |
by (simp add: lift_rec_def)
|
|
81 |
|
|
82 |
lemma lift_rec_le [simp]:
|
|
83 |
"[|i \<in> nat; k\<le>i|] ==> lift_rec(Var(i),k) = Var(succ(i))"
|
|
84 |
by (simp add: lift_rec_def le_in_nat)
|
|
85 |
|
|
86 |
lemma lift_rec_gt [simp]: "[| k \<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)"
|
|
87 |
by (simp add: lift_rec_def)
|
|
88 |
|
|
89 |
lemma lift_rec_Fun [simp]:
|
|
90 |
"k \<in> nat ==> lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"
|
|
91 |
by (simp add: lift_rec_def)
|
|
92 |
|
|
93 |
lemma lift_rec_App [simp]:
|
|
94 |
"k \<in> nat ==> lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"
|
|
95 |
by (simp add: lift_rec_def)
|
|
96 |
|
|
97 |
|
|
98 |
(* ------------------------------------------------------------------------- *)
|
|
99 |
(* substitution quality rules *)
|
|
100 |
(* ------------------------------------------------------------------------- *)
|
|
101 |
|
|
102 |
lemma subst_Var:
|
|
103 |
"[|k \<in> nat; u \<in> redexes|]
|
|
104 |
==> subst_rec(u,Var(i),k) =
|
|
105 |
(if k<i then Var(i #- 1) else if k=i then u else Var(i))"
|
|
106 |
by (simp add: subst_rec_def gt_not_eq leI)
|
|
107 |
|
|
108 |
|
|
109 |
lemma subst_eq [simp]:
|
|
110 |
"[|n \<in> nat; u \<in> redexes|] ==> subst_rec(u,Var(n),n) = u"
|
|
111 |
by (simp add: subst_rec_def)
|
|
112 |
|
|
113 |
lemma subst_gt [simp]:
|
|
114 |
"[|u \<in> redexes; p \<in> nat; p<n|] ==> subst_rec(u,Var(n),p) = Var(n #- 1)"
|
|
115 |
by (simp add: subst_rec_def)
|
|
116 |
|
|
117 |
lemma subst_lt [simp]:
|
|
118 |
"[|u \<in> redexes; p \<in> nat; n<p|] ==> subst_rec(u,Var(n),p) = Var(n)"
|
|
119 |
by (simp add: subst_rec_def gt_not_eq leI lt_nat_in_nat)
|
|
120 |
|
|
121 |
lemma subst_Fun [simp]:
|
|
122 |
"[|p \<in> nat; u \<in> redexes|]
|
|
123 |
==> subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "
|
|
124 |
by (simp add: subst_rec_def)
|
|
125 |
|
|
126 |
lemma subst_App [simp]:
|
|
127 |
"[|p \<in> nat; u \<in> redexes|]
|
|
128 |
==> subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"
|
|
129 |
by (simp add: subst_rec_def)
|
|
130 |
|
|
131 |
|
|
132 |
lemma lift_rec_type [rule_format, simp]:
|
|
133 |
"u \<in> redexes ==> \<forall>k \<in> nat. lift_rec(u,k) \<in> redexes"
|
|
134 |
apply (erule redexes.induct)
|
|
135 |
apply (simp_all add: lift_rec_Var lift_rec_Fun lift_rec_App)
|
|
136 |
done
|
|
137 |
|
|
138 |
lemma subst_type [rule_format, simp]:
|
|
139 |
"v \<in> redexes ==> \<forall>n \<in> nat. \<forall>u \<in> redexes. subst_rec(u,v,n) \<in> redexes"
|
|
140 |
apply (erule redexes.induct)
|
|
141 |
apply (simp_all add: subst_Var lift_rec_type)
|
|
142 |
done
|
|
143 |
|
|
144 |
|
|
145 |
(* ------------------------------------------------------------------------- *)
|
|
146 |
(* lift and substitution proofs *)
|
|
147 |
(* ------------------------------------------------------------------------- *)
|
|
148 |
|
|
149 |
(*The i\<in>nat is redundant*)
|
|
150 |
lemma lift_lift_rec [rule_format]:
|
|
151 |
"u \<in> redexes
|
|
152 |
==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->
|
|
153 |
(lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
|
|
154 |
apply (erule redexes.induct)
|
|
155 |
apply auto
|
|
156 |
apply (case_tac "n < i")
|
|
157 |
apply (frule lt_trans2, assumption)
|
|
158 |
apply (simp_all add: lift_rec_Var leI)
|
|
159 |
done
|
|
160 |
|
|
161 |
lemma lift_lift:
|
|
162 |
"[|u \<in> redexes; n \<in> nat|]
|
|
163 |
==> lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"
|
|
164 |
by (simp add: lift_lift_rec)
|
|
165 |
|
|
166 |
lemma lt_not_m1_lt: "\<lbrakk>m < n; n \<in> nat; m \<in> nat\<rbrakk>\<Longrightarrow> ~ n #- 1 < m"
|
|
167 |
by (erule natE, auto)
|
|
168 |
|
|
169 |
lemma lift_rec_subst_rec [rule_format]:
|
|
170 |
"v \<in> redexes ==>
|
|
171 |
\<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m-->
|
|
172 |
lift_rec(subst_rec(u,v,n),m) =
|
|
173 |
subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
|
|
174 |
apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
|
|
175 |
apply safe
|
|
176 |
apply (case_tac "n < x")
|
|
177 |
apply (frule_tac j = "x" in lt_trans2, assumption)
|
|
178 |
apply (simp add: leI)
|
|
179 |
apply simp
|
|
180 |
apply (erule_tac j = "n" in leE)
|
|
181 |
apply (auto simp add: lift_rec_Var subst_Var leI lt_not_m1_lt)
|
|
182 |
done
|
|
183 |
|
|
184 |
|
|
185 |
lemma lift_subst:
|
|
186 |
"[|v \<in> redexes; u \<in> redexes; n \<in> nat|]
|
|
187 |
==> lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"
|
|
188 |
by (simp add: lift_rec_subst_rec)
|
|
189 |
|
|
190 |
|
|
191 |
lemma lift_rec_subst_rec_lt [rule_format]:
|
|
192 |
"v \<in> redexes ==>
|
|
193 |
\<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n-->
|
|
194 |
lift_rec(subst_rec(u,v,n),m) =
|
|
195 |
subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
|
|
196 |
apply (erule redexes.induct , simp_all (no_asm_simp) add: lift_lift)
|
|
197 |
apply safe
|
|
198 |
apply (case_tac "n < x")
|
|
199 |
apply (case_tac "n < xa")
|
|
200 |
apply (simp_all add: leI)
|
|
201 |
apply (erule_tac i = "x" in leE)
|
|
202 |
apply (frule lt_trans1, assumption)
|
|
203 |
apply (simp_all add: succ_pred leI gt_pred)
|
|
204 |
done
|
|
205 |
|
|
206 |
|
|
207 |
lemma subst_rec_lift_rec [rule_format]:
|
|
208 |
"u \<in> redexes ==>
|
|
209 |
\<forall>n \<in> nat. \<forall>v \<in> redexes. subst_rec(v,lift_rec(u,n),n) = u"
|
|
210 |
apply (erule redexes.induct)
|
|
211 |
apply auto
|
|
212 |
apply (case_tac "n < na")
|
|
213 |
apply auto
|
|
214 |
done
|
|
215 |
|
|
216 |
lemma subst_rec_subst_rec [rule_format]:
|
|
217 |
"v \<in> redexes ==>
|
|
218 |
\<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->
|
|
219 |
subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) =
|
|
220 |
subst_rec(w,subst_rec(u,v,m),n)"
|
|
221 |
apply (erule redexes.induct)
|
|
222 |
apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt)
|
|
223 |
apply safe
|
|
224 |
apply (case_tac "n\<le>succ (xa) ")
|
|
225 |
apply (erule_tac i = "n" in leE)
|
|
226 |
apply (simp_all add: succ_pred subst_rec_lift_rec leI)
|
|
227 |
apply (case_tac "n < x")
|
|
228 |
apply (frule lt_trans2 , assumption, simp add: gt_pred)
|
|
229 |
apply simp
|
|
230 |
apply (erule_tac j = "n" in leE, simp add: gt_pred)
|
|
231 |
apply (simp add: subst_rec_lift_rec)
|
|
232 |
(*final case*)
|
|
233 |
apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans] , assumption)
|
|
234 |
apply (erule leE)
|
|
235 |
apply (frule succ_leI [THEN lt_trans] , assumption)
|
|
236 |
apply (frule_tac i = "x" in nat_into_Ord [THEN le_refl, THEN lt_trans],
|
|
237 |
assumption)
|
|
238 |
apply (simp_all add: succ_pred lt_pred)
|
|
239 |
done
|
|
240 |
|
|
241 |
|
|
242 |
lemma substitution:
|
|
243 |
"[|v \<in> redexes; u \<in> redexes; w \<in> redexes; n \<in> nat|]
|
|
244 |
==> subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"
|
|
245 |
by (simp add: subst_rec_subst_rec)
|
|
246 |
|
|
247 |
|
|
248 |
(* ------------------------------------------------------------------------- *)
|
|
249 |
(* Preservation lemmas *)
|
|
250 |
(* Substitution preserves comp and regular *)
|
|
251 |
(* ------------------------------------------------------------------------- *)
|
|
252 |
|
|
253 |
|
|
254 |
lemma lift_rec_preserve_comp [rule_format, simp]:
|
|
255 |
"u ~ v ==> \<forall>m \<in> nat. lift_rec(u,m) ~ lift_rec(v,m)"
|
|
256 |
by (erule Scomp.induct, simp_all add: comp_refl)
|
|
257 |
|
|
258 |
lemma subst_rec_preserve_comp [rule_format, simp]:
|
|
259 |
"u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes.
|
|
260 |
u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"
|
|
261 |
by (erule Scomp.induct,
|
|
262 |
simp_all add: subst_Var lift_rec_preserve_comp comp_refl)
|
|
263 |
|
|
264 |
lemma lift_rec_preserve_reg [simp]:
|
|
265 |
"regular(u) ==> \<forall>m \<in> nat. regular(lift_rec(u,m))"
|
|
266 |
by (erule Sreg.induct, simp_all add: lift_rec_Var)
|
|
267 |
|
|
268 |
lemma subst_rec_preserve_reg [simp]:
|
|
269 |
"regular(v) ==>
|
|
270 |
\<forall>m \<in> nat. \<forall>u \<in> redexes. regular(u)-->regular(subst_rec(u,v,m))"
|
|
271 |
by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
|
1048
|
272 |
|
|
273 |
end
|
|
274 |
|
|
275 |
|