1open HolKernel bossLib boolLib Parse termTheory chap2Theory chap3Theory reductionEval binderLib relationTheory lcsymtacs
2
3val _ = new_theory "abselim"
4
5val _ = remove_ovl_mapping "LAM" {Name="LAM", Thy="labelledTerms"}
6val _ = clear_overloads_on "FV"
7val _ = overload_on ("FV", ``supp tpm``)
8val _ = remove_ovl_mapping "VAR" {Name="VAR", Thy="labelledTerms"}
9val _ = remove_ovl_mapping "APP"  {Name="APP", Thy="labelledTerms"}
10
11val (absfree_rules,absfree_ind,absfree_cases) = Hol_reln`
12  (absfree S) ��� (absfree K) ��� (absfree (VAR x)) ���
13  (absfree t1 ��� absfree t2 ��� absfree (APP t1 t2))`
14
15val (abselim_rules,abselim_ind,abselim_cases) = Hol_reln`
16  (abselim (VAR x) (VAR x)) ���
17  (abselim t1 t1' ��� abselim t2 t2' ��� abselim (t1 @@ t2) (t1' @@ t2')) ���
18  (abselim t t' ��� x ��� FV t ��� abselim (LAM x t) (K @@ t')) ���
19  (abselim (LAM x (VAR x)) (S @@ K @@ K)) ���
20  (abselim (LAM y t) r1 ��� abselim (LAM x r1) r2
21   ��� x ��� FV (LAM y t) ��� (LAM x (LAM y t) ��� S) ��� (LAM x (LAM y t) ��� K)
22    ��� abselim (LAM x (LAM y t)) r2) ���
23  (abselim (LAM x t1) t1' ��� abselim (LAM x t2) t2' ��� x ��� FV (t1 @@ t2)
24    ��� abselim (LAM x (t1 @@ t2)) (S @@ t1' @@ t2')) ���
25  (abselim S S) ��� (abselim K K)`
26
27val abselim_absfree = store_thm(
28"abselim_absfree",
29``���t u. abselim t u ��� absfree u``,
30ho_match_mp_tac abselim_ind >>
31srw_tac [][absfree_rules])
32
33val absfree_abselim_id = store_thm(
34"absfree_abselim_id",
35``���t. absfree t ��� abselim t t``,
36ho_match_mp_tac absfree_ind >>
37srw_tac [][abselim_rules]);
38
39val lameq_lamext = store_thm(
40"lameq_lamext",
41``���t u. t == u ��� lamext t u``,
42ho_match_mp_tac lameq_ind >>
43metis_tac [lamext_rules])
44
45val lamext_refl = store_thm(
46  "lamext_refl",
47  ``lamext M M``,
48  SRW_TAC [][lamext_rules]);
49val _ = export_rewrites["lamext_refl"];
50
51val lamext_app_cong = store_thm(
52  "lamext_app_cong",
53  ``lamext M1 M2 ==> lamext N1 N2 ==> lamext (M1 @@ N1) (M2 @@ N2)``,
54  METIS_TAC [lamext_rules]);
55
56val [_,lamext_refl,lamext_sym,lamext_trans,_,_,_,lamext_ext] = CONJUNCTS lamext_rules
57val [_,conversion_sym,conversion_trans,conversion_subset,_,_] = CONJUNCTS (SPEC_ALL conversion_rules)
58
59val lamext_betaeta = store_thm(
60"lamext_betaeta",
61``lamext = conversion (�� RUNION ��)``,
62metis_tac [lemma2_14,beta_eta_lameta,FUN_EQ_THM]);
63
64val abselim_lamext = store_thm(
65"abselim_lamext",
66``���t u. abselim t u ��� lamext t u``,
67ho_match_mp_tac abselim_ind >>
68conj_tac >- srw_tac [][] >>
69conj_tac >- srw_tac [][lamext_app_cong] >>
70conj_tac >- (
71  map_every qx_gen_tac [`t`,`u`,`x`] >>
72  strip_tac >>
73  match_mp_tac lamext_ext >>
74  Q_TAC (NEW_TAC "z") `FV (LAM x t @@ (K @@ u))` >>
75  qexists_tac `z` >> conj_tac >- fsrw_tac [][] >>
76  srw_tac [][lamext_betaeta] >>
77  match_mp_tac conversion_trans >>
78  qexists_tac `t` >>
79  conj_tac >- (
80    match_mp_tac conversion_subset >>
81    srw_tac [][RUNION,beta_def] >>
82    disj1_tac >>
83    map_every qexists_tac [`x`,`t`] >>
84    srw_tac [][lemma14b] ) >>
85  match_mp_tac conversion_trans >>
86  qexists_tac `u` >>
87  conj_tac >- (
88    srw_tac [][SYM lamext_betaeta] ) >>
89  srw_tac [][SYM lamext_betaeta] >>
90  match_mp_tac lameq_lamext >>
91  srw_tac [BETA_ss][] ) >>
92conj_tac >- (
93  srw_tac [][] >>
94  match_mp_tac lamext_ext >>
95  Q_TAC (NEW_TAC "z") `FV (LAM x (VAR x) @@ (S @@ K @@ K))` >>
96  qexists_tac `z` >> srw_tac [][] >>
97  match_mp_tac lameq_lamext >>
98  srw_tac [BETA_ss][] ) >>
99conj_tac >-
100  metis_tac [lamext_rules] >>
101conj_tac >- (
102  rpt gen_tac >>
103  strip_tac >>
104  pop_assum (K ALL_TAC) >>
105  match_mp_tac lamext_ext >>
106  Q_TAC (NEW_TAC "z") `FV (LAM x (t1 @@ t2) @@ (S @@ t1' @@ t2'))` >>
107  qexists_tac `z` >> fsrw_tac [][] >>
108  match_mp_tac lamext_sym >>
109  match_mp_tac lamext_trans >>
110  qexists_tac `S @@ (LAM x t1) @@ (LAM x t2) @@ VAR z` >>
111  conj_tac >- PROVE_TAC [lamext_rules] >>
112  match_mp_tac lameq_lamext >>
113  srw_tac [BETA_ss][] ) >>
114srw_tac [][lamext_refl]);
115
116val lemma1 = prove(
117``x ��� FV t ��� (LAM x (tpm [(x,y)] t) = LAM y t)``,
118srw_tac [][LAM_eq_thm] >>
119Cases_on `x=y` >> srw_tac [][])
120
121val lemma2 = prove(
122``(LAM (swapstr x y v) (tpm [(x,y)] t) = S) = (LAM v t = S)``,
123srw_tac [][EQ_IMP_THM] >- (
124  `tpm [(x,y)] (LAM (swapstr x y v) (tpm [(x,y)] t)) = tpm [(x,y)] S` by
125    metis_tac [] >>
126  fsrw_tac [][] >> srw_tac [][tpm_fresh] ) >>
127`tpm [(x,y)] (LAM v t) = tpm [(x,y)] S` by metis_tac [] >>
128fsrw_tac [][] >> srw_tac [][tpm_fresh])
129
130val lemma3 = prove(
131``(LAM (swapstr x y v) (tpm [(x,y)] t) = K) = (LAM v t = K)``,
132srw_tac [][EQ_IMP_THM] >- (
133  `tpm [(x,y)] (LAM (swapstr x y v) (tpm [(x,y)] t)) = tpm [(x,y)] K` by
134    metis_tac [] >>
135  fsrw_tac [][] >> srw_tac [][tpm_fresh] ) >>
136`tpm [(x,y)] (LAM v t) = tpm [(x,y)] K` by metis_tac [] >>
137fsrw_tac [][] >> srw_tac [][tpm_fresh])
138
139val lam_count_exists =
140  tm_recursion
141|> INST_TYPE [alpha |-> ``:num``]
142|> Q.INST [`apm`|->`K I`,`A`|->`{}`,
143           `vr`|->`K 0`,
144           `ap`|->`��m n t1 t2. m + n`,
145           `lm`|->`��m v t. if (LAM v t = S) ��� (LAM v t = K) then 0 else m + 1`]
146|> SIMP_RULE (srw_ss()) [lemma1,lemma2,lemma3]
147
148val lam_count_def = new_specification ("lam_count_def",["lam_count"],lam_count_exists)
149
150val app_count_exists =
151  tm_recursion
152|> INST_TYPE [alpha |-> ``:num``]
153|> Q.INST [`apm`|->`K I`,`A`|->`{}`,
154           `vr`|->`K 0`,
155           `ap`|->`��m n t1 t2. m + n + 1`,
156           `lm`|->`��m v t. if (LAM v t = S) ��� (LAM v t = K) then 0 else m`]
157|> SIMP_RULE (srw_ss()) [lemma1,lemma2,lemma3]
158
159val app_count_def = new_specification ("app_count_def",["app_count"],app_count_exists)
160
161val _ = export_rewrites["lam_count_def","app_count_def"];
162
163val lam_count_absfree = store_thm(
164"lam_count_absfree",
165``���t. absfree t ��� (lam_count t = 0)``,
166ho_match_mp_tac absfree_ind >>
167srw_tac [][S_def,K_def])
168
169val abselim_total = store_thm(
170"abselim_total",
171``���t.���u. abselim t u``,
172WF_INDUCTION_THM
173 |> Q.ISPEC `inv_image ($< LEX $<) (��t. (lam_count t, app_count t))`
174 |> SIMP_RULE (srw_ss()) [pairTheory.WF_LEX,prim_recTheory.WF_LESS,relationTheory.WF_inv_image]
175 |> ho_match_mp_tac >>
176srw_tac [][relationTheory.inv_image_def,prim_recTheory.measure_def,pairTheory.LEX_DEF] >>
177FULL_STRUCT_CASES_TAC (Q.SPEC `t` term_CASES) >- (
178  fsrw_tac [][] >> metis_tac [abselim_rules] )
179>- (
180  `(���u. abselim t1 u) ��� (���u. abselim t2 u)` by (
181    srw_tac [][] >> first_x_assum match_mp_tac >>
182    srw_tac [ARITH_ss][] ) >>
183  metis_tac [abselim_rules] ) >>
184qmatch_rename_tac `���u. abselim (LAM x t) u` [] >>
185Cases_on `LAM x t = S` >- metis_tac [abselim_rules] >>
186Cases_on `LAM x t = K` >- metis_tac [abselim_rules] >>
187Cases_on `x ��� FV t` >- (
188  `���u. abselim t u` by (
189    first_x_assum match_mp_tac >>
190    srw_tac [ARITH_ss][] ) >>
191  metis_tac [abselim_rules] ) >> fsrw_tac [][] >>
192FULL_STRUCT_CASES_TAC (Q.SPEC `t` term_CASES) >- (
193  fsrw_tac [][] >> metis_tac [abselim_rules] )
194>- (
195  `(���u. abselim (LAM x t1) u) ��� (���u. abselim (LAM x t2) u)` by (
196    srw_tac [][] >> first_x_assum match_mp_tac >>
197    srw_tac [ARITH_ss][] ) >>
198  `x ��� FV t1 ��� FV t2` by fsrw_tac [][] >>
199  metis_tac [abselim_rules] ) >>
200qmatch_rename_tac `���u. abselim (LAM x (LAM y t)) u` [] >>
201`���r1. abselim (LAM y t) r1` by (
202  first_x_assum match_mp_tac >>
203  srw_tac [ARITH_ss][] ) >>
204`x ��� FV t` by fsrw_tac [][] >>
205qsuff_tac `���r2. abselim (LAM x r1) r2` >- metis_tac [abselim_rules] >>
206first_x_assum match_mp_tac >>
207disj1_tac >>
208Cases_on `LAM x r1 = S` >- srw_tac [ARITH_ss][] >>
209Cases_on `LAM x r1 = K` >- srw_tac [ARITH_ss][] >>
210`absfree r1` by metis_tac [abselim_absfree] >>
211`lam_count r1 = 0` by metis_tac [lam_count_absfree] >>
212Cases_on `LAM y t = S` >- (
213  `x ��� FV S` by metis_tac [] >> fsrw_tac [][S_def] ) >>
214Cases_on `LAM y t = K` >- (
215  `x ��� FV K` by metis_tac [] >> fsrw_tac [][K_def] ) >>
216srw_tac [ARITH_ss][])
217
218val [abselim_VAR,abselim_APP,abselim_LAM,abselim_LAM_VAR,abselim_LAM_LAM,abselim_LAM_APP,abselim_S,abselim_K] = CONJUNCTS abselim_rules
219
220val abselim_tpm = store_thm(
221"abselim_tpm",
222``���t u. abselim t u ��� ���x y. abselim (tpm [(x,y)] t) (tpm [(x,y)] u)``,
223ho_match_mp_tac abselim_ind >>
224conj_tac >- srw_tac [][abselim_VAR] >>
225conj_tac >- srw_tac [][abselim_APP] >>
226conj_tac >- srw_tac [][abselim_LAM,tpm_fresh] >>
227conj_tac >- srw_tac [][abselim_LAM_VAR,tpm_fresh] >>
228conj_tac >- (
229  srw_tac [][] >>
230  match_mp_tac abselim_LAM_LAM >>
231  srw_tac [][] >>
232  qexists_tac `(tpm [(x',y')] u)` >>
233  `tpm [(x',y')] (LAM x (LAM y t)) ��� tpm [(x',y')] S` by metis_tac [tpm_inverse] >>
234  `tpm [(x',y')] (LAM x (LAM y t)) ��� tpm [(x',y')] K` by metis_tac [tpm_inverse] >>
235  fsrw_tac [][tpm_fresh] ) >>
236conj_tac >- (
237  rpt gen_tac >>
238  strip_tac >>
239  rpt gen_tac >>
240  asm_simp_tac (srw_ss()) [tpm_fresh] >>
241  match_mp_tac abselim_LAM_APP >>
242  fsrw_tac [][] ) >>
243srw_tac [][tpm_fresh,abselim_S,abselim_K]);
244
245val abselim_FV = store_thm(
246"abselim_FV",
247``���t u. abselim t u ��� (FV t = FV u)``,
248ho_match_mp_tac abselim_ind >>
249conj_tac >- srw_tac [][] >>
250conj_tac >- srw_tac [][] >>
251conj_tac >- fsrw_tac [][pred_setTheory.DELETE_NON_ELEMENT] >>
252conj_tac >- srw_tac [][] >>
253conj_tac >- srw_tac [][] >>
254conj_tac >- fsrw_tac [][pred_setTheory.DELETE_NON_ELEMENT,pred_setTheory.UNION_DELETE] >>
255srw_tac [][]);
256
257val abselim_unique = store_thm(
258"abselim_unique",
259``���t u1 u2. abselim t u1 ��� abselim t u2 ��� (u1 = u2)``,
260qsuff_tac `���t u1. abselim t u1 ��� ���u2. abselim t u2 ��� (u1 = u2)` >- metis_tac [] >>
261ho_match_mp_tac abselim_ind >>
262conj_tac >- (
263  srw_tac [][] >>
264  qspecl_then [`VAR x`,`u2`] mp_tac abselim_cases >>
265  fsrw_tac [][] >>
266  srw_tac [][S_def,K_def] ) >>
267conj_tac >- (
268  map_every qx_gen_tac [`t1`,`v1`,`t2`,`v2`] >>
269  srw_tac [][] >>
270  qspecl_then [`t1@@t2`,`u2`] mp_tac abselim_cases >>
271  fsrw_tac [][S_def,K_def] >>
272  srw_tac [][] >> srw_tac [][] ) >>
273conj_tac >- (
274  srw_tac [][] >>
275  qspecl_then [`LAM x t`,`u2`] mp_tac abselim_cases >>
276  fsrw_tac [][] >>
277  srw_tac [][] >-
278    fsrw_tac [][LAM_eq_thm,tpm_fresh]
279  >- (
280    fsrw_tac [][LAM_eq_thm] >>
281    fsrw_tac [][] )
282  >- (
283    fsrw_tac [][LAM_eq_thm] >> srw_tac [][] >>
284    fsrw_tac [][] >>
285    Cases_on `x=y` >> fsrw_tac [][] )
286  >- (
287    fsrw_tac [][LAM_eq_thm] >> srw_tac [][] >>
288    fsrw_tac [][] )
289  >- (
290    fsrw_tac [][LAM_eq_thm] >> srw_tac [][] >>
291    fsrw_tac [][] )
292  >- (
293    fsrw_tac [][LAM_eq_thm,S_def] >> srw_tac [][] >>
294    fsrw_tac [][] >>
295    Cases_on `x = "x"` >> fsrw_tac [][] >>
296    Cases_on `x = "y"` >> fsrw_tac [][] >>
297    Cases_on `x = "z"` >> fsrw_tac [][] ) >>
298  fsrw_tac [][K_def,LAM_eq_thm] >> srw_tac [][] >>
299  fsrw_tac [][] >>
300  Cases_on `x = "x"` >> fsrw_tac [][] >>
301  Cases_on `x = "y"` >> fsrw_tac [][] ) >>
302conj_tac >- (
303  srw_tac [][] >>
304  qspecl_then [`LAM x (VAR x)`,`u2`] mp_tac abselim_cases >>
305  fsrw_tac [][LAM_eq_thm] >>
306  srw_tac [][] >> fsrw_tac [][] >>
307  fsrw_tac [][tpm_eqr] >> srw_tac [][] >>
308  fsrw_tac [][] >>
309  fsrw_tac [][S_def,K_def,LAM_eq_thm] ) >>
310conj_tac >- (
311  srw_tac [][] >>
312  qspecl_then [`LAM x (LAM y t)`,`u2`] mp_tac abselim_cases >>
313  full_simp_tac std_ss [term_distinct] >>
314  strip_tac >- (
315    fsrw_tac [][LAM_eq_thm] >>
316    srw_tac [][] >> fsrw_tac [][] >>
317    fsrw_tac [][tpm_eqr] >>
318    srw_tac [][] >>
319    fsrw_tac [][] >>
320    qpat_assum `x <> x'` assume_tac >>
321    qpat_assum `x <> y` assume_tac >>
322    Cases_on`x'=y` >> fsrw_tac [][] )
323  >- ( fsrw_tac [][LAM_eq_thm] )
324  >- (
325    Cases_on `x=x'` >- (
326      qpat_assum `LAM x tt = LAM x' ttt` mp_tac >>
327      asm_simp_tac (srw_ss()) [Once LAM_eq_thm] >>
328      metis_tac [] ) >>
329    qpat_assum `LAM x tt = LAM x' ttt` mp_tac >>
330    asm_simp_tac (srw_ss()) [Once LAM_eq_thm] >>
331    `abselim (tpm [(x,x')] (LAM y' t')) (tpm [(x,x')] r1)` by metis_tac [abselim_tpm] >>
332    fsrw_tac [][] >> rpt strip_tac >>
333    fsrw_tac [][] >>
334    `u1 = tpm [(x,x')] r1` by metis_tac [] >>
335    fsrw_tac [][] >>
336    `abselim (tpm [(x,x')] (LAM x' r1)) (tpm [(x,x')] u2)` by metis_tac [abselim_tpm] >>
337    fsrw_tac [][] >>
338    `u1' = tpm [(x,x')] u2` by metis_tac [] >>
339    srw_tac [][] >>
340    match_mp_tac tpm_fresh >>
341    `FV u2 = FV (LAM x' r1)` by metis_tac [abselim_FV] >>
342    fsrw_tac [][] >>
343    `FV r1 = FV (LAM y' t')` by metis_tac [abselim_FV] >>
344    fsrw_tac [][] >>
345    Cases_on `x=y'` >> fsrw_tac [][] ) >>
346  fsrw_tac [][LAM_eq_thm] ) >>
347conj_tac >- (
348  rpt gen_tac >>
349  strip_tac >>
350  gen_tac >> strip_tac >>
351  qspecl_then [`LAM x (t1 @@ t2)`,`u2`] mp_tac abselim_cases >>
352  qabbrev_tac `fva = (x ��� FV (t1 @@ t2))` >>
353  fsrw_tac [][] >>
354  qpat_assum `abselim (LAM x (t1 @@ t2)) u2` (K ALL_TAC) >>
355  fsrw_tac [][S_def,LAM_eq_thm,K_def] >>
356  fsrw_tac [][GSYM S_def, GSYM K_def] >>
357  qmatch_abbrev_tac `aa ��� bb ��� cc` >>
358  strip_tac >- (
359    unabbrev_all_tac >>
360    fsrw_tac [][tpm_eqr] >> srw_tac [][] >>
361    fsrw_tac [][] ) >>
362  qunabbrev_tac `aa` >>
363  full_simp_tac std_ss [Abbr`cc`,Abbr`bb`,(GSYM pred_setTheory.IN_UNION)] >-
364    fsrw_tac [][] >>
365  qabbrev_tac `fva' = x' ��� FV t1' ��� FV t2'` >>
366  qpat_assum `Abbrev (fva = X)` assume_tac >>
367  fsrw_tac [][] >>
368  `abselim (tpm [(x,x')] (LAM x' t1')) (tpm [(x,x')] t1'')` by metis_tac [abselim_tpm] >>
369  `abselim (tpm [(x,x')] (LAM x' t2')) (tpm [(x,x')] t2'')` by metis_tac [abselim_tpm] >>
370  fsrw_tac [][] >>
371  res_tac >>
372  `(FV t1'' = FV (LAM x' t1')) ��� (FV t2'' = FV (LAM x' t2'))` by metis_tac [abselim_FV] >>
373  srw_tac [][tpm_fresh] ) >>
374conj_tac >- (
375  srw_tac [][] >>
376  qspecl_then [`S`,`u2`] mp_tac abselim_cases >>
377  srw_tac [][]
378  >- srw_tac [][S_def]
379  >- fsrw_tac [][S_def]
380  >- (
381    fsrw_tac [][S_def,LAM_eq_thm] >- (
382      srw_tac [][] >> fsrw_tac [][] ) >>
383    fsrw_tac [][tpm_eqr] >> srw_tac [][] >>
384    fsrw_tac [][] >>
385    Cases_on `x="x"` >> fsrw_tac [][] >>
386    Cases_on `x="y"` >> fsrw_tac [][] >>
387    Cases_on `x="z"` >> fsrw_tac [][] )
388  >- ( fsrw_tac [][S_def,LAM_eq_thm] )
389  >- ( metis_tac [] )
390  >- ( fsrw_tac [][S_def,LAM_eq_thm] )
391  >- ( fsrw_tac [][S_def,LAM_eq_thm] )
392  >- ( fsrw_tac [][] ) ) >>
393srw_tac [][] >>
394qspecl_then [`K`,`u2`] mp_tac abselim_cases >>
395srw_tac [][]
396>- srw_tac [][K_def]
397>- fsrw_tac [][K_def]
398>- (
399  fsrw_tac [][K_def,LAM_eq_thm] >- (
400    srw_tac [][] >> fsrw_tac [][] ) >>
401  fsrw_tac [][tpm_eqr] >> srw_tac [][] >>
402  fsrw_tac [][] >>
403  Cases_on `x="x"` >> fsrw_tac [][] >>
404  Cases_on `x="y"` >> fsrw_tac [][] )
405>- ( fsrw_tac [][K_def,LAM_eq_thm] )
406>- ( metis_tac [] )
407>- ( fsrw_tac [][K_def,LAM_eq_thm] )
408>- ( fsrw_tac [][K_def,LAM_eq_thm] )
409>- ( fsrw_tac [][] ) )
410
411val _ = export_theory ()
412