# HG changeset patch # User wenzelm # Date 1178750388 -7200 # Node ID ac833b4bb7ee01686ca3cdc9e0fd0edf12051a44 # Parent 481cd919c47f43cbabbfb49d658c61599104d5e5 moved some Drule operations to Thm (see more_thm.ML); diff -r 481cd919c47f -r ac833b4bb7ee src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/HOL/Import/shuffler.ML Thu May 10 00:39:48 2007 +0200 @@ -493,7 +493,7 @@ addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy] fun chain f th = let - val rhs = snd (dest_equals (cprop_of th)) + val rhs = Thm.rhs_of th in transitive th (f rhs) end @@ -585,7 +585,7 @@ val closed_t = Library.foldr (fn (v, body) => let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t) val rew_th = norm_term thy closed_t - val rhs = snd (dest_equals (cprop_of rew_th)) + val rhs = Thm.rhs_of rew_th val shuffles = ShuffleData.get thy fun process [] = NONE diff -r 481cd919c47f -r ac833b4bb7ee src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu May 10 00:39:48 2007 +0200 @@ -48,7 +48,7 @@ (*Populate the abstraction cache with common combinators.*) fun seed th net = - let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th) + let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th) val t = Logic.legacy_varify (term_of ct) in Net.insert_term Thm.eq_thm (t, th) net end; @@ -184,7 +184,7 @@ (*Apply a function definition to an argument, beta-reducing the result.*) fun beta_comb cf x = let val th1 = combination cf (reflexive x) - val th2 = beta_conversion false (Drule.rhs_of th1) + val th2 = beta_conversion false (Thm.rhs_of th1) in transitive th1 th2 end; (*Apply a function definition to arguments, beta-reducing along the way.*) @@ -259,7 +259,7 @@ val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else (); val (u'_th,defs) = abstract thy cta val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else (); - val cu' = Drule.rhs_of u'_th + val cu' = Thm.rhs_of u'_th val u' = term_of cu' val abs_v_u = lambda_list (map term_of cvs) u' (*get the formal parameters: ALL variables free in the term*) @@ -335,7 +335,7 @@ val (cvs,cta) = dest_abs_list ct val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) val (u'_th,defs) = abstract cta - val cu' = Drule.rhs_of u'_th + val cu' = Thm.rhs_of u'_th val u' = term_of cu' (*Could use Thm.cabs instead of lambda to work at level of cterms*) val abs_v_u = lambda_list (map term_of cvs) (term_of cu') @@ -396,7 +396,7 @@ an existential formula by a use of that function. Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) fun skolem_of_def def = - let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def)) + let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def)) val (ch, frees) = c_variant_abs_multi (rhs, []) val (chilbert,cabs) = Thm.dest_comb ch val {thy,t, ...} = rep_cterm chilbert diff -r 481cd919c47f -r ac833b4bb7ee src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/HOL/Tools/specification_package.ML Thu May 10 00:39:48 2007 +0200 @@ -123,7 +123,7 @@ val rew_imps = alt_props |> map (ObjectLogic.atomize_cterm o Thm.read_cterm thy o rpair Term.propT o snd) val props' = rew_imps |> - map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) + map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) fun proc_single prop = let diff -r 481cd919c47f -r ac833b4bb7ee src/Pure/Tools/codegen_data.ML --- a/src/Pure/Tools/codegen_data.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/Pure/Tools/codegen_data.ML Thu May 10 00:39:48 2007 +0200 @@ -707,7 +707,7 @@ fun rhs_conv conv thm = let - val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm; + val thm' = (conv o Thm.rhs_of) thm; in Thm.transitive thm thm' end in diff -r 481cd919c47f -r ac833b4bb7ee src/Pure/Tools/codegen_funcgr.ML --- a/src/Pure/Tools/codegen_funcgr.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/Pure/Tools/codegen_funcgr.ML Thu May 10 00:39:48 2007 +0200 @@ -314,18 +314,18 @@ fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t [] fun rhs_conv conv thm = let - val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm; + val thm' = (conv o Thm.rhs_of) thm; in Thm.transitive thm thm' end val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct); val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); val thm1 = CodegenData.preprocess_cterm ct |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy); - val ct' = Drule.dest_equals_rhs (Thm.cprop_of thm1); + val ct' = Thm.rhs_of thm1; val consts = consts_of thy (Thm.term_of ct'); val funcgr' = ensure_consts rewrites thy consts funcgr; val algebra = CodegenData.coregular_algebra thy; val (_, thm2) = Thm.varifyT' [] thm1; - val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_of thm2)); + val thm3 = Thm.reflexive (Thm.rhs_of thm2); val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.const_of_cexpr thy); val [thm4] = resort_thms algebra typ_funcgr [thm3]; val tfrees = Term.add_tfrees (Thm.prop_of thm1) []; @@ -337,7 +337,7 @@ in Thm.instantiate (instmap, []) thm end; val thm5 = inst thm2; val thm6 = inst thm4; - val ct'' = Drule.dest_equals_rhs (Thm.cprop_of thm6); + val ct'' = Thm.rhs_of thm6; val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') []; val drop = drop_classes thy tfrees; val instdefs = instances_of_consts thy algebra funcgr' cs; diff -r 481cd919c47f -r ac833b4bb7ee src/Pure/Tools/nbe.ML --- a/src/Pure/Tools/nbe.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/Pure/Tools/nbe.ML Thu May 10 00:39:48 2007 +0200 @@ -179,7 +179,7 @@ let val t = Thm.term_of ct; val thm2 = normalization_invoke thy funcgr t; - val thm3 = apply_posts thy ((snd o Drule.dest_equals o Thm.cprop_of) thm2); + val thm3 = apply_posts thy (Thm.rhs_of thm2); val thm23 = drop_classes (Thm.transitive thm2 thm3); in Thm.transitive thm1 thm23 handle THM _ => diff -r 481cd919c47f -r ac833b4bb7ee src/Pure/goal.ML --- a/src/Pure/goal.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/Pure/goal.ML Thu May 10 00:39:48 2007 +0200 @@ -49,7 +49,7 @@ C ==> #C *) val init = - let val A = #1 (Drule.dest_implies (Thm.cprop_of Drule.protectI)) + let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI)) in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end; (* diff -r 481cd919c47f -r ac833b4bb7ee src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Thu May 10 00:39:46 2007 +0200 +++ b/src/Pure/meta_simplifier.ML Thu May 10 00:39:48 2007 +0200 @@ -460,7 +460,7 @@ val {thy, prop, ...} = Thm.rep_thm thm; val prems = Logic.strip_imp_prems prop; val concl = Drule.strip_imp_concl (Thm.cprop_of thm); - val (lhs, rhs) = Drule.dest_equals concl handle TERM _ => + val (lhs, rhs) = Thm.dest_equals concl handle TERM _ => raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs)); val elhs = if term_of elhs aconv term_of lhs then lhs else elhs; (*share identical copies*) @@ -578,7 +578,7 @@ fun add_cong (ss, thm) = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => let - val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) + val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); (*val lhs = Envir.eta_contract lhs;*) val a = the (cong_name (head_of (term_of lhs))) handle Option.Option => @@ -828,7 +828,7 @@ fun check_conv msg ss thm thm' = let val thm'' = transitive thm (transitive - (symmetric (Drule.beta_eta_conversion (Drule.lhs_of thm'))) thm') + (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm') in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end handle THM _ => let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in @@ -890,16 +890,17 @@ let val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss; val eta_thm = Thm.eta_conversion t; - val eta_t' = Drule.rhs_of eta_thm; + val eta_t' = Thm.rhs_of eta_thm; val eta_t = term_of eta_t'; fun rew {thm, name, lhs, elhs, extra, fo, perm} = let val {thy, prop, maxidx, ...} = rep_thm thm; val (rthm, elhs') = if maxt = ~1 orelse not extra then (thm, elhs) - else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs); - val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t') - else Thm.cterm_match (elhs', eta_t'); + else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); + val insts = + if fo then Thm.first_order_match (elhs', eta_t') + else Thm.match (elhs', eta_t'); val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); val prop' = Thm.prop_of thm'; val unconditional = (Logic.count_prems prop' = 0); @@ -974,10 +975,10 @@ (* conversion to apply a congruence rule to a term *) fun congc prover ss maxt {thm=cong,lhs=lhs} t = - let val rthm = Thm.incr_indexes (maxt+1) cong; - val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm))); - val insts = Thm.cterm_match (rlhs, t) - (* Pattern.match can raise Pattern.MATCH; + let val rthm = Thm.incr_indexes (maxt + 1) cong; + val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm))); + val insts = Thm.match (rlhs, t) + (* Thm.match can raise Pattern.MATCH; is handled when congc is called *) val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm); val unit = trace_thm (fn () => "Applying congruence rule:") ss thm'; @@ -987,12 +988,12 @@ | SOME thm2 => (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of NONE => err ("Congruence proof failed. Should not have proved", thm2) | SOME thm2' => - if op aconv (pairself term_of (dest_equals (cprop_of thm2'))) + if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2'))) then NONE else SOME thm2') end; val (cA, (cB, cC)) = - apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong))); + apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong))); fun transitive1 NONE NONE = NONE | transitive1 (SOME thm1) NONE = SOME thm1 @@ -1009,15 +1010,15 @@ else (case subc skel ss t of some as SOME thm1 => - (case rewritec (prover, thy, maxidx) ss (Drule.rhs_of thm1) of + (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of SOME (thm2, skel2) => transitive2 (transitive thm1 thm2) - (botc skel2 ss (Drule.rhs_of thm2)) + (botc skel2 ss (Thm.rhs_of thm2)) | NONE => some) | NONE => (case rewritec (prover, thy, maxidx) ss t of SOME (thm2, skel2) => transitive2 thm2 - (botc skel2 ss (Drule.rhs_of thm2)) + (botc skel2 ss (Thm.rhs_of thm2)) | NONE => NONE)) and try_botc ss t = @@ -1045,7 +1046,7 @@ Const ("==>", _) $ _ => impc t0 ss | Abs _ => let val thm = beta_conversion false t0 - in case subc skel0 ss (Drule.rhs_of thm) of + in case subc skel0 ss (Thm.rhs_of thm) of NONE => SOME thm | SOME thm' => SOME (transitive thm thm') end @@ -1077,7 +1078,7 @@ may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) (let val thm = congc (prover ss) ss maxidx cong t0; - val t = the_default t0 (Option.map Drule.rhs_of thm); + val t = the_default t0 (Option.map Thm.rhs_of thm); val (cl, cr) = Thm.dest_comb t val dVar = Var(("", 0), dummyT) val skel = @@ -1108,14 +1109,14 @@ and disch r (prem, eq) = let - val (lhs, rhs) = Drule.dest_equals (Thm.cprop_of eq); + val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq); val eq' = implies_elim (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) (implies_intr prem eq) in if not r then eq' else let - val (prem', concl) = dest_implies lhs; - val (prem'', _) = dest_implies rhs + val (prem', concl) = Thm.dest_implies lhs; + val (prem'', _) = Thm.dest_implies rhs in transitive (transitive (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq) eq') @@ -1129,13 +1130,13 @@ let val ss' = add_rrules (rev rrss, rev asms) ss; val concl' = - Drule.mk_implies (prem, the_default concl (Option.map Drule.rhs_of eq)); + Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq)); val dprem = Option.map (curry (disch false) prem) in case rewritec (prover, thy, maxidx) ss' concl' of NONE => rebuild prems concl' rrss asms ss (dprem eq) | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap) (the (transitive3 (dprem eq) eq'), prems)) - (mut_impc0 (rev prems) (Drule.rhs_of eq') (rev rrss) (rev asms) ss) + (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss) end and mut_impc0 prems concl rrss asms ss = @@ -1164,7 +1165,7 @@ (if k = 0 then 0 else k - 1) | SOME eqn => let - val prem' = Drule.rhs_of eqn; + val prem' = Thm.rhs_of eqn; val tprems = map term_of prems; val i = 1 + Library.foldl Int.max (~1, map (fn p => find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))); @@ -1178,9 +1179,9 @@ (*legacy code - only for backwards compatibility*) and nonmut_impc ct ss = - let val (prem, conc) = dest_implies ct; + let val (prem, conc) = Thm.dest_implies ct; val thm1 = if simprem then botc skel0 ss prem else NONE; - val prem1 = the_default prem (Option.map Drule.rhs_of thm1); + val prem1 = the_default prem (Option.map Thm.rhs_of thm1); val ss1 = if not useprem then ss else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss in (case botc skel0 ss1 conc of @@ -1253,7 +1254,7 @@ (*Rewrite a theorem*) fun simplify _ [] th = th | simplify full thms th = - Drule.fconv_rule (rewrite_cterm (full, false, false) simple_prover + Conv.fconv_rule (rewrite_cterm (full, false, false) simple_prover (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)) th; val rewrite_rule = simplify true; @@ -1262,17 +1263,17 @@ fun rewrite_term thy rules procs = Pattern.rewrite_term thy (map decomp_simp' rules) procs; -fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss); +fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss); (*Rewrite the subgoals of a proof state (represented by a theorem) *) fun rewrite_goals_rule thms th = - Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover + Conv.fconv_rule (Conv.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th; (*Rewrite the subgoal of a proof state (represented by a theorem)*) fun rewrite_goal_rule mode prover ss i thm = if 0 < i andalso i <= nprems_of thm - then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm + then Conv.fconv_rule (Conv.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm else raise THM("rewrite_goal_rule", i, [thm]); @@ -1320,7 +1321,7 @@ fun gen_norm_hhf ss th = (if Drule.is_norm_hhf (Thm.prop_of th) then th - else Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th) + else Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss) th) |> Thm.adjust_maxidx_thm ~1 |> Drule.gen_all;