src/Pure/Proof/proof_rewrite_rules.ML
author wenzelm
Thu May 31 23:47:36 2007 +0200 (2007-05-31 ago)
changeset 23178 07ba6b58b3d2
parent 22662 3e492ba59355
child 26424 a6cad32a27b0
permissions -rw-r--r--
simplified/unified list fold;
     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 : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
    14   val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
    15   val hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
    16   val un_hhf_proof : term -> term -> Proofterm.proof -> Proofterm.proof
    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.protectD", _, _, _) % _ %%
    38         (PThm ("ProtoPure.protectI", _, _, _) % _ %% prf)) = SOME prf
    39       | rew' (PThm ("ProtoPure.conjunctionD1", _, _, _) % _ % _ %%
    40         (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf
    41       | rew' (PThm ("ProtoPure.conjunctionD2", _, _, _) % _ % _ %%
    42         (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf
    43       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
    44         (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
    45       | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    46         (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
    47             SOME (equal_intr_axm % B % A %% prf2 %% prf1)
    48 
    49       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    50         (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
    51           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
    52         ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
    53         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    54 
    55       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    56         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    57           (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
    58              _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
    59         ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
    60         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
    61           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
    62 
    63       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    64         (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    65           (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    66              (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
    67         let
    68           val _ $ A $ C = Envir.beta_norm X;
    69           val _ $ B $ D = Envir.beta_norm Y
    70         in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,
    71           equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
    72             (PBound 1 %% (equal_elim_axm %> B %> A %%
    73               (symmetric_axm % ?? A % ?? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
    74         end
    75 
    76       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    77         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    78           (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
    79             (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    80                (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
    81         let
    82           val _ $ A $ C = Envir.beta_norm Y;
    83           val _ $ B $ D = Envir.beta_norm X
    84         in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,
    85           equal_elim_axm %> D %> C %%
    86             (symmetric_axm % ?? C % ?? D %% incr_pboundvars 2 0 prf2)
    87               %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
    88         end
    89 
    90       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
    91         (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
    92           (PAxm ("ProtoPure.reflexive", _, _) % _) %%
    93             (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
    94         let
    95           val Const (_, T) $ P = Envir.beta_norm X;
    96           val _ $ Q = Envir.beta_norm Y;
    97         in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
    98             equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
    99               (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
   100         end
   101 
   102       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
   103         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%        
   104           (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
   105             (PAxm ("ProtoPure.reflexive", _, _) % _) %%
   106               (PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
   107         let
   108           val Const (_, T) $ P = Envir.beta_norm X;
   109           val _ $ Q = Envir.beta_norm Y;
   110           val t = incr_boundvars 1 P $ Bound 0;
   111           val u = incr_boundvars 1 Q $ Bound 0
   112         in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
   113           equal_elim_axm %> t %> u %%
   114             (symmetric_axm % ?? u % ?? t %% (incr_pboundvars 1 1 prf %> Bound 0))
   115               %% (PBound 0 %> Bound 0))))
   116         end
   117 
   118       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
   119         (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
   120            SOME (equal_elim_axm %> B %> C %% prf2 %%
   121              (equal_elim_axm %> A %> B %% prf1 %% prf3))
   122       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
   123         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   124           (PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
   125            SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ?? C % ?? B %% prf1) %%
   126              (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf2) %% prf3))
   127 
   128       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   129         (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = SOME prf
   130       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   131         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   132           (PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = SOME prf
   133 
   134       | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   135         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
   136 
   137       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   138         (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   139           (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   140             (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   141               (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
   142           SOME (equal_elim_axm %> C %> D %% prf2 %%
   143             (equal_elim_axm %> A %> C %% prf3 %%
   144               (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% prf4)))
   145 
   146       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   147         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   148           (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   149             (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   150               (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   151                 (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
   152           SOME (equal_elim_axm %> A %> B %% prf1 %%
   153             (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
   154               (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% prf4)))
   155 
   156       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   157         (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   158           (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   159             (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   160               (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   161                 (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
   162           SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
   163             (equal_elim_axm %> B %> D %% prf3 %%
   164               (equal_elim_axm %> A %> B %% prf1 %% prf4)))
   165 
   166       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
   167         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   168           (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   169             (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
   170               (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
   171                 (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   172                   (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
   173           SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
   174             (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
   175               (equal_elim_axm %> C %> D %% prf2 %% prf4)))
   176 
   177       | rew' ((prf as PAxm ("ProtoPure.combination", _, _) %
   178         SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
   179           (PAxm ("ProtoPure.reflexive", _, _) % _)) =
   180         let val (U, V) = (case T of
   181           Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
   182         in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %%
   183           (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
   184         end
   185 
   186       | rew' _ = NONE;
   187   in rew' end;
   188 
   189 fun rprocs b = [("Pure/meta_equality", rew b)];
   190 val _ = Context.add_setup (fold Proofterm.add_prf_rproc (rprocs false));
   191 
   192 
   193 (**** apply rewriting function to all terms in proof ****)
   194 
   195 fun rewrite_terms r =
   196   let
   197     fun rew_term Ts t =
   198       let
   199         val frees = map Free (Name.invent_list (add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
   200         val t' = r (subst_bounds (frees, t));
   201         fun strip [] t = t
   202           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
   203       in
   204         strip Ts (fold lambda frees t')
   205       end;
   206 
   207     fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
   208       | rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
   209       | rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
   210       | rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
   211       | rew _ prf = prf
   212 
   213   in rew [] end;
   214 
   215 
   216 (**** eliminate definitions in proof ****)
   217 
   218 fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
   219 
   220 fun insert_refl defs Ts (prf1 %% prf2) =
   221       insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
   222   | insert_refl defs Ts (Abst (s, SOME T, prf)) =
   223       Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
   224   | insert_refl defs Ts (AbsP (s, t, prf)) =
   225       AbsP (s, t, insert_refl defs Ts prf)
   226   | insert_refl defs Ts prf = (case strip_combt prf of
   227         (PThm (s, _, prop, SOME Ts), ts) =>
   228           if member (op =) defs s then
   229             let
   230               val vs = vars_of prop;
   231               val tvars = term_tvars prop;
   232               val (_, rhs) = Logic.dest_equals prop;
   233               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
   234                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
   235                 map the ts);
   236             in
   237               change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
   238             end
   239           else prf
   240       | (_, []) => prf
   241       | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
   242 
   243 fun elim_defs thy r defs prf =
   244   let
   245     val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
   246     val defnames = map Thm.get_name defs;
   247     val f = if not r then I else
   248       let
   249         val cnames = map (fst o dest_Const o fst) defs';
   250         val thms = maps (fn (s, ps) =>
   251             if member (op =) defnames s then []
   252             else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
   253               null (term_consts p inter cnames)) ps))
   254           (Symtab.dest (thms_of_proof prf Symtab.empty))
   255       in Reconstruct.expand_proof thy thms end
   256   in
   257     rewrite_terms (Pattern.rewrite_term thy defs' [])
   258       (insert_refl defnames [] (f prf))
   259   end;
   260 
   261 
   262 (**** eliminate all variables that don't occur in the proposition ****)
   263 
   264 fun elim_vars mk_default prf =
   265   let
   266     val prop = Reconstruct.prop_of prf;
   267     val tv = Term.add_vars prop [];
   268     val tf = Term.add_frees prop [];
   269 
   270     fun hidden_variable (Var v) = not (member (op =) tv v)
   271       | hidden_variable (Free f) = not (member (op =) tf f)
   272       | hidden_variable _ = false;
   273 
   274     fun mk_default' T = list_abs
   275       (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
   276 
   277     fun elim_varst (t $ u) = elim_varst t $ elim_varst u
   278       | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
   279       | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
   280       | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
   281       | elim_varst t = t;
   282   in
   283     map_proof_terms (fn t =>
   284       if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf
   285   end;
   286 
   287 
   288 (**** convert between hhf and non-hhf form ****)
   289 
   290 fun hhf_proof P Q prf =
   291   let
   292     val params = Logic.strip_params Q;
   293     val Hs = Logic.strip_assums_hyp P;
   294     val Hs' = Logic.strip_assums_hyp Q;
   295     val k = length Hs;
   296     val l = length params;
   297     fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf =
   298           mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
   299       | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf =
   300           mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
   301       | mk_prf _ _ _ _ _ prf = prf
   302   in
   303     prf |> Proofterm.incr_pboundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
   304     fold_rev (fn P => fn prf => AbsP ("H", SOME P, prf)) Hs' |>
   305     fold_rev (fn (s, T) => fn prf => Abst (s, SOME T, prf)) params
   306   end
   307 and un_hhf_proof P Q prf =
   308   let
   309     val params = Logic.strip_params Q;
   310     val Hs = Logic.strip_assums_hyp P;
   311     val Hs' = Logic.strip_assums_hyp Q;
   312     val k = length Hs;
   313     val l = length params;
   314     fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf =
   315           Abst (s, SOME T, mk_prf P prf)
   316       | mk_prf (Const ("==>", _) $ P $ Q) prf =
   317           AbsP ("H", SOME P, mk_prf Q prf)
   318       | mk_prf _ prf = prf
   319   in
   320     prf |> Proofterm.incr_pboundvars k l |>
   321     fold (fn i => fn prf => prf %> Bound i) (l - 1 downto 0) |>
   322     fold (fn ((H, H'), i) => fn prf => prf %% hhf_proof H' H (PBound i))
   323       (Hs ~~ Hs' ~~ (k - 1 downto 0)) |>
   324     mk_prf Q
   325   end;
   326 
   327 end;