equal
deleted
inserted
replaced
90 val m = map (fn (name, _) => (name, @{typ real})) (Term.add_tvars t []) |
90 val m = map (fn (name, _) => (name, @{typ real})) (Term.add_tvars t []) |
91 val t = Term.subst_TVars m t |
91 val t = Term.subst_TVars m t |
92 in t end |
92 in t end |
93 |
93 |
94 fun apply_tactic ctxt term tactic = |
94 fun apply_tactic ctxt term tactic = |
95 Proof_Context.cterm_of ctxt term |
95 Thm.cterm_of ctxt term |
96 |> Goal.init |
96 |> Goal.init |
97 |> SINGLE tactic |
97 |> SINGLE tactic |
98 |> the |> Thm.prems_of |> hd |
98 |> the |> Thm.prems_of |> hd |
99 |
99 |
100 fun prepare_form ctxt term = apply_tactic ctxt term ( |
100 fun prepare_form ctxt term = apply_tactic ctxt term ( |
118 |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term) |
118 |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term) |
119 |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s)) |
119 |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s)) |
120 |> foldr1 HOLogic.mk_conj)) |
120 |> foldr1 HOLogic.mk_conj)) |
121 |
121 |
122 fun approx_arith prec ctxt t = realify t |
122 fun approx_arith prec ctxt t = realify t |
123 |> Proof_Context.cterm_of ctxt |
123 |> Thm.cterm_of ctxt |
124 |> Reification.conv ctxt form_equations |
124 |> Reification.conv ctxt form_equations |
125 |> Thm.prop_of |
125 |> Thm.prop_of |
126 |> Logic.dest_equals |> snd |
126 |> Logic.dest_equals |> snd |
127 |> dest_interpret |> fst |
127 |> dest_interpret |> fst |
128 |> mk_approx' prec |
128 |> mk_approx' prec |