--- a/src/HOL/arith_data.ML Mon Jul 31 14:08:42 2006 +0200
+++ b/src/HOL/arith_data.ML Mon Jul 31 15:29:36 2006 +0200
@@ -141,15 +141,19 @@
val nat_cancel_sums_add = map prep_simproc
[("nateq_cancel_sums",
- ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], K EqCancelSums.proc),
+ ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
+ K EqCancelSums.proc),
("natless_cancel_sums",
- ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], K LessCancelSums.proc),
+ ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
+ K LessCancelSums.proc),
("natle_cancel_sums",
- ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], K LeCancelSums.proc)];
+ ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
+ K LeCancelSums.proc)];
val nat_cancel_sums = nat_cancel_sums_add @
[prep_simproc ("natdiff_cancel_sums",
- ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], K DiffCancelSums.proc)];
+ ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
+ K DiffCancelSums.proc)];
end; (* ArithData *)
@@ -202,8 +206,10 @@
structure ArithTheoryData = TheoryDataFun
(struct
val name = "HOL/arith";
- type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string list, presburger: (int -> tactic) option};
-
+ type T = {splits: thm list,
+ inj_consts: (string * typ) list,
+ discrete: string list,
+ presburger: (int -> tactic) option};
val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE};
val copy = I;
val extend = I;
@@ -241,8 +247,6 @@
(* Decomposition of terms *)
-(* typ -> bool *)
-
fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT)
| nT _ = false;
@@ -274,9 +278,7 @@
their coefficients
*)
-(* (string * Term.typ) list -> ... *)
-
-fun demult inj_consts =
+fun demult (inj_consts : (string * Term.typ) list) =
let
fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = (
(case s of
@@ -292,29 +294,34 @@
let
val den = HOLogic.dest_binum dent
in
- if den = 0 then raise Zero else demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
+ if den = 0 then
+ raise Zero
+ else
+ demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
end
| _ =>
atomult (mC, s, t, m)
) handle TERM _ => atomult (mC, s, t, m)
)
- | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) = (
- let
+ | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) =
+ (let
val den = HOLogic.dest_binum dent
in
- if den = 0 then raise Zero else demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
+ if den = 0 then
+ raise Zero
+ else
+ demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
end
- handle TERM _ => (SOME atom, m)
- )
- | demult(Const("0",_),m) = (NONE, Rat.rat_of_int 0)
- | demult(Const("1",_),m) = (NONE, m)
- | demult(t as Const("Numeral.number_of",_)$n,m) =
- ((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n)))
- handle TERM _ => (SOME t,m))
- | demult(Const("HOL.uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
- | demult(t as Const f $ x, m) =
- (if f mem inj_consts then SOME x else SOME t,m)
- | demult(atom,m) = (SOME atom,m)
+ handle TERM _ => (SOME atom, m))
+ | demult (Const ("0", _), m) = (NONE, Rat.rat_of_int 0)
+ | demult (Const ("1", _), m) = (NONE, m)
+ | demult (t as Const ("Numeral.number_of", _) $ n, m) =
+ ((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
+ handle TERM _ => (SOME t,m))
+ | demult (Const ("HOL.uminus", _) $ t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
+ | demult (t as Const f $ x, m) =
+ (if f mem inj_consts then SOME x else SOME t, m)
+ | demult (atom, m) = (SOME atom, m)
and
atomult (mC, atom, t, m) = (
case demult (t, m) of (NONE, m') => (SOME atom, m')
@@ -412,24 +419,31 @@
val fast_arith_split_limit = ref 9;
-(* checks whether splitting with 'thm' is implemented *)
-
-(* Thm.thm -> bool *)
+(* checks if splitting with 'thm' is implemented *)
-fun is_split_thm thm =
- case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
- (case head_of lhs of
- Const (a, _) => a mem_string ["Orderings.max", "Orderings.min", "HOL.abs", "HOL.minus", "IntDef.nat", "Divides.op mod", "Divides.op div"]
- | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false))
- | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false);
+fun is_split_thm (thm : thm) : bool =
+ case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
+ (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
+ case head_of lhs of
+ Const (a, _) => a mem_string ["Orderings.max",
+ "Orderings.min",
+ "HOL.abs",
+ "HOL.minus",
+ "IntDef.nat",
+ "Divides.op mod",
+ "Divides.op div"]
+ | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
+ Display.string_of_thm thm);
+ false))
+ | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
+ Display.string_of_thm thm);
+ false);
(* substitute new for occurrences of old in a term, incrementing bound *)
(* variables as needed when substituting inside an abstraction *)
-(* (term * term) list -> term -> term *)
-
-fun subst_term [] t = t
- | subst_term pairs t =
+fun subst_term ([] : (term * term) list) (t : term) = t
+ | subst_term pairs t =
(case AList.lookup (op aconv) pairs t of
SOME new =>
new
@@ -447,14 +461,17 @@
(* variables and a term list for premises), or NONE if split_tac would fail *)
(* on the subgoal *)
-(* theory -> typ list * term list -> (typ list * term list) list option *)
-
(* FIXME: currently only the effect of certain split theorems is reproduced *)
(* (which is why we need 'is_split_thm'). A more canonical *)
(* implementation should analyze the right-hand side of the split *)
(* theorem that can be applied, and modify the subgoal accordingly. *)
+(* Or even better, the splitter should be extended to provide *)
+(* splitting on terms as well as splitting on theorems (where the *)
+(* former can have a faster implementation as it does not need to be *)
+(* proof-producing). *)
-fun split_once_items sg (Ts, terms) =
+fun split_once_items (sg : theory) (Ts : typ list, terms : term list) :
+ (typ list * term list) list option =
let
(* takes a list [t1, ..., tn] to the term *)
(* tn' --> ... --> t1' --> False , *)
@@ -467,12 +484,15 @@
val splits = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms)
in
if length splits > !fast_arith_split_limit then (
- tracing ("fast_arith_split_limit exceeded (current value is " ^ string_of_int (!fast_arith_split_limit) ^ ")");
+ tracing ("fast_arith_split_limit exceeded (current value is " ^
+ string_of_int (!fast_arith_split_limit) ^ ")");
NONE
) else (
case splits of [] =>
- NONE (* split_tac would fail: no possible split *)
- | ((_, _, _, split_type, split_term) :: _) => ( (* ignore all but the first possible split *)
+ (* split_tac would fail: no possible split *)
+ NONE
+ | ((_, _, _, split_type, split_term) :: _) => (
+ (* ignore all but the first possible split *)
case strip_comb split_term of
(* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
(Const ("Orderings.max", _), [t1, t2]) =>
@@ -480,7 +500,8 @@
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+ val t1_leq_t2 = Const ("Orderings.less_eq",
+ split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
@@ -494,7 +515,8 @@
val rev_terms = rev terms
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
val terms2 = map (subst_term [(split_term, t2)]) rev_terms
- val t1_leq_t2 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+ val t1_leq_t2 = Const ("Orderings.less_eq",
+ split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
@@ -505,15 +527,18 @@
(* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
| (Const ("HOL.abs", _), [t1]) =>
let
- val rev_terms = rev terms
- val terms1 = map (subst_term [(split_term, t1)]) rev_terms
- val terms2 = map (subst_term [(split_term, Const ("HOL.uminus", split_type --> split_type) $ t1)]) rev_terms
- val zero = Const ("0", split_type)
- val zero_leq_t1 = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ t1
- val t1_lt_zero = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
- val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
- val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
- val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
+ val rev_terms = rev terms
+ val terms1 = map (subst_term [(split_term, t1)]) rev_terms
+ val terms2 = map (subst_term [(split_term, Const ("HOL.uminus",
+ split_type --> split_type) $ t1)]) rev_terms
+ val zero = Const ("0", split_type)
+ val zero_leq_t1 = Const ("Orderings.less_eq",
+ split_type --> split_type --> HOLogic.boolT) $ zero $ t1
+ val t1_lt_zero = Const ("Orderings.less",
+ split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
+ val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+ val subgoal1 = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
+ val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
in
SOME [(Ts, subgoal1), (Ts, subgoal2)]
end
@@ -526,11 +551,15 @@
val zero = Const ("0", split_type)
val d = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
- val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)]) (map (incr_boundvars 1) rev_terms)
+ val terms2 = map (subst_term [(incr_boundvars 1 split_term, d)])
+ (map (incr_boundvars 1) rev_terms)
val t1' = incr_boundvars 1 t1
val t2' = incr_boundvars 1 t2
- val t1_lt_t2 = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
- val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const ("HOL.plus", split_type --> split_type --> split_type) $ t2' $ d)
+ val t1_lt_t2 = Const ("Orderings.less",
+ split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+ val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ (Const ("HOL.plus",
+ split_type --> split_type --> split_type) $ t2' $ d)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
@@ -544,18 +573,23 @@
val zero_int = Const ("0", HOLogic.intT)
val zero_nat = Const ("0", HOLogic.natT)
val n = Bound 0
- val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms)
+ val terms1 = map (subst_term [(incr_boundvars 1 split_term, n)])
+ (map (incr_boundvars 1) rev_terms)
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
val t1' = incr_boundvars 1 t1
- val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
- val t1_lt_zero = Const ("Orderings.less", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
+ val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
+ (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
+ val t1_lt_zero = Const ("Orderings.less",
+ HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
in
SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
end
- (* "?P ((?n::nat) mod (number_of ?k)) = ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) --> (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
+ (* "?P ((?n::nat) mod (number_of ?k)) =
+ ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
+ (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
| (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
@@ -563,22 +597,31 @@
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
- val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
+ val terms2 = map (subst_term [(incr_boundvars 2 split_term, j)])
+ (map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ val t2_eq_zero = Const ("op =",
+ split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+ val t2_neq_zero = HOLogic.mk_not (Const ("op =",
+ split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
+ val j_lt_t2 = Const ("Orderings.less",
+ split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const ("HOL.plus", split_type --> split_type --> split_type) $
- (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+ (Const ("HOL.times",
+ split_type --> split_type --> split_type) $ t2' $ i) $ j)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
- val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
+ val subgoal2 = (map HOLogic.mk_Trueprop
+ [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
+ @ terms2 @ [not_false]
in
SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
end
- (* "?P ((?n::nat) div (number_of ?k)) = ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) --> (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
+ (* "?P ((?n::nat) div (number_of ?k)) =
+ ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
+ (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
| (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
let
val rev_terms = rev terms
@@ -586,45 +629,64 @@
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
- val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
+ val terms2 = map (subst_term [(incr_boundvars 2 split_term, i)])
+ (map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val t2' = incr_boundvars 2 t2
- val t2_eq_zero = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
- val t2_neq_zero = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
- val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ val t2_eq_zero = Const ("op =",
+ split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+ val t2_neq_zero = HOLogic.mk_not (Const ("op =",
+ split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
+ val j_lt_t2 = Const ("Orderings.less",
+ split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const ("HOL.plus", split_type --> split_type --> split_type) $
- (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+ (Const ("HOL.times",
+ split_type --> split_type --> split_type) $ t2' $ i) $ j)
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
- val subgoal2 = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
+ val subgoal2 = (map HOLogic.mk_Trueprop
+ [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
+ @ terms2 @ [not_false]
in
SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
end
- (* "?P ((?n::int) mod (number_of ?k)) = ((iszero (number_of ?k) --> ?P ?n) &
- (neg (number_of (bin_minus ?k)) --> (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
- (neg (number_of ?k) --> (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
- | (Const ("Divides.op mod", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+ (* "?P ((?n::int) mod (number_of ?k)) =
+ ((iszero (number_of ?k) --> ?P ?n) &
+ (neg (number_of (bin_minus ?k)) -->
+ (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
+ (neg (number_of ?k) -->
+ (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
+ | (Const ("Divides.op mod",
+ Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
let
val rev_terms = rev terms
val zero = Const ("0", split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, t1)]) rev_terms
- val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
+ val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, j)])
+ (map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val (t2' as (_ $ k')) = incr_boundvars 2 t2
val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
- (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
- val zero_leq_j = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ (number_of $
+ (Const ("Numeral.bin_minus",
+ HOLogic.binT --> HOLogic.binT) $ k'))
+ val zero_leq_j = Const ("Orderings.less_eq",
+ split_type --> split_type --> HOLogic.boolT) $ zero $ j
+ val j_lt_t2 = Const ("Orderings.less",
+ split_type --> split_type--> HOLogic.boolT) $ j $ t2'
val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const ("HOL.plus", split_type --> split_type --> split_type) $
- (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+ (Const ("HOL.times",
+ split_type --> split_type --> split_type) $ t2' $ i) $ j)
val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
- val t2_lt_j = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val j_leq_zero = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
+ val t2_lt_j = Const ("Orderings.less",
+ split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+ val j_leq_zero = Const ("Orderings.less_eq",
+ split_type --> split_type --> HOLogic.boolT) $ j $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
val subgoal2 = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
@@ -641,61 +703,76 @@
in
SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
end
- (* "?P ((?n::int) div (number_of ?k)) = ((iszero (number_of ?k) --> ?P 0) &
- (neg (number_of (bin_minus ?k)) --> (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
- (neg (number_of ?k) --> (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
- | (Const ("Divides.op div", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+ (* "?P ((?n::int) div (number_of ?k)) =
+ ((iszero (number_of ?k) --> ?P 0) &
+ (neg (number_of (bin_minus ?k)) -->
+ (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
+ (neg (number_of ?k) -->
+ (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
+ | (Const ("Divides.op div",
+ Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
let
val rev_terms = rev terms
val zero = Const ("0", split_type)
val i = Bound 1
val j = Bound 0
val terms1 = map (subst_term [(split_term, zero)]) rev_terms
- val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
+ val terms2_3 = map (subst_term [(incr_boundvars 2 split_term, i)])
+ (map (incr_boundvars 2) rev_terms)
val t1' = incr_boundvars 2 t1
val (t2' as (_ $ k')) = incr_boundvars 2 t2
val iszero_t2 = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
val neg_minus_k = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
- (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
- val zero_leq_j = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
- val j_lt_t2 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
- val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+ (number_of $
+ (Const ("Numeral.bin_minus",
+ HOLogic.binT --> HOLogic.binT) $ k'))
+ val zero_leq_j = Const ("Orderings.less_eq",
+ split_type --> split_type --> HOLogic.boolT) $ zero $ j
+ val j_lt_t2 = Const ("Orderings.less",
+ split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+ val t1_eq_t2_times_i_plus_j = Const ("op =",
+ split_type --> split_type --> HOLogic.boolT) $ t1' $
(Const ("HOL.plus", split_type --> split_type --> split_type) $
- (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+ (Const ("HOL.times",
+ split_type --> split_type --> split_type) $ t2' $ i) $ j)
val neg_t2 = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
- val t2_lt_j = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
- val j_leq_zero = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
+ val t2_lt_j = Const ("Orderings.less",
+ split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+ val j_leq_zero = Const ("Orderings.less_eq",
+ split_type --> split_type --> HOLogic.boolT) $ j $ zero
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
val subgoal1 = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
val subgoal2 = (HOLogic.mk_Trueprop neg_minus_k)
:: terms2_3
@ not_false
- :: (map HOLogic.mk_Trueprop [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
+ :: (map HOLogic.mk_Trueprop
+ [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
val subgoal3 = (HOLogic.mk_Trueprop neg_t2)
:: terms2_3
@ not_false
- :: (map HOLogic.mk_Trueprop [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
+ :: (map HOLogic.mk_Trueprop
+ [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
val Ts' = split_type :: split_type :: Ts
in
SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
end
- (* this will only happen if a split theorem can be applied for which no code exists above -- *)
- (* in which case either the split theorem should be implemented above, or 'is_split_thm' *)
- (* should be modified to filter it out *)
+ (* this will only happen if a split theorem can be applied for which no *)
+ (* code exists above -- in which case either the split theorem should be *)
+ (* implemented above, or 'is_split_thm' should be modified to filter it *)
+ (* out *)
| (t, ts) => (
- warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^ " (with " ^ Int.toString (length ts) ^
+ warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^
+ " (with " ^ Int.toString (length ts) ^
" argument(s)) not implemented; proof reconstruction is likely to fail");
NONE
))
)
end;
-(* remove terms that do not satisfy p; change the order of the remaining *)
+(* remove terms that do not satisfy 'p'; change the order of the remaining *)
(* terms in the same way as filter_prems_tac does *)
-(* (term -> bool) -> term list -> term list *)
-
-fun filter_prems_tac_items p terms =
+fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
let
fun filter_prems (t, (left, right)) =
if p t then (left, right @ [t]) else (left @ right, [])
@@ -707,29 +784,31 @@
(* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a *)
(* subgoal that has 'terms' as premises *)
-(* term list -> bool *)
+fun negated_term_occurs_positively (terms : term list) : bool =
+ List.exists
+ (fn (Trueprop $ (Const ("Not", _) $ t)) => member (op aconv) terms (Trueprop $ t)
+ | _ => false)
+ terms;
-fun negated_term_occurs_positively terms =
- List.exists (fn (TP $ (Const ("Not", _) $ t)) => member (op aconv) terms (TP $ t) | _ => false) terms;
-
-(* theory -> typ list * term list -> (typ list * term list) list *)
-
-fun pre_decomp sg (Ts, terms) =
+fun pre_decomp sg (Ts : typ list, terms : term list) : (typ list * term list) list =
let
(* repeatedly split (including newly emerging subgoals) until no further *)
(* splitting is possible *)
- (* (typ list * term list) list -> (typ list * term list) list *)
- fun split_loop [] = []
- | split_loop (subgoal::subgoals) = (
+ fun split_loop ([] : (typ list * term list) list) = []
+ | split_loop (subgoal::subgoals) = (
case split_once_items sg subgoal of
SOME new_subgoals => split_loop (new_subgoals @ subgoals)
| NONE => subgoal :: split_loop subgoals
)
fun is_relevant t = isSome (decomp sg t)
- val relevant_terms = filter_prems_tac_items is_relevant terms (* filter_prems_tac is_relevant *)
- val split_goals = split_loop [(Ts, relevant_terms)] (* split_tac, NNF normalization *)
- val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals (* necessary because split_once_tac may normalize terms *)
- val result = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm (* TRY (etac notE) THEN eq_assume_tac *)
+ (* filter_prems_tac is_relevant: *)
+ val relevant_terms = filter_prems_tac_items is_relevant terms
+ (* split_tac, NNF normalization: *)
+ val split_goals = split_loop [(Ts, relevant_terms)]
+ (* necessary because split_once_tac may normalize terms: *)
+ val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals
+ (* TRY (etac notE) THEN eq_assume_tac: *)
+ val result = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm
in
result
end;
@@ -743,9 +822,7 @@
(* general form [| Q1; ...; Qm |] ==> False. Fails if more than *)
(* !fast_arith_split_limit splits are possible. *)
-(* Thm.thm list -> int -> Tactical.tactic *)
-
-fun split_once_tac split_thms i =
+fun split_once_tac (split_thms : thm list) (i : int) : tactic =
let
val nnf_simpset =
empty_ss setmkeqTrue mk_eq_True
@@ -782,8 +859,6 @@
(* subgoals and finally attempt to solve them by finding an immediate *)
(* contradiction (i.e. a term and its negation) in their premises. *)
-(* int -> Tactical.tactic *)
-
fun pre_tac i st =
let
val sg = theory_of_thm st
@@ -795,7 +870,9 @@
THEN (
(TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
THEN_ALL_NEW
- ((fn j => PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
+ ((fn j => PRIMITIVE
+ (Drule.fconv_rule
+ (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
THEN'
(TRY o (etac notE THEN' eq_assume_tac)))
) i
@@ -893,7 +970,8 @@
refute_tac (K true)
(* Splitting is also done inside fast_arith_tac, but not completely -- *)
(* split_tac may use split theorems that have not been implemented in *)
- (* fast_arith_tac (cf. pre_decomp and split_once_items above). *)
+ (* fast_arith_tac (cf. pre_decomp and split_once_items above), and *)
+ (* fast_arith_split_limit may trigger. *)
(* Therefore splitting outside of fast_arith_tac may allow us to prove *)
(* some goals that fast_arith_tac alone would fail on. *)
(REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Jul 31 14:08:42 2006 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Jul 31 15:29:36 2006 +0200
@@ -52,10 +52,13 @@
signature LIN_ARITH_DATA =
sig
- type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool (* internal representation of linear (in-)equations *)
+ (* internal representation of linear (in-)equations: *)
+ type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool
val decomp: theory -> term -> decompT option
- val pre_decomp: theory -> typ list * term list -> (typ list * term list) list (* preprocessing, performed on a representation of subgoals as list of premises *)
- val pre_tac : int -> Tactical.tactic (* preprocessing, performed on the goal -- must do the same as 'pre_decomp' *)
+ (* preprocessing, performed on a representation of subgoals as list of premises: *)
+ val pre_decomp: theory -> typ list * term list -> (typ list * term list) list
+ (* preprocessing, performed on the goal -- must do the same as 'pre_decomp': *)
+ val pre_tac : int -> Tactical.tactic
val number_of: IntInf.int * typ -> term
end;
(*
@@ -400,12 +403,10 @@
(* Translate back a proof. *)
(* ------------------------------------------------------------------------- *)
-(* string -> Thm.thm -> Thm.thm *)
-fun trace_thm msg th =
+fun trace_thm (msg : string) (th : thm) : thm =
(if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
-(* string -> unit *)
-fun trace_msg msg =
+fun trace_msg (msg : string) : unit =
if !trace then tracing msg else ();
(* FIXME OPTIMIZE!!!! (partly done already)
@@ -420,8 +421,7 @@
local
exception FalseE of thm
in
-(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> injust -> Thm.thm *)
-fun mkthm (sg, ss) asms just =
+fun mkthm (sg:theory, ss:simpset) (asms:thm list) (just:injust) : thm =
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
Data.get sg;
val simpset' = Simplifier.inherit_context ss simpset;
@@ -495,8 +495,7 @@
fun coeff poly atom : IntInf.int =
AList.lookup (op =) poly atom |> the_default 0;
-(* int list -> int *)
-fun lcms is = Library.foldl lcm (1, is);
+fun lcms (is:int list) : int = Library.foldl lcm (1, is);
fun integ(rlhs,r,rel,rrhs,s,d) =
let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
@@ -563,9 +562,7 @@
(* ------------------------------------------------------------------------- *)
-(* Term.typ list -> int list -> Term.term * int -> lineq option *)
-
-fun mknat pTs ixs (atom, i) =
+fun mknat (pTs : typ list) (ixs : int list) (atom : term, i : int) : lineq option =
if LA_Logic.is_nat (pTs, atom)
then let val l = map (fn j => if j=i then 1 else 0) ixs
in SOME (Lineq (0, Le, l, Nat i)) end
@@ -590,9 +587,7 @@
(* failure as soon as a case could not be refuted; i.e. delay further *)
(* splitting until after a refutation for other cases has been found. *)
-(* Theory.theory -> typ list * term list -> (typ list * (decompT * int) list) list *)
-
-fun split_items sg (Ts, terms) =
+fun split_items sg (Ts : typ list, terms : term list) : (typ list * (LA_Data.decompT * int) list) list =
let
(*
val _ = trace_msg ("split_items: Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
@@ -601,71 +596,61 @@
(* splits inequalities '~=' into '<' and '>'; this corresponds to *)
(* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *)
(* level *)
- (* decompT option list -> decompT option list list *)
fun elim_neq [] = [[]]
| elim_neq (NONE :: ineqs) = map (cons NONE) (elim_neq ineqs)
| elim_neq (SOME(ineq as (l,i,rel,r,j,d)) :: ineqs) =
if rel = "~=" then elim_neq (ineqs @ [SOME (l, i, "<", r, j, d)]) @
elim_neq (ineqs @ [SOME (r, j, "<", l, i, d)])
else map (cons (SOME ineq)) (elim_neq ineqs)
- (* int -> decompT option list -> (decompT * int) list *)
+
fun number_hyps _ [] = []
| number_hyps n (NONE::xs) = number_hyps (n+1) xs
| number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs
val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *)
- (* (typ list * term list) list *)
LA_Data.pre_decomp sg
|> (* compute the internal encoding of (in-)equalities *)
- (* (typ list * decompT option list) list *)
map (apsnd (map (LA_Data.decomp sg)))
|> (* splitting of inequalities *)
- (* (typ list * decompT option list) list list *)
map (fn (Ts, items) => map (pair Ts) (elim_neq items))
|> (* combine the list of lists of subgoals into a single list *)
- (* (typ list * decompT option list) list *)
List.concat
|> (* numbering of hypotheses, ignoring irrelevant ones *)
- (* (typ list * (decompT * int) list) list *)
map (apsnd (number_hyps 0))
(*
- val _ = trace_msg ("split_items: result has " ^ Int.toString (length result) ^ " subgoal(s)"
- ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
- (" " ^ Int.toString n ^ ". Ts = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
- " items = " ^ string_of_list
- (string_of_pair
- (fn (l, i, rel, r, j, d) =>
- enclose "(" ")" (commas
- [string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
- Rat.string_of_rat i,
- rel,
- string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
- Rat.string_of_rat j,
- Bool.toString d]))
- Int.toString) items, n+1)) result 1))
+ val _ = trace_msg ("split_items: result has " ^ Int.toString (length result) ^
+ " subgoal(s)" ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
+ (" " ^ Int.toString n ^ ". Ts = " ^
+ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
+ " items = " ^ string_of_list (string_of_pair
+ (fn (l, i, rel, r, j, d) => enclose "(" ")" (commas
+ [string_of_list
+ (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
+ Rat.string_of_rat i,
+ rel,
+ string_of_list
+ (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
+ Rat.string_of_rat j,
+ Bool.toString d]))
+ Int.toString) items, n+1)) result 1))
*)
in result end;
-(* term list * (decompT * int) -> term list *)
-
-fun add_atoms (ats, ((lhs,_,_,rhs,_,_),_)) =
+fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decompT, _)) : term list =
(map fst lhs) union ((map fst rhs) union ats);
-(* (bool * term) list * (decompT * int) -> (bool * term) list *)
-
-fun add_datoms (dats, ((lhs,_,_,rhs,_,d),_)) =
- (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats);
-
-(* (decompT * int) list -> bool list *)
+fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decompT, _)) :
+ (bool * term) list =
+ (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats);
-fun discr initems = map fst (Library.foldl add_datoms ([],initems));
-
-(* Theory.theory -> (string * typ) list -> bool -> (typ list * (decompT * int) list) list -> injust list -> injust list option *)
+fun discr (initems : (LA_Data.decompT * int) list) : bool list =
+ map fst (Library.foldl add_datoms ([],initems));
-fun refutes sg params show_ex =
+fun refutes (sg : theory) (params : (string * typ) list) (show_ex : bool) :
+ (typ list * (LA_Data.decompT * int) list) list -> injust list -> injust list option =
let
- (* (typ list * (decompT * int) list) list -> injust list -> injust list option *)
- fun refute ((Ts, initems)::initemss) js =
+ fun refute ((Ts : typ list, initems : (LA_Data.decompT * int) list)::initemss)
+ (js : injust list) : injust list option =
let val atoms = Library.foldl add_atoms ([], initems)
val n = length atoms
val mkleq = mklineq n atoms
@@ -675,7 +660,8 @@
val ineqs = map mkleq initems @ natlineqs
in case elim (ineqs, []) of
Success j =>
- (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); refute initemss (js@[j]))
+ (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")");
+ refute initemss (js@[j]))
| Failure hist =>
(if not show_ex then
()
@@ -692,62 +678,63 @@
| refute [] js = SOME js
in refute end;
-(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> term list -> injust list option *)
-
-fun refute sg params show_ex terms =
+fun refute (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) (terms : term list) :
+ injust list option =
refutes sg params show_ex (split_items sg (map snd params, terms)) [];
-(* ('a -> bool) -> 'a list -> int *)
-
-fun count P xs = length (List.filter P xs);
+fun count (P : 'a -> bool) (xs : 'a list) : int = length (List.filter P xs);
(* The limit on the number of ~= allowed.
Because each ~= is split into two cases, this can lead to an explosion.
*)
val fast_arith_neq_limit = ref 9;
-(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> Term.term list -> Term.term -> injust list option *)
-
-fun prove sg params show_ex Hs concl =
+fun prove (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) (Hs : term list)
+ (concl : term) : injust list option =
let
(* append the negated conclusion to 'Hs' -- this corresponds to *)
(* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *)
(* theorem/tactic level *)
val Hs' = Hs @ [LA_Logic.neg_prop concl]
- (* decompT option -> bool *)
fun is_neq NONE = false
| is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
in
trace_msg "prove";
if count is_neq (map (LA_Data.decomp sg) Hs')
> !fast_arith_neq_limit then (
- trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ string_of_int (!fast_arith_neq_limit) ^ ")");
+ trace_msg ("fast_arith_neq_limit exceeded (current value is " ^
+ string_of_int (!fast_arith_neq_limit) ^ ")");
NONE
) else
refute sg params show_ex Hs'
end;
-(* MetaSimplifier.simpset -> int * injust list -> Tactical.tactic *)
-
-fun refute_tac ss (i, justs) =
+fun refute_tac (ss : simpset) (i : int, justs : injust list) : tactic =
fn state =>
- let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ Int.toString (length justs) ^ " justification(s)):") state
+ let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^
+ Int.toString (length justs) ^ " justification(s)):") state
val sg = theory_of_thm state
val {neqE, ...} = Data.get sg
fun just1 j =
- REPEAT_DETERM (eresolve_tac neqE i) THEN (* eliminate inequalities *)
- METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i (* use theorems generated from the actual justifications *)
- in DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
- DETERM (LA_Data.pre_tac i) THEN (* user-defined preprocessing of the subgoal *)
+ (* eliminate inequalities *)
+ REPEAT_DETERM (eresolve_tac neqE i) THEN
+ (* use theorems generated from the actual justifications *)
+ METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i
+ in (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
+ DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
+ (* user-defined preprocessing of the subgoal *)
+ DETERM (LA_Data.pre_tac i) THEN
PRIMITIVE (trace_thm "State after pre_tac:") THEN
- EVERY (map just1 justs) (* prove every resulting subgoal, using its justification *)
+ (* prove every resulting subgoal, using its justification *)
+ EVERY (map just1 justs)
end state;
(*
Fast but very incomplete decider. Only premises and conclusions
that are already (negated) (in)equations are taken into account.
*)
-fun simpset_lin_arith_tac ss show_ex i st = SUBGOAL (fn (A,_) =>
+fun simpset_lin_arith_tac (ss : simpset) (show_ex : bool) (i : int) (st : thm) =
+ SUBGOAL (fn (A,_) =>
let val params = rev (Logic.strip_params A)
val Hs = Logic.strip_assums_hyp A
val concl = Logic.strip_assums_concl A
@@ -757,19 +744,17 @@
| SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
end) i st;
-fun lin_arith_tac show_ex i st =
+fun lin_arith_tac (show_ex : bool) (i : int) (st : thm) =
simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
show_ex i st;
-fun cut_lin_arith_tac ss i =
+fun cut_lin_arith_tac (ss : simpset) (i : int) =
cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
simpset_lin_arith_tac ss false i;
(** Forward proof from theorems **)
-(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> Term.term -> injust list -> bool -> Thm.thm option *)
-
-fun prover (ctxt as (sg, ss)) thms Tconcl js pos =
+fun prover (ctxt as (sg, ss)) thms (Tconcl : term) (js : injust list) (pos : bool) : thm option =
let
(* There is no "forward version" of 'pre_tac'. Therefore we combine the *)
(* available theorems into a single proof state and perform "backward proof" *)
@@ -794,9 +779,7 @@
dives into terms and will thus try the non-negated concl anyway.
*)
-(* Theory.theory -> MetaSimplifier.simpset -> Term.term -> Thm.thm option *)
-
-fun lin_arith_prover sg ss concl =
+fun lin_arith_prover sg ss (concl : term) : thm option =
let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss));
val Hs = map prop_of thms
val Tconcl = LA_Logic.mk_Trueprop concl