89 |
89 |
90 fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm |
90 fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm |
91 fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) |
91 fun dest_binop ((c as Const _) $ t $ u) = (c, t, u) |
92 | dest_binop t = raise TERM ("dest_binop", [t]) |
92 | dest_binop t = raise TERM ("dest_binop", [t]) |
93 |
93 |
94 fun prove_antisym_le ctxt t = |
94 fun prove_antisym_le ctxt ct = |
95 let |
95 let |
96 val (le, r, s) = dest_binop t |
96 val (le, r, s) = dest_binop (Thm.term_of ct) |
97 val less = Const (@{const_name less}, Term.fastype_of le) |
97 val less = Const (@{const_name less}, Term.fastype_of le) |
98 val prems = Simplifier.prems_of ctxt |
98 val prems = Simplifier.prems_of ctxt |
99 in |
99 in |
100 (case find_first (eq_prop (le $ s $ r)) prems of |
100 (case find_first (eq_prop (le $ s $ r)) prems of |
101 NONE => |
101 NONE => |
103 |> Option.map (fn thm => thm RS antisym_less1) |
103 |> Option.map (fn thm => thm RS antisym_less1) |
104 | SOME thm => SOME (thm RS antisym_le1)) |
104 | SOME thm => SOME (thm RS antisym_le1)) |
105 end |
105 end |
106 handle THM _ => NONE |
106 handle THM _ => NONE |
107 |
107 |
108 fun prove_antisym_less ctxt t = |
108 fun prove_antisym_less ctxt ct = |
109 let |
109 let |
110 val (less, r, s) = dest_binop (HOLogic.dest_not t) |
110 val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct)) |
111 val le = Const (@{const_name less_eq}, Term.fastype_of less) |
111 val le = Const (@{const_name less_eq}, Term.fastype_of less) |
112 val prems = Simplifier.prems_of ctxt |
112 val prems = Simplifier.prems_of ctxt |
113 in |
113 in |
114 (case find_first (eq_prop (le $ r $ s)) prems of |
114 (case find_first (eq_prop (le $ r $ s)) prems of |
115 NONE => |
115 NONE => |
122 val basic_simpset = |
122 val basic_simpset = |
123 simpset_of (put_simpset HOL_ss @{context} |
123 simpset_of (put_simpset HOL_ss @{context} |
124 addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special |
124 addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special |
125 arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def} |
125 arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def} |
126 addsimprocs [@{simproc numeral_divmod}, |
126 addsimprocs [@{simproc numeral_divmod}, |
127 Simplifier.simproc_global @{theory} "fast_int_arith" [ |
127 Simplifier.make_simproc @{context} "fast_int_arith" |
128 "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc, |
128 {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}], |
129 Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] prove_antisym_le, |
129 proc = K Lin_Arith.simproc, identifier = []}, |
130 Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"] |
130 Simplifier.make_simproc @{context} "antisym_le" |
131 prove_antisym_less]) |
131 {lhss = [@{term "(x::'a::order) \<le> y"}], |
|
132 proc = K prove_antisym_le, identifier = []}, |
|
133 Simplifier.make_simproc @{context} "antisym_less" |
|
134 {lhss = [@{term "\<not> (x::'a::linorder) < y"}], |
|
135 proc = K prove_antisym_less, identifier = []}]) |
132 |
136 |
133 structure Simpset = Generic_Data |
137 structure Simpset = Generic_Data |
134 ( |
138 ( |
135 type T = simpset |
139 type T = simpset |
136 val empty = basic_simpset |
140 val empty = basic_simpset |