27 |
27 |
28 (** The clumsy _aux functions are required because other arguments vary |
28 (** The clumsy _aux functions are required because other arguments vary |
29 in the recursive calls ***) |
29 in the recursive calls ***) |
30 |
30 |
31 primrec |
31 primrec |
32 "lift_aux(Var(i)) = (\\<lambda>k \\<in> nat. if i<k then Var(i) else Var(succ(i)))" |
32 "lift_aux(Var(i)) = (\<lambda>k \<in> nat. if i<k then Var(i) else Var(succ(i)))" |
33 |
33 |
34 "lift_aux(Fun(t)) = (\\<lambda>k \\<in> nat. Fun(lift_aux(t) ` succ(k)))" |
34 "lift_aux(Fun(t)) = (\<lambda>k \<in> nat. Fun(lift_aux(t) ` succ(k)))" |
35 |
35 |
36 "lift_aux(App(b,f,a)) = (\\<lambda>k \\<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))" |
36 "lift_aux(App(b,f,a)) = (\<lambda>k \<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))" |
37 |
37 |
38 |
38 |
39 |
39 |
40 primrec |
40 primrec |
41 "subst_aux(Var(i)) = |
41 "subst_aux(Var(i)) = |
42 (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. if k<i then Var(i #- 1) |
42 (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1) |
43 else if k=i then r else Var(i))" |
43 else if k=i then r else Var(i))" |
44 "subst_aux(Fun(t)) = |
44 "subst_aux(Fun(t)) = |
45 (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))" |
45 (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))" |
46 |
46 |
47 "subst_aux(App(b,f,a)) = |
47 "subst_aux(App(b,f,a)) = |
48 (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))" |
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) |
49 |
272 |
50 end |
273 end |
51 |
274 |
52 |
275 |