dropped dead code
authorhaftmann
Mon Nov 04 20:10:10 2013 +0100 (2013-11-04)
changeset 54251adea9f6986b2
parent 54250 7d2544dd3988
child 54252 a4a00347e59f
dropped dead code
src/HOL/Groebner_Basis.thy
src/HOL/Tools/groebner.ML
     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