Removed practically all references to Library.foldr.
(* Title: Pure/Proof/proof_rewrite_rules.ML
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Simplification functions for proof terms involving meta level rules.
*)
signature PROOF_REWRITE_RULES =
sig
val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
val setup : (theory -> theory) list
end;
structure ProofRewriteRules : PROOF_REWRITE_RULES =
struct
open Proofterm;
fun rew b =
let
fun ? x = if b then SOME x else NONE;
fun ax (prf as PAxm (s, prop, _)) Ts =
if b then PAxm (s, prop, SOME Ts) else prf;
fun ty T = if b then
let val Type (_, [Type (_, [U, _]), _]) = T
in SOME U end
else NONE;
val equal_intr_axm = ax equal_intr_axm [];
val equal_elim_axm = ax equal_elim_axm [];
val symmetric_axm = ax symmetric_axm [propT];
fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
(PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = SOME prf
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
(PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
| rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
SOME (equal_intr_axm % B % A %% prf2 %% prf1)
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
_ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
_ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %%
(symmetric_axm % ? B % ? A %% prf1) %% prf2))
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) =
let
val _ $ A $ C = Envir.beta_norm X;
val _ $ B $ D = Envir.beta_norm Y
in SOME (AbsP ("H1", ? X, AbsP ("H2", ? B,
equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
(PBound 1 %% (equal_elim_axm %> B %> A %%
(symmetric_axm % ? A % ? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
end
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==>", _)) % _ % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2))) =
let
val _ $ A $ C = Envir.beta_norm Y;
val _ $ B $ D = Envir.beta_norm X
in SOME (AbsP ("H1", ? X, AbsP ("H2", ? A,
equal_elim_axm %> D %> C %%
(symmetric_axm % ? C % ? D %% incr_pboundvars 2 0 prf2)
%% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
end
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %%
(PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf))) =
let
val Const (_, T) $ P = Envir.beta_norm X;
val _ $ Q = Envir.beta_norm Y;
in SOME (AbsP ("H", ? X, Abst ("x", ty T,
equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
(incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
end
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME X % SOME Y %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("all", _)) % _ % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %%
(PAxm ("ProtoPure.abstract_rule", _, _) % _ % _ %% prf)))) =
let
val Const (_, T) $ P = Envir.beta_norm X;
val _ $ Q = Envir.beta_norm Y;
val t = incr_boundvars 1 P $ Bound 0;
val u = incr_boundvars 1 Q $ Bound 0
in SOME (AbsP ("H", ? X, Abst ("x", ty T,
equal_elim_axm %> t %> u %%
(symmetric_axm % ? u % ? t %% (incr_pboundvars 1 1 prf %> Bound 0))
%% (PBound 0 %> Bound 0))))
end
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
(PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2) %% prf3) =
SOME (equal_elim_axm %> B %> C %% prf2 %%
(equal_elim_axm %> A %> B %% prf1 %% prf3))
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME A % SOME C %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.transitive", _, _) % _ % SOME B % _ %% prf1 %% prf2)) %% prf3) =
SOME (equal_elim_axm %> B %> C %% (symmetric_axm % ? C % ? B %% prf1) %%
(equal_elim_axm %> A %> B %% (symmetric_axm % ? B % ? A %% prf2) %% prf3))
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf) = SOME prf
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _)) %% prf) = SOME prf
| rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf)) = SOME prf
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
(PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3) %% prf4) =
SOME (equal_elim_axm %> C %> D %% prf2 %%
(equal_elim_axm %> A %> C %% prf3 %%
(equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %% prf4)))
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A $ C) % SOME (_ $ B $ D) %%
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2) %% prf3)) %% prf4) =
SOME (equal_elim_axm %> A %> B %% prf1 %%
(equal_elim_axm %> C %> A %% (symmetric_axm % ? A % ? C %% prf3) %%
(equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %% prf4)))
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
(PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3) %% prf4) =
SOME (equal_elim_axm %> D %> C %% (symmetric_axm % ? C % ? D %% prf2) %%
(equal_elim_axm %> B %> D %% prf3 %%
(equal_elim_axm %> A %> B %% prf1 %% prf4)))
| rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ B $ D) % SOME (_ $ A $ C) %%
(PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
(PAxm ("ProtoPure.combination", _, _) % SOME (Const ("==", _)) % _ % _ % _ %%
(PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %% prf2)) %% prf3)) %% prf4) =
SOME (equal_elim_axm %> B %> A %% (symmetric_axm % ? A % ? B %% prf1) %%
(equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %%
(equal_elim_axm %> C %> D %% prf2 %% prf4)))
| rew' _ ((prf as PAxm ("ProtoPure.combination", _, _) %
SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
(PAxm ("ProtoPure.reflexive", _, _) % _)) =
let val (U, V) = (case T of
Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
in SOME (prf %% (ax combination_axm [V, U] %> eq % ? eq % ? t % ? t %%
(ax reflexive_axm [T] % ? eq) %% (ax reflexive_axm [U] % ? t)))
end
| rew' _ _ = NONE;
in rew' end;
fun rprocs b = [("Pure/meta_equality", rew b)];
val setup = [Proofterm.add_prf_rprocs (rprocs false)];
(**** apply rewriting function to all terms in proof ****)
fun rewrite_terms r =
let
fun rew_term Ts t =
let
val frees = map Free (variantlist
(replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts);
val t' = r (subst_bounds (frees, t));
fun strip [] t = t
| strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
in
strip Ts (Library.foldl (uncurry lambda o Library.swap) (t', frees))
end;
fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
| rew Ts (prf % SOME t) = rew Ts prf % SOME (rew_term Ts t)
| rew Ts (Abst (s, SOME T, prf)) = Abst (s, SOME T, rew (T :: Ts) prf)
| rew Ts (AbsP (s, SOME t, prf)) = AbsP (s, SOME (rew_term Ts t), rew Ts prf)
| rew _ prf = prf
in rew [] end;
(**** eliminate definitions in proof ****)
fun vars_of t = rev (foldl_aterms
(fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
fun insert_refl defs Ts (prf1 %% prf2) =
insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
| insert_refl defs Ts (Abst (s, SOME T, prf)) =
Abst (s, SOME T, insert_refl defs (T :: Ts) prf)
| insert_refl defs Ts (AbsP (s, t, prf)) =
AbsP (s, t, insert_refl defs Ts prf)
| insert_refl defs Ts prf = (case strip_combt prf of
(PThm ((s, _), _, prop, SOME Ts), ts) =>
if s mem defs then
let
val vs = vars_of prop;
val tvars = term_tvars prop;
val (_, rhs) = Logic.dest_equals prop;
val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
(foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
map valOf ts);
in
change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
end
else prf
| (_, []) => prf
| (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
fun elim_defs sign r defs prf =
let
val tsig = Sign.tsig_of sign;
val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
val defnames = map Thm.name_of_thm defs;
val f = if not r then I else
let
val cnames = map (fst o dest_Const o fst) defs';
val thms = List.concat (map (fn (s, ps) =>
if s mem defnames then []
else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
null (term_consts p inter cnames)) ps))
(Symtab.dest (thms_of_proof Symtab.empty prf)))
in Reconstruct.expand_proof sign thms end
in
rewrite_terms (Pattern.rewrite_term tsig defs' [])
(insert_refl defnames [] (f prf))
end;
(**** eliminate all variables that don't occur in the proposition ****)
fun elim_vars mk_default prf =
let
val prop = Reconstruct.prop_of prf;
val tv = term_vars prop;
val tf = term_frees prop;
fun mk_default' T = list_abs
(apfst (map (pair "x")) (apsnd mk_default (strip_type T)));
fun elim_varst (t $ u) = elim_varst t $ elim_varst u
| elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
| elim_varst (f as Free (_, T)) = if f mem tf then f else mk_default' T
| elim_varst (v as Var (_, T)) = if v mem tv then v else mk_default' T
| elim_varst t = t
in
map_proof_terms (fn t => if not (null (term_vars t \\ tv)) orelse
not (null (term_frees t \\ tf)) then Envir.beta_norm (elim_varst t)
else t) I prf
end;
end;