1(* ===================================================================== *)
2(* FILE          : barendregt.sml                                        *)
3(* VERSION       : 1.0                                                   *)
4(* DESCRIPTION   : Tactics for working with substitutions naively.       *)
5(*                                                                       *)
6(* AUTHOR        : Peter Vincent Homeier                                 *)
7(* DATE          : September 3, 2000                                     *)
8(* COPYRIGHT     : Copyright (c) 2000 by Peter Vincent Homeier           *)
9(*                                                                       *)
10(* ===================================================================== *)
11
12
13structure barendregt :> barendregt =
14struct
15
16open HolKernel Parse boolLib;
17infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->;
18infixr -->;
19
20(*
21type term = Term.term
22type thm = Thm.thm;
23*)
24
25
26
27local
28
29
30(* In interactive sessions, do:
31
32app load ["pairTheory",
33          "listLib", "numTheory", "Num_induct",
34          "pred_setTheory", "pred_setLib",
35          "mutualLib", "ind_defLib", "bossLib",
36          "ind_rel", "dep_rewrite",
37          "more_listTheory", "more_setTheory", "variableTheory",
38          "termTheory", "alphaTheory", "liftTheory"
39         ];
40
41*)
42
43
44open pred_setTheory more_setTheory;
45open listTheory;
46open liftTheory;
47open dep_rewrite;
48open Rsyntax;
49
50
51val LIST_INDUCT_TAC =
52    INDUCT_THEN list_induction ASSUME_TAC;
53
54val REWRITE_THM = fn th => REWRITE_TAC[th];
55val UNDISCH_LAST_TAC = POP_ASSUM MP_TAC;
56
57fun REWRITE_ASSUM_TAC rths :tactic =
58    RULE_ASSUM_TAC (REWRITE_RULE rths);
59
60fun REWRITE_ALL_TAC rths :tactic =
61    REWRITE_TAC rths  THEN
62    REWRITE_ASSUM_TAC rths;
63
64val REWRITE_ALL_THM = fn th => REWRITE_ALL_TAC[th];
65
66
67
68(*
69val (asl,gl) = top_goal();
70*)
71
72
73fun TACTIC_ERR{function,message} =
74    Feedback.HOL_ERR{origin_structure = "Tactic",
75                     origin_function = function,
76                     message = message};
77
78fun failwith function =
79   ( (* if debug_fail then
80         print_string ("Failure in Cond_rewrite: "^function^"\n")
81     else (); *)
82    raise TACTIC_ERR{function = function,message = ""});
83
84
85fun mk_subst l = map (fn (residue:'a, redex:'b) =>
86                         {redex=redex,residue=residue}) l;
87val INST_TY_TERM = (Drule.INST_TY_TERM) o (mk_subst##mk_subst);
88fun dest_subst l = map (fn {residue,redex} => (residue:'a, redex:'b)) l;
89
90
91
92val get_shift_matches = (dest_subst##dest_subst) o
93                        (Term.match_term ���Lam x t :'a term���);
94(*
95val get_shift_matches = Psyntax.match_term ���Lam x t :'a term���;
96*)
97
98(* SEARCH_matches applies the function f to every subterm of the
99   given term tm, except to variables or constants, for which
100   SEARCH_matches always raises an exception.
101   The return value is a list of 'a objects, as produced by f
102   for every subterm of tm, all collected into one list.
103*)
104fun SEARCH_matches (f:term->'a list) tm =
105   ( (* if debug_matches then (print_string "SEARCH_matches: ";
106                    print_term tm; print_newline()) else (); *)
107    if is_comb tm then
108       (let val {Rator,Rand} = Rsyntax.dest_comb tm
109            val m1 = (f Rator handle _ => [])
110            val m2 = (f Rand  handle _ => [])
111         in  append m1 m2
112        end)
113    else
114    if is_abs tm then
115       let val {Bvar,Body} = Rsyntax.dest_abs tm in
116           (f Body handle _ => [])
117       end
118    else failwith "SEARCH_matches");
119
120(*
121fun SUB_matches (f:term->'a) tm =
122   ( (* if debug_matches then (print_string "SUB_matches: ";
123                    print_term tm; print_newline()) else (); *)
124    if is_comb tm then
125       (let val {Rator,Rand} = Rsyntax.dest_comb tm in
126        (f Rator handle _ => f Rand)
127        end)
128    else
129    if is_abs tm then
130       let val {Bvar,Body} = Rsyntax.dest_abs tm in
131           f Body
132       end
133    else failwith "SUB_matches");
134
135fun ONCE_DEPTH_matches (f:term->'a) tm =
136     ( (* if debug_matches then
137        (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline())
138      else (); *)
139       (f tm handle _ => (SUB_matches (ONCE_DEPTH_matches f) tm)));
140*)
141
142fun ALL_DEPTH_matches (f:term->'a) tm =
143     ( (* if debug_matches then
144        (print_string "ONCE_DEPTH_matches: "; print_term tm; print_newline())
145      else (); *)
146       ([f tm] handle _ => (SEARCH_matches (ALL_DEPTH_matches f) tm)));
147
148
149fun remove_s_matches matches =
150    let val (terms_list,types_list) = matches;
151        val nsterms = filter (fn (f,s) => not (#Name(dest_var s) = "s"))
152                             terms_list
153    in
154        (nsterms,([]:(hol_type * hol_type) list))
155    end;
156
157
158(* ------------------------------------------------------------------ *)
159(* Need to group together matches which have the same "x" match;      *)
160(* for each such group, we should compute a variant of the x once,    *)
161(* and then use the same variant x' for each of the new shifted       *)
162(* bodies of the SIGMA expressions.  This ensures that SIGMA        *)
163(* expressions which had identical bound variables before, still      *)
164(* have identical bound variables afterwards.  This is important.     *)
165(* ------------------------------------------------------------------ *)
166
167fun find_x (match::matches) =
168    let val (l,r) = match in
169      if r = ���x:var��� then l else find_x matches
170    end
171  | find_x [] = ���x:var���;
172
173fun find_t (match::matches) =
174    let val (l,r) = match in
175      if r = ���t:'a term��� then l else find_t matches
176    end
177  | find_t [] = ���t:'a term���;
178
179fun sort_matches matchesl =
180    let val (mtermsl,_) = split matchesl
181        val xtms = map find_x mtermsl
182        val dist_xtms = mk_set xtms
183        val xs_termsl = zip xtms mtermsl
184        val xmgroups = map (fn dx => filter (fn (x,matches) => (x = dx))
185                                            xs_termsl)
186                           dist_xtms
187        val mgroups = map (map snd) xmgroups
188        val t's = map (map find_t) mgroups
189        val mtygroups = map (map (fn tms =>
190                                     (tms, ([]:(hol_type * hol_type) list))))
191                            mgroups
192        val tmgroups = zip (zip dist_xtms t's) mtygroups
193    in
194        tmgroups
195    end;
196
197
198
199val EVERY_LENGTH_LEMMA = TAC_PROOF(([],
200    ���!os (a:'a) as.
201         (LENGTH os = LENGTH (CONS a as)) ==>
202         (?(o':'b) os'. (LENGTH os' = LENGTH as) /\ (os = CONS o' os'))���),
203    LIST_INDUCT_TAC
204    THEN REWRITE_TAC[LENGTH,arithmeticTheory.SUC_NOT]
205    THEN REWRITE_TAC[prim_recTheory.INV_SUC_EQ,CONS_11]
206    THEN REPEAT GEN_TAC THEN STRIP_TAC
207    THEN EXISTS_TAC ���h:'b���
208    THEN EXISTS_TAC ���os:'b list���
209    THEN ASM_REWRITE_TAC[]
210   );
211
212val NIL_LENGTH_LEMMA = TAC_PROOF(([],
213    ���!os:'b list.
214         (LENGTH os = LENGTH ([]:'a list)) ==>
215         (os = [])���),
216    REWRITE_TAC[LENGTH,LENGTH_NIL]
217   );
218
219fun REPEAT_N 0 tac = ALL_TAC
220  | REPEAT_N n tac = (tac THEN REPEAT_N (n-1) tac);
221
222
223
224fun make_new_objects thm =
225    let val cn = concl thm
226        val rhs = #rhs(dest_eq cn)
227        val lst = #Rand(dest_comb rhs)
228        fun length_list lst =
229             if lst = ���[]:obj list��� then 0
230             else  1 + length_list (#Rand(dest_comb lst))
231        val n = length_list lst
232        fun make_one 0 thm = thm
233          | make_one n thm = thm
234    in
235        (make_one n thm; n)
236    end;
237
238
239(*
240fun MAKE_CLEAN_VAR_THM free_vrs matches =
241    let val (terms_list,types_list) = matches;
242        val ftm = foldr (fn (x,s) =>
243                           if type_of x = (==`:var`==)
244                             then ���^x INSERT ^s���
245                           else if type_of x = (==`:var list`==)
246                             then ���SL ^x UNION ^s���
247                           else if type_of x = (==`:var set`==)
248                             then ���^x UNION ^s���
249                           else if type_of x = (==`:'a term`==)
250                             then ���(FV ^x) UNION ^s���
251                           else s)
252                         ���{}:var set���
253                         free_vrs;
254        val sterms = (ftm, ���s:var set���)::terms_list;
255        val smatches = (sterms,([]:(hol_type * hol_type) list));
256        val sigma_thm = INST_TY_TERM smatches (SPEC_ALL SIGMA_CLEAN_VAR);
257    in
258        REWRITE_RULE[FINITE_EMPTY,FINITE_INSERT,FINITE_UNION,
259                     FINITE_FV_object,IN,IN_UNION,DE_MORGAN_THM]
260                   sigma_thm
261    end;
262*)
263
264
265fun MAKE_LIST_CLEAN_VAR_THM free_vrs (x, os) =
266    let val ftm = foldr (fn (x,s) =>
267                           if type_of x = (==`:var`==)
268                             then ���^x INSERT ^s���
269                           else if type_of x = (==`:var list`==)
270                             then ���SL ^x UNION ^s���
271                           else if type_of x = (==`:var set`==)
272                             then ���^x UNION ^s���
273                           else if type_of x = (==`:'a term`==)
274                             then ���(FV ^x) UNION ^s���
275                           else s)
276                         ���{}:var set���
277                         free_vrs;
278         val mk_term_list = foldr (fn (a,os) => ���CONS ^a ^os���)
279                                 ���[]:'a term list���
280         val os_tm = mk_term_list os
281         val lambda_thm = SPECL[ftm,x,os_tm] LAMBDA_LIST_CLEAN_VAR
282         val exists_list_thm =
283                REWRITE_RULE[FINITE_EMPTY,FINITE_INSERT,FINITE_UNION,
284                             FINITE_FV,IN,IN_UNION,DE_MORGAN_THM]
285                           lambda_thm
286         val os' = foldr (fn (v,l) => (Term.variant (l @ free_vrs) v)::l)
287                         [] os
288         val os'_tm = mk_term_list os'
289         val {Bvar=zvar, Body=body1} = dest_exists (concl exists_list_thm)
290         val {Rator=exists_binder, Rand=body2} = dest_comb body1
291         val os'_vr = #Bvar(dest_abs body2)
292         val exists_tm1 = beta_conv (mk_comb{Rator=body2, Rand=os'_tm})
293         val exists_tm2 = foldr (fn (o1,tm) => mk_exists{Bvar=o1, Body=tm})
294                                exists_tm1  os'
295         val exists_tm  = mk_exists{Bvar=zvar, Body=exists_tm2}
296         val exists_thm = TAC_PROOF (([],exists_tm),
297               STRIP_ASSUME_TAC exists_list_thm
298               THEN ASSUM_LIST (fn asl1 =>
299                      EXISTS_TAC (#Rand (dest_comb (#Rator(dest_comb
300                            (#Rand(dest_comb (concl (hd (rev asl1))))))))))
301               THEN REPEAT
302                     (POP_ASSUM (fn lth =>
303                         STRIP_ASSUME_TAC (MATCH_MP EVERY_LENGTH_LEMMA lth))
304                      THEN FIRST_ASSUM (fn eth =>
305                           EXISTS_TAC
306                             (#Rand (dest_comb (#Rator(dest_comb
307                                  (#rhs(dest_eq (concl eth))))))))
308                      THEN POP_ASSUM REWRITE_ALL_THM)
309               THEN POP_ASSUM (REWRITE_ALL_THM o MATCH_MP NIL_LENGTH_LEMMA)
310               THEN ASM_REWRITE_TAC[LENGTH]
311          )
312    in
313         BETA_RULE (REWRITE_RULE[EVERY_DEF,MAP2,combinTheory.I_THM] exists_thm)
314    end;
315
316
317val MAKE_SIMPLE_SUBST_TAC =
318    DEP_REWRITE_TAC[LAMBDA_SUBST_SIMPLE]
319    THEN CONJ_TAC
320    THENL
321      [ ASM_REWRITE_TAC[termTheory.BV_subst_def,pairTheory.FST,IN]
322        THEN REPEAT (CHANGED_TAC
323               (ASM_REWRITE_TAC[IN_DIFF,IN,FV_term,FV_term_subst]
324                THEN DEP_REWRITE_TAC[NOT_IN_FV_subst,NOT_IN_FV_subst2]))
325        THEN ASM_REWRITE_TAC[],
326
327        ALL_TAC
328      ];
329
330
331(*
332val SHIFT_LAMBDA_TAC :tactic = fn (asl,gl) =>
333    let val matches = ONCE_DEPTH_matches get_shift_matches gl;
334        val free_vrs = mk_set (append (free_vars gl)
335                                      (flatten (map free_vars asl)));
336        val lambda_thm = MAKE_CLEAN_VAR_THM free_vrs matches
337    in
338        (STRIP_ASSUME_TAC lambda_thm
339         THEN FIRST_ASSUM REWRITE_THM
340         THEN UNDISCH_LAST_TAC
341         THEN FIRST_ASSUM (fn hght => EVERY_ASSUM (fn th =>
342                             ASSUME_TAC (MATCH_MP th hght)
343                             handle _ => ALL_TAC))
344         THEN DISCH_TAC) (asl,gl)
345    end;
346*)
347
348val SHIFT_LAMBDAS_TAC :tactic = fn (asl,gl) =>
349    let val matchesl = mk_set (ALL_DEPTH_matches get_shift_matches gl);
350        val match_groups = sort_matches matchesl
351        val (tags,groups) = split match_groups
352        (* val (xs,bodies) = split tags *)
353        val free_vrs = mk_set (append (free_vars gl)
354                                      (flatten (map free_vars asl)));
355        val lambda_thms = map (MAKE_LIST_CLEAN_VAR_THM free_vrs) tags
356        val t_lambda_thms = zip tags lambda_thms
357      (*  val lambda_thm = map (MAKE_CLEAN_VAR_THM free_vrs) matchesl *)
358    in
359       if matchesl = [] then
360          ONCE_REWRITE_TAC[SUB_term] (asl,gl)
361       else
362       (EVERY (map (fn ((x,os),lambda_thm) =>
363         let val n = length os in
364          STRIP_ASSUME_TAC lambda_thm
365          THEN POP_ASSUM (fn th => ALL_TAC)
366          THEN REPEAT_N n
367                  (FIRST_ASSUM REWRITE_THM THEN UNDISCH_LAST_TAC)
368          THEN REPEAT_N n UNDISCH_LAST_TAC (* the HEIGHT = HEIGHT asms *)
369          THEN REPEAT_N n
370                  (DISCH_THEN (fn hght =>
371                                 EVERY_ASSUM (fn th =>
372                                    ASSUME_TAC (MATCH_MP th hght)
373                                     handle _ => ALL_TAC)
374                                 THEN ASSUME_TAC hght))
375          THEN REPEAT_N n DISCH_TAC
376         end)
377                   t_lambda_thms) )
378       (* above is tactic, applied to: *)
379       (asl,gl)
380    end;
381
382
383(* ================================================================== *)
384(* End of local declarations.                                         *)
385(* Beginning of exported declarations.                                *)
386(* ================================================================== *)
387
388in
389
390
391val SHIFT_LAMBDAS_TAC = SHIFT_LAMBDAS_TAC;
392
393
394val MAKE_SIMPLE_SUBST_TAC = MAKE_SIMPLE_SUBST_TAC;
395
396val SIMPLE_SUBST_TAC =
397        SHIFT_LAMBDAS_TAC THEN MAKE_SIMPLE_SUBST_TAC;
398
399
400end (* of local declaration block *)
401
402end;  (* of structure barendregt *)
403
404
405(* TEST EXAMPLES:
406
407load "MutualIndThen";
408open MutualIndThen;
409
410(* Barendregt's Substitution Lemma, 2.1.16, page 27: *)
411
412val BARENDREGT_SUBSTITUTION_LEMMA = TAC_PROOF
413   (([],
414    ���!(M:'a term) N L x y.
415          ~(x = y) /\ ~(x IN FV L) ==>
416          (((M <[ [x,N]) <[ [y,L]) =
417           ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))���),
418    MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC
419    THENL
420      [ (* Con case *)
421        REPEAT STRIP_TAC
422        THEN REWRITE_TAC[SUB_term,SUB],
423
424        (* Var case *)
425        REPEAT STRIP_TAC
426        THEN REWRITE_TAC[SUB_term,SUB]
427        THEN COND_CASES_TAC
428        THENL
429          [ ASM_REWRITE_TAC[SUB_term,SUB],
430
431            REWRITE_TAC[SUB_term,SUB]
432            THEN COND_CASES_TAC
433            THENL
434              [ IMP_RES_THEN REWRITE_THM subst_EMPTY,
435
436                ASM_REWRITE_TAC[SUB_term,SUB]
437              ]
438          ],
439
440        (* App case *)
441        REPEAT STRIP_TAC
442        THEN RES_TAC
443        THEN ASM_REWRITE_TAC[SUB_term],
444
445        (* Lam case *)
446        REPEAT STRIP_TAC
447        THEN SIMPLE_SUBST_TAC
448        THEN DEP_ASM_REWRITE_TAC[]
449      ]
450   );
451
452*)
453