# HG changeset patch # User nipkow # Date 916316289 -3600 # Node ID 2acc5d36610c9792b46c4a7f4c95214a247a9fcd # Parent ece970eb5850053387e2742c2280582c4aff462d More arith refinements. diff -r ece970eb5850 -r 2acc5d36610c src/HOL/Arith.ML --- a/src/HOL/Arith.ML Thu Jan 14 12:32:13 1999 +0100 +++ b/src/HOL/Arith.ML Thu Jan 14 13:18:09 1999 +0100 @@ -853,8 +853,11 @@ val notI = notI; val sym = sym; val not_lessD = linorder_not_less RS iffD1; +val not_leD = linorder_not_le RS iffD1; -val mk_Eq = mk_eq; + +fun mk_Eq thm = (thm RS Eq_FalseI) handle _ => (thm RS Eq_TrueI); + val mk_Trueprop = HOLogic.mk_Trueprop; fun neg_prop(TP$(Const("Not",_)$t)) = TP$t @@ -864,13 +867,18 @@ let val _ $ t = #prop(rep_thm thm) in t = Const("False",HOLogic.boolT) end; +fun is_nat(t) = fastype_of1 t = HOLogic.natT; + +fun mk_nat_thm sg t = + let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) + in instantiate ([],[(cn,ct)]) le0 end; + end; -structure Nat_LA_Data: LIN_ARITH_DATA = +structure Nat_LA_Data (* : LIN_ARITH_DATA *) = struct -val lessD = Suc_leI; -val not_leD = not_leE RS Suc_leI; +val lessD = [Suc_leI]; (* Turn term into list of summand * multiplicity plus a constant *) fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1)) @@ -882,8 +890,7 @@ fun nnb T = T = ([HOLogic.natT,HOLogic.natT] ---> HOLogic.boolT); -fun decomp2(rel,T,lhs,rhs) = - if not(nnb T) then None else +fun decomp2(rel,lhs,rhs) = let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0)) in case rel of "op <" => Some(p,i,"<",q,j) @@ -895,9 +902,11 @@ fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j) | negate None = None; -fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs) +fun decomp1(T,xxx) = if nnb T then decomp2 xxx else None; + +fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs)) | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = - negate(decomp2(rel,T,lhs,rhs)) + negate(decomp1(T,(rel,lhs,rhs))) | decomp _ = None (* reduce contradictory <= to False. @@ -919,29 +928,27 @@ "(i = j) & (k = l) ==> i + k = j + (l::nat)" ]; -fun is_nat(t) = fastype_of1 t = HOLogic.natT; +end; -fun mk_nat_thm sg t = - let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) - in instantiate ([],[(cn,ct)]) le0 end; - +structure LA_Data_Ref = +struct + val add_mono_thms = ref Nat_LA_Data.add_mono_thms + val lessD = ref Nat_LA_Data.lessD + val decomp = ref Nat_LA_Data.decomp + val simp = ref Nat_LA_Data.simp end; -structure Fast_Nat_Arith = - Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Nat_LA_Data); +structure Fast_Arith = + Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref); -val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac; - -local -fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT); +val fast_arith_tac = Fast_Arith.lin_arith_tac; -val pats = map prep_pat - ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] +val nat_arith_simproc_pats = + map (fn s => Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT)) + ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]; -in -val fast_nat_arith_simproc = - mk_simproc "fast_nat_arith" pats Fast_Nat_Arith.lin_arith_prover; -end; +val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats + Fast_Arith.lin_arith_prover; Addsimprocs [fast_nat_arith_simproc]; @@ -951,7 +958,7 @@ fast_nat_arith_simproc anyway. However, it seems cheaper to activate the solver all the time rather than add the additional check. *) -simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac); +simpset_ref () := (simpset() addSolver Fast_Arith.cut_lin_arith_tac); (* Elimination of `-' on nat due to John Harrison *) Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))"; @@ -964,9 +971,9 @@ (* FIXME: K true should be replaced by a sensible test to speed things up in case there are lots of irrelevant terms involved *) -val nat_arith_tac = +val arith_tac = refute_tac (K true) (REPEAT o split_tac[nat_diff_split]) - ((REPEAT_DETERM o etac nat_neqE) THEN' fast_nat_arith_tac); + ((REPEAT_DETERM o etac nat_neqE) THEN' fast_arith_tac); (*---------------------------------------------------------------------------*) (* End of proof procedures. Now go and USE them! *) @@ -975,75 +982,75 @@ (*** Subtraction laws -- mostly from Clemens Ballarin ***) Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_less_mono"; Goal "a+b < (c::nat) ==> a < c-b"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "add_less_imp_less_diff"; Goal "(i < j-k) = (i+k < (j::nat))"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "less_diff_conv"; Goal "(j-k <= (i::nat)) = (j <= i+k)"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "le_diff_conv"; Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "le_diff_conv2"; Goal "Suc i <= n ==> Suc (n - Suc i) = n - i"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "Suc_diff_Suc"; Goal "i <= (n::nat) ==> n - (n - i) = i"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_diff_cancel"; Addsimps [diff_diff_cancel]; Goal "k <= (n::nat) ==> m <= n + m - k"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "le_add_diff"; Goal "[| 0 j+k-i < k"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "add_diff_less"; Goal "m-1 < n ==> m <= n"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "pred_less_imp_le"; Goal "j<=i ==> i - j < Suc i - j"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_less_Suc_diff"; Goal "i - j <= Suc i - j"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_le_Suc_diff"; AddIffs [diff_le_Suc_diff]; Goal "n - Suc i <= n - i"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_Suc_le_diff"; AddIffs [diff_Suc_le_diff]; Goal "0 < n ==> (m <= n-1) = (m (m-1 < n) = (m<=n)"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "less_pred_eq"; (*In ordinary notation: if 0 m - n < m"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_less"; Goal "[| 0 m - n < m"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "le_diff_less"; @@ -1052,19 +1059,19 @@ (* Monotonicity of subtraction in first argument *) Goal "m <= (n::nat) ==> (m-l) <= (n-l)"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_le_mono"; Goal "m <= (n::nat) ==> (l-n) <= (l-m)"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_le_mono2"; (*This proof requires natdiff_cancel_sums*) Goal "[| m < (n::nat); m (l-n) < (l-m)"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diff_less_mono2"; Goal "[| m-n = 0; n-m = 0 |] ==> m=n"; -by(nat_arith_tac 1); +by(arith_tac 1); qed "diffs0_imp_equal"; diff -r ece970eb5850 -r 2acc5d36610c src/HOL/Integ/Bin.ML --- a/src/HOL/Integ/Bin.ML Thu Jan 14 12:32:13 1999 +0100 +++ b/src/HOL/Integ/Bin.ML Thu Jan 14 13:18:09 1999 +0100 @@ -399,13 +399,10 @@ (The latter option is very inefficient!) *) -structure Int_LA_Data: LIN_ARITH_DATA = +structure Int_LA_Data(*: LIN_ARITH_DATA*) = struct -val lessD = add1_zle_eq RS iffD2; -val not_leD = not_zleE RS lessD; - -val intT = Type("IntDef.int",[]); +val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2]; (* borrowed from Bin.thy: *) fun dest_bit (Const ("False", _)) = 0 @@ -437,10 +434,7 @@ ((p,i + m*dest_bin t) handle Match => add_atom(all,m,(p,i))) | poly x = add_atom x; -fun iib T = T = ([intT,intT] ---> HOLogic.boolT); - -fun decomp2(rel,T,lhs,rhs) = - if not(iib T) then None else +fun decomp2(rel,lhs,rhs) = let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) in case rel of "op <" => Some(p,i,"<",q,j) @@ -449,80 +443,89 @@ | _ => None end; -fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j) - | negate None = None; +val intT = Type("IntDef.int",[]); +fun iib T = T = ([intT,intT] ---> HOLogic.boolT); -fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs) +fun decomp1(T,xxx) = + if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx); + +fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs)) | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = - negate(decomp2(rel,T,lhs,rhs)) + Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs))) | decomp _ = None (* reduce contradictory <= to False *) val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0]; -val cancel_sums_ss = HOL_basic_ss addsimps add_rules +val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; val simp = simplify cancel_sums_ss; -val add_mono_thms = map (fn s => prove_goal Int.thy s - (fn prems => [cut_facts_tac prems 1, - asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) -["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", - "(i = j) & (k <= l) ==> i + k <= j + (l::int)", - "(i <= j) & (k = l) ==> i + k <= j + (l::int)", - "(i = j) & (k = l) ==> i + k = j + (l::int)" -]; - -fun is_nat(t) = false; - -fun mk_nat_thm sg t = sys_error "Int/mk_nat_thm"; +val add_mono_thms = Nat_LA_Data.add_mono_thms @ + map (fn s => prove_goal Int.thy s + (fn prems => [cut_facts_tac prems 1, + asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) + ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", + "(i = j) & (k <= l) ==> i + k <= j + (l::int)", + "(i <= j) & (k = l) ==> i + k <= j + (l::int)", + "(i = j) & (k = l) ==> i + k = j + (l::int)" + ]; end; -structure Fast_Int_Arith = - Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=Int_LA_Data); +(* Update parameters of arithmetic prover *) +LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms; +LA_Data_Ref.lessD := Int_LA_Data.lessD; +LA_Data_Ref.decomp := Int_LA_Data.decomp; +LA_Data_Ref.simp := Int_LA_Data.simp; + -val fast_int_arith_tac = Fast_Int_Arith.lin_arith_tac; +val int_arith_simproc_pats = + map (fn s => Thm.read_cterm (sign_of Int.thy) (s, HOLogic.boolT)) + ["(m::int) < n","(m::int) <= n", "(m::int) = n"]; -simpset_ref () := (simpset() addSolver Fast_Int_Arith.cut_lin_arith_tac); +val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats + Fast_Arith.lin_arith_prover; + +Addsimprocs [fast_int_arith_simproc]; (* FIXME: K true should be replaced by a sensible test to speed things up in case there are lots of irrelevant terms involved. *) -val int_arith_tac = - refute_tac (K true) (K all_tac) - ((REPEAT o etac int_neqE) THEN' fast_int_arith_tac); +val arith_tac = + refute_tac (K true) (REPEAT o split_tac[nat_diff_split]) + ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac); (* Some test data Goal "!!a::int. [| a <= b; c <= d; x+y a+c <= b+d"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ \ ==> a+a <= j+j"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. [| a+b < i+j; a a+a - - #-1 < j+j - #3"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; -by(int_arith_tac 1); +by(arith_tac 1); Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ \ ==> a <= l"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ \ ==> a+a+a+a <= l+l+l+l"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ \ ==> a+a+a+a+a <= l+l+l+l+i"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ \ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); *) (*---------------------------------------------------------------------------*) @@ -544,50 +547,50 @@ (** Simplification of inequalities involving numerical constants **) Goal "(w <= z + #1) = (w<=z | w = z + #1)"; -by(int_arith_tac 1); +by(arith_tac 1); qed "zle_add1_eq"; Goal "(w <= z - #1) = (w w <= z + v"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); qed "zle_imp_zle_zadd"; Goal "w <= z ==> w <= z + #1"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); qed "zle_imp_zle_zadd1"; (*2nd premise can be proved automatically if v is a literal*) Goal "[| w < z; #0 <= v |] ==> w < z + v"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); qed "zless_imp_zless_zadd"; Goal "w < z ==> w < z + #1"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); qed "zless_imp_zless_zadd1"; Goal "(w < z + #1) = (w<=z)"; -by(int_arith_tac 1); +by(arith_tac 1); qed "zle_add1_eq_le"; Addsimps [zle_add1_eq_le]; Goal "(z = z + w) = (w = #0)"; -by(int_arith_tac 1); +by(arith_tac 1); qed "zadd_left_cancel0"; Addsimps [zadd_left_cancel0]; (*LOOPS as a simprule!*) Goal "[| w + v < z; #0 <= v |] ==> w < z"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); qed "zless_zadd_imp_zless"; (*LOOPS as a simprule! Analogous to Suc_lessD*) Goal "w + #1 < z ==> w < z"; -by(fast_int_arith_tac 1); +by(fast_arith_tac 1); qed "zless_zadd1_imp_zless"; Goal "w + #-1 = w - #1"; diff -r ece970eb5850 -r 2acc5d36610c src/HOL/Lambda/Eta.ML --- a/src/HOL/Lambda/Eta.ML Thu Jan 14 12:32:13 1999 +0100 +++ b/src/HOL/Lambda/Eta.ML Thu Jan 14 13:18:09 1999 +0100 @@ -29,7 +29,7 @@ Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))"; by (induct_tac "t" 1); by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong]))); - by(nat_arith_tac 1); + by(arith_tac 1); by(Auto_tac); qed "free_lift"; Addsimps [free_lift]; diff -r ece970eb5850 -r 2acc5d36610c src/HOL/Lambda/ListApplication.ML --- a/src/HOL/Lambda/ListApplication.ML Thu Jan 14 12:32:13 1999 +0100 +++ b/src/HOL/Lambda/ListApplication.ML Thu Jan 14 13:18:09 1999 +0100 @@ -88,7 +88,7 @@ Addsimps [size_apps]; Goal "[| 0 < k; m <= n |] ==> m < n+k"; -by(fast_nat_arith_tac 1); +by(fast_arith_tac 1); val lemma = result(); (* a customized induction schema for $$ *) diff -r ece970eb5850 -r 2acc5d36610c src/HOL/Ord.ML --- a/src/HOL/Ord.ML Thu Jan 14 12:32:13 1999 +0100 +++ b/src/HOL/Ord.ML Thu Jan 14 13:18:09 1999 +0100 @@ -104,6 +104,28 @@ by (Blast_tac 1); qed "linorder_less_linear"; +Goal "!!x::'a::linorder. (~ x < y) = (y <= x)"; +by (simp_tac (simpset() addsimps [order_less_le]) 1); +by (cut_facts_tac [linorder_linear] 1); +by (blast_tac (claset() addIs [order_antisym]) 1); +qed "linorder_not_less"; + +Goal "!!x::'a::linorder. (~ x <= y) = (y < x)"; +by (simp_tac (simpset() addsimps [order_less_le]) 1); +by (cut_facts_tac [linorder_linear] 1); +by (blast_tac (claset() addIs [order_antisym]) 1); +qed "linorder_not_le"; + +Goal "!!x::'a::linorder. (x ~= y) = (x (P = True)" RS mp; - val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; - - val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; - val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection; - in (*Make meta-equalities. The operator below is Trueprop*) - fun mk_meta_eq r = r RS eq_reflection; +fun mk_meta_eq r = r RS eq_reflection; + +val Eq_TrueI = mk_meta_eq(prover "P --> (P = True)" RS mp); +val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp); - fun mk_eq th = case concl_of th of - Const("==",_)$_$_ => th - | _$(Const("op =",_)$_$_) => mk_meta_eq th - | _$(Const("Not",_)$_) => th RS not_P_imp_P_eq_False - | _ => th RS P_imp_P_eq_True; - (* last 2 lines requires all formulae to be of the from Trueprop(.) *) +fun mk_eq th = case concl_of th of + Const("==",_)$_$_ => th + | _$(Const("op =",_)$_$_) => mk_meta_eq th + | _$(Const("Not",_)$_) => th RS Eq_FalseI + | _ => th RS Eq_TrueI; +(* last 2 lines requires all formulae to be of the from Trueprop(.) *) - fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True); +fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI); - fun mk_meta_cong rl = - standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl)) - handle THM _ => - error("Premises and conclusion of congruence rules must be =-equalities"); +fun mk_meta_cong rl = + standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl)) + handle THM _ => + error("Premises and conclusion of congruence rules must be =-equalities"); val not_not = prover "(~ ~ P) = P"; @@ -505,6 +502,6 @@ eresolve_tac [disjE] 1) THEN ref_tac 1; in EVERY'[TRY o filter_prems_tac test, - REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, + DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac, SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)] end; diff -r ece970eb5850 -r 2acc5d36610c src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Thu Jan 14 12:32:13 1999 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jan 14 13:18:09 1999 +0100 @@ -26,11 +26,14 @@ val neqE: thm (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *) val notI: thm (* (P ==> False) ==> ~ P *) val not_lessD: thm (* ~(m < n) ==> n <= m *) + val not_leD: thm (* ~(m <= n) ==> n < m *) val sym: thm (* x = y ==> y = x *) val mk_Eq: thm -> thm val mk_Trueprop: term -> term val neg_prop: term -> term val is_False: thm -> bool + val is_nat: typ list * term -> bool + val mk_nat_thm: Sign.sg -> term -> thm end; (* mk_Eq(~in) = `in == False' @@ -40,19 +43,20 @@ neg_prop(t) = neg if t is wrapped up in Trueprop and nt is the (logically) negated version of t, where the negation of a negative term is the term itself (no double negation!); + +is_nat(parameter-types,t) = t:nat +mk_nat_thm(t) = "0 <= t" *) signature LIN_ARITH_DATA = sig - val add_mono_thms: thm list + val add_mono_thms: thm list ref (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *) - val lessD: thm (* m < n ==> Suc m <= n *) - val not_leD: thm (* ~(m <= n) ==> Suc n <= m *) - val decomp: term -> - ((term * int)list * int * string * (term * int)list * int)option - val simp: thm -> thm - val is_nat: typ list * term -> bool - val mk_nat_thm: Sign.sg -> term -> thm + val lessD: thm list ref (* m < n ==> m+1 <= n *) + val decomp: + (term -> ((term * int)list * int * string * (term * int)list * int)option) + ref + val simp: (thm -> thm) ref end; (* decomp(`x Rel y') should yield (p,i,Rel,q,j) @@ -63,9 +67,6 @@ simp must reduce contradictory <= to False. It should also cancel common summands to keep <= reduced; otherwise <= can grow to massive proportions. - -is_nat(parameter-types,t) = t:nat -mk_nat_thm(t) = "0 <= t" *) signature FAST_LIN_ARITH = @@ -90,7 +91,9 @@ datatype injust = Asm of int | Nat of int (* index of atom *) - | Fwd of injust * thm + | LessD of injust + | NotLessD of injust + | NotLeD of injust | Multiplied of int * injust | Added of injust * injust; @@ -250,12 +253,12 @@ fun mkthm sg asms just = let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_)) => map fst lhs union (map fst rhs union ats)) - ([], mapfilter (LA_Data.decomp o concl_of) asms) + ([], mapfilter (!LA_Data.decomp o concl_of) asms) fun addthms thm1 thm2 = let val conj = thm1 RS (thm2 RS LA_Logic.conjI) in the(get_first (fn th => Some(conj RS th) handle _ => None) - LA_Data.add_mono_thms) + (!LA_Data.add_mono_thms)) end; fun multn(n,thm) = @@ -263,16 +266,18 @@ in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end; fun simp thm = - let val thm' = LA_Data.simp thm + let val thm' = !LA_Data.simp thm in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end fun mk(Asm i) = nth_elem(i,asms) - | mk(Nat(i)) = LA_Data.mk_nat_thm sg (nth_elem(i,atoms)) - | mk(Fwd(j,thm)) = mk j RS thm + | mk(Nat(i)) = LA_Logic.mk_nat_thm sg (nth_elem(i,atoms)) + | mk(LessD(j)) = hd([mk j] RL !LA_Data.lessD) + | mk(NotLeD(j)) = hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD) + | mk(NotLessD(j)) = mk j RS LA_Logic.not_lessD | mk(Added(j1,j2)) = simp(addthms (mk j1) (mk j2)) | mk(Multiplied(n,j)) = multn(n,mk j) - in LA_Data.simp(mk just) handle FalseE thm => thm end + in !LA_Data.simp(mk just) handle FalseE thm => thm end end; fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i; @@ -287,9 +292,9 @@ val just = Asm k in case rel of "<=" => Some(Lineq(c,Le,diff,just)) - | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,Fwd(just,LA_Data.not_leD))) - | "<" => Some(Lineq(c+1,Le,diff,Fwd(just,LA_Data.lessD))) - | "~<" => Some(Lineq(~c,Le,map (op~) diff,Fwd(just,LA_Logic.not_lessD))) + | "~<=" => Some(Lineq(1-c,Le,map (op ~) diff,NotLeD(just))) + | "<" => Some(Lineq(c+1,Le,diff,LessD(just))) + | "~<" => Some(Lineq(~c,Le,map (op~) diff,NotLessD(just))) | "=" => Some(Lineq(c,Eq,diff,just)) | "~=" => None | _ => sys_error("mklineq" ^ rel) @@ -297,7 +302,7 @@ end; fun mknat pTs ixs (atom,i) = - if LA_Data.is_nat(pTs,atom) + 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 else None @@ -345,9 +350,9 @@ fun prove(pTs,Hs,concl) = let val nHs = length Hs val ixHs = Hs ~~ (0 upto (nHs-1)) - val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of + val Hitems = mapfilter (fn (h,i) => case !LA_Data.decomp h of None => None | Some(it) => Some(it,i)) ixHs -in case LA_Data.decomp concl of +in case !LA_Data.decomp concl of None => if null Hitems then [] else refute1(pTs,Hitems) | Some(citem as (r,i,rel,l,j)) => if rel = "="