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