--- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon May 20 18:38:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon May 20 20:47:33 2013 +0200
@@ -2695,8 +2695,8 @@
val in_bd_tacs = map7 (fn i => fn isNode_hsets => fn carT_def =>
fn card_of_carT => fn mor_image => fn Rep_inverse => fn mor_hsets =>
- K (mk_in_bd_tac lthy (* FIXME proper context!? *)
- (nth isNode_hsets (i - 1)) isNode_hsets carT_def
+ (fn {context = ctxt, prems = _} =>
+ mk_in_bd_tac ctxt (nth isNode_hsets (i - 1)) isNode_hsets carT_def
card_of_carT mor_image Rep_inverse mor_hsets
sbd_Cnotzero sbd_Card_order mor_Rep_thm coalgT_thm mor_T_final_thm tcoalg_thm))
ks isNode_hset_thmss carT_defs card_of_carT_thms
--- a/src/HOL/Decision_Procs/Approximation.thy Mon May 20 18:38:28 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon May 20 20:47:33 2013 +0200
@@ -3487,7 +3487,7 @@
(@{cpat "?prec::nat"}, p),
(@{cpat "?ss::nat list"}, s)])
@{thm "approx_form"}) i
- THEN simp_tac @{context} i) st
+ THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
end
| SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st]))
@@ -3531,7 +3531,7 @@
REPEAT (FIRST' [etac @{thm intervalE},
etac @{thm meta_eqE},
rtac @{thm impI}] i)
- THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
+ THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
THEN DETERM (TRY (filter_prems_tac (K false) i))
THEN DETERM (Reflection.gen_reify_tac ctxt form_equations NONE i)
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
@@ -3621,33 +3621,33 @@
|> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> snd
- fun apply_tactic context term tactic = cterm_of context term
+ fun apply_tactic ctxt term tactic =
+ cterm_of (Proof_Context.theory_of ctxt) term
|> Goal.init
|> SINGLE tactic
|> the |> prems_of |> hd
- fun prepare_form context term = apply_tactic context term (
+ fun prepare_form ctxt term = apply_tactic ctxt term (
REPEAT (FIRST' [etac @{thm intervalE}, etac @{thm meta_eqE}, rtac @{thm impI}] 1)
- THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) @{context} 1
+ THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) ctxt 1
THEN DETERM (TRY (filter_prems_tac (K false) 1)))
- fun reify_form context term = apply_tactic context term
- (Reflection.gen_reify_tac @{context} form_equations NONE 1)
+ fun reify_form ctxt term = apply_tactic ctxt term
+ (Reflection.gen_reify_tac ctxt form_equations NONE 1)
fun approx_form prec ctxt t =
realify t
- |> prepare_form (Proof_Context.theory_of ctxt)
- |> (fn arith_term =>
- reify_form (Proof_Context.theory_of ctxt) arith_term
- |> HOLogic.dest_Trueprop |> dest_interpret_form
- |> (fn (data, xs) =>
- mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
- (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
- |> approximate ctxt
- |> HOLogic.dest_list
- |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
- |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
- |> foldr1 HOLogic.mk_conj))
+ |> prepare_form ctxt
+ |> (fn arith_term => reify_form ctxt arith_term
+ |> HOLogic.dest_Trueprop |> dest_interpret_form
+ |> (fn (data, xs) =>
+ mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}
+ (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
+ |> approximate ctxt
+ |> HOLogic.dest_list
+ |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
+ |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
+ |> foldr1 HOLogic.mk_conj))
fun approx_arith prec ctxt t = realify t
|> Reflection.gen_reify ctxt form_equations
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon May 20 18:38:28 2013 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon May 20 20:47:33 2013 +0200
@@ -872,6 +872,7 @@
val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"}
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
+ val ss = simpset_of @{context}
in
fun field_isolate_conv phi ctxt vs ct = case term_of ct of
Const(@{const_name Orderings.less},_)$a$b =>
@@ -880,7 +881,7 @@
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
- (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+ (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
| Const(@{const_name Orderings.less_eq},_)$a$b =>
@@ -889,7 +890,7 @@
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
- (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+ (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
@@ -899,7 +900,7 @@
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
val nth = Conv.fconv_rule
(Conv.arg_conv (Conv.arg1_conv
- (Semiring_Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
+ (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
in rth end
| @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct