src/Pure/Proof/proof_rewrite_rules.ML
author wenzelm
Sat May 15 23:23:45 2010 +0200 (2010-05-15)
changeset 36951 985c197f2fe9
parent 36744 6e1f3d609a68
child 37233 b78f31ca4675
permissions -rw-r--r--
renamed structure ValueParse to Parse_Value;
eliminated old-style structure alias V;
     1 (*  Title:      Pure/Proof/proof_rewrite_rules.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 Simplification functions for proof terms involving meta level rules.
     5 *)
     6 
     7 signature PROOF_REWRITE_RULES =
     8 sig
     9   val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
    10   val rprocs : bool ->
    11     (typ list -> Proofterm.proof -> (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 (_, (("Pure.protectD", _, _), _)) % _ %%
    38         (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
    39       | rew' (PThm (_, (("Pure.conjunctionD1", _, _), _)) % _ % _ %%
    40         (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% prf %% _)) = SOME prf
    41       | rew' (PThm (_, (("Pure.conjunctionD2", _, _), _)) % _ % _ %%
    42         (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
    43       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
    44         (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
    45       | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    46         (PAxm ("Pure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
    47             SOME (equal_intr_axm % B % A %% prf2 %% prf1)
    48 
    49       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    50         (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
    51           _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
    52         ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
    53         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    54 
    55       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    56         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    57           (PAxm ("Pure.combination", _, _) % SOME (Const ("prop", _)) %
    58              _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
    59         ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
    60         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
    61           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
    62 
    63       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    64         (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
    65           (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    66              (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    77         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    78           (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
    79             (PAxm ("Pure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
    80                (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    91         (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
    92           (PAxm ("Pure.reflexive", _, _) % _) %%
    93             (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   103         (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
   104           (PAxm ("Pure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
   105             (PAxm ("Pure.reflexive", _, _) % _) %%
   106               (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % SOME A % SOME C %%
   119         (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % SOME A % SOME C %%
   123         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   124           (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % _ % _ %%
   129         (PAxm ("Pure.reflexive", _, _) % _) %% prf) = SOME prf
   130       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   131         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   132           (PAxm ("Pure.reflexive", _, _) % _)) %% prf) = SOME prf
   133 
   134       | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   135         (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
   136 
   137       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   138         (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   139           (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   140             (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   141               (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % _ % _ %%
   147         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   148           (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   149             (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   150               (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   151                 (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % _ % _ %%
   157         (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   158           (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   159             (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   160               (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   161                 (PAxm ("Pure.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 ("Pure.equal_elim", _, _) % _ % _ %%
   167         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   168           (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   169             (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   170               (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   171                 (PAxm ("Pure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
   172                   (PAxm ("Pure.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 ("Pure.combination", _, _) %
   178         SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
   179           (PAxm ("Pure.reflexive", _, _) % _)) =
   180         let val (U, V) = (case T of
   181           Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
   182         in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
   183           (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
   184         end
   185 
   186       | rew' _ = NONE;
   187   in rew' #> Option.map (rpair no_skel) end;
   188 
   189 fun rprocs b = [rew b];
   190 val _ = Context.>> (Context.map_theory (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 =
   200           map Free (Name.invent_list (OldTerm.add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
   201         val t' = r (subst_bounds (frees, t));
   202         fun strip [] t = t
   203           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
   204       in
   205         strip Ts (fold lambda frees t')
   206       end;
   207 
   208     fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
   209       | rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
   210       | rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
   211       | rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
   212       | rew _ prf = prf
   213 
   214   in rew [] end;
   215 
   216 
   217 (**** eliminate definitions in proof ****)
   218 
   219 fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
   220 
   221 fun insert_refl defs Ts (prf1 %% prf2) =
   222       insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
   223   | insert_refl defs Ts (Abst (s, SOME T, prf)) =
   224       Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
   225   | insert_refl defs Ts (AbsP (s, t, prf)) =
   226       AbsP (s, t, insert_refl defs Ts prf)
   227   | insert_refl defs Ts prf = (case strip_combt prf of
   228         (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
   229           if member (op =) defs s then
   230             let
   231               val vs = vars_of prop;
   232               val tvars = Term.add_tvars prop [] |> rev;
   233               val (_, rhs) = Logic.dest_equals prop;
   234               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
   235                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
   236                 map the ts);
   237             in
   238               change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
   239             end
   240           else prf
   241       | (_, []) => prf
   242       | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
   243 
   244 fun elim_defs thy r defs prf =
   245   let
   246     val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
   247     val defnames = map Thm.derivation_name defs;
   248     val f = if not r then I else
   249       let
   250         val cnames = map (fst o dest_Const o fst) defs';
   251         val thms = fold_proof_atoms true
   252           (fn PThm (_, ((name, prop, _), _)) =>
   253               if member (op =) defnames name orelse
   254                 not (exists_Const (member (op =) cnames o #1) prop)
   255               then I
   256               else cons (name, SOME prop)
   257             | _ => I) [prf] [];
   258       in Reconstruct.expand_proof thy thms end;
   259   in
   260     rewrite_terms (Pattern.rewrite_term thy defs' [])
   261       (insert_refl defnames [] (f prf))
   262   end;
   263 
   264 
   265 (**** eliminate all variables that don't occur in the proposition ****)
   266 
   267 fun elim_vars mk_default prf =
   268   let
   269     val prop = Reconstruct.prop_of prf;
   270     val tv = Term.add_vars prop [];
   271     val tf = Term.add_frees prop [];
   272 
   273     fun hidden_variable (Var v) = not (member (op =) tv v)
   274       | hidden_variable (Free f) = not (member (op =) tf f)
   275       | hidden_variable _ = false;
   276 
   277     fun mk_default' T = list_abs
   278       (apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
   279 
   280     fun elim_varst (t $ u) = elim_varst t $ elim_varst u
   281       | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
   282       | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
   283       | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
   284       | elim_varst t = t;
   285   in
   286     map_proof_terms (fn t =>
   287       if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf
   288   end;
   289 
   290 
   291 (**** convert between hhf and non-hhf form ****)
   292 
   293 fun hhf_proof P Q prf =
   294   let
   295     val params = Logic.strip_params Q;
   296     val Hs = Logic.strip_assums_hyp P;
   297     val Hs' = Logic.strip_assums_hyp Q;
   298     val k = length Hs;
   299     val l = length params;
   300     fun mk_prf i j Hs Hs' (Const ("all", _) $ Abs (_, _, P)) prf =
   301           mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
   302       | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("==>", _) $ _ $ P) prf =
   303           mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
   304       | mk_prf _ _ _ _ _ prf = prf
   305   in
   306     prf |> Proofterm.incr_pboundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
   307     fold_rev (fn P => fn prf => AbsP ("H", SOME P, prf)) Hs' |>
   308     fold_rev (fn (s, T) => fn prf => Abst (s, SOME T, prf)) params
   309   end
   310 and un_hhf_proof P Q prf =
   311   let
   312     val params = Logic.strip_params Q;
   313     val Hs = Logic.strip_assums_hyp P;
   314     val Hs' = Logic.strip_assums_hyp Q;
   315     val k = length Hs;
   316     val l = length params;
   317     fun mk_prf (Const ("all", _) $ Abs (s, T, P)) prf =
   318           Abst (s, SOME T, mk_prf P prf)
   319       | mk_prf (Const ("==>", _) $ P $ Q) prf =
   320           AbsP ("H", SOME P, mk_prf Q prf)
   321       | mk_prf _ prf = prf
   322   in
   323     prf |> Proofterm.incr_pboundvars k l |>
   324     fold (fn i => fn prf => prf %> Bound i) (l - 1 downto 0) |>
   325     fold (fn ((H, H'), i) => fn prf => prf %% hhf_proof H' H (PBound i))
   326       (Hs ~~ Hs' ~~ (k - 1 downto 0)) |>
   327     mk_prf Q
   328   end;
   329 
   330 end;