1.1 --- a/src/FOLP/simp.ML Sat May 15 21:41:32 2010 +0200
1.2 +++ b/src/FOLP/simp.ML Sat May 15 21:50:05 2010 +0200
1.3 @@ -431,7 +431,7 @@
1.4 are represented by rules, generalized over their parameters*)
1.5 fun add_asms(ss,thm,a,anet,ats,cs) =
1.6 let val As = strip_varify(nth_subgoal i thm, a, []);
1.7 - val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
1.8 + val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As;
1.9 val new_rws = maps mk_rew_rules thms;
1.10 val rwrls = map mk_trans (maps mk_rew_rules thms);
1.11 val anet' = fold_rev lhs_insert_thm rwrls anet;
2.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat May 15 21:41:32 2010 +0200
2.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sat May 15 21:50:05 2010 +0200
2.3 @@ -681,7 +681,7 @@
2.4 else ("Nox",[])
2.5 | t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
2.6
2.7 -fun xnormalize_conv ctxt [] ct = reflexive ct
2.8 +fun xnormalize_conv ctxt [] ct = Thm.reflexive ct
2.9 | xnormalize_conv ctxt (vs as (x::_)) ct =
2.10 case term_of ct of
2.11 Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) =>
2.12 @@ -696,8 +696,8 @@
2.13 (Thm.capply @{cterm "Trueprop"}
2.14 (if neg then Thm.capply (Thm.capply clt c) cz
2.15 else Thm.capply (Thm.capply clt cz) c))
2.16 - val cth = equal_elim (symmetric cthp) TrueI
2.17 - val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
2.18 + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
2.19 + val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
2.20 (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
2.21 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
2.22 (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
2.23 @@ -719,12 +719,12 @@
2.24 (Thm.capply @{cterm "Trueprop"}
2.25 (if neg then Thm.capply (Thm.capply clt c) cz
2.26 else Thm.capply (Thm.capply clt cz) c))
2.27 - val cth = equal_elim (symmetric cthp) TrueI
2.28 - val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
2.29 + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
2.30 + val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
2.31 (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
2.32 val rth = th
2.33 in rth end
2.34 - | _ => reflexive ct)
2.35 + | _ => Thm.reflexive ct)
2.36
2.37
2.38 | Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.zero},_) =>
2.39 @@ -740,8 +740,8 @@
2.40 (Thm.capply @{cterm "Trueprop"}
2.41 (if neg then Thm.capply (Thm.capply clt c) cz
2.42 else Thm.capply (Thm.capply clt cz) c))
2.43 - val cth = equal_elim (symmetric cthp) TrueI
2.44 - val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
2.45 + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
2.46 + val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
2.47 (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
2.48 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
2.49 (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
2.50 @@ -764,12 +764,12 @@
2.51 (Thm.capply @{cterm "Trueprop"}
2.52 (if neg then Thm.capply (Thm.capply clt c) cz
2.53 else Thm.capply (Thm.capply clt cz) c))
2.54 - val cth = equal_elim (symmetric cthp) TrueI
2.55 - val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
2.56 + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
2.57 + val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
2.58 (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
2.59 val rth = th
2.60 in rth end
2.61 - | _ => reflexive ct)
2.62 + | _ => Thm.reflexive ct)
2.63
2.64 | Const("op =",_)$_$Const(@{const_name Groups.zero},_) =>
2.65 (case whatis x (Thm.dest_arg1 ct) of
2.66 @@ -782,8 +782,8 @@
2.67 val cthp = Simplifier.rewrite (simpset_of ctxt)
2.68 (Thm.capply @{cterm "Trueprop"}
2.69 (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
2.70 - val cth = equal_elim (symmetric cthp) TrueI
2.71 - val th = implies_elim
2.72 + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
2.73 + val th = Thm.implies_elim
2.74 (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
2.75 val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
2.76 (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
2.77 @@ -804,11 +804,11 @@
2.78 val cthp = Simplifier.rewrite (simpset_of ctxt)
2.79 (Thm.capply @{cterm "Trueprop"}
2.80 (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
2.81 - val cth = equal_elim (symmetric cthp) TrueI
2.82 - val rth = implies_elim
2.83 + val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
2.84 + val rth = Thm.implies_elim
2.85 (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
2.86 in rth end
2.87 - | _ => reflexive ct);
2.88 + | _ => Thm.reflexive ct);
2.89
2.90 local
2.91 val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
2.92 @@ -823,7 +823,7 @@
2.93 val nth = Conv.fconv_rule
2.94 (Conv.arg_conv (Conv.arg1_conv
2.95 (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
2.96 - val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
2.97 + val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
2.98 in rth end
2.99 | Const(@{const_name Orderings.less_eq},_)$a$b =>
2.100 let val (ca,cb) = Thm.dest_binop ct
2.101 @@ -832,7 +832,7 @@
2.102 val nth = Conv.fconv_rule
2.103 (Conv.arg_conv (Conv.arg1_conv
2.104 (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
2.105 - val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
2.106 + val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
2.107 in rth end
2.108
2.109 | Const("op =",_)$a$b =>
2.110 @@ -842,10 +842,10 @@
2.111 val nth = Conv.fconv_rule
2.112 (Conv.arg_conv (Conv.arg1_conv
2.113 (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
2.114 - val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
2.115 + val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
2.116 in rth end
2.117 | @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
2.118 -| _ => reflexive ct
2.119 +| _ => Thm.reflexive ct
2.120 end;
2.121
2.122 fun classfield_whatis phi =
3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML Sat May 15 21:41:32 2010 +0200
3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat May 15 21:50:05 2010 +0200
3.3 @@ -106,7 +106,7 @@
3.4 [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
3.5 TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
3.6 TRY (simp_tac simpset3 1), TRY (simp_tac cooper_ss 1)]
3.7 - (trivial ct))
3.8 + (Thm.trivial ct))
3.9 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
3.10 (* The result of the quantifier elimination *)
3.11 val (th, tac) = case (prop_of pre_thm) of
4.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML Sat May 15 21:41:32 2010 +0200
4.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sat May 15 21:50:05 2010 +0200
4.3 @@ -87,7 +87,7 @@
4.4 val pre_thm = Seq.hd (EVERY
4.5 [simp_tac simpset0 1,
4.6 TRY (simp_tac (Simplifier.context ctxt ferrack_ss) 1)]
4.7 - (trivial ct))
4.8 + (Thm.trivial ct))
4.9 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
4.10 (* The result of the quantifier elimination *)
4.11 val (th, tac) = case prop_of pre_thm of
5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML Sat May 15 21:41:32 2010 +0200
5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat May 15 21:50:05 2010 +0200
5.3 @@ -128,7 +128,7 @@
5.4 val pre_thm = Seq.hd (EVERY
5.5 [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
5.6 TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), TRY (simp_tac mir_ss 1)]
5.7 - (trivial ct))
5.8 + (Thm.trivial ct))
5.9 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
5.10 (* The result of the quantifier elimination *)
5.11 val (th, tac) = case (prop_of pre_thm) of
6.1 --- a/src/HOL/HOL.thy Sat May 15 21:41:32 2010 +0200
6.2 +++ b/src/HOL/HOL.thy Sat May 15 21:50:05 2010 +0200
6.3 @@ -1282,12 +1282,12 @@
6.4 else let
6.5 val abs_g'= Abs (n,xT,g');
6.6 val g'x = abs_g'$x;
6.7 - val g_g'x = symmetric (beta_conversion false (cterm_of thy g'x));
6.8 + val g_g'x = Thm.symmetric (Thm.beta_conversion false (cterm_of thy g'x));
6.9 val rl = cterm_instantiate
6.10 [(f_Let_folded, cterm_of thy f), (x_Let_folded, cx),
6.11 (g_Let_folded, cterm_of thy abs_g')]
6.12 @{thm Let_folded};
6.13 - in SOME (rl OF [transitive fx_g g_g'x])
6.14 + in SOME (rl OF [Thm.transitive fx_g g_g'x])
6.15 end)
6.16 end
6.17 | _ => NONE)
7.1 --- a/src/HOL/Import/import.ML Sat May 15 21:41:32 2010 +0200
7.2 +++ b/src/HOL/Import/import.ML Sat May 15 21:50:05 2010 +0200
7.3 @@ -40,7 +40,7 @@
7.4 val hol4thm = snd (Replay.replay_proof int_thms thyname thmname proof thy)
7.5 val thm = snd (ProofKernel.to_isa_thm hol4thm)
7.6 val rew = ProofKernel.rewrite_hol4_term (concl_of thm) thy
7.7 - val thm = equal_elim rew thm
7.8 + val thm = Thm.equal_elim rew thm
7.9 val prew = ProofKernel.rewrite_hol4_term prem thy
7.10 val prem' = #2 (Logic.dest_equals (prop_of prew))
7.11 val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
7.12 @@ -53,7 +53,7 @@
7.13 val _ = if prem' aconv (prop_of thm)
7.14 then message "import: Terms match up"
7.15 else message "import: Terms DO NOT match up"
7.16 - val thm' = equal_elim (symmetric prew) thm
7.17 + val thm' = Thm.equal_elim (Thm.symmetric prew) thm
7.18 val res = Thm.bicompose true (false,thm',0) 1 th
7.19 in
7.20 res
8.1 --- a/src/HOL/Import/proof_kernel.ML Sat May 15 21:41:32 2010 +0200
8.2 +++ b/src/HOL/Import/proof_kernel.ML Sat May 15 21:50:05 2010 +0200
8.3 @@ -1013,12 +1013,12 @@
8.4 local
8.5 val th = thm "not_def"
8.6 val thy = theory_of_thm th
8.7 - val pp = reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
8.8 + val pp = Thm.reflexive (cterm_of thy (Const("Trueprop",boolT-->propT)))
8.9 in
8.10 -val not_elim_thm = combination pp th
8.11 +val not_elim_thm = Thm.combination pp th
8.12 end
8.13
8.14 -val not_intro_thm = symmetric not_elim_thm
8.15 +val not_intro_thm = Thm.symmetric not_elim_thm
8.16 val abs_thm = thm "ext"
8.17 val trans_thm = thm "trans"
8.18 val symmetry_thm = thm "sym"
8.19 @@ -1039,7 +1039,7 @@
8.20 end
8.21
8.22 fun implies_elim_all th =
8.23 - Library.foldl (fn (th,p) => implies_elim th (assume p)) (th,cprems_of th)
8.24 + Library.foldl (fn (th,p) => Thm.implies_elim th (Thm.assume p)) (th,cprems_of th)
8.25
8.26 fun norm_hyps th =
8.27 th |> beta_eta_thm
8.28 @@ -1054,7 +1054,7 @@
8.29 val clc = Thm.cterm_of sg lc
8.30 val cvty = ctyp_of_term cv
8.31 val th1 = implies_elim_all th
8.32 - val th2 = beta_eta_thm (forall_intr cv th1)
8.33 + val th2 = beta_eta_thm (Thm.forall_intr cv th1)
8.34 val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm))
8.35 val c = prop_of th3
8.36 val vname = fst(dest_Free v)
8.37 @@ -1072,7 +1072,7 @@
8.38 fun rearrange sg tm th =
8.39 let
8.40 val tm' = Envir.beta_eta_contract tm
8.41 - fun find [] n = Thm.permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
8.42 + fun find [] n = Thm.permute_prems 0 1 (Thm.implies_intr (Thm.cterm_of sg tm) th)
8.43 | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
8.44 then Thm.permute_prems n 1 th
8.45 else find ps (n+1)
8.46 @@ -1258,7 +1258,7 @@
8.47 fun get_isabelle_thm thyname thmname hol4conc thy =
8.48 let
8.49 val (info,hol4conc') = disamb_term hol4conc
8.50 - val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
8.51 + val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
8.52 val isaconc =
8.53 case concl_of i2h_conc of
8.54 Const("==",_) $ lhs $ _ => lhs
8.55 @@ -1268,7 +1268,7 @@
8.56 message "Modified conclusion:";
8.57 if_debug prin isaconc)
8.58
8.59 - fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th)
8.60 + fun mk_res th = HOLThm (rens_of info, Thm.equal_elim i2h_conc th)
8.61 in
8.62 case get_hol4_mapping thyname thmname thy of
8.63 SOME (SOME thmname) =>
8.64 @@ -1320,7 +1320,7 @@
8.65 fun warn () =
8.66 let
8.67 val (info,hol4conc') = disamb_term hol4conc
8.68 - val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
8.69 + val i2h_conc = Thm.symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
8.70 in
8.71 case concl_of i2h_conc of
8.72 Const("==",_) $ lhs $ _ =>
8.73 @@ -1369,7 +1369,7 @@
8.74 let
8.75 val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
8.76 val rew = rewrite_hol4_term (concl_of th) thy
8.77 - val th = equal_elim rew th
8.78 + val th = Thm.equal_elim rew th
8.79 val thy' = add_hol4_pending thyname thmname args thy
8.80 val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
8.81 val th = disambiguate_frees th
8.82 @@ -1683,7 +1683,7 @@
8.83 val (info',v') = disamb_term_from info v
8.84 fun strip 0 _ th = th
8.85 | strip n (p::ps) th =
8.86 - strip (n-1) ps (implies_elim th (assume p))
8.87 + strip (n-1) ps (Thm.implies_elim th (Thm.assume p))
8.88 | strip _ _ _ = raise ERR "CHOOSE" "strip error"
8.89 val cv = cterm_of thy v'
8.90 val th2 = norm_hyps th2
8.91 @@ -1697,7 +1697,7 @@
8.92 val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
8.93 val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
8.94 val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21
8.95 - val th23 = beta_eta_thm (forall_intr cv th22)
8.96 + val th23 = beta_eta_thm (Thm.forall_intr cv th22)
8.97 val th11 = implies_elim_all (beta_eta_thm th1)
8.98 val th' = th23 COMP (th11 COMP choose_thm')
8.99 val th = implies_intr_hyps th'
8.100 @@ -1796,7 +1796,7 @@
8.101 | _ => raise ERR "mk_ABS" "Bad conclusion"
8.102 val (fd,fr) = dom_rng (type_of f)
8.103 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
8.104 - val th2 = forall_intr cv th1
8.105 + val th2 = Thm.forall_intr cv th1
8.106 val th3 = th2 COMP abs_thm'
8.107 val res = implies_intr_hyps th3
8.108 in
8.109 @@ -1867,7 +1867,7 @@
8.110 _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
8.111 | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
8.112 val ca = cterm_of thy a
8.113 - val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
8.114 + val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
8.115 val res = HOLThm(rens,implies_intr_hyps th2)
8.116 val _ = message "RESULT:"
8.117 val _ = if_debug pth res
8.118 @@ -1884,7 +1884,7 @@
8.119 _ $ (Const("Not",_) $ a) => a
8.120 | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
8.121 val ca = cterm_of thy a
8.122 - val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
8.123 + val th2 = Thm.equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
8.124 val res = HOLThm(rens,implies_intr_hyps th2)
8.125 val _ = message "RESULT:"
8.126 val _ = if_debug pth res
8.127 @@ -1902,9 +1902,9 @@
8.128 val prems = prems_of th
8.129 val th1 = beta_eta_thm th
8.130 val th2 = implies_elim_all th1
8.131 - val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
8.132 + val th3 = Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
8.133 val th4 = th3 COMP disch_thm
8.134 - val res = HOLThm(rens_of info',implies_intr_hyps th4)
8.135 + val res = HOLThm (rens_of info', implies_intr_hyps th4)
8.136 val _ = message "RESULT:"
8.137 val _ = if_debug pth res
8.138 in
8.139 @@ -2032,7 +2032,7 @@
8.140 val res' = Thm.unvarify_global res
8.141 val hth = HOLThm(rens,res')
8.142 val rew = rewrite_hol4_term (concl_of res') thy'
8.143 - val th = equal_elim rew res'
8.144 + val th = Thm.equal_elim rew res'
8.145 fun handle_const (name,thy) =
8.146 let
8.147 val defname = Thm.def_name name
8.148 @@ -2112,7 +2112,7 @@
8.149 val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
8.150
8.151 val rew = rewrite_hol4_term (concl_of td_th) thy4
8.152 - val th = equal_elim rew (Thm.transfer thy4 td_th)
8.153 + val th = Thm.equal_elim rew (Thm.transfer thy4 td_th)
8.154 val c = case HOLogic.dest_Trueprop (prop_of th) of
8.155 Const("Ex",exT) $ P =>
8.156 let
9.1 --- a/src/HOL/Import/shuffler.ML Sat May 15 21:41:32 2010 +0200
9.2 +++ b/src/HOL/Import/shuffler.ML Sat May 15 21:50:05 2010 +0200
9.3 @@ -95,12 +95,12 @@
9.4 val cQ = cert Q
9.5 val cPQ = cert PQ
9.6 val cPPQ = cert PPQ
9.7 - val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
9.8 - val th3 = assume cP
9.9 - val th4 = implies_elim_list (assume cPPQ) [th3,th3]
9.10 + val th1 = Thm.assume cPQ |> implies_intr_list [cPQ,cP]
9.11 + val th3 = Thm.assume cP
9.12 + val th4 = implies_elim_list (Thm.assume cPPQ) [th3,th3]
9.13 |> implies_intr_list [cPPQ,cP]
9.14 in
9.15 - equal_intr th4 th1 |> Drule.export_without_context
9.16 + Thm.equal_intr th4 th1 |> Drule.export_without_context
9.17 end
9.18
9.19 val imp_comm =
9.20 @@ -115,12 +115,12 @@
9.21 val cQ = cert Q
9.22 val cPQR = cert PQR
9.23 val cQPR = cert QPR
9.24 - val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
9.25 + val th1 = implies_elim_list (Thm.assume cPQR) [Thm.assume cP,Thm.assume cQ]
9.26 |> implies_intr_list [cPQR,cQ,cP]
9.27 - val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
9.28 + val th2 = implies_elim_list (Thm.assume cQPR) [Thm.assume cQ,Thm.assume cP]
9.29 |> implies_intr_list [cQPR,cP,cQ]
9.30 in
9.31 - equal_intr th1 th2 |> Drule.export_without_context
9.32 + Thm.equal_intr th1 th2 |> Drule.export_without_context
9.33 end
9.34
9.35 val def_norm =
9.36 @@ -134,20 +134,20 @@
9.37 val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
9.38 val cPQ = cert (Logic.mk_equals(P,Q))
9.39 val cv = cert v
9.40 - val rew = assume cvPQ
9.41 - |> forall_elim cv
9.42 - |> abstract_rule "v" cv
9.43 + val rew = Thm.assume cvPQ
9.44 + |> Thm.forall_elim cv
9.45 + |> Thm.abstract_rule "v" cv
9.46 val (lhs,rhs) = Logic.dest_equals(concl_of rew)
9.47 - val th1 = transitive (transitive
9.48 - (eta_conversion (cert lhs) |> symmetric)
9.49 + val th1 = Thm.transitive (Thm.transitive
9.50 + (Thm.eta_conversion (cert lhs) |> Thm.symmetric)
9.51 rew)
9.52 - (eta_conversion (cert rhs))
9.53 - |> implies_intr cvPQ
9.54 - val th2 = combination (assume cPQ) (reflexive cv)
9.55 - |> forall_intr cv
9.56 - |> implies_intr cPQ
9.57 + (Thm.eta_conversion (cert rhs))
9.58 + |> Thm.implies_intr cvPQ
9.59 + val th2 = Thm.combination (Thm.assume cPQ) (Thm.reflexive cv)
9.60 + |> Thm.forall_intr cv
9.61 + |> Thm.implies_intr cPQ
9.62 in
9.63 - equal_intr th1 th2 |> Drule.export_without_context
9.64 + Thm.equal_intr th1 th2 |> Drule.export_without_context
9.65 end
9.66
9.67 val all_comm =
9.68 @@ -164,16 +164,16 @@
9.69 val cr = cert rhs
9.70 val cx = cert x
9.71 val cy = cert y
9.72 - val th1 = assume cr
9.73 + val th1 = Thm.assume cr
9.74 |> forall_elim_list [cy,cx]
9.75 |> forall_intr_list [cx,cy]
9.76 - |> implies_intr cr
9.77 - val th2 = assume cl
9.78 + |> Thm.implies_intr cr
9.79 + val th2 = Thm.assume cl
9.80 |> forall_elim_list [cx,cy]
9.81 |> forall_intr_list [cy,cx]
9.82 - |> implies_intr cl
9.83 + |> Thm.implies_intr cl
9.84 in
9.85 - equal_intr th1 th2 |> Drule.export_without_context
9.86 + Thm.equal_intr th1 th2 |> Drule.export_without_context
9.87 end
9.88
9.89 val equiv_comm =
9.90 @@ -184,10 +184,10 @@
9.91 val u = Free("u",T)
9.92 val ctu = cert (Logic.mk_equals(t,u))
9.93 val cut = cert (Logic.mk_equals(u,t))
9.94 - val th1 = assume ctu |> symmetric |> implies_intr ctu
9.95 - val th2 = assume cut |> symmetric |> implies_intr cut
9.96 + val th1 = Thm.assume ctu |> Thm.symmetric |> Thm.implies_intr ctu
9.97 + val th2 = Thm.assume cut |> Thm.symmetric |> Thm.implies_intr cut
9.98 in
9.99 - equal_intr th1 th2 |> Drule.export_without_context
9.100 + Thm.equal_intr th1 th2 |> Drule.export_without_context
9.101 end
9.102
9.103 (* This simplification procedure rewrites !!x y. P x y
9.104 @@ -217,7 +217,7 @@
9.105 val lhs = list_all ([xv,yv],t)
9.106 val rhs = list_all ([yv,xv],swap_bound 0 t)
9.107 val rew = Logic.mk_equals (lhs,rhs)
9.108 - val init = trivial (cterm_of thy rew)
9.109 + val init = Thm.trivial (cterm_of thy rew)
9.110 in
9.111 (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
9.112 end
9.113 @@ -232,10 +232,10 @@
9.114 then
9.115 let
9.116 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
9.117 - val t_th = reflexive (cterm_of thy t)
9.118 - val newt_th = reflexive (cterm_of thy newt)
9.119 + val t_th = Thm.reflexive (cterm_of thy t)
9.120 + val newt_th = Thm.reflexive (cterm_of thy newt)
9.121 in
9.122 - SOME (transitive t_th newt_th)
9.123 + SOME (Thm.transitive t_th newt_th)
9.124 end
9.125 else NONE
9.126 | _ => error "norm_term (quant_rewrite) internal error"
9.127 @@ -294,7 +294,7 @@
9.128 fun eta_contract thy assumes origt =
9.129 let
9.130 val (typet,Tinst) = freeze_thaw_term origt
9.131 - val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
9.132 + val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
9.133 val final = inst_tfrees thy Tinst o thaw
9.134 val t = #1 (Logic.dest_equals (prop_of init))
9.135 val _ =
9.136 @@ -322,18 +322,18 @@
9.137 val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
9.138 val cv = cert v
9.139 val ct = cert t
9.140 - val th = (assume ct)
9.141 - |> forall_elim cv
9.142 - |> abstract_rule x cv
9.143 - val ext_th = eta_conversion (cert (Abs(x,xT,P)))
9.144 - val th' = transitive (symmetric ext_th) th
9.145 + val th = (Thm.assume ct)
9.146 + |> Thm.forall_elim cv
9.147 + |> Thm.abstract_rule x cv
9.148 + val ext_th = Thm.eta_conversion (cert (Abs(x,xT,P)))
9.149 + val th' = Thm.transitive (Thm.symmetric ext_th) th
9.150 val cu = cert (prop_of th')
9.151 - val uth = combination (assume cu) (reflexive cv)
9.152 - val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
9.153 - |> transitive uth
9.154 - |> forall_intr cv
9.155 - |> implies_intr cu
9.156 - val rew_th = equal_intr (th' |> implies_intr ct) uth'
9.157 + val uth = Thm.combination (Thm.assume cu) (Thm.reflexive cv)
9.158 + val uth' = (Thm.beta_conversion false (cert (Abs(x,xT,Q) $ v)))
9.159 + |> Thm.transitive uth
9.160 + |> Thm.forall_intr cv
9.161 + |> Thm.implies_intr cu
9.162 + val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth'
9.163 val res = final rew_th
9.164 val lhs = (#1 (Logic.dest_equals (prop_of res)))
9.165 in
9.166 @@ -345,7 +345,7 @@
9.167 end
9.168
9.169 fun beta_fun thy assume t =
9.170 - SOME (beta_conversion true (cterm_of thy t))
9.171 + SOME (Thm.beta_conversion true (cterm_of thy t))
9.172
9.173 val meta_sym_rew = thm "refl"
9.174
9.175 @@ -357,7 +357,7 @@
9.176 fun eta_expand thy assumes origt =
9.177 let
9.178 val (typet,Tinst) = freeze_thaw_term origt
9.179 - val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
9.180 + val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
9.181 val final = inst_tfrees thy Tinst o thaw
9.182 val t = #1 (Logic.dest_equals (prop_of init))
9.183 val _ =
9.184 @@ -387,20 +387,20 @@
9.185 val v = Free(vname,aT)
9.186 val cv = cert v
9.187 val ct = cert t
9.188 - val th1 = (combination (assume ct) (reflexive cv))
9.189 - |> forall_intr cv
9.190 - |> implies_intr ct
9.191 + val th1 = (Thm.combination (Thm.assume ct) (Thm.reflexive cv))
9.192 + |> Thm.forall_intr cv
9.193 + |> Thm.implies_intr ct
9.194 val concl = cert (concl_of th1)
9.195 - val th2 = (assume concl)
9.196 - |> forall_elim cv
9.197 - |> abstract_rule vname cv
9.198 + val th2 = (Thm.assume concl)
9.199 + |> Thm.forall_elim cv
9.200 + |> Thm.abstract_rule vname cv
9.201 val (lhs,rhs) = Logic.dest_equals (prop_of th2)
9.202 - val elhs = eta_conversion (cert lhs)
9.203 - val erhs = eta_conversion (cert rhs)
9.204 - val th2' = transitive
9.205 - (transitive (symmetric elhs) th2)
9.206 + val elhs = Thm.eta_conversion (cert lhs)
9.207 + val erhs = Thm.eta_conversion (cert rhs)
9.208 + val th2' = Thm.transitive
9.209 + (Thm.transitive (Thm.symmetric elhs) th2)
9.210 erhs
9.211 - val res = equal_intr th1 (th2' |> implies_intr concl)
9.212 + val res = Thm.equal_intr th1 (th2' |> Thm.implies_intr concl)
9.213 val res' = final res
9.214 in
9.215 SOME res'
9.216 @@ -475,7 +475,7 @@
9.217 val (t',_) = F (t,0)
9.218 val ct = cterm_of thy t
9.219 val ct' = cterm_of thy t'
9.220 - val res = transitive (reflexive ct) (reflexive ct')
9.221 + val res = Thm.transitive (Thm.reflexive ct) (Thm.reflexive ct')
9.222 val _ = message ("disamb_term: " ^ (string_of_thm res))
9.223 in
9.224 res
9.225 @@ -496,12 +496,12 @@
9.226 let
9.227 val rhs = Thm.rhs_of th
9.228 in
9.229 - transitive th (f rhs)
9.230 + Thm.transitive th (f rhs)
9.231 end
9.232 val th =
9.233 t |> disamb_bound thy
9.234 |> chain (Simplifier.full_rewrite ss)
9.235 - |> chain eta_conversion
9.236 + |> chain Thm.eta_conversion
9.237 |> Thm.strip_shyps
9.238 val _ = message ("norm_term: " ^ (string_of_thm th))
9.239 in
9.240 @@ -529,7 +529,7 @@
9.241 let
9.242 val c = prop_of th
9.243 in
9.244 - equal_elim (norm_term thy c) th
9.245 + Thm.equal_elim (norm_term thy c) th
9.246 end
9.247
9.248 (* make_equal thy t u tries to construct the theorem t == u under the
9.249 @@ -540,7 +540,7 @@
9.250 let
9.251 val t_is_t' = norm_term thy t
9.252 val u_is_u' = norm_term thy u
9.253 - val th = transitive t_is_t' (symmetric u_is_u')
9.254 + val th = Thm.transitive t_is_t' (Thm.symmetric u_is_u')
9.255 val _ = message ("make_equal: SOME " ^ (string_of_thm th))
9.256 in
9.257 SOME th
9.258 @@ -593,7 +593,7 @@
9.259 | process ((name,th)::thms) =
9.260 let
9.261 val norm_th = Thm.varifyT_global (norm_thm thy (close_thm (Thm.transfer thy th)))
9.262 - val triv_th = trivial rhs
9.263 + val triv_th = Thm.trivial rhs
9.264 val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
9.265 val mod_th = case Seq.pull (Thm.bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
9.266 SOME(th,_) => SOME th
9.267 @@ -602,7 +602,7 @@
9.268 case mod_th of
9.269 SOME mod_th =>
9.270 let
9.271 - val closed_th = equal_elim (symmetric rew_th) mod_th
9.272 + val closed_th = Thm.equal_elim (Thm.symmetric rew_th) mod_th
9.273 in
9.274 message ("Shuffler.set_prop succeeded by " ^ name);
9.275 SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
10.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat May 15 21:41:32 2010 +0200
10.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat May 15 21:50:05 2010 +0200
10.3 @@ -1272,7 +1272,7 @@
10.4 fun subst_conv eqs t =
10.5 let
10.6 val t' = fold (Thm.cabs o Thm.lhs_of) eqs t
10.7 - in Conv.fconv_rule (Thm.beta_conversion true) (fold (C combination) eqs (reflexive t'))
10.8 + in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t'))
10.9 end
10.10
10.11 (* A wrapper that tries to substitute away variables first. *)
11.1 --- a/src/HOL/Library/positivstellensatz.ML Sat May 15 21:41:32 2010 +0200
11.2 +++ b/src/HOL/Library/positivstellensatz.ML Sat May 15 21:50:05 2010 +0200
11.3 @@ -182,12 +182,12 @@
11.4
11.5 (* Some useful derived rules *)
11.6 fun deduct_antisym_rule tha thb =
11.7 - equal_intr (implies_intr (cprop_of thb) tha)
11.8 - (implies_intr (cprop_of tha) thb);
11.9 + Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha)
11.10 + (Thm.implies_intr (cprop_of tha) thb);
11.11
11.12 fun prove_hyp tha thb =
11.13 if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb))
11.14 - then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
11.15 + then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
11.16
11.17 val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
11.18 "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and
11.19 @@ -375,7 +375,7 @@
11.20 val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss)
11.21 val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps
11.22 val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss)
11.23 - fun eqT_elim th = equal_elim (symmetric th) @{thm TrueI}
11.24 + fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
11.25 fun oprconv cv ct =
11.26 let val g = Thm.dest_fun2 ct
11.27 in if g aconvc @{cterm "op <= :: real => _"}
11.28 @@ -387,7 +387,7 @@
11.29 let
11.30 val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th
11.31 handle MATCH => raise CTERM ("real_ineq_conv", [ct]))
11.32 - in transitive th' (oprconv poly_conv (Thm.rhs_of th'))
11.33 + in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th'))
11.34 end
11.35 val [real_lt_conv, real_le_conv, real_eq_conv,
11.36 real_not_lt_conv, real_not_le_conv, _] =
11.37 @@ -446,10 +446,10 @@
11.38 let val (p,q) = Thm.dest_binop (concl th)
11.39 val c = concl th1
11.40 val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
11.41 - in implies_elim (implies_elim
11.42 - (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
11.43 - (implies_intr (Thm.capply @{cterm Trueprop} p) th1))
11.44 - (implies_intr (Thm.capply @{cterm Trueprop} q) th2)
11.45 + in Thm.implies_elim (Thm.implies_elim
11.46 + (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
11.47 + (Thm.implies_intr (Thm.capply @{cterm Trueprop} p) th1))
11.48 + (Thm.implies_intr (Thm.capply @{cterm Trueprop} q) th2)
11.49 end
11.50 fun overall cert_choice dun ths = case ths of
11.51 [] =>
11.52 @@ -468,8 +468,8 @@
11.53 overall cert_choice dun (th1::th2::oths) end
11.54 else if is_disj ct then
11.55 let
11.56 - val (th1, cert1) = overall (Left::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
11.57 - val (th2, cert2) = overall (Right::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
11.58 + val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
11.59 + val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
11.60 in (disj_cases th th1 th2, Branch (cert1, cert2)) end
11.61 else overall cert_choice (th::dun) oths
11.62 end
11.63 @@ -487,12 +487,12 @@
11.64 val th' = Drule.binop_cong_rule @{cterm "op |"}
11.65 (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
11.66 (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
11.67 - in transitive th th'
11.68 + in Thm.transitive th th'
11.69 end
11.70 fun equal_implies_1_rule PQ =
11.71 let
11.72 val P = Thm.lhs_of PQ
11.73 - in implies_intr P (equal_elim PQ (assume P))
11.74 + in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
11.75 end
11.76 (* FIXME!!! Copied from groebner.ml *)
11.77 val strip_exists =
11.78 @@ -507,7 +507,7 @@
11.79 | Var ((s,_),_) => s
11.80 | _ => "x"
11.81
11.82 - 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)
11.83 + 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)
11.84
11.85 val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
11.86
11.87 @@ -523,12 +523,12 @@
11.88 (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
11.89 val pv = (Thm.rhs_of o Thm.beta_conversion true)
11.90 (Thm.capply @{cterm Trueprop} (Thm.capply p v))
11.91 - val th1 = forall_intr v (implies_intr pv th')
11.92 - in implies_elim (implies_elim th0 th) th1 end
11.93 + val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
11.94 + in Thm.implies_elim (Thm.implies_elim th0 th) th1 end
11.95 | _ => raise THM ("choose",0,[th, th'])
11.96
11.97 fun simple_choose v th =
11.98 - choose v (assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
11.99 + 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
11.100
11.101 val strip_forall =
11.102 let fun h (acc, t) =
11.103 @@ -558,11 +558,11 @@
11.104 val (evs,bod) = strip_exists tm0
11.105 val (avs,ibod) = strip_forall bod
11.106 val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
11.107 - val (th2, certs) = overall [] [] [specl avs (assume (Thm.rhs_of th1))]
11.108 - val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (Thm.capply @{cterm Trueprop} bod))) th2)
11.109 - in (Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3), certs)
11.110 + val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
11.111 + val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.capply @{cterm Trueprop} bod))) th2)
11.112 + in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
11.113 end
11.114 - in (implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
11.115 + in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
11.116 end
11.117 in f
11.118 end;
11.119 @@ -715,10 +715,10 @@
11.120 fun eliminate_construct p c tm =
11.121 let
11.122 val t = find_cterm p tm
11.123 - val th0 = (symmetric o beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
11.124 + val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
11.125 val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
11.126 - in fconv_rule(arg_conv(binop_conv (arg_conv (beta_conversion false))))
11.127 - (transitive th0 (c p ax))
11.128 + in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
11.129 + (Thm.transitive th0 (c p ax))
11.130 end
11.131
11.132 val elim_abs = eliminate_construct is_abs
12.1 --- a/src/HOL/Library/reflection.ML Sat May 15 21:41:32 2010 +0200
12.2 +++ b/src/HOL/Library/reflection.ML Sat May 15 21:50:05 2010 +0200
12.3 @@ -133,7 +133,7 @@
12.4 (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds))
12.5 in (([(ta, ctxt')],
12.6 fn ([th], bds) =>
12.7 - (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]),
12.8 + (hd (Variable.export ctxt' ctxt [(Thm.forall_intr (cert x) th) COMP allI]),
12.9 let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT))
12.10 in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds
12.11 end)),
13.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML Sat May 15 21:41:32 2010 +0200
13.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML Sat May 15 21:50:05 2010 +0200
13.3 @@ -81,8 +81,8 @@
13.4 fun matrix_simplify th =
13.5 let
13.6 val simp_th = matrix_compute (cprop_of th)
13.7 - val th = Thm.strip_shyps (equal_elim simp_th th)
13.8 - fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
13.9 + val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
13.10 + fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
13.11 in
13.12 removeTrue th
13.13 end
14.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML Sat May 15 21:41:32 2010 +0200
14.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat May 15 21:50:05 2010 +0200
14.3 @@ -80,8 +80,8 @@
14.4 fun replacenegnorms cv t = case term_of t of
14.5 @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
14.6 | @{term "op * :: real => _"}$_$_ =>
14.7 - if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t
14.8 -| _ => reflexive t
14.9 + if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t
14.10 +| _ => Thm.reflexive t
14.11 fun flip v eq =
14.12 if FuncUtil.Ctermfunc.defined eq v
14.13 then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
14.14 @@ -211,7 +211,7 @@
14.15 ((apply_ptha then_conv vector_add_conv) else_conv
14.16 arg_conv vector_add_conv then_conv apply_pthd)) ct)
14.17 end
14.18 - | _ => reflexive ct))
14.19 + | _ => Thm.reflexive ct))
14.20
14.21 fun vector_canon_conv ct = case term_of ct of
14.22 Const(@{const_name plus},_)$_$_ =>
14.23 @@ -237,7 +237,7 @@
14.24 | Const(@{const_name vec},_)$n =>
14.25 let val n = Thm.dest_arg ct
14.26 in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
14.27 - then reflexive ct else apply_pth1 ct
14.28 + then Thm.reflexive ct else apply_pth1 ct
14.29 end
14.30 *)
14.31 | _ => apply_pth1 ct
14.32 @@ -342,7 +342,7 @@
14.33 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
14.34 fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
14.35 fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
14.36 - 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
14.37 + 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
14.38 val replace_conv = try_conv (rewrs_conv asl)
14.39 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
14.40 val ges' =
14.41 @@ -352,10 +352,10 @@
14.42 val nubs = map (conjunct2 o norm_mp) asl
14.43 val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
14.44 val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
14.45 - val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1])
14.46 + val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
14.47 val cps = map (swap o Thm.dest_equals) (cprems_of th11)
14.48 val th12 = instantiate ([], cps) th11
14.49 - val th13 = fold Thm.elim_implies (map (reflexive o snd) cps) th12;
14.50 + val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
14.51 in hd (Variable.export ctxt' ctxt [th13])
14.52 end
14.53 in val real_vector_ineq_prover = real_vector_ineq_prover
14.54 @@ -390,7 +390,7 @@
14.55 let
14.56 val ctxt' = Variable.declare_term (term_of ct) ctxt
14.57 val th = init_conv ctxt' ct
14.58 - in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th))
14.59 + in Thm.equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (Thm.symmetric th))
14.60 (pure ctxt' (Thm.rhs_of th))
14.61 end
14.62
15.1 --- a/src/HOL/Nominal/nominal_datatype.ML Sat May 15 21:41:32 2010 +0200
15.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat May 15 21:50:05 2010 +0200
15.3 @@ -602,7 +602,7 @@
15.4 (fn _ => EVERY
15.5 [indtac rep_induct [] 1,
15.6 ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
15.7 - (symmetric perm_fun_def :: abs_perm))),
15.8 + (Thm.symmetric perm_fun_def :: abs_perm))),
15.9 ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
15.10 length new_type_names));
15.11
15.12 @@ -927,7 +927,7 @@
15.13 simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
15.14 constr_defs @ perm_closed_thms)) 1,
15.15 TRY (simp_tac (HOL_basic_ss addsimps
15.16 - (symmetric perm_fun_def :: abs_perm)) 1),
15.17 + (Thm.symmetric perm_fun_def :: abs_perm)) 1),
15.18 TRY (simp_tac (HOL_basic_ss addsimps
15.19 (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
15.20 perm_closed_thms)) 1)])
15.21 @@ -1077,7 +1077,7 @@
15.22 (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
15.23 EVERY (map (fn (prem, r) => (EVERY
15.24 [REPEAT (eresolve_tac Abs_inverse_thms' 1),
15.25 - simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
15.26 + simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1,
15.27 DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
15.28 (prems ~~ constr_defs))]);
15.29
15.30 @@ -1641,7 +1641,7 @@
15.31 fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
15.32 supports_fresh) 1,
15.33 simp_tac (HOL_basic_ss addsimps
15.34 - [supports_def, symmetric fresh_def, fresh_prod]) 1,
15.35 + [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1,
15.36 REPEAT_DETERM (resolve_tac [allI, impI] 1),
15.37 REPEAT_DETERM (etac conjE 1),
15.38 rtac unique 1,
15.39 @@ -1655,7 +1655,7 @@
15.40 rtac rec_prem 1,
15.41 simp_tac (HOL_ss addsimps (fs_name ::
15.42 supp_prod :: finite_Un :: finite_prems)) 1,
15.43 - simp_tac (HOL_ss addsimps (symmetric fresh_def ::
15.44 + simp_tac (HOL_ss addsimps (Thm.symmetric fresh_def ::
15.45 fresh_prod :: fresh_prems)) 1]
15.46 end))
15.47 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
15.48 @@ -1746,7 +1746,7 @@
15.49 asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1])
15.50 (finite_thss ~~ finite_ctxt_ths) @
15.51 maps (fn ((_, idxss), elim) => maps (fn idxs =>
15.52 - [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1,
15.53 + [full_simp_tac (HOL_ss addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
15.54 REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
15.55 rtac ex1I 1,
15.56 (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
16.1 --- a/src/HOL/Nominal/nominal_permeq.ML Sat May 15 21:41:32 2010 +0200
16.2 +++ b/src/HOL/Nominal/nominal_permeq.ML Sat May 15 21:50:05 2010 +0200
16.3 @@ -266,7 +266,7 @@
16.4 (* intros, then applies eqvt_simp_tac *)
16.5 fun supports_tac_i tactical ss i =
16.6 let
16.7 - val simps = [supports_def,symmetric fresh_def,fresh_prod]
16.8 + val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod]
16.9 in
16.10 EVERY [tactical ("unfolding of supports ", simp_tac (HOL_basic_ss addsimps simps) i),
16.11 tactical ("stripping of foralls ", REPEAT_DETERM (rtac allI i)),
16.12 @@ -329,7 +329,7 @@
16.13 val goal = List.nth(cprems_of st, i-1)
16.14 val fin_supp = dynamic_thms st ("fin_supp")
16.15 val fresh_atm = dynamic_thms st ("fresh_atm")
16.16 - val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
16.17 + val ss1 = ss addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
16.18 val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
16.19 in
16.20 case Logic.strip_assums_concl (term_of goal) of
17.1 --- a/src/HOL/Prolog/prolog.ML Sat May 15 21:41:32 2010 +0200
17.2 +++ b/src/HOL/Prolog/prolog.ML Sat May 15 21:50:05 2010 +0200
17.3 @@ -82,7 +82,7 @@
17.4 val (prems, Const("Trueprop", _)$concl) = rep_goal
17.5 (#3(dest_state (st,i)));
17.6 *)
17.7 - val subgoal = #3(dest_state (st,i));
17.8 + val subgoal = #3(Thm.dest_state (st,i));
17.9 val prems = Logic.strip_assums_hyp subgoal;
17.10 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
17.11 fun drot_tac k i = DETERM (rotate_tac k i);
18.1 --- a/src/HOL/Statespace/state_fun.ML Sat May 15 21:41:32 2010 +0200
18.2 +++ b/src/HOL/Statespace/state_fun.ML Sat May 15 21:50:05 2010 +0200
18.3 @@ -245,7 +245,7 @@
18.4 (fn _ => rtac meta_ext 1 THEN
18.5 simp_tac ss1 1);
18.6 val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
18.7 - in SOME (transitive eq1 eq2) end
18.8 + in SOME (Thm.transitive eq1 eq2) end
18.9 | _ => NONE)
18.10 end
18.11 | _ => NONE));
19.1 --- a/src/HOL/Tools/Datatype/datatype.ML Sat May 15 21:41:32 2010 +0200
19.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Sat May 15 21:50:05 2010 +0200
19.3 @@ -483,8 +483,8 @@
19.4 [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
19.5 REPEAT (rtac TrueI 1),
19.6 rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
19.7 - symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
19.8 - rewrite_goals_tac (map symmetric range_eqs),
19.9 + Thm.symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
19.10 + rewrite_goals_tac (map Thm.symmetric range_eqs),
19.11 REPEAT (EVERY
19.12 [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
19.13 maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
19.14 @@ -621,7 +621,7 @@
19.15 (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
19.16 EVERY (map (fn (prem, r) => (EVERY
19.17 [REPEAT (eresolve_tac Abs_inverse_thms 1),
19.18 - simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
19.19 + simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
19.20 DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
19.21 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
19.22
20.1 --- a/src/HOL/Tools/Function/context_tree.ML Sat May 15 21:41:32 2010 +0200
20.2 +++ b/src/HOL/Tools/Function/context_tree.ML Sat May 15 21:50:05 2010 +0200
20.3 @@ -148,7 +148,7 @@
20.4 val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t
20.5 fun subtree (ctx', fixes, assumes, st) =
20.6 ((fixes,
20.7 - map (assume o cterm_of (ProofContext.theory_of ctx)) assumes),
20.8 + map (Thm.assume o cterm_of (ProofContext.theory_of ctx)) assumes),
20.9 mk_tree' ctx' st)
20.10 in
20.11 Cong (r, dep, map subtree branches)
20.12 @@ -165,7 +165,7 @@
20.13 fun inst_term t =
20.14 subst_bound(f, abstract_over (fvar, t))
20.15
20.16 - val inst_thm = forall_elim cf o forall_intr cfvar
20.17 + val inst_thm = Thm.forall_elim cf o Thm.forall_intr cfvar
20.18
20.19 fun inst_tree_aux (Leaf t) = Leaf t
20.20 | inst_tree_aux (Cong (crule, deps, branches)) =
20.21 @@ -173,7 +173,7 @@
20.22 | inst_tree_aux (RCall (t, str)) =
20.23 RCall (inst_term t, inst_tree_aux str)
20.24 and inst_branch ((fxs, assms), str) =
20.25 - ((fxs, map (assume o cterm_of thy o inst_term o prop_of) assms),
20.26 + ((fxs, map (Thm.assume o cterm_of thy o inst_term o prop_of) assms),
20.27 inst_tree_aux str)
20.28 in
20.29 inst_tree_aux tr
20.30 @@ -188,11 +188,11 @@
20.31 #> fold_rev (Logic.all o Free) fixes
20.32
20.33 fun export_thm thy (fixes, assumes) =
20.34 - fold_rev (implies_intr o cprop_of) assumes
20.35 - #> fold_rev (forall_intr o cterm_of thy o Free) fixes
20.36 + fold_rev (Thm.implies_intr o cprop_of) assumes
20.37 + #> fold_rev (Thm.forall_intr o cterm_of thy o Free) fixes
20.38
20.39 fun import_thm thy (fixes, athms) =
20.40 - fold (forall_elim o cterm_of thy o Free) fixes
20.41 + fold (Thm.forall_elim o cterm_of thy o Free) fixes
20.42 #> fold Thm.elim_implies athms
20.43
20.44
20.45 @@ -241,7 +241,7 @@
20.46
20.47 fun rewrite_by_tree thy h ih x tr =
20.48 let
20.49 - fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x)
20.50 + fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (cterm_of thy t), x)
20.51 | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
20.52 let
20.53 val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
20.54 @@ -250,11 +250,11 @@
20.55 |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
20.56 (* (a, h a) : G *)
20.57 val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
20.58 - val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *)
20.59 + val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
20.60
20.61 - val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner
20.62 + val h_a'_eq_h_a = Thm.combination (Thm.reflexive (cterm_of thy h)) inner
20.63 val h_a_eq_f_a = eq RS eq_reflection
20.64 - val result = transitive h_a'_eq_h_a h_a_eq_f_a
20.65 + val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
20.66 in
20.67 (result, x')
20.68 end
21.1 --- a/src/HOL/Tools/Function/function_core.ML Sat May 15 21:41:32 2010 +0200
21.2 +++ b/src/HOL/Tools/Function/function_core.ML Sat May 15 21:50:05 2010 +0200
21.3 @@ -154,9 +154,9 @@
21.4 val rhs = inst pre_rhs
21.5
21.6 val cqs = map (cterm_of thy) qs
21.7 - val ags = map (assume o cterm_of thy) gs
21.8 + val ags = map (Thm.assume o cterm_of thy) gs
21.9
21.10 - val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
21.11 + val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
21.12 in
21.13 ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
21.14 cqs = cqs, ags = ags, case_hyp = case_hyp }
21.15 @@ -188,15 +188,15 @@
21.16
21.17 (* Instantiate the GIntro thm with "f" and import into the clause context. *)
21.18 val lGI = GIntro_thm
21.19 - |> forall_elim (cert f)
21.20 - |> fold forall_elim cqs
21.21 + |> Thm.forall_elim (cert f)
21.22 + |> fold Thm.forall_elim cqs
21.23 |> fold Thm.elim_implies ags
21.24
21.25 fun mk_call_info (rcfix, rcassm, rcarg) RI =
21.26 let
21.27 val llRI = RI
21.28 - |> fold forall_elim cqs
21.29 - |> fold (forall_elim o cert o Free) rcfix
21.30 + |> fold Thm.forall_elim cqs
21.31 + |> fold (Thm.forall_elim o cert o Free) rcfix
21.32 |> fold Thm.elim_implies ags
21.33 |> fold Thm.elim_implies rcassm
21.34
21.35 @@ -242,20 +242,20 @@
21.36 val compat = lookup_compat_thm j i cts
21.37 in
21.38 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
21.39 - |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
21.40 + |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
21.41 |> fold Thm.elim_implies agsj
21.42 |> fold Thm.elim_implies agsi
21.43 - |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
21.44 + |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
21.45 end
21.46 else
21.47 let
21.48 val compat = lookup_compat_thm i j cts
21.49 in
21.50 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
21.51 - |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
21.52 + |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
21.53 |> fold Thm.elim_implies agsi
21.54 |> fold Thm.elim_implies agsj
21.55 - |> Thm.elim_implies (assume lhsi_eq_lhsj)
21.56 + |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)
21.57 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
21.58 end
21.59 end
21.60 @@ -274,16 +274,16 @@
21.61
21.62 val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
21.63 val h_assums = map (fn RCInfo {h_assum, ...} =>
21.64 - assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
21.65 + Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
21.66
21.67 val (eql, _) =
21.68 Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
21.69
21.70 val replace_lemma = (eql RS meta_eq_to_obj_eq)
21.71 - |> implies_intr (cprop_of case_hyp)
21.72 - |> fold_rev (implies_intr o cprop_of) h_assums
21.73 - |> fold_rev (implies_intr o cprop_of) ags
21.74 - |> fold_rev forall_intr cqs
21.75 + |> Thm.implies_intr (cprop_of case_hyp)
21.76 + |> fold_rev (Thm.implies_intr o cprop_of) h_assums
21.77 + |> fold_rev (Thm.implies_intr o cprop_of) ags
21.78 + |> fold_rev Thm.forall_intr cqs
21.79 |> Thm.close_derivation
21.80 in
21.81 replace_lemma
21.82 @@ -301,30 +301,30 @@
21.83
21.84 val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
21.85 val compat = get_compat_thm thy compat_store i j cctxi cctxj
21.86 - val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
21.87 + val Ghsj' = map (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
21.88
21.89 val RLj_import = RLj
21.90 - |> fold forall_elim cqsj'
21.91 + |> fold Thm.forall_elim cqsj'
21.92 |> fold Thm.elim_implies agsj'
21.93 |> fold Thm.elim_implies Ghsj'
21.94
21.95 - val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
21.96 - val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
21.97 + val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
21.98 + val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))
21.99 (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
21.100 in
21.101 (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
21.102 - |> implies_elim RLj_import
21.103 + |> Thm.implies_elim RLj_import
21.104 (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
21.105 |> (fn it => trans OF [it, compat])
21.106 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
21.107 |> (fn it => trans OF [y_eq_rhsj'h, it])
21.108 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
21.109 - |> fold_rev (implies_intr o cprop_of) Ghsj'
21.110 - |> fold_rev (implies_intr o cprop_of) agsj'
21.111 + |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'
21.112 + |> fold_rev (Thm.implies_intr o cprop_of) agsj'
21.113 (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
21.114 - |> implies_intr (cprop_of y_eq_rhsj'h)
21.115 - |> implies_intr (cprop_of lhsi_eq_lhsj')
21.116 - |> fold_rev forall_intr (cterm_of thy h :: cqsj')
21.117 + |> Thm.implies_intr (cprop_of y_eq_rhsj'h)
21.118 + |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')
21.119 + |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')
21.120 end
21.121
21.122
21.123 @@ -338,13 +338,13 @@
21.124 val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
21.125
21.126 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
21.127 - |> fold_rev (implies_intr o cprop_of) CCas
21.128 - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
21.129 + |> fold_rev (Thm.implies_intr o cprop_of) CCas
21.130 + |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
21.131
21.132 val existence = fold (curry op COMP o prep_RC) RCs lGI
21.133
21.134 val P = cterm_of thy (mk_eq (y, rhsC))
21.135 - val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
21.136 + val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
21.137
21.138 val unique_clauses =
21.139 map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
21.140 @@ -353,13 +353,13 @@
21.141 Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
21.142
21.143 val uniqueness = G_cases
21.144 - |> forall_elim (cterm_of thy lhs)
21.145 - |> forall_elim (cterm_of thy y)
21.146 - |> forall_elim P
21.147 + |> Thm.forall_elim (cterm_of thy lhs)
21.148 + |> Thm.forall_elim (cterm_of thy y)
21.149 + |> Thm.forall_elim P
21.150 |> Thm.elim_implies G_lhs_y
21.151 |> fold elim_implies_eta unique_clauses
21.152 - |> implies_intr (cprop_of G_lhs_y)
21.153 - |> forall_intr (cterm_of thy y)
21.154 + |> Thm.implies_intr (cprop_of G_lhs_y)
21.155 + |> Thm.forall_intr (cterm_of thy y)
21.156
21.157 val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
21.158
21.159 @@ -368,16 +368,16 @@
21.160 |> curry (op COMP) existence
21.161 |> curry (op COMP) uniqueness
21.162 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
21.163 - |> implies_intr (cprop_of case_hyp)
21.164 - |> fold_rev (implies_intr o cprop_of) ags
21.165 - |> fold_rev forall_intr cqs
21.166 + |> Thm.implies_intr (cprop_of case_hyp)
21.167 + |> fold_rev (Thm.implies_intr o cprop_of) ags
21.168 + |> fold_rev Thm.forall_intr cqs
21.169
21.170 val function_value =
21.171 existence
21.172 - |> implies_intr ihyp
21.173 - |> implies_intr (cprop_of case_hyp)
21.174 - |> forall_intr (cterm_of thy x)
21.175 - |> forall_elim (cterm_of thy lhs)
21.176 + |> Thm.implies_intr ihyp
21.177 + |> Thm.implies_intr (cprop_of case_hyp)
21.178 + |> Thm.forall_intr (cterm_of thy x)
21.179 + |> Thm.forall_elim (cterm_of thy lhs)
21.180 |> curry (op RS) refl
21.181 in
21.182 (exactly_one, function_value)
21.183 @@ -396,7 +396,7 @@
21.184 Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
21.185 |> cterm_of thy
21.186
21.187 - val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
21.188 + val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
21.189 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
21.190 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
21.191 |> instantiate' [] [NONE, SOME (cterm_of thy h)]
21.192 @@ -412,17 +412,17 @@
21.193 val graph_is_function = complete
21.194 |> Thm.forall_elim_vars 0
21.195 |> fold (curry op COMP) ex1s
21.196 - |> implies_intr (ihyp)
21.197 - |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
21.198 - |> forall_intr (cterm_of thy x)
21.199 + |> Thm.implies_intr (ihyp)
21.200 + |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
21.201 + |> Thm.forall_intr (cterm_of thy x)
21.202 |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
21.203 - |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
21.204 + |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
21.205
21.206 val goalstate = Conjunction.intr graph_is_function complete
21.207 |> Thm.close_derivation
21.208 |> Goal.protect
21.209 - |> fold_rev (implies_intr o cprop_of) compat
21.210 - |> implies_intr (cprop_of complete)
21.211 + |> fold_rev (Thm.implies_intr o cprop_of) compat
21.212 + |> Thm.implies_intr (cprop_of complete)
21.213 in
21.214 (goalstate, values)
21.215 end
21.216 @@ -544,7 +544,7 @@
21.217 let
21.218 fun inst_term t = subst_bound(f, abstract_over (fvar, t))
21.219 in
21.220 - (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
21.221 + (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
21.222 end
21.223
21.224
21.225 @@ -562,14 +562,14 @@
21.226 val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
21.227 val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
21.228 in
21.229 - ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
21.230 + ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward))
21.231 |> (fn it => it COMP graph_is_function)
21.232 - |> implies_intr z_smaller
21.233 - |> forall_intr (cterm_of thy z)
21.234 + |> Thm.implies_intr z_smaller
21.235 + |> Thm.forall_intr (cterm_of thy z)
21.236 |> (fn it => it COMP valthm)
21.237 - |> implies_intr lhs_acc
21.238 + |> Thm.implies_intr lhs_acc
21.239 |> asm_simplify (HOL_basic_ss addsimps [f_iff])
21.240 - |> fold_rev (implies_intr o cprop_of) ags
21.241 + |> fold_rev (Thm.implies_intr o cprop_of) ags
21.242 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
21.243 end
21.244 in
21.245 @@ -588,7 +588,7 @@
21.246 val Globals {domT, x, z, a, P, D, ...} = globals
21.247 val acc_R = mk_acc domT R
21.248
21.249 - val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
21.250 + val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
21.251 val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
21.252
21.253 val D_subset = cterm_of thy (Logic.all x
21.254 @@ -606,7 +606,7 @@
21.255 HOLogic.mk_Trueprop (P $ Bound 0)))
21.256 |> cterm_of thy
21.257
21.258 - val aihyp = assume ihyp
21.259 + val aihyp = Thm.assume ihyp
21.260
21.261 fun prove_case clause =
21.262 let
21.263 @@ -622,10 +622,10 @@
21.264 end
21.265
21.266 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih
21.267 - |> forall_elim (cterm_of thy rcarg)
21.268 + |> Thm.forall_elim (cterm_of thy rcarg)
21.269 |> Thm.elim_implies llRI
21.270 - |> fold_rev (implies_intr o cprop_of) CCas
21.271 - |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
21.272 + |> fold_rev (Thm.implies_intr o cprop_of) CCas
21.273 + |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
21.274
21.275 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
21.276
21.277 @@ -636,19 +636,19 @@
21.278 |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
21.279 |> cterm_of thy
21.280
21.281 - val P_lhs = assume step
21.282 - |> fold forall_elim cqs
21.283 + val P_lhs = Thm.assume step
21.284 + |> fold Thm.forall_elim cqs
21.285 |> Thm.elim_implies lhs_D
21.286 |> fold Thm.elim_implies ags
21.287 |> fold Thm.elim_implies P_recs
21.288
21.289 val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
21.290 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
21.291 - |> symmetric (* P lhs == P x *)
21.292 - |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
21.293 - |> implies_intr (cprop_of case_hyp)
21.294 - |> fold_rev (implies_intr o cprop_of) ags
21.295 - |> fold_rev forall_intr cqs
21.296 + |> Thm.symmetric (* P lhs == P x *)
21.297 + |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *)
21.298 + |> Thm.implies_intr (cprop_of case_hyp)
21.299 + |> fold_rev (Thm.implies_intr o cprop_of) ags
21.300 + |> fold_rev Thm.forall_intr cqs
21.301 in
21.302 (res, step)
21.303 end
21.304 @@ -658,33 +658,33 @@
21.305 val istep = complete_thm
21.306 |> Thm.forall_elim_vars 0
21.307 |> fold (curry op COMP) cases (* P x *)
21.308 - |> implies_intr ihyp
21.309 - |> implies_intr (cprop_of x_D)
21.310 - |> forall_intr (cterm_of thy x)
21.311 + |> Thm.implies_intr ihyp
21.312 + |> Thm.implies_intr (cprop_of x_D)
21.313 + |> Thm.forall_intr (cterm_of thy x)
21.314
21.315 val subset_induct_rule =
21.316 acc_subset_induct
21.317 - |> (curry op COMP) (assume D_subset)
21.318 - |> (curry op COMP) (assume D_dcl)
21.319 - |> (curry op COMP) (assume a_D)
21.320 + |> (curry op COMP) (Thm.assume D_subset)
21.321 + |> (curry op COMP) (Thm.assume D_dcl)
21.322 + |> (curry op COMP) (Thm.assume a_D)
21.323 |> (curry op COMP) istep
21.324 - |> fold_rev implies_intr steps
21.325 - |> implies_intr a_D
21.326 - |> implies_intr D_dcl
21.327 - |> implies_intr D_subset
21.328 + |> fold_rev Thm.implies_intr steps
21.329 + |> Thm.implies_intr a_D
21.330 + |> Thm.implies_intr D_dcl
21.331 + |> Thm.implies_intr D_subset
21.332
21.333 val simple_induct_rule =
21.334 subset_induct_rule
21.335 - |> forall_intr (cterm_of thy D)
21.336 - |> forall_elim (cterm_of thy acc_R)
21.337 + |> Thm.forall_intr (cterm_of thy D)
21.338 + |> Thm.forall_elim (cterm_of thy acc_R)
21.339 |> assume_tac 1 |> Seq.hd
21.340 |> (curry op COMP) (acc_downward
21.341 |> (instantiate' [SOME (ctyp_of thy domT)]
21.342 (map (SOME o cterm_of thy) [R, x, z]))
21.343 - |> forall_intr (cterm_of thy z)
21.344 - |> forall_intr (cterm_of thy x))
21.345 - |> forall_intr (cterm_of thy a)
21.346 - |> forall_intr (cterm_of thy P)
21.347 + |> Thm.forall_intr (cterm_of thy z)
21.348 + |> Thm.forall_intr (cterm_of thy x))
21.349 + |> Thm.forall_intr (cterm_of thy a)
21.350 + |> Thm.forall_intr (cterm_of thy P)
21.351 in
21.352 simple_induct_rule
21.353 end
21.354 @@ -736,18 +736,19 @@
21.355 |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
21.356 |> cterm_of thy
21.357
21.358 - val thm = assume hyp
21.359 - |> fold forall_elim cqs
21.360 + val thm = Thm.assume hyp
21.361 + |> fold Thm.forall_elim cqs
21.362 |> fold Thm.elim_implies ags
21.363 |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
21.364 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
21.365
21.366 val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
21.367 - |> cterm_of thy |> assume
21.368 + |> cterm_of thy |> Thm.assume
21.369
21.370 val acc = thm COMP ih_case
21.371 val z_acc_local = acc
21.372 - |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
21.373 + |> Conv.fconv_rule
21.374 + (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
21.375
21.376 val ethm = z_acc_local
21.377 |> Function_Ctx_Tree.export_thm thy (fixes,
21.378 @@ -785,34 +786,34 @@
21.379 HOLogic.mk_Trueprop (acc_R $ Bound 0)))
21.380 |> cterm_of thy
21.381
21.382 - val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
21.383 + val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
21.384
21.385 val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
21.386
21.387 val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], [])
21.388 in
21.389 R_cases
21.390 - |> forall_elim (cterm_of thy z)
21.391 - |> forall_elim (cterm_of thy x)
21.392 - |> forall_elim (cterm_of thy (acc_R $ z))
21.393 - |> curry op COMP (assume R_z_x)
21.394 + |> Thm.forall_elim (cterm_of thy z)
21.395 + |> Thm.forall_elim (cterm_of thy x)
21.396 + |> Thm.forall_elim (cterm_of thy (acc_R $ z))
21.397 + |> curry op COMP (Thm.assume R_z_x)
21.398 |> fold_rev (curry op COMP) cases
21.399 - |> implies_intr R_z_x
21.400 - |> forall_intr (cterm_of thy z)
21.401 + |> Thm.implies_intr R_z_x
21.402 + |> Thm.forall_intr (cterm_of thy z)
21.403 |> (fn it => it COMP accI)
21.404 - |> implies_intr ihyp
21.405 - |> forall_intr (cterm_of thy x)
21.406 + |> Thm.implies_intr ihyp
21.407 + |> Thm.forall_intr (cterm_of thy x)
21.408 |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
21.409 - |> curry op RS (assume wfR')
21.410 + |> curry op RS (Thm.assume wfR')
21.411 |> forall_intr_vars
21.412 |> (fn it => it COMP allI)
21.413 - |> fold implies_intr hyps
21.414 - |> implies_intr wfR'
21.415 - |> forall_intr (cterm_of thy R')
21.416 - |> forall_elim (cterm_of thy (inrel_R))
21.417 + |> fold Thm.implies_intr hyps
21.418 + |> Thm.implies_intr wfR'
21.419 + |> Thm.forall_intr (cterm_of thy R')
21.420 + |> Thm.forall_elim (cterm_of thy (inrel_R))
21.421 |> curry op RS wf_in_rel
21.422 |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
21.423 - |> forall_intr (cterm_of thy Rrel)
21.424 + |> Thm.forall_intr (cterm_of thy Rrel)
21.425 end
21.426
21.427
21.428 @@ -919,11 +920,11 @@
21.429 RCss GIntro_thms) RIntro_thmss
21.430
21.431 val complete =
21.432 - mk_completeness globals clauses abstract_qglrs |> cert |> assume
21.433 + mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume
21.434
21.435 val compat =
21.436 mk_compat_proof_obligations domT ranT fvar f abstract_qglrs
21.437 - |> map (cert #> assume)
21.438 + |> map (cert #> Thm.assume)
21.439
21.440 val compat_store = store_compat_thms n compat
21.441
22.1 --- a/src/HOL/Tools/Function/function_lib.ML Sat May 15 21:41:32 2010 +0200
22.2 +++ b/src/HOL/Tools/Function/function_lib.ML Sat May 15 21:50:05 2010 +0200
22.3 @@ -5,7 +5,7 @@
22.4 Some fairly general functions that should probably go somewhere else...
22.5 *)
22.6
22.7 -structure Function_Lib =
22.8 +structure Function_Lib = (* FIXME proper signature *)
22.9 struct
22.10
22.11 fun map_option f NONE = NONE
22.12 @@ -104,7 +104,7 @@
22.13
22.14 fun forall_intr_rename (n, cv) thm =
22.15 let
22.16 - val allthm = forall_intr cv thm
22.17 + val allthm = Thm.forall_intr cv thm
22.18 val (_ $ abs) = prop_of allthm
22.19 in
22.20 Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
23.1 --- a/src/HOL/Tools/Function/induction_schema.ML Sat May 15 21:41:32 2010 +0200
23.2 +++ b/src/HOL/Tools/Function/induction_schema.ML Sat May 15 21:50:05 2010 +0200
23.3 @@ -226,7 +226,7 @@
23.4 HOLogic.mk_Trueprop (P_comp $ Bound 0)))
23.5 |> cert
23.6
23.7 - val aihyp = assume ihyp
23.8 + val aihyp = Thm.assume ihyp
23.9
23.10 (* Rule for case splitting along the sum types *)
23.11 val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
23.12 @@ -237,9 +237,9 @@
23.13 fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
23.14 let
23.15 val fxs = map Free xs
23.16 - val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
23.17 + val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
23.18
23.19 - val C_hyps = map (cert #> assume) Cs
23.20 + val C_hyps = map (cert #> Thm.assume) Cs
23.21
23.22 val (relevant_cases, ineqss') =
23.23 (scases_idx ~~ ineqss)
23.24 @@ -248,32 +248,33 @@
23.25
23.26 fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
23.27 let
23.28 - val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
23.29 + val case_hyps =
23.30 + map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
23.31
23.32 val cqs = map (cert o Free) qs
23.33 - val ags = map (assume o cert) gs
23.34 + val ags = map (Thm.assume o cert) gs
23.35
23.36 val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
23.37 val sih = full_simplify replace_x_ss aihyp
23.38
23.39 fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
23.40 let
23.41 - val cGas = map (assume o cert) Gas
23.42 + val cGas = map (Thm.assume o cert) Gas
23.43 val cGvs = map (cert o Free) Gvs
23.44 - val import = fold forall_elim (cqs @ cGvs)
23.45 + val import = fold Thm.forall_elim (cqs @ cGvs)
23.46 #> fold Thm.elim_implies (ags @ cGas)
23.47 val ipres = pres
23.48 - |> forall_elim (cert (list_comb (P_of idx, rcargs)))
23.49 + |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
23.50 |> import
23.51 in
23.52 sih
23.53 - |> forall_elim (cert (inject idx rcargs))
23.54 + |> Thm.forall_elim (cert (inject idx rcargs))
23.55 |> Thm.elim_implies (import ineq) (* Psum rcargs *)
23.56 |> Conv.fconv_rule sum_prod_conv
23.57 |> Conv.fconv_rule ind_rulify
23.58 |> (fn th => th COMP ipres) (* P rs *)
23.59 - |> fold_rev (implies_intr o cprop_of) cGas
23.60 - |> fold_rev forall_intr cGvs
23.61 + |> fold_rev (Thm.implies_intr o cprop_of) cGas
23.62 + |> fold_rev Thm.forall_intr cGvs
23.63 end
23.64
23.65 val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *)
23.66 @@ -288,13 +289,13 @@
23.67 foldl1 (uncurry Conv.combination_conv)
23.68 (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
23.69
23.70 - val res = assume step
23.71 - |> fold forall_elim cqs
23.72 + val res = Thm.assume step
23.73 + |> fold Thm.forall_elim cqs
23.74 |> fold Thm.elim_implies ags
23.75 |> fold Thm.elim_implies P_recs (* P lhs *)
23.76 |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
23.77 - |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
23.78 - |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
23.79 + |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps)
23.80 + |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
23.81 in
23.82 (res, (cidx, step))
23.83 end
23.84 @@ -302,12 +303,12 @@
23.85 val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
23.86
23.87 val bstep = complete_thm
23.88 - |> forall_elim (cert (list_comb (P, fxs)))
23.89 - |> fold (forall_elim o cert) (fxs @ map Free ws)
23.90 + |> Thm.forall_elim (cert (list_comb (P, fxs)))
23.91 + |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
23.92 |> fold Thm.elim_implies C_hyps
23.93 |> fold Thm.elim_implies cases (* P xs *)
23.94 - |> fold_rev (implies_intr o cprop_of) C_hyps
23.95 - |> fold_rev (forall_intr o cert o Free) ws
23.96 + |> fold_rev (Thm.implies_intr o cprop_of) C_hyps
23.97 + |> fold_rev (Thm.forall_intr o cert o Free) ws
23.98
23.99 val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
23.100 |> Goal.init
23.101 @@ -316,8 +317,8 @@
23.102 |> Seq.hd
23.103 |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
23.104 |> Goal.finish ctxt
23.105 - |> implies_intr (cprop_of branch_hyp)
23.106 - |> fold_rev (forall_intr o cert) fxs
23.107 + |> Thm.implies_intr (cprop_of branch_hyp)
23.108 + |> fold_rev (Thm.forall_intr o cert) fxs
23.109 in
23.110 (Pxs, steps)
23.111 end
23.112 @@ -328,8 +329,8 @@
23.113
23.114 val istep = sum_split_rule
23.115 |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
23.116 - |> implies_intr ihyp
23.117 - |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
23.118 + |> Thm.implies_intr ihyp
23.119 + |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
23.120
23.121 val induct_rule =
23.122 @{thm "wf_induct_rule"}
23.123 @@ -353,10 +354,10 @@
23.124 val cert = cterm_of (ProofContext.theory_of ctxt)
23.125
23.126 val ineqss = mk_ineqs R scheme
23.127 - |> map (map (pairself (assume o cert)))
23.128 + |> map (map (pairself (Thm.assume o cert)))
23.129 val complete =
23.130 - map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
23.131 - val wf_thm = mk_wf R scheme |> cert |> assume
23.132 + map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
23.133 + val wf_thm = mk_wf R scheme |> cert |> Thm.assume
23.134
23.135 val (descent, pres) = split_list (flat ineqss)
23.136 val newgoals = complete @ pres @ wf_thm :: descent
23.137 @@ -377,7 +378,7 @@
23.138 end
23.139
23.140 val res = Conjunction.intr_balanced (map_index project branches)
23.141 - |> fold_rev implies_intr (map cprop_of newgoals @ steps)
23.142 + |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps)
23.143 |> Drule.generalize ([], [Rn])
23.144
23.145 val nbranches = length branches
24.1 --- a/src/HOL/Tools/Function/mutual.ML Sat May 15 21:41:32 2010 +0200
24.2 +++ b/src/HOL/Tools/Function/mutual.ML Sat May 15 21:50:05 2010 +0200
24.3 @@ -164,12 +164,12 @@
24.4 val rhs = inst pre_rhs
24.5
24.6 val cqs = map (cterm_of thy) qs
24.7 - val ags = map (assume o cterm_of thy) gs
24.8 + val ags = map (Thm.assume o cterm_of thy) gs
24.9
24.10 - val import = fold forall_elim cqs
24.11 + val import = fold Thm.forall_elim cqs
24.12 #> fold Thm.elim_implies ags
24.13
24.14 - val export = fold_rev (implies_intr o cprop_of) ags
24.15 + val export = fold_rev (Thm.implies_intr o cprop_of) ags
24.16 #> fold_rev forall_intr_rename (oqnames ~~ cqs)
24.17 in
24.18 F ctxt (f, qs, gs, args, rhs) import export
24.19 @@ -184,7 +184,7 @@
24.20 val (simp, restore_cond) =
24.21 case cprems_of psimp of
24.22 [] => (psimp, I)
24.23 - | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
24.24 + | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
24.25 | _ => sys_error "Too many conditions"
24.26
24.27 in
24.28 @@ -202,9 +202,9 @@
24.29 val thy = ProofContext.theory_of ctxt
24.30 val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
24.31 in
24.32 - fold (fn x => fn thm => combination thm (reflexive x)) xs thm
24.33 + fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
24.34 |> Conv.fconv_rule (Thm.beta_conversion true)
24.35 - |> fold_rev forall_intr xs
24.36 + |> fold_rev Thm.forall_intr xs
24.37 |> Thm.forall_elim_vars 0
24.38 end
24.39
24.40 @@ -228,7 +228,7 @@
24.41 val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
24.42
24.43 val induct_inst =
24.44 - forall_elim (cert case_exp) induct
24.45 + Thm.forall_elim (cert case_exp) induct
24.46 |> full_simplify SumTree.sumcase_split_ss
24.47 |> full_simplify (HOL_basic_ss addsimps all_f_defs)
24.48
24.49 @@ -238,9 +238,9 @@
24.50 val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
24.51 in
24.52 (rule
24.53 - |> forall_elim (cert inj)
24.54 + |> Thm.forall_elim (cert inj)
24.55 |> full_simplify SumTree.sumcase_split_ss
24.56 - |> fold_rev (forall_intr o cert) (afs @ newPs),
24.57 + |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
24.58 k + length cargTs)
24.59 end
24.60 in
24.61 @@ -255,7 +255,7 @@
24.62
24.63 val (all_f_defs, fs) =
24.64 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
24.65 - (mk_applied_form lthy cargTs (symmetric f_def), f))
24.66 + (mk_applied_form lthy cargTs (Thm.symmetric f_def), f))
24.67 parts
24.68 |> split_list
24.69
25.1 --- a/src/HOL/Tools/Function/pat_completeness.ML Sat May 15 21:41:32 2010 +0200
25.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML Sat May 15 21:50:05 2010 +0200
25.3 @@ -24,7 +24,7 @@
25.4 fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
25.5 fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
25.6
25.7 -fun inst_free var inst = forall_elim inst o forall_intr var
25.8 +fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
25.9
25.10 fun inst_case_thm thy x P thm =
25.11 let val [Pv, xv] = Term.add_vars (prop_of thm) []
25.12 @@ -69,10 +69,10 @@
25.13 let
25.14 val (_, subps) = strip_comb pat
25.15 val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
25.16 - val c_eq_pat = simplify (HOL_basic_ss addsimps (map assume eqs)) c_assum
25.17 + val c_eq_pat = simplify (HOL_basic_ss addsimps (map Thm.assume eqs)) c_assum
25.18 in
25.19 (subps @ pats,
25.20 - fold_rev implies_intr eqs (implies_elim thm c_eq_pat))
25.21 + fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
25.22 end
25.23
25.24
25.25 @@ -82,12 +82,12 @@
25.26 let
25.27 val (avars, pvars, newidx) = invent_vars cons idx
25.28 val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
25.29 - val c_assum = assume c_hyp
25.30 + val c_assum = Thm.assume c_hyp
25.31 val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
25.32 in
25.33 o_alg thy P newidx (avars @ vs) newpats
25.34 - |> implies_intr c_hyp
25.35 - |> fold_rev (forall_intr o cterm_of thy) avars
25.36 + |> Thm.implies_intr c_hyp
25.37 + |> fold_rev (Thm.forall_intr o cterm_of thy) avars
25.38 end
25.39 | constr_case _ _ _ _ _ _ = raise Match
25.40 and o_alg thy P idx [] (([], Pthm) :: _) = Pthm
25.41 @@ -119,11 +119,11 @@
25.42 |> cterm_of thy
25.43
25.44 val hyps = map2 mk_assum qss patss
25.45 - fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
25.46 + fun inst_hyps hyp qs = fold (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp)
25.47 val assums = map2 inst_hyps hyps qss
25.48 in
25.49 o_alg thy P 2 xs (patss ~~ assums)
25.50 - |> fold_rev implies_intr hyps
25.51 + |> fold_rev Thm.implies_intr hyps
25.52 end
25.53
25.54 fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
25.55 @@ -147,7 +147,7 @@
25.56
25.57 val patss = map (map snd) x_pats
25.58 val complete_thm = prove_completeness thy xs thesis qss patss
25.59 - |> fold_rev (forall_intr o cterm_of thy) vs
25.60 + |> fold_rev (Thm.forall_intr o cterm_of thy) vs
25.61 in
25.62 PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
25.63 end
26.1 --- a/src/HOL/Tools/Qelim/cooper.ML Sat May 15 21:41:32 2010 +0200
26.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Sat May 15 21:50:05 2010 +0200
26.3 @@ -331,7 +331,7 @@
26.4 | t => if is_intrel t
26.5 then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
26.6 RS eq_reflection
26.7 - else reflexive ct;
26.8 + else Thm.reflexive ct;
26.9
26.10 val dvdc = @{cterm "op dvd :: int => _"};
26.11
26.12 @@ -369,7 +369,7 @@
26.13 (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
26.14 (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
26.15 @{cterm "0::int"})))
26.16 - in equal_elim (Thm.symmetric th) TrueI end;
26.17 + in Thm.equal_elim (Thm.symmetric th) TrueI end;
26.18 val notz =
26.19 let val tab = fold Inttab.update
26.20 (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
26.21 @@ -412,11 +412,11 @@
26.22 val ltx = Thm.capply (Thm.capply cmulC clt) cx
26.23 val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
26.24 val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
26.25 - val thf = transitive th
26.26 - (transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
26.27 + val thf = Thm.transitive th
26.28 + (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
26.29 val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
26.30 - ||> beta_conversion true |>> Thm.symmetric
26.31 - in transitive (transitive lth thf) rth end;
26.32 + ||> Thm.beta_conversion true |>> Thm.symmetric
26.33 + in Thm.transitive (Thm.transitive lth thf) rth end;
26.34
26.35
26.36 val emptyIS = @{cterm "{}::int set"};
26.37 @@ -459,7 +459,7 @@
26.38 Simplifier.rewrite lin_ss
26.39 (Thm.capply @{cterm Trueprop}
26.40 (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
26.41 - in equal_elim (Thm.symmetric th) TrueI end;
26.42 + in Thm.equal_elim (Thm.symmetric th) TrueI end;
26.43 val dvd =
26.44 let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
26.45 fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
26.46 @@ -471,7 +471,7 @@
26.47 let val th = Simplifier.rewrite lin_ss
26.48 (Thm.capply @{cterm Trueprop}
26.49 (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
26.50 - in equal_elim (Thm.symmetric th) TrueI end;
26.51 + in Thm.equal_elim (Thm.symmetric th) TrueI end;
26.52 (* A and B set *)
26.53 local
26.54 val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
26.55 @@ -483,7 +483,7 @@
26.56 | Const(@{const_name insert}, _) $ y $ _ =>
26.57 let val (cy,S') = Thm.dest_binop S
26.58 in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
26.59 - else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
26.60 + else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
26.61 (provein x S')
26.62 end
26.63 end
26.64 @@ -494,14 +494,14 @@
26.65 if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
26.66 then
26.67 (bl,b0,decomp_minf,
26.68 - fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
26.69 + fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
26.70 [bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
26.71 (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
26.72 [bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
26.73 bsetdisj,infDconj, infDdisj]),
26.74 cpmi)
26.75 else (al,a0,decomp_pinf,fn A =>
26.76 - (map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
26.77 + (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
26.78 [aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
26.79 (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
26.80 [asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
26.81 @@ -776,7 +776,7 @@
26.82 fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
26.83 val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
26.84 val p' = fold_rev gen ts p
26.85 - in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
26.86 + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
26.87
26.88 local
26.89 val ss1 = comp_ss
26.90 @@ -792,7 +792,7 @@
26.91 @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
26.92 addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
26.93 val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
26.94 - @ map (symmetric o mk_meta_eq)
26.95 + @ map (Thm.symmetric o mk_meta_eq)
26.96 [@{thm "dvd_eq_mod_eq_0"},
26.97 @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
26.98 @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
26.99 @@ -823,7 +823,7 @@
26.100 then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
26.101 else Conv.arg_conv (conv ctxt) p
26.102 val p' = Thm.rhs_of cpth
26.103 - val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
26.104 + val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
26.105 in rtac th i end
26.106 handle COOPER _ => no_tac);
26.107
27.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sat May 15 21:41:32 2010 +0200
27.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sat May 15 21:50:05 2010 +0200
27.3 @@ -69,7 +69,7 @@
27.4 val th0 = if mi then
27.5 instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th
27.6 else instantiate ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th
27.7 - in implies_elim (implies_elim th0 th') th'' end
27.8 + in Thm.implies_elim (Thm.implies_elim th0 th') th'' end
27.9 in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
27.10 fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
27.11 end
27.12 @@ -88,7 +88,7 @@
27.13 val enth = Drule.arg_cong_rule ce nthx
27.14 val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
27.15 fun ins x th =
27.16 - implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
27.17 + Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
27.18 (Thm.cprop_of th), SOME x] th1) th
27.19 val fU = fold ins u th0
27.20 val cU = funpow 2 Thm.dest_arg (Thm.cprop_of fU)
27.21 @@ -102,7 +102,7 @@
27.22 | Const(@{const_name insert}, _) $ y $_ =>
27.23 let val (cy,S') = Thm.dest_binop S
27.24 in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
27.25 - else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
27.26 + else Thm.implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
27.27 (provein x S')
27.28 end
27.29 end
27.30 @@ -152,7 +152,7 @@
27.31 | Eq => [minf_eq, pinf_eq, nmi_eq, npi_eq, ld_eq]
27.32 | NEq => [minf_neq, pinf_neq, nmi_neq, npi_neq, ld_neq])
27.33 val tU = U t
27.34 - fun Ufw th = implies_elim th tU
27.35 + fun Ufw th = Thm.implies_elim th tU
27.36 in [mi_th, pi_th, Ufw nmi_th, Ufw npi_th, Ufw ld_th]
27.37 end
27.38 in ([], K (mi_th, pi_th, nmi_th, npi_th, ld_th)) end)
27.39 @@ -164,7 +164,7 @@
27.40 [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
27.41 val bex_conv =
27.42 Simplifier.rewrite (HOL_basic_ss addsimps simp_thms@(@{thms "bex_simps" (1-5)}))
27.43 - val result_th = fconv_rule (arg_conv bex_conv) (transitive enth qe_th)
27.44 + val result_th = fconv_rule (arg_conv bex_conv) (Thm.transitive enth qe_th)
27.45 in result_th
27.46 end
27.47
28.1 --- a/src/HOL/Tools/Qelim/langford.ML Sat May 15 21:41:32 2010 +0200
28.2 +++ b/src/HOL/Tools/Qelim/langford.ML Sat May 15 21:50:05 2010 +0200
28.3 @@ -22,7 +22,7 @@
28.4 fun prove_finite cT u =
28.5 let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
28.6 fun ins x th =
28.7 - implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
28.8 + Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
28.9 (Thm.cprop_of th), SOME x] th1) th
28.10 in fold ins u th0 end;
28.11
28.12 @@ -51,17 +51,17 @@
28.13 (Const (@{const_name Orderings.bot}, _),_) =>
28.14 let
28.15 val (neU,fU) = proveneF U
28.16 - in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end
28.17 + in simp_rule (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
28.18 | (_,Const (@{const_name Orderings.bot}, _)) =>
28.19 let
28.20 val (neL,fL) = proveneF L
28.21 - in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end
28.22 + in simp_rule (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
28.23
28.24 | (_,_) =>
28.25 let
28.26 val (neL,fL) = proveneF L
28.27 val (neU,fU) = proveneF U
28.28 - in simp_rule (transitive ths (dlo_qeth OF [neL, neU, fL, fU]))
28.29 + in simp_rule (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU]))
28.30 end
28.31 in qe end
28.32 | _ => error "dlo_qe : Not an existential formula";
28.33 @@ -101,8 +101,8 @@
28.34 fun conj_aci_rule eq =
28.35 let
28.36 val (l,r) = Thm.dest_equals eq
28.37 - fun tabl c = the (Termtab.lookup (mk_conj_tab (assume l)) (term_of c))
28.38 - fun tabr c = the (Termtab.lookup (mk_conj_tab (assume r)) (term_of c))
28.39 + fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
28.40 + fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
28.41 val ll = Thm.dest_arg l
28.42 val rr = Thm.dest_arg r
28.43
28.44 @@ -111,7 +111,7 @@
28.45 val thr = prove_conj tabr (conjuncts ll)
28.46 |> Drule.implies_intr_hyps
28.47 val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
28.48 - in implies_elim (implies_elim eqI thl) thr |> mk_meta_eq end;
28.49 + in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
28.50
28.51 fun contains x ct = member (op aconv) (OldTerm.term_frees (term_of ct)) (term_of x);
28.52
28.53 @@ -136,7 +136,7 @@
28.54 | _ =>
28.55 conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
28.56 (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
28.57 - |> abstract_rule xn x |> Drule.arg_cong_rule e
28.58 + |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
28.59 |> Conv.fconv_rule (Conv.arg_conv
28.60 (Simplifier.rewrite
28.61 (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
28.62 @@ -144,7 +144,7 @@
28.63 end
28.64 | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
28.65 (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
28.66 - |> abstract_rule xn x |> Drule.arg_cong_rule e
28.67 + |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
28.68 |> Conv.fconv_rule (Conv.arg_conv
28.69 (Simplifier.rewrite
28.70 (HOL_basic_ss addsimps (simp_thms @ ex_simps))))
28.71 @@ -167,7 +167,7 @@
28.72 @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib])
28.73 in fn p =>
28.74 Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
28.75 - (Thm.add_cterm_frees p []) (K reflexive) (K reflexive)
28.76 + (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
28.77 (K (basic_dloqe () gst qe_bnds qe_nolb qe_noub gs)) p
28.78 end;
28.79
28.80 @@ -212,7 +212,7 @@
28.81 fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
28.82 val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
28.83 val p' = fold_rev gen ts p
28.84 - in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
28.85 + in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
28.86
28.87
28.88 fun cfrees ats ct =
29.1 --- a/src/HOL/Tools/Qelim/qelim.ML Sat May 15 21:41:32 2010 +0200
29.2 +++ b/src/HOL/Tools/Qelim/qelim.ML Sat May 15 21:50:05 2010 +0200
29.3 @@ -47,7 +47,7 @@
29.4 val p = Thm.dest_arg p
29.5 val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
29.6 val th = instantiate' [SOME T] [SOME p] all_not_ex
29.7 - in transitive th (conv env (Thm.rhs_of th))
29.8 + in Thm.transitive th (conv env (Thm.rhs_of th))
29.9 end
29.10 | _ => atcv env p
29.11 in precv then_conv (conv env) then_conv postcv end
30.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat May 15 21:41:32 2010 +0200
30.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat May 15 21:50:05 2010 +0200
30.3 @@ -517,7 +517,7 @@
30.4 *)
30.5 fun clean_tac lthy =
30.6 let
30.7 - val defs = map (symmetric o #def) (qconsts_dest lthy)
30.8 + val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
30.9 val prs = prs_rules_get lthy
30.10 val ids = id_simps_get lthy
30.11 val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
31.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat May 15 21:41:32 2010 +0200
31.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat May 15 21:50:05 2010 +0200
31.3 @@ -35,7 +35,7 @@
31.4 (* Useful Theorems *)
31.5 (* ------------------------------------------------------------------------- *)
31.6 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
31.7 -val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
31.8 +val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
31.9 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
31.10 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
31.11
31.12 @@ -364,7 +364,7 @@
31.13 in cterm_instantiate substs th end;
31.14
31.15 (* INFERENCE RULE: AXIOM *)
31.16 -fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th);
31.17 +fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
31.18 (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
31.19
31.20 (* INFERENCE RULE: ASSUME *)
31.21 @@ -527,7 +527,7 @@
31.22 val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
31.23 val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
31.24 val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
31.25 - val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
31.26 + val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
31.27 val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
31.28 val eq_terms = map (pairself (cterm_of thy))
31.29 (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
32.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat May 15 21:41:32 2010 +0200
32.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat May 15 21:50:05 2010 +0200
32.3 @@ -209,7 +209,7 @@
32.4 Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
32.5 end
32.6 else if loose_bvar1 (rand,0) then (*B or eta*)
32.7 - if rand = Bound 0 then eta_conversion ct
32.8 + if rand = Bound 0 then Thm.eta_conversion ct
32.9 else (*B*)
32.10 let val crand = cterm_of thy (Abs(x,xT,rand))
32.11 val crator = cterm_of thy rator
32.12 @@ -225,7 +225,7 @@
32.13 (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
32.14 prefix for the constants.*)
32.15 fun combinators_aux ct =
32.16 - if lambda_free (term_of ct) then reflexive ct
32.17 + if lambda_free (term_of ct) then Thm.reflexive ct
32.18 else
32.19 case term_of ct of
32.20 Abs _ =>
32.21 @@ -234,17 +234,17 @@
32.22 val u_th = combinators_aux cta
32.23 val cu = Thm.rhs_of u_th
32.24 val comb_eq = abstract (Thm.cabs cv cu)
32.25 - in transitive (abstract_rule v cv u_th) comb_eq end
32.26 + in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
32.27 | _ $ _ =>
32.28 let val (ct1, ct2) = Thm.dest_comb ct
32.29 - in combination (combinators_aux ct1) (combinators_aux ct2) end;
32.30 + in Thm.combination (combinators_aux ct1) (combinators_aux ct2) end;
32.31
32.32 fun combinators th =
32.33 if lambda_free (prop_of th) then th
32.34 else
32.35 let val th = Drule.eta_contraction_rule th
32.36 val eqth = combinators_aux (cprop_of th)
32.37 - in equal_elim eqth th end
32.38 + in Thm.equal_elim eqth th end
32.39 handle THM (msg,_,_) =>
32.40 (warning (cat_lines
32.41 ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th,
32.42 @@ -298,7 +298,7 @@
32.43
32.44 (*Generate Skolem functions for a theorem supplied in nnf*)
32.45 fun assume_skolem_of_def s th =
32.46 - map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
32.47 + map (skolem_of_def o Thm.assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
32.48
32.49
32.50 (*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
33.1 --- a/src/HOL/Tools/TFL/casesplit.ML Sat May 15 21:41:32 2010 +0200
33.2 +++ b/src/HOL/Tools/TFL/casesplit.ML Sat May 15 21:50:05 2010 +0200
33.3 @@ -79,8 +79,8 @@
33.4 (* beta-eta contract the theorem *)
33.5 fun beta_eta_contract thm =
33.6 let
33.7 - val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
33.8 - val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
33.9 + val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
33.10 + val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
33.11 in thm3 end;
33.12
33.13 (* make a casethm from an induction thm *)
34.1 --- a/src/HOL/Tools/TFL/rules.ML Sat May 15 21:41:32 2010 +0200
34.2 +++ b/src/HOL/Tools/TFL/rules.ML Sat May 15 21:50:05 2010 +0200
34.3 @@ -172,7 +172,7 @@
34.4 val [P,Q] = OldTerm.term_vars prop
34.5 val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
34.6 in
34.7 -fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
34.8 +fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1)
34.9 handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
34.10 end;
34.11
34.12 @@ -181,7 +181,7 @@
34.13 val [P,Q] = OldTerm.term_vars prop
34.14 val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
34.15 in
34.16 -fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
34.17 +fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2)
34.18 handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
34.19 end;
34.20
34.21 @@ -276,11 +276,11 @@
34.22 val prop = Thm.prop_of spec
34.23 val x = hd (tl (OldTerm.term_vars prop))
34.24 val cTV = ctyp_of thy (type_of x)
34.25 - val gspec = forall_intr (cterm_of thy x) spec
34.26 + val gspec = Thm.forall_intr (cterm_of thy x) spec
34.27 in
34.28 fun SPEC tm thm =
34.29 let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
34.30 - in thm RS (forall_elim tm gspec') end
34.31 + in thm RS (Thm.forall_elim tm gspec') end
34.32 end;
34.33
34.34 fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
34.35 @@ -302,7 +302,7 @@
34.36 ctm_theta s (Vartab.dest tm_theta))
34.37 in
34.38 fun GEN v th =
34.39 - let val gth = forall_intr v th
34.40 + let val gth = Thm.forall_intr v th
34.41 val thy = Thm.theory_of_thm gth
34.42 val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
34.43 val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
34.44 @@ -533,9 +533,9 @@
34.45 *---------------------------------------------------------------------------*)
34.46
34.47 fun list_beta_conv tm =
34.48 - let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))
34.49 + let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th))))
34.50 fun iter [] = Thm.reflexive tm
34.51 - | iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v))
34.52 + | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
34.53 in iter end;
34.54
34.55
34.56 @@ -619,7 +619,7 @@
34.57 fun VSTRUCT_ELIM tych a vstr th =
34.58 let val L = S.free_vars_lr vstr
34.59 val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
34.60 - val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
34.61 + val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
34.62 val thm2 = forall_intr_list (map tych L) thm1
34.63 val thm3 = forall_elim_list (XFILL tych a vstr) thm2
34.64 in refl RS
34.65 @@ -630,7 +630,7 @@
34.66 let val a1 = tych a
34.67 val vstr1 = tych vstr
34.68 in
34.69 - forall_intr a1
34.70 + Thm.forall_intr a1
34.71 (if (is_Free vstr)
34.72 then cterm_instantiate [(vstr1,a1)] th
34.73 else VSTRUCT_ELIM tych a vstr th)
34.74 @@ -803,7 +803,7 @@
34.75 val names = OldTerm.add_term_names (term_of ctm, [])
34.76 val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
34.77 (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
34.78 - val th2 = equal_elim th1 th
34.79 + val th2 = Thm.equal_elim th1 th
34.80 in
34.81 (th2, filter_out restricted (!tc_list))
34.82 end;
35.1 --- a/src/HOL/Tools/TFL/tfl.ML Sat May 15 21:41:32 2010 +0200
35.2 +++ b/src/HOL/Tools/TFL/tfl.ML Sat May 15 21:50:05 2010 +0200
35.3 @@ -556,8 +556,8 @@
35.4 else ()
35.5 val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
35.6 val SV' = map tych SV;
35.7 - val SVrefls = map reflexive SV'
35.8 - val def0 = (fold (fn x => fn th => R.rbeta(combination th x))
35.9 + val SVrefls = map Thm.reflexive SV'
35.10 + val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x))
35.11 SVrefls def)
35.12 RS meta_eq_to_obj_eq
35.13 val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
36.1 --- a/src/HOL/Tools/choice_specification.ML Sat May 15 21:41:32 2010 +0200
36.2 +++ b/src/HOL/Tools/choice_specification.ML Sat May 15 21:50:05 2010 +0200
36.3 @@ -183,7 +183,7 @@
36.4 fun process_single ((name,atts),rew_imp,frees) args =
36.5 let
36.6 fun undo_imps thm =
36.7 - equal_elim (symmetric rew_imp) thm
36.8 + Thm.equal_elim (Thm.symmetric rew_imp) thm
36.9
36.10 fun add_final (arg as (thy, thm)) =
36.11 if name = ""
37.1 --- a/src/HOL/Tools/cnf_funcs.ML Sat May 15 21:41:32 2010 +0200
37.2 +++ b/src/HOL/Tools/cnf_funcs.ML Sat May 15 21:50:05 2010 +0200
37.3 @@ -435,9 +435,9 @@
37.4 val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
37.5 val var = new_free ()
37.6 val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *)
37.7 - val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
37.8 - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
37.9 - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
37.10 + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
37.11 + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
37.12 + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
37.13 in
37.14 iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
37.15 end
37.16 @@ -446,9 +446,9 @@
37.17 val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
37.18 val var = new_free ()
37.19 val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *)
37.20 - val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
37.21 - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
37.22 - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
37.23 + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
37.24 + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
37.25 + val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
37.26 in
37.27 iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *)
37.28 end
37.29 @@ -466,8 +466,8 @@
37.30 val var = new_free ()
37.31 val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
37.32 val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *)
37.33 - val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *)
37.34 - val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
37.35 + val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *)
37.36 + val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
37.37 val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
37.38 in
37.39 iff_trans OF [thm1, thm5]
38.1 --- a/src/HOL/Tools/inductive_realizer.ML Sat May 15 21:41:32 2010 +0200
38.2 +++ b/src/HOL/Tools/inductive_realizer.ML Sat May 15 21:50:05 2010 +0200
38.3 @@ -21,7 +21,7 @@
38.4 [name] => name
38.5 | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
38.6
38.7 -val all_simps = map (symmetric o mk_meta_eq) @{thms HOL.all_simps};
38.8 +val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
38.9
38.10 fun prf_of thm =
38.11 let
39.1 --- a/src/HOL/Tools/inductive_set.ML Sat May 15 21:41:32 2010 +0200
39.2 +++ b/src/HOL/Tools/inductive_set.ML Sat May 15 21:50:05 2010 +0200
39.3 @@ -114,9 +114,9 @@
39.4 let val rews = map mk_rew ts
39.5 in
39.6 if forall is_none rews then NONE
39.7 - else SOME (fold (fn th1 => fn th2 => combination th2 th1)
39.8 - (map2 (fn SOME r => K r | NONE => reflexive o cterm_of thy)
39.9 - rews ts) (reflexive (cterm_of thy h)))
39.10 + else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
39.11 + (map2 (fn SOME r => K r | NONE => Thm.reflexive o cterm_of thy)
39.12 + rews ts) (Thm.reflexive (cterm_of thy h)))
39.13 end
39.14 | NONE => NONE)
39.15 | _ => NONE
40.1 --- a/src/HOL/Tools/int_arith.ML Sat May 15 21:41:32 2010 +0200
40.2 +++ b/src/HOL/Tools/int_arith.ML Sat May 15 21:50:05 2010 +0200
40.3 @@ -21,7 +21,7 @@
40.4 That is, m and n consist only of 1s combined with "+", "-" and "*".
40.5 *)
40.6
40.7 -val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
40.8 +val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0};
40.9
40.10 val lhss0 = [@{cpat "0::?'a::ring"}];
40.11
40.12 @@ -35,7 +35,7 @@
40.13 make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
40.14 proc = proc0, identifier = []};
40.15
40.16 -val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
40.17 +val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1};
40.18
40.19 val lhss1 = [@{cpat "1::?'a::ring_1"}];
40.20
41.1 --- a/src/HOL/Tools/numeral_simprocs.ML Sat May 15 21:41:32 2010 +0200
41.2 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat May 15 21:50:05 2010 +0200
41.3 @@ -614,12 +614,12 @@
41.4
41.5 fun prove_nz ss T t =
41.6 let
41.7 - val z = instantiate_cterm ([(zT,T)],[]) zr
41.8 - val eq = instantiate_cterm ([(eqT,T)],[]) geq
41.9 + val z = Thm.instantiate_cterm ([(zT,T)],[]) zr
41.10 + val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq
41.11 val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
41.12 (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
41.13 (Thm.capply (Thm.capply eq t) z)))
41.14 - in equal_elim (symmetric th) TrueI
41.15 + in Thm.equal_elim (Thm.symmetric th) TrueI
41.16 end
41.17
41.18 fun proc phi ss ct =
41.19 @@ -630,7 +630,7 @@
41.20 val T = ctyp_of_term x
41.21 val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
41.22 val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
41.23 - in SOME (implies_elim (implies_elim th y_nz) z_nz)
41.24 + in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
41.25 end
41.26 handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
41.27
41.28 @@ -643,13 +643,13 @@
41.29 let val (x,y) = Thm.dest_binop l val z = r
41.30 val _ = map (HOLogic.dest_number o term_of) [x,y,z]
41.31 val ynz = prove_nz ss T y
41.32 - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
41.33 + in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
41.34 end
41.35 | (_, Const (@{const_name Rings.divide},_)$_$_) =>
41.36 let val (x,y) = Thm.dest_binop r val z = l
41.37 val _ = map (HOLogic.dest_number o term_of) [x,y,z]
41.38 val ynz = prove_nz ss T y
41.39 - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
41.40 + in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
41.41 end
41.42 | _ => NONE)
41.43 end
42.1 --- a/src/HOL/Tools/record.ML Sat May 15 21:41:32 2010 +0200
42.2 +++ b/src/HOL/Tools/record.ML Sat May 15 21:50:05 2010 +0200
42.3 @@ -2171,7 +2171,7 @@
42.4
42.5 fun get_upd_acc_congs () =
42.6 let
42.7 - val symdefs = map symmetric (sel_defs @ upd_defs);
42.8 + val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
42.9 val fold_ss = HOL_basic_ss addsimps symdefs;
42.10 val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
42.11 in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
42.12 @@ -2257,17 +2257,17 @@
42.13 val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
42.14 val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
42.15 val thl =
42.16 - assume cl (*All r. P r*) (* 1 *)
42.17 - |> obj_to_meta_all (*!!r. P r*)
42.18 - |> equal_elim split_meta' (*!!n m more. P (ext n m more)*)
42.19 - |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*)
42.20 - |> implies_intr cl (* 1 ==> 2 *)
42.21 + Thm.assume cl (*All r. P r*) (* 1 *)
42.22 + |> obj_to_meta_all (*!!r. P r*)
42.23 + |> Thm.equal_elim split_meta' (*!!n m more. P (ext n m more)*)
42.24 + |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*)
42.25 + |> Thm.implies_intr cl (* 1 ==> 2 *)
42.26 val thr =
42.27 - assume cr (*All n m more. P (ext n m more)*)
42.28 - |> obj_to_meta_all (*!!n m more. P (ext n m more)*)
42.29 - |> equal_elim (symmetric split_meta') (*!!r. P r*)
42.30 - |> meta_to_obj_all (*All r. P r*)
42.31 - |> implies_intr cr (* 2 ==> 1 *)
42.32 + Thm.assume cr (*All n m more. P (ext n m more)*)
42.33 + |> obj_to_meta_all (*!!n m more. P (ext n m more)*)
42.34 + |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
42.35 + |> meta_to_obj_all (*All r. P r*)
42.36 + |> Thm.implies_intr cr (* 2 ==> 1 *)
42.37 in thr COMP (thl COMP iffI) end;
42.38
42.39
43.1 --- a/src/HOL/Tools/semiring_normalizer.ML Sat May 15 21:41:32 2010 +0200
43.2 +++ b/src/HOL/Tools/semiring_normalizer.ML Sat May 15 21:50:05 2010 +0200
43.3 @@ -147,7 +147,7 @@
43.4 val semiring = (sr_ops, sr_rules');
43.5 val ring = (r_ops, r_rules');
43.6 val field = (f_ops, f_rules');
43.7 - val ideal' = map (symmetric o mk_meta) ideal
43.8 + val ideal' = map (Thm.symmetric o mk_meta) ideal
43.9 in
43.10 AList.delete Thm.eq_thm key #>
43.11 cons (key, ({vars = vars, semiring = semiring,
43.12 @@ -328,16 +328,16 @@
43.13 ((let val (rx,rn) = dest_pow r
43.14 val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29
43.15 val (tm1,tm2) = Thm.dest_comb(concl th1) in
43.16 - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
43.17 + Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
43.18 handle CTERM _ =>
43.19 (let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31
43.20 val (tm1,tm2) = Thm.dest_comb(concl th1) in
43.21 - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
43.22 + Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end)
43.23 handle CTERM _ =>
43.24 ((let val (rx,rn) = dest_pow r
43.25 val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30
43.26 val (tm1,tm2) = Thm.dest_comb(concl th1) in
43.27 - transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
43.28 + Thm.transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)
43.29 handle CTERM _ => inst_thm [(cx,l)] pthm_32
43.30
43.31 ))
43.32 @@ -348,7 +348,7 @@
43.33 fun monomial_deone th =
43.34 (let val (l,r) = dest_mul(concl th) in
43.35 if l aconvc one_tm
43.36 - then transitive th (inst_thm [(ca,r)] pthm_13) else th end)
43.37 + then Thm.transitive th (inst_thm [(ca,r)] pthm_13) else th end)
43.38 handle CTERM _ => th;
43.39
43.40 (* Conversion for "(monomial)^n", where n is a numeral. *)
43.41 @@ -357,7 +357,7 @@
43.42 let
43.43 fun monomial_pow tm bod ntm =
43.44 if not(is_comb bod)
43.45 - then reflexive tm
43.46 + then Thm.reflexive tm
43.47 else
43.48 if is_semiring_constant bod
43.49 then semiring_pow_conv tm
43.50 @@ -365,7 +365,7 @@
43.51 let
43.52 val (lopr,r) = Thm.dest_comb bod
43.53 in if not(is_comb lopr)
43.54 - then reflexive tm
43.55 + then Thm.reflexive tm
43.56 else
43.57 let
43.58 val (opr,l) = Thm.dest_comb lopr
43.59 @@ -374,7 +374,7 @@
43.60 then
43.61 let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34
43.62 val (l,r) = Thm.dest_comb(concl th1)
43.63 - in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
43.64 + in Thm.transitive th1 (Drule.arg_cong_rule l (nat_add_conv r))
43.65 end
43.66 else
43.67 if opr aconvc mul_tm
43.68 @@ -385,9 +385,9 @@
43.69 val (x,y) = Thm.dest_comb xy
43.70 val thl = monomial_pow y l ntm
43.71 val thr = monomial_pow z r ntm
43.72 - in transitive th1 (combination (Drule.arg_cong_rule x thl) thr)
43.73 + in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule x thl) thr)
43.74 end
43.75 - else reflexive tm
43.76 + else Thm.reflexive tm
43.77 end
43.78 end
43.79 in fn tm =>
43.80 @@ -436,18 +436,18 @@
43.81 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.82 val (tm3,tm4) = Thm.dest_comb tm1
43.83 val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
43.84 - val th3 = transitive th1 th2
43.85 + val th3 = Thm.transitive th1 th2
43.86 val (tm5,tm6) = Thm.dest_comb(concl th3)
43.87 val (tm7,tm8) = Thm.dest_comb tm6
43.88 val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8
43.89 - in transitive th3 (Drule.arg_cong_rule tm5 th4)
43.90 + in Thm.transitive th3 (Drule.arg_cong_rule tm5 th4)
43.91 end
43.92 else
43.93 let val th0 = if ord < 0 then pthm_16 else pthm_17
43.94 val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0
43.95 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.96 val (tm3,tm4) = Thm.dest_comb tm2
43.97 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
43.98 + in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
43.99 end
43.100 end)
43.101 handle CTERM _ =>
43.102 @@ -459,14 +459,14 @@
43.103 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.104 val (tm3,tm4) = Thm.dest_comb tm1
43.105 val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2
43.106 - in transitive th1 th2
43.107 + in Thm.transitive th1 th2
43.108 end
43.109 else
43.110 if ord < 0 then
43.111 let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19
43.112 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.113 val (tm3,tm4) = Thm.dest_comb tm2
43.114 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
43.115 + in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
43.116 end
43.117 else inst_thm [(ca,l),(cb,r)] pthm_09
43.118 end)) end)
43.119 @@ -480,22 +480,22 @@
43.120 let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21
43.121 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.122 val (tm3,tm4) = Thm.dest_comb tm1
43.123 - in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
43.124 + in Thm.transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2)
43.125 end
43.126 else if ord > 0 then
43.127 let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22
43.128 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.129 val (tm3,tm4) = Thm.dest_comb tm2
43.130 - in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
43.131 + in Thm.transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4))
43.132 end
43.133 - else reflexive tm
43.134 + else Thm.reflexive tm
43.135 end)
43.136 handle CTERM _ =>
43.137 (let val vr = powvar r
43.138 val ord = vorder vl vr
43.139 in if ord = 0 then powvar_mul_conv tm
43.140 else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09
43.141 - else reflexive tm
43.142 + else Thm.reflexive tm
43.143 end)) end))
43.144 in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r)
43.145 end
43.146 @@ -511,8 +511,8 @@
43.147 val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37
43.148 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.149 val (tm3,tm4) = Thm.dest_comb tm1
43.150 - val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
43.151 - in transitive th1 th2
43.152 + val th2 = Thm.combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2)
43.153 + in Thm.transitive th1 th2
43.154 end)
43.155 handle CTERM _ => monomial_mul_conv tm)
43.156 end
43.157 @@ -537,11 +537,11 @@
43.158 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.159 val (tm3,tm4) = Thm.dest_comb tm1
43.160 val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4)
43.161 - val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2)
43.162 + val th3 = Thm.transitive th1 (Drule.fun_cong_rule th2 tm2)
43.163 val tm5 = concl th3
43.164 in
43.165 if (Thm.dest_arg1 tm5) aconvc zero_tm
43.166 - then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
43.167 + then Thm.transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11)
43.168 else monomial_deone th3
43.169 end
43.170 end;
43.171 @@ -603,9 +603,9 @@
43.172 val l = Thm.dest_arg lopr
43.173 in
43.174 if l aconvc zero_tm
43.175 - then transitive th (inst_thm [(ca,r)] pthm_07) else
43.176 + then Thm.transitive th (inst_thm [(ca,r)] pthm_07) else
43.177 if r aconvc zero_tm
43.178 - then transitive th (inst_thm [(ca,l)] pthm_08) else th
43.179 + then Thm.transitive th (inst_thm [(ca,l)] pthm_08) else th
43.180 end
43.181 end
43.182 fun padd tm =
43.183 @@ -628,14 +628,14 @@
43.184 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.185 val (tm3,tm4) = Thm.dest_comb tm1
43.186 val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4)
43.187 - in dezero_rule (transitive th1 (combination th2 (padd tm2)))
43.188 + in dezero_rule (Thm.transitive th1 (Thm.combination th2 (padd tm2)))
43.189 end
43.190 else (* ord <> 0*)
43.191 let val th1 =
43.192 if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
43.193 else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
43.194 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.195 - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
43.196 + in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
43.197 end
43.198 end
43.199 else (* not (is_add r)*)
43.200 @@ -646,13 +646,13 @@
43.201 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.202 val (tm3,tm4) = Thm.dest_comb tm1
43.203 val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
43.204 - in dezero_rule (transitive th1 th2)
43.205 + in dezero_rule (Thm.transitive th1 th2)
43.206 end
43.207 else (* ord <> 0*)
43.208 if ord > 0 then
43.209 let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24
43.210 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.211 - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
43.212 + in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
43.213 end
43.214 else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
43.215 end
43.216 @@ -667,21 +667,21 @@
43.217 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.218 val (tm3,tm4) = Thm.dest_comb tm1
43.219 val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2
43.220 - in dezero_rule (transitive th1 th2)
43.221 + in dezero_rule (Thm.transitive th1 th2)
43.222 end
43.223 else
43.224 - if ord > 0 then reflexive tm
43.225 + if ord > 0 then Thm.reflexive tm
43.226 else
43.227 let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25
43.228 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.229 - in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
43.230 + in dezero_rule (Thm.transitive th1 (Drule.arg_cong_rule tm1 (padd tm2)))
43.231 end
43.232 end
43.233 else
43.234 let val ord = morder l r
43.235 in
43.236 if ord = 0 then monomial_add_conv tm
43.237 - else if ord > 0 then dezero_rule(reflexive tm)
43.238 + else if ord > 0 then dezero_rule(Thm.reflexive tm)
43.239 else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27)
43.240 end
43.241 end
43.242 @@ -699,7 +699,7 @@
43.243 else
43.244 if not(is_add r) then
43.245 let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09
43.246 - in transitive th1 (polynomial_monomial_mul_conv(concl th1))
43.247 + in Thm.transitive th1 (polynomial_monomial_mul_conv(concl th1))
43.248 end
43.249 else
43.250 let val (a,b) = dest_add l
43.251 @@ -707,8 +707,8 @@
43.252 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.253 val (tm3,tm4) = Thm.dest_comb tm1
43.254 val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4)
43.255 - val th3 = transitive th1 (combination th2 (pmul tm2))
43.256 - in transitive th3 (polynomial_add_conv (concl th3))
43.257 + val th3 = Thm.transitive th1 (Thm.combination th2 (pmul tm2))
43.258 + in Thm.transitive th3 (polynomial_add_conv (concl th3))
43.259 end
43.260 end
43.261 in fn tm =>
43.262 @@ -740,9 +740,9 @@
43.263 let val th1 = num_conv n
43.264 val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38
43.265 val (tm1,tm2) = Thm.dest_comb(concl th2)
43.266 - val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
43.267 - val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
43.268 - in transitive th4 (polynomial_mul_conv (concl th4))
43.269 + val th3 = Thm.transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2))
43.270 + val th4 = Thm.transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3
43.271 + in Thm.transitive th4 (polynomial_mul_conv (concl th4))
43.272 end
43.273 end
43.274 in fn tm =>
43.275 @@ -755,8 +755,8 @@
43.276 let val (l,r) = Thm.dest_comb tm in
43.277 if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
43.278 let val th1 = inst_thm [(cx',r)] neg_mul
43.279 - val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
43.280 - in transitive th2 (polynomial_monomial_mul_conv (concl th2))
43.281 + val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
43.282 + in Thm.transitive th2 (polynomial_monomial_mul_conv (concl th2))
43.283 end
43.284 end;
43.285
43.286 @@ -767,51 +767,52 @@
43.287 val th1 = inst_thm [(cx',l),(cy',r)] sub_add
43.288 val (tm1,tm2) = Thm.dest_comb(concl th1)
43.289 val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2)
43.290 - in transitive th1 (transitive th2 (polynomial_add_conv (concl th2)))
43.291 + in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv (concl th2)))
43.292 end;
43.293
43.294 (* Conversion from HOL term. *)
43.295
43.296 fun polynomial_conv tm =
43.297 if is_semiring_constant tm then semiring_add_conv tm
43.298 - else if not(is_comb tm) then reflexive tm
43.299 + else if not(is_comb tm) then Thm.reflexive tm
43.300 else
43.301 let val (lopr,r) = Thm.dest_comb tm
43.302 in if lopr aconvc neg_tm then
43.303 let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
43.304 - in transitive th1 (polynomial_neg_conv (concl th1))
43.305 + in Thm.transitive th1 (polynomial_neg_conv (concl th1))
43.306 end
43.307 else if lopr aconvc inverse_tm then
43.308 let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r)
43.309 - in transitive th1 (semiring_mul_conv (concl th1))
43.310 + in Thm.transitive th1 (semiring_mul_conv (concl th1))
43.311 end
43.312 else
43.313 - if not(is_comb lopr) then reflexive tm
43.314 + if not(is_comb lopr) then Thm.reflexive tm
43.315 else
43.316 let val (opr,l) = Thm.dest_comb lopr
43.317 in if opr aconvc pow_tm andalso is_numeral r
43.318 then
43.319 let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r
43.320 - in transitive th1 (polynomial_pow_conv (concl th1))
43.321 + in Thm.transitive th1 (polynomial_pow_conv (concl th1))
43.322 end
43.323 else if opr aconvc divide_tm
43.324 then
43.325 - let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l))
43.326 + let val th1 = Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l))
43.327 (polynomial_conv r)
43.328 val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
43.329 (Thm.rhs_of th1)
43.330 - in transitive th1 th2
43.331 + in Thm.transitive th1 th2
43.332 end
43.333 else
43.334 if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm
43.335 then
43.336 - let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
43.337 + let val th1 =
43.338 + Thm.combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r)
43.339 val f = if opr aconvc add_tm then polynomial_add_conv
43.340 else if opr aconvc mul_tm then polynomial_mul_conv
43.341 else polynomial_sub_conv
43.342 - in transitive th1 (f (concl th1))
43.343 + in Thm.transitive th1 (f (concl th1))
43.344 end
43.345 - else reflexive tm
43.346 + else Thm.reflexive tm
43.347 end
43.348 end;
43.349 in
43.350 @@ -852,7 +853,7 @@
43.351
43.352 fun semiring_normalize_ord_conv ctxt ord tm =
43.353 (case match ctxt tm of
43.354 - NONE => reflexive tm
43.355 + NONE => Thm.reflexive tm
43.356 | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
43.357
43.358 fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
44.1 --- a/src/Provers/Arith/fast_lin_arith.ML Sat May 15 21:41:32 2010 +0200
44.2 +++ b/src/Provers/Arith/fast_lin_arith.ML Sat May 15 21:50:05 2010 +0200
44.3 @@ -845,8 +845,8 @@
44.4 (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of
44.5 SOME spl =>
44.6 let val (ct1, ct2) = extract (cprop_of spl)
44.7 - val thm1 = assume ct1
44.8 - val thm2 = assume ct2
44.9 + val thm1 = Thm.assume ct1
44.10 + val thm2 = Thm.assume ct2
44.11 in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]),
44.12 ct2, elim_neq neqs (asms', asms@[thm2]))
44.13 end
44.14 @@ -858,8 +858,8 @@
44.15 let
44.16 val (thm1, js1) = fwdproof ss tree1 js
44.17 val (thm2, js2) = fwdproof ss tree2 js1
44.18 - val thm1' = implies_intr ct1 thm1
44.19 - val thm2' = implies_intr ct2 thm2
44.20 + val thm1' = Thm.implies_intr ct1 thm1
44.21 + val thm2' = Thm.implies_intr ct2 thm2
44.22 in (thm2' COMP (thm1' COMP thm), js2) end;
44.23 (* FIXME needs handle THM _ => NONE ? *)
44.24
44.25 @@ -869,11 +869,11 @@
44.26 val thy = ProofContext.theory_of ctxt
44.27 val nTconcl = LA_Logic.neg_prop Tconcl
44.28 val cnTconcl = cterm_of thy nTconcl
44.29 - val nTconclthm = assume cnTconcl
44.30 + val nTconclthm = Thm.assume cnTconcl
44.31 val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm])
44.32 val (Falsethm, _) = fwdproof ss tree js
44.33 val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
44.34 - val concl = implies_intr cnTconcl Falsethm COMP contr
44.35 + val concl = Thm.implies_intr cnTconcl Falsethm COMP contr
44.36 in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
44.37 (*in case concl contains ?-var, which makes assume fail:*) (* FIXME Variable.import_terms *)
44.38 handle THM _ => NONE;
45.1 --- a/src/Provers/hypsubst.ML Sat May 15 21:41:32 2010 +0200
45.2 +++ b/src/Provers/hypsubst.ML Sat May 15 21:50:05 2010 +0200
45.3 @@ -143,7 +143,7 @@
45.4 [ if inspect_pair bnd false (Data.dest_eq
45.5 (Data.dest_Trueprop (#prop (rep_thm th))))
45.6 then th RS Data.eq_reflection
45.7 - else symmetric(th RS Data.eq_reflection) (*reorient*) ]
45.8 + else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
45.9 handle TERM _ => [] | Match => [];
45.10
45.11 local
46.1 --- a/src/Tools/Compute_Oracle/compute.ML Sat May 15 21:41:32 2010 +0200
46.2 +++ b/src/Tools/Compute_Oracle/compute.ML Sat May 15 21:50:05 2010 +0200
46.3 @@ -391,9 +391,9 @@
46.4 fun export_thm thy hyps shyps prop =
46.5 let
46.6 val th = export_oracle (thy, hyps, shyps, prop)
46.7 - val hyps = map (fn h => assume (cterm_of thy h)) hyps
46.8 + val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps
46.9 in
46.10 - fold (fn h => fn p => implies_elim p h) hyps th
46.11 + fold (fn h => fn p => Thm.implies_elim p h) hyps th
46.12 end
46.13
46.14 (* --------- Rewrite ----------- *)
47.1 --- a/src/Tools/IsaPlanner/rw_inst.ML Sat May 15 21:41:32 2010 +0200
47.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML Sat May 15 21:50:05 2010 +0200
47.3 @@ -54,13 +54,13 @@
47.4
47.5 (* beta contract the theorem *)
47.6 fun beta_contract thm =
47.7 - equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
47.8 + Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
47.9
47.10 (* beta-eta contract the theorem *)
47.11 fun beta_eta_contract thm =
47.12 let
47.13 - val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
47.14 - val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
47.15 + val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
47.16 + val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
47.17 in thm3 end;
47.18
47.19
48.1 --- a/src/Tools/coherent.ML Sat May 15 21:41:32 2010 +0200
48.2 +++ b/src/Tools/coherent.ML Sat May 15 21:50:05 2010 +0200
48.3 @@ -46,8 +46,8 @@
48.4 fun rulify_elim_conv ct =
48.5 if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
48.6 else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
48.7 - (rewr_conv (symmetric Data.atomize_elimL) then_conv
48.8 - MetaSimplifier.rewrite true (map symmetric
48.9 + (rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
48.10 + MetaSimplifier.rewrite true (map Thm.symmetric
48.11 [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
48.12
48.13 end;
49.1 --- a/src/ZF/Tools/induct_tacs.ML Sat May 15 21:41:32 2010 +0200
49.2 +++ b/src/ZF/Tools/induct_tacs.ML Sat May 15 21:50:05 2010 +0200
49.3 @@ -89,7 +89,7 @@
49.4 fun exhaust_induct_tac exh ctxt var i state =
49.5 let
49.6 val thy = ProofContext.theory_of ctxt
49.7 - val (_, _, Bi, _) = dest_state (state, i)
49.8 + val (_, _, Bi, _) = Thm.dest_state (state, i)
49.9 val tn = find_tname var Bi
49.10 val rule =
49.11 if exh then #exhaustion (datatype_info thy tn)