1open HolKernel boolLib Parse bossLib generic_termsTheory
2
3open boolSimps
4
5open nomsetTheory
6open pred_setTheory
7open binderLib
8open nomdatatype
9val _ = new_theory "term";
10
11val _ = set_fixity "=" (Infix(NONASSOC, 450))
12
13fun Save_thm (nm, th) = save_thm(nm,th) before export_rewrites [nm]
14fun Store_thm(nm,t,tac) = store_thm(nm,t,tac) before export_rewrites [nm]
15
16val tyname = "term"
17
18val vp = ``(��n u:unit. n = 0)``
19val lp = ``(��n (d:unit + unit) tns uns.
20               (n = 0) ��� ISL d ��� (tns = []) ��� (uns = [0;0]) ���
21               (n = 0) ��� ISR d ��� (tns = [0]) ��� (uns = []))``
22
23val {term_ABS_pseudo11, term_REP_11, genind_term_REP, genind_exists,
24     termP, absrep_id, repabs_pseudo_id, term_REP_t, term_ABS_t, newty, ...} =
25    new_type_step1 tyname 0 {vp=vp, lp = lp}
26val [gvar,glam] = genind_rules |> SPEC_ALL |> CONJUNCTS
27
28val LAM_t = mk_var("LAM", ``:string -> ^newty -> ^newty``)
29val LAM_def = new_definition(
30  "LAM_def",
31  ``^LAM_t v t = ^term_ABS_t (GLAM v (INR ()) [^term_REP_t t] [])``)
32val LAM_termP = prove(
33  mk_comb(termP, LAM_def |> SPEC_ALL |> concl |> rhs |> rand),
34  match_mp_tac glam >> srw_tac [][genind_term_REP]);
35val LAM_t = defined_const LAM_def
36
37
38val APP_t = mk_var("APP", ``:^newty -> ^newty -> ^newty``)
39val APP_def = new_definition(
40  "APP_def",
41  ``^APP_t t1 t2 =
42       ^term_ABS_t (GLAM ARB (INL ()) [] [^term_REP_t t1; ^term_REP_t t2])``);
43val APP_termP = prove(
44  ``^termP (GLAM x (INL ()) [] [^term_REP_t t1; ^term_REP_t t2])``,
45  match_mp_tac glam >> srw_tac [][genind_term_REP])
46val APP_t = defined_const APP_def
47
48val APP_def' = prove(
49  ``^term_ABS_t (GLAM v (INL ()) [] [^term_REP_t t1; ^term_REP_t t2]) = ^APP_t t1 t2``,
50  srw_tac [][APP_def, GLAM_NIL_EQ, term_ABS_pseudo11, APP_termP]);
51
52val VAR_t = mk_var("VAR", ``:string -> ^newty``)
53val VAR_def = new_definition(
54  "VAR_def",
55  ``^VAR_t s = ^term_ABS_t (GVAR s ())``);
56val VAR_termP = prove(
57  mk_comb(termP, VAR_def |> SPEC_ALL |> concl |> rhs |> rand),
58  srw_tac [][genind_rules]);
59val VAR_t = defined_const VAR_def
60
61val cons_info =
62    [{con_termP = VAR_termP, con_def = VAR_def},
63     {con_termP = APP_termP, con_def = SYM APP_def'},
64     {con_termP = LAM_termP, con_def = LAM_def}]
65
66val tpm_name_pfx = "t"
67val {tpm_thm, term_REP_tpm, t_pmact_t, tpm_t} =
68    define_permutation {name_pfx = "t", name = tyname,
69                        term_REP_t = term_REP_t,
70                        term_ABS_t = term_ABS_t, absrep_id = absrep_id,
71                        repabs_pseudo_id = repabs_pseudo_id,
72                        cons_info = cons_info, newty = newty,
73                        genind_term_REP = genind_term_REP}
74
75(* support *)
76val term_REP_eqv = prove(
77   ``support (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t {}`` ,
78   srw_tac [][support_def, fnpm_def, FUN_EQ_THM, term_REP_tpm, pmact_sing_inv]);
79
80val supp_term_REP = prove(
81  ``supp (fn_pmact ^t_pmact_t gt_pmact) ^term_REP_t = {}``,
82  REWRITE_TAC [GSYM SUBSET_EMPTY] >> MATCH_MP_TAC (GEN_ALL supp_smallest) >>
83  srw_tac [][term_REP_eqv])
84
85val tpm_def' =
86    term_REP_tpm |> AP_TERM term_ABS_t |> PURE_REWRITE_RULE [absrep_id]
87
88val t = mk_var("t", newty)
89val supptpm_support = prove(
90  ``support ^t_pmact_t ^t (supp gt_pmact (^term_REP_t ^t))``,
91  srw_tac [][support_def, tpm_def', supp_fresh, absrep_id]);
92
93val supptpm_apart = prove(
94  ``x ��� supp gt_pmact (^term_REP_t ^t) ��� y ��� supp gt_pmact (^term_REP_t ^t) ���
95    ^tpm_t [(x,y)] ^t ��� ^t``,
96  srw_tac [][tpm_def']>>
97  DISCH_THEN (MP_TAC o AP_TERM term_REP_t) >>
98  srw_tac [][repabs_pseudo_id, genind_gtpm_eqn, genind_term_REP, supp_apart]);
99
100val supp_tpm = prove(
101  ``supp ^t_pmact_t ^t = supp gt_pmact (^term_REP_t ^t)``,
102  match_mp_tac (GEN_ALL supp_unique_apart) >>
103  srw_tac [][supptpm_support, supptpm_apart, FINITE_GFV])
104
105val _ = overload_on ("FV", ``supp ^t_pmact_t``)
106
107val FINITE_FV = store_thm(
108  "FINITE_FV",
109  ``FINITE (FV t)``,
110  srw_tac [][supp_tpm, FINITE_GFV]);
111val _ = export_rewrites ["FINITE_FV"]
112
113fun supp_clause {con_termP, con_def} = let
114  val t = mk_comb(``supp ^t_pmact_t``, lhand (concl (SPEC_ALL con_def)))
115in
116  t |> REWRITE_CONV [supp_tpm, con_def, MATCH_MP repabs_pseudo_id con_termP,
117                     GFV_thm]
118    |> REWRITE_RULE [supp_listpm, EMPTY_DELETE, UNION_EMPTY]
119    |> REWRITE_RULE [GSYM supp_tpm]
120    |> GEN_ALL
121end
122
123val FV_thm = Save_thm(
124  "FV_thm",
125  LIST_CONJ (map supp_clause cons_info))
126
127
128
129fun genit th = let
130  val (_, args) = strip_comb (concl th)
131  val (tm, x) = case args of [x,y] => (x,y) | _ => raise Fail "Bind"
132  val ty = type_of tm
133  val t = mk_var("t", ty)
134in
135  th |> INST [tm |-> t] |> GEN x |> GEN t
136end
137
138val LIST_REL_CONS1 = listTheory.LIST_REL_CONS1
139val LIST_REL_NIL = listTheory.LIST_REL_NIL
140
141val term_ind =
142    bvc_genind
143        |> INST_TYPE [alpha |-> ``:unit+unit``, beta |-> ``:unit``]
144        |> Q.INST [`vp` |-> `^vp`, `lp` |-> `^lp`]
145        |> SIMP_RULE std_ss [LIST_REL_CONS1, RIGHT_AND_OVER_OR,
146                             LEFT_AND_OVER_OR, DISJ_IMP_THM, LIST_REL_NIL]
147        |> Q.SPEC `��n t0 x. Q t0 x`
148        |> Q.SPEC `fv`
149        |> UNDISCH |> Q.SPEC `0` |> DISCH_ALL
150        |> SIMP_RULE (std_ss ++ DNF_ss)
151                     [sumTheory.FORALL_SUM, supp_listpm,
152                      IN_UNION, NOT_IN_EMPTY, oneTheory.FORALL_ONE,
153                      genind_exists, LIST_REL_CONS1, LIST_REL_NIL]
154        |> Q.INST [`Q` |-> `��t. P (term_ABS t)`]
155        |> SIMP_RULE std_ss [GSYM LAM_def, APP_def', GSYM VAR_def, absrep_id]
156        |> SIMP_RULE (srw_ss()) [GSYM supp_tpm]
157        |> elim_unnecessary_atoms {finite_fv = FINITE_FV}
158                                  [ASSUME ``!x:'c. FINITE (fv x:string set)``]
159        |> SPEC_ALL |> UNDISCH
160        |> genit |> DISCH_ALL |> Q.GEN `fv` |> Q.GEN `P`
161
162fun mkX_ind th = th |> Q.SPEC `��t x. Q t` |> Q.SPEC `��x. X`
163                    |> SIMP_RULE std_ss [] |> Q.GEN `X`
164                    |> Q.INST [`Q` |-> `P`] |> Q.GEN `P`
165
166(* exactly mimic historical bound variable names etc for backwards
167   compatibility *)
168val nc_INDUCTION2 = store_thm(
169  "nc_INDUCTION2",
170  ``���P X.
171      (���s. P (VAR s)) ���
172      (���t u. P t ��� P u ==> P (APP t u)) ���
173      (���y u. y ��� X ��� P u ==> P (LAM y u)) ��� FINITE X ==>
174      ���u. P u``,
175  metis_tac [mkX_ind term_ind]);
176
177
178val LAM_eq_thm = save_thm(
179  "LAM_eq_thm",
180  ``(LAM u t1 = LAM v t2)``
181     |> SIMP_CONV (srw_ss()) [LAM_def, LAM_termP, term_ABS_pseudo11,
182                              GLAM_eq_thm, term_REP_11, GSYM term_REP_tpm,
183                              GSYM supp_tpm]
184     |> GENL [``u:string``, ``v:string``, ``t1:term``, ``t2:term``]);
185
186
187
188
189val (_, repty) = dom_rng (type_of term_REP_t)
190val repty' = ty_antiq repty
191
192val tlf =
193  ``��(v:string) (u:unit + unit) (ds1:(�� -> ��) list) (ds2:(�� -> ��)  list)
194                                (ts1:^repty' list) (ts2:^repty' list) (p:��).
195       if ISR u then tlf (HD ds1) v (term_ABS (HD ts1)) p: ��
196       else taf (HD ds2) (HD (TL ds2)) (term_ABS (HD ts2))
197                (term_ABS (HD (TL ts2))) p: ��``
198val tvf = ``��(s:string) (u:unit) (p:��). tvf s p : ��``
199
200val LENGTH_NIL' =
201    CONV_RULE (BINDER_CONV (LAND_CONV (REWR_CONV EQ_SYM_EQ)))
202              listTheory.LENGTH_NIL
203val LENGTH1 = prove(
204  ``(1 = LENGTH l) ��� ���e. l = [e]``,
205  Cases_on `l` >> srw_tac [][listTheory.LENGTH_NIL]);
206val LENGTH2 = prove(
207  ``(2 = LENGTH l) ��� ���a b. l = [a;b]``,
208  Cases_on `l` >> srw_tac [][LENGTH1]);
209
210val termP_elim = prove(
211  ``(���g. ^termP g ��� P g) ��� (���t. P (^term_REP_t t))``,
212  srw_tac [][EQ_IMP_THM] >- srw_tac [][genind_term_REP] >>
213  first_x_assum (qspec_then `^term_ABS_t g` mp_tac) >>
214  srw_tac [][repabs_pseudo_id]);
215
216val termP_removal =
217    nomdatatype.termP_removal {
218      elimth = termP_elim, absrep_id = absrep_id,
219      tpm_def = AP_TERM term_ABS_t term_REP_tpm |> REWRITE_RULE [absrep_id],
220      termP = termP, repty = repty}
221
222val termP0 = prove(
223  ``genind ^vp ^lp n t <=> ^termP t ��� (n = 0)``,
224  EQ_TAC >> simp_tac (srw_ss()) [] >> strip_tac >>
225  qsuff_tac `n = 0` >- (strip_tac >> srw_tac [][]) >>
226  pop_assum mp_tac >>
227  Q.ISPEC_THEN `t` STRUCT_CASES_TAC gterm_cases >>
228  srw_tac [][genind_GVAR, genind_GLAM_eqn]);
229
230
231
232val parameter_tm_recursion = save_thm(
233  "parameter_tm_recursion",
234  parameter_gtm_recursion
235      |> INST_TYPE [alpha |-> ``:unit + unit``, beta |-> ``:unit``,
236                    gamma |-> alpha]
237      |> Q.INST [`lf` |-> `^tlf`, `vf` |-> `^tvf`, `vp` |-> `^vp`,
238                 `lp` |-> `^lp`, `n` |-> `0`]
239      |> SIMP_RULE (srw_ss()) [sumTheory.FORALL_SUM, FORALL_AND_THM,
240                               GSYM RIGHT_FORALL_IMP_THM, IMP_CONJ_THM,
241                               GSYM RIGHT_EXISTS_AND_THM,
242                               GSYM LEFT_EXISTS_AND_THM,
243                               GSYM LEFT_FORALL_IMP_THM,
244                               LIST_REL_CONS1, genind_GVAR,
245                               genind_GLAM_eqn, sidecond_def,
246                               NEWFCB_def, relsupp_def,
247                               LENGTH_NIL', LENGTH1, LENGTH2]
248      |> ONCE_REWRITE_RULE [termP0]
249      |> SIMP_RULE (srw_ss() ++ DNF_ss) [LENGTH1, LENGTH2,
250                                         listTheory.LENGTH_NIL]
251      |> CONV_RULE (DEPTH_CONV termP_removal)
252      |> SIMP_RULE (srw_ss()) [GSYM supp_tpm, SYM term_REP_tpm]
253      |> UNDISCH
254      |> rpt_hyp_dest_conj
255      |> lift_exfunction {repabs_pseudo_id = repabs_pseudo_id,
256                          term_REP_t = term_REP_t,
257                          cons_info = cons_info}
258      |> DISCH_ALL
259      |> elim_unnecessary_atoms {finite_fv = FINITE_FV}
260                                [ASSUME ``FINITE (A:string set)``,
261                                 ASSUME ``!p:��. FINITE (supp ppm p)``]
262      |> UNDISCH_ALL |> DISCH_ALL
263      |> REWRITE_RULE [AND_IMP_INTRO]
264      |> CONV_RULE (LAND_CONV (REWRITE_CONV [GSYM CONJ_ASSOC]))
265      |> Q.INST [`tvf` |-> `vr`, `tlf` |-> `lm`, `taf` |-> `ap`,
266                 `dpm` |-> `apm`]
267      |> CONV_RULE (REDEPTH_CONV sort_uvars))
268
269val FORALL_ONE = prove(
270  ``(!u:one. P u) = P ()``,
271  SRW_TAC [][EQ_IMP_THM, oneTheory.one_induction]);
272val FORALL_ONE_FN = prove(
273  ``(!uf : one -> 'a. P uf) = !a. P (\u. a)``,
274  SRW_TAC [][EQ_IMP_THM] THEN
275  POP_ASSUM (Q.SPEC_THEN `uf ()` MP_TAC) THEN
276  Q_TAC SUFF_TAC `(\y. uf()) = uf` THEN1 SRW_TAC [][] THEN
277  SRW_TAC [][FUN_EQ_THM, oneTheory.one]);
278
279val EXISTS_ONE_FN = prove(
280  ``(?f : 'a -> one -> 'b. P f) = (?f : 'a -> 'b. P (\x u. f x))``,
281  SRW_TAC [][EQ_IMP_THM] THENL [
282    Q.EXISTS_TAC `\a. f a ()` THEN SRW_TAC [][] THEN
283    Q_TAC SUFF_TAC `(\x u. f x ()) = f` THEN1 SRW_TAC [][] THEN
284    SRW_TAC [][FUN_EQ_THM, oneTheory.one],
285    Q.EXISTS_TAC `\a u. f a` THEN SRW_TAC [][]
286  ]);
287
288val tm_recursion = save_thm(
289  "tm_recursion",
290  parameter_tm_recursion
291      |> Q.INST_TYPE [`:��` |-> `:unit`]
292      |> Q.INST [`ppm` |-> `discrete_pmact`, `vr` |-> `��s u. vru s`,
293                 `ap` |-> `��r1 r2 t1 t2 u. apu (r1()) (r2()) t1 t2`,
294                 `lm` |-> `��r v t u. lmu (r()) v t`]
295      |> SIMP_RULE (srw_ss()) [FORALL_ONE, FORALL_ONE_FN, EXISTS_ONE_FN,
296                               fnpm_def]
297      |> SIMP_RULE (srw_ss() ++ CONJ_ss) [supp_unitfn]
298      |> Q.INST [`apu` |-> `ap`, `lmu` |-> `lm`, `vru` |-> `vr`])
299
300val tm_recursion_nosideset = save_thm(
301  "tm_recursion_nosideset",
302  tm_recursion |> Q.INST [`A` |-> `{}`]
303               |> REWRITE_RULE [NOT_IN_EMPTY, FINITE_EMPTY]);
304
305val FV_tpm = Save_thm("FV_tpm",
306                      ``x ��� FV (tpm p t)``
307                      |> REWRITE_CONV [perm_supp,pmact_IN]
308                      |> GEN_ALL);
309
310val _ = set_mapped_fixity { term_name = "APP", tok = "@@",
311                            fixity = Infixl 901}
312
313val FRESH_APP = Store_thm(
314  "FRESH_APP",
315  ``v NOTIN FV (M @@ N) <=> v NOTIN FV M /\ v NOTIN FV N``,
316  SRW_TAC [][]);
317val FRESH_LAM = Store_thm(
318  "FRESH_LAM",
319  ``u NOTIN FV (LAM v M) <=> (u <> v ==> u NOTIN FV M)``,
320  SRW_TAC [][] THEN METIS_TAC []);
321val FV_EMPTY = store_thm(
322  "FV_EMPTY",
323  ``(FV t = {}) <=> !v. v NOTIN FV t``,
324  SIMP_TAC (srw_ss()) [EXTENSION]);
325
326(* quote the term in order to get the variable names specified *)
327val simple_induction = store_thm(
328  "simple_induction",
329  ``!P. (!s. P (VAR s)) /\
330        (!M N. P M /\ P N ==> P (M @@ N)) /\
331        (!v M. P M ==> P (LAM v M)) ==>
332        !M. P M``,
333  METIS_TAC [nc_INDUCTION2, FINITE_EMPTY, NOT_IN_EMPTY])
334
335val tpm_eqr = store_thm(
336  "tpm_eqr",
337  ``(t = tpm pi u) = (tpm (REVERSE pi) t = u)``,
338  METIS_TAC [pmact_inverse]);
339
340val tpm_CONS = store_thm(
341  "tpm_CONS",
342  ``tpm ((x,y)::pi) t = tpm [(x,y)] (tpm pi t)``,
343  SRW_TAC [][GSYM pmact_decompose]);
344
345val tpm_ALPHA = store_thm(
346  "tpm_ALPHA",
347  ``v ��� FV u ==> (LAM x u = LAM v (tpm [(v,x)] u))``,
348  SRW_TAC [boolSimps.CONJ_ss][LAM_eq_thm, pmact_flip_args]);
349
350(* cases theorem *)
351val term_CASES = store_thm(
352  "term_CASES",
353  ``!t. (?s. t = VAR s) \/ (?t1 t2. t = t1 @@ t2) \/ (?v t0. t = LAM v t0)``,
354  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN METIS_TAC []);
355
356(* should derive automatically *)
357val term_distinct = Store_thm(
358  "term_distinct",
359  ``VAR s ��� APP t1 t2 ��� VAR s ��� LAM v t ��� APP t1 t2 ��� LAM v t``,
360  srw_tac [][VAR_def, APP_def, LAM_def, LAM_termP, VAR_termP, APP_termP,
361             term_ABS_pseudo11, gterm_distinct, GLAM_eq_thm]);
362
363val term_11 = Store_thm(
364  "term_11",
365  ``((VAR s1 = VAR s2) <=> (s1 = s2)) ���
366    ((t11 @@ t12 = t21 @@ t22) <=> (t11 = t21) ��� (t12 = t22)) ���
367    ((LAM v t1 = LAM v t2) <=> (t1 = t2))``,
368  srw_tac [][VAR_def, APP_def, LAM_def, LAM_termP, VAR_termP, APP_termP,
369             term_ABS_pseudo11, gterm_11, term_REP_11]);
370
371(* "acyclicity" *)
372val APP_acyclic = store_thm(
373  "APP_acyclic",
374  ``!t1 t2. t1 <> t1 @@ t2 /\ t1 <> t2 @@ t1``,
375  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
376
377val FORALL_TERM = store_thm(
378  "FORALL_TERM",
379  ``(���t. P t) <=>
380      (���s. P (VAR s)) ��� (���t1 t2. P (t1 @@ t2)) ��� (���v t. P (LAM v t))``,
381  EQ_TAC THEN SRW_TAC [][] THEN
382  Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN SRW_TAC [][]);
383
384(* ----------------------------------------------------------------------
385    Establish substitution function
386   ---------------------------------------------------------------------- *)
387
388val tpm_COND = prove(
389  ``tpm pi (if P then x else y) = if P then tpm pi x else tpm pi y``,
390  SRW_TAC [][]);
391
392val tpm_apart = store_thm(
393  "tpm_apart",
394  ``!t. ~(x IN FV t) /\ (y IN FV t) ==> ~(tpm [(x,y)] t = t)``,
395  metis_tac[supp_apart, pmact_flip_args]);
396
397val tpm_fresh = store_thm(
398  "tpm_fresh",
399  ``���t x y. x ��� FV t ��� y ��� FV t ==> (tpm [(x,y)] t = t)``,
400  srw_tac [][supp_fresh]);
401
402val rewrite_pairing = prove(
403  ``(���f: term -> (string # term) -> term. P f) <=>
404    (���f: term -> string -> term -> term. P (��M (x,N). f N x M))``,
405  EQ_TAC >> strip_tac >| [
406    qexists_tac `��N x M. f M (x,N)` >> srw_tac [][] >>
407    CONV_TAC (DEPTH_CONV pairLib.PAIRED_ETA_CONV) >>
408    srw_tac [ETA_ss][],
409    qexists_tac `��M (x,N). f N x M` >> srw_tac [][]
410  ]);
411
412val subst_exists =
413    parameter_tm_recursion
414        |> INST_TYPE [alpha |-> ``:term``, ``:��`` |-> ``:string # term``]
415        |> SPEC_ALL
416        |> Q.INST [`A` |-> `{}`, `apm` |-> `^t_pmact_t`,
417                   `ppm` |-> `pair_pmact string_pmact ^t_pmact_t`,
418                   `vr` |-> `\s (x,N). if s = x then N else VAR s`,
419                   `ap` |-> `\r1 r2 t1 t2 p. r1 p @@ r2 p`,
420                   `lm` |-> `\r v t p. LAM v (r p)`]
421        |> CONV_RULE (LAND_CONV (SIMP_CONV (srw_ss()) [pairTheory.FORALL_PROD]))
422        |> SIMP_RULE (srw_ss()) [support_def, FUN_EQ_THM, fnpm_def,
423                                 tpm_COND, tpm_fresh, pmact_sing_inv,
424                                 basic_swapTheory.swapstr_eq_left]
425        |> SIMP_RULE (srw_ss()) [rewrite_pairing, pairTheory.FORALL_PROD]
426        |> CONV_RULE (DEPTH_CONV (rename_vars [("p_1", "u"), ("p_2", "N")]))
427        |> prove_alpha_fcbhyp {ppm = ``pair_pmact string_pmact ^t_pmact_t``,
428                               rwts = [],
429                               alphas = [tpm_ALPHA]}
430
431val SUB_DEF = new_specification("SUB_DEF", ["SUB"], subst_exists)
432
433val _ = add_rule {term_name = "SUB", fixity = Closefix,
434                  pp_elements = [TOK "[", TM, TOK "/", TM, TOK "]"],
435                  paren_style = OnlyIfNecessary,
436                  block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2))};
437
438(* Give substitution theorems names compatible with historical usage *)
439
440val SUB_THMv = prove(
441  ``([N/x](VAR x) = N) /\ (~(x = y) ==> ([N/y](VAR x) = VAR x))``,
442  SRW_TAC [][SUB_DEF]);
443val SUB_COMM = prove(
444  ``���N x x' y t.
445        x' ��� x ��� x' ��� FV N ��� y ��� x ��� y ��� FV N ���
446        (tpm [(x',y)] ([N/x] t) = [N/x] (tpm [(x',y)] t))``,
447  srw_tac [][SUB_DEF, supp_fresh]);
448
449
450val SUB_THM = save_thm(
451  "SUB_THM",
452  let val (eqns,_) = CONJ_PAIR SUB_DEF
453  in
454    CONJ (REWRITE_RULE [GSYM CONJ_ASSOC]
455                       (LIST_CONJ (SUB_THMv :: tl (CONJUNCTS eqns))))
456         SUB_COMM
457  end)
458val _ = export_rewrites ["SUB_THM"]
459val SUB_VAR = save_thm("SUB_VAR", hd (CONJUNCTS SUB_DEF))
460
461(* ----------------------------------------------------------------------
462    Results about substitution
463   ---------------------------------------------------------------------- *)
464
465Theorem fresh_tpm_subst:
466  !t. ~(u IN FV t) ==> (tpm [(u,v)] t = [VAR u/v] t)
467Proof
468  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN
469  SRW_TAC [][SUB_THM, SUB_VAR]
470QED
471
472Theorem tpm_subst:
473  !N. tpm pi ([M/v] N) = [tpm pi M/lswapstr pi v] (tpm pi N)
474Proof
475  HO_MATCH_MP_TAC nc_INDUCTION2 THEN
476  Q.EXISTS_TAC `v INSERT FV M` THEN
477  SRW_TAC [][SUB_THM, SUB_VAR] THEN
478  MATCH_MP_TAC (SUB_THM |> CONJUNCTS |> C (curry List.nth) 3 |> GSYM) THEN
479  SRW_TAC [][stringpm_raw]
480QED
481
482Theorem tpm_subst_out:
483  [M/v] (tpm pi N) = tpm pi ([tpm (REVERSE pi) M/lswapstr (REVERSE pi) v] N)
484Proof SRW_TAC [][tpm_subst]
485QED
486
487Theorem lemma14a[simp]:
488  !t. [VAR v/v] t = t
489Proof
490  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{v}` THEN
491  SRW_TAC [][SUB_THM, SUB_VAR]
492QED
493
494Theorem lemma14b:
495  !M. ~(v IN FV M) ==> ([N/v] M = M)
496Proof
497  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV N` THEN
498  SRW_TAC [][SUB_THM, SUB_VAR]
499QED
500
501Theorem lemma14c:
502  !t x u. x IN FV u ==> (FV ([t/x]u) = FV t UNION (FV u DELETE x))
503Proof
504  NTAC 2 GEN_TAC THEN HO_MATCH_MP_TAC nc_INDUCTION2 THEN
505  Q.EXISTS_TAC `x INSERT FV t` THEN
506  SRW_TAC [][SUB_THM, SUB_VAR, EXTENSION] THEN
507  METIS_TAC [lemma14b]
508QED
509
510Theorem FV_SUB:
511  !t u v. FV ([t/v] u) = if v ��� FV u then FV t ��� (FV u DELETE v) else FV u
512Proof PROVE_TAC [lemma14b, lemma14c]
513QED
514
515Theorem lemma15a:
516  !M. v ��� FV M ==> [N/v]([VAR v/x]M) = [N/x]M
517Proof
518  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v} UNION FV N` THEN
519  SRW_TAC [][SUB_THM, SUB_VAR]
520QED
521
522Theorem lemma15b:
523  v ��� FV M ==> [VAR u/v]([VAR v/u] M) = M
524Proof SRW_TAC [][lemma15a]
525QED
526
527(* ----------------------------------------------------------------------
528    alpha-convertibility results
529   ---------------------------------------------------------------------- *)
530
531Theorem SIMPLE_ALPHA:
532  y ��� FV u ==> !x. LAM x u = LAM y ([VAR y/x] u)
533Proof
534  SRW_TAC [][GSYM fresh_tpm_subst] THEN
535  SRW_TAC [boolSimps.CONJ_ss][LAM_eq_thm, pmact_flip_args]
536QED
537
538
539(* ----------------------------------------------------------------------
540    size function
541   ---------------------------------------------------------------------- *)
542
543val size_exists =
544    tm_recursion
545        |> INST_TYPE [alpha |-> ``:num``]
546        |> SPEC_ALL
547        |> Q.INST [`A` |-> `{}`, `apm` |-> `discrete_pmact`,
548             `vr` |-> `\s. 1`, `ap` |-> `\m n t1 t2. m + n + 1`,
549             `lm` |-> `\m v t. m + 1`]
550        |> SIMP_RULE (srw_ss()) []
551
552val size_def = new_specification("size_thm", ["size"], size_exists)
553Theorem size_thm[simp] = CONJUNCT1 size_def
554
555Theorem size_tpm[simp] = GSYM (CONJUNCT2 size_def)
556
557(* ----------------------------------------------------------------------
558    iterated substitutions (ugh)
559   ---------------------------------------------------------------------- *)
560
561Definition ISUB_def:
562     ($ISUB t [] = t)
563  /\ ($ISUB t ((s,x)::rst) = $ISUB ([s/x]t) rst)
564End
565
566val _ = set_fixity "ISUB" (Infixr 501);
567
568val DOM_DEF =
569 Define
570     `(DOM [] = {})
571  /\  (DOM ((x,y)::rst) = {y} UNION DOM rst)`;
572
573val FVS_DEF =
574 Define
575    `(FVS [] = {})
576 /\  (FVS ((t,x)::rst) = FV t UNION FVS rst)`;
577
578
579val FINITE_DOM = Q.store_thm("FINITE_DOM",
580 `!ss. FINITE (DOM ss)`,
581Induct THENL [ALL_TAC, Cases]
582   THEN RW_TAC std_ss [DOM_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_SING]);
583val _ = export_rewrites ["FINITE_DOM"]
584
585
586val FINITE_FVS = Q.store_thm("FINITE_FVS",
587`!ss. FINITE (FVS ss)`,
588Induct THENL [ALL_TAC, Cases]
589   THEN RW_TAC std_ss [FVS_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_FV]);
590val _ = export_rewrites ["FINITE_FVS"]
591
592val ISUB_LAM = store_thm(
593  "ISUB_LAM",
594  ``!R x. ~(x IN (DOM R UNION FVS R)) ==>
595          !t. (LAM x t) ISUB R = LAM x (t ISUB R)``,
596  Induct THEN
597  ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD,
598                           DOM_DEF, FVS_DEF, SUB_THM]);
599
600(* ----------------------------------------------------------------------
601    Simultaneous substitution (using a finite map) - much more interesting
602   ---------------------------------------------------------------------- *)
603
604val strterm_fmap_supp = store_thm(
605  "strterm_fmap_supp",
606  ``supp (fm_pmact string_pmact ^t_pmact_t) fmap =
607      FDOM fmap ���
608      supp (set_pmact ^t_pmact_t) (FRANGE fmap)``,
609  SRW_TAC [][fmap_supp]);
610
611val FINITE_strterm_fmap_supp = store_thm(
612  "FINITE_strterm_fmap_supp",
613  ``FINITE (supp (fm_pmact string_pmact ^t_pmact_t) fmap)``,
614  SRW_TAC [][strterm_fmap_supp, supp_setpm] THEN SRW_TAC [][]);
615val _ = export_rewrites ["FINITE_strterm_fmap_supp"]
616
617val lem1 = prove(
618  ``���a. ~(a ��� supp (fm_pmact string_pmact ^t_pmact_t) fm)``,
619  Q_TAC (NEW_TAC "z") `supp (fm_pmact string_pmact ^t_pmact_t) fm` THEN
620  METIS_TAC []);
621
622val supp_FRANGE = prove(
623  ``~(x ��� supp (set_pmact ^t_pmact_t) (FRANGE fm)) =
624   ���y. y ��� FDOM fm ==> ~(x ��� FV (fm ' y))``,
625  SRW_TAC [][supp_setpm, finite_mapTheory.FRANGE_DEF] THEN METIS_TAC []);
626
627fun ex_conj1 thm = let
628  val (v,c) = dest_exists (concl thm)
629  val c1 = CONJUNCT1 (ASSUME c)
630  val fm = mk_exists(v,concl c1)
631in
632  CHOOSE (v, thm) (EXISTS(fm,v) c1)
633end
634
635val supp_EMPTY = prove(
636  ``(supp (set_pmact apm) {} = {})``,
637  srw_tac [][EXTENSION] >> match_mp_tac notinsupp_I >>
638  qexists_tac `{}` >> srw_tac [][support_def]);
639
640
641val lem2 = prove(
642  ``���fm. FINITE (supp (set_pmact ^t_pmact_t) (FRANGE fm))``,
643  srw_tac [][supp_setpm] >> srw_tac [][]);
644
645val ordering = prove(
646  ``(���f. P f) <=> (���f. P (combin$C f))``,
647  srw_tac [][EQ_IMP_THM] >-
648    (qexists_tac `��x y. f y x` >> srw_tac [ETA_ss][combinTheory.C_DEF]) >>
649  metis_tac [])
650
651val notin_frange = prove(
652  ``v ��� supp (set_pmact ^t_pmact_t) (FRANGE p) <=> ���y. y ��� FDOM p ==> v ��� FV (p ' y)``,
653  srw_tac [][supp_setpm, EQ_IMP_THM, finite_mapTheory.FRANGE_DEF] >>
654  metis_tac []);
655
656val ssub_exists =
657    parameter_tm_recursion
658        |> INST_TYPE [alpha |-> ``:term``, ``:��`` |-> ``:string |-> term``]
659        |> Q.INST [`vr` |-> `\s fm. if s ��� FDOM fm then fm ' s else VAR s`,
660                   `lm` |-> `\r v t fm. LAM v (r fm)`, `apm` |-> `^t_pmact_t`,
661                   `ppm` |-> `fm_pmact string_pmact ^t_pmact_t`,
662                   `ap` |-> `\r1 r2 t1 t2 fm. r1 fm @@ r2 fm`,
663                   `A` |-> `{}`]
664        |> SIMP_RULE (srw_ss()) [tpm_COND, strterm_fmap_supp, lem2,
665                                 FAPPLY_eqv_lswapstr, supp_fresh,
666                                 pmact_sing_inv, fnpm_def,
667                                 fmpm_FDOM, notin_frange]
668        |> SIMP_RULE (srw_ss()) [Once ordering]
669        |> CONV_RULE (DEPTH_CONV (rename_vars [("p", "fm")]))
670        |> prove_alpha_fcbhyp {ppm = ``fm_pmact string_pmact ^t_pmact_t``,
671                               rwts = [notin_frange, strterm_fmap_supp],
672                               alphas = [tpm_ALPHA]}
673
674val ssub_def = new_specification ("ssub_def", ["ssub"], ssub_exists)
675val ssub_thm = Save_thm("ssub_thm", CONJUNCT1 ssub_def)
676
677val _ = overload_on ("'", ``ssub``)
678
679val tpm_ssub = save_thm("tpm_ssub", CONJUNCT2 ssub_def)
680
681val single_ssub = store_thm(
682  "single_ssub",
683  ``���N. (FEMPTY |+ (s,M)) ' N = [M/s]N``,
684  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `s INSERT FV M` THEN
685  SRW_TAC [][SUB_VAR, SUB_THM]);
686
687val in_fmap_supp = store_thm(
688  "in_fmap_supp",
689  ``x ��� supp (fm_pmact string_pmact ^t_pmact_t) fm <=>
690      x ��� FDOM fm ���
691      ���y. y ��� FDOM fm ��� x ��� FV (fm ' y)``,
692  SRW_TAC [][strterm_fmap_supp, nomsetTheory.supp_setpm] THEN
693  SRW_TAC [boolSimps.DNF_ss][finite_mapTheory.FRANGE_DEF] THEN METIS_TAC []);
694
695val not_in_fmap_supp = store_thm(
696  "not_in_fmap_supp",
697  ``x ��� supp (fm_pmact string_pmact ^t_pmact_t) fm <=>
698      x ��� FDOM fm ��� ���y. y ��� FDOM fm ==> x ��� FV (fm ' y)``,
699  METIS_TAC [in_fmap_supp]);
700val _ = export_rewrites ["not_in_fmap_supp"]
701
702val ssub_14b = store_thm(
703  "ssub_14b",
704  ``���t. (FV t ��� FDOM phi = EMPTY) ==> ((phi : string |-> term) ' t = t)``,
705  HO_MATCH_MP_TAC nc_INDUCTION2 THEN
706  Q.EXISTS_TAC `supp (fm_pmact string_pmact ^t_pmact_t) phi` THEN
707  SRW_TAC [][SUB_THM, SUB_VAR, pred_setTheory.EXTENSION] THEN METIS_TAC []);
708
709val ssub_value = store_thm(
710  "ssub_value",
711  ``(FV t = EMPTY) ==> ((phi : string |-> term) ' t = t)``,
712  SRW_TAC [][ssub_14b]);
713
714val ssub_FEMPTY = store_thm(
715  "ssub_FEMPTY",
716  ``���t. (FEMPTY:string|->term) ' t = t``,
717  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
718val _ = export_rewrites ["ssub_FEMPTY"]
719
720(* ----------------------------------------------------------------------
721    Set up the recursion functionality in binderLib
722   ---------------------------------------------------------------------- *)
723
724val lemma = prove(
725  ``(���x y t. pmact apm [(x,y)] (h t) = h (tpm [(x,y)] t)) <=>
726     ���pi t. pmact apm pi (h t) = h (tpm pi t)``,
727  simp_tac (srw_ss()) [EQ_IMP_THM] >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >>
728  strip_tac >> Induct_on `pi` >>
729  asm_simp_tac (srw_ss()) [pmact_nil, pairTheory.FORALL_PROD] >>
730  srw_tac [][Once tpm_CONS] >> srw_tac [][GSYM pmact_decompose]);
731
732val tm_recursion_nosideset = save_thm(
733  "tm_recursion_nosideset",
734  tm_recursion |> Q.INST [`A` |-> `{}`] |> SIMP_RULE (srw_ss()) [lemma])
735
736val term_info_string =
737    "local\n\
738    \fun k |-> v = {redex = k, residue = v}\n\
739    \open binderLib\n\
740    \val term_info = \n\
741    \   NTI {nullfv = ``LAM \"\" (VAR \"\")``,\n\
742    \        pm_rewrites = [],\n\
743    \        pm_constant = ``nomset$mk_pmact term$raw_tpm``,\n\
744    \        fv_rewrites = [],\n\
745    \        recursion_thm = SOME tm_recursion_nosideset,\n\
746    \        binders = [(``term$LAM``, 0, tpm_ALPHA)]}\n\
747    \val _ = type_db :=\n\
748    \          Binarymap.insert(!type_db,\n\
749    \                           {Name = \"term\",Thy=\"term\"},\n\
750    \                           term_info)\n\
751    \in end;\n"
752
753val _ = adjoin_after_completion (fn _ => PP.add_string term_info_string)
754
755
756val _ = export_theory()
757