1.1 --- a/src/HOL/Groebner_Basis.thy Mon Nov 04 20:10:09 2013 +0100
1.2 +++ b/src/HOL/Groebner_Basis.thy Mon Nov 04 20:10:10 2013 +0100
1.3 @@ -10,20 +10,23 @@
1.4
1.5 subsection {* Groebner Bases *}
1.6
1.7 -lemmas bool_simps = simp_thms(1-34)
1.8 +lemmas bool_simps = simp_thms(1-34) -- {* FIXME move to @{theory HOL} *}
1.9 +
1.10 +lemma nnf_simps: -- {* FIXME shadows fact binding in @{theory HOL} *}
1.11 + "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
1.12 + "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
1.13 + "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
1.14 + by blast+
1.15
1.16 lemma dnf:
1.17 - "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))"
1.18 - "(P \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
1.19 + "(P & (Q | R)) = ((P&Q) | (P&R))"
1.20 + "((Q | R) & P) = ((Q&P) | (R&P))"
1.21 + "(P \<and> Q) = (Q \<and> P)"
1.22 + "(P \<or> Q) = (Q \<or> P)"
1.23 by blast+
1.24
1.25 lemmas weak_dnf_simps = dnf bool_simps
1.26
1.27 -lemma nnf_simps:
1.28 - "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
1.29 - "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
1.30 - by blast+
1.31 -
1.32 lemma PFalse:
1.33 "P \<equiv> False \<Longrightarrow> \<not> P"
1.34 "\<not> P \<Longrightarrow> (P \<equiv> False)"
2.1 --- a/src/HOL/Tools/groebner.ML Mon Nov 04 20:10:09 2013 +0100
2.2 +++ b/src/HOL/Tools/groebner.ML Mon Nov 04 20:10:10 2013 +0100
2.3 @@ -21,11 +21,6 @@
2.4 structure Groebner : GROEBNER =
2.5 struct
2.6
2.7 -fun is_comb ct =
2.8 - (case Thm.term_of ct of
2.9 - _ $ _ => true
2.10 - | _ => false);
2.11 -
2.12 val concl = Thm.cprop_of #> Thm.dest_arg;
2.13
2.14 fun is_binop ct ct' =
2.15 @@ -37,8 +32,6 @@
2.16 if is_binop ct ct' then Thm.dest_binop ct'
2.17 else raise CTERM ("dest_binary: bad binop", [ct, ct'])
2.18
2.19 -fun inst_thm inst = Thm.instantiate ([], inst);
2.20 -
2.21 val rat_0 = Rat.zero;
2.22 val rat_1 = Rat.one;
2.23 val minus_rat = Rat.neg;
2.24 @@ -77,10 +70,6 @@
2.25 n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
2.26 end;
2.27
2.28 -fun morder_le m1 m2 = morder_lt m1 m2 orelse (m1 = m2);
2.29 -
2.30 -fun morder_gt m1 m2 = morder_lt m2 m1;
2.31 -
2.32 (* Arithmetic on canonical polynomials. *)
2.33
2.34 fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
2.35 @@ -125,33 +114,9 @@
2.36
2.37 fun grob_pow vars l n =
2.38 if n < 0 then error "grob_pow: negative power"
2.39 - else if n = 0 then [(rat_1,map (fn v => 0) vars)]
2.40 + else if n = 0 then [(rat_1,map (K 0) vars)]
2.41 else grob_mul l (grob_pow vars l (n - 1));
2.42
2.43 -fun degree vn p =
2.44 - case p of
2.45 - [] => error "Zero polynomial"
2.46 -| [(c,ns)] => nth ns vn
2.47 -| (c,ns)::p' => Int.max (nth ns vn, degree vn p');
2.48 -
2.49 -fun head_deg vn p = let val d = degree vn p in
2.50 - (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end;
2.51 -
2.52 -val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
2.53 -val grob_pdiv =
2.54 - let fun pdiv_aux vn (n,a) p k s =
2.55 - if is_zerop s then (k,s) else
2.56 - let val (m,b) = head_deg vn s
2.57 - in if m < n then (k,s) else
2.58 - let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
2.59 - (snd (hd s)))]
2.60 - in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
2.61 - else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
2.62 - end
2.63 - end
2.64 - in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
2.65 - end;
2.66 -
2.67 (* Monomial division operation. *)
2.68
2.69 fun mdiv (c1,m1) (c2,m2) =
2.70 @@ -160,7 +125,7 @@
2.71
2.72 (* Lowest common multiple of two monomials. *)
2.73
2.74 -fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2));
2.75 +fun mlcm (_,m1) (_,m2) = (rat_1, ListPair.map Int.max (m1, m2));
2.76
2.77 (* Reduce monomial cm by polynomial pol, returning replacement for cm. *)
2.78
2.79 @@ -200,8 +165,8 @@
2.80
2.81 fun spoly cm ph1 ph2 =
2.82 case (ph1,ph2) of
2.83 - (([],h),p) => ([],h)
2.84 - | (p,([],h)) => ([],h)
2.85 + (([],h),_) => ([],h)
2.86 + | (_,([],h)) => ([],h)
2.87 | ((cm1::ptl1,his1),(cm2::ptl2,his2)) =>
2.88 (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
2.89 (grob_cmul (mdiv cm cm2) ptl2),
2.90 @@ -218,12 +183,12 @@
2.91
2.92 (* The most popular heuristic is to order critical pairs by LCM monomial. *)
2.93
2.94 -fun forder ((c1,m1),_) ((c2,m2),_) = morder_lt m1 m2;
2.95 +fun forder ((_,m1),_) ((_,m2),_) = morder_lt m1 m2;
2.96
2.97 fun poly_lt p q =
2.98 case (p,q) of
2.99 - (p,[]) => false
2.100 - | ([],q) => true
2.101 + (_,[]) => false
2.102 + | ([],_) => true
2.103 | ((c1,m1)::o1,(c2,m2)::o2) =>
2.104 c1 </ c2 orelse
2.105 c1 =/ c2 andalso ((morder_lt m1 m2) orelse m1 = m2 andalso poly_lt o1 o2);
2.106 @@ -234,7 +199,7 @@
2.107 fun poly_eq p1 p2 =
2.108 eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
2.109
2.110 -fun memx ((p1,h1),(p2,h2)) ppairs =
2.111 +fun memx ((p1,_),(p2,_)) ppairs =
2.112 not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
2.113
2.114 (* Buchberger's second criterion. *)
2.115 @@ -277,7 +242,7 @@
2.116 case pairs of
2.117 [] => basis
2.118 | (l,(p1,p2))::opairs =>
2.119 - let val (sph as (sp,hist)) = monic (reduce basis (spoly l p1 p2))
2.120 + let val (sph as (sp,_)) = monic (reduce basis (spoly l p1 p2))
2.121 in
2.122 if null sp orelse criterion2 basis (l,(p1,p2)) opairs
2.123 then grobner_basis basis opairs
2.124 @@ -324,7 +289,7 @@
2.125
2.126 fun grobner_refute pols =
2.127 let val gb = grobner pols in
2.128 - snd(find (fn (p,h) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb)
2.129 + snd(find (fn (p,_) => length p = 1 andalso forall (fn x=> x=0) (snd(hd p))) gb)
2.130 end;
2.131
2.132 (* Turn proof into a certificate as sum of multipliers. *)
2.133 @@ -366,8 +331,8 @@
2.134
2.135 fun grobner_strong vars pols pol =
2.136 let val vars' = @{cterm "True"}::vars
2.137 - val grob_z = [(rat_1,1::(map (fn x => 0) vars))]
2.138 - val grob_1 = [(rat_1,(map (fn x => 0) vars'))]
2.139 + val grob_z = [(rat_1,1::(map (K 0) vars))]
2.140 + val grob_1 = [(rat_1,(map (K 0) vars'))]
2.141 fun augment p= map (fn (c,m) => (c,0::m)) p
2.142 val pols' = map augment pols
2.143 val pol' = augment pol
2.144 @@ -387,7 +352,7 @@
2.145
2.146 fun refute_disj rfn tm =
2.147 case term_of tm of
2.148 - Const(@{const_name HOL.disj},_)$l$r =>
2.149 + Const(@{const_name HOL.disj},_)$_$_ =>
2.150 Drule.compose
2.151 (refute_disj rfn (Thm.dest_arg tm), 2,
2.152 Drule.compose (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE))
2.153 @@ -398,7 +363,7 @@
2.154
2.155 fun is_neg t =
2.156 case term_of t of
2.157 - (Const(@{const_name Not},_)$p) => true
2.158 + (Const(@{const_name Not},_)$_) => true
2.159 | _ => false;
2.160 fun is_eq t =
2.161 case term_of t of
2.162 @@ -423,7 +388,7 @@
2.163 val strip_exists =
2.164 let fun h (acc, t) =
2.165 case term_of t of
2.166 - Const (@{const_name Ex}, _) $ Abs (x, T, p) =>
2.167 + Const (@{const_name Ex}, _) $ Abs _ =>
2.168 h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
2.169 | _ => (acc,t)
2.170 in fn t => h ([],t)
2.171 @@ -435,10 +400,7 @@
2.172 | _ => false;
2.173
2.174 val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq;
2.175 -val bool_simps = @{thms bool_simps};
2.176 val nnf_simps = @{thms nnf_simps};
2.177 -fun nnf_conv ctxt =
2.178 - Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps bool_simps addsimps nnf_simps)
2.179
2.180 fun weak_dnf_conv ctxt =
2.181 Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms weak_dnf_simps});
2.182 @@ -484,12 +446,10 @@
2.183
2.184 fun fold1 f = foldr1 (uncurry f);
2.185
2.186 -val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
2.187 -
2.188 fun mk_conj_tab th =
2.189 let fun h acc th =
2.190 case prop_of th of
2.191 - @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
2.192 + @{term "Trueprop"}$(@{term HOL.conj}$_$_) =>
2.193 h (h acc (th RS conjunct2)) (th RS conjunct1)
2.194 | @{term "Trueprop"}$p => (p,th)::acc
2.195 in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
2.196 @@ -567,8 +527,7 @@
2.197 | Var ((s,_),_) => s
2.198 | _ => "x"
2.199 fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
2.200 - fun mkeq s t = Thm.apply @{cterm Trueprop} (Thm.apply (Thm.apply @{cterm "op = :: bool => _"} s) t)
2.201 - fun mk_exists v th = Drule.arg_cong_rule (ext (ctyp_of_term v))
2.202 + fun mk_exists v th = Drule.arg_cong_rule (ext (ctyp_of_term v))
2.203 (Thm.abstract_rule (getname v) v th)
2.204 fun simp_ex_conv ctxt =
2.205 Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
2.206 @@ -585,8 +544,8 @@
2.207 (** main **)
2.208
2.209 fun ring_and_ideal_conv
2.210 - {vars, semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules),
2.211 - field = (f_ops, f_rules), idom, ideal}
2.212 + {vars = _, semiring = (sr_ops, _), ring = (r_ops, _),
2.213 + field = (f_ops, _), idom, ideal}
2.214 dest_const mk_const ring_eq_conv ring_normalize_conv =
2.215 let
2.216 val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops;
2.217 @@ -612,7 +571,6 @@
2.218 else raise CTERM ("ring_dest_neg", [t])
2.219 end
2.220
2.221 - val ring_mk_neg = fn tm => Thm.apply (ring_neg_tm) (tm);
2.222 fun field_dest_inv t =
2.223 let val (l,r) = Thm.dest_comb t in
2.224 if Term.could_unify(term_of l, term_of field_inv_tm) then r
2.225 @@ -621,11 +579,9 @@
2.226 val ring_dest_add = dest_binary ring_add_tm;
2.227 val ring_mk_add = mk_binop ring_add_tm;
2.228 val ring_dest_sub = dest_binary ring_sub_tm;
2.229 - val ring_mk_sub = mk_binop ring_sub_tm;
2.230 val ring_dest_mul = dest_binary ring_mul_tm;
2.231 val ring_mk_mul = mk_binop ring_mul_tm;
2.232 val field_dest_div = dest_binary field_div_tm;
2.233 - val field_mk_div = mk_binop field_div_tm;
2.234 val ring_dest_pow = dest_binary ring_pow_tm;
2.235 val ring_mk_pow = mk_binop ring_pow_tm ;
2.236 fun grobvars tm acc =
2.237 @@ -652,7 +608,7 @@
2.238 [(rat_1,map (fn i => if i aconvc tm then 1 else 0) vars)])
2.239 handle CTERM _ =>
2.240 ((let val x = dest_const tm
2.241 - in if x =/ rat_0 then [] else [(x,map (fn v => 0) vars)]
2.242 + in if x =/ rat_0 then [] else [(x,map (K 0) vars)]
2.243 end)
2.244 handle ERROR _ =>
2.245 ((grob_neg(grobify_term vars (ring_dest_neg tm)))
2.246 @@ -732,7 +688,7 @@
2.247 Conv.fconv_rule
2.248 ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
2.249 val conc = th2 |> concl |> Thm.dest_arg
2.250 - val (l,r) = conc |> dest_eq
2.251 + val (l,_) = conc |> dest_eq
2.252 in Thm.implies_intr (Thm.apply cTrp tm)
2.253 (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
2.254 (Thm.reflexive l |> mk_object_eq))
2.255 @@ -756,9 +712,9 @@
2.256 val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr th1) neq_01
2.257 in (vars,l,cert,th2)
2.258 end)
2.259 - val cert_pos = map (fn (i,p) => (i,filter (fn (c,m) => c >/ rat_0) p)) cert
2.260 + val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c >/ rat_0) p)) cert
2.261 val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
2.262 - (filter (fn (c,m) => c </ rat_0) p))) cert
2.263 + (filter (fn (c,_) => c </ rat_0) p))) cert
2.264 val herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
2.265 val herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
2.266 fun thm_fn pols =
2.267 @@ -772,7 +728,7 @@
2.268 val th4 =
2.269 Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
2.270 (neq_rule l th3)
2.271 - val (l,r) = dest_eq(Thm.dest_arg(concl th4))
2.272 + val (l, _) = dest_eq(Thm.dest_arg(concl th4))
2.273 in Thm.implies_intr (Thm.apply cTrp tm)
2.274 (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
2.275 (Thm.reflexive l |> mk_object_eq))
2.276 @@ -873,7 +829,6 @@
2.277 (Drule.binop_cong_rule @{cterm HOL.conj} th1
2.278 (Thm.reflexive (Thm.dest_arg (Thm.rhs_of th2))))
2.279 val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3))
2.280 - val vars' = (remove op aconvc v vars) @ [v]
2.281 val th4 = Conv.fconv_rule (Conv.arg_conv (simp_ex_conv ctxt)) (mk_exists v th3)
2.282 val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4)))
2.283 in Thm.transitive th5 (fold mk_exists (remove op aconvc v vars) th4)
2.284 @@ -961,23 +916,12 @@
2.285 | SOME tm =>
2.286 (case Semiring_Normalizer.match ctxt tm of
2.287 NONE => NONE
2.288 - | SOME (res as (theory, {is_const, dest_const,
2.289 + | SOME (res as (theory, {is_const = _, dest_const,
2.290 mk_const, conv = ring_eq_conv})) =>
2.291 SOME (ring_and_ideal_conv theory
2.292 dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
2.293 (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)))
2.294
2.295 -fun ring_solve ctxt form =
2.296 - (case try (find_term 0 (* FIXME !? *)) form of
2.297 - NONE => Thm.reflexive form
2.298 - | SOME tm =>
2.299 - (case Semiring_Normalizer.match ctxt tm of
2.300 - NONE => Thm.reflexive form
2.301 - | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) =>
2.302 - #ring_conv (ring_and_ideal_conv theory
2.303 - dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt)
2.304 - (Semiring_Normalizer.semiring_normalize_wrapper ctxt res)) ctxt form));
2.305 -
2.306 fun presimplify ctxt add_thms del_thms =
2.307 asm_full_simp_tac (put_simpset HOL_basic_ss ctxt
2.308 addsimps (Algebra_Simplification.get ctxt)
2.309 @@ -1014,7 +958,7 @@
2.310 | SOME thy =>
2.311 let
2.312 fun poly_exists_tac {asms = asms, concl = concl, prems = prems,
2.313 - params = params, context = ctxt, schematics = scs} =
2.314 + params = _, context = ctxt, schematics = _} =
2.315 let
2.316 val (evs,bod) = strip_exists (Thm.dest_arg concl)
2.317 val ps = map_filter (try (lhs o Thm.dest_arg)) asms