# HG changeset patch # User wenzelm # Date 1369075653 -7200 # Node ID ff1ec795604b2d411a3fa7275f9a3a6fe4c65481 # Parent 6ce832f71bdd51ac638bc4beed812e1e925afa6f proper context; diff -r 6ce832f71bdd -r ff1ec795604b src/HOL/BNF/Tools/bnf_gfp.ML --- 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 diff -r 6ce832f71bdd -r ff1ec795604b src/HOL/Decision_Procs/Approximation.thy --- 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 \ real set \ 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 \ real set \ 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 diff -r 6ce832f71bdd -r ff1ec795604b src/HOL/Decision_Procs/Dense_Linear_Order.thy --- 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