New function for eliminating definitions in proof term.
authorberghofe
Wed Feb 20 15:56:26 2002 +0100 (2002-02-20 ago)
changeset 12906165f4e1937f4
parent 12905 bbbae3f359e6
child 12907 27e6d344d724
New function for eliminating definitions in proof term.
src/Pure/Proof/proof_rewrite_rules.ML
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Feb 20 15:47:42 2002 +0100
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Feb 20 15:56:26 2002 +0100
     1.3 @@ -3,14 +3,15 @@
     1.4      Author:     Stefan Berghofer, TU Muenchen
     1.5      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.6  
     1.7 -Simplification function for partial proof terms involving
     1.8 -meta level rules.
     1.9 +Simplification functions for proof terms involving meta level rules.
    1.10  *)
    1.11  
    1.12  signature PROOF_REWRITE_RULES =
    1.13  sig
    1.14    val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
    1.15    val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
    1.16 +  val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
    1.17 +  val elim_defs : Sign.sg -> thm list -> Proofterm.proof -> Proofterm.proof
    1.18    val setup : (theory -> theory) list
    1.19  end;
    1.20  
    1.21 @@ -174,4 +175,80 @@
    1.22  fun rprocs b = [("Pure/meta_equality", rew b)];
    1.23  val setup = [Proofterm.add_prf_rprocs (rprocs false)];
    1.24  
    1.25 +
    1.26 +(**** apply rewriting function to all terms in proof ****)
    1.27 +
    1.28 +fun rewrite_terms r =
    1.29 +  let
    1.30 +    fun rew_term Ts t =
    1.31 +      let
    1.32 +        val frees = map Free (variantlist
    1.33 +          (replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts);
    1.34 +        val t' = r (subst_bounds (frees, t));
    1.35 +        fun strip [] t = t
    1.36 +          | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
    1.37 +      in
    1.38 +        strip Ts (foldl (uncurry lambda o Library.swap) (t', frees))
    1.39 +      end;
    1.40 +
    1.41 +    fun rew Ts (prf1 %% prf2) = rew Ts prf1 %% rew Ts prf2
    1.42 +      | rew Ts (prf % Some t) = rew Ts prf % Some (rew_term Ts t)
    1.43 +      | rew Ts (Abst (s, Some T, prf)) = Abst (s, Some T, rew (T :: Ts) prf)
    1.44 +      | rew Ts (AbsP (s, Some t, prf)) = AbsP (s, Some (rew_term Ts t), rew Ts prf)
    1.45 +      | rew _ prf = prf
    1.46 +
    1.47 +  in rew [] end;
    1.48 +
    1.49 +
    1.50 +(**** eliminate definitions in proof ****)
    1.51 +
    1.52 +fun abs_def thm =
    1.53 +  let
    1.54 +    val (_, cvs) = Drule.strip_comb (fst (dest_equals (cprop_of thm)));
    1.55 +    val thm' = foldr (fn (ct, thm) =>
    1.56 +      Thm.abstract_rule (fst (fst (dest_Var (term_of ct)))) ct thm) (cvs, thm);
    1.57 +  in
    1.58 +    MetaSimplifier.fconv_rule Thm.eta_conversion thm'
    1.59 +  end;
    1.60 +
    1.61 +fun vars_of t = rev (foldl_aterms
    1.62 +  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
    1.63 +
    1.64 +fun insert_refl defs Ts (prf1 %% prf2) =
    1.65 +      insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
    1.66 +  | insert_refl defs Ts (Abst (s, Some T, prf)) =
    1.67 +      Abst (s, Some T, insert_refl defs (T :: Ts) prf)
    1.68 +  | insert_refl defs Ts (AbsP (s, t, prf)) =
    1.69 +      AbsP (s, t, insert_refl defs Ts prf)
    1.70 +  | insert_refl defs Ts prf = (case strip_combt prf of
    1.71 +        (PThm ((s, _), _, prop, Some Ts), ts) =>
    1.72 +          if s mem defs then
    1.73 +            let
    1.74 +              val vs = vars_of prop;
    1.75 +              val tvars = term_tvars prop;
    1.76 +              val (_, rhs) = Logic.dest_equals prop;
    1.77 +              val rhs' = foldl betapply (subst_TVars (map fst tvars ~~ Ts)
    1.78 +                (foldr (fn p => Abs ("", dummyT, abstract_over p)) (vs, rhs)),
    1.79 +                map the ts);
    1.80 +            in
    1.81 +              change_type (Some [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
    1.82 +            end
    1.83 +          else prf
    1.84 +      | (_, []) => prf
    1.85 +      | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
    1.86 +
    1.87 +fun elim_defs sign defs prf =
    1.88 +  let
    1.89 +    val tsig = Sign.tsig_of sign;
    1.90 +    val defs' = map (Logic.dest_equals o prop_of o abs_def) defs;
    1.91 +    val defnames = map Thm.name_of_thm defs;
    1.92 +    val cnames = map (fst o dest_Const o fst) defs';
    1.93 +    val thmnames = map fst (filter_out (fn (s, ps) =>
    1.94 +      null (foldr add_term_consts (map fst ps, []) inter cnames))
    1.95 +        (Symtab.dest (thms_of_proof Symtab.empty prf))) \\ defnames
    1.96 +  in
    1.97 +    rewrite_terms (Pattern.rewrite_term tsig defs') (insert_refl defnames []
    1.98 +      (Reconstruct.expand_proof sign thmnames prf))
    1.99 +  end;
   1.100 +
   1.101  end;