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