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