--- a/src/HOL/Arith.ML Wed Sep 22 21:49:37 1999 +0200
+++ b/src/HOL/Arith.ML Thu Sep 23 09:04:36 1999 +0200
@@ -890,29 +890,18 @@
end;
-structure Nat_LA_Data (* : LIN_ARITH_DATA *) =
-struct
-
-val lessD = [Suc_leI];
-
-(* reduce contradictory <= to False.
- Most of the work is done by the cancel tactics.
-*)
-val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
+signature LIN_ARITH_DATA2 =
+sig
+ include LIN_ARITH_DATA
+ val discrete: (string * bool)list ref
+end;
-val cancel_sums_ss = HOL_basic_ss addsimps add_rules
- addsimprocs nat_cancel_sums_add;
-
-val simp = simplify cancel_sums_ss;
-
-val add_mono_thms = map (fn s => prove_goal Arith.thy s
- (fn prems => [cut_facts_tac prems 1,
- blast_tac (claset() addIs [add_le_mono]) 1]))
-["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
- "(i = j) & (k <= l) ==> i + k <= j + (l::nat)",
- "(i <= j) & (k = l) ==> i + k <= j + (l::nat)",
- "(i = j) & (k = l) ==> i + k = j + (l::nat)"
-];
+structure LA_Data_Ref: LIN_ARITH_DATA2 =
+struct
+ val add_mono_thms = ref ([]:thm list);
+ val lessD = ref ([]:thm list);
+ val ss_ref = ref HOL_basic_ss;
+ val discrete = ref ([]:(string*bool)list);
(* Decomposition of terms *)
@@ -953,31 +942,44 @@
fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
| negate None = None;
-fun decomp1 tab (T,xxx) =
+fun decomp1 (T,xxx) =
(case T of
Type("fun",[Type(D,[]),_]) =>
- (case assoc(!tab,D) of
+ (case assoc(!discrete,D) of
None => None
| Some d => (case decomp2 xxx of
None => None
| Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
| _ => None);
-(* tab: (string * bool)list ref contains the discreteneness flag *)
-fun decomp tab (_$(Const(rel,T)$lhs$rhs)) = decomp1 tab (T,(rel,lhs,rhs))
- | decomp tab (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
- negate(decomp1 tab (T,(rel,lhs,rhs)))
- | decomp _ _ = None
-
+fun decomp (_$(Const(rel,T)$lhs$rhs)) = decomp1 (T,(rel,lhs,rhs))
+ | decomp (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
+ negate(decomp1 (T,(rel,lhs,rhs)))
+ | decomp _ = None
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 simp = ref Nat_LA_Data.simp
- val discrete = ref [("nat",true)]
- val decomp = Nat_LA_Data.decomp discrete
+let
+
+(* reduce contradictory <= to False.
+ Most of the work is done by the cancel tactics.
+*)
+val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
+
+val add_mono_thms = map (fn s => prove_goal Arith.thy s
+ (fn prems => [cut_facts_tac prems 1,
+ blast_tac (claset() addIs [add_le_mono]) 1]))
+["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
+ "(i = j) & (k <= l) ==> i + k <= j + (l::nat)",
+ "(i <= j) & (k = l) ==> i + k <= j + (l::nat)",
+ "(i = j) & (k = l) ==> i + k = j + (l::nat)"
+];
+
+in
+LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
+LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [Suc_leI];
+LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
+ addsimprocs nat_cancel_sums_add;
+LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("nat",true)]
end;
structure Fast_Arith =
@@ -985,14 +987,16 @@
val fast_arith_tac = Fast_Arith.lin_arith_tac;
+let
val nat_arith_simproc_pats =
map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT))
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
-val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats
- Fast_Arith.lin_arith_prover;
-
-Addsimprocs [fast_nat_arith_simproc];
+val fast_nat_arith_simproc = mk_simproc
+ "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover;
+in
+Addsimprocs [fast_nat_arith_simproc]
+end;
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
useful to detect inconsistencies among the premises for subgoals which are
@@ -1017,9 +1021,10 @@
(max m n + k <= r) = (m+k <= r & n+k <= r)
(l <= min m n + k) = (l <= m+k & l <= n+k)
*)
-val arith_tac =
- refute_tac (K true) (REPEAT o split_tac[nat_diff_split,split_min,split_max])
- ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
+val arith_tac_split_thms = ref [nat_diff_split,split_min,split_max];
+fun arith_tac i =
+ refute_tac (K true) (REPEAT o split_tac (!arith_tac_split_thms))
+ ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i;
(* proof method setup *)