--- 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;
--- 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 =
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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)
--- 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. *)
--- 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
--- 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)),
--- 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
--- 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) </ Rat.zero then arg_conv cv t else reflexive t
-| _ => reflexive t
+ if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive 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
--- 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,
--- 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
--- 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);
--- 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));
--- 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))))]);
--- 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
--- 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
--- 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
--- 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<x. P y) ==> P x" *)
+ |> Thm.implies_intr ihyp
+ |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P 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
--- 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
--- 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
--- 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);
--- 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
--- 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 =
--- 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
--- 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
--- 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]))
--- 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"?) ***)
--- 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 *)
--- 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;
--- 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
--- 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 = ""
--- 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]
--- 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
--- 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
--- 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"}];
--- 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
--- 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;
--- 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;
--- 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;
--- 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
--- 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 ----------- *)
--- 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;
--- 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;
--- 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)