src/Pure/meta_simplifier.ML
changeset 15001 fb2141a9f8c0
parent 14981 e73f8140af78
child 15006 107e4dfd3b96
     1.1 --- a/src/Pure/meta_simplifier.ML	Wed Jun 23 09:09:18 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Wed Jun 23 14:44:22 2004 +0200
     1.3 @@ -43,12 +43,8 @@
     1.4    val get_mk_sym        : meta_simpset -> thm -> thm option
     1.5    val get_mk_eq_True    : meta_simpset -> thm -> thm option
     1.6    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
     1.7 -  val beta_eta_conversion: cterm -> thm
     1.8    val rewrite_cterm: bool * bool * bool ->
     1.9      (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
    1.10 -  val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm
    1.11 -  val forall_conv       : (cterm -> thm) -> cterm -> thm
    1.12 -  val fconv_rule        : (cterm -> thm) -> thm -> thm
    1.13    val rewrite_aux       : (meta_simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
    1.14    val simplify_aux      : (meta_simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
    1.15    val rewrite_thm       : bool * bool * bool
    1.16 @@ -544,14 +540,10 @@
    1.17  val lhs_of = fst o dest_eq;
    1.18  val rhs_of = snd o dest_eq;
    1.19  
    1.20 -fun beta_eta_conversion t =
    1.21 -  let val thm = beta_conversion true t;
    1.22 -  in transitive thm (eta_conversion (rhs_of thm)) end;
    1.23 -
    1.24  fun check_conv msg thm thm' =
    1.25    let
    1.26      val thm'' = transitive thm (transitive
    1.27 -      (symmetric (beta_eta_conversion (lhs_of thm'))) thm')
    1.28 +      (symmetric (Drule.beta_eta_conversion (lhs_of thm'))) thm')
    1.29    in (if msg then trace_thm "SUCCEEDED" thm' else (); Some thm'') end
    1.30    handle THM _ =>
    1.31      let val {sign, prop = _ $ _ $ prop0, ...} = rep_thm thm;
    1.32 @@ -713,7 +705,7 @@
    1.33        fun err (msg, thm) = (trace_thm msg thm; None)
    1.34    in case prover thm' of
    1.35         None => err ("Congruence proof failed.  Could not prove", thm')
    1.36 -     | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
    1.37 +     | Some thm2 => (case check_conv true (Drule.beta_eta_conversion t) thm2 of
    1.38            None => err ("Congruence proof failed.  Should not have proved", thm2)
    1.39          | Some thm2' =>
    1.40              if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
    1.41 @@ -731,8 +723,6 @@
    1.42  fun transitive2 thm = transitive1 (Some thm);
    1.43  fun transitive3 thm = transitive1 thm o Some;
    1.44  
    1.45 -fun imp_cong' e = combination (combination refl_implies e);
    1.46 -
    1.47  fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
    1.48    let
    1.49      fun botc skel mss t =
    1.50 @@ -897,7 +887,7 @@
    1.51                val (rrs', asm') = rules_of_prem mss prem'
    1.52              in mut_impc prems concl rrss asms (prem' :: prems')
    1.53                (rrs' :: rrss') (asm' :: asms') (Some (foldr (disch true)
    1.54 -                (take (i, prems), imp_cong' eqn (reflexive (Drule.list_implies
    1.55 +                (take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies
    1.56                    (drop (i, prems), concl))))) :: eqns) mss (length prems') ~1
    1.57              end
    1.58  
    1.59 @@ -911,13 +901,13 @@
    1.60         in (case botc skel0 mss1 conc of
    1.61             None => (case thm1 of
    1.62                 None => None
    1.63 -             | Some thm1' => Some (imp_cong' thm1' (reflexive conc)))
    1.64 +             | Some thm1' => Some (Drule.imp_cong' thm1' (reflexive conc)))
    1.65           | Some thm2 =>
    1.66             let val thm2' = disch false (prem1, thm2)
    1.67             in (case thm1 of
    1.68                 None => Some thm2'
    1.69               | Some thm1' =>
    1.70 -                 Some (transitive (imp_cong' thm1' (reflexive conc)) thm2'))
    1.71 +                 Some (transitive (Drule.imp_cong' thm1' (reflexive conc)) thm2'))
    1.72             end)
    1.73         end
    1.74  
    1.75 @@ -947,29 +937,6 @@
    1.76      error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
    1.77        Pretty.string_of (Display.pretty_thms thms));
    1.78  
    1.79 -(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
    1.80 -fun goals_conv pred cv =
    1.81 -  let fun gconv i ct =
    1.82 -        let val (A,B) = Drule.dest_implies ct
    1.83 -        in imp_cong' (if pred i then cv A else reflexive A) (gconv (i+1) B) end
    1.84 -        handle TERM _ => reflexive ct
    1.85 -  in gconv 1 end;
    1.86 -
    1.87 -(* Rewrite A in !!x1,...,xn. A *)
    1.88 -fun forall_conv cv ct =
    1.89 -  let val p as (ct1, ct2) = Thm.dest_comb ct
    1.90 -  in (case pairself term_of p of
    1.91 -      (Const ("all", _), Abs (s, _, _)) =>
    1.92 -         let val (v, ct') = Thm.dest_abs (Some "@") ct2;
    1.93 -         in Thm.combination (Thm.reflexive ct1)
    1.94 -           (Thm.abstract_rule s v (forall_conv cv ct'))
    1.95 -         end
    1.96 -    | _ => cv ct)
    1.97 -  end handle TERM _ => cv ct;
    1.98 -
    1.99 -(*Use a conversion to transform a theorem*)
   1.100 -fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   1.101 -
   1.102  (*Rewrite a cterm*)
   1.103  fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)
   1.104    | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (mss_of thms);
   1.105 @@ -977,20 +944,20 @@
   1.106  (*Rewrite a theorem*)
   1.107  fun simplify_aux _ _ [] = (fn th => th)
   1.108    | simplify_aux prover full thms =
   1.109 -      fconv_rule (rewrite_cterm (full, false, false) prover (mss_of thms));
   1.110 +      Drule.fconv_rule (rewrite_cterm (full, false, false) prover (mss_of thms));
   1.111  
   1.112 -fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);
   1.113 +fun rewrite_thm mode prover mss = Drule.fconv_rule (rewrite_cterm mode prover mss);
   1.114  
   1.115  (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   1.116  fun rewrite_goals_rule_aux _ []   th = th
   1.117    | rewrite_goals_rule_aux prover thms th =
   1.118 -      fconv_rule (goals_conv (K true) (rewrite_cterm (true, true, false) prover
   1.119 +      Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, false) prover
   1.120          (mss_of thms))) th;
   1.121  
   1.122  (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   1.123  fun rewrite_goal_rule mode prover mss i thm =
   1.124    if 0 < i  andalso  i <= nprems_of thm
   1.125 -  then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   1.126 +  then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   1.127    else raise THM("rewrite_goal_rule",i,[thm]);
   1.128  
   1.129