src/Pure/Proof/proof_rewrite_rules.ML
author wenzelm
Fri Oct 07 21:16:48 2016 +0200 (2016-10-07)
changeset 64092 95469c544b82
parent 62922 96691631c1eb
child 70412 64ead6de6212
permissions -rw-r--r--
accept obscure timezone used in 2011;
     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 -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
    10   val rprocs : bool ->
    11     (typ list -> term option list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
    12   val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
    13   val elim_defs : Proof.context -> 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   val mk_of_sort_proof : Proof.context -> term option list -> typ * sort -> Proofterm.proof list
    18   val expand_of_class : Proof.context -> typ list -> term option list -> Proofterm.proof ->
    19     (Proofterm.proof * Proofterm.proof) option
    20 end;
    21 
    22 structure ProofRewriteRules : PROOF_REWRITE_RULES =
    23 struct
    24 
    25 fun rew b _ _ =
    26   let
    27     fun ?? x = if b then SOME x else NONE;
    28     fun ax (prf as PAxm (s, prop, _)) Ts =
    29       if b then PAxm (s, prop, SOME Ts) else prf;
    30     fun ty T = if b then
    31         let val Type (_, [Type (_, [U, _]), _]) = T
    32         in SOME U end
    33       else NONE;
    34     val equal_intr_axm = ax Proofterm.equal_intr_axm [];
    35     val equal_elim_axm = ax Proofterm.equal_elim_axm [];
    36     val symmetric_axm = ax Proofterm.symmetric_axm [propT];
    37 
    38     fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %%
    39         (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
    40       | rew' (PThm (_, (("Pure.conjunctionD1", _, _), _)) % _ % _ %%
    41         (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% prf %% _)) = SOME prf
    42       | rew' (PThm (_, (("Pure.conjunctionD2", _, _), _)) % _ % _ %%
    43         (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
    44       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
    45         (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
    46       | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    47         (PAxm ("Pure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
    48             SOME (equal_intr_axm % B % A %% prf2 %% prf1)
    49 
    50       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    51         (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
    52           _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
    53         ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
    54         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    55 
    56       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    57         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    58           (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
    59              _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
    60         ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
    61         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
    62           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
    63 
    64       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    65         (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
    66           (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
    67              (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) =
    68         let
    69           val _ $ A $ C = Envir.beta_norm X;
    70           val _ $ B $ D = Envir.beta_norm Y
    71         in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,
    72           Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_pboundvars 2 0 prf2 %%
    73             (PBound 1 %% (equal_elim_axm %> B %> A %%
    74               (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_pboundvars 2 0 prf1) %%
    75                 PBound 0)))))
    76         end
    77 
    78       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    79         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
    80           (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
    81             (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.imp", _)) % _ % _ % _ %%
    82                (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2))) =
    83         let
    84           val _ $ A $ C = Envir.beta_norm Y;
    85           val _ $ B $ D = Envir.beta_norm X
    86         in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,
    87           equal_elim_axm %> D %> C %%
    88             (symmetric_axm % ?? C % ?? D %% Proofterm.incr_pboundvars 2 0 prf2) %%
    89               (PBound 1 %%
    90                 (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0)))))
    91         end
    92 
    93       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
    94         (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
    95           (PAxm ("Pure.reflexive", _, _) % _) %%
    96             (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf))) =
    97         let
    98           val Const (_, T) $ P = Envir.beta_norm X;
    99           val _ $ Q = Envir.beta_norm Y;
   100         in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
   101             equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
   102               (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
   103         end
   104 
   105       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
   106         (PAxm ("Pure.symmetric", _, _) % _ % _ %%        
   107           (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.all", _)) % _ % _ % _ %%
   108             (PAxm ("Pure.reflexive", _, _) % _) %%
   109               (PAxm ("Pure.abstract_rule", _, _) % _ % _ %% prf)))) =
   110         let
   111           val Const (_, T) $ P = Envir.beta_norm X;
   112           val _ $ Q = Envir.beta_norm Y;
   113           val t = incr_boundvars 1 P $ Bound 0;
   114           val u = incr_boundvars 1 Q $ Bound 0
   115         in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
   116           equal_elim_axm %> t %> u %%
   117             (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_pboundvars 1 1 prf %> Bound 0))
   118               %% (PBound 0 %> Bound 0))))
   119         end
   120 
   121       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
   122         (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
   123            SOME (equal_elim_axm %> B %> C %% prf2 %%
   124              (equal_elim_axm %> A %> B %% prf1 %% prf3))
   125       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME A % SOME C %%
   126         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   127           (PAxm ("Pure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
   128            SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ?? C % ?? B %% prf1) %%
   129              (equal_elim_axm %> A %> B %% (symmetric_axm % ?? B % ?? A %% prf2) %% prf3))
   130 
   131       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   132         (PAxm ("Pure.reflexive", _, _) % _) %% prf) = SOME prf
   133       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   134         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   135           (PAxm ("Pure.reflexive", _, _) % _)) %% prf) = SOME prf
   136 
   137       | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   138         (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
   139 
   140       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   141         (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   142           (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   143             (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   144               (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
   145           SOME (equal_elim_axm %> C %> D %% prf2 %%
   146             (equal_elim_axm %> A %> C %% prf3 %%
   147               (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %% prf4)))
   148 
   149       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   150         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   151           (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
   152             (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   153               (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   154                 (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
   155           SOME (equal_elim_axm %> A %> B %% prf1 %%
   156             (equal_elim_axm %> C %> A %% (symmetric_axm % ?? A % ?? C %% prf3) %%
   157               (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %% prf4)))
   158 
   159       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   160         (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   161           (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   162             (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   163               (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   164                 (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
   165           SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ?? C % ?? D %% prf2) %%
   166             (equal_elim_axm %> B %> D %% prf3 %%
   167               (equal_elim_axm %> A %> B %% prf1 %% prf4)))
   168 
   169       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
   170         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   171           (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
   172             (PAxm ("Pure.symmetric", _, _) % _ % _ %%
   173               (PAxm ("Pure.combination", _, _) % _ % _ % _ % _ %%
   174                 (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.eq", _)) % _ % _ % _ %%
   175                   (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
   176           SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ?? A % ?? B %% prf1) %%
   177             (equal_elim_axm %> D %> B %% (symmetric_axm % ?? B % ?? D %% prf3) %%
   178               (equal_elim_axm %> C %> D %% prf2 %% prf4)))
   179 
   180       | rew' ((prf as PAxm ("Pure.combination", _, _) %
   181         SOME ((eq as Const ("Pure.eq", T)) $ t) % _ % _ % _) %%
   182           (PAxm ("Pure.reflexive", _, _) % _)) =
   183         let val (U, V) = (case T of
   184           Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
   185         in SOME (prf %% (ax Proofterm.combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
   186           (ax Proofterm.reflexive_axm [T] % ?? eq) %% (ax Proofterm.reflexive_axm [U] % ?? t)))
   187         end
   188 
   189       | rew' _ = NONE;
   190   in rew' #> Option.map (rpair Proofterm.no_skel) end;
   191 
   192 fun rprocs b = [rew b];
   193 val _ = Theory.setup (fold Proofterm.add_prf_rproc (rprocs false));
   194 
   195 
   196 (**** apply rewriting function to all terms in proof ****)
   197 
   198 fun rewrite_terms r =
   199   let
   200     fun rew_term Ts t =
   201       let
   202         val frees =
   203           map Free (Name.invent (Term.declare_term_frees t Name.context) "xa" (length Ts) ~~ Ts);
   204         val t' = r (subst_bounds (frees, t));
   205         fun strip [] t = t
   206           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
   207       in
   208         strip Ts (fold lambda frees t')
   209       end;
   210 
   211     fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
   212       | rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
   213       | rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
   214       | rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
   215       | rew _ prf = prf
   216 
   217   in rew [] end;
   218 
   219 
   220 (**** eliminate definitions in proof ****)
   221 
   222 fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
   223 
   224 fun insert_refl defs Ts (prf1 %% prf2) =
   225       let val (prf1', b) = insert_refl defs Ts prf1
   226       in
   227         if b then (prf1', true)
   228         else (prf1' %% fst (insert_refl defs Ts prf2), false)
   229       end
   230   | insert_refl defs Ts (Abst (s, SOME T, prf)) =
   231       (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
   232   | insert_refl defs Ts (AbsP (s, t, prf)) =
   233       (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
   234   | insert_refl defs Ts prf =
   235       (case Proofterm.strip_combt prf of
   236         (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
   237           if member (op =) defs s then
   238             let
   239               val vs = vars_of prop;
   240               val tvars = Term.add_tvars prop [] |> rev;
   241               val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
   242               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
   243                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
   244                 map the ts);
   245             in
   246               (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')])
   247                 Proofterm.reflexive_axm %> rhs', true)
   248             end
   249           else (prf, false)
   250       | (_, []) => (prf, false)
   251       | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
   252 
   253 fun elim_defs ctxt r defs prf =
   254   let
   255     val defs' = map (Logic.dest_equals o
   256       map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
   257     val defnames = map Thm.derivation_name defs;
   258     val f = if not r then I else
   259       let
   260         val cnames = map (fst o dest_Const o fst) defs';
   261         val thms = Proofterm.fold_proof_atoms true
   262           (fn PThm (_, ((name, prop, _), _)) =>
   263               if member (op =) defnames name orelse
   264                 not (exists_Const (member (op =) cnames o #1) prop)
   265               then I
   266               else cons (name, SOME prop)
   267             | _ => I) [prf] [];
   268       in Reconstruct.expand_proof ctxt thms end;
   269   in
   270     rewrite_terms (Pattern.rewrite_term (Proof_Context.theory_of ctxt) defs' [])
   271       (fst (insert_refl defnames [] (f prf)))
   272   end;
   273 
   274 
   275 (**** eliminate all variables that don't occur in the proposition ****)
   276 
   277 fun elim_vars mk_default prf =
   278   let
   279     val prop = Reconstruct.prop_of prf;
   280     val tv = Term.add_vars prop [];
   281     val tf = Term.add_frees prop [];
   282 
   283     fun hidden_variable (Var v) = not (member (op =) tv v)
   284       | hidden_variable (Free f) = not (member (op =) tf f)
   285       | hidden_variable _ = false;
   286 
   287     fun mk_default' T =
   288       fold_rev (Term.abs o pair "x") (binder_types T) (mk_default (body_type T));
   289 
   290     fun elim_varst (t $ u) = elim_varst t $ elim_varst u
   291       | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
   292       | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
   293       | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
   294       | elim_varst t = t;
   295   in
   296     Proofterm.map_proof_terms (fn t =>
   297       if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf
   298   end;
   299 
   300 
   301 (**** convert between hhf and non-hhf form ****)
   302 
   303 fun hhf_proof P Q prf =
   304   let
   305     val params = Logic.strip_params Q;
   306     val Hs = Logic.strip_assums_hyp P;
   307     val Hs' = Logic.strip_assums_hyp Q;
   308     val k = length Hs;
   309     val l = length params;
   310     fun mk_prf i j Hs Hs' (Const ("Pure.all", _) $ Abs (_, _, P)) prf =
   311           mk_prf i (j - 1) Hs Hs' P (prf %> Bound j)
   312       | mk_prf i j (H :: Hs) (H' :: Hs') (Const ("Pure.imp", _) $ _ $ P) prf =
   313           mk_prf (i - 1) j Hs Hs' P (prf %% un_hhf_proof H' H (PBound i))
   314       | mk_prf _ _ _ _ _ prf = prf
   315   in
   316     prf |> Proofterm.incr_pboundvars k l |> mk_prf (k - 1) (l - 1) Hs Hs' P |>
   317     fold_rev (fn P => fn prf => AbsP ("H", SOME P, prf)) Hs' |>
   318     fold_rev (fn (s, T) => fn prf => Abst (s, SOME T, prf)) params
   319   end
   320 and un_hhf_proof P Q prf =
   321   let
   322     val params = Logic.strip_params Q;
   323     val Hs = Logic.strip_assums_hyp P;
   324     val Hs' = Logic.strip_assums_hyp Q;
   325     val k = length Hs;
   326     val l = length params;
   327     fun mk_prf (Const ("Pure.all", _) $ Abs (s, T, P)) prf =
   328           Abst (s, SOME T, mk_prf P prf)
   329       | mk_prf (Const ("Pure.imp", _) $ P $ Q) prf =
   330           AbsP ("H", SOME P, mk_prf Q prf)
   331       | mk_prf _ prf = prf
   332   in
   333     prf |> Proofterm.incr_pboundvars k l |>
   334     fold (fn i => fn prf => prf %> Bound i) (l - 1 downto 0) |>
   335     fold (fn ((H, H'), i) => fn prf => prf %% hhf_proof H' H (PBound i))
   336       (Hs ~~ Hs' ~~ (k - 1 downto 0)) |>
   337     mk_prf Q
   338   end;
   339 
   340 
   341 (**** expand OfClass proofs ****)
   342 
   343 fun mk_of_sort_proof ctxt hs (T, S) =
   344   let
   345     val hs' = map
   346       (fn SOME t => (SOME (Logic.dest_of_class t) handle TERM _ => NONE)
   347         | NONE => NONE) hs;
   348     val sorts = AList.coalesce (op =) (rev (map_filter I hs'));
   349     fun get_sort T = the_default [] (AList.lookup (op =) sorts T);
   350     val subst = map_atyps
   351       (fn T as TVar (ixn, _) => TVar (ixn, get_sort T)
   352         | T as TFree (s, _) => TFree (s, get_sort T));
   353     fun hyp T_c = case find_index (equal (SOME T_c)) hs' of
   354         ~1 => error "expand_of_class: missing class hypothesis"
   355       | i => PBound i;
   356     fun reconstruct prf prop = prf |>
   357       Reconstruct.reconstruct_proof ctxt prop |>
   358       Reconstruct.expand_proof ctxt [("", NONE)] |>
   359       Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
   360   in
   361     map2 reconstruct
   362       (Proofterm.of_sort_proof (Proof_Context.theory_of ctxt)
   363         (OfClass o apfst Type.strip_sorts) (subst T, S))
   364       (Logic.mk_of_sort (T, S))
   365   end;
   366 
   367 fun expand_of_class ctxt Ts hs (OfClass (T, c)) =
   368       mk_of_sort_proof ctxt hs (T, [c]) |>
   369       hd |> rpair Proofterm.no_skel |> SOME
   370   | expand_of_class ctxt Ts hs _ = NONE;
   371 
   372 end;