# HG changeset patch # User wenzelm # Date 1273953005 -7200 # Node ID 9bec62c1071483976bed82f9610c891c6b198cc0 # Parent dbf831a50e4a02d761d8e6ee4fada49b50d7af37 less pervasive names from structure Thm; diff -r dbf831a50e4a -r 9bec62c10714 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/FOLP/simp.ML Sat May 15 21:50:05 2010 +0200 @@ -431,7 +431,7 @@ are represented by rules, generalized over their parameters*) fun add_asms(ss,thm,a,anet,ats,cs) = let val As = strip_varify(nth_subgoal i thm, a, []); - val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As; + val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As; val new_rws = maps mk_rew_rules thms; val rwrls = map mk_trans (maps mk_rew_rules thms); val anet' = fold_rev lhs_insert_thm rwrls anet; diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat May 15 21:50:05 2010 +0200 @@ -681,7 +681,7 @@ else ("Nox",[]) | t => if t aconv term_of x then ("x",[]) else ("Nox",[]); -fun xnormalize_conv ctxt [] ct = reflexive ct +fun xnormalize_conv ctxt [] ct = Thm.reflexive ct | xnormalize_conv ctxt (vs as (x::_)) ct = case term_of ct of Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) => @@ -696,8 +696,8 @@ (Thm.capply @{cterm "Trueprop"} (if neg then Thm.capply (Thm.capply clt c) cz else Thm.capply (Thm.capply clt cz) c)) - val cth = equal_elim (symmetric cthp) TrueI - val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t]) + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI + val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t]) (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th @@ -719,12 +719,12 @@ (Thm.capply @{cterm "Trueprop"} (if neg then Thm.capply (Thm.capply clt c) cz else Thm.capply (Thm.capply clt cz) c)) - val cth = equal_elim (symmetric cthp) TrueI - val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI + val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth val rth = th in rth end - | _ => reflexive ct) + | _ => Thm.reflexive ct) | Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.zero},_) => @@ -740,8 +740,8 @@ (Thm.capply @{cterm "Trueprop"} (if neg then Thm.capply (Thm.capply clt c) cz else Thm.capply (Thm.capply clt cz) c)) - val cth = equal_elim (symmetric cthp) TrueI - val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI + val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th @@ -764,12 +764,12 @@ (Thm.capply @{cterm "Trueprop"} (if neg then Thm.capply (Thm.capply clt c) cz else Thm.capply (Thm.capply clt cz) c)) - val cth = equal_elim (symmetric cthp) TrueI - val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI + val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth val rth = th in rth end - | _ => reflexive ct) + | _ => Thm.reflexive ct) | Const("op =",_)$_$Const(@{const_name Groups.zero},_) => (case whatis x (Thm.dest_arg1 ct) of @@ -782,8 +782,8 @@ val cthp = Simplifier.rewrite (simpset_of ctxt) (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) - val cth = equal_elim (symmetric cthp) TrueI - val th = implies_elim + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI + val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th @@ -804,11 +804,11 @@ val cthp = Simplifier.rewrite (simpset_of ctxt) (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) - val cth = equal_elim (symmetric cthp) TrueI - val rth = implies_elim + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI + val rth = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth in rth end - | _ => reflexive ct); + | _ => Thm.reflexive ct); local val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"} @@ -823,7 +823,7 @@ val nth = Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th - val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) + val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) in rth end | Const(@{const_name Orderings.less_eq},_)$a$b => let val (ca,cb) = Thm.dest_binop ct @@ -832,7 +832,7 @@ val nth = Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th - val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) + val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) in rth end | Const("op =",_)$a$b => @@ -842,10 +842,10 @@ val nth = Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th - val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) + val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) in rth end | @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct -| _ => reflexive ct +| _ => Thm.reflexive ct end; fun classfield_whatis phi = diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat May 15 21:50:05 2010 +0200 @@ -106,7 +106,7 @@ [simp_tac mod_div_simpset 1, simp_tac simpset0 1, TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac simpset3 1), TRY (simp_tac cooper_ss 1)] - (trivial ct)) + (Thm.trivial ct)) fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) (* The result of the quantifier elimination *) val (th, tac) = case (prop_of pre_thm) of diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sat May 15 21:50:05 2010 +0200 @@ -87,7 +87,7 @@ val pre_thm = Seq.hd (EVERY [simp_tac simpset0 1, TRY (simp_tac (Simplifier.context ctxt ferrack_ss) 1)] - (trivial ct)) + (Thm.trivial ct)) fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) (* The result of the quantifier elimination *) val (th, tac) = case prop_of pre_thm of diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat May 15 21:50:05 2010 +0200 @@ -128,7 +128,7 @@ val pre_thm = Seq.hd (EVERY [simp_tac mod_div_simpset 1, simp_tac simpset0 1, TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac mir_ss 1)] - (trivial ct)) + (Thm.trivial ct)) fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) (* The result of the quantifier elimination *) val (th, tac) = case (prop_of pre_thm) of diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/HOL.thy Sat May 15 21:50:05 2010 +0200 @@ -1282,12 +1282,12 @@ else let val abs_g'= Abs (n,xT,g'); val g'x = abs_g'$x; - val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x)); + val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x)); val rl = cterm_instantiate [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx), (g_Let_folded, cterm_of thy abs_g')] @{thm Let_folded}; - in SOME (rl OF [transitive fx_g g_g'x]) + in SOME (rl OF [Thm.transitive fx_g g_g'x]) end) end | _ => NONE) diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Import/import.ML --- a/src/HOL/Import/import.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Import/import.ML Sat May 15 21:50:05 2010 +0200 @@ -40,7 +40,7 @@ val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy) val thm = snd (ProofKernel.to_isa_thm hol4thm) val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy - val thm = equal_elim rew thm + val thm = Thm.equal_elim rew thm val prew = ProofKernel.rewrite_hol4_term prem thy val prem' = #2 (Logic.dest_equals (prop_of prew)) val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm) @@ -53,7 +53,7 @@ val _ = if prem' aconv (prop_of thm) then message "import: Terms match up" else message "import: Terms DO NOT match up" - val thm' = equal_elim (symmetric prew) thm + val thm' = Thm.equal_elim (Thm.symmetric prew) thm val res = Thm.bicompose true (false,thm',0) 1 th in res diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Sat May 15 21:50:05 2010 +0200 @@ -1013,12 +1013,12 @@ local val th = thm "not_def" val thy = theory_of_thm th - val pp = reflexive (cterm_of thy (Const("Trueprop",boolT-->propT))) + val pp = Thm.reflexive (cterm_of thy (Const("Trueprop",boolT-->propT))) in -val not_elim_thm = combination pp th +val not_elim_thm = Thm.combination pp th end -val not_intro_thm = symmetric not_elim_thm +val not_intro_thm = Thm.symmetric not_elim_thm val abs_thm = thm "ext" val trans_thm = thm "trans" val symmetry_thm = thm "sym" @@ -1039,7 +1039,7 @@ end fun implies_elim_all th = - Library.foldl (fn (th,p) => implies_elim th (assume p)) (th,cprems_of th) + Library.foldl (fn (th,p) => Thm.implies_elim th (Thm.assume p)) (th,cprems_of th) fun norm_hyps th = th |> beta_eta_thm @@ -1054,7 +1054,7 @@ val clc = Thm.cterm_of sg lc val cvty = ctyp_of_term cv val th1 = implies_elim_all th - val th2 = beta_eta_thm (forall_intr cv th1) + val th2 = beta_eta_thm (Thm.forall_intr cv th1) val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm)) val c = prop_of th3 val vname = fst(dest_Free v) @@ -1072,7 +1072,7 @@ fun rearrange sg tm th = let val tm' = Envir.beta_eta_contract tm - fun find [] n = Thm.permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th) + fun find [] n = Thm.permute_prems 0 1 (Thm.implies_intr (Thm.cterm_of sg tm) th) | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p) then Thm.permute_prems n 1 th else find ps (n+1) @@ -1258,7 +1258,7 @@ fun get_isabelle_thm thyname thmname hol4conc thy = let val (info,hol4conc') = disamb_term hol4conc - val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) + val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) val isaconc = case concl_of i2h_conc of Const("==",_) $ lhs $ _ => lhs @@ -1268,7 +1268,7 @@ message "Modified conclusion:"; if_debug prin isaconc) - fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th) + fun mk_res th = HOLThm (rens_of info, Thm.equal_elim i2h_conc th) in case get_hol4_mapping thyname thmname thy of SOME (SOME thmname) => @@ -1320,7 +1320,7 @@ fun warn () = let val (info,hol4conc') = disamb_term hol4conc - val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) + val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) in case concl_of i2h_conc of Const("==",_) $ lhs $ _ => @@ -1369,7 +1369,7 @@ let val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth val rew = rewrite_hol4_term (concl_of th) thy - val th = equal_elim rew th + val th = Thm.equal_elim rew th val thy' = add_hol4_pending thyname thmname args thy val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') val th = disambiguate_frees th @@ -1683,7 +1683,7 @@ val (info',v') = disamb_term_from info v fun strip 0 _ th = th | strip n (p::ps) th = - strip (n-1) ps (implies_elim th (assume p)) + strip (n-1) ps (Thm.implies_elim th (Thm.assume p)) | strip _ _ _ = raise ERR "CHOOSE" "strip error" val cv = cterm_of thy v' val th2 = norm_hyps th2 @@ -1697,7 +1697,7 @@ val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm) val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2 val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21 - val th23 = beta_eta_thm (forall_intr cv th22) + val th23 = beta_eta_thm (Thm.forall_intr cv th22) val th11 = implies_elim_all (beta_eta_thm th1) val th' = th23 COMP (th11 COMP choose_thm') val th = implies_intr_hyps th' @@ -1796,7 +1796,7 @@ | _ => raise ERR "mk_ABS" "Bad conclusion" val (fd,fr) = dom_rng (type_of f) val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm - val th2 = forall_intr cv th1 + val th2 = Thm.forall_intr cv th1 val th3 = th2 COMP abs_thm' val res = implies_intr_hyps th3 in @@ -1867,7 +1867,7 @@ _ $ (Const("op -->",_) $ a $ Const("False",_)) => a | _ => raise ERR "NOT_INTRO" "Conclusion of bad form" val ca = cterm_of thy a - val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1 + val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1 val res = HOLThm(rens,implies_intr_hyps th2) val _ = message "RESULT:" val _ = if_debug pth res @@ -1884,7 +1884,7 @@ _ $ (Const("Not",_) $ a) => a | _ => raise ERR "NOT_ELIM" "Conclusion of bad form" val ca = cterm_of thy a - val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1 + val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1 val res = HOLThm(rens,implies_intr_hyps th2) val _ = message "RESULT:" val _ = if_debug pth res @@ -1902,9 +1902,9 @@ val prems = prems_of th val th1 = beta_eta_thm th val th2 = implies_elim_all th1 - val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2 + val th3 = Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2 val th4 = th3 COMP disch_thm - val res = HOLThm(rens_of info',implies_intr_hyps th4) + val res = HOLThm (rens_of info', implies_intr_hyps th4) val _ = message "RESULT:" val _ = if_debug pth res in @@ -2032,7 +2032,7 @@ val res' = Thm.unvarify_global res val hth = HOLThm(rens,res') val rew = rewrite_hol4_term (concl_of res') thy' - val th = equal_elim rew res' + val th = Thm.equal_elim rew res' fun handle_const (name,thy) = let val defname = Thm.def_name name @@ -2112,7 +2112,7 @@ val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') val rew = rewrite_hol4_term (concl_of td_th) thy4 - val th = equal_elim rew (Thm.transfer thy4 td_th) + val th = Thm.equal_elim rew (Thm.transfer thy4 td_th) val c = case HOLogic.dest_Trueprop (prop_of th) of Const("Ex",exT) $ P => let diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Import/shuffler.ML Sat May 15 21:50:05 2010 +0200 @@ -95,12 +95,12 @@ val cQ = cert Q val cPQ = cert PQ val cPPQ = cert PPQ - val th1 = assume cPQ |> implies_intr_list [cPQ,cP] - val th3 = assume cP - val th4 = implies_elim_list (assume cPPQ) [th3,th3] + val th1 = Thm.assume cPQ |> implies_intr_list [cPQ,cP] + val th3 = Thm.assume cP + val th4 = implies_elim_list (Thm.assume cPPQ) [th3,th3] |> implies_intr_list [cPPQ,cP] in - equal_intr th4 th1 |> Drule.export_without_context + Thm.equal_intr th4 th1 |> Drule.export_without_context end val imp_comm = @@ -115,12 +115,12 @@ val cQ = cert Q val cPQR = cert PQR val cQPR = cert QPR - val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ] + val th1 = implies_elim_list (Thm.assume cPQR) [Thm.assume cP,Thm.assume cQ] |> implies_intr_list [cPQR,cQ,cP] - val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP] + val th2 = implies_elim_list (Thm.assume cQPR) [Thm.assume cQ,Thm.assume cP] |> implies_intr_list [cQPR,cP,cQ] in - equal_intr th1 th2 |> Drule.export_without_context + Thm.equal_intr th1 th2 |> Drule.export_without_context end val def_norm = @@ -134,20 +134,20 @@ val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0))) val cPQ = cert (Logic.mk_equals(P,Q)) val cv = cert v - val rew = assume cvPQ - |> forall_elim cv - |> abstract_rule "v" cv + val rew = Thm.assume cvPQ + |> Thm.forall_elim cv + |> Thm.abstract_rule "v" cv val (lhs,rhs) = Logic.dest_equals(concl_of rew) - val th1 = transitive (transitive - (eta_conversion (cert lhs) |> symmetric) + val th1 = Thm.transitive (Thm.transitive + (Thm.eta_conversion (cert lhs) |> Thm.symmetric) rew) - (eta_conversion (cert rhs)) - |> implies_intr cvPQ - val th2 = combination (assume cPQ) (reflexive cv) - |> forall_intr cv - |> implies_intr cPQ + (Thm.eta_conversion (cert rhs)) + |> Thm.implies_intr cvPQ + val th2 = Thm.combination (Thm.assume cPQ) (Thm.reflexive cv) + |> Thm.forall_intr cv + |> Thm.implies_intr cPQ in - equal_intr th1 th2 |> Drule.export_without_context + Thm.equal_intr th1 th2 |> Drule.export_without_context end val all_comm = @@ -164,16 +164,16 @@ val cr = cert rhs val cx = cert x val cy = cert y - val th1 = assume cr + val th1 = Thm.assume cr |> forall_elim_list [cy,cx] |> forall_intr_list [cx,cy] - |> implies_intr cr - val th2 = assume cl + |> Thm.implies_intr cr + val th2 = Thm.assume cl |> forall_elim_list [cx,cy] |> forall_intr_list [cy,cx] - |> implies_intr cl + |> Thm.implies_intr cl in - equal_intr th1 th2 |> Drule.export_without_context + Thm.equal_intr th1 th2 |> Drule.export_without_context end val equiv_comm = @@ -184,10 +184,10 @@ val u = Free("u",T) val ctu = cert (Logic.mk_equals(t,u)) val cut = cert (Logic.mk_equals(u,t)) - val th1 = assume ctu |> symmetric |> implies_intr ctu - val th2 = assume cut |> symmetric |> implies_intr cut + val th1 = Thm.assume ctu |> Thm.symmetric |> Thm.implies_intr ctu + val th2 = Thm.assume cut |> Thm.symmetric |> Thm.implies_intr cut in - equal_intr th1 th2 |> Drule.export_without_context + Thm.equal_intr th1 th2 |> Drule.export_without_context end (* This simplification procedure rewrites !!x y. P x y @@ -217,7 +217,7 @@ val lhs = list_all ([xv,yv],t) val rhs = list_all ([yv,xv],swap_bound 0 t) val rew = Logic.mk_equals (lhs,rhs) - val init = trivial (cterm_of thy rew) + val init = Thm.trivial (cterm_of thy rew) in (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e)) end @@ -232,10 +232,10 @@ then let val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body))) - val t_th = reflexive (cterm_of thy t) - val newt_th = reflexive (cterm_of thy newt) + val t_th = Thm.reflexive (cterm_of thy t) + val newt_th = Thm.reflexive (cterm_of thy newt) in - SOME (transitive t_th newt_th) + SOME (Thm.transitive t_th newt_th) end else NONE | _ => error "norm_term (quant_rewrite) internal error" @@ -294,7 +294,7 @@ fun eta_contract thy assumes origt = let val (typet,Tinst) = freeze_thaw_term origt - val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet)) + val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet)) val final = inst_tfrees thy Tinst o thaw val t = #1 (Logic.dest_equals (prop_of init)) val _ = @@ -322,18 +322,18 @@ val v = Free (Name.variant (Term.add_free_names t []) "v", xT) val cv = cert v val ct = cert t - val th = (assume ct) - |> forall_elim cv - |> abstract_rule x cv - val ext_th = eta_conversion (cert (Abs(x,xT,P))) - val th' = transitive (symmetric ext_th) th + val th = (Thm.assume ct) + |> Thm.forall_elim cv + |> Thm.abstract_rule x cv + val ext_th = Thm.eta_conversion (cert (Abs(x,xT,P))) + val th' = Thm.transitive (Thm.symmetric ext_th) th val cu = cert (prop_of th') - val uth = combination (assume cu) (reflexive cv) - val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v))) - |> transitive uth - |> forall_intr cv - |> implies_intr cu - val rew_th = equal_intr (th' |> implies_intr ct) uth' + val uth = Thm.combination (Thm.assume cu) (Thm.reflexive cv) + val uth' = (Thm.beta_conversion false (cert (Abs(x,xT,Q) $ v))) + |> Thm.transitive uth + |> Thm.forall_intr cv + |> Thm.implies_intr cu + val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth' val res = final rew_th val lhs = (#1 (Logic.dest_equals (prop_of res))) in @@ -345,7 +345,7 @@ end fun beta_fun thy assume t = - SOME (beta_conversion true (cterm_of thy t)) + SOME (Thm.beta_conversion true (cterm_of thy t)) val meta_sym_rew = thm "refl" @@ -357,7 +357,7 @@ fun eta_expand thy assumes origt = let val (typet,Tinst) = freeze_thaw_term origt - val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet)) + val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet)) val final = inst_tfrees thy Tinst o thaw val t = #1 (Logic.dest_equals (prop_of init)) val _ = @@ -387,20 +387,20 @@ val v = Free(vname,aT) val cv = cert v val ct = cert t - val th1 = (combination (assume ct) (reflexive cv)) - |> forall_intr cv - |> implies_intr ct + val th1 = (Thm.combination (Thm.assume ct) (Thm.reflexive cv)) + |> Thm.forall_intr cv + |> Thm.implies_intr ct val concl = cert (concl_of th1) - val th2 = (assume concl) - |> forall_elim cv - |> abstract_rule vname cv + val th2 = (Thm.assume concl) + |> Thm.forall_elim cv + |> Thm.abstract_rule vname cv val (lhs,rhs) = Logic.dest_equals (prop_of th2) - val elhs = eta_conversion (cert lhs) - val erhs = eta_conversion (cert rhs) - val th2' = transitive - (transitive (symmetric elhs) th2) + val elhs = Thm.eta_conversion (cert lhs) + val erhs = Thm.eta_conversion (cert rhs) + val th2' = Thm.transitive + (Thm.transitive (Thm.symmetric elhs) th2) erhs - val res = equal_intr th1 (th2' |> implies_intr concl) + val res = Thm.equal_intr th1 (th2' |> Thm.implies_intr concl) val res' = final res in SOME res' @@ -475,7 +475,7 @@ val (t',_) = F (t,0) val ct = cterm_of thy t val ct' = cterm_of thy t' - val res = transitive (reflexive ct) (reflexive ct') + val res = Thm.transitive (Thm.reflexive ct) (Thm.reflexive ct') val _ = message ("disamb_term: " ^ (string_of_thm res)) in res @@ -496,12 +496,12 @@ let val rhs = Thm.rhs_of th in - transitive th (f rhs) + Thm.transitive th (f rhs) end val th = t |> disamb_bound thy |> chain (Simplifier.full_rewrite ss) - |> chain eta_conversion + |> chain Thm.eta_conversion |> Thm.strip_shyps val _ = message ("norm_term: " ^ (string_of_thm th)) in @@ -529,7 +529,7 @@ let val c = prop_of th in - equal_elim (norm_term thy c) th + Thm.equal_elim (norm_term thy c) th end (* make_equal thy t u tries to construct the theorem t == u under the @@ -540,7 +540,7 @@ let val t_is_t' = norm_term thy t val u_is_u' = norm_term thy u - val th = transitive t_is_t' (symmetric u_is_u') + val th = Thm.transitive t_is_t' (Thm.symmetric u_is_u') val _ = message ("make_equal: SOME " ^ (string_of_thm th)) in SOME th @@ -593,7 +593,7 @@ | process ((name,th)::thms) = let val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th))) - val triv_th = trivial rhs + val triv_th = Thm.trivial rhs val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th)) val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of SOME(th,_) => SOME th @@ -602,7 +602,7 @@ case mod_th of SOME mod_th => let - val closed_th = equal_elim (symmetric rew_th) mod_th + val closed_th = Thm.equal_elim (Thm.symmetric rew_th) mod_th in message ("Shuffler.set_prop succeeded by " ^ name); SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th) diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat May 15 21:50:05 2010 +0200 @@ -1272,7 +1272,7 @@ fun subst_conv eqs t = let val t' = fold (Thm.cabs o Thm.lhs_of) eqs t - in Conv.fconv_rule (Thm.beta_conversion true) (fold (C combination) eqs (reflexive t')) + in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t')) end (* A wrapper that tries to substitute away variables first. *) diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Sat May 15 21:50:05 2010 +0200 @@ -182,12 +182,12 @@ (* Some useful derived rules *) fun deduct_antisym_rule tha thb = - equal_intr (implies_intr (cprop_of thb) tha) - (implies_intr (cprop_of tha) thb); + Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) + (Thm.implies_intr (cprop_of tha) thb); fun prove_hyp tha thb = if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) - then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb; + then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb; val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and @@ -375,7 +375,7 @@ val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss) val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss) - fun eqT_elim th = equal_elim (symmetric th) @{thm TrueI} + fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI} fun oprconv cv ct = let val g = Thm.dest_fun2 ct in if g aconvc @{cterm "op <= :: real => _"} @@ -387,7 +387,7 @@ let val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th handle MATCH => raise CTERM ("real_ineq_conv", [ct])) - in transitive th' (oprconv poly_conv (Thm.rhs_of th')) + in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th')) end val [real_lt_conv, real_le_conv, real_eq_conv, real_not_lt_conv, real_not_le_conv, _] = @@ -446,10 +446,10 @@ let val (p,q) = Thm.dest_binop (concl th) val c = concl th1 val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible" - in implies_elim (implies_elim - (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th) - (implies_intr (Thm.capply @{cterm Trueprop} p) th1)) - (implies_intr (Thm.capply @{cterm Trueprop} q) th2) + in Thm.implies_elim (Thm.implies_elim + (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th) + (Thm.implies_intr (Thm.capply @{cterm Trueprop} p) th1)) + (Thm.implies_intr (Thm.capply @{cterm Trueprop} q) th2) end fun overall cert_choice dun ths = case ths of [] => @@ -468,8 +468,8 @@ overall cert_choice dun (th1::th2::oths) end else if is_disj ct then let - val (th1, cert1) = overall (Left::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths) - val (th2, cert2) = overall (Right::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths) + val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths) + val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths) in (disj_cases th th1 th2, Branch (cert1, cert2)) end else overall cert_choice (th::dun) oths end @@ -487,12 +487,12 @@ val th' = Drule.binop_cong_rule @{cterm "op |"} (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p) (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n) - in transitive th th' + in Thm.transitive th th' end fun equal_implies_1_rule PQ = let val P = Thm.lhs_of PQ - in implies_intr P (equal_elim PQ (assume P)) + in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P)) end (* FIXME!!! Copied from groebner.ml *) val strip_exists = @@ -507,7 +507,7 @@ | Var ((s,_),_) => s | _ => "x" - fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (abstract_rule (name_of x) x th) + fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (Thm.abstract_rule (name_of x) x th) val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec)); @@ -523,12 +523,12 @@ (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE) val pv = (Thm.rhs_of o Thm.beta_conversion true) (Thm.capply @{cterm Trueprop} (Thm.capply p v)) - val th1 = forall_intr v (implies_intr pv th') - in implies_elim (implies_elim th0 th) th1 end + val th1 = Thm.forall_intr v (Thm.implies_intr pv th') + in Thm.implies_elim (Thm.implies_elim th0 th) th1 end | _ => raise THM ("choose",0,[th, th']) fun simple_choose v th = - choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th + choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th val strip_forall = let fun h (acc, t) = @@ -558,11 +558,11 @@ val (evs,bod) = strip_exists tm0 val (avs,ibod) = strip_forall bod val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod)) - val (th2, certs) = overall [] [] [specl avs (assume (Thm.rhs_of th1))] - val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (Thm.capply @{cterm Trueprop} bod))) th2) - in (Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3), certs) + val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))] + val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.capply @{cterm Trueprop} bod))) th2) + in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs) end - in (implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates) + in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates) end in f end; @@ -715,10 +715,10 @@ fun eliminate_construct p c tm = let val t = find_cterm p tm - val th0 = (symmetric o beta_conversion false) (Thm.capply (Thm.cabs t tm) t) + val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.capply (Thm.cabs t tm) t) val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0 - in fconv_rule(arg_conv(binop_conv (arg_conv (beta_conversion false)))) - (transitive th0 (c p ax)) + in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false)))) + (Thm.transitive th0 (c p ax)) end val elim_abs = eliminate_construct is_abs diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Library/reflection.ML Sat May 15 21:50:05 2010 +0200 @@ -133,7 +133,7 @@ (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds)) in (([(ta, ctxt')], fn ([th], bds) => - (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]), + (hd (Variable.export ctxt' ctxt [(Thm.forall_intr (cert x) th) COMP allI]), let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT)) in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds end)), diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Matrix/cplex/matrixlp.ML --- a/src/HOL/Matrix/cplex/matrixlp.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Matrix/cplex/matrixlp.ML Sat May 15 21:50:05 2010 +0200 @@ -81,8 +81,8 @@ fun matrix_simplify th = let val simp_th = matrix_compute (cprop_of th) - val th = Thm.strip_shyps (equal_elim simp_th th) - fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *) + val th = Thm.strip_shyps (Thm.equal_elim simp_th th) + fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *) in removeTrue th end diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat May 15 21:50:05 2010 +0200 @@ -80,8 +80,8 @@ fun replacenegnorms cv t = case term_of t of @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t | @{term "op * :: real => _"}$_$_ => - if dest_ratconst (Thm.dest_arg1 t) reflexive t + if dest_ratconst (Thm.dest_arg1 t) Thm.reflexive t fun flip v eq = if FuncUtil.Ctermfunc.defined eq v then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq @@ -211,7 +211,7 @@ ((apply_ptha then_conv vector_add_conv) else_conv arg_conv vector_add_conv then_conv apply_pthd)) ct) end - | _ => reflexive ct)) + | _ => Thm.reflexive ct)) fun vector_canon_conv ct = case term_of ct of Const(@{const_name plus},_)$_$_ => @@ -237,7 +237,7 @@ | Const(@{const_name vec},_)$n => let val n = Thm.dest_arg ct in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) - then reflexive ct else apply_pth1 ct + then Thm.reflexive ct else apply_pth1 ct end *) | _ => apply_pth1 ct @@ -342,7 +342,7 @@ fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r - val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns + val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns val replace_conv = try_conv (rewrs_conv asl) val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) val ges' = @@ -352,10 +352,10 @@ val nubs = map (conjunct2 o norm_mp) asl val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts') val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1)) - val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1]) + val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1]) val cps = map (swap o Thm.dest_equals) (cprems_of th11) val th12 = instantiate ([], cps) th11 - val th13 = fold Thm.elim_implies (map (reflexive o snd) cps) th12; + val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12; in hd (Variable.export ctxt' ctxt [th13]) end in val real_vector_ineq_prover = real_vector_ineq_prover @@ -390,7 +390,7 @@ let val ctxt' = Variable.declare_term (term_of ct) ctxt val th = init_conv ctxt' ct - in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th)) + in Thm.equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (Thm.symmetric th)) (pure ctxt' (Thm.rhs_of th)) end diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat May 15 21:50:05 2010 +0200 @@ -602,7 +602,7 @@ (fn _ => EVERY [indtac rep_induct [] 1, ALLGOALS (simp_tac (global_simpset_of thy4 addsimps - (symmetric perm_fun_def :: abs_perm))), + (Thm.symmetric perm_fun_def :: abs_perm))), ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])), length new_type_names)); @@ -927,7 +927,7 @@ simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @ constr_defs @ perm_closed_thms)) 1, TRY (simp_tac (HOL_basic_ss addsimps - (symmetric perm_fun_def :: abs_perm)) 1), + (Thm.symmetric perm_fun_def :: abs_perm)) 1), TRY (simp_tac (HOL_basic_ss addsimps (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @ perm_closed_thms)) 1)]) @@ -1077,7 +1077,7 @@ (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1, EVERY (map (fn (prem, r) => (EVERY [REPEAT (eresolve_tac Abs_inverse_thms' 1), - simp_tac (HOL_basic_ss addsimps [symmetric r]) 1, + simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1, DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) (prems ~~ constr_defs))]); @@ -1641,7 +1641,7 @@ fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))] supports_fresh) 1, simp_tac (HOL_basic_ss addsimps - [supports_def, symmetric fresh_def, fresh_prod]) 1, + [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1, REPEAT_DETERM (resolve_tac [allI, impI] 1), REPEAT_DETERM (etac conjE 1), rtac unique 1, @@ -1655,7 +1655,7 @@ rtac rec_prem 1, simp_tac (HOL_ss addsimps (fs_name :: supp_prod :: finite_Un :: finite_prems)) 1, - simp_tac (HOL_ss addsimps (symmetric fresh_def :: + simp_tac (HOL_ss addsimps (Thm.symmetric fresh_def :: fresh_prod :: fresh_prems)) 1] end)) end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths) @@ -1746,7 +1746,7 @@ asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) (finite_thss ~~ finite_ctxt_ths) @ maps (fn ((_, idxss), elim) => maps (fn idxs => - [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1, + [full_simp_tac (HOL_ss addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1, REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1), rtac ex1I 1, (resolve_tac rec_intrs THEN_ALL_NEW atac) 1, diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Sat May 15 21:50:05 2010 +0200 @@ -266,7 +266,7 @@ (* intros, then applies eqvt_simp_tac *) fun supports_tac_i tactical ss i = let - val simps = [supports_def,symmetric fresh_def,fresh_prod] + val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod] in EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i), tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), @@ -329,7 +329,7 @@ val goal = List.nth(cprems_of st, i-1) val fin_supp = dynamic_thms st ("fin_supp") val fresh_atm = dynamic_thms st ("fresh_atm") - val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm + val ss1 = ss addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp in case Logic.strip_assums_concl (term_of goal) of diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Prolog/prolog.ML Sat May 15 21:50:05 2010 +0200 @@ -82,7 +82,7 @@ val (prems, Const("Trueprop", _)$concl) = rep_goal (#3(dest_state (st,i))); *) - val subgoal = #3(dest_state (st,i)); + val subgoal = #3(Thm.dest_state (st,i)); val prems = Logic.strip_assums_hyp subgoal; val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); fun drot_tac k i = DETERM (rotate_tac k i); diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Statespace/state_fun.ML Sat May 15 21:50:05 2010 +0200 @@ -245,7 +245,7 @@ (fn _ => rtac meta_ext 1 THEN simp_tac ss1 1); val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1)); - in SOME (transitive eq1 eq2) end + in SOME (Thm.transitive eq1 eq2) end | _ => NONE) end | _ => NONE)); diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Sat May 15 21:50:05 2010 +0200 @@ -483,8 +483,8 @@ [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1, REPEAT (rtac TrueI 1), rewrite_goals_tac (mk_meta_eq @{thm choice_eq} :: - symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs), - rewrite_goals_tac (map symmetric range_eqs), + Thm.symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs), + rewrite_goals_tac (map Thm.symmetric range_eqs), REPEAT (EVERY [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @ maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1), @@ -621,7 +621,7 @@ (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1, EVERY (map (fn (prem, r) => (EVERY [REPEAT (eresolve_tac Abs_inverse_thms 1), - simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1, + simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1, DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Function/context_tree.ML Sat May 15 21:50:05 2010 +0200 @@ -148,7 +148,7 @@ val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t fun subtree (ctx', fixes, assumes, st) = ((fixes, - map (assume o cterm_of (ProofContext.theory_of ctx)) assumes), + map (Thm.assume o cterm_of (ProofContext.theory_of ctx)) assumes), mk_tree' ctx' st) in Cong (r, dep, map subtree branches) @@ -165,7 +165,7 @@ fun inst_term t = subst_bound(f, abstract_over (fvar, t)) - val inst_thm = forall_elim cf o forall_intr cfvar + val inst_thm = Thm.forall_elim cf o Thm.forall_intr cfvar fun inst_tree_aux (Leaf t) = Leaf t | inst_tree_aux (Cong (crule, deps, branches)) = @@ -173,7 +173,7 @@ | inst_tree_aux (RCall (t, str)) = RCall (inst_term t, inst_tree_aux str) and inst_branch ((fxs, assms), str) = - ((fxs, map (assume o cterm_of thy o inst_term o prop_of) assms), + ((fxs, map (Thm.assume o cterm_of thy o inst_term o prop_of) assms), inst_tree_aux str) in inst_tree_aux tr @@ -188,11 +188,11 @@ #> fold_rev (Logic.all o Free) fixes fun export_thm thy (fixes, assumes) = - fold_rev (implies_intr o cprop_of) assumes - #> fold_rev (forall_intr o cterm_of thy o Free) fixes + fold_rev (Thm.implies_intr o cprop_of) assumes + #> fold_rev (Thm.forall_intr o cterm_of thy o Free) fixes fun import_thm thy (fixes, athms) = - fold (forall_elim o cterm_of thy o Free) fixes + fold (Thm.forall_elim o cterm_of thy o Free) fixes #> fold Thm.elim_implies athms @@ -241,7 +241,7 @@ fun rewrite_by_tree thy h ih x tr = let - fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x) + fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (cterm_of thy t), x) | rewrite_help fix h_as x (RCall (_ $ arg, st)) = let val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *) @@ -250,11 +250,11 @@ |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner)))) (* (a, h a) : G *) val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih - val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *) + val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *) - val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner + val h_a'_eq_h_a = Thm.combination (Thm.reflexive (cterm_of thy h)) inner val h_a_eq_f_a = eq RS eq_reflection - val result = transitive h_a'_eq_h_a h_a_eq_f_a + val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a in (result, x') end diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Sat May 15 21:50:05 2010 +0200 @@ -154,9 +154,9 @@ val rhs = inst pre_rhs val cqs = map (cterm_of thy) qs - val ags = map (assume o cterm_of thy) gs + val ags = map (Thm.assume o cterm_of thy) gs - val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) + val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) in ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } @@ -188,15 +188,15 @@ (* Instantiate the GIntro thm with "f" and import into the clause context. *) val lGI = GIntro_thm - |> forall_elim (cert f) - |> fold forall_elim cqs + |> Thm.forall_elim (cert f) + |> fold Thm.forall_elim cqs |> fold Thm.elim_implies ags fun mk_call_info (rcfix, rcassm, rcarg) RI = let val llRI = RI - |> fold forall_elim cqs - |> fold (forall_elim o cert o Free) rcfix + |> fold Thm.forall_elim cqs + |> fold (Thm.forall_elim o cert o Free) rcfix |> fold Thm.elim_implies ags |> fold Thm.elim_implies rcassm @@ -242,20 +242,20 @@ val compat = lookup_compat_thm j i cts in compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) - |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) + |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold Thm.elim_implies agsj |> fold Thm.elim_implies agsi - |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) + |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) end else let val compat = lookup_compat_thm i j cts in compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) - |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) + |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold Thm.elim_implies agsi |> fold Thm.elim_implies agsj - |> Thm.elim_implies (assume lhsi_eq_lhsj) + |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) end end @@ -274,16 +274,16 @@ val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs val h_assums = map (fn RCInfo {h_assum, ...} => - assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs + Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree val replace_lemma = (eql RS meta_eq_to_obj_eq) - |> implies_intr (cprop_of case_hyp) - |> fold_rev (implies_intr o cprop_of) h_assums - |> fold_rev (implies_intr o cprop_of) ags - |> fold_rev forall_intr cqs + |> Thm.implies_intr (cprop_of case_hyp) + |> fold_rev (Thm.implies_intr o cprop_of) h_assums + |> fold_rev (Thm.implies_intr o cprop_of) ags + |> fold_rev Thm.forall_intr cqs |> Thm.close_derivation in replace_lemma @@ -301,30 +301,30 @@ val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' val compat = get_compat_thm thy compat_store i j cctxi cctxj - val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj + val Ghsj' = map (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj val RLj_import = RLj - |> fold forall_elim cqsj' + |> fold Thm.forall_elim cqsj' |> fold Thm.elim_implies agsj' |> fold Thm.elim_implies Ghsj' - val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) - val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) + val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) + val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) in (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) - |> implies_elim RLj_import + |> Thm.implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) - |> fold_rev (implies_intr o cprop_of) Ghsj' - |> fold_rev (implies_intr o cprop_of) agsj' + |> fold_rev (Thm.implies_intr o cprop_of) Ghsj' + |> fold_rev (Thm.implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) - |> implies_intr (cprop_of y_eq_rhsj'h) - |> implies_intr (cprop_of lhsi_eq_lhsj') - |> fold_rev forall_intr (cterm_of thy h :: cqsj') + |> Thm.implies_intr (cprop_of y_eq_rhsj'h) + |> Thm.implies_intr (cprop_of lhsi_eq_lhsj') + |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj') end @@ -338,13 +338,13 @@ val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) - |> fold_rev (implies_intr o cprop_of) CCas - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs + |> fold_rev (Thm.implies_intr o cprop_of) CCas + |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs val existence = fold (curry op COMP o prep_RC) RCs lGI val P = cterm_of thy (mk_eq (y, rhsC)) - val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) + val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas @@ -353,13 +353,13 @@ Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single val uniqueness = G_cases - |> forall_elim (cterm_of thy lhs) - |> forall_elim (cterm_of thy y) - |> forall_elim P + |> Thm.forall_elim (cterm_of thy lhs) + |> Thm.forall_elim (cterm_of thy y) + |> Thm.forall_elim P |> Thm.elim_implies G_lhs_y |> fold elim_implies_eta unique_clauses - |> implies_intr (cprop_of G_lhs_y) - |> forall_intr (cterm_of thy y) + |> Thm.implies_intr (cprop_of G_lhs_y) + |> Thm.forall_intr (cterm_of thy y) val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) @@ -368,16 +368,16 @@ |> curry (op COMP) existence |> curry (op COMP) uniqueness |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) - |> implies_intr (cprop_of case_hyp) - |> fold_rev (implies_intr o cprop_of) ags - |> fold_rev forall_intr cqs + |> Thm.implies_intr (cprop_of case_hyp) + |> fold_rev (Thm.implies_intr o cprop_of) ags + |> fold_rev Thm.forall_intr cqs val function_value = existence - |> implies_intr ihyp - |> implies_intr (cprop_of case_hyp) - |> forall_intr (cterm_of thy x) - |> forall_elim (cterm_of thy lhs) + |> Thm.implies_intr ihyp + |> Thm.implies_intr (cprop_of case_hyp) + |> Thm.forall_intr (cterm_of thy x) + |> Thm.forall_elim (cterm_of thy lhs) |> curry (op RS) refl in (exactly_one, function_value) @@ -396,7 +396,7 @@ Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |> cterm_of thy - val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0 + val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |> instantiate' [] [NONE, SOME (cterm_of thy h)] @@ -412,17 +412,17 @@ val graph_is_function = complete |> Thm.forall_elim_vars 0 |> fold (curry op COMP) ex1s - |> implies_intr (ihyp) - |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) - |> forall_intr (cterm_of thy x) + |> Thm.implies_intr (ihyp) + |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) + |> Thm.forall_intr (cterm_of thy x) |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) - |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) + |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) val goalstate = Conjunction.intr graph_is_function complete |> Thm.close_derivation |> Goal.protect - |> fold_rev (implies_intr o cprop_of) compat - |> implies_intr (cprop_of complete) + |> fold_rev (Thm.implies_intr o cprop_of) compat + |> Thm.implies_intr (cprop_of complete) in (goalstate, values) end @@ -544,7 +544,7 @@ let fun inst_term t = subst_bound(f, abstract_over (fvar, t)) in - (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) + (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) end @@ -562,14 +562,14 @@ val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) in - ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward)) + ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) |> (fn it => it COMP graph_is_function) - |> implies_intr z_smaller - |> forall_intr (cterm_of thy z) + |> Thm.implies_intr z_smaller + |> Thm.forall_intr (cterm_of thy z) |> (fn it => it COMP valthm) - |> implies_intr lhs_acc + |> Thm.implies_intr lhs_acc |> asm_simplify (HOL_basic_ss addsimps [f_iff]) - |> fold_rev (implies_intr o cprop_of) ags + |> fold_rev (Thm.implies_intr o cprop_of) ags |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end in @@ -588,7 +588,7 @@ val Globals {domT, x, z, a, P, D, ...} = globals val acc_R = mk_acc domT R - val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) + val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) val D_subset = cterm_of thy (Logic.all x @@ -606,7 +606,7 @@ HOLogic.mk_Trueprop (P $ Bound 0))) |> cterm_of thy - val aihyp = assume ihyp + val aihyp = Thm.assume ihyp fun prove_case clause = let @@ -622,10 +622,10 @@ end fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih - |> forall_elim (cterm_of thy rcarg) + |> Thm.forall_elim (cterm_of thy rcarg) |> Thm.elim_implies llRI - |> fold_rev (implies_intr o cprop_of) CCas - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs + |> fold_rev (Thm.implies_intr o cprop_of) CCas + |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) @@ -636,19 +636,19 @@ |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> cterm_of thy - val P_lhs = assume step - |> fold forall_elim cqs + val P_lhs = Thm.assume step + |> fold Thm.forall_elim cqs |> Thm.elim_implies lhs_D |> fold Thm.elim_implies ags |> fold Thm.elim_implies P_recs val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) - |> symmetric (* P lhs == P x *) - |> (fn eql => equal_elim eql P_lhs) (* "P x" *) - |> implies_intr (cprop_of case_hyp) - |> fold_rev (implies_intr o cprop_of) ags - |> fold_rev forall_intr cqs + |> Thm.symmetric (* P lhs == P x *) + |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) + |> Thm.implies_intr (cprop_of case_hyp) + |> fold_rev (Thm.implies_intr o cprop_of) ags + |> fold_rev Thm.forall_intr cqs in (res, step) end @@ -658,33 +658,33 @@ val istep = complete_thm |> Thm.forall_elim_vars 0 |> fold (curry op COMP) cases (* P x *) - |> implies_intr ihyp - |> implies_intr (cprop_of x_D) - |> forall_intr (cterm_of thy x) + |> Thm.implies_intr ihyp + |> Thm.implies_intr (cprop_of x_D) + |> Thm.forall_intr (cterm_of thy x) val subset_induct_rule = acc_subset_induct - |> (curry op COMP) (assume D_subset) - |> (curry op COMP) (assume D_dcl) - |> (curry op COMP) (assume a_D) + |> (curry op COMP) (Thm.assume D_subset) + |> (curry op COMP) (Thm.assume D_dcl) + |> (curry op COMP) (Thm.assume a_D) |> (curry op COMP) istep - |> fold_rev implies_intr steps - |> implies_intr a_D - |> implies_intr D_dcl - |> implies_intr D_subset + |> fold_rev Thm.implies_intr steps + |> Thm.implies_intr a_D + |> Thm.implies_intr D_dcl + |> Thm.implies_intr D_subset val simple_induct_rule = subset_induct_rule - |> forall_intr (cterm_of thy D) - |> forall_elim (cterm_of thy acc_R) + |> Thm.forall_intr (cterm_of thy D) + |> Thm.forall_elim (cterm_of thy acc_R) |> assume_tac 1 |> Seq.hd |> (curry op COMP) (acc_downward |> (instantiate' [SOME (ctyp_of thy domT)] (map (SOME o cterm_of thy) [R, x, z])) - |> forall_intr (cterm_of thy z) - |> forall_intr (cterm_of thy x)) - |> forall_intr (cterm_of thy a) - |> forall_intr (cterm_of thy P) + |> Thm.forall_intr (cterm_of thy z) + |> Thm.forall_intr (cterm_of thy x)) + |> Thm.forall_intr (cterm_of thy a) + |> Thm.forall_intr (cterm_of thy P) in simple_induct_rule end @@ -736,18 +736,19 @@ |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> cterm_of thy - val thm = assume hyp - |> fold forall_elim cqs + val thm = Thm.assume hyp + |> fold Thm.forall_elim cqs |> fold Thm.elim_implies ags |> Function_Ctx_Tree.import_thm thy (fixes, assumes) |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) - |> cterm_of thy |> assume + |> cterm_of thy |> Thm.assume val acc = thm COMP ih_case val z_acc_local = acc - |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection))))) + |> Conv.fconv_rule + (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) val ethm = z_acc_local |> Function_Ctx_Tree.export_thm thy (fixes, @@ -785,34 +786,34 @@ HOLogic.mk_Trueprop (acc_R $ Bound 0))) |> cterm_of thy - val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0 + val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], []) in R_cases - |> forall_elim (cterm_of thy z) - |> forall_elim (cterm_of thy x) - |> forall_elim (cterm_of thy (acc_R $ z)) - |> curry op COMP (assume R_z_x) + |> Thm.forall_elim (cterm_of thy z) + |> Thm.forall_elim (cterm_of thy x) + |> Thm.forall_elim (cterm_of thy (acc_R $ z)) + |> curry op COMP (Thm.assume R_z_x) |> fold_rev (curry op COMP) cases - |> implies_intr R_z_x - |> forall_intr (cterm_of thy z) + |> Thm.implies_intr R_z_x + |> Thm.forall_intr (cterm_of thy z) |> (fn it => it COMP accI) - |> implies_intr ihyp - |> forall_intr (cterm_of thy x) + |> Thm.implies_intr ihyp + |> Thm.forall_intr (cterm_of thy x) |> (fn it => Drule.compose_single(it,2,wf_induct_rule)) - |> curry op RS (assume wfR') + |> curry op RS (Thm.assume wfR') |> forall_intr_vars |> (fn it => it COMP allI) - |> fold implies_intr hyps - |> implies_intr wfR' - |> forall_intr (cterm_of thy R') - |> forall_elim (cterm_of thy (inrel_R)) + |> fold Thm.implies_intr hyps + |> Thm.implies_intr wfR' + |> Thm.forall_intr (cterm_of thy R') + |> Thm.forall_elim (cterm_of thy (inrel_R)) |> curry op RS wf_in_rel |> full_simplify (HOL_basic_ss addsimps [in_rel_def]) - |> forall_intr (cterm_of thy Rrel) + |> Thm.forall_intr (cterm_of thy Rrel) end @@ -919,11 +920,11 @@ RCss GIntro_thms) RIntro_thmss val complete = - mk_completeness globals clauses abstract_qglrs |> cert |> assume + mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs - |> map (cert #> assume) + |> map (cert #> Thm.assume) val compat_store = store_compat_thms n compat diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Function/function_lib.ML Sat May 15 21:50:05 2010 +0200 @@ -5,7 +5,7 @@ Some fairly general functions that should probably go somewhere else... *) -structure Function_Lib = +structure Function_Lib = (* FIXME proper signature *) struct fun map_option f NONE = NONE @@ -104,7 +104,7 @@ fun forall_intr_rename (n, cv) thm = let - val allthm = forall_intr cv thm + val allthm = Thm.forall_intr cv thm val (_ $ abs) = prop_of allthm in Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat May 15 21:50:05 2010 +0200 @@ -226,7 +226,7 @@ HOLogic.mk_Trueprop (P_comp $ Bound 0))) |> cert - val aihyp = assume ihyp + val aihyp = Thm.assume ihyp (* Rule for case splitting along the sum types *) val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches @@ -237,9 +237,9 @@ fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = let val fxs = map Free xs - val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) + val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) - val C_hyps = map (cert #> assume) Cs + val C_hyps = map (cert #> Thm.assume) Cs val (relevant_cases, ineqss') = (scases_idx ~~ ineqss) @@ -248,32 +248,33 @@ fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press = let - val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) + val case_hyps = + map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) val cqs = map (cert o Free) qs - val ags = map (assume o cert) gs + val ags = map (Thm.assume o cert) gs val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) val sih = full_simplify replace_x_ss aihyp fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = let - val cGas = map (assume o cert) Gas + val cGas = map (Thm.assume o cert) Gas val cGvs = map (cert o Free) Gvs - val import = fold forall_elim (cqs @ cGvs) + val import = fold Thm.forall_elim (cqs @ cGvs) #> fold Thm.elim_implies (ags @ cGas) val ipres = pres - |> forall_elim (cert (list_comb (P_of idx, rcargs))) + |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs))) |> import in sih - |> forall_elim (cert (inject idx rcargs)) + |> Thm.forall_elim (cert (inject idx rcargs)) |> Thm.elim_implies (import ineq) (* Psum rcargs *) |> Conv.fconv_rule sum_prod_conv |> Conv.fconv_rule ind_rulify |> (fn th => th COMP ipres) (* P rs *) - |> fold_rev (implies_intr o cprop_of) cGas - |> fold_rev forall_intr cGvs + |> fold_rev (Thm.implies_intr o cprop_of) cGas + |> fold_rev Thm.forall_intr cGvs end val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) @@ -288,13 +289,13 @@ foldl1 (uncurry Conv.combination_conv) (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) - val res = assume step - |> fold forall_elim cqs + val res = Thm.assume step + |> fold Thm.forall_elim cqs |> fold Thm.elim_implies ags |> fold Thm.elim_implies P_recs (* P lhs *) |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) - |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps) - |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) + |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps) + |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) in (res, (cidx, step)) end @@ -302,12 +303,12 @@ val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') val bstep = complete_thm - |> forall_elim (cert (list_comb (P, fxs))) - |> fold (forall_elim o cert) (fxs @ map Free ws) + |> Thm.forall_elim (cert (list_comb (P, fxs))) + |> fold (Thm.forall_elim o cert) (fxs @ map Free ws) |> fold Thm.elim_implies C_hyps |> fold Thm.elim_implies cases (* P xs *) - |> fold_rev (implies_intr o cprop_of) C_hyps - |> fold_rev (forall_intr o cert o Free) ws + |> fold_rev (Thm.implies_intr o cprop_of) C_hyps + |> fold_rev (Thm.forall_intr o cert o Free) ws val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) |> Goal.init @@ -316,8 +317,8 @@ |> Seq.hd |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) |> Goal.finish ctxt - |> implies_intr (cprop_of branch_hyp) - |> fold_rev (forall_intr o cert) fxs + |> Thm.implies_intr (cprop_of branch_hyp) + |> fold_rev (Thm.forall_intr o cert) fxs in (Pxs, steps) end @@ -328,8 +329,8 @@ val istep = sum_split_rule |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches - |> implies_intr ihyp - |> forall_intr (cert x) (* "!!x. (!!y P x" *) + |> Thm.implies_intr ihyp + |> Thm.forall_intr (cert x) (* "!!x. (!!y P x" *) val induct_rule = @{thm "wf_induct_rule"} @@ -353,10 +354,10 @@ val cert = cterm_of (ProofContext.theory_of ctxt) val ineqss = mk_ineqs R scheme - |> map (map (pairself (assume o cert))) + |> map (map (pairself (Thm.assume o cert))) val complete = - map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches) - val wf_thm = mk_wf R scheme |> cert |> assume + map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches) + val wf_thm = mk_wf R scheme |> cert |> Thm.assume val (descent, pres) = split_list (flat ineqss) val newgoals = complete @ pres @ wf_thm :: descent @@ -377,7 +378,7 @@ end val res = Conjunction.intr_balanced (map_index project branches) - |> fold_rev implies_intr (map cprop_of newgoals @ steps) + |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps) |> Drule.generalize ([], [Rn]) val nbranches = length branches diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Sat May 15 21:50:05 2010 +0200 @@ -164,12 +164,12 @@ val rhs = inst pre_rhs val cqs = map (cterm_of thy) qs - val ags = map (assume o cterm_of thy) gs + val ags = map (Thm.assume o cterm_of thy) gs - val import = fold forall_elim cqs + val import = fold Thm.forall_elim cqs #> fold Thm.elim_implies ags - val export = fold_rev (implies_intr o cprop_of) ags + val export = fold_rev (Thm.implies_intr o cprop_of) ags #> fold_rev forall_intr_rename (oqnames ~~ cqs) in F ctxt (f, qs, gs, args, rhs) import export @@ -184,7 +184,7 @@ val (simp, restore_cond) = case cprems_of psimp of [] => (psimp, I) - | [cond] => (implies_elim psimp (assume cond), implies_intr cond) + | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) | _ => sys_error "Too many conditions" in @@ -202,9 +202,9 @@ val thy = ProofContext.theory_of ctxt val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) in - fold (fn x => fn thm => combination thm (reflexive x)) xs thm + fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |> Conv.fconv_rule (Thm.beta_conversion true) - |> fold_rev forall_intr xs + |> fold_rev Thm.forall_intr xs |> Thm.forall_elim_vars 0 end @@ -228,7 +228,7 @@ val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps val induct_inst = - forall_elim (cert case_exp) induct + Thm.forall_elim (cert case_exp) induct |> full_simplify SumTree.sumcase_split_ss |> full_simplify (HOL_basic_ss addsimps all_f_defs) @@ -238,9 +238,9 @@ val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) in (rule - |> forall_elim (cert inj) + |> Thm.forall_elim (cert inj) |> full_simplify SumTree.sumcase_split_ss - |> fold_rev (forall_intr o cert) (afs @ newPs), + |> fold_rev (Thm.forall_intr o cert) (afs @ newPs), k + length cargTs) end in @@ -255,7 +255,7 @@ val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => - (mk_applied_form lthy cargTs (symmetric f_def), f)) + (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) parts |> split_list diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Function/pat_completeness.ML --- a/src/HOL/Tools/Function/pat_completeness.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Function/pat_completeness.ML Sat May 15 21:50:05 2010 +0200 @@ -24,7 +24,7 @@ fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) -fun inst_free var inst = forall_elim inst o forall_intr var +fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var fun inst_case_thm thy x P thm = let val [Pv, xv] = Term.add_vars (prop_of thm) [] @@ -69,10 +69,10 @@ let val (_, subps) = strip_comb pat val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) - val c_eq_pat = simplify (HOL_basic_ss addsimps (map assume eqs)) c_assum + val c_eq_pat = simplify (HOL_basic_ss addsimps (map Thm.assume eqs)) c_assum in (subps @ pats, - fold_rev implies_intr eqs (implies_elim thm c_eq_pat)) + fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat)) end @@ -82,12 +82,12 @@ let val (avars, pvars, newidx) = invent_vars cons idx val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars)))) - val c_assum = assume c_hyp + val c_assum = Thm.assume c_hyp val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats) in o_alg thy P newidx (avars @ vs) newpats - |> implies_intr c_hyp - |> fold_rev (forall_intr o cterm_of thy) avars + |> Thm.implies_intr c_hyp + |> fold_rev (Thm.forall_intr o cterm_of thy) avars end | constr_case _ _ _ _ _ _ = raise Match and o_alg thy P idx [] (([], Pthm) :: _) = Pthm @@ -119,11 +119,11 @@ |> cterm_of thy val hyps = map2 mk_assum qss patss - fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp) + fun inst_hyps hyp qs = fold (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp) val assums = map2 inst_hyps hyps qss in o_alg thy P 2 xs (patss ~~ assums) - |> fold_rev implies_intr hyps + |> fold_rev Thm.implies_intr hyps end fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => @@ -147,7 +147,7 @@ val patss = map (map snd) x_pats val complete_thm = prove_completeness thy xs thesis qss patss - |> fold_rev (forall_intr o cterm_of thy) vs + |> fold_rev (Thm.forall_intr o cterm_of thy) vs in PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st)) end diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sat May 15 21:50:05 2010 +0200 @@ -331,7 +331,7 @@ | t => if is_intrel t then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop)) RS eq_reflection - else reflexive ct; + else Thm.reflexive ct; val dvdc = @{cterm "op dvd :: int => _"}; @@ -369,7 +369,7 @@ (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x)) @{cterm "0::int"}))) - in equal_elim (Thm.symmetric th) TrueI end; + in Thm.equal_elim (Thm.symmetric th) TrueI end; val notz = let val tab = fold Inttab.update (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty @@ -412,11 +412,11 @@ val ltx = Thm.capply (Thm.capply cmulC clt) cx val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth) val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex - val thf = transitive th - (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th') + val thf = Thm.transitive th + (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th') val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true - ||> beta_conversion true |>> Thm.symmetric - in transitive (transitive lth thf) rth end; + ||> Thm.beta_conversion true |>> Thm.symmetric + in Thm.transitive (Thm.transitive lth thf) rth end; val emptyIS = @{cterm "{}::int set"}; @@ -459,7 +459,7 @@ Simplifier.rewrite lin_ss (Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd)) - in equal_elim (Thm.symmetric th) TrueI end; + in Thm.equal_elim (Thm.symmetric th) TrueI end; val dvd = let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in fn ct => the (Inttab.lookup tab (term_of ct |> dest_number)) @@ -471,7 +471,7 @@ let val th = Simplifier.rewrite lin_ss (Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd)) - in equal_elim (Thm.symmetric th) TrueI end; + in Thm.equal_elim (Thm.symmetric th) TrueI end; (* A and B set *) local val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"} @@ -483,7 +483,7 @@ | Const(@{const_name insert}, _) $ y $ _ => let val (cy,S') = Thm.dest_binop S in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 - else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) + else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) (provein x S') end end @@ -494,14 +494,14 @@ if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) then (bl,b0,decomp_minf, - fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) + fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)])) [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, bsetdisj,infDconj, infDdisj]), cpmi) else (al,a0,decomp_pinf,fn A => - (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp) + (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp) [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)])) [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, @@ -776,7 +776,7 @@ fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) val p' = fold_rev gen ts p - in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end)); + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); local val ss1 = comp_ss @@ -792,7 +792,7 @@ @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}] addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms} - @ map (symmetric o mk_meta_eq) + @ map (Thm.symmetric o mk_meta_eq) [@{thm "dvd_eq_mod_eq_0"}, @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}] @@ -823,7 +823,7 @@ then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))) else Conv.arg_conv (conv ctxt) p val p' = Thm.rhs_of cpth - val th = implies_intr p' (equal_elim (symmetric cpth) (assume p')) + val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p')) in rtac th i end handle COOPER _ => no_tac); diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Qelim/ferrante_rackoff.ML --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sat May 15 21:50:05 2010 +0200 @@ -69,7 +69,7 @@ val th0 = if mi then instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th - in implies_elim (implies_elim th0 th') th'' end + in Thm.implies_elim (Thm.implies_elim th0 th') th'' end in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') end @@ -88,7 +88,7 @@ val enth = Drule.arg_cong_rule ce nthx val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"} fun ins x th = - implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) + Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th val fU = fold ins u th0 val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU) @@ -102,7 +102,7 @@ | Const(@{const_name insert}, _) $ y $_ => let val (cy,S') = Thm.dest_binop S in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 - else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) + else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) (provein x S') end end @@ -152,7 +152,7 @@ | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq] | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq]) val tU = U t - fun Ufw th = implies_elim th tU + fun Ufw th = Thm.implies_elim th tU in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th] end in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end) @@ -164,7 +164,7 @@ [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th] val bex_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)})) - val result_th = fconv_rule (arg_conv bex_conv) (transitive enth qe_th) + val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th) in result_th end diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Qelim/langford.ML --- a/src/HOL/Tools/Qelim/langford.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Qelim/langford.ML Sat May 15 21:50:05 2010 +0200 @@ -22,7 +22,7 @@ fun prove_finite cT u = let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"} fun ins x th = - implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) + Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th in fold ins u th0 end; @@ -51,17 +51,17 @@ (Const (@{const_name Orderings.bot}, _),_) => let val (neU,fU) = proveneF U - in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end + in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end | (_,Const (@{const_name Orderings.bot}, _)) => let val (neL,fL) = proveneF L - in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end + in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end | (_,_) => let val (neL,fL) = proveneF L val (neU,fU) = proveneF U - in simp_rule (transitive ths (dlo_qeth OF [neL, neU, fL, fU])) + in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) end in qe end | _ => error "dlo_qe : Not an existential formula"; @@ -101,8 +101,8 @@ fun conj_aci_rule eq = let val (l,r) = Thm.dest_equals eq - fun tabl c = the (Termtab.lookup (mk_conj_tab (assume l)) (term_of c)) - fun tabr c = the (Termtab.lookup (mk_conj_tab (assume r)) (term_of c)) + fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c)) + fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c)) val ll = Thm.dest_arg l val rr = Thm.dest_arg r @@ -111,7 +111,7 @@ val thr = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI} - in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end; + in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end; fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x); @@ -136,7 +136,7 @@ | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx)))) - |> abstract_rule xn x |> Drule.arg_cong_rule e + |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |> Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) @@ -144,7 +144,7 @@ end | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs)))) - |> abstract_rule xn x |> Drule.arg_cong_rule e + |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |> Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (HOL_basic_ss addsimps (simp_thms @ ex_simps)))) @@ -167,7 +167,7 @@ @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]) in fn p => Qelim.gen_qelim_conv pcv pcv dnfex_conv cons - (Thm.add_cterm_frees p []) (K reflexive) (K reflexive) + (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive) (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p end; @@ -212,7 +212,7 @@ fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) val p' = fold_rev gen ts p - in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end)); + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); fun cfrees ats ct = diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Sat May 15 21:50:05 2010 +0200 @@ -47,7 +47,7 @@ val p = Thm.dest_arg p val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p) val th = instantiate' [SOME T] [SOME p] all_not_ex - in transitive th (conv env (Thm.rhs_of th)) + in Thm.transitive th (conv env (Thm.rhs_of th)) end | _ => atcv env p in precv then_conv (conv env) then_conv postcv end diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat May 15 21:50:05 2010 +0200 @@ -517,7 +517,7 @@ *) fun clean_tac lthy = let - val defs = map (symmetric o #def) (qconsts_dest lthy) + val defs = map (Thm.symmetric o #def) (qconsts_dest lthy) val prs = prs_rules_get lthy val ids = id_simps_get lthy val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat May 15 21:50:05 2010 +0200 @@ -35,7 +35,7 @@ (* Useful Theorems *) (* ------------------------------------------------------------------------- *) val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} -val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp} +val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} @@ -364,7 +364,7 @@ in cterm_instantiate substs th end; (* INFERENCE RULE: AXIOM *) -fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th); +fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) (* INFERENCE RULE: ASSUME *) @@ -527,7 +527,7 @@ val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) - val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) + val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') val eq_terms = map (pairself (cterm_of thy)) (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat May 15 21:50:05 2010 +0200 @@ -209,7 +209,7 @@ Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) end else if loose_bvar1 (rand,0) then (*B or eta*) - if rand = Bound 0 then eta_conversion ct + if rand = Bound 0 then Thm.eta_conversion ct else (*B*) let val crand = cterm_of thy (Abs(x,xT,rand)) val crator = cterm_of thy rator @@ -225,7 +225,7 @@ (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested prefix for the constants.*) fun combinators_aux ct = - if lambda_free (term_of ct) then reflexive ct + if lambda_free (term_of ct) then Thm.reflexive ct else case term_of ct of Abs _ => @@ -234,17 +234,17 @@ val u_th = combinators_aux cta val cu = Thm.rhs_of u_th val comb_eq = abstract (Thm.cabs cv cu) - in transitive (abstract_rule v cv u_th) comb_eq end + in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end | _ $ _ => let val (ct1, ct2) = Thm.dest_comb ct - in combination (combinators_aux ct1) (combinators_aux ct2) end; + in Thm.combination (combinators_aux ct1) (combinators_aux ct2) end; fun combinators th = if lambda_free (prop_of th) then th else let val th = Drule.eta_contraction_rule th val eqth = combinators_aux (cprop_of th) - in equal_elim eqth th end + in Thm.equal_elim eqth th end handle THM (msg,_,_) => (warning (cat_lines ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th, @@ -298,7 +298,7 @@ (*Generate Skolem functions for a theorem supplied in nnf*) fun assume_skolem_of_def s th = - map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th); + map (skolem_of_def o Thm.assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th); (*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***) diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Sat May 15 21:50:05 2010 +0200 @@ -79,8 +79,8 @@ (* beta-eta contract the theorem *) fun beta_eta_contract thm = let - val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm - val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 + val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm + val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 in thm3 end; (* make a casethm from an induction thm *) diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Sat May 15 21:50:05 2010 +0200 @@ -172,7 +172,7 @@ val [P,Q] = OldTerm.term_vars prop val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1 in -fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1) +fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1) handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg; end; @@ -181,7 +181,7 @@ val [P,Q] = OldTerm.term_vars prop val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2 in -fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2) +fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2) handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg; end; @@ -276,11 +276,11 @@ val prop = Thm.prop_of spec val x = hd (tl (OldTerm.term_vars prop)) val cTV = ctyp_of thy (type_of x) - val gspec = forall_intr (cterm_of thy x) spec + val gspec = Thm.forall_intr (cterm_of thy x) spec in fun SPEC tm thm = let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec - in thm RS (forall_elim tm gspec') end + in thm RS (Thm.forall_elim tm gspec') end end; fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm; @@ -302,7 +302,7 @@ ctm_theta s (Vartab.dest tm_theta)) in fun GEN v th = - let val gth = forall_intr v th + let val gth = Thm.forall_intr v th val thy = Thm.theory_of_thm gth val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) @@ -533,9 +533,9 @@ *---------------------------------------------------------------------------*) fun list_beta_conv tm = - let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th)))) + let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th)))) fun iter [] = Thm.reflexive tm - | iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v)) + | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v)) in iter end; @@ -619,7 +619,7 @@ fun VSTRUCT_ELIM tych a vstr th = let val L = S.free_vars_lr vstr val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr))) - val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th) + val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th) val thm2 = forall_intr_list (map tych L) thm1 val thm3 = forall_elim_list (XFILL tych a vstr) thm2 in refl RS @@ -630,7 +630,7 @@ let val a1 = tych a val vstr1 = tych vstr in - forall_intr a1 + Thm.forall_intr a1 (if (is_Free vstr) then cterm_instantiate [(vstr1,a1)] th else VSTRUCT_ELIM tych a vstr th) @@ -803,7 +803,7 @@ val names = OldTerm.add_term_names (term_of ctm, []) val th1 = MetaSimplifier.rewrite_cterm(false,true,false) (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm - val th2 = equal_elim th1 th + val th2 = Thm.equal_elim th1 th in (th2, filter_out restricted (!tc_list)) end; diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Sat May 15 21:50:05 2010 +0200 @@ -556,8 +556,8 @@ else () val f_free = Free (fid, fastype_of f) (*'cos f is a Const*) val SV' = map tych SV; - val SVrefls = map reflexive SV' - val def0 = (fold (fn x => fn th => R.rbeta(combination th x)) + val SVrefls = map Thm.reflexive SV' + val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x)) SVrefls def) RS meta_eq_to_obj_eq val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0 diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/choice_specification.ML Sat May 15 21:50:05 2010 +0200 @@ -183,7 +183,7 @@ fun process_single ((name,atts),rew_imp,frees) args = let fun undo_imps thm = - equal_elim (symmetric rew_imp) thm + Thm.equal_elim (Thm.symmetric rew_imp) thm fun add_final (arg as (thy, thm)) = if name = "" diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Sat May 15 21:50:05 2010 +0200 @@ -435,9 +435,9 @@ val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *) val var = new_free () val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *) - val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) in iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *) end @@ -446,9 +446,9 @@ val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *) val var = new_free () val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *) - val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *) + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *) in iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *) end @@ -466,8 +466,8 @@ val var = new_free () val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var)) val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *) - val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *) - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *) + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *) + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *) val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *) in iff_trans OF [thm1, thm5] diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Sat May 15 21:50:05 2010 +0200 @@ -21,7 +21,7 @@ [name] => name | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm)); -val all_simps = map (symmetric o mk_meta_eq) @{thms HOL.all_simps}; +val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps}; fun prf_of thm = let diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/inductive_set.ML Sat May 15 21:50:05 2010 +0200 @@ -114,9 +114,9 @@ let val rews = map mk_rew ts in if forall is_none rews then NONE - else SOME (fold (fn th1 => fn th2 => combination th2 th1) - (map2 (fn SOME r => K r | NONE => reflexive o cterm_of thy) - rews ts) (reflexive (cterm_of thy h))) + else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1) + (map2 (fn SOME r => K r | NONE => Thm.reflexive o cterm_of thy) + rews ts) (Thm.reflexive (cterm_of thy h))) end | NONE => NONE) | _ => NONE diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/int_arith.ML Sat May 15 21:50:05 2010 +0200 @@ -21,7 +21,7 @@ That is, m and n consist only of 1s combined with "+", "-" and "*". *) -val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0}; +val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0}; val lhss0 = [@{cpat "0::?'a::ring"}]; @@ -35,7 +35,7 @@ make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc", proc = proc0, identifier = []}; -val oneth = (symmetric o mk_meta_eq) @{thm of_int_1}; +val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1}; val lhss1 = [@{cpat "1::?'a::ring_1"}]; diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat May 15 21:50:05 2010 +0200 @@ -614,12 +614,12 @@ fun prove_nz ss T t = let - val z = instantiate_cterm ([(zT,T)],[]) zr - val eq = instantiate_cterm ([(eqT,T)],[]) geq + val z = Thm.instantiate_cterm ([(zT,T)],[]) zr + val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply eq t) z))) - in equal_elim (symmetric th) TrueI + in Thm.equal_elim (Thm.symmetric th) TrueI end fun proc phi ss ct = @@ -630,7 +630,7 @@ val T = ctyp_of_term x val [y_nz, z_nz] = map (prove_nz ss T) [y, z] val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq - in SOME (implies_elim (implies_elim th y_nz) z_nz) + in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE @@ -643,13 +643,13 @@ let val (x,y) = Thm.dest_binop l val z = r val _ = map (HOLogic.dest_number o term_of) [x,y,z] val ynz = prove_nz ss T y - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) + in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) end | (_, Const (@{const_name Rings.divide},_)$_$_) => let val (x,y) = Thm.dest_binop r val z = l val _ = map (HOLogic.dest_number o term_of) [x,y,z] val ynz = prove_nz ss T y - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) + in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) end | _ => NONE) end diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/record.ML Sat May 15 21:50:05 2010 +0200 @@ -2171,7 +2171,7 @@ fun get_upd_acc_congs () = let - val symdefs = map symmetric (sel_defs @ upd_defs); + val symdefs = map Thm.symmetric (sel_defs @ upd_defs); val fold_ss = HOL_basic_ss addsimps symdefs; val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists; in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end; @@ -2257,17 +2257,17 @@ val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l); val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r); val thl = - assume cl (*All r. P r*) (* 1 *) - |> obj_to_meta_all (*!!r. P r*) - |> equal_elim split_meta' (*!!n m more. P (ext n m more)*) - |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*) - |> implies_intr cl (* 1 ==> 2 *) + Thm.assume cl (*All r. P r*) (* 1 *) + |> obj_to_meta_all (*!!r. P r*) + |> Thm.equal_elim split_meta' (*!!n m more. P (ext n m more)*) + |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*) + |> Thm.implies_intr cl (* 1 ==> 2 *) val thr = - assume cr (*All n m more. P (ext n m more)*) - |> obj_to_meta_all (*!!n m more. P (ext n m more)*) - |> equal_elim (symmetric split_meta') (*!!r. P r*) - |> meta_to_obj_all (*All r. P r*) - |> implies_intr cr (* 2 ==> 1 *) + Thm.assume cr (*All n m more. P (ext n m more)*) + |> obj_to_meta_all (*!!n m more. P (ext n m more)*) + |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*) + |> meta_to_obj_all (*All r. P r*) + |> Thm.implies_intr cr (* 2 ==> 1 *) in thr COMP (thl COMP iffI) end; diff -r dbf831a50e4a -r 9bec62c10714 src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Sat May 15 21:50:05 2010 +0200 @@ -147,7 +147,7 @@ val semiring = (sr_ops, sr_rules'); val ring = (r_ops, r_rules'); val field = (f_ops, f_rules'); - val ideal' = map (symmetric o mk_meta) ideal + val ideal' = map (Thm.symmetric o mk_meta) ideal in AList.delete Thm.eq_thm key #> cons (key, ({vars = vars, semiring = semiring, @@ -328,16 +328,16 @@ ((let val (rx,rn) = dest_pow r val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29 val (tm1,tm2) = Thm.dest_comb(concl th1) in - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) + Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) handle CTERM _ => (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31 val (tm1,tm2) = Thm.dest_comb(concl th1) in - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end) + Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end) handle CTERM _ => ((let val (rx,rn) = dest_pow r val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30 val (tm1,tm2) = Thm.dest_comb(concl th1) in - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) + Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) handle CTERM _ => inst_thm [(cx,l)] pthm_32 )) @@ -348,7 +348,7 @@ fun monomial_deone th = (let val (l,r) = dest_mul(concl th) in if l aconvc one_tm - then transitive th (inst_thm [(ca,r)] pthm_13) else th end) + then Thm.transitive th (inst_thm [(ca,r)] pthm_13) else th end) handle CTERM _ => th; (* Conversion for "(monomial)^n", where n is a numeral. *) @@ -357,7 +357,7 @@ let fun monomial_pow tm bod ntm = if not(is_comb bod) - then reflexive tm + then Thm.reflexive tm else if is_semiring_constant bod then semiring_pow_conv tm @@ -365,7 +365,7 @@ let val (lopr,r) = Thm.dest_comb bod in if not(is_comb lopr) - then reflexive tm + then Thm.reflexive tm else let val (opr,l) = Thm.dest_comb lopr @@ -374,7 +374,7 @@ then let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34 val (l,r) = Thm.dest_comb(concl th1) - in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r)) + in Thm.transitive th1 (Drule.arg_cong_rule l (nat_add_conv r)) end else if opr aconvc mul_tm @@ -385,9 +385,9 @@ val (x,y) = Thm.dest_comb xy val thl = monomial_pow y l ntm val thr = monomial_pow z r ntm - in transitive th1 (combination (Drule.arg_cong_rule x thl) thr) + in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule x thl) thr) end - else reflexive tm + else Thm.reflexive tm end end in fn tm => @@ -436,18 +436,18 @@ val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 - val th3 = transitive th1 th2 + val th3 = Thm.transitive th1 th2 val (tm5,tm6) = Thm.dest_comb(concl th3) val (tm7,tm8) = Thm.dest_comb tm6 val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8 - in transitive th3 (Drule.arg_cong_rule tm5 th4) + in Thm.transitive th3 (Drule.arg_cong_rule tm5 th4) end else let val th0 = if ord < 0 then pthm_16 else pthm_17 val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0 val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm2 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) + in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) end end) handle CTERM _ => @@ -459,14 +459,14 @@ val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 - in transitive th1 th2 + in Thm.transitive th1 th2 end else if ord < 0 then let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19 val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm2 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) + in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) end else inst_thm [(ca,l),(cb,r)] pthm_09 end)) end) @@ -480,22 +480,22 @@ let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21 val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 - in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2) + in Thm.transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2) end else if ord > 0 then let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22 val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm2 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) + in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) end - else reflexive tm + else Thm.reflexive tm end) handle CTERM _ => (let val vr = powvar r val ord = vorder vl vr in if ord = 0 then powvar_mul_conv tm else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09 - else reflexive tm + else Thm.reflexive tm end)) end)) in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r) end @@ -511,8 +511,8 @@ val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37 val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 - val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2) - in transitive th1 th2 + val th2 = Thm.combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2) + in Thm.transitive th1 th2 end) handle CTERM _ => monomial_mul_conv tm) end @@ -537,11 +537,11 @@ val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4) - val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2) + val th3 = Thm.transitive th1 (Drule.fun_cong_rule th2 tm2) val tm5 = concl th3 in if (Thm.dest_arg1 tm5) aconvc zero_tm - then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11) + then Thm.transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11) else monomial_deone th3 end end; @@ -603,9 +603,9 @@ val l = Thm.dest_arg lopr in if l aconvc zero_tm - then transitive th (inst_thm [(ca,r)] pthm_07) else + then Thm.transitive th (inst_thm [(ca,r)] pthm_07) else if r aconvc zero_tm - then transitive th (inst_thm [(ca,l)] pthm_08) else th + then Thm.transitive th (inst_thm [(ca,l)] pthm_08) else th end end fun padd tm = @@ -628,14 +628,14 @@ val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4) - in dezero_rule (transitive th1 (combination th2 (padd tm2))) + in dezero_rule (Thm.transitive th1 (Thm.combination th2 (padd tm2))) end else (* ord <> 0*) let val th1 = if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 val (tm1,tm2) = Thm.dest_comb(concl th1) - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) + in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) end end else (* not (is_add r)*) @@ -646,13 +646,13 @@ val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 - in dezero_rule (transitive th1 th2) + in dezero_rule (Thm.transitive th1 th2) end else (* ord <> 0*) if ord > 0 then let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 val (tm1,tm2) = Thm.dest_comb(concl th1) - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) + in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) end else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) end @@ -667,21 +667,21 @@ val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 - in dezero_rule (transitive th1 th2) + in dezero_rule (Thm.transitive th1 th2) end else - if ord > 0 then reflexive tm + if ord > 0 then Thm.reflexive tm else let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 val (tm1,tm2) = Thm.dest_comb(concl th1) - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) + in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) end end else let val ord = morder l r in if ord = 0 then monomial_add_conv tm - else if ord > 0 then dezero_rule(reflexive tm) + else if ord > 0 then dezero_rule(Thm.reflexive tm) else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) end end @@ -699,7 +699,7 @@ else if not(is_add r) then let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09 - in transitive th1 (polynomial_monomial_mul_conv(concl th1)) + in Thm.transitive th1 (polynomial_monomial_mul_conv(concl th1)) end else let val (a,b) = dest_add l @@ -707,8 +707,8 @@ val (tm1,tm2) = Thm.dest_comb(concl th1) val (tm3,tm4) = Thm.dest_comb tm1 val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4) - val th3 = transitive th1 (combination th2 (pmul tm2)) - in transitive th3 (polynomial_add_conv (concl th3)) + val th3 = Thm.transitive th1 (Thm.combination th2 (pmul tm2)) + in Thm.transitive th3 (polynomial_add_conv (concl th3)) end end in fn tm => @@ -740,9 +740,9 @@ let val th1 = num_conv n val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38 val (tm1,tm2) = Thm.dest_comb(concl th2) - val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2)) - val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3 - in transitive th4 (polynomial_mul_conv (concl th4)) + val th3 = Thm.transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2)) + val th4 = Thm.transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3 + in Thm.transitive th4 (polynomial_mul_conv (concl th4)) end end in fn tm => @@ -755,8 +755,8 @@ let val (l,r) = Thm.dest_comb tm in if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else let val th1 = inst_thm [(cx',r)] neg_mul - val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) - in transitive th2 (polynomial_monomial_mul_conv (concl th2)) + val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) + in Thm.transitive th2 (polynomial_monomial_mul_conv (concl th2)) end end; @@ -767,51 +767,52 @@ val th1 = inst_thm [(cx',l),(cy',r)] sub_add val (tm1,tm2) = Thm.dest_comb(concl th1) val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2) - in transitive th1 (transitive th2 (polynomial_add_conv (concl th2))) + in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv (concl th2))) end; (* Conversion from HOL term. *) fun polynomial_conv tm = if is_semiring_constant tm then semiring_add_conv tm - else if not(is_comb tm) then reflexive tm + else if not(is_comb tm) then Thm.reflexive tm else let val (lopr,r) = Thm.dest_comb tm in if lopr aconvc neg_tm then let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) - in transitive th1 (polynomial_neg_conv (concl th1)) + in Thm.transitive th1 (polynomial_neg_conv (concl th1)) end else if lopr aconvc inverse_tm then let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) - in transitive th1 (semiring_mul_conv (concl th1)) + in Thm.transitive th1 (semiring_mul_conv (concl th1)) end else - if not(is_comb lopr) then reflexive tm + if not(is_comb lopr) then Thm.reflexive tm else let val (opr,l) = Thm.dest_comb lopr in if opr aconvc pow_tm andalso is_numeral r then let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r - in transitive th1 (polynomial_pow_conv (concl th1)) + in Thm.transitive th1 (polynomial_pow_conv (concl th1)) end else if opr aconvc divide_tm then - let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) + let val th1 = Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r) val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv) (Thm.rhs_of th1) - in transitive th1 th2 + in Thm.transitive th1 th2 end else if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm then - let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r) + let val th1 = + Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r) val f = if opr aconvc add_tm then polynomial_add_conv else if opr aconvc mul_tm then polynomial_mul_conv else polynomial_sub_conv - in transitive th1 (f (concl th1)) + in Thm.transitive th1 (f (concl th1)) end - else reflexive tm + else Thm.reflexive tm end end; in @@ -852,7 +853,7 @@ fun semiring_normalize_ord_conv ctxt ord tm = (case match ctxt tm of - NONE => reflexive tm + NONE => Thm.reflexive tm | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; diff -r dbf831a50e4a -r 9bec62c10714 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat May 15 21:50:05 2010 +0200 @@ -845,8 +845,8 @@ (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of SOME spl => let val (ct1, ct2) = extract (cprop_of spl) - val thm1 = assume ct1 - val thm2 = assume ct2 + val thm1 = Thm.assume ct1 + val thm2 = Thm.assume ct2 in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]), ct2, elim_neq neqs (asms', asms@[thm2])) end @@ -858,8 +858,8 @@ let val (thm1, js1) = fwdproof ss tree1 js val (thm2, js2) = fwdproof ss tree2 js1 - val thm1' = implies_intr ct1 thm1 - val thm2' = implies_intr ct2 thm2 + val thm1' = Thm.implies_intr ct1 thm1 + val thm2' = Thm.implies_intr ct2 thm2 in (thm2' COMP (thm1' COMP thm), js2) end; (* FIXME needs handle THM _ => NONE ? *) @@ -869,11 +869,11 @@ val thy = ProofContext.theory_of ctxt val nTconcl = LA_Logic.neg_prop Tconcl val cnTconcl = cterm_of thy nTconcl - val nTconclthm = assume cnTconcl + val nTconclthm = Thm.assume cnTconcl val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm]) val (Falsethm, _) = fwdproof ss tree js val contr = if pos then LA_Logic.ccontr else LA_Logic.notI - val concl = implies_intr cnTconcl Falsethm COMP contr + val concl = Thm.implies_intr cnTconcl Falsethm COMP contr in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end (*in case concl contains ?-var, which makes assume fail:*) (* FIXME Variable.import_terms *) handle THM _ => NONE; diff -r dbf831a50e4a -r 9bec62c10714 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/Provers/hypsubst.ML Sat May 15 21:50:05 2010 +0200 @@ -143,7 +143,7 @@ [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (#prop (rep_thm th)))) then th RS Data.eq_reflection - else symmetric(th RS Data.eq_reflection) (*reorient*) ] + else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ] handle TERM _ => [] | Match => []; local diff -r dbf831a50e4a -r 9bec62c10714 src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Sat May 15 21:50:05 2010 +0200 @@ -391,9 +391,9 @@ fun export_thm thy hyps shyps prop = let val th = export_oracle (thy, hyps, shyps, prop) - val hyps = map (fn h => assume (cterm_of thy h)) hyps + val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps in - fold (fn h => fn p => implies_elim p h) hyps th + fold (fn h => fn p => Thm.implies_elim p h) hyps th end (* --------- Rewrite ----------- *) diff -r dbf831a50e4a -r 9bec62c10714 src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/Tools/IsaPlanner/rw_inst.ML Sat May 15 21:50:05 2010 +0200 @@ -54,13 +54,13 @@ (* beta contract the theorem *) fun beta_contract thm = - equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm; + Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm; (* beta-eta contract the theorem *) fun beta_eta_contract thm = let - val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm - val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 + val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm + val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 in thm3 end; diff -r dbf831a50e4a -r 9bec62c10714 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/Tools/coherent.ML Sat May 15 21:50:05 2010 +0200 @@ -46,8 +46,8 @@ fun rulify_elim_conv ct = if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct else concl_conv (length (Logic.strip_imp_prems (term_of ct))) - (rewr_conv (symmetric Data.atomize_elimL) then_conv - MetaSimplifier.rewrite true (map symmetric + (rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv + MetaSimplifier.rewrite true (map Thm.symmetric [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct end; diff -r dbf831a50e4a -r 9bec62c10714 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Sat May 15 21:41:32 2010 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Sat May 15 21:50:05 2010 +0200 @@ -89,7 +89,7 @@ fun exhaust_induct_tac exh ctxt var i state = let val thy = ProofContext.theory_of ctxt - val (_, _, Bi, _) = dest_state (state, i) + val (_, _, Bi, _) = Thm.dest_state (state, i) val tn = find_tname var Bi val rule = if exh then #exhaustion (datatype_info thy tn)