--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Jul 03 22:27:13 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Jul 03 22:27:16 2007 +0200
@@ -17,10 +17,9 @@
structure Groebner: GROEBNER =
struct
-open Normalizer;
-open Misc;
-fun assocd x al d = case AList.lookup (op =) al x of SOME y => y | NONE => d;
+open Conv Misc Normalizer;
+
val rat_0 = Rat.zero;
val rat_1 = Rat.one;
val minus_rat = Rat.neg;
@@ -331,8 +330,6 @@
(* In principle this is very inefficient: in a heavily shared proof it may *)
(* make the same calculation many times. Could put in a cache or something. *)
(* ------------------------------------------------------------------------- *)
-fun assoc x l = snd(find (fn p => fst p = x) l);
-
fun resolve_proof vars prf =
case prf of
Start(~1) => []
@@ -345,9 +342,9 @@
val lis2 = resolve_proof vars lin2
val dom = distinct (op =) ((map fst lis1) union (map fst lis2))
in
- map (fn n => let val a = ((assoc n lis1) handle _ => []) (* FIXME *)
- val b = ((assoc n lis2) handle _ => []) in (* FIXME *)
- (n,grob_add a b) end) dom end;
+ map (fn n => let val a = these (AList.lookup (op =) lis1 n)
+ val b = these (AList.lookup (op =) lis2 n)
+ in (n,grob_add a b) end) dom end;
(* ------------------------------------------------------------------------- *)
(* Run the procedure and produce Weak Nullstellensatz certificate. *)
@@ -388,18 +385,6 @@
(filter (fn (k,_) => k <> 0) cert) in
(d,l,cert') end;
-fun string_of_pol vars pol =
- foldl (fn ((c,m),s) => ((Rat.string_of_rat c)
- ^ "*(" ^
- (snd (foldl
- (fn (e,(i,s)) =>
- (i+ 1,
- (nth vars i
- |>cterm_of (the_context()) (* FIXME *)
- |> string_of_cterm)^ "^"
- ^ (Int.toString e) ^" * " ^ s)) (0,"0") m))
- ^ ") + ") ^ s) "" pol;
-
(* ------------------------------------------------------------------------- *)
(* Overall parametrized universal procedure for (semi)rings. *)
@@ -457,7 +442,7 @@
val bool_simps = @{thms "bool_simps"};
val nnf_simps = @{thms "nnf_simps"};
val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps bool_simps addsimps nnf_simps)
-val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps (@{thms "weak_dnf_simps"}));
+val weak_dnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms "weak_dnf_simps"});
val initial_conv =
Simplifier.rewrite
(HOL_basic_ss addsimps nnf_simps
@@ -468,7 +453,7 @@
val cTrp = @{cterm "Trueprop"};
val cConj = @{cterm "op &"};
val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
-val ASSUME = mk_comb cTrp #> assume;
+val assume_Trueprop = mk_comb cTrp #> assume;
val list_mk_conj = list_mk_binop cConj;
val conjs = list_dest_binop cConj;
val mk_neg = mk_comb cNot;
@@ -607,15 +592,15 @@
fun mk_add th1 = combination(Drule.arg_cong_rule ring_add_tm th1);
fun refute tm =
- if tm aconvc false_tm then ASSUME tm else
+ if tm aconvc false_tm then assume_Trueprop tm else
let
- val (nths0,eths0) = List.partition (is_neg o concl) (conjuncts(ASSUME tm))
+ val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm))
val nths = filter (is_eq o Thm.dest_arg o concl) nths0
val eths = filter (is_eq o concl) eths0
in
if null eths then
let
- val th1 = end_itlist (fn th1 => fn th2 => idom_rule(conji th1 th2)) nths
+ val th1 = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths
val th2 = Conv.fconv_rule
((arg_conv #> arg_conv)
(binop_conv ring_normalize_conv)) th1
@@ -635,12 +620,12 @@
end
else
let
- val nth = end_itlist (fn th1 => fn th2 => idom_rule(conji th1 th2)) nths
+ val nth = end_itlist (fn th1 => fn th2 => idom_rule(HOLogic.conj_intr th1 th2)) nths
val (vars,pol::pols) =
grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
val (deg,l,cert) = grobner_strong vars pols pol
val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth
- val th2 = funpow (Integer.machine_int deg) (idom_rule o conji th1) neq_01
+ val th2 = funpow (Integer.machine_int deg) (idom_rule o HOLogic.conj_intr th1) neq_01
in (vars,l,cert,th2)
end)
(* val _ = writeln ("Translating certificate to HOL inferences") *)
@@ -656,7 +641,7 @@
(nth eths (Integer.machine_int i) |> mk_meta_eq)) pols)
val th1 = thm_fn herts_pos
val th2 = thm_fn herts_neg
- val th3 = conji(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
+ val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
val th4 = Conv.fconv_rule ((arg_conv o arg_conv o binop_conv) ring_normalize_conv)
(neq_rule l th3)
val (l,r) = dest_eq(Thm.dest_arg(concl th4))
@@ -696,7 +681,7 @@
val pols = map (grobify_term vars) tms
val pol = grobify_term vars tm
val cert = grobner_ideal vars pols pol
- in map (fn n => let val p = assocd n cert [] in holify_polynomial vars p end)
+ in map (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
(map Integer.int (0 upto (length pols - 1)))
end
in (ring,ideal)
@@ -733,7 +718,7 @@
dest_const (mk_const (Thm.ctyp_of_term tm)) (ring_eq_conv ctxt)
(semiring_normalize_wrapper ctxt res)) form));
-fun algebra_tac add_ths del_ths ctxt i = ObjectLogic.full_atomize_tac i
+fun algebra_tac add_ths del_ths ctxt i = ObjectLogic.full_atomize_tac i
THEN (simp_tac (fst (NormalizerData.get ctxt) delsimps del_ths addsimps add_ths) i)
THEN (fn st =>
case try (nth (cprems_of st)) (i - 1) of
@@ -742,7 +727,7 @@
in rtac th i st end
handle TERM _ => no_tac st
| THM _ => no_tac st
- | ERROR _ => no_tac st
+ | ERROR _ => no_tac st (* FIXME !? *)
| CTERM _ => no_tac st);
end;