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