File ‹order.ML›
val TY_NAT_ORDER = "NAT_ORDER"
signature NAT_ORDER =
sig
val is_order: term -> bool
val is_plus_const: term -> bool
val is_minus_const: term -> bool
val is_standard_ineq: term -> bool
val dest_ineq: term -> term * term * int
val dest_ineq_th: thm -> term * term * int
val fold_double_plus: conv
val norm_ineq_th': thm -> thm
val convert_const_x: thm -> thm
val convert_const_y: thm -> thm
val norm_ineq_th: thm -> thm
val norm_ineq_minus_th': thm -> thm option
val norm_ineq_minus_th: thm -> thm option
datatype order_type =
LESS | LESS_LMINUS | LESS_LPLUS | LESS_RMINUS | LESS_RPLUS |
LE | LE_LMINUS | LE_LPLUS | LE_RMINUS | LE_RPLUS
type order_info
val to_normal_th: order_type -> thm -> thm
val th_to_ritem: thm -> raw_item
val th_to_normed_ritems: thm -> raw_item list
val nat_order_normalizer: Auto2_Setup.Normalizer.normalizer
val nat_eq_diff_prfstep: proofstep
val get_nat_order_info: box_item -> order_info
val nat_order_typed_matcher: item_matcher
val transitive: proofstep
val transitive_resolve: proofstep
val single_resolve: proofstep
val single_resolve_zero: proofstep
val nat_order_match: term -> box_item -> Proof.context -> id_inst ->
id_inst_th list
val nat_order_matcher: item_matcher
val nat_order_noteq_matcher: item_matcher
val nat_order_single_match: term -> box_item -> Proof.context -> id_inst ->
id_inst_th list
val nat_order_single_matcher: item_matcher
val shadow_nat_order_prfstep: proofstep
val shadow_nat_order_single: proofstep
val string_of_nat_order: Proof.context -> term * term * int * thm -> string
val output_nat_order: Proof.context -> term list * thm -> string
val shadow_nat_order: Proof.context -> box_id -> term list * cterm list -> bool
val add_nat_order_proofsteps: theory -> theory
end;
structure Nat_Order : NAT_ORDER =
struct
val is_numc = UtilArith.is_numc
val dest_numc = UtilArith.dest_numc
val nat0 = Nat_Util.nat0
val nat_less_th = Nat_Util.nat_less_th
val nat_fold_conv0_right =
Conv.try_conv (rewr_obj_eq @{thm Nat.add_0_right})
val nat_fold_conv0_left =
Conv.try_conv (rewr_obj_eq @{thm Nat.plus_nat.add_0})
fun is_less t =
case t of Const (@{const_name less}, _) $ _ $ _ => true
| _ => false
fun is_less_eq t =
case t of Const (@{const_name less_eq}, _) $ _ $ _ => true
| _ => false
fun is_order t = is_less t orelse is_less_eq t
datatype order_type =
LESS_LMINUS | LESS_LPLUS | LESS_RMINUS | LESS_RPLUS | LESS |
LE_LMINUS | LE_LPLUS | LE_RMINUS | LE_RPLUS | LE
fun is_plus_const t =
UtilArith.is_plus t andalso UtilArith.is_numc (dest_arg t)
fun is_minus_const t =
UtilArith.is_minus t andalso UtilArith.is_numc (dest_arg t)
fun is_standard_ineq t =
if is_less_eq t then
let
val (lhs, rhs) = Util.dest_binop_args t
in
fastype_of lhs = natT andalso
((is_plus_const lhs andalso not (is_plus_const rhs) andalso
UtilArith.dest_numc (dest_arg lhs) > 0) orelse
(is_plus_const rhs andalso not (is_plus_const lhs)))
end
else false
fun dest_ineq t =
let
val _ = assert (is_standard_ineq t) "dest_ineq"
val (lhs, rhs) = Util.dest_binop_args t
in
if is_plus_const lhs then
(dest_arg1 lhs, rhs, ~ (UtilArith.dest_numc (dest_arg lhs)))
else
(lhs, dest_arg1 rhs, UtilArith.dest_numc (dest_arg rhs))
end
fun dest_ineq_th th =
if Auto2_Setup.UtilLogic.is_Trueprop (Thm.prop_of th) andalso
is_standard_ineq (prop_of' th) then
dest_ineq (prop_of' th)
else let
val _ = trace_thm_global "th:" th
in
raise Fail "dest_ineq_th"
end
val fold_const_left =
apply_to_thm' (Conv.arg1_conv (Conv.arg_conv Nat_Util.nat_fold_conv))
val fold_const_right =
apply_to_thm' (Conv.arg_conv (Conv.arg_conv Nat_Util.nat_fold_conv))
fun fold_double_plus ct =
let
val t = Thm.term_of ct
in
if is_plus_const t andalso is_plus_const (dest_arg1 t) then
Conv.every_conv [rewr_obj_eq @{thm add_ac(1)},
Conv.arg_conv Nat_Util.nat_fold_conv,
fold_double_plus] ct
else
Conv.all_conv ct
end
fun norm_ineq_th' th =
let
val t = prop_of' th
val _ = assert (is_less_eq t orelse is_less t) "norm_ineq_th"
val (lhs, rhs) = Util.dest_binop_args t
val try_fold0 = Conv.try_conv (Conv.arg_conv nat_fold_conv0_right)
in
if is_less_eq t then
if is_plus_const lhs andalso is_plus_const rhs then
let
val (lhs, rhs) = Util.dest_binop_args t
val (n1, n2) = apply2 (UtilArith.dest_numc o dest_arg) (lhs, rhs)
in
if n1 <= n2 then
(th RS @{thm reduce_le_plus_consts}) |> fold_const_right
else
([Nat_Util.nat_le_th n2 n1, th]
MRS @{thm reduce_le_plus_consts'}) |> fold_const_left
end
else if is_plus_const lhs then
if UtilArith.dest_numc (dest_arg lhs) = 0 then
th RS @{thm norm_le_lplus0}
else th
else if is_plus_const rhs then th
else if is_minus_const lhs then
th RS @{thm norm_le_lminus}
else if is_minus_const rhs then
th RS @{thm norm_le_rminus}
else
th RS @{thm norm_le}
else
if is_plus_const lhs andalso is_plus_const rhs then
let
val (lhs, rhs) = Util.dest_binop_args t
val (n1, n2) = apply2 (UtilArith.dest_numc o dest_arg) (lhs, rhs)
in
if n1 <= n2 then
(th RS @{thm reduce_less_plus_consts}) |> fold_const_right
|> apply_to_thm' try_fold0
|> norm_ineq_th'
else
([Nat_Util.nat_le_th n2 n1, th]
MRS @{thm reduce_less_plus_consts'}) |> fold_const_left
|> norm_ineq_th'
end
else if is_plus_const lhs then
(th RS @{thm norm_less_lplus}) |> fold_const_left
else if is_plus_const rhs then
(th RS @{thm norm_less_rplus}) |> fold_const_right
else if is_minus_const lhs then
(th RS @{thm norm_less_lminus}) |> fold_const_right
else if is_minus_const rhs then
(th RS @{thm norm_less_rminus}) |> fold_const_left
else
th RS @{thm norm_less}
end
fun convert_const_x th =
let
val (x, _, d) = dest_ineq_th th
in
if UtilArith.is_numc x then
let
val xn = UtilArith.dest_numc x
in
if xn = 0 then th
else if d < 0 then
(th RS @{thm cv_const1}) |> fold_const_left
else if d - xn < 0 then
(th RS @{thm cv_const4}) |> fold_const_left
else
(th RS @{thm cv_const5}) |> fold_const_right
end
else th
end
fun convert_const_y th =
let
val (_, y, d) = dest_ineq_th th
in
if UtilArith.is_numc y then
let
val yn = UtilArith.dest_numc y
in
if yn = 0 then th
else if d < 0 andalso yn + d >= 0 then
(th RS @{thm cv_const2}) |> fold_const_right
else if d < 0 andalso yn + d < 0 then
([Nat_Util.nat_less_th yn (~d), th] MRS @{thm cv_const3})
|> fold_const_left
else
(th RS @{thm cv_const6}) |> fold_const_right
end
else th
end
fun norm_ineq_th th =
let
val th' =
th |> apply_to_thm' (Conv.arg1_conv fold_double_plus)
|> apply_to_thm' (Conv.arg_conv fold_double_plus)
|> norm_ineq_th' |> convert_const_x |> convert_const_y
in
if is_standard_ineq (prop_of' th') then th'
else let
val _ = trace_thm_global "th':" th'
in
raise Fail "norm_ineq_th: invalid output."
end
end
fun norm_ineq_minus_th' th =
let
val t = prop_of' th
val _ = assert (is_less_eq t orelse is_less t) "norm_ineq_minus_th"
val (lhs, rhs) = Util.dest_binop_args t
in
if is_less_eq t then
if is_minus_const lhs andalso not (is_plus_const rhs) then
SOME (th RS @{thm norm_le})
else if is_minus_const rhs andalso not (is_plus_const lhs) then
SOME (th RS @{thm norm_le})
else NONE
else
if is_minus_const lhs andalso not (is_plus_const rhs) then
SOME (th RS @{thm norm_less})
else if is_minus_const rhs andalso not (is_plus_const lhs) then
SOME (th RS @{thm norm_less})
else NONE
end
fun norm_ineq_minus_th th =
case norm_ineq_minus_th' th of
NONE => NONE
| SOME th' =>
let
val th'' = th' |> convert_const_x |> convert_const_y
in
if is_standard_ineq (prop_of' th'') then SOME th''
else let
val _ = trace_thm_global "th'':" th''
in
raise Fail "norm_ineq_minus_th: invalid output."
end
end
type order_info = cterm * cterm * int * thm
fun to_normal_th order_ty th =
case order_ty of
LESS_LMINUS => (th RS @{thm norm_less_lminus}) |> fold_const_right
| LESS_LPLUS => (th RS @{thm norm_less_lplus}) |> fold_const_left
| LESS_RMINUS => (th RS @{thm norm_less_rminus}) |> fold_const_left
| LESS_RPLUS => (th RS @{thm norm_less_rplus}) |> fold_const_right
| LESS => th RS @{thm norm_less}
| LE_LMINUS => th RS @{thm norm_le_lminus}
| LE_RMINUS => th RS @{thm norm_le_rminus}
| LE => th RS @{thm norm_le}
| LE_LPLUS =>
if UtilArith.dest_numc (dest_arg (dest_arg1 (prop_of' th))) = 0 then
th RS @{thm norm_le_lplus0}
else th
| _ => th
fun rewrite_info_x eq_x (cx, cy, diff, th) =
let
val _ = assert (Thm.lhs_of eq_x aconvc cx)
"rewrite_info_x: invalid equality."
val th' =
if diff >= 0 then
th |> apply_to_thm' (Conv.arg1_conv (Conv.rewr_conv eq_x))
else
th |> apply_to_thm' (Conv.arg1_conv (
Conv.arg1_conv (Conv.rewr_conv eq_x)))
in
(Thm.rhs_of eq_x, cy, diff, th')
end
fun rewrite_info_y eq_y (cx, cy, diff, th) =
let
val _ = assert (Thm.lhs_of eq_y aconvc cy)
"rewrite_info_y: invalid equality."
val th' =
if diff >= 0 then
th |> apply_to_thm' (Conv.arg_conv (
Conv.arg1_conv (Conv.rewr_conv eq_y)))
else
th |> apply_to_thm' (Conv.arg_conv (Conv.rewr_conv eq_y))
in
(cx, Thm.rhs_of eq_y, diff, th')
end
fun th_to_ritem th =
let
val (x, y, n) = dest_ineq_th th
in
Fact (TY_NAT_ORDER, [x, y, mk_int n], th)
end
fun th_to_normed_ritems th =
let
val th' = norm_ineq_th th
val minus_th = the_list (norm_ineq_minus_th th)
in
map th_to_ritem (th' :: minus_th)
end
fun nat_order_normalizer _ ritem =
case ritem of
Handler _ => [ritem]
| Fact (ty_str, _, th) =>
if ty_str <> TY_PROP then [ritem]
else if is_order (prop_of' th) andalso
fastype_of (dest_arg (prop_of' th)) = natT then
th_to_normed_ritems th
else [ritem]
val nat_eq_diff_prfstep =
Auto2_Setup.ProofStep.prfstep_custom
"nat_eq_diff"
[WithItem (TY_EQ, @{term_pat "(?x::nat) = ?y"})]
(fn ((id, _), _) => fn items => fn _ =>
let
val {prop, ...} = the_single items
val (lhs, rhs) = prop |> prop_of' |> Util.dest_binop_args
in
if is_plus_const lhs orelse is_plus_const rhs orelse
is_numc lhs orelse is_numc rhs then
let
val prop' = to_meta_eq prop
val ths = (prop' RS @{thm eq_to_ineqs})
|> Auto2_Setup.UtilLogic.split_conj_th
in
[AddItems {id = id, sc = NONE,
raw_items = maps th_to_normed_ritems ths}]
end
else []
end)
fun get_nat_order_info {tname, prop, ...} =
let
val (cx, cy, cdiff_t) = the_triple tname
in
(cx, cy, dest_numc (Thm.term_of cdiff_t), prop)
end
val nat_order_typed_matcher =
let
fun pre_match pat {tname, ...} ctxt =
Auto2_Setup.Matcher.pre_match_head
ctxt (pat, Thm.cterm_of ctxt (HOLogic.mk_tuple (map Thm.term_of tname)))
fun match pat (item as {tname = cts, ...}) ctxt (id, inst) =
let
val pats = HOLogic.strip_tuple pat
val insts' = Auto2_Setup.Matcher.rewrite_match_list
ctxt (map (pair false) (pats ~~ cts)) (id, inst)
fun process_inst (inst, ths) =
let
val (eq_x, eq_y, eq_n) = the_triple ths
in
if Thm.is_reflexive eq_n then
let
val (_, _, _, prop) =
item |> get_nat_order_info
|> rewrite_info_x (meta_sym eq_x)
|> rewrite_info_y (meta_sym eq_y)
in
[(inst, prop)]
end
else []
end
in
maps process_inst insts'
end
in
{pre_match = pre_match, match = match}
end
fun order_trans th1 th2 =
let
val (_, y1, d1) = dest_ineq_th th1
val (x2, _, d2) = dest_ineq_th th2
val _ = assert (y1 aconv x2) "order_trans"
in
if d1 < 0 andalso d2 < 0 then
([th1, th2] MRS @{thm trans1}) |> fold_const_left
else if d1 >= 0 andalso d2 >= 0 then
([th1, th2] MRS @{thm trans2}) |> fold_const_right
else if d1 < 0 andalso d2 >= 0 then
if d2 >= (~d1) then
([th1, th2] MRS @{thm trans3}) |> fold_const_right
else
([Nat_Util.nat_less_th d2 (~d1), th1, th2] MRS @{thm trans4})
|> fold_const_left
else
if d1 >= (~d2) then
([th1, th2] MRS @{thm trans5}) |> fold_const_right
else
([Nat_Util.nat_less_th d1 (~d2), th1, th2] MRS @{thm trans6})
|> fold_const_left
end
val transitive =
Auto2_Setup.ProofStep.prfstep_custom
"nat_order_transitive"
[WithItem (TY_NAT_ORDER, @{term_pat "(?x, ?y, ?m)"}),
WithItem (TY_NAT_ORDER, @{term_pat "(?y, ?z, ?n)"}),
Filter (neq_filter @{term_pat "?x ~= ?y"}),
Filter (neq_filter @{term_pat "?y ~= ?z"}),
Filter (neq_filter @{term_pat "?x ~= ?z"})]
(fn ((id, _), ths) => fn _ => fn _ =>
let
val (th1, th2) = the_pair ths
val item' = th_to_ritem (order_trans th1 th2)
in
[AddItems {id = id, sc = NONE, raw_items = [item']}]
end)
fun order_trans_resolve th1 th2 =
let
val (_, _, d1) = dest_ineq_th th1
val (_, _, d2) = dest_ineq_th th2
in
if d1 < 0 andalso d2 < 0 then
[nat_less_th 0 (~d1), th1, th2] MRS @{thm trans_resolve1}
else if d1 < 0 andalso d2 >= 0 then
[nat_less_th d2 (~d1), th1, th2] MRS @{thm trans_resolve2}
else
[nat_less_th d1 (~d2), th2, th1] MRS @{thm trans_resolve2}
end
val transitive_resolve =
Auto2_Setup.ProofStep.prfstep_custom
"nat_order_transitive_resolve"
[WithItem (TY_NAT_ORDER, @{term_pat "(?x, ?y, ?m)"}),
WithItem (TY_NAT_ORDER, @{term_pat "(?y, ?x, ?n)"})]
(fn ((id, inst), ths) => fn _ => fn _ =>
let
val m = dest_numc (lookup_inst inst "m")
val n = dest_numc (lookup_inst inst "n")
val (th1, th2) = the_pair ths
val fold0 = apply_to_thm' (Conv.arg_conv nat_fold_conv0_right)
val try_fold0l = Conv.try_conv nat_fold_conv0_left
val res_ths =
if m + n < 0 then [order_trans_resolve th1 th2]
else if m = 0 andalso n = 0 then
[(map fold0 [th1, th2]) MRS @{thm Orderings.order_antisym}]
else if m + n = 0 then
[([th1, th2] MRS @{thm Orderings.order_antisym})
|> apply_to_thm' (Conv.arg_conv try_fold0l)
|> apply_to_thm' (Conv.arg1_conv try_fold0l)]
else []
in
map (fn th => Auto2_Setup.Update.thm_update (id, th)) res_ths
end)
val single_resolve =
Auto2_Setup.ProofStep.prfstep_custom
"nat_order_single_resolve"
[WithItem (TY_NAT_ORDER, @{term_pat "(?x, ?x, ?n)"})]
(fn ((id, inst), ths) => fn _ => fn _ =>
let
val n = dest_numc (lookup_inst inst "n")
val th = the_single ths
in
if n < 0 then
[Auto2_Setup.Update.thm_update (
id, [nat_less_th 0 (~n), th] MRS @{thm single_resolve})]
else []
end)
val single_resolve_zero =
Auto2_Setup.ProofStep.prfstep_custom
"nat_order_single_resolve_zero"
[WithItem (TY_NAT_ORDER, @{term_pat "(?x, 0, ?n)"})]
(fn ((id, inst), ths) => fn _ => fn _ =>
let
val n = dest_numc (lookup_inst inst "n")
val th = the_single ths
in
if n < 0 then
[Auto2_Setup.Update.thm_update (id, [nat_less_th 0 (~n), th]
MRS @{thm single_resolve_const})]
else []
end)
fun valid_type ctxt ty =
case ty of
TVar _ => Sign.of_sort (Proof_Context.theory_of ctxt)
(ty, ["Orderings.linorder"])
| _ => (ty = natT)
fun valid_arg_type ctxt t =
valid_type ctxt (fastype_of (dest_arg t))
fun is_order_pat ctxt pat =
(is_order pat andalso valid_arg_type ctxt pat) orelse
(is_order (get_neg pat) andalso valid_arg_type ctxt (get_neg pat))
val less_nat = @{term "(<)::nat => nat => bool"}
val le_nat = @{term "(<=)::nat => nat => bool"}
fun get_neg_order t =
if is_neg t then dest_not t
else if is_less t then le_nat $ dest_arg t $ dest_arg1 t
else if is_less_eq t then less_nat $ dest_arg t $ dest_arg1 t
else raise Fail "get_neg_order"
fun is_plus_const_gen t =
is_plus_const t orelse (is_numc t andalso not (t aconv nat0))
fun plus_const_of_gen t =
if is_plus_const t then dest_arg1 t else nat0
fun rewr_side eq_th ct =
if Thm.lhs_of eq_th aconvc ct then
Conv.rewr_conv eq_th ct
else if is_numc (Thm.term_of ct) then
Conv.every_conv [rewr_obj_eq (obj_sym @{thm Nat.plus_nat.add_0}),
Conv.arg1_conv (Conv.rewr_conv eq_th)] ct
else
Conv.arg1_conv (Conv.rewr_conv eq_th) ct
fun analyze_pattern t =
let
val (lhs, rhs) = Util.dest_binop_args t
in
if is_plus_const_gen lhs then
(plus_const_of_gen lhs, rhs,
if is_less t then LESS_LPLUS else LE_LPLUS)
else if is_plus_const_gen rhs then
(lhs, plus_const_of_gen rhs,
if is_less t then LESS_RPLUS else LE_RPLUS)
else if is_minus_const lhs then
(dest_arg1 lhs, rhs,
if is_less t then LESS_LMINUS else LE_LMINUS)
else if is_minus_const rhs then
(lhs, dest_arg1 rhs,
if is_less t then LESS_RMINUS else LE_RMINUS)
else
(lhs, rhs, if is_less t then LESS else LE)
end
fun analyze_pattern2 t =
let
val (lhs, rhs) = Util.dest_binop_args t
in
if is_minus_const lhs andalso not (is_plus_const_gen rhs) then
SOME (lhs, rhs, if is_less t then LESS else LE)
else if is_minus_const rhs andalso not (is_plus_const_gen lhs) then
SOME (lhs, rhs, if is_less t then LESS else LE)
else NONE
end
fun find_contradiction_item pat item ctxt (id, inst) =
let
val (x, y, d1, th1) = get_nat_order_info item
fun process_pattern (pat_l, pat_r, order_ty) =
let
val pairs = [(false, (pat_l, y)), (false, (pat_r, x))]
in
map (pair order_ty)
(Auto2_Setup.Matcher.rewrite_match_list ctxt pairs (id, inst))
end
val insts = process_pattern (analyze_pattern pat)
val insts2 = case analyze_pattern2 pat of
NONE => [] | SOME pattern => process_pattern pattern
fun process_inst (order_ty, ((id', inst'), eq_ths)) =
let
val (eq_th1, eq_th2) = the_pair eq_ths
val assum = pat |> Util.subst_term_norm inst'
|> mk_Trueprop |> Thm.cterm_of ctxt
val th2 = assum |> Thm.assume
|> apply_to_thm' (Conv.arg1_conv (rewr_side eq_th1))
|> apply_to_thm' (Conv.arg_conv (rewr_side eq_th2))
|> to_normal_th order_ty
val (_, _, d2) = dest_ineq_th th2
in
if d1 + d2 < 0 then
[((id', inst'),
(order_trans_resolve th1 th2)
|> Thm.implies_intr assum
|> apply_to_thm Auto2_Setup.UtilLogic.rewrite_from_contra_form)]
else []
end
in
maps process_inst (insts @ insts2)
end
fun nat_order_match pat item ctxt (id, inst) =
if not (is_order_pat ctxt pat) then [] else
let
val is_neg = is_neg pat
val neg_pat = get_neg_order pat
val res = find_contradiction_item neg_pat item ctxt (id, inst)
in
if is_neg then res
else res |> map (apsnd (apply_to_thm' UtilArith.neg_ineq_cv))
end
fun nat_order_pre_match pat item ctxt =
if not (is_order_pat ctxt pat) then false else
let
val neg_pat = get_neg_order pat
val (x, y, _, _) = get_nat_order_info item
fun process_pattern (pat_l, pat_r, _) =
Auto2_Setup.Matcher.pre_match ctxt (pat_l, y) andalso
Auto2_Setup.Matcher.pre_match ctxt (pat_r, x)
val match1 = process_pattern (analyze_pattern neg_pat)
val match2 = case analyze_pattern2 neg_pat of
NONE => false | SOME pattern => process_pattern pattern
in
match1 orelse match2
end
val nat_order_matcher =
{pre_match = nat_order_pre_match, match = nat_order_match}
val nat_order_noteq_matcher =
let
fun get_insts pat item ctxt (id, inst) =
if not (is_neg pat andalso is_eq_term (dest_not pat)) then ([], [])
else let
val (A, B) = pat |> dest_not |> dest_eq
val (cx, cy, n, _) = get_nat_order_info item
in
if n >= 0 then ([], [])
else (Auto2_Setup.Matcher.rewrite_match_list
ctxt [(false, (A, cx)), (false, (B, cy))] (id, inst),
Auto2_Setup.Matcher.rewrite_match_list
ctxt [(false, (B, cx)), (false, (A, cy))] (id, inst))
end
fun pre_match pat item ctxt =
if not (is_neg pat andalso is_eq_term (dest_not pat)) then false
else let
val (A, B) = pat |> dest_not |> dest_eq
val (cx, cy, n, _) = get_nat_order_info item
in
n < 0 andalso ((Auto2_Setup.Matcher.pre_match ctxt (A, cx) andalso
Auto2_Setup.Matcher.pre_match ctxt (B, cy)) orelse
(Auto2_Setup.Matcher.pre_match ctxt (A, cy) andalso
Auto2_Setup.Matcher.pre_match ctxt (A, cx)))
end
fun match pat item ctxt (id, inst) =
if Util.has_vars pat then [] else
let
val (instAB, instBA) = get_insts pat item ctxt (id, inst)
fun process_inst (inst', ths) =
let
val (eq_x, eq_y) = the_pair ths
val (_, _, n, prop) = item |> get_nat_order_info
|> rewrite_info_x (meta_sym eq_x)
|> rewrite_info_y (meta_sym eq_y)
in
(inst', [prop, nat_less_th 0 (~n)]
MRS @{thm nat_ineq_impl_not_eq})
end
fun switch_ineq (inst', th) = (inst', th RS @{thm HOL.not_sym})
in
map process_inst instAB @ (map (switch_ineq o process_inst) instBA)
end
in
{pre_match = pre_match, match = match}
end
fun find_contradiction pat ctxt (id, inst) =
let
fun process_pattern (pat_l, pat_r, order_ty) =
map (fn (id', eq_th) =>
(order_ty,
(id', eq_th, Thm.reflexive (Thm.cterm_of ctxt pat_r))))
(Auto2_Setup.RewriteTable.equiv_info_t ctxt id (pat_l, pat_r))
val insts = process_pattern (analyze_pattern pat)
val insts2 = case analyze_pattern2 pat of
NONE => [] | SOME pattern => process_pattern pattern
fun process_inst (order_ty, (id', eq_th1, eq_th2)) =
let
val assum = pat |> Util.subst_term_norm inst
|> mk_Trueprop |> Thm.cterm_of ctxt
val norm_th =
assum |> Thm.assume
|> apply_to_thm' (Conv.arg1_conv (rewr_side eq_th1))
|> apply_to_thm' (Conv.arg_conv (rewr_side eq_th2))
|> to_normal_th order_ty
val (lhs, rhs) = Util.dest_binop_args (prop_of' norm_th)
in
if is_plus_const lhs andalso dest_arg1 lhs aconv rhs then
let
val d = dest_numc (dest_arg lhs)
in
if d = 0 then [] else
[((id', inst),
([nat_less_th 0 d, norm_th] MRS @{thm single_resolve})
|> Thm.implies_intr assum
|> apply_to_thm Auto2_Setup.UtilLogic.rewrite_from_contra_form)]
end
else []
end
in
maps process_inst (insts @ insts2)
end
fun find_contradiction_trivial pat ctxt (id, inst) =
let
val (A, B) = Util.dest_binop_args pat
in
if not (is_numc A andalso is_numc B) then [] else
if not (is_less pat andalso dest_numc A >= dest_numc B) andalso
not (is_less_eq pat andalso dest_numc A > dest_numc B) then []
else let
val assum = pat |> mk_Trueprop |> Thm.cterm_of ctxt
in
[((id, inst),
(UtilArith.contra_by_arith ctxt [Thm.assume assum])
|> Thm.implies_intr assum
|> apply_to_thm Auto2_Setup.UtilLogic.rewrite_from_contra_form)]
end
end
fun find_contradiction_trivial2 pat ctxt (id, inst) =
let
val (_, B) = Util.dest_binop_args pat
in
if is_less pat andalso B aconv nat0 then
let
val assum = pat |> mk_Trueprop |> Thm.cterm_of ctxt
in
[((id, inst),
([@{thm Nat.not_less0}, Thm.assume assum] MRS Auto2_UtilBase.contra_triv_th)
|> Thm.implies_intr assum
|> apply_to_thm Auto2_Setup.UtilLogic.rewrite_from_contra_form)]
end
else []
end
fun nat_order_single_match pat _ ctxt (id, inst) =
if not (is_order_pat ctxt pat) orelse Util.has_vars pat then [] else
let
val is_neg = is_neg pat
val neg_pat = get_neg_order pat
val (A, B) = Util.dest_binop_args neg_pat
val res =
if is_less neg_pat andalso B aconv nat0 then
find_contradiction_trivial2 neg_pat ctxt (id, inst)
else if is_numc A andalso is_numc B then
find_contradiction_trivial neg_pat ctxt (id, inst)
else
find_contradiction neg_pat ctxt (id, inst)
in
if is_neg then res
else res |> map (apsnd (apply_to_thm' UtilArith.neg_ineq_cv))
end
val nat_order_single_matcher =
{pre_match = (fn pat => fn _ => fn ctxt => is_order_pat ctxt pat),
match = nat_order_single_match}
val shadow_nat_order_prfstep =
Auto2_Setup.ProofStep.gen_prfstep
"shadow_nat_order"
[WithItem (TY_NAT_ORDER, @{term_pat "(?x, ?y, ?m)"}),
WithItem (TY_NAT_ORDER, @{term_pat "(?x, ?y, ?n)"}),
Filter (fn _ => fn (_, inst) =>
dest_numc (lookup_inst inst "m") <=
dest_numc (lookup_inst inst "n")),
ShadowSecond]
val shadow_nat_order_single =
Auto2_Setup.ProofStep.gen_prfstep
"shadow_nat_order_single"
[WithItem (TY_NAT_ORDER, @{term_pat "(?x, ?x, ?n)"}),
Filter (fn _ => fn (_, inst) => dest_numc (lookup_inst inst "n") >= 0),
ShadowFirst]
val shadow_nat_order_single_zero =
Auto2_Setup.ProofStep.gen_prfstep
"shadow_nat_order_single_zero"
[WithItem (TY_NAT_ORDER, @{term_pat "(0, ?x, ?n)"}),
Filter (fn _ => fn (_, inst) => dest_numc (lookup_inst inst "n") >= 0),
ShadowFirst]
fun string_of_nat_order ctxt (x, y, diff, th) =
if x aconv nat0 andalso diff < 0 then
th |> apply_to_thm' (Conv.arg1_conv nat_fold_conv0_left)
|> Thm.prop_of |> Syntax.string_of_term ctxt
else if y aconv nat0 andalso diff >= 0 then
th |> apply_to_thm' (Conv.arg_conv nat_fold_conv0_left)
|> Thm.prop_of |> Syntax.string_of_term ctxt
else if diff = 0 then
th |> apply_to_thm' (Conv.arg_conv nat_fold_conv0_right)
|> Thm.prop_of |> Syntax.string_of_term ctxt
else
th |> Thm.prop_of |> Syntax.string_of_term ctxt
fun output_nat_order ctxt (ts, th) =
let
val (x, y, diff_t) = the_triple ts
val diff = dest_numc diff_t
in
"ORDER " ^ string_of_nat_order ctxt (x, y, diff, th)
end
fun shadow_nat_order _ _ (ts1, cts2) =
let
val (x1, y1, m) = the_triple ts1
val (cx2, cy2, n) = the_triple cts2
val m = dest_numc m
val n = dest_numc (Thm.term_of n)
in
if m < n then false else
x1 aconv Thm.term_of cx2 andalso y1 aconv Thm.term_of cy2
end
val add_nat_order_proofsteps =
Auto2_Setup.ItemIO.add_item_type (
TY_NAT_ORDER, SOME (take 2), SOME output_nat_order, SOME shadow_nat_order
) #> Auto2_Setup.ItemIO.add_typed_matcher (
TY_NAT_ORDER, nat_order_typed_matcher
) #> fold Auto2_Setup.ItemIO.add_prop_matcher [
(TY_NAT_ORDER, nat_order_matcher),
(TY_NAT_ORDER, nat_order_noteq_matcher),
(TY_NULL, nat_order_single_matcher)
] #> Auto2_Setup.Normalizer.add_normalizer (
("nat_order", nat_order_normalizer)
) #> fold add_prfstep [
nat_eq_diff_prfstep,
transitive, transitive_resolve, single_resolve, single_resolve_zero,
shadow_nat_order_prfstep, shadow_nat_order_single,
shadow_nat_order_single_zero
]
end
val _ = Theory.setup (Nat_Order.add_nat_order_proofsteps)