moved some Drule operations to Thm (see more_thm.ML);
authorwenzelm
Thu May 10 00:39:48 2007 +0200 (2007-05-10)
changeset 22902ac833b4bb7ee
parent 22901 481cd919c47f
child 22903 95ad1a91ecef
moved some Drule operations to Thm (see more_thm.ML);
src/HOL/Import/shuffler.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/specification_package.ML
src/Pure/Tools/codegen_data.ML
src/Pure/Tools/codegen_funcgr.ML
src/Pure/Tools/nbe.ML
src/Pure/goal.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu May 10 00:39:46 2007 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu May 10 00:39:48 2007 +0200
     1.3 @@ -493,7 +493,7 @@
     1.4            addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
     1.5          fun chain f th =
     1.6              let
     1.7 -                val rhs = snd (dest_equals (cprop_of th))
     1.8 +                val rhs = Thm.rhs_of th
     1.9              in
    1.10                  transitive th (f rhs)
    1.11              end
    1.12 @@ -585,7 +585,7 @@
    1.13          val closed_t = Library.foldr (fn (v, body) =>
    1.14        let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
    1.15          val rew_th = norm_term thy closed_t
    1.16 -        val rhs = snd (dest_equals (cprop_of rew_th))
    1.17 +        val rhs = Thm.rhs_of rew_th
    1.18  
    1.19          val shuffles = ShuffleData.get thy
    1.20          fun process [] = NONE
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Thu May 10 00:39:46 2007 +0200
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu May 10 00:39:48 2007 +0200
     2.3 @@ -48,7 +48,7 @@
     2.4  
     2.5  (*Populate the abstraction cache with common combinators.*)
     2.6  fun seed th net =
     2.7 -  let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th)
     2.8 +  let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th)
     2.9        val t = Logic.legacy_varify (term_of ct)
    2.10    in  Net.insert_term Thm.eq_thm (t, th) net end;
    2.11    
    2.12 @@ -184,7 +184,7 @@
    2.13  (*Apply a function definition to an argument, beta-reducing the result.*)
    2.14  fun beta_comb cf x =
    2.15    let val th1 = combination cf (reflexive x)
    2.16 -      val th2 = beta_conversion false (Drule.rhs_of th1)
    2.17 +      val th2 = beta_conversion false (Thm.rhs_of th1)
    2.18    in  transitive th1 th2  end;
    2.19  
    2.20  (*Apply a function definition to arguments, beta-reducing along the way.*)
    2.21 @@ -259,7 +259,7 @@
    2.22                  val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else ();
    2.23                  val (u'_th,defs) = abstract thy cta
    2.24                  val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else ();
    2.25 -                val cu' = Drule.rhs_of u'_th
    2.26 +                val cu' = Thm.rhs_of u'_th
    2.27                  val u' = term_of cu'
    2.28                  val abs_v_u = lambda_list (map term_of cvs) u'
    2.29                  (*get the formal parameters: ALL variables free in the term*)
    2.30 @@ -335,7 +335,7 @@
    2.31                  val (cvs,cta) = dest_abs_list ct
    2.32                  val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
    2.33                  val (u'_th,defs) = abstract cta
    2.34 -                val cu' = Drule.rhs_of u'_th
    2.35 +                val cu' = Thm.rhs_of u'_th
    2.36                  val u' = term_of cu'
    2.37                  (*Could use Thm.cabs instead of lambda to work at level of cterms*)
    2.38                  val abs_v_u = lambda_list (map term_of cvs) (term_of cu')
    2.39 @@ -396,7 +396,7 @@
    2.40    an existential formula by a use of that function.
    2.41     Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
    2.42  fun skolem_of_def def =
    2.43 -  let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def))
    2.44 +  let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
    2.45        val (ch, frees) = c_variant_abs_multi (rhs, [])
    2.46        val (chilbert,cabs) = Thm.dest_comb ch
    2.47        val {thy,t, ...} = rep_cterm chilbert
     3.1 --- a/src/HOL/Tools/specification_package.ML	Thu May 10 00:39:46 2007 +0200
     3.2 +++ b/src/HOL/Tools/specification_package.ML	Thu May 10 00:39:48 2007 +0200
     3.3 @@ -123,7 +123,7 @@
     3.4          val rew_imps = alt_props |>
     3.5            map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd)
     3.6          val props' = rew_imps |>
     3.7 -          map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of)
     3.8 +          map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
     3.9  
    3.10          fun proc_single prop =
    3.11              let
     4.1 --- a/src/Pure/Tools/codegen_data.ML	Thu May 10 00:39:46 2007 +0200
     4.2 +++ b/src/Pure/Tools/codegen_data.ML	Thu May 10 00:39:48 2007 +0200
     4.3 @@ -707,7 +707,7 @@
     4.4  
     4.5  fun rhs_conv conv thm =
     4.6    let
     4.7 -    val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm;
     4.8 +    val thm' = (conv o Thm.rhs_of) thm;
     4.9    in Thm.transitive thm thm' end
    4.10  
    4.11  in
     5.1 --- a/src/Pure/Tools/codegen_funcgr.ML	Thu May 10 00:39:46 2007 +0200
     5.2 +++ b/src/Pure/Tools/codegen_funcgr.ML	Thu May 10 00:39:48 2007 +0200
     5.3 @@ -314,18 +314,18 @@
     5.4        fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
     5.5      fun rhs_conv conv thm =
     5.6        let
     5.7 -        val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm;
     5.8 +        val thm' = (conv o Thm.rhs_of) thm;
     5.9        in Thm.transitive thm thm' end
    5.10      val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
    5.11      val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
    5.12      val thm1 = CodegenData.preprocess_cterm ct
    5.13        |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
    5.14 -    val ct' = Drule.dest_equals_rhs (Thm.cprop_of thm1);
    5.15 +    val ct' = Thm.rhs_of thm1;
    5.16      val consts = consts_of thy (Thm.term_of ct');
    5.17      val funcgr' = ensure_consts rewrites thy consts funcgr;
    5.18      val algebra = CodegenData.coregular_algebra thy;
    5.19      val (_, thm2) = Thm.varifyT' [] thm1;
    5.20 -    val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_of thm2));
    5.21 +    val thm3 = Thm.reflexive (Thm.rhs_of thm2);
    5.22      val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.const_of_cexpr thy);
    5.23      val [thm4] = resort_thms algebra typ_funcgr [thm3];
    5.24      val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
    5.25 @@ -337,7 +337,7 @@
    5.26        in Thm.instantiate (instmap, []) thm end;
    5.27      val thm5 = inst thm2;
    5.28      val thm6 = inst thm4;
    5.29 -    val ct'' = Drule.dest_equals_rhs (Thm.cprop_of thm6);
    5.30 +    val ct'' = Thm.rhs_of thm6;
    5.31      val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
    5.32      val drop = drop_classes thy tfrees;
    5.33      val instdefs = instances_of_consts thy algebra funcgr' cs;
     6.1 --- a/src/Pure/Tools/nbe.ML	Thu May 10 00:39:46 2007 +0200
     6.2 +++ b/src/Pure/Tools/nbe.ML	Thu May 10 00:39:48 2007 +0200
     6.3 @@ -179,7 +179,7 @@
     6.4        let
     6.5          val t = Thm.term_of ct;
     6.6          val thm2 = normalization_invoke thy funcgr t;
     6.7 -        val thm3 = apply_posts thy ((snd o Drule.dest_equals o Thm.cprop_of) thm2);
     6.8 +        val thm3 = apply_posts thy (Thm.rhs_of thm2);
     6.9          val thm23 = drop_classes (Thm.transitive thm2 thm3);
    6.10        in
    6.11          Thm.transitive thm1 thm23 handle THM _ =>
     7.1 --- a/src/Pure/goal.ML	Thu May 10 00:39:46 2007 +0200
     7.2 +++ b/src/Pure/goal.ML	Thu May 10 00:39:48 2007 +0200
     7.3 @@ -49,7 +49,7 @@
     7.4    C ==> #C
     7.5  *)
     7.6  val init =
     7.7 -  let val A = #1 (Drule.dest_implies (Thm.cprop_of Drule.protectI))
     7.8 +  let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI))
     7.9    in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
    7.10  
    7.11  (*
     8.1 --- a/src/Pure/meta_simplifier.ML	Thu May 10 00:39:46 2007 +0200
     8.2 +++ b/src/Pure/meta_simplifier.ML	Thu May 10 00:39:48 2007 +0200
     8.3 @@ -460,7 +460,7 @@
     8.4      val {thy, prop, ...} = Thm.rep_thm thm;
     8.5      val prems = Logic.strip_imp_prems prop;
     8.6      val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
     8.7 -    val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
     8.8 +    val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
     8.9        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
    8.10      val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
    8.11      val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
    8.12 @@ -578,7 +578,7 @@
    8.13  fun add_cong (ss, thm) = ss |>
    8.14    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    8.15      let
    8.16 -      val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
    8.17 +      val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
    8.18          handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    8.19      (*val lhs = Envir.eta_contract lhs;*)
    8.20        val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
    8.21 @@ -828,7 +828,7 @@
    8.22  fun check_conv msg ss thm thm' =
    8.23    let
    8.24      val thm'' = transitive thm (transitive
    8.25 -      (symmetric (Drule.beta_eta_conversion (Drule.lhs_of thm'))) thm')
    8.26 +      (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
    8.27    in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
    8.28    handle THM _ =>
    8.29      let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
    8.30 @@ -890,16 +890,17 @@
    8.31    let
    8.32      val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
    8.33      val eta_thm = Thm.eta_conversion t;
    8.34 -    val eta_t' = Drule.rhs_of eta_thm;
    8.35 +    val eta_t' = Thm.rhs_of eta_thm;
    8.36      val eta_t = term_of eta_t';
    8.37      fun rew {thm, name, lhs, elhs, extra, fo, perm} =
    8.38        let
    8.39          val {thy, prop, maxidx, ...} = rep_thm thm;
    8.40          val (rthm, elhs') =
    8.41            if maxt = ~1 orelse not extra then (thm, elhs)
    8.42 -          else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
    8.43 -        val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
    8.44 -                          else Thm.cterm_match (elhs', eta_t');
    8.45 +          else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
    8.46 +        val insts =
    8.47 +          if fo then Thm.first_order_match (elhs', eta_t')
    8.48 +          else Thm.match (elhs', eta_t');
    8.49          val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
    8.50          val prop' = Thm.prop_of thm';
    8.51          val unconditional = (Logic.count_prems prop' = 0);
    8.52 @@ -974,10 +975,10 @@
    8.53  (* conversion to apply a congruence rule to a term *)
    8.54  
    8.55  fun congc prover ss maxt {thm=cong,lhs=lhs} t =
    8.56 -  let val rthm = Thm.incr_indexes (maxt+1) cong;
    8.57 -      val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
    8.58 -      val insts = Thm.cterm_match (rlhs, t)
    8.59 -      (* Pattern.match can raise Pattern.MATCH;
    8.60 +  let val rthm = Thm.incr_indexes (maxt + 1) cong;
    8.61 +      val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
    8.62 +      val insts = Thm.match (rlhs, t)
    8.63 +      (* Thm.match can raise Pattern.MATCH;
    8.64           is handled when congc is called *)
    8.65        val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
    8.66        val unit = trace_thm (fn () => "Applying congruence rule:") ss thm';
    8.67 @@ -987,12 +988,12 @@
    8.68       | SOME thm2 => (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
    8.69            NONE => err ("Congruence proof failed.  Should not have proved", thm2)
    8.70          | SOME thm2' =>
    8.71 -            if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
    8.72 +            if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
    8.73              then NONE else SOME thm2')
    8.74    end;
    8.75  
    8.76  val (cA, (cB, cC)) =
    8.77 -  apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
    8.78 +  apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
    8.79  
    8.80  fun transitive1 NONE NONE = NONE
    8.81    | transitive1 (SOME thm1) NONE = SOME thm1
    8.82 @@ -1009,15 +1010,15 @@
    8.83            else
    8.84            (case subc skel ss t of
    8.85               some as SOME thm1 =>
    8.86 -               (case rewritec (prover, thy, maxidx) ss (Drule.rhs_of thm1) of
    8.87 +               (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
    8.88                    SOME (thm2, skel2) =>
    8.89                      transitive2 (transitive thm1 thm2)
    8.90 -                      (botc skel2 ss (Drule.rhs_of thm2))
    8.91 +                      (botc skel2 ss (Thm.rhs_of thm2))
    8.92                  | NONE => some)
    8.93             | NONE =>
    8.94                 (case rewritec (prover, thy, maxidx) ss t of
    8.95                    SOME (thm2, skel2) => transitive2 thm2
    8.96 -                    (botc skel2 ss (Drule.rhs_of thm2))
    8.97 +                    (botc skel2 ss (Thm.rhs_of thm2))
    8.98                  | NONE => NONE))
    8.99  
   8.100      and try_botc ss t =
   8.101 @@ -1045,7 +1046,7 @@
   8.102               Const ("==>", _) $ _  => impc t0 ss
   8.103             | Abs _ =>
   8.104                 let val thm = beta_conversion false t0
   8.105 -               in case subc skel0 ss (Drule.rhs_of thm) of
   8.106 +               in case subc skel0 ss (Thm.rhs_of thm) of
   8.107                      NONE => SOME thm
   8.108                    | SOME thm' => SOME (transitive thm thm')
   8.109                 end
   8.110 @@ -1077,7 +1078,7 @@
   8.111      may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
   8.112                            (let
   8.113                               val thm = congc (prover ss) ss maxidx cong t0;
   8.114 -                             val t = the_default t0 (Option.map Drule.rhs_of thm);
   8.115 +                             val t = the_default t0 (Option.map Thm.rhs_of thm);
   8.116                               val (cl, cr) = Thm.dest_comb t
   8.117                               val dVar = Var(("", 0), dummyT)
   8.118                               val skel =
   8.119 @@ -1108,14 +1109,14 @@
   8.120  
   8.121      and disch r (prem, eq) =
   8.122        let
   8.123 -        val (lhs, rhs) = Drule.dest_equals (Thm.cprop_of eq);
   8.124 +        val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
   8.125          val eq' = implies_elim (Thm.instantiate
   8.126            ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
   8.127            (implies_intr prem eq)
   8.128        in if not r then eq' else
   8.129          let
   8.130 -          val (prem', concl) = dest_implies lhs;
   8.131 -          val (prem'', _) = dest_implies rhs
   8.132 +          val (prem', concl) = Thm.dest_implies lhs;
   8.133 +          val (prem'', _) = Thm.dest_implies rhs
   8.134          in transitive (transitive
   8.135            (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
   8.136               Drule.swap_prems_eq) eq')
   8.137 @@ -1129,13 +1130,13 @@
   8.138            let
   8.139              val ss' = add_rrules (rev rrss, rev asms) ss;
   8.140              val concl' =
   8.141 -              Drule.mk_implies (prem, the_default concl (Option.map Drule.rhs_of eq));
   8.142 +              Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
   8.143              val dprem = Option.map (curry (disch false) prem)
   8.144            in case rewritec (prover, thy, maxidx) ss' concl' of
   8.145                NONE => rebuild prems concl' rrss asms ss (dprem eq)
   8.146              | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
   8.147                    (the (transitive3 (dprem eq) eq'), prems))
   8.148 -                (mut_impc0 (rev prems) (Drule.rhs_of eq') (rev rrss) (rev asms) ss)
   8.149 +                (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss)
   8.150            end
   8.151  
   8.152      and mut_impc0 prems concl rrss asms ss =
   8.153 @@ -1164,7 +1165,7 @@
   8.154                (if k = 0 then 0 else k - 1)
   8.155            | SOME eqn =>
   8.156              let
   8.157 -              val prem' = Drule.rhs_of eqn;
   8.158 +              val prem' = Thm.rhs_of eqn;
   8.159                val tprems = map term_of prems;
   8.160                val i = 1 + Library.foldl Int.max (~1, map (fn p =>
   8.161                  find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
   8.162 @@ -1178,9 +1179,9 @@
   8.163  
   8.164       (*legacy code - only for backwards compatibility*)
   8.165       and nonmut_impc ct ss =
   8.166 -       let val (prem, conc) = dest_implies ct;
   8.167 +       let val (prem, conc) = Thm.dest_implies ct;
   8.168             val thm1 = if simprem then botc skel0 ss prem else NONE;
   8.169 -           val prem1 = the_default prem (Option.map Drule.rhs_of thm1);
   8.170 +           val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
   8.171             val ss1 = if not useprem then ss else add_rrules
   8.172               (apsnd single (apfst single (rules_of_prem ss prem1))) ss
   8.173         in (case botc skel0 ss1 conc of
   8.174 @@ -1253,7 +1254,7 @@
   8.175  (*Rewrite a theorem*)
   8.176  fun simplify _ [] th = th
   8.177    | simplify full thms th =
   8.178 -      Drule.fconv_rule (rewrite_cterm (full, false, false) simple_prover
   8.179 +      Conv.fconv_rule (rewrite_cterm (full, false, false) simple_prover
   8.180          (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)) th;
   8.181  
   8.182  val rewrite_rule = simplify true;
   8.183 @@ -1262,17 +1263,17 @@
   8.184  fun rewrite_term thy rules procs =
   8.185    Pattern.rewrite_term thy (map decomp_simp' rules) procs;
   8.186  
   8.187 -fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
   8.188 +fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
   8.189  
   8.190  (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   8.191  fun rewrite_goals_rule thms th =
   8.192 -  Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover
   8.193 +  Conv.fconv_rule (Conv.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover
   8.194      (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
   8.195  
   8.196  (*Rewrite the subgoal of a proof state (represented by a theorem)*)
   8.197  fun rewrite_goal_rule mode prover ss i thm =
   8.198    if 0 < i  andalso  i <= nprems_of thm
   8.199 -  then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
   8.200 +  then Conv.fconv_rule (Conv.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
   8.201    else raise THM("rewrite_goal_rule", i, [thm]);
   8.202  
   8.203  
   8.204 @@ -1320,7 +1321,7 @@
   8.205  
   8.206  fun gen_norm_hhf ss th =
   8.207    (if Drule.is_norm_hhf (Thm.prop_of th) then th
   8.208 -   else Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th)
   8.209 +   else Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th)
   8.210    |> Thm.adjust_maxidx_thm ~1
   8.211    |> Drule.gen_all;
   8.212