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