108 | dest_binop t = raise TERM ("dest_binop", [t]) |
108 | dest_binop t = raise TERM ("dest_binop", [t]) |
109 |
109 |
110 fun prove_antisym_le ctxt ct = |
110 fun prove_antisym_le ctxt ct = |
111 let |
111 let |
112 val (le, r, s) = dest_binop (Thm.term_of ct) |
112 val (le, r, s) = dest_binop (Thm.term_of ct) |
113 val less = Const (@{const_name less}, Term.fastype_of le) |
113 val less = Const (\<^const_name>\<open>less\<close>, Term.fastype_of le) |
114 val prems = Simplifier.prems_of ctxt |
114 val prems = Simplifier.prems_of ctxt |
115 in |
115 in |
116 (case find_first (eq_prop (le $ s $ r)) prems of |
116 (case find_first (eq_prop (le $ s $ r)) prems of |
117 NONE => |
117 NONE => |
118 find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems |
118 find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems |
122 handle THM _ => NONE |
122 handle THM _ => NONE |
123 |
123 |
124 fun prove_antisym_less ctxt ct = |
124 fun prove_antisym_less ctxt ct = |
125 let |
125 let |
126 val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct)) |
126 val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct)) |
127 val le = Const (@{const_name less_eq}, Term.fastype_of less) |
127 val le = Const (\<^const_name>\<open>less_eq\<close>, Term.fastype_of less) |
128 val prems = Simplifier.prems_of ctxt |
128 val prems = Simplifier.prems_of ctxt |
129 in |
129 in |
130 (case find_first (eq_prop (le $ r $ s)) prems of |
130 (case find_first (eq_prop (le $ r $ s)) prems of |
131 NONE => |
131 NONE => |
132 find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems |
132 find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems |
134 | SOME thm => SOME (thm RS antisym_le2)) |
134 | SOME thm => SOME (thm RS antisym_le2)) |
135 end |
135 end |
136 handle THM _ => NONE |
136 handle THM _ => NONE |
137 |
137 |
138 val basic_simpset = |
138 val basic_simpset = |
139 simpset_of (put_simpset HOL_ss @{context} |
139 simpset_of (put_simpset HOL_ss \<^context> |
140 addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special |
140 addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special |
141 arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def} |
141 arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def} |
142 addsimprocs [@{simproc numeral_divmod}, |
142 addsimprocs [\<^simproc>\<open>numeral_divmod\<close>, |
143 Simplifier.make_simproc @{context} "fast_int_arith" |
143 Simplifier.make_simproc \<^context> "fast_int_arith" |
144 {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}], |
144 {lhss = [\<^term>\<open>(m::int) < n\<close>, \<^term>\<open>(m::int) \<le> n\<close>, \<^term>\<open>(m::int) = n\<close>], |
145 proc = K Lin_Arith.simproc}, |
145 proc = K Lin_Arith.simproc}, |
146 Simplifier.make_simproc @{context} "antisym_le" |
146 Simplifier.make_simproc \<^context> "antisym_le" |
147 {lhss = [@{term "(x::'a::order) \<le> y"}], |
147 {lhss = [\<^term>\<open>(x::'a::order) \<le> y\<close>], |
148 proc = K prove_antisym_le}, |
148 proc = K prove_antisym_le}, |
149 Simplifier.make_simproc @{context} "antisym_less" |
149 Simplifier.make_simproc \<^context> "antisym_less" |
150 {lhss = [@{term "\<not> (x::'a::linorder) < y"}], |
150 {lhss = [\<^term>\<open>\<not> (x::'a::linorder) < y\<close>], |
151 proc = K prove_antisym_less}]) |
151 proc = K prove_antisym_less}]) |
152 |
152 |
153 structure Simpset = Generic_Data |
153 structure Simpset = Generic_Data |
154 ( |
154 ( |
155 type T = simpset |
155 type T = simpset |
231 end |
231 end |
232 in fold add steps (([], []), (ctxt, tab_empty)) end |
232 in fold add steps (([], []), (ctxt, tab_empty)) end |
233 |
233 |
234 end |
234 end |
235 |
235 |
236 fun params_of t = Term.strip_qnt_vars @{const_name Pure.all} t |
236 fun params_of t = Term.strip_qnt_vars \<^const_name>\<open>Pure.all\<close> t |
237 |
237 |
238 fun varify ctxt thm = |
238 fun varify ctxt thm = |
239 let |
239 let |
240 val maxidx = Thm.maxidx_of thm + 1 |
240 val maxidx = Thm.maxidx_of thm + 1 |
241 val vs = params_of (Thm.prop_of thm) |
241 val vs = params_of (Thm.prop_of thm) |