--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue Sep 01 17:25:36 2015 +0200
@@ -902,15 +902,6 @@
| Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
| t => Rat.rat_of_int (snd (HOLogic.dest_number t))
-fun mk_frac phi cT x =
- let val (a, b) = Rat.quotient_of_rat x
- in if b = 1 then Numeral.mk_cnumber cT a
- else Thm.apply
- (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
- (Numeral.mk_cnumber cT a))
- (Numeral.mk_cnumber cT b)
- end
-
fun whatis x ct = case Thm.term_of ct of
Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ =>
if y aconv Thm.term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
@@ -973,9 +964,10 @@
(case whatis x (Thm.dest_arg1 ct) of
("c*x+t",[c,t]) =>
let
- val T = Thm.ctyp_of_cterm x
+ val T = Thm.typ_of_cterm x
+ val cT = Thm.ctyp_of_cterm x
val cr = dest_frac c
- val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
+ val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
val cthp = Simplifier.rewrite ctxt
@@ -983,7 +975,7 @@
(if neg then Thm.apply (Thm.apply clt c) cz
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
- val th = Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [c,x,t])
+ val th = Thm.implies_elim (Thm.instantiate' [SOME cT] (map SOME [c,x,t])
(if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
@@ -997,9 +989,10 @@
in rth end
| ("c*x",[c]) =>
let
- val T = Thm.ctyp_of_cterm x
+ val T = Thm.typ_of_cterm x
+ val cT = Thm.ctyp_of_cterm x
val cr = dest_frac c
- val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"}
+ val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool}))
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
val cthp = Simplifier.rewrite ctxt
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Tue Sep 01 17:25:36 2015 +0200
@@ -206,7 +206,7 @@
val pcv = Simplifier.rewrite (put_simpset ss' ctxt);
val postcv = Simplifier.rewrite (put_simpset ss ctxt);
val nnf = K (nnf_conv ctxt then_conv postcv)
- val qe_conv = Qelim.gen_qelim_conv pcv postcv pcv cons (Drule.cterm_add_frees tm [])
+ val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Drule.cterm_add_frees tm [])
(isolate_conv ctxt) nnf
(fn vs => ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt,
whatis = whatis, simpset = ss}) vs
--- a/src/HOL/Decision_Procs/langford.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Tue Sep 01 17:25:36 2015 +0200
@@ -190,7 +190,7 @@
addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
in
fn p =>
- Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
+ Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons
(Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive)
(K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
end;
@@ -228,12 +228,12 @@
(_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm])
| (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
-fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
+fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
let
- fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
- fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
- val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
- val p' = fold_rev gen ts p
+ fun all x t =
+ Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
+ val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
+ val p' = fold_rev all ts p
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
fun cfrees ats ct =
@@ -259,7 +259,7 @@
Object_Logic.full_atomize_tac ctxt i THEN
simp_tac (put_simpset ss ctxt) i
THEN (CONVERSION Thm.eta_long_conversion) i
- THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
+ THEN (TRY o generalize_tac ctxt (cfrees (#atoms instance))) i
THEN Object_Logic.full_atomize_tac ctxt i
THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
THEN (simp_tac (put_simpset ss ctxt) i)));
--- a/src/HOL/Library/positivstellensatz.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Tue Sep 01 17:25:36 2015 +0200
@@ -514,14 +514,15 @@
| _ => "x"
fun mk_forall x th =
- Drule.arg_cong_rule
- (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" })
- (Thm.abstract_rule (name_of x) x th)
+ let
+ val T = Thm.typ_of_cterm x
+ val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool}))
+ in Drule.arg_cong_rule all (Thm.abstract_rule (name_of x) x th) end
val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
- fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
- fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
+ fun ext T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool}))
+ fun mk_ex v t = Thm.apply (ext (Thm.typ_of_cterm v)) (Thm.lambda v t)
fun choose v th th' =
case Thm.concl_of th of
--- a/src/HOL/Multivariate_Analysis/normarith.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Tue Sep 01 17:25:36 2015 +0200
@@ -343,8 +343,14 @@
val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
- fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
- fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r
+ fun mk_norm t =
+ let val T = Thm.typ_of_cterm t
+ in Thm.apply (Thm.cterm_of ctxt' (Const (@{const_name norm}, T --> @{typ real}))) t end
+ fun mk_equals l r =
+ let
+ val T = Thm.typ_of_cterm l
+ val eq = Thm.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT))
+ in Thm.apply (Thm.apply eq l) r end
val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Thm.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns
val replace_conv = try_conv (rewrs_conv asl)
val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Sep 01 17:25:36 2015 +0200
@@ -569,7 +569,7 @@
[not_all, all_not_ex, @{thm ex_disj_distrib}]));
fun conv ctxt p =
- Qelim.gen_qelim_conv
+ Qelim.gen_qelim_conv ctxt
(Simplifier.rewrite (put_simpset conv_ss ctxt))
(Simplifier.rewrite (put_simpset presburger_ss ctxt))
(Simplifier.rewrite (put_simpset conv_ss ctxt))
@@ -799,12 +799,12 @@
in h [] ct end
end;
-fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
+fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
let
- fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"}
- fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t)
- val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
- val p' = fold_rev gen ts p
+ fun all x t =
+ Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
+ val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
+ val p' = fold_rev all ts p
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
local
@@ -875,7 +875,7 @@
THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW simp_tac simpset_ctxt
- THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
+ THEN_ALL_NEW (TRY o generalize_tac ctxt (int_nat_terms ctxt))
THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
--- a/src/HOL/Tools/Qelim/qelim.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML Tue Sep 01 17:25:36 2015 +0200
@@ -6,7 +6,7 @@
signature QELIM =
sig
- val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a ->
+ val gen_qelim_conv: Proof.context -> conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a ->
('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
val standard_qelim_conv: Proof.context ->
(cterm list -> conv) -> (cterm list -> conv) ->
@@ -18,7 +18,7 @@
val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
-fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =
+fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv =
let
fun conv env p =
case Thm.term_of p of
@@ -41,10 +41,10 @@
in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
else Thm.transitive (Thm.transitive th th') (conv env r) end
| Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
- | Const(@{const_name All},_)$_ =>
+ | Const(@{const_name All}, allT)$_ =>
let
+ val T = Thm.ctyp_of ctxt (#1 (Term.dest_funT (#1 (Term.dest_funT allT))))
val p = Thm.dest_arg p
- val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p)
val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
in Thm.transitive th (conv env (Thm.rhs_of th))
end
@@ -65,7 +65,7 @@
fun standard_qelim_conv ctxt atcv ncv qcv p =
let val pcv = pcv ctxt
- in gen_qelim_conv pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
+ in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end
end;
--- a/src/HOL/Tools/Transfer/transfer.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Tue Sep 01 17:25:36 2015 +0200
@@ -709,7 +709,8 @@
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
- val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
+ val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), @{typ bool})))
+ val thm3 = Goal.prove_internal ctxt' [] goal (K tac)
val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
in
thm3
@@ -746,7 +747,8 @@
(SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
handle TERM (_, ts) => raise TERM (err_msg, ts)
- val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
+ val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), @{typ bool})))
+ val thm3 = Goal.prove_internal ctxt' [] goal (K tac)
val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
in
thm3
--- a/src/HOL/Tools/groebner.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Tools/groebner.ML Tue Sep 01 17:25:36 2015 +0200
@@ -478,8 +478,8 @@
(* Conversion for the equivalence of existential statements where
EX quantifiers are rearranged differently *)
- fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex}
- fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t)
+fun ext ctxt T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool}))
+fun mk_ex ctxt v t = Thm.apply (ext ctxt (Thm.typ_of_cterm v)) (Thm.lambda v t)
fun choose v th th' = case Thm.concl_of th of
@{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
@@ -494,8 +494,8 @@
in Thm.implies_elim (Thm.implies_elim th0 th) th1 end
| _ => error "" (* FIXME ? *)
-fun simple_choose v th =
- choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
+fun simple_choose ctxt v th =
+ choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex ctxt v)
(Thm.dest_arg (hd (Thm.chyps_of th))))) th
@@ -507,14 +507,14 @@
(Thm.instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI}))
th
end
- fun ex_eq_conv t =
+ fun ex_eq_conv ctxt t =
let
val (p0,q0) = Thm.dest_binop t
val (vs',P) = strip_exists p0
val (vs,_) = strip_exists q0
val th = Thm.assume (Thm.apply @{cterm Trueprop} P)
- val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th))
- val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
+ val th1 = implies_intr_hyps (fold (simple_choose ctxt) vs' (fold mkexi vs th))
+ val th2 = implies_intr_hyps (fold (simple_choose ctxt) vs (fold mkexi vs' th))
val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1
val q = (Thm.dest_arg o Thm.dest_arg o Thm.cprop_of) th1
in Thm.implies_elim (Thm.implies_elim (Thm.instantiate' [] [SOME p, SOME q] iffI) th1) th2
@@ -527,7 +527,7 @@
| Var ((s,_),_) => s
| _ => "x"
fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
- fun mk_exists v th = Drule.arg_cong_rule (ext (Thm.ctyp_of_cterm v))
+ fun mk_exists ctxt v th = Drule.arg_cong_rule (ext ctxt (Thm.typ_of_cterm v))
(Thm.abstract_rule (getname v) v th)
fun simp_ex_conv ctxt =
Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
@@ -738,9 +738,10 @@
fun ring ctxt tm =
let
fun mk_forall x p =
- Thm.apply
- (Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] [])
- @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
+ let
+ val T = Thm.typ_of_cterm x;
+ val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool}))
+ in Thm.apply all (Thm.lambda x p) end
val avs = Drule.cterm_add_frees tm []
val P' = fold mk_forall avs tm
val th1 = initial_conv ctxt (mk_neg P')
@@ -829,9 +830,9 @@
(Drule.binop_cong_rule @{cterm HOL.conj} th1
(Thm.reflexive (Thm.dest_arg (Thm.rhs_of th2))))
val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
- val th4 = Conv.fconv_rule (Conv.arg_conv (simp_ex_conv ctxt)) (mk_exists v th3)
- val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4)))
- in Thm.transitive th5 (fold mk_exists (remove op aconvc v vars) th4)
+ val th4 = Conv.fconv_rule (Conv.arg_conv (simp_ex_conv ctxt)) (mk_exists ctxt v th3)
+ val th5 = ex_eq_conv ctxt (mk_eq tm (fold (mk_ex ctxt) (remove op aconvc v vars) (Thm.lhs_of th4)))
+ in Thm.transitive th5 (fold (mk_exists ctxt) (remove op aconvc v vars) th4)
end;
end
--- a/src/HOL/Tools/semiring_normalizer.ML Mon Aug 31 22:45:40 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Tue Sep 01 17:25:36 2015 +0200
@@ -123,6 +123,9 @@
Simplifier.rewrite (put_simpset semiring_norm_ss ctxt)
then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_1_eq_1}))};
+val divide_const = Thm.cterm_of @{context} (Logic.varify_global @{term "op /"});
+val [divide_tvar] = Term.add_tvars (Thm.term_of divide_const) [];
+
val field_funs =
let
fun numeral_is_const ct =
@@ -142,7 +145,7 @@
let val (a, b) = Rat.quotient_of_rat x
in if b = 1 then Numeral.mk_cnumber cT a
else Thm.apply
- (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"})
+ (Thm.apply (Thm.instantiate_cterm ([(divide_tvar, cT)], []) divide_const)
(Numeral.mk_cnumber cT a))
(Numeral.mk_cnumber cT b)
end