- Moved abs_def to drule.ML
authorberghofe
Wed Jul 10 18:37:51 2002 +0200 (2002-07-10 ago)
changeset 13341f15ed50d16cf
parent 13340 9b0332344ae2
child 13342 915d4d004643
- Moved abs_def to drule.ML
- elim_defs now takes a boolean argument which controls the automatic
expansion of theorems mentioning constants whose definitions are
eliminated
src/Pure/Proof/proof_rewrite_rules.ML
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jul 10 18:35:34 2002 +0200
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jul 10 18:37:51 2002 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
     1.5    val rprocs : bool -> (string * (typ list -> Proofterm.proof -> Proofterm.proof option)) list
     1.6    val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
     1.7 -  val elim_defs : Sign.sg -> thm list -> Proofterm.proof -> Proofterm.proof
     1.8 +  val elim_defs : Sign.sg -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
     1.9    val setup : (theory -> theory) list
    1.10  end;
    1.11  
    1.12 @@ -211,15 +211,6 @@
    1.13  
    1.14  (**** eliminate definitions in proof ****)
    1.15  
    1.16 -fun abs_def thm =
    1.17 -  let
    1.18 -    val (_, cvs) = Drule.strip_comb (fst (dest_equals (cprop_of thm)));
    1.19 -    val thm' = foldr (fn (ct, thm) =>
    1.20 -      Thm.abstract_rule (fst (fst (dest_Var (term_of ct)))) ct thm) (cvs, thm);
    1.21 -  in
    1.22 -    MetaSimplifier.fconv_rule Thm.eta_conversion thm'
    1.23 -  end;
    1.24 -
    1.25  fun vars_of t = rev (foldl_aterms
    1.26    (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
    1.27  
    1.28 @@ -246,18 +237,23 @@
    1.29        | (_, []) => prf
    1.30        | (prf', ts) => proof_combt' (insert_refl defs Ts prf', ts));
    1.31  
    1.32 -fun elim_defs sign defs prf =
    1.33 +fun elim_defs sign r defs prf =
    1.34    let
    1.35      val tsig = Sign.tsig_of sign;
    1.36 -    val defs' = map (Logic.dest_equals o prop_of o abs_def) defs;
    1.37 +    val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
    1.38      val defnames = map Thm.name_of_thm defs;
    1.39 -    val cnames = map (fst o dest_Const o fst) defs';
    1.40 -    val thmnames = map fst (filter_out (fn (s, ps) =>
    1.41 -      null (foldr add_term_consts (map fst ps, []) inter cnames))
    1.42 -        (Symtab.dest (thms_of_proof Symtab.empty prf))) \\ defnames
    1.43 +    val f = if not r then I else
    1.44 +      let
    1.45 +        val cnames = map (fst o dest_Const o fst) defs';
    1.46 +        val thms = flat (map (fn (s, ps) =>
    1.47 +            if s mem defnames then []
    1.48 +            else map (pair s o Some o fst) (filter_out (fn (p, _) =>
    1.49 +              null (add_term_consts (p, []) inter cnames)) ps))
    1.50 +          (Symtab.dest (thms_of_proof Symtab.empty prf)))
    1.51 +      in Reconstruct.expand_proof sign thms end
    1.52    in
    1.53 -    rewrite_terms (Pattern.rewrite_term tsig defs' []) (insert_refl defnames []
    1.54 -      (Reconstruct.expand_proof sign thmnames prf))
    1.55 +    rewrite_terms (Pattern.rewrite_term tsig defs' [])
    1.56 +      (insert_refl defnames [] (f prf))
    1.57    end;
    1.58  
    1.59  end;