src/Pure/Proof/proof_rewrite_rules.ML
author wenzelm
Fri Jul 15 15:44:15 2005 +0200 (2005-07-15 ago)
changeset 16861 7446b4be013b
parent 16787 b6b6e2faaa41
child 17018 1e9e0f5877f2
permissions -rw-r--r--
tuned fold on terms;
     1 (*  Title:      Pure/Proof/proof_rewrite_rules.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     5 Simplification functions for proof terms involving meta level rules.
     6 *)
     7 
     8 signature PROOF_REWRITE_RULES =
     9 sig
    10   val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
    11   val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
    12   val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
    13   val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
    14   val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
    15 end;
    16 
    17 structure ProofRewriteRules : PROOF_REWRITE_RULES =
    18 struct
    19 
    20 open Proofterm;
    21 
    22 fun rew b =
    23   let
    24     fun ? x = if b then SOME x else NONE;
    25     fun ax (prf as PAxm (s, prop, _)) Ts =
    26       if b then PAxm (s, prop, SOME Ts) else prf;
    27     fun ty T = if b then
    28         let val Type (_, [Type (_, [U, _]), _]) = T
    29         in SOME U end
    30       else NONE;
    31     val equal_intr_axm = ax equal_intr_axm [];
    32     val equal_elim_axm = ax equal_elim_axm [];
    33     val symmetric_axm = ax symmetric_axm [propT];
    34 
    35     fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
    36         (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = SOME prf
    37       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
    38         (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
    39       | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    40         (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
    41             SOME (equal_intr_axm % B % A %% prf2 %% prf1)
    42 
    43       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    44         (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
    45           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
    46         ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    47         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    48 
    49       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    50         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    51           (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
    52              _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
    53         ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    54         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
    55           (symmetric_axm % ? B % ? A %% prf1) %% prf2))
    56 
    57       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    58         (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    59           (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    60              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
    61         let
    62           val _ $ A $ C = Envir.beta_norm X;
    63           val _ $ B $ D = Envir.beta_norm Y
    64         in SOME (AbsP ("H1", ? X, AbsP ("H2", ? B,
    65           equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
    66             (PBound 1 %% (equal_elim_axm %> B %> A %%
    67               (symmetric_axm % ? A % ? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
    68         end
    69 
    70       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    71         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    72           (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    73             (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    74                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
    75         let
    76           val _ $ A $ C = Envir.beta_norm Y;
    77           val _ $ B $ D = Envir.beta_norm X
    78         in SOME (AbsP ("H1", ? X, AbsP ("H2", ? A,
    79           equal_elim_axm %> D %> C %%
    80             (symmetric_axm % ? C % ? D %% incr_pboundvars 2 0 prf2)
    81               %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
    82         end
    83 
    84       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    85         (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
    86           (PAxm ("ProtoPure.reflexive", _, _) % _) %%
    87             (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
    88         let
    89           val Const (_, T) $ P = Envir.beta_norm X;
    90           val _ $ Q = Envir.beta_norm Y;
    91         in SOME (AbsP ("H", ? X, Abst ("x", ty T,
    92             equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
    93               (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
    94         end
    95 
    96       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    97         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
    98           (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
    99             (PAxm ("ProtoPure.reflexive", _, _) % _) %%
   100               (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
   101         let
   102           val Const (_, T) $ P = Envir.beta_norm X;
   103           val _ $ Q = Envir.beta_norm Y;
   104           val t = incr_boundvars 1 P $ Bound 0;
   105           val u = incr_boundvars 1 Q $ Bound 0
   106         in SOME (AbsP ("H", ? X, Abst ("x", ty T,
   107           equal_elim_axm %> t %> u %%
   108             (symmetric_axm % ? u % ? t %% (incr_pboundvars 1 1 prf %> Bound 0))
   109               %% (PBound 0 %> Bound 0))))
   110         end
   111 
   112       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
   113         (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
   114            SOME (equal_elim_axm %> B %> C %% prf2 %%
   115              (equal_elim_axm %> A %> B %% prf1 %% prf3))
   116       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
   117         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   118           (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
   119            SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ? C % ? B %% prf1) %%
   120              (equal_elim_axm %> A %> B %% (symmetric_axm % ? B % ? A %% prf2) %% prf3))
   121 
   122       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   123         (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = SOME prf
   124       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   125         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   126           (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = SOME prf
   127 
   128       | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   129         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
   130 
   131       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   132         (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   133           (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   134             (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   135               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
   136           SOME (equal_elim_axm %> C %> D %% prf2 %%
   137             (equal_elim_axm %> A %> C %% prf3 %%
   138               (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% prf4)))
   139 
   140       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   141         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   142           (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   143             (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   144               (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   145                 (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
   146           SOME (equal_elim_axm %> A %> B %% prf1 %%
   147             (equal_elim_axm %> C %> A %% (symmetric_axm % ? A % ? C %% prf3) %%
   148               (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% prf4)))
   149 
   150       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   151         (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   152           (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   153             (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   154               (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   155                 (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
   156           SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %%
   157             (equal_elim_axm %> B %> D %% prf3 %%
   158               (equal_elim_axm %> A %> B %% prf1 %% prf4)))
   159 
   160       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   161         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   162           (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   163             (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   164               (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   165                 (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   166                   (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
   167           SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %%
   168             (equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %%
   169               (equal_elim_axm %> C %> D %% prf2 %% prf4)))
   170 
   171       | rew' _ ((prf as PAxm ("ProtoPure.combination", _, _) %
   172         SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
   173           (PAxm ("ProtoPure.reflexive", _, _) % _)) =
   174         let val (U, V) = (case T of
   175           Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
   176         in SOME (prf %% (ax combination_axm [V, U] %> eq % ? eq % ? t % ? t %%
   177           (ax reflexive_axm [T] % ? eq) %% (ax reflexive_axm [U] % ? t)))
   178         end
   179 
   180       | rew' _ _ = NONE;
   181   in rew' end;
   182 
   183 fun rprocs b = [("Pure/meta_equality", rew b)];
   184 val _ = Context.add_setup [Proofterm.add_prf_rprocs (rprocs false)];
   185 
   186 
   187 (**** apply rewriting function to all terms in proof ****)
   188 
   189 fun rewrite_terms r =
   190   let
   191     fun rew_term Ts t =
   192       let
   193         val frees = map Free (variantlist
   194           (replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts);
   195         val t' = r (subst_bounds (frees, t));
   196         fun strip [] t = t
   197           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
   198       in
   199         strip Ts (Library.foldl (uncurry lambda o Library.swap) (t', frees))
   200       end;
   201 
   202     fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
   203       | rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
   204       | rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
   205       | rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
   206       | rew _ prf = prf
   207 
   208   in rew [] end;
   209 
   210 
   211 (**** eliminate definitions in proof ****)
   212 
   213 fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
   214 
   215 fun insert_refl defs Ts (prf1 %% prf2) =
   216       insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
   217   | insert_refl defs Ts (Abst (s, SOME T, prf)) =
   218       Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
   219   | insert_refl defs Ts (AbsP (s, t, prf)) =
   220       AbsP (s, t, insert_refl defs Ts prf)
   221   | insert_refl defs Ts prf = (case strip_combt prf of
   222         (PThm ((s, _), _, prop, SOME Ts), ts) =>
   223           if s mem defs then
   224             let
   225               val vs = vars_of prop;
   226               val tvars = term_tvars prop;
   227               val (_, rhs) = Logic.dest_equals prop;
   228               val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
   229                 (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
   230                 map valOf ts);
   231             in
   232               change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
   233             end
   234           else prf
   235       | (_, []) => prf
   236       | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
   237 
   238 fun elim_defs sign r defs prf =
   239   let
   240     val tsig = Sign.tsig_of sign;
   241     val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
   242     val defnames = map Thm.name_of_thm defs;
   243     val f = if not r then I else
   244       let
   245         val cnames = map (fst o dest_Const o fst) defs';
   246         val thms = List.concat (map (fn (s, ps) =>
   247             if s mem defnames then []
   248             else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
   249               null (term_consts p inter cnames)) ps))
   250           (Symtab.dest (thms_of_proof Symtab.empty prf)))
   251       in Reconstruct.expand_proof sign thms end
   252   in
   253     rewrite_terms (Pattern.rewrite_term tsig defs' [])
   254       (insert_refl defnames [] (f prf))
   255   end;
   256 
   257 
   258 (**** eliminate all variables that don't occur in the proposition ****)
   259 
   260 fun elim_vars mk_default prf =
   261   let
   262     val prop = Reconstruct.prop_of prf;
   263     val tv = term_vars prop;
   264     val tf = term_frees prop;
   265 
   266     fun mk_default' T = list_abs
   267       (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
   268 
   269     fun elim_varst (t $ u) = elim_varst t $ elim_varst u
   270       | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
   271       | elim_varst (f as Free (_, T)) = if f mem tf then f else mk_default' T
   272       | elim_varst (v as Var (_, T)) = if v mem tv then v else mk_default' T
   273       | elim_varst t = t
   274   in
   275     map_proof_terms (fn t => if not (null (term_vars t \\ tv)) orelse
   276         not (null (term_frees t \\ tf)) then Envir.beta_norm (elim_varst t)
   277       else t) I prf
   278   end;
   279 
   280 end;