# HG changeset patch # User wenzelm # Date 1273236429 -7200 # Node ID 51e3b38a5e412b7d422bf6327c212e90d6f4a264 # Parent 47ba1770da8e4a4464bca536807e01444c916907# Parent 97d2780ad6f0deda2821af15a92f680ed049b3e8 merged diff -r 97d2780ad6f0 -r 51e3b38a5e41 NEWS --- a/NEWS Thu May 06 23:57:55 2010 +0200 +++ b/NEWS Fri May 07 14:47:09 2010 +0200 @@ -140,6 +140,8 @@ *** HOL *** +* Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. + * Theory 'Finite_Set': various folding_* locales facilitate the application of the various fold combinators on finite sets. diff -r 97d2780ad6f0 -r 51e3b38a5e41 doc-src/Locales/Locales/Examples.thy --- a/doc-src/Locales/Locales/Examples.thy Thu May 06 23:57:55 2010 +0200 +++ b/doc-src/Locales/Locales/Examples.thy Fri May 07 14:47:09 2010 +0200 @@ -2,7 +2,6 @@ imports Main begin -hide_const %invisible Lattices.lattice pretty_setmargin %invisible 65 (* diff -r 97d2780ad6f0 -r 51e3b38a5e41 doc-src/Locales/Locales/document/Examples.tex --- a/doc-src/Locales/Locales/document/Examples.tex Thu May 06 23:57:55 2010 +0200 +++ b/doc-src/Locales/Locales/document/Examples.tex Fri May 07 14:47:09 2010 +0200 @@ -25,8 +25,6 @@ \endisadeliminvisible % \isataginvisible -\isacommand{hide{\isacharunderscore}const}\isamarkupfalse% -\ Lattices{\isachardot}lattice\isanewline \isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse% \ {\isadigit{6}}{\isadigit{5}}% \endisataginvisible diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/FOLP/hypsubst.ML --- a/src/FOLP/hypsubst.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/FOLP/hypsubst.ML Fri May 07 14:47:09 2010 +0200 @@ -33,7 +33,7 @@ exception EQ_VAR; -fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); +fun loose (i, t) = member (op =) (add_loose_bnos (t, i, [])) 0; (*It's not safe to substitute for a constant; consider 0=1. It's not safe to substitute for x=t[x] since x is not eliminated. diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/FOLP/simp.ML Fri May 07 14:47:09 2010 +0200 @@ -98,7 +98,7 @@ in var(lhs_of_eq i thm) end; fun contains_op opns = - let fun contains(Const(s,_)) = s mem opns | + let fun contains(Const(s,_)) = member (op =) opns s | contains(s$t) = contains s orelse contains t | contains(Abs(_,_,t)) = contains t | contains _ = false; @@ -117,7 +117,7 @@ in map norm normE_thms end; fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of - Const(s,_)$_ => s mem norms | _ => false; + Const(s,_)$_ => member (op =) norms s | _ => false; val refl_tac = resolve_tac refl_thms; @@ -203,7 +203,7 @@ val refl1_tac = refl_tac 1 fun norm_step_tac st = st |> (case head_of(rhs_of_eq 1 st) of - Var(ixn,_) => if ixn mem hvs then refl1_tac + Var(ixn,_) => if member (op =) hvs ixn then refl1_tac else resolve_tac normI_thms 1 ORELSE refl1_tac | Const _ => resolve_tac normI_thms 1 ORELSE resolve_tac congs 1 ORELSE refl1_tac diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri May 07 14:47:09 2010 +0200 @@ -46,7 +46,7 @@ val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) fun mk_all ((s, T), (P,n)) = - if 0 mem loose_bnos P then + if member (op =) (loose_bnos P) 0 then (HOLogic.all_const T $ Abs (s, T, P), n) else (incr_boundvars ~1 P, n-1) fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri May 07 14:47:09 2010 +0200 @@ -51,7 +51,7 @@ val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) fun mk_all ((s, T), (P,n)) = - if 0 mem loose_bnos P then + if member (op =) (loose_bnos P) 0 then (HOLogic.all_const T $ Abs (s, T, P), n) else (incr_boundvars ~1 P, n-1) fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri May 07 14:47:09 2010 +0200 @@ -66,7 +66,7 @@ val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm) fun mk_all ((s, T), (P,n)) = - if 0 mem loose_bnos P then + if member (op =) (loose_bnos P) 0 then (HOLogic.all_const T $ Abs (s, T, P), n) else (incr_boundvars ~1 P, n-1) fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Fields.thy Fri May 07 14:47:09 2010 +0200 @@ -234,6 +234,18 @@ "1 = a / b \ b \ 0 \ a = b" by (simp add: eq_commute [of 1]) +lemma times_divide_times_eq: + "(x / y) * (z / w) = (x * z) / (y * w)" + by simp + +lemma add_frac_num: + "y \ 0 \ x / y + z = (x + z * y) / y" + by (simp add: add_divide_distrib) + +lemma add_num_frac: + "y \ 0 \ z + x / y = (x + z * y) / y" + by (simp add: add_divide_distrib add.commute) + end diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Groebner_Basis.thy Fri May 07 14:47:09 2010 +0200 @@ -5,20 +5,17 @@ header {* Semiring normalization and Groebner Bases *} theory Groebner_Basis -imports Numeral_Simprocs +imports Numeral_Simprocs Nat_Transfer uses - "Tools/Groebner_Basis/misc.ML" - "Tools/Groebner_Basis/normalizer_data.ML" - ("Tools/Groebner_Basis/normalizer.ML") + "Tools/Groebner_Basis/normalizer.ML" ("Tools/Groebner_Basis/groebner.ML") begin subsection {* Semiring normalization *} -setup NormalizerData.setup +setup Normalizer.setup - -locale gb_semiring = +locale normalizing_semiring = fixes add mul pwr r0 r1 assumes add_a:"(add x (add y z) = add (add x y) z)" and add_c: "add x y = add y x" and add_0:"add r0 x = x" @@ -59,9 +56,6 @@ thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc) qed - -subsubsection {* Declaring the abstract theory *} - lemma semiring_ops: shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)" and "TERM r0" and "TERM r1" . @@ -156,71 +150,21 @@ qed -lemmas gb_semiring_axioms' = - gb_semiring_axioms [normalizer +lemmas normalizing_semiring_axioms' = + normalizing_semiring_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules] end -interpretation class_semiring: gb_semiring - "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1" - proof qed (auto simp add: algebra_simps) - -lemmas nat_arith = - add_nat_number_of - diff_nat_number_of - mult_nat_number_of - eq_nat_number_of - less_nat_number_of - -lemma not_iszero_Numeral1: "\ iszero (Numeral1::'a::number_ring)" - by simp - -lemmas comp_arith = - Let_def arith_simps nat_arith rel_simps neg_simps if_False - if_True add_0 add_Suc add_number_of_left mult_number_of_left - numeral_1_eq_1[symmetric] Suc_eq_plus1 - numeral_0_eq_0[symmetric] numerals[symmetric] - iszero_simps not_iszero_Numeral1 - -lemmas semiring_norm = comp_arith - -ML {* -local - -open Conv; +sublocale comm_semiring_1 + < normalizing!: normalizing_semiring plus times power zero one +proof +qed (simp_all add: algebra_simps) -fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct); - -fun int_of_rat x = - (case Rat.quotient_of_rat x of (i, 1) => i - | _ => error "int_of_rat: bad int"); - -val numeral_conv = - Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) then_conv - Simplifier.rewrite (HOL_basic_ss addsimps - (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)})); - -in +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_semiring_axioms'} *} -fun normalizer_funs key = - NormalizerData.funs key - {is_const = fn phi => numeral_is_const, - dest_const = fn phi => fn ct => - Rat.rat_of_int (snd - (HOLogic.dest_number (Thm.term_of ct) - handle TERM _ => error "ring_dest_const")), - mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT (int_of_rat x), - conv = fn phi => K numeral_conv} - -end -*} - -declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms'} *} - - -locale gb_ring = gb_semiring + +locale normalizing_ring = normalizing_semiring + fixes sub :: "'a \ 'a \ 'a" and neg :: "'a \ 'a" assumes neg_mul: "neg x = mul (neg r1) x" @@ -231,8 +175,8 @@ lemmas ring_rules = neg_mul sub_add -lemmas gb_ring_axioms' = - gb_ring_axioms [normalizer +lemmas normalizing_ring_axioms' = + normalizing_ring_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops @@ -240,23 +184,14 @@ end - -interpretation class_ring: gb_ring "op +" "op *" "op ^" - "0::'a::{comm_semiring_1,number_ring}" 1 "op -" "uminus" - proof qed simp_all - - -declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *} +sublocale comm_ring_1 + < normalizing!: normalizing_ring plus times power zero one minus uminus +proof +qed (simp_all add: diff_minus) -use "Tools/Groebner_Basis/normalizer.ML" - +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_axioms'} *} -method_setup sring_norm = {* - Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac) -*} "semiring normalizer" - - -locale gb_field = gb_ring + +locale normalizing_field = normalizing_ring + fixes divide :: "'a \ 'a \ 'a" and inverse:: "'a \ 'a" assumes divide_inverse: "divide x y = mul x (inverse y)" @@ -267,8 +202,8 @@ lemmas field_rules = divide_inverse inverse_divide -lemmas gb_field_axioms' = - gb_field_axioms [normalizer +lemmas normalizing_field_axioms' = + normalizing_field_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops @@ -278,10 +213,7 @@ end - -subsection {* Groebner Bases *} - -locale semiringb = gb_semiring + +locale normalizing_semiring_cancel = normalizing_semiring + assumes add_cancel: "add (x::'a) y = add x z \ y = z" and add_mul_solve: "add (mul w y) (mul x z) = add (mul w z) (mul x y) \ w = x \ y = z" @@ -313,22 +245,23 @@ thus "x = add x a \ a = r0" by (auto simp add: add_c add_0) qed -declare gb_semiring_axioms' [normalizer del] +declare normalizing_semiring_axioms' [normalizer del] -lemmas semiringb_axioms' = semiringb_axioms [normalizer - semiring ops: semiring_ops - semiring rules: semiring_rules - idom rules: noteq_reduce add_scale_eq_noteq] +lemmas normalizing_semiring_cancel_axioms' = + normalizing_semiring_cancel_axioms [normalizer + semiring ops: semiring_ops + semiring rules: semiring_rules + idom rules: noteq_reduce add_scale_eq_noteq] end -locale ringb = semiringb + gb_ring + +locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring + assumes subr0_iff: "sub x y = r0 \ x = y" begin -declare gb_ring_axioms' [normalizer del] +declare normalizing_ring_axioms' [normalizer del] -lemmas ringb_axioms' = ringb_axioms [normalizer +lemmas normalizing_ring_cancel_axioms' = normalizing_ring_cancel_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops @@ -338,33 +271,24 @@ end - -lemma no_zero_divirors_neq0: - assumes az: "(a::'a::no_zero_divisors) \ 0" - and ab: "a*b = 0" shows "b = 0" -proof - - { assume bz: "b \ 0" - from no_zero_divisors [OF az bz] ab have False by blast } - thus "b = 0" by blast -qed +sublocale idom + < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus +proof + fix w x y z + show "w * y + x * z = w * z + x * y \ w = x \ y = z" + proof + assume "w * y + x * z = w * z + x * y" + then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps) + then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) + then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps) + then have "y - z = 0 \ w - x = 0" by (rule divisors_zero) + then show "w = x \ y = z" by auto + qed (auto simp add: add_ac) +qed (simp_all add: algebra_simps) -interpretation class_ringb: ringb - "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus" -proof(unfold_locales, simp add: algebra_simps, auto) - fix w x y z ::"'a::{idom,number_ring}" - assume p: "w * y + x * z = w * z + x * y" and ynz: "y \ z" - hence ynz': "y - z \ 0" by simp - from p have "w * y + x* z - w*z - x*y = 0" by simp - hence "w* (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) - hence "(y - z) * (w - x) = 0" by (simp add: algebra_simps) - with no_zero_divirors_neq0 [OF ynz'] - have "w - x = 0" by blast - thus "w = x" by simp -qed +declaration {* Normalizer.semiring_funs @{thm normalizing.normalizing_ring_cancel_axioms'} *} -declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *} - -interpretation natgb: semiringb +interpretation normalizing_nat!: normalizing_semiring_cancel "op +" "op *" "op ^" "0::nat" "1" proof (unfold_locales, simp add: algebra_simps) fix w x y z ::"nat" @@ -386,14 +310,14 @@ thus "(w * y + x * z = w * z + x * y) = (w = x \ y = z)" by auto qed -declaration {* normalizer_funs @{thm natgb.semiringb_axioms'} *} +declaration {* Normalizer.semiring_funs @{thm normalizing_nat.normalizing_semiring_cancel_axioms'} *} -locale fieldgb = ringb + gb_field +locale normalizing_field_cancel = normalizing_ring_cancel + normalizing_field begin -declare gb_field_axioms' [normalizer del] +declare normalizing_field_axioms' [normalizer del] -lemmas fieldgb_axioms' = fieldgb_axioms [normalizer +lemmas normalizing_field_cancel_axioms' = normalizing_field_cancel_axioms [normalizer semiring ops: semiring_ops semiring rules: semiring_rules ring ops: ring_ops @@ -405,8 +329,18 @@ end +sublocale field + < normalizing!: normalizing_field_cancel plus times power zero one minus uminus divide inverse +proof +qed (simp_all add: divide_inverse) + +declaration {* Normalizer.field_funs @{thm normalizing.normalizing_field_cancel_axioms'} *} + + +subsection {* Groebner Bases *} lemmas bool_simps = simp_thms(1-34) + lemma dnf: "(P & (Q | R)) = ((P&Q) | (P&R))" "((Q | R) & P) = ((Q&P) | (R&P))" "(P \ Q) = (Q \ P)" "(P \ Q) = (Q \ P)" @@ -423,23 +357,16 @@ "P \ False \ \ P" "\ P \ (P \ False)" by auto -use "Tools/Groebner_Basis/groebner.ML" -method_setup algebra = -{* -let - fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () - val addN = "add" - val delN = "del" - val any_keyword = keyword addN || keyword delN - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -in - ((Scan.optional (keyword addN |-- thms) []) -- - (Scan.optional (keyword delN |-- thms) [])) >> - (fn (add_ths, del_ths) => fn ctxt => - SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt)) -end -*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" +ML {* +structure Algebra_Simplification = Named_Thms( + val name = "algebra" + val description = "pre-simplification rules for algebraic methods" +) +*} + +setup Algebra_Simplification.setup + declare dvd_def[algebra] declare dvd_eq_mod_eq_0[symmetric, algebra] declare mod_div_trivial[algebra] @@ -468,222 +395,9 @@ declare zmod_eq_dvd_iff[algebra] declare nat_mod_eq_iff[algebra] -subsection{* Groebner Bases for fields *} - -interpretation class_fieldgb: - fieldgb "op +" "op *" "op ^" "0::'a::{field,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse) - -lemma divide_Numeral1: "(x::'a::{field, number_ring}) / Numeral1 = x" by simp -lemma divide_Numeral0: "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0" - by simp -lemma mult_frac_frac: "((x::'a::field_inverse_zero) / y) * (z / w) = (x*z) / (y*w)" - by simp -lemma mult_frac_num: "((x::'a::field_inverse_zero) / y) * z = (x*z) / y" - by simp -lemma mult_num_frac: "((x::'a::field_inverse_zero) / y) * z = (x*z) / y" - by simp - -lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp - -lemma add_frac_num: "y\ 0 \ (x::'a::field_inverse_zero) / y + z = (x + z*y) / y" - by (simp add: add_divide_distrib) -lemma add_num_frac: "y\ 0 \ z + (x::'a::field_inverse_zero) / y = (x + z*y) / y" - by (simp add: add_divide_distrib) - -ML {* -let open Conv -in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym) -end -*} - -ML{* -local - val zr = @{cpat "0"} - val zT = ctyp_of_term zr - val geq = @{cpat "op ="} - val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd - val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} - val add_frac_num = mk_meta_eq @{thm "add_frac_num"} - val add_num_frac = mk_meta_eq @{thm "add_num_frac"} - - fun prove_nz ss T t = - let - val z = instantiate_cterm ([(zT,T)],[]) zr - val eq = instantiate_cterm ([(eqT,T)],[]) geq - val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) - (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} - (Thm.capply (Thm.capply eq t) z))) - in equal_elim (symmetric th) TrueI - end - - fun proc phi ss ct = - let - val ((x,y),(w,z)) = - (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct - val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] - val T = ctyp_of_term x - val [y_nz, z_nz] = map (prove_nz ss T) [y, z] - val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq - in SOME (implies_elim (implies_elim th y_nz) z_nz) - end - handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - - fun proc2 phi ss ct = - let - val (l,r) = Thm.dest_binop ct - val T = ctyp_of_term l - in (case (term_of l, term_of r) of - (Const(@{const_name Rings.divide},_)$_$_, _) => - let val (x,y) = Thm.dest_binop l val z = r - val _ = map (HOLogic.dest_number o term_of) [x,y,z] - val ynz = prove_nz ss T y - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) - end - | (_, Const (@{const_name Rings.divide},_)$_$_) => - let val (x,y) = Thm.dest_binop r val z = l - val _ = map (HOLogic.dest_number o term_of) [x,y,z] - val ynz = prove_nz ss T y - in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) - end - | _ => NONE) - end - handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - - fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b - | is_number t = can HOLogic.dest_number t - - val is_number = is_number o term_of +use "Tools/Groebner_Basis/groebner.ML" - fun proc3 phi ss ct = - (case term_of ct of - Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} - in SOME (mk_meta_eq th) end - | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => - let - val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} - in SOME (mk_meta_eq th) end - | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} - in SOME (mk_meta_eq th) end - | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) => - let - val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop - val _ = map is_number [a,b,c] - val T = ctyp_of_term c - val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} - in SOME (mk_meta_eq th) end - | _ => NONE) - handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE - -val add_frac_frac_simproc = - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], - name = "add_frac_frac_simproc", - proc = proc, identifier = []} - -val add_frac_num_simproc = - make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], - name = "add_frac_num_simproc", - proc = proc2, identifier = []} - -val ord_frac_simproc = - make_simproc - {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, - @{cpat "(?a::(?'a::{field, ord}))/?b \ ?c"}, - @{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, - @{cpat "?c \ (?a::(?'a::{field, ord}))/?b"}, - @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, - @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], - name = "ord_frac_simproc", proc = proc3, identifier = []} - -local -open Conv -in - -val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, - @{thm "divide_Numeral1"}, - @{thm "divide_zero"}, @{thm "divide_Numeral0"}, - @{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"}, - @{thm "mult_num_frac"}, @{thm "mult_frac_num"}, - @{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"}, - @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, - @{thm "diff_def"}, @{thm "minus_divide_left"}, - @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, - @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, - fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) - (@{thm field_divide_inverse} RS sym)] - -val comp_conv = (Simplifier.rewrite -(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} - addsimps ths addsimps @{thms simp_thms} - addsimprocs Numeral_Simprocs.field_cancel_numeral_factors - addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, - ord_frac_simproc] - addcongs [@{thm "if_weak_cong"}])) -then_conv (Simplifier.rewrite (HOL_basic_ss addsimps - [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})) -end - -fun numeral_is_const ct = - case term_of ct of - Const (@{const_name Rings.divide},_) $ a $ b => - can HOLogic.dest_number a andalso can HOLogic.dest_number b - | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t - | t => can HOLogic.dest_number t - -fun dest_const ct = ((case term_of ct of - Const (@{const_name Rings.divide},_) $ a $ b=> - Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) - | Const (@{const_name Rings.inverse},_)$t => - Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) - | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) - handle TERM _ => error "ring_dest_const") - -fun mk_const phi cT x = - let val (a, b) = Rat.quotient_of_rat x - in if b = 1 then Numeral.mk_cnumber cT a - else Thm.capply - (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) - (Numeral.mk_cnumber cT a)) - (Numeral.mk_cnumber cT b) - end - -in - val field_comp_conv = comp_conv; - val fieldgb_declaration = - NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms'} - {is_const = K numeral_is_const, - dest_const = K dest_const, - mk_const = mk_const, - conv = K (K comp_conv)} -end; -*} - -declaration fieldgb_declaration +method_setup algebra = Groebner.algebra_method + "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases" end diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/HOL.thy Fri May 07 14:47:09 2010 +0200 @@ -1963,7 +1963,7 @@ text {* Avoid some named infixes in evaluation environment *} -code_reserved Eval oo ooo oooo upto downto orf andf mem mem_int mem_string +code_reserved Eval oo ooo oooo upto downto orf andf setup {* Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Import/hol4rews.ML Fri May 07 14:47:09 2010 +0200 @@ -604,9 +604,9 @@ val defname = Thm.def_name name val pdefname = name ^ "_primdef" in - if not (defname mem used) + if not (member (op =) used defname) then F defname (* name_def *) - else if not (pdefname mem used) + else if not (member (op =) used pdefname) then F pdefname (* name_primdef *) else F (Name.variant used pdefname) (* last resort *) end diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Fri May 07 14:47:09 2010 +0200 @@ -276,6 +276,7 @@ in F end +infix mem; fun i mem L = let fun itr [] = false | itr (a::rst) = i=a orelse itr rst @@ -1091,7 +1092,7 @@ let fun F vars (Bound _) = vars | F vars (tm as Free _) = - if tm mem vars + if member (op =) vars tm then vars else (tm::vars) | F vars (Const _) = vars diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Import/shuffler.ML Fri May 07 14:47:09 2010 +0200 @@ -550,7 +550,7 @@ fun match_consts ignore t (* th *) = let fun add_consts (Const (c, _), cs) = - if c mem_string ignore + if member (op =) ignore c then cs else insert (op =) c cs | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Int.thy --- a/src/HOL/Int.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Int.thy Fri May 07 14:47:09 2010 +0200 @@ -1063,20 +1063,24 @@ text {* First version by Norbert Voelker *} -definition (*for simplifying equalities*) - iszero :: "'a\semiring_1 \ bool" -where +definition (*for simplifying equalities*) iszero :: "'a\semiring_1 \ bool" where "iszero z \ z = 0" lemma iszero_0: "iszero 0" -by (simp add: iszero_def) - -lemma not_iszero_1: "~ iszero 1" -by (simp add: iszero_def eq_commute) + by (simp add: iszero_def) + +lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)" + by (simp add: iszero_0) + +lemma not_iszero_1: "\ iszero 1" + by (simp add: iszero_def) + +lemma not_iszero_Numeral1: "\ iszero (Numeral1 :: 'a::number_ring)" + by (simp add: not_iszero_1) lemma eq_number_of_eq [simp]: "((number_of x::'a::number_ring) = number_of y) = - iszero (number_of (x + uminus y) :: 'a)" + iszero (number_of (x + uminus y) :: 'a)" unfolding iszero_def number_of_add number_of_minus by (simp add: algebra_simps) @@ -2021,6 +2025,14 @@ lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard] +lemma divide_Numeral1: + "(x::'a::{field, number_ring}) / Numeral1 = x" + by simp + +lemma divide_Numeral0: + "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0" + by simp + subsection {* The divides relation *} diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/IsaMakefile Fri May 07 14:47:09 2010 +0200 @@ -284,9 +284,7 @@ Tools/ATP_Manager/atp_manager.ML \ Tools/ATP_Manager/atp_systems.ML \ Tools/Groebner_Basis/groebner.ML \ - Tools/Groebner_Basis/misc.ML \ Tools/Groebner_Basis/normalizer.ML \ - Tools/Groebner_Basis/normalizer_data.ML \ Tools/choice_specification.ML \ Tools/int_arith.ML \ Tools/list_code.ML \ diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Fri May 07 14:47:09 2010 +0200 @@ -93,6 +93,25 @@ shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) +lemma [quot_respect]: + shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> + prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" + by auto + +lemma [quot_preserve]: + assumes q1: "Quotient R1 abs1 rep1" + and q2: "Quotient R2 abs2 rep2" + shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> + prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel" + by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + +lemma [quot_preserve]: + shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) + (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \ R2 (rep2 l2) (rep2 r2))" + by simp + +declare Pair_eq[quot_preserve] + lemma prod_fun_id[id_simps]: shows "prod_fun id id = id" by (simp add: prod_fun_def) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri May 07 14:47:09 2010 +0200 @@ -528,8 +528,8 @@ end end; -fun isspace x = x = " " ; -fun isnum x = x mem_string ["0","1","2","3","4","5","6","7","8","9"] +fun isspace x = (x = " "); +fun isnum x = member (op =) ["0","1","2","3","4","5","6","7","8","9"] x; (* More parser basics. *) @@ -1195,7 +1195,7 @@ fun real_nonlinear_prover proof_method ctxt = let val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) @@ -1222,7 +1222,7 @@ in (let val th = tryfind trivial_axiom (keq @ klep @ kltp) in - (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, RealArith.Trivial) + (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv Normalizer.field_comp_conv) th, RealArith.Trivial) end) handle Failure _ => (let val proof = @@ -1310,7 +1310,7 @@ fun real_nonlinear_subst_prover prover ctxt = let val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Library/normarith.ML Fri May 07 14:47:09 2010 +0200 @@ -167,8 +167,8 @@ (* FIXME : Should be computed statically!! *) val real_poly_conv = Normalizer.semiring_normalize_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) - in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv))) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) + in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Normalizer.field_comp_conv then_conv real_poly_conv))) end; fun absc cv ct = case term_of ct of @@ -190,8 +190,8 @@ val apply_pth5 = rewr_conv @{thm pth_5}; val apply_pth6 = rewr_conv @{thm pth_6}; val apply_pth7 = rewrs_conv @{thms pth_7}; - val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); - val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv); + val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Normalizer.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); + val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Normalizer.field_comp_conv); val apply_ptha = rewr_conv @{thm pth_a}; val apply_pthb = rewrs_conv @{thms pth_b}; val apply_pthc = rewrs_conv @{thms pth_c}; @@ -204,7 +204,7 @@ | _ => error "headvector: non-canonical term" fun vector_cmul_conv ct = - ((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv + ((apply_pth5 then_conv arg1_conv Normalizer.field_comp_conv) else_conv (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct fun vector_add_conv ct = apply_pth7 ct @@ -278,7 +278,7 @@ (* FIXME: Should be computed statically!!*) val real_poly_conv = Normalizer.semiring_normalize_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" @@ -311,7 +311,7 @@ in forall (fn e => evaluate f e =/ Rat.zero) flippedequations end val goodverts = filter check_solution rawverts - val signfixups = map (fn n => if n mem_int f then ~1 else 1) nvs + val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts end val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) [] @@ -384,7 +384,7 @@ let val real_poly_neg_conv = #neg (Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) val (th1,th2) = conj_pair(rawrule th) in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc end @@ -396,7 +396,7 @@ fun init_conv ctxt = Simplifier.rewrite (Simplifier.context ctxt (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) - then_conv field_comp_conv + then_conv Normalizer.field_comp_conv then_conv nnf_conv fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Fri May 07 14:47:09 2010 +0200 @@ -748,10 +748,10 @@ fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt - (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) + (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord in gen_real_arith ctxt - (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv, + (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv, main,neg,add,mul, prover) end; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Library/reflection.ML Fri May 07 14:47:09 2010 +0200 @@ -149,7 +149,7 @@ Pattern.match thy ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) (Vartab.empty, Vartab.empty) - val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) + val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv) val (fts,its) = (map (snd o snd) fnvs, map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Metis_Examples/BT.thy --- a/src/HOL/Metis_Examples/BT.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Metis_Examples/BT.thy Fri May 07 14:47:09 2010 +0200 @@ -88,7 +88,7 @@ case Lf thus ?case by (metis reflect.simps(1)) next case (Br a t1 t2) thus ?case - by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2)) + by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2)) qed declare [[ atp_problem_prefix = "BT__depth_reflect" ]] diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Metis_Examples/BigO.thy --- a/src/HOL/Metis_Examples/BigO.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Metis_Examples/BigO.thy Fri May 07 14:47:09 2010 +0200 @@ -41,7 +41,7 @@ fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" have F1: "\x\<^isub>1\'a\linordered_idom. 0 \ \x\<^isub>1\" by (metis abs_ge_zero) - have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F3: "\x\<^isub>1 x\<^isub>3. x\<^isub>3 \ \h x\<^isub>1\ \ x\<^isub>3 \ c * \f x\<^isub>1\" by (metis A1 order_trans) have F4: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" by (metis abs_mult) @@ -70,7 +70,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F2: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" by (metis abs_mult) have "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_mult_pos abs_one) @@ -92,7 +92,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F2: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" by (metis abs_mult_pos) hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_one) hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F2 A1 abs_ge_zero order_trans) @@ -111,7 +111,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) @@ -145,12 +145,12 @@ declare [[ atp_problem_prefix = "BigO__bigo_refl" ]] lemma bigo_refl [intro]: "f : O(f)" apply (auto simp add: bigo_def) -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) declare [[ atp_problem_prefix = "BigO__bigo_zero" ]] lemma bigo_zero: "0 : O(g)" apply (auto simp add: bigo_def func_zero) -by (metis class_semiring.mul_0 order_refl) +by (metis normalizing.mul_0 order_refl) lemma bigo_zero2: "O(%x.0) = {%x.0}" apply (auto simp add: bigo_def) @@ -307,7 +307,7 @@ apply (auto simp add: diff_minus fun_Compl_def func_plus) prefer 2 apply (drule_tac x = x in spec)+ - apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans) + apply (metis add_right_mono normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans) proof - fix x :: 'a assume "\x. lb x \ f x" @@ -318,13 +318,13 @@ lemma bigo_abs: "(%x. abs(f x)) =o O(f)" apply (unfold bigo_def) apply auto -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]] lemma bigo_abs2: "f =o O(%x. abs(f x))" apply (unfold bigo_def) apply auto -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) lemma bigo_abs3: "O(f) = O(%x. abs(f x))" proof - diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Fri May 07 14:47:09 2010 +0200 @@ -921,7 +921,7 @@ check_finity gl bl ((t,cl)::r) b = let fun listmem [] _ = true | -listmem (a::r) l = if (a mem l) then (listmem r l) else false; +listmem (a::r) l = if member (op =) l a then (listmem r l) else false; fun snd_listmem [] _ = true | snd_listmem ((a,b)::r) l = if (listmem b l) then (snd_listmem r l) else false; in @@ -966,7 +966,7 @@ (ll @ (new_types r)) end; in - if (a mem done) + if member (op =) done a then (preprocess_td sg b done) else (let diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 07 14:47:09 2010 +0200 @@ -1877,7 +1877,7 @@ using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR apply (rule mult_left_le_imp_le[of "1 - u"]) - unfolding class_semiring.mul_a using `u<1` by auto + unfolding normalizing.mul_a using `u<1` by auto thus "y \ s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u] using as unfolding scaleR_scaleR by auto qed auto thus "u *\<^sub>R x \ s - frontier s" using frontier_def and interior_subset by auto qed @@ -2231,7 +2231,7 @@ apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof fix z assume z:"z\{x - ?d..x + ?d}" have e:"e = setsum (\i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1 - by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) + by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) show "dist x z \ e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono) using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed hence k:"\y\{x - ?d..x + ?d}. f y \ k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri May 07 14:47:09 2010 +0200 @@ -698,7 +698,7 @@ unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto then guess x .. note x=this show ?thesis proof(cases "f a = f b") - case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:class_semiring.semiring_rules) + case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:normalizing.semiring_rules) also have "\ = (f b - f a) \ (f b - f a)" unfolding power2_norm_eq_inner .. also have "\ = (f b - f a) \ f' x (b - a)" using x unfolding inner_simps by auto also have "\ \ norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz) @@ -810,7 +810,7 @@ guess k using real_lbound_gt_zero[OF d[THEN conjunct1] d'[THEN conjunct1]] .. note k=this show ?case apply(rule_tac x=k in exI,rule) defer proof(rule,rule) fix z assume as:"norm(z - y) < k" hence "norm (g z - g y - g' (z - y)) \ e / B * norm(g z - g y)" using d' k by auto - also have "\ \ e * norm(z - y)" unfolding mult_frac_num pos_divide_le_eq[OF `B>0`] + also have "\ \ e * norm(z - y)" unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`] using lem2[THEN spec[where x=z]] using k as using `e>0` by(auto simp add:field_simps) finally show "norm (g z - g y - g' (z - y)) \ e * norm (z - y)" by simp qed(insert k, auto) qed qed diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 07 14:47:09 2010 +0200 @@ -2533,7 +2533,7 @@ show "content x \ 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le) qed have **:"norm (1::real) \ 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit] note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]] - note this[unfolded real_scaleR_def real_norm_def class_semiring.semiring_rules, of k c d] note le_less_trans[OF this d(2)] + note this[unfolded real_scaleR_def real_norm_def normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)] from this[unfolded abs_of_nonneg[OF *]] show "(\ka\snd ` p. content (ka \ {x. \x $ k - c\ \ d})) < e" apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym]) apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p''] @@ -4723,7 +4723,7 @@ have "\e sg dsa dia ig. norm(sg) \ dsa \ abs(dsa - dia) < e / 2 \ norm(sg - ig) < e / 2 \ norm(ig) < dia + e" proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]]) - apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a + apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1) apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith qed note norm=this[rule_format] diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle.ML Fri May 07 14:47:09 2010 +0200 @@ -361,7 +361,7 @@ val t' = canonize_term t comms; val u' = canonize_term u comms; in - if s mem comms andalso Term_Ord.termless (u', t') + if member (op =) comms s andalso Term_Ord.termless (u', t') then Const (s, T) $ u' $ t' else Const (s, T) $ t' $ u' end diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri May 07 14:47:09 2010 +0200 @@ -218,8 +218,8 @@ fun is_forbidden_theorem (s, th) = let val consts = Term.add_const_names (prop_of th) [] in - exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse - exists (fn s' => s' mem forbidden_consts) consts orelse + exists (member (op =) (space_explode "." s)) forbidden_thms orelse + exists (member (op =) forbidden_consts) consts orelse length (space_explode "." s) <> 2 orelse String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse String.isSuffix "_def" s orelse diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Nat_Numeral.thy Fri May 07 14:47:09 2010 +0200 @@ -319,6 +319,10 @@ lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)" by (simp add: nat_number_of_def) +lemma Numeral1_eq1_nat: + "(1::nat) = Numeral1" + by simp + lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0" by (simp only: nat_numeral_1_eq_1 One_nat_def) @@ -687,6 +691,20 @@ lemmas nat_number' = nat_number_of_Bit0 nat_number_of_Bit1 +lemmas nat_arith = + add_nat_number_of + diff_nat_number_of + mult_nat_number_of + eq_nat_number_of + less_nat_number_of + +lemmas semiring_norm = + Let_def arith_simps nat_arith rel_simps neg_simps if_False + if_True add_0 add_Suc add_number_of_left mult_number_of_left + numeral_1_eq_1 [symmetric] Suc_eq_plus1 + numeral_0_eq_0 [symmetric] numerals [symmetric] + iszero_simps not_iszero_Numeral1 + lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" by (fact Let_def) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri May 07 14:47:09 2010 +0200 @@ -66,7 +66,7 @@ fun mk_case_names_exhausts descr new = map (Rule_Cases.case_names o exhaust_cases descr o #1) - (filter (fn ((_, (name, _, _))) => name mem_string new) descr); + (filter (fn ((_, (name, _, _))) => member (op =) new name) descr); end; @@ -131,7 +131,7 @@ let val (aT as Type (a, []), S) = dest_permT T; val (bT as Type (b, []), _) = dest_permT U - in if aT mem permTs_of u andalso aT <> bT then + in if member (op =) (permTs_of u) aT andalso aT <> bT then let val cp = cp_inst_of thy a b; val dj = dj_thm_of thy b a; @@ -1772,7 +1772,7 @@ val params' = params1 @ params2; val rec_prems = filter (fn th => case prop_of th of _ $ p => (case head_of p of - Const (s, _) => s mem rec_set_names + Const (s, _) => member (op =) rec_set_names s | _ => false) | _ => false) prems'; val fresh_prems = filter (fn th => case prop_of th of diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri May 07 14:47:09 2010 +0200 @@ -43,7 +43,7 @@ fun mk_perm_bool_simproc names = Simplifier.simproc_i (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss => fn Const ("Nominal.perm", _) $ _ $ t => - if the_default "" (try (head_of #> dest_Const #> fst) t) mem names + if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE | _ => NONE); @@ -73,7 +73,7 @@ fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of Const (name, _) => - if name mem names then SOME (f p q) else NONE + if member (op =) names name then SOME (f p q) else NONE | _ => NONE) | split_conj _ _ _ _ = NONE; @@ -92,7 +92,7 @@ fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ = (case head_of p of Const (name, _) => - if name mem names then SOME (HOLogic.mk_conj (p, + if member (op =) names name then SOME (HOLogic.mk_conj (p, Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ (subst_bounds (pis, strip_all pis q)))) else NONE @@ -214,7 +214,7 @@ fun lift_prem (t as (f $ u)) = let val (p, ts) = strip_comb t in - if p mem ps then + if member (op =) ps p then Const (inductive_forall_name, (fsT --> HOLogic.boolT) --> HOLogic.boolT) $ Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) @@ -510,7 +510,7 @@ val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis); val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms (fn x as Free _ => - if x mem args then x + if member (op =) args x then x else (case AList.lookup op = tab x of SOME y => y | NONE => fold_rev (NominalDatatype.mk_perm []) pis x) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri May 07 14:47:09 2010 +0200 @@ -46,7 +46,7 @@ fun mk_perm_bool_simproc names = Simplifier.simproc_i (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss => fn Const ("Nominal.perm", _) $ _ $ t => - if the_default "" (try (head_of #> dest_Const #> fst) t) mem names + if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE | _ => NONE); @@ -77,7 +77,7 @@ fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of Const (name, _) => - if name mem names then SOME (f p q) else NONE + if member (op =) names name then SOME (f p q) else NONE | _ => NONE) | split_conj _ _ _ _ = NONE; @@ -96,7 +96,7 @@ fun inst_conj_all names ps pis (Const ("op &", _) $ p $ q) _ = (case head_of p of Const (name, _) => - if name mem names then SOME (HOLogic.mk_conj (p, + if member (op =) names name then SOME (HOLogic.mk_conj (p, Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $ (subst_bounds (pis, strip_all pis q)))) else NONE @@ -239,7 +239,7 @@ fun lift_prem (t as (f $ u)) = let val (p, ts) = strip_comb t in - if p mem ps then + if member (op =) ps p then Const (inductive_forall_name, (fsT --> HOLogic.boolT) --> HOLogic.boolT) $ Abs ("z", fsT, lift_pred p (map (incr_boundvars 1) ts)) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/PReal.thy --- a/src/HOL/PReal.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/PReal.thy Fri May 07 14:47:09 2010 +0200 @@ -47,10 +47,6 @@ by (blast intro: cut_of_rat [OF zero_less_one]) definition - preal_of_rat :: "rat => preal" where - "preal_of_rat q = Abs_preal {x::rat. 0 < x & x < q}" - -definition psup :: "preal set => preal" where [code del]: "psup P = Abs_preal (\X \ P. Rep_preal X)" @@ -101,7 +97,7 @@ definition preal_one_def: - "1 == preal_of_rat 1" + "1 == Abs_preal {x. 0 < x & x < 1}" instance .. @@ -172,25 +168,6 @@ lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal] - -subsection{*@{term preal_of_prat}: the Injection from prat to preal*} - -lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \ preal" -by (simp add: preal_def cut_of_rat) - -lemma rat_subset_imp_le: - "[|{u::rat. 0 < u & u < x} \ {u. 0 < u & u < y}; 0 x \ y" -apply (simp add: linorder_not_less [symmetric]) -apply (blast dest: dense intro: order_less_trans) -done - -lemma rat_set_eq_imp_eq: - "[|{u::rat. 0 < u & u < x} = {u. 0 < u & u < y}; - 0 < x; 0 < y|] ==> x = y" -by (blast intro: rat_subset_imp_le order_antisym) - - - subsection{*Properties of Ordering*} instance preal :: order @@ -355,12 +332,6 @@ show "a + b = b + a" by (rule preal_add_commute) qed -lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)" -by (rule add_left_commute) - -text{* Positive Real addition is an AC operator *} -lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute - subsection{*Properties of Multiplication*} @@ -490,19 +461,10 @@ show "a * b = b * a" by (rule preal_mult_commute) qed -lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)" -by (rule mult_left_commute) - - -text{* Positive Real multiplication is an AC operator *} -lemmas preal_mult_ac = - preal_mult_assoc preal_mult_commute preal_mult_left_commute - text{* Positive real 1 is the multiplicative identity element *} lemma preal_mult_1: "(1::preal) * z = z" -unfolding preal_one_def proof (induct z) fix A :: "rat set" assume A: "A \ preal" @@ -543,17 +505,14 @@ qed qed qed - thus "preal_of_rat 1 * Abs_preal A = Abs_preal A" - by (simp add: preal_of_rat_def preal_mult_def mult_set_def + thus "1 * Abs_preal A = Abs_preal A" + by (simp add: preal_one_def preal_mult_def mult_set_def rat_mem_preal A) qed instance preal :: comm_monoid_mult by intro_classes (rule preal_mult_1) -lemma preal_mult_1_right: "z * (1::preal) = z" -by (rule mult_1_right) - subsection{*Distribution of Multiplication across Addition*} @@ -839,9 +798,9 @@ apply (simp add: inverse_set_def) done -lemma Rep_preal_of_rat: - "0 < q ==> Rep_preal (preal_of_rat q) = {x. 0 < x \ x < q}" -by (simp add: preal_of_rat_def rat_mem_preal) +lemma Rep_preal_one: + "Rep_preal 1 = {x. 0 < x \ x < 1}" +by (simp add: preal_one_def rat_mem_preal) lemma subset_inverse_mult_lemma: assumes xpos: "0 < x" and xless: "x < 1" @@ -871,8 +830,8 @@ qed lemma subset_inverse_mult: - "Rep_preal(preal_of_rat 1) \ Rep_preal(inverse R * R)" -apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff + "Rep_preal 1 \ Rep_preal(inverse R * R)" +apply (auto simp add: Bex_def Rep_preal_one mem_Rep_preal_inverse_iff mem_Rep_preal_mult_iff) apply (blast dest: subset_inverse_mult_lemma) done @@ -894,15 +853,14 @@ qed lemma inverse_mult_subset: - "Rep_preal(inverse R * R) \ Rep_preal(preal_of_rat 1)" -apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff + "Rep_preal(inverse R * R) \ Rep_preal 1" +apply (auto simp add: Bex_def Rep_preal_one mem_Rep_preal_inverse_iff mem_Rep_preal_mult_iff) apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal]) apply (blast intro: inverse_mult_subset_lemma) done lemma preal_mult_inverse: "inverse R * R = (1::preal)" -unfolding preal_one_def apply (rule Rep_preal_inject [THEN iffD1]) apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) done @@ -950,12 +908,6 @@ apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym]) done -lemma preal_self_less_add_right: "(R::preal) < S + R" -by (simp add: preal_add_commute preal_self_less_add_left) - -lemma preal_not_eq_self: "x \ x + (y::preal)" -by (insert preal_self_less_add_left [of x y], auto) - subsection{*Subtraction for Positive Reals*} @@ -1117,25 +1069,12 @@ lemma preal_add_left_less_cancel: "T + R < T + S ==> R < (S::preal)" by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T]) -lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)" -by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel) - lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)" by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel) -lemma preal_add_le_cancel_right: "((R::preal) + T \ S + T) = (R \ S)" -by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right) - lemma preal_add_le_cancel_left: "(T + (R::preal) \ T + S) = (R \ S)" by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left) -lemma preal_add_less_mono: - "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)" -apply (auto dest!: less_add_left_Ex simp add: preal_add_ac) -apply (rule preal_add_assoc [THEN subst]) -apply (rule preal_self_less_add_right) -done - lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S" apply (insert linorder_less_linear [of R S], safe) apply (drule_tac [!] T = T in preal_add_less2_mono1, auto) @@ -1144,17 +1083,6 @@ lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)" by (auto intro: preal_add_right_cancel simp add: preal_add_commute) -lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)" -by (fast intro: preal_add_left_cancel) - -lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)" -by (fast intro: preal_add_right_cancel) - -lemmas preal_cancels = - preal_add_less_cancel_right preal_add_less_cancel_left - preal_add_le_cancel_right preal_add_le_cancel_left - preal_add_left_cancel_iff preal_add_right_cancel_iff - instance preal :: linordered_cancel_ab_semigroup_add proof fix a b c :: preal @@ -1232,117 +1160,4 @@ apply (auto simp add: preal_less_def) done - -subsection{*The Embedding from @{typ rat} into @{typ preal}*} - -lemma preal_of_rat_add_lemma1: - "[|x < y + z; 0 < x; 0 < y|] ==> x * y * inverse (y + z) < (y::rat)" -apply (frule_tac c = "y * inverse (y + z) " in mult_strict_right_mono) -apply (simp add: zero_less_mult_iff) -apply (simp add: mult_ac) -done - -lemma preal_of_rat_add_lemma2: - assumes "u < x + y" - and "0 < x" - and "0 < y" - and "0 < u" - shows "\v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w" -proof (intro exI conjI) - show "u * x * inverse(x+y) < x" using prems - by (simp add: preal_of_rat_add_lemma1) - show "u * y * inverse(x+y) < y" using prems - by (simp add: preal_of_rat_add_lemma1 add_commute [of x]) - show "0 < u * x * inverse (x + y)" using prems - by (simp add: zero_less_mult_iff) - show "0 < u * y * inverse (x + y)" using prems - by (simp add: zero_less_mult_iff) - show "u = u * x * inverse (x + y) + u * y * inverse (x + y)" using prems - by (simp add: left_distrib [symmetric] right_distrib [symmetric] mult_ac) -qed - -lemma preal_of_rat_add: - "[| 0 < x; 0 < y|] - ==> preal_of_rat ((x::rat) + y) = preal_of_rat x + preal_of_rat y" -apply (unfold preal_of_rat_def preal_add_def) -apply (simp add: rat_mem_preal) -apply (rule_tac f = Abs_preal in arg_cong) -apply (auto simp add: add_set_def) -apply (blast dest: preal_of_rat_add_lemma2) -done - -lemma preal_of_rat_mult_lemma1: - "[|x < y; 0 < x; 0 < z|] ==> x * z * inverse y < (z::rat)" -apply (frule_tac c = "z * inverse y" in mult_strict_right_mono) -apply (simp add: zero_less_mult_iff) -apply (subgoal_tac "y * (z * inverse y) = z * (y * inverse y)") -apply (simp_all add: mult_ac) -done - -lemma preal_of_rat_mult_lemma2: - assumes xless: "x < y * z" - and xpos: "0 < x" - and ypos: "0 < y" - shows "x * z * inverse y * inverse z < (z::rat)" -proof - - have "0 < y * z" using prems by simp - hence zpos: "0 < z" using prems by (simp add: zero_less_mult_iff) - have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)" - by (simp add: mult_ac) - also have "... = x/y" using zpos - by (simp add: divide_inverse) - also from xless have "... < z" - by (simp add: pos_divide_less_eq [OF ypos] mult_commute) - finally show ?thesis . -qed - -lemma preal_of_rat_mult_lemma3: - assumes uless: "u < x * y" - and "0 < x" - and "0 < y" - and "0 < u" - shows "\v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w" -proof - - from dense [OF uless] - obtain r where "u < r" "r < x * y" by blast - thus ?thesis - proof (intro exI conjI) - show "u * x * inverse r < x" using prems - by (simp add: preal_of_rat_mult_lemma1) - show "r * y * inverse x * inverse y < y" using prems - by (simp add: preal_of_rat_mult_lemma2) - show "0 < u * x * inverse r" using prems - by (simp add: zero_less_mult_iff) - show "0 < r * y * inverse x * inverse y" using prems - by (simp add: zero_less_mult_iff) - have "u * x * inverse r * (r * y * inverse x * inverse y) = - u * (r * inverse r) * (x * inverse x) * (y * inverse y)" - by (simp only: mult_ac) - thus "u = u * x * inverse r * (r * y * inverse x * inverse y)" using prems - by simp - qed -qed - -lemma preal_of_rat_mult: - "[| 0 < x; 0 < y|] - ==> preal_of_rat ((x::rat) * y) = preal_of_rat x * preal_of_rat y" -apply (unfold preal_of_rat_def preal_mult_def) -apply (simp add: rat_mem_preal) -apply (rule_tac f = Abs_preal in arg_cong) -apply (auto simp add: zero_less_mult_iff mult_strict_mono mult_set_def) -apply (blast dest: preal_of_rat_mult_lemma3) -done - -lemma preal_of_rat_less_iff: - "[| 0 < x; 0 < y|] ==> (preal_of_rat x < preal_of_rat y) = (x < y)" -by (force simp add: preal_of_rat_def preal_less_def rat_mem_preal) - -lemma preal_of_rat_le_iff: - "[| 0 < x; 0 < y|] ==> (preal_of_rat x \ preal_of_rat y) = (x \ y)" -by (simp add: preal_of_rat_less_iff linorder_not_less [symmetric]) - -lemma preal_of_rat_eq_iff: - "[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)" -by (simp add: preal_of_rat_le_iff order_eq_iff) - end diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Parity.thy Fri May 07 14:47:09 2010 +0200 @@ -229,7 +229,7 @@ lemma zero_le_odd_power: "odd n ==> (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)" apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff) -apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square) +apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square) done lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Probability/Lebesgue.thy --- a/src/HOL/Probability/Lebesgue.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Probability/Lebesgue.thy Fri May 07 14:47:09 2010 +0200 @@ -938,17 +938,17 @@ proof safe fix t assume t: "t \ space M" { fix m n :: nat assume "m \ n" - hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto + hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \ real (natfloor (f t * 2 ^ n))" apply (subst *) - apply (subst class_semiring.mul_a) + apply (subst normalizing.mul_a) apply (subst real_of_nat_le_iff) apply (rule le_mult_natfloor) using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg) hence "real (natfloor (f t * 2^m)) * 2^n \ real (natfloor (f t * 2^n)) * 2^m" apply (subst *) - apply (subst (3) class_semiring.mul_c) - apply (subst class_semiring.mul_a) + apply (subst (3) normalizing.mul_c) + apply (subst normalizing.mul_a) by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) } thus "incseq (\n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def by (auto simp add: le_divide_eq divide_le_eq less_divide_eq) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Rings.thy Fri May 07 14:47:09 2010 +0200 @@ -183,9 +183,21 @@ end - class no_zero_divisors = zero + times + assumes no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0" +begin + +lemma divisors_zero: + assumes "a * b = 0" + shows "a = 0 \ b = 0" +proof (rule classical) + assume "\ (a = 0 \ b = 0)" + then have "a \ 0" and "b \ 0" by auto + with no_zero_divisors have "a * b \ 0" by blast + with assms show ?thesis by simp +qed + +end class semiring_1_cancel = semiring + cancel_comm_monoid_add + zero_neq_one + monoid_mult diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Statespace/state_space.ML Fri May 07 14:47:09 2010 +0200 @@ -528,7 +528,7 @@ | dups => ["Duplicate renaming(s) for " ^ commas dups]) val cnames = map fst components; - val err_rename_unknowns = (case (filter (fn n => not (n mem cnames))) rnames of + val err_rename_unknowns = (case subtract (op =) cnames rnames of [] => [] | rs => ["Unknown components " ^ commas rs]); diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri May 07 14:47:09 2010 +0200 @@ -309,7 +309,7 @@ val T' = typ_of_dtyp descr' sorts dt; val (Us, U) = strip_type T' in (case strip_dtyp dt of - (_, DtRec j) => if j mem ks' then + (_, DtRec j) => if member (op =) ks' j then (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us], Ts @ [Us ---> Univ_elT]) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri May 07 14:47:09 2010 +0200 @@ -136,7 +136,7 @@ val getP = if can HOLogic.dest_imp (hd ts) then (apfst SOME) o HOLogic.dest_imp else pair NONE; val flt = if null indnames then I else - filter (fn Free (s, _) => s mem indnames | _ => false); + filter (fn Free (s, _) => member (op =) indnames s | _ => false); fun abstr (t1, t2) = (case t1 of NONE => (case flt (OldTerm.term_frees t2) of [Free (s, T)] => SOME (absfree (s, T, t2)) @@ -300,7 +300,7 @@ fun is_nonempty_dt is i = let val (_, _, constrs) = (the o AList.lookup (op =) descr') i; - fun arg_nonempty (_, DtRec i) = if i mem is then false + fun arg_nonempty (_, DtRec i) = if member (op =) is i then false else is_nonempty_dt (i::is) i | arg_nonempty _ = true; in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Fri May 07 14:47:09 2010 +0200 @@ -306,11 +306,11 @@ map_node node_id (K (NONE, module', string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @ [str ";"])) ^ "\n\n" ^ - (if "term_of" mem !mode then + (if member (op =) (!mode) "term_of" then string_of (Pretty.blk (0, separate Pretty.fbrk (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n" else "") ^ - (if "test" mem !mode then + (if member (op =) (!mode) "test" then string_of (Pretty.blk (0, separate Pretty.fbrk (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n" else ""))) gr2 diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri May 07 14:47:09 2010 +0200 @@ -41,16 +41,16 @@ else map (fn i => "P" ^ string_of_int i) (1 upto length descr); val rec_result_Ts = map (fn ((i, _), P) => - if i mem is then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT) + if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT) (descr ~~ pnames); fun make_pred i T U r x = - if i mem is then + if member (op =) is i then Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x; fun mk_all i s T t = - if i mem is then list_all_free ([(s, T)], t) else t; + if member (op =) is i then list_all_free ([(s, T)], t) else t; val (prems, rec_fns) = split_list (flat (fst (fold_map (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j => @@ -66,7 +66,7 @@ val vs' = filter_out is_unit vs; val f = mk_Free "f" (map fastype_of vs' ---> rT) j; val f' = Envir.eta_contract (list_abs_free - (map dest_Free vs, if i mem is then list_comb (f, vs') + (map dest_Free vs, if member (op =) is i then list_comb (f, vs') else HOLogic.unit)); in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs')) (list_comb (Const (cname, Ts ---> T), map Free frees))), f') @@ -100,7 +100,7 @@ (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names); val r = if null is then Extraction.nullt else foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) => - if i mem is then SOME + if member (op =) is i then SOME (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T)) else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames)); val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"}) @@ -131,7 +131,7 @@ val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []); val rvs = rev (Thm.fold_terms Term.add_vars thm' []); val ivs1 = map Var (filter_out (fn (_, T) => (* FIXME set (!??) *) - tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs); + member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs); val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs; val prf = diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Function/function_common.ML Fri May 07 14:47:09 2010 +0200 @@ -244,7 +244,7 @@ val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq - val _ = fname mem fnames + val _ = member (op =) fnames fname orelse input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames ^ commas_quote fnames) @@ -259,7 +259,7 @@ " occur" ^ plural "s" "" rvs ^ " on right hand side only:") val _ = forall (not o Term.exists_subterm - (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args) + (fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) orelse input_error "Defined function may not occur in premises or arguments" val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Fri May 07 14:47:09 2010 +0200 @@ -9,19 +9,20 @@ vars: cterm list, semiring: cterm list * thm list, ideal : thm list} -> (cterm -> Rat.rat) -> (Rat.rat -> cterm) -> conv -> conv -> - {ring_conv : conv, - simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list), - multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list, - poly_eq_ss: simpset, unwind_conv : conv} - val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic - val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic - val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic + {ring_conv : conv, + simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list), + multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list, + poly_eq_ss: simpset, unwind_conv : conv} + val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic + val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic + val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic + val algebra_method: (Proof.context -> Method.method) context_parser end structure Groebner : GROEBNER = struct -open Conv Normalizer Drule Thm; +open Conv Drule Thm; fun is_comb ct = (case Thm.term_of ct of @@ -50,11 +51,11 @@ val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y)); val (eqF_intr, eqF_elim) = - let val [th1,th2] = thms "PFalse" + let val [th1,th2] = @{thms PFalse} in (fn th => th COMP th2, fn th => th COMP th1) end; val (PFalse, PFalse') = - let val PFalse_eq = nth (thms "simp_thms") 13 + let val PFalse_eq = nth @{thms simp_thms} 13 in (PFalse_eq RS iffD1, PFalse_eq RS iffD2) end; @@ -398,7 +399,7 @@ compose_single(refute_disj rfn (dest_arg tm),2,compose_single(refute_disj rfn (dest_arg1 tm),2,disjE)) | _ => rfn tm ; -val notnotD = @{thm "notnotD"}; +val notnotD = @{thm notnotD}; fun mk_binop ct x y = capply (capply ct x) y val mk_comb = capply; @@ -440,10 +441,10 @@ | _ => false; val mk_object_eq = fn th => th COMP meta_eq_to_obj_eq; -val bool_simps = @{thms "bool_simps"}; -val nnf_simps = @{thms "nnf_simps"}; +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 @@ -947,29 +948,31 @@ case try (find_term 0) form of NONE => NONE | SOME tm => - (case NormalizerData.match ctxt tm of + (case Normalizer.match ctxt tm of NONE => NONE | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => SOME (ring_and_ideal_conv theory dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) - (semiring_normalize_wrapper ctxt res))) + (Normalizer.semiring_normalize_wrapper ctxt res))) fun ring_solve ctxt form = (case try (find_term 0 (* FIXME !? *)) form of NONE => reflexive form | SOME tm => - (case NormalizerData.match ctxt tm of + (case Normalizer.match ctxt tm of NONE => reflexive form | SOME (res as (theory, {is_const, dest_const, mk_const, conv = ring_eq_conv})) => #ring_conv (ring_and_ideal_conv theory dest_const (mk_const (ctyp_of_term tm)) (ring_eq_conv ctxt) - (semiring_normalize_wrapper ctxt res)) form)); + (Normalizer.semiring_normalize_wrapper ctxt res)) form)); + +fun presimplify ctxt add_thms del_thms = asm_full_simp_tac (Simplifier.context ctxt + (HOL_basic_ss addsimps (Algebra_Simplification.get ctxt) delsimps del_thms addsimps add_thms)); fun ring_tac add_ths del_ths ctxt = Object_Logic.full_atomize_tac - THEN' asm_full_simp_tac - (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths) + THEN' presimplify ctxt add_ths del_ths THEN' CSUBGOAL (fn (p, i) => rtac (let val form = Object_Logic.dest_judgment p in case get_ring_ideal_convs ctxt form of @@ -988,8 +991,7 @@ | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1 in fun ideal_tac add_ths del_ths ctxt = - asm_full_simp_tac - (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths) + presimplify ctxt add_ths del_ths THEN' CSUBGOAL (fn (p, i) => case get_ring_ideal_convs ctxt p of @@ -1023,6 +1025,21 @@ fun algebra_tac add_ths del_ths ctxt i = ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i - +local + +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () +val addN = "add" +val delN = "del" +val any_keyword = keyword addN || keyword delN +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; + +in + +val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- + (Scan.optional (keyword delN |-- thms) [])) >> + (fn (add_ths, del_ths) => fn ctxt => + SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt)) end; + +end; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Groebner_Basis/misc.ML --- a/src/HOL/Tools/Groebner_Basis/misc.ML Thu May 06 23:57:55 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -(* Title: HOL/Tools/Groebner_Basis/misc.ML - ID: $Id$ - Author: Amine Chaieb, TU Muenchen - -Very basic stuff for cterms. -*) - -structure Misc = -struct - -fun is_comb ct = - (case Thm.term_of ct of - _ $ _ => true - | _ => false); - -val concl = Thm.cprop_of #> Thm.dest_arg; - -fun is_binop ct ct' = - (case Thm.term_of ct' of - c $ _ $ _ => term_of ct aconv c - | _ => false); - -fun dest_binop ct ct' = - if is_binop ct ct' then Thm.dest_binop ct' - else raise CTERM ("dest_binop: bad binop", [ct, ct']) - -fun inst_thm inst = Thm.instantiate ([], inst); - -end; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Fri May 07 14:47:09 2010 +0200 @@ -1,30 +1,376 @@ (* Title: HOL/Tools/Groebner_Basis/normalizer.ML Author: Amine Chaieb, TU Muenchen + +Normalization of expressions in semirings. *) signature NORMALIZER = sig - val semiring_normalize_conv : Proof.context -> conv - val semiring_normalize_ord_conv : Proof.context -> (cterm -> cterm -> bool) -> conv - val semiring_normalize_tac : Proof.context -> int -> tactic - val semiring_normalize_wrapper : Proof.context -> NormalizerData.entry -> conv - val semiring_normalizers_ord_wrapper : - Proof.context -> NormalizerData.entry -> (cterm -> cterm -> bool) -> + type entry + val get: Proof.context -> (thm * entry) list + val match: Proof.context -> cterm -> entry option + val del: attribute + val add: {semiring: cterm list * thm list, ring: cterm list * thm list, + field: cterm list * thm list, idom: thm list, ideal: thm list} -> attribute + val funs: thm -> {is_const: morphism -> cterm -> bool, + dest_const: morphism -> cterm -> Rat.rat, + mk_const: morphism -> ctyp -> Rat.rat -> cterm, + conv: morphism -> Proof.context -> cterm -> thm} -> declaration + val semiring_funs: thm -> declaration + val field_funs: thm -> declaration + + val semiring_normalize_conv: Proof.context -> conv + val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv + val semiring_normalize_wrapper: Proof.context -> entry -> conv + val semiring_normalize_ord_wrapper: Proof.context -> entry + -> (cterm -> cterm -> bool) -> conv + val semiring_normalizers_conv: cterm list -> cterm list * thm list + -> cterm list * thm list -> cterm list * thm list -> + (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) -> + {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} + val semiring_normalizers_ord_wrapper: Proof.context -> entry -> + (cterm -> cterm -> bool) -> {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} - val semiring_normalize_ord_wrapper : Proof.context -> NormalizerData.entry -> - (cterm -> cterm -> bool) -> conv - val semiring_normalizers_conv : - cterm list -> cterm list * thm list -> cterm list * thm list -> cterm list * thm list -> - (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) -> - {add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} + val field_comp_conv: conv + + val setup: theory -> theory end structure Normalizer: NORMALIZER = struct -open Conv; +(** some conversion **) + +local + val zr = @{cpat "0"} + val zT = ctyp_of_term zr + val geq = @{cpat "op ="} + val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd + val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} + val add_frac_num = mk_meta_eq @{thm "add_frac_num"} + val add_num_frac = mk_meta_eq @{thm "add_num_frac"} + + fun prove_nz ss T t = + let + val z = instantiate_cterm ([(zT,T)],[]) zr + val eq = instantiate_cterm ([(eqT,T)],[]) geq + val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) + (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} + (Thm.capply (Thm.capply eq t) z))) + in equal_elim (symmetric th) TrueI + end + + fun proc phi ss ct = + let + val ((x,y),(w,z)) = + (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct + val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] + val T = ctyp_of_term x + val [y_nz, z_nz] = map (prove_nz ss T) [y, z] + val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq + in SOME (implies_elim (implies_elim th y_nz) z_nz) + end + handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE + + fun proc2 phi ss ct = + let + val (l,r) = Thm.dest_binop ct + val T = ctyp_of_term l + in (case (term_of l, term_of r) of + (Const(@{const_name Rings.divide},_)$_$_, _) => + let val (x,y) = Thm.dest_binop l val z = r + val _ = map (HOLogic.dest_number o term_of) [x,y,z] + val ynz = prove_nz ss T y + in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) + end + | (_, Const (@{const_name Rings.divide},_)$_$_) => + let val (x,y) = Thm.dest_binop r val z = l + val _ = map (HOLogic.dest_number o term_of) [x,y,z] + val ynz = prove_nz ss T y + in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) + end + | _ => NONE) + end + handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE + + fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b + | is_number t = can HOLogic.dest_number t + + val is_number = is_number o term_of + + fun proc3 phi ss ct = + (case term_of ct of + Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} + in SOME (mk_meta_eq th) end + | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => + let + val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} + in SOME (mk_meta_eq th) end + | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} + in SOME (mk_meta_eq th) end + | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) => + let + val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop + val _ = map is_number [a,b,c] + val T = ctyp_of_term c + val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} + in SOME (mk_meta_eq th) end + | _ => NONE) + handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE + +val add_frac_frac_simproc = + make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], + name = "add_frac_frac_simproc", + proc = proc, identifier = []} + +val add_frac_num_simproc = + make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], + name = "add_frac_num_simproc", + proc = proc2, identifier = []} + +val ord_frac_simproc = + make_simproc + {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, + @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"}, + @{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, + @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"}, + @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, + @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], + name = "ord_frac_simproc", proc = proc3, identifier = []} + +val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, + @{thm "divide_Numeral1"}, + @{thm "divide_zero"}, @{thm "divide_Numeral0"}, + @{thm "divide_divide_eq_left"}, + @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, + @{thm "times_divide_times_eq"}, + @{thm "divide_divide_eq_right"}, + @{thm "diff_def"}, @{thm "minus_divide_left"}, + @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, + @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, + Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute})))) + (@{thm field_divide_inverse} RS sym)] + +in + +val field_comp_conv = (Simplifier.rewrite +(HOL_basic_ss addsimps @{thms "semiring_norm"} + addsimps ths addsimps @{thms simp_thms} + addsimprocs Numeral_Simprocs.field_cancel_numeral_factors + addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, + ord_frac_simproc] + addcongs [@{thm "if_weak_cong"}])) +then_conv (Simplifier.rewrite (HOL_basic_ss addsimps + [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})) + +end + + +(** data **) -(* Very basic stuff for terms *) +type entry = + {vars: cterm list, + semiring: cterm list * thm list, + ring: cterm list * thm list, + field: cterm list * thm list, + idom: thm list, + ideal: thm list} * + {is_const: cterm -> bool, + dest_const: cterm -> Rat.rat, + mk_const: ctyp -> Rat.rat -> cterm, + conv: Proof.context -> cterm -> thm}; + +structure Data = Generic_Data +( + type T = (thm * entry) list; + val empty = []; + val extend = I; + val merge = AList.merge Thm.eq_thm (K true); +); + +val get = Data.get o Context.Proof; + +fun match ctxt tm = + let + fun match_inst + ({vars, semiring = (sr_ops, sr_rules), + ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal}, + fns as {is_const, dest_const, mk_const, conv}) pat = + let + fun h instT = + let + val substT = Thm.instantiate (instT, []); + val substT_cterm = Drule.cterm_rule substT; + + val vars' = map substT_cterm vars; + val semiring' = (map substT_cterm sr_ops, map substT sr_rules); + val ring' = (map substT_cterm r_ops, map substT r_rules); + val field' = (map substT_cterm f_ops, map substT f_rules); + val idom' = map substT idom; + val ideal' = map substT ideal; + + val result = ({vars = vars', semiring = semiring', + ring = ring', field = field', idom = idom', ideal = ideal'}, fns); + in SOME result end + in (case try Thm.match (pat, tm) of + NONE => NONE + | SOME (instT, _) => h instT) + end; + + fun match_struct (_, + entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) = + get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); + in get_first match_struct (get ctxt) end; + + +(* logical content *) + +val semiringN = "semiring"; +val ringN = "ring"; +val idomN = "idom"; +val idealN = "ideal"; +val fieldN = "field"; + +fun undefined _ = raise Match; + +val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm); + +fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), + field = (f_ops, f_rules), idom, ideal} = + Thm.declaration_attribute (fn key => fn context => context |> Data.map + let + val ctxt = Context.proof_of context; + + fun check kind name xs n = + null xs orelse length xs = n orelse + error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); + val check_ops = check "operations"; + val check_rules = check "rules"; + + val _ = + check_ops semiringN sr_ops 5 andalso + check_rules semiringN sr_rules 37 andalso + check_ops ringN r_ops 2 andalso + check_rules ringN r_rules 2 andalso + check_ops fieldN f_ops 2 andalso + check_rules fieldN f_rules 2 andalso + check_rules idomN idom 2; + + val mk_meta = Local_Defs.meta_rewrite_rule ctxt; + val sr_rules' = map mk_meta sr_rules; + val r_rules' = map mk_meta r_rules; + val f_rules' = map mk_meta f_rules; + + fun rule i = nth sr_rules' (i - 1); + + val (cx, cy) = Thm.dest_binop (hd sr_ops); + val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; + val ((clx, crx), (cly, cry)) = + rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; + val ((ca, cb), (cc, cd)) = + rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; + val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; + val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg; + + val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; + val semiring = (sr_ops, sr_rules'); + val ring = (r_ops, r_rules'); + val field = (f_ops, f_rules'); + val ideal' = map (symmetric o mk_meta) ideal + in + AList.delete Thm.eq_thm key #> + cons (key, ({vars = vars, semiring = semiring, + ring = ring, field = field, idom = idom, ideal = ideal'}, + {is_const = undefined, dest_const = undefined, mk_const = undefined, + conv = undefined})) + end); + + +(* extra-logical functions *) + +fun funs raw_key {is_const, dest_const, mk_const, conv} phi = + Data.map (fn data => + let + val key = Morphism.thm phi raw_key; + val _ = AList.defined Thm.eq_thm data key orelse + raise THM ("No data entry for structure key", 0, [key]); + val fns = {is_const = is_const phi, dest_const = dest_const phi, + mk_const = mk_const phi, conv = conv phi}; + in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); + +fun semiring_funs key = funs key + {is_const = fn phi => can HOLogic.dest_number o Thm.term_of, + dest_const = fn phi => fn ct => + Rat.rat_of_int (snd + (HOLogic.dest_number (Thm.term_of ct) + handle TERM _ => error "ring_dest_const")), + mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT + (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int"), + conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) + then_conv Simplifier.rewrite (HOL_basic_ss addsimps + (@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(1-2)}))}; + +fun field_funs key = + let + fun numeral_is_const ct = + case term_of ct of + Const (@{const_name Rings.divide},_) $ a $ b => + can HOLogic.dest_number a andalso can HOLogic.dest_number b + | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t + | t => can HOLogic.dest_number t + fun dest_const ct = ((case term_of ct of + Const (@{const_name Rings.divide},_) $ a $ b=> + Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) + | Const (@{const_name Rings.inverse},_)$t => + Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) + | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) + handle TERM _ => error "ring_dest_const") + fun mk_const phi cT x = + let val (a, b) = Rat.quotient_of_rat x + in if b = 1 then Numeral.mk_cnumber cT a + else Thm.capply + (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) + (Numeral.mk_cnumber cT a)) + (Numeral.mk_cnumber cT b) + end + in funs key + {is_const = K numeral_is_const, + dest_const = K dest_const, + mk_const = mk_const, + conv = K (K field_comp_conv)} + end; + + + +(** auxiliary **) fun is_comb ct = (case Thm.term_of ct of @@ -55,6 +401,7 @@ val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, @{thm "less_nat_number_of"}]; + val nat_add_conv = zerone_conv (Simplifier.rewrite @@ -64,13 +411,15 @@ @{thm add_number_of_left}, @{thm Suc_eq_plus1}] @ map (fn th => th RS sym) @{thms numerals})); -val nat_mul_conv = nat_add_conv; val zeron_tm = @{cterm "0::nat"}; val onen_tm = @{cterm "1::nat"}; val true_tm = @{cterm "True"}; -(* The main function! *) +(** normalizing conversions **) + +(* core conversion *) + fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules) (is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) = let @@ -182,7 +531,7 @@ then let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34 val (l,r) = Thm.dest_comb(concl th1) - in transitive th1 (Drule.arg_cong_rule l (nat_mul_conv r)) + in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r)) end else if opr aconvc mul_tm @@ -563,7 +912,7 @@ let val (l,r) = Thm.dest_comb tm in if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else let val th1 = inst_thm [(cx',r)] neg_mul - val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1)) + val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) in transitive th2 (polynomial_monomial_mul_conv (concl th2)) end end; @@ -606,7 +955,7 @@ then let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r) - val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv) + val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv) (Thm.rhs_of th1) in transitive th1 th2 end @@ -638,11 +987,14 @@ fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; + +(* various normalizing conversions *) + fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = let val pow_conv = - arg_conv (Simplifier.rewrite nat_exp_ss) + Conv.arg_conv (Simplifier.rewrite nat_exp_ss) then_conv Simplifier.rewrite (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) then_conv conv ctxt @@ -656,14 +1008,57 @@ semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; fun semiring_normalize_ord_conv ctxt ord tm = - (case NormalizerData.match ctxt tm of + (case match ctxt tm of NONE => reflexive tm | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); - fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; -fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) => - rtac (semiring_normalize_conv ctxt - (cterm_of (ProofContext.theory_of ctxt) (fst (Logic.dest_equals goal)))) i); + +(** Isar setup **) + +local + +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); +fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K (); +fun keyword3 k1 k2 k3 = + Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K (); + +val opsN = "ops"; +val rulesN = "rules"; + +val normN = "norm"; +val constN = "const"; +val delN = "del"; + +val any_keyword = + keyword2 semiringN opsN || keyword2 semiringN rulesN || + keyword2 ringN opsN || keyword2 ringN rulesN || + keyword2 fieldN opsN || keyword2 fieldN rulesN || + keyword2 idomN rulesN || keyword2 idealN rulesN; + +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; +val terms = thms >> map Drule.dest_term; + +fun optional scan = Scan.optional scan []; + +in + +val setup = + Attrib.setup @{binding normalizer} + (Scan.lift (Args.$$$ delN >> K del) || + ((keyword2 semiringN opsN |-- terms) -- + (keyword2 semiringN rulesN |-- thms)) -- + (optional (keyword2 ringN opsN |-- terms) -- + optional (keyword2 ringN rulesN |-- thms)) -- + (optional (keyword2 fieldN opsN |-- terms) -- + optional (keyword2 fieldN rulesN |-- thms)) -- + optional (keyword2 idomN rulesN |-- thms) -- + optional (keyword2 idealN rulesN |-- thms) + >> (fn ((((sr, r), f), id), idl) => + add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) + "semiring normalizer data"; + end; + +end; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Thu May 06 23:57:55 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,227 +0,0 @@ -(* Title: HOL/Tools/Groebner_Basis/normalizer_data.ML - ID: $Id$ - Author: Amine Chaieb, TU Muenchen - -Ring normalization data. -*) - -signature NORMALIZER_DATA = -sig - type entry - val get: Proof.context -> simpset * (thm * entry) list - val match: Proof.context -> cterm -> entry option - val del: attribute - val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list} - -> attribute - val funs: thm -> {is_const: morphism -> cterm -> bool, - dest_const: morphism -> cterm -> Rat.rat, - mk_const: morphism -> ctyp -> Rat.rat -> cterm, - conv: morphism -> Proof.context -> cterm -> thm} -> declaration - val setup: theory -> theory -end; - -structure NormalizerData: NORMALIZER_DATA = -struct - -(* data *) - -type entry = - {vars: cterm list, - semiring: cterm list * thm list, - ring: cterm list * thm list, - field: cterm list * thm list, - idom: thm list, - ideal: thm list} * - {is_const: cterm -> bool, - dest_const: cterm -> Rat.rat, - mk_const: ctyp -> Rat.rat -> cterm, - conv: Proof.context -> cterm -> thm}; - -val eq_key = Thm.eq_thm; -fun eq_data arg = eq_fst eq_key arg; - -structure Data = Generic_Data -( - type T = simpset * (thm * entry) list; - val empty = (HOL_basic_ss, []); - val extend = I; - fun merge ((ss, e), (ss', e')) : T = - (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e')); -); - -val get = Data.get o Context.Proof; - - -(* match data *) - -fun match ctxt tm = - let - fun match_inst - ({vars, semiring = (sr_ops, sr_rules), - ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal}, - fns as {is_const, dest_const, mk_const, conv}) pat = - let - fun h instT = - let - val substT = Thm.instantiate (instT, []); - val substT_cterm = Drule.cterm_rule substT; - - val vars' = map substT_cterm vars; - val semiring' = (map substT_cterm sr_ops, map substT sr_rules); - val ring' = (map substT_cterm r_ops, map substT r_rules); - val field' = (map substT_cterm f_ops, map substT f_rules); - val idom' = map substT idom; - val ideal' = map substT ideal; - - val result = ({vars = vars', semiring = semiring', - ring = ring', field = field', idom = idom', ideal = ideal'}, fns); - in SOME result end - in (case try Thm.match (pat, tm) of - NONE => NONE - | SOME (instT, _) => h instT) - end; - - fun match_struct (_, - entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) = - get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); - in get_first match_struct (snd (get ctxt)) end; - - -(* logical content *) - -val semiringN = "semiring"; -val ringN = "ring"; -val idomN = "idom"; -val idealN = "ideal"; -val fieldN = "field"; - -fun undefined _ = raise Match; - -fun del_data key = apsnd (remove eq_data (key, [])); - -val del = Thm.declaration_attribute (Data.map o del_data); -val add_ss = Thm.declaration_attribute - (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data))); - -val del_ss = Thm.declaration_attribute - (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data))); - -fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), - field = (f_ops, f_rules), idom, ideal} = - Thm.declaration_attribute (fn key => fn context => context |> Data.map - let - val ctxt = Context.proof_of context; - - fun check kind name xs n = - null xs orelse length xs = n orelse - error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); - val check_ops = check "operations"; - val check_rules = check "rules"; - - val _ = - check_ops semiringN sr_ops 5 andalso - check_rules semiringN sr_rules 37 andalso - check_ops ringN r_ops 2 andalso - check_rules ringN r_rules 2 andalso - check_ops fieldN f_ops 2 andalso - check_rules fieldN f_rules 2 andalso - check_rules idomN idom 2; - - val mk_meta = Local_Defs.meta_rewrite_rule ctxt; - val sr_rules' = map mk_meta sr_rules; - val r_rules' = map mk_meta r_rules; - val f_rules' = map mk_meta f_rules; - - fun rule i = nth sr_rules' (i - 1); - - val (cx, cy) = Thm.dest_binop (hd sr_ops); - val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; - val ((clx, crx), (cly, cry)) = - rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; - val ((ca, cb), (cc, cd)) = - rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; - val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; - val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg; - - val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; - val semiring = (sr_ops, sr_rules'); - val ring = (r_ops, r_rules'); - val field = (f_ops, f_rules'); - val ideal' = map (symmetric o mk_meta) ideal - in - del_data key #> - apsnd (cons (key, ({vars = vars, semiring = semiring, - ring = ring, field = field, idom = idom, ideal = ideal'}, - {is_const = undefined, dest_const = undefined, mk_const = undefined, - conv = undefined}))) - end); - - -(* extra-logical functions *) - -fun funs raw_key {is_const, dest_const, mk_const, conv} phi = - (Data.map o apsnd) (fn data => - let - val key = Morphism.thm phi raw_key; - val _ = AList.defined eq_key data key orelse - raise THM ("No data entry for structure key", 0, [key]); - val fns = {is_const = is_const phi, dest_const = dest_const phi, - mk_const = mk_const phi, conv = conv phi}; - in AList.map_entry eq_key key (apsnd (K fns)) data end); - - -(* concrete syntax *) - -local - -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); -fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.colon) >> K (); -fun keyword3 k1 k2 k3 = - Scan.lift (Args.$$$ k1 -- Args.$$$ k2 -- Args.$$$ k3 -- Args.colon) >> K (); - -val opsN = "ops"; -val rulesN = "rules"; - -val normN = "norm"; -val constN = "const"; -val delN = "del"; - -val any_keyword = - keyword2 semiringN opsN || keyword2 semiringN rulesN || - keyword2 ringN opsN || keyword2 ringN rulesN || - keyword2 fieldN opsN || keyword2 fieldN rulesN || - keyword2 idomN rulesN || keyword2 idealN rulesN; - -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; -val terms = thms >> map Drule.dest_term; - -fun optional scan = Scan.optional scan []; - -in - -val normalizer_setup = - Attrib.setup @{binding normalizer} - (Scan.lift (Args.$$$ delN >> K del) || - ((keyword2 semiringN opsN |-- terms) -- - (keyword2 semiringN rulesN |-- thms)) -- - (optional (keyword2 ringN opsN |-- terms) -- - optional (keyword2 ringN rulesN |-- thms)) -- - (optional (keyword2 fieldN opsN |-- terms) -- - optional (keyword2 fieldN rulesN |-- thms)) -- - optional (keyword2 idomN rulesN |-- thms) -- - optional (keyword2 idealN rulesN |-- thms) - >> (fn ((((sr, r), f), id), idl) => - add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) - "semiring normalizer data"; - -end; - - -(* theory setup *) - -val setup = - normalizer_setup #> - Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra"; - -end; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri May 07 14:47:09 2010 +0200 @@ -2178,7 +2178,7 @@ val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) val (c, _) = strip_comb t in (case c of - Const (name, _) => name mem_string constr_consts + Const (name, _) => member (op =) constr_consts name | _ => false) end)) else false diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Fri May 07 14:47:09 2010 +0200 @@ -3,7 +3,7 @@ *) signature COOPER = - sig +sig val cooper_conv : Proof.context -> conv exception COOPER of string * exn end; @@ -12,7 +12,6 @@ struct open Conv; -open Normalizer; exception COOPER of string * exn; fun simp_thms_conv ctxt = @@ -538,6 +537,8 @@ open Generated_Cooper; +fun member eq = Library.member eq; + fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s); fun i_of_term vs t = case t of Free (xn, xT) => (case AList.lookup (op aconv) vs t @@ -593,12 +594,12 @@ in fun term_bools acc t = case t of - (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b + (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b else insert (op aconv) t acc - | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a + | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a else insert (op aconv) t acc | Abs p => term_bools acc (snd (variant_abs p)) - | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc + | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc end; fun myassoc2 l v = diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Qelim/cooper_data.ML --- a/src/HOL/Tools/Qelim/cooper_data.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper_data.ML Fri May 07 14:47:09 2010 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/Qelim/cooper_data.ML - ID: $Id$ Author: Amine Chaieb, TU Muenchen *) @@ -16,8 +15,7 @@ struct type entry = simpset * (term list); -val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"} - addcongs [if_weak_cong, @{thm "let_weak_cong"}];*) + val allowed_consts = [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, @{term "op - :: int => _"}, @{term "op - :: nat => _"}, @@ -47,7 +45,7 @@ structure Data = Generic_Data ( type T = simpset * term list; - val empty = (start_ss, allowed_consts); + val empty = (HOL_ss, allowed_consts); val extend = I; fun merge ((ss1, ts1), (ss2, ts2)) = (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2)); @@ -64,7 +62,7 @@ (ss delsimps [th], subtract (op aconv) ts' ts ))) -(* concrete syntax *) +(* theory setup *) local @@ -79,16 +77,11 @@ in -val presburger_setup = +val setup = Attrib.setup @{binding presburger} ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del || optional (keyword constsN |-- terms) >> add) "Cooper data"; end; - -(* theory setup *) - -val setup = presburger_setup; - end; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Qelim/presburger.ML Fri May 07 14:47:09 2010 +0200 @@ -11,7 +11,7 @@ struct open Conv; -val comp_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"}; +val comp_ss = HOL_ss addsimps @{thms semiring_norm}; fun strip_objimp ct = (case Thm.term_of ct of @@ -67,9 +67,9 @@ | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t fun ty cts t = - if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false + if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false else case term_of t of - c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] + c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c then not (isnum l orelse isnum r) else not (member (op aconv) cts c) | c$_ => not (member (op aconv) cts c) @@ -85,8 +85,8 @@ in fun is_relevant ctxt ct = subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt)) - andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct)) - andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct)); + andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct)) + andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct)); fun int_nat_terms ctxt ct = let diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri May 07 14:47:09 2010 +0200 @@ -728,7 +728,7 @@ val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos val ty_substs = if qtys = [] then all_ty_substs else - filter (fn (_, qty) => qty mem qtys) all_ty_substs + filter (fn (_, qty) => member (op =) qtys qty) all_ty_substs val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri May 07 14:47:09 2010 +0200 @@ -387,7 +387,7 @@ (*Ignore blacklisted basenames*) fun add_multi_names (a, ths) pairs = - if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs + if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs else add_single_names (a, ths) pairs; fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri May 07 14:47:09 2010 +0200 @@ -410,7 +410,7 @@ | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) arity_clause dfg seen n (tcons,ars) | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) = - if class mem_string seen then (*multiple arities for the same tycon, class pair*) + if member (op =) seen class then (*multiple arities for the same tycon, class pair*) make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: arity_clause dfg seen (n+1) (tcons,ars) else diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/TFL/tfl.ML Fri May 07 14:47:09 2010 +0200 @@ -76,7 +76,7 @@ let val slist = Unsynchronized.ref names val vname = Unsynchronized.ref "u" fun new() = - if !vname mem_string (!slist) + if member (op =) (!slist) (!vname) then (vname := Symbol.bump_string (!vname); new()) else (slist := !vname :: !slist; !vname) in diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Fri May 07 14:47:09 2010 +0200 @@ -122,7 +122,7 @@ | dual x = HOLogic.Not $ x (* Term.term list -> bool *) fun has_duals [] = false - | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs + | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs in has_duals (HOLogic.disjuncts c) end; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/hologic.ML Fri May 07 14:47:09 2010 +0200 @@ -356,7 +356,7 @@ fun mk_ptupleT ps = let fun mk p Ts = - if p mem ps then + if member (op =) ps p then let val (T, Ts') = mk (1::p) Ts; val (U, Ts'') = mk (2::p) Ts' @@ -366,7 +366,7 @@ fun strip_ptupleT ps = let - fun factors p T = if p mem ps then (case T of + fun factors p T = if member (op =) ps p then (case T of Type ("*", [T1, T2]) => factors (1::p) T1 @ factors (2::p) T2 | _ => ptuple_err "strip_ptupleT") else [T] @@ -382,7 +382,7 @@ fun mk_ptuple ps = let fun mk p T ts = - if p mem ps then (case T of + if member (op =) ps p then (case T of Type ("*", [T1, T2]) => let val (t, ts') = mk (1::p) T1 ts; @@ -394,7 +394,7 @@ fun strip_ptuple ps = let - fun dest p t = if p mem ps then (case t of + fun dest p t = if member (op =) ps p then (case t of Const ("Pair", _) $ t $ u => dest (1::p) t @ dest (2::p) u | _ => ptuple_err "strip_ptuple") else [t] @@ -413,7 +413,7 @@ fun mk_psplits ps T T3 u = let fun ap ((p, T) :: pTs) = - if p mem ps then (case T of + if member (op =) ps p then (case T of Type ("*", [T1, T2]) => split_const (T1, T2, map snd pTs ---> T3) $ ap ((1::p, T1) :: (2::p, T2) :: pTs) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/inductive.ML Fri May 07 14:47:09 2010 +0200 @@ -288,7 +288,7 @@ then err bad_ind_occ else (); fun check_prem' prem t = - if head_of t mem cs then + if member (op =) cs (head_of t) then check_ind (err_in_prem ctxt err_name rule prem) t else (case t of Abs (_, _, t) => check_prem' prem t @@ -301,7 +301,7 @@ in (case concl of Const (@{const_name Trueprop}, _) $ t => - if head_of t mem cs then + if member (op =) cs (head_of t) then (check_ind (err_in_rule ctxt err_name rule') t; List.app check_prem (prems ~~ aprems)) else err_in_rule ctxt err_name rule' bad_concl diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Fri May 07 14:47:09 2010 +0200 @@ -140,7 +140,7 @@ fold_aterms (fn Var ((x, _), T) => cons (x, T) | _ => I) tm []; fun get_args _ _ [] = ([], []) - | get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x) + | get_args is i (x::xs) = (if member (op =) is i then apfst else apsnd) (cons x) (get_args is (i+1) xs); fun merge xs [] = xs @@ -237,7 +237,7 @@ end) ps)); -fun use_random () = "random_ind" mem !Codegen.mode; +fun use_random () = member (op =) (!Codegen.mode) "random_ind"; fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) = let @@ -557,7 +557,7 @@ fun mk_extra_defs thy defs gr dep names module ts = fold (fn name => fn gr => - if name mem names then gr + if member (op =) names name then gr else (case get_clauses thy name of NONE => gr @@ -576,7 +576,7 @@ val args = List.take (snd (strip_comb u), nparms); val arg_vs = maps term_vs args; - fun get_nparms s = if s mem names then SOME nparms else + fun get_nparms s = if member (op =) names s then SOME nparms else Option.map #3 (get_clauses thy s); fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) = @@ -585,7 +585,7 @@ Prem ([t, u], eq, false) | dest_prem (_ $ t) = (case strip_comb t of - (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t + (v as Var _, ts) => if member (op =) args v then Prem (ts, v, false) else Sidecond t | (c as Const (s, _), ts) => (case get_nparms s of NONE => Sidecond t @@ -704,7 +704,7 @@ val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1); val xs' = map (fn Bound i => nth xs (k - i)) ts; fun conv xs js = - if js mem fs then + if member (op =) fs js then let val (p, xs') = conv xs (1::js); val (q, xs'') = conv xs' (2::js) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Fri May 07 14:47:09 2010 +0200 @@ -57,7 +57,7 @@ fun relevant_vars prop = List.foldr (fn (Var ((a, i), T), vs) => (case strip_type T of - (_, Type (s, _)) => if s mem [@{type_name bool}] then (a, T) :: vs else vs + (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs | _ => vs) | (_, vs) => vs) [] (OldTerm.term_vars prop); @@ -90,7 +90,7 @@ val xs = map (pair "x") Ts; val u = list_comb (t, map Bound (i - 1 downto 0)) in - if a mem vs then + if member (op =) vs a then list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u) else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u) end @@ -257,7 +257,7 @@ let val rvs = map fst (relevant_vars (prop_of rule)); val xs = rev (Term.add_vars (prop_of rule) []); - val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs); + val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs); val rlzvs = rev (Term.add_vars (prop_of rrule) []); val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; val rs = map Var (subtract (op = o pairself fst) xs rlzvs); @@ -292,7 +292,7 @@ Sign.root_path |> Sign.add_path (Long_Name.implode prfx); val (ty_eqs, rlz_eqs) = split_list - (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss); + (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss); val thy1' = thy1 |> Theory.copy |> @@ -300,7 +300,7 @@ fold (fn s => AxClass.axiomatize_arity (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |> Extraction.add_typeof_eqns_i ty_eqs; - val dts = map_filter (fn (s, rs) => if s mem rsets then + val dts = map_filter (fn (s, rs) => if member (op =) rsets s then SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss; (** datatype representing computational content of inductive set **) @@ -363,7 +363,7 @@ (** realizer for induction rule **) - val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then + val Ps = map_filter (fn _ $ M $ P => if member (op =) rsets (pred_of M) then SOME (fst (fst (dest_Var (head_of P)))) else NONE) (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct))); @@ -471,7 +471,7 @@ list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) [])))))) (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4; val elimps = map_filter (fn ((s, intrs), p) => - if s mem rsets then SOME (p, intrs) else NONE) + if member (op =) rsets s then SOME (p, intrs) else NONE) (rss' ~~ (elims ~~ #elims ind_info)); val thy6 = fold (fn p as (((((elim, _), _), _), _), _) => diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/inductive_set.ML Fri May 07 14:47:09 2010 +0200 @@ -419,7 +419,7 @@ | infer (t $ u) = infer t #> infer u | infer _ = I; val new_arities = filter_out - (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1 + (fn (x as Free (_, T), _) => member (op =) params x andalso length (binder_types T) > 1 | _ => false) (fold (snd #> infer) intros []); val params' = map (fn x => (case AList.lookup op = new_arities x of diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/lin_arith.ML Fri May 07 14:47:09 2010 +0200 @@ -221,7 +221,7 @@ in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end handle TERM _ => add_atom all m pi) | poly (all as Const f $ x, m, pi) = - if f mem inj_consts then poly (x, m, pi) else add_atom all m pi + if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi | poly (all, m, pi) = add_atom all m pi val (p, i) = poly (lhs, Rat.one, ([], Rat.zero)) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/old_primrec.ML Fri May 07 14:47:09 2010 +0200 @@ -120,7 +120,7 @@ let val (f, ts) = strip_comb t; in - if is_Const f andalso dest_Const f mem map fst rec_eqns then + if is_Const f andalso member (op =) (map fst rec_eqns) (dest_Const f) then let val fnameT' as (fname', _) = dest_Const f; val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT'); diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Fri May 07 14:47:09 2010 +0200 @@ -114,7 +114,7 @@ in (case xs of [_] => (module, put_code module fundef gr2) | _ => - if not (dep mem xs) then + if not (member (op =) xs dep) then let val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; val module' = if_library thyname module; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/refute.ML Fri May 07 14:47:09 2010 +0200 @@ -463,7 +463,7 @@ in (* I'm not quite sure if checking the name 's' is sufficient, *) (* or if we should also check the type 'T'. *) - s mem_string class_const_names + member (op =) class_const_names s end; (* ------------------------------------------------------------------------- *) @@ -499,7 +499,7 @@ in (* I'm not quite sure if checking the name 's' is sufficient, *) (* or if we should also check the type 'T'. *) - s mem_string rec_names + member (op =) rec_names s end; (* ------------------------------------------------------------------------- *) @@ -932,7 +932,7 @@ | Datatype_Aux.DtType (_, ds) => collect_types dT (fold_rev collect_dtyp ds acc) | Datatype_Aux.DtRec i => - if dT mem acc then + if member (op =) acc dT then acc (* prevent infinite recursion *) else let @@ -2248,7 +2248,7 @@ (* if 't_elem' existed at the previous depth, *) (* proceed recursively, otherwise map the entire *) (* subtree to "undefined" *) - if t_elem mem terms' then + if member (op =) terms' t_elem then make_constr ds off else (make_undef ds, off)) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/sat_solver.ML Fri May 07 14:47:09 2010 +0200 @@ -350,7 +350,7 @@ o (map (map literal_from_int)) o clauses o (map int_from_string) - o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"]))) + o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"]))) o filter_preamble o filter (fn l => l <> "") o split_lines @@ -421,7 +421,7 @@ SOME (y::x::xs) (* int list -> int -> bool *) fun assignment_from_list xs i = - i mem xs + member (op =) xs i (* int list -> SatSolver.result *) fun solver_loop xs = if PropLogic.eval (assignment_from_list xs) fm then @@ -490,7 +490,7 @@ end (* int list -> int option *) fun fresh_var xs = - Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices + find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices (* int list -> prop_formula -> int list option *) (* partial assignment 'xs' *) fun dpll xs fm = diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/Tools/typedef_codegen.ML --- a/src/HOL/Tools/typedef_codegen.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/Tools/typedef_codegen.ML Fri May 07 14:47:09 2010 +0200 @@ -78,7 +78,7 @@ Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id), Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, Codegen.str "x) = x;"]) ^ "\n\n" ^ - (if "term_of" mem !Codegen.mode then + (if member (op =) (!Codegen.mode) "term_of" then Codegen.string_of (Pretty.block [Codegen.str "fun ", Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, @@ -89,7 +89,7 @@ Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1, Codegen.str "x;"]) ^ "\n\n" else "") ^ - (if "test" mem !Codegen.mode then + (if member (op =) (!Codegen.mode) "test" then Codegen.string_of (Pretty.block [Codegen.str "fun ", Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1, Codegen.str "i =", Pretty.brk 1, diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOL/ex/Groebner_Examples.thy --- a/src/HOL/ex/Groebner_Examples.thy Thu May 06 23:57:55 2010 +0200 +++ b/src/HOL/ex/Groebner_Examples.thy Fri May 07 14:47:09 2010 +0200 @@ -10,18 +10,30 @@ subsection {* Basic examples *} -schematic_lemma "3 ^ 3 == (?X::'a::{number_ring})" - by sring_norm +lemma + fixes x :: int + shows "x ^ 3 = x ^ 3" + apply (tactic {* ALLGOALS (CONVERSION + (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + by (rule refl) -schematic_lemma "(x - (-2))^5 == ?X::int" - by sring_norm +lemma + fixes x :: int + shows "(x - (-2))^5 = x ^ 5 + (10 * x ^ 4 + (40 * x ^ 3 + (80 * x\ + (80 * x + 32))))" + apply (tactic {* ALLGOALS (CONVERSION + (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + by (rule refl) -schematic_lemma "(x - (-2))^5 * (y - 78) ^ 8 == ?X::int" - by sring_norm +schematic_lemma + fixes x :: int + shows "(x - (-2))^5 * (y - 78) ^ 8 = ?X" + apply (tactic {* ALLGOALS (CONVERSION + (Conv.arg_conv (Conv.arg1_conv (Normalizer.semiring_normalize_conv @{context})))) *}) + by (rule refl) lemma "((-3) ^ (Suc (Suc (Suc 0)))) == (X::'a::{number_ring})" apply (simp only: power_Suc power_0) - apply (simp only: comp_arith) + apply (simp only: semiring_norm) oops lemma "((x::int) + y)^3 - 1 = (x - z)^2 - 10 \ x = z + 3 \ x = - y" diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOLCF/IOA/ABP/Check.ML --- a/src/HOLCF/IOA/ABP/Check.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOLCF/IOA/ABP/Check.ML Fri May 07 14:47:09 2010 +0200 @@ -16,7 +16,7 @@ let fun check_s(s,unchecked,checked) = let fun check_sa a unchecked = let fun check_sas t unchecked = - (if a mem extacts then + (if member (op =) extacts a then (if transA(hom s,a,hom t) then ( ) else (writeln("Error: Mapping of Externals!"); string_of_s s; writeln""; @@ -27,11 +27,11 @@ string_of_s s; writeln""; string_of_a a; writeln""; string_of_s t;writeln"";writeln"" )); - if t mem checked then unchecked else insert (op =) t unchecked) + if member (op =) checked t then unchecked else insert (op =) t unchecked) in fold check_sas (nexts s a) unchecked end; val unchecked' = fold check_sa (extacts @ intacts) unchecked - in (if s mem startsI then - (if hom(s) mem startsS then () + in (if member (op =) startsI s then + (if member (op =) startsS (hom s) then () else writeln("Error: At start states!")) else (); checks(unchecked',s::checked)) end diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOLCF/IOA/meta_theory/automaton.ML --- a/src/HOLCF/IOA/meta_theory/automaton.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML Fri May 07 14:47:09 2010 +0200 @@ -211,11 +211,11 @@ (* used by write_alts *) fun write_alt thy (chead,tr) inp out int [] = -if (chead mem inp) then +if member (op =) inp chead then ( error("Input action " ^ tr ^ " was not specified") ) else ( -if (chead mem (out@int)) then +if member (op =) out chead orelse member (op =) int chead then (writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else (); (tr ^ " => False",tr ^ " => False")) | write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) = @@ -227,9 +227,9 @@ occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r); in if (chead=(hd_of a)) then -(if ((chead mem inp) andalso e) then ( +(if member (op =) inp chead andalso e then ( error("Input action " ^ b ^ " has a precondition") -) else (if (chead mem (inp@out@int)) then +) else (if member (op =) (inp@out@int) chead then (if (occurs_again chead r) then ( error("Two specifications for action: " ^ b) ) else (b ^ " => " ^ c,b ^ " => " ^ d)) @@ -275,7 +275,7 @@ check_free_primed _ = []; fun overlap [] _ = true | -overlap (a::r) l = if (a mem l) then ( +overlap (a::r) l = if member (op =) l a then ( error("Two occurences of action " ^ a ^ " in automaton signature") ) else (overlap r l); diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Fri May 07 14:47:09 2010 +0200 @@ -228,7 +228,7 @@ fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = (case cont_eta_contract body of body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => - if not (0 mem loose_bnos f) then incr_boundvars ~1 f + if not (member (op =) (loose_bnos f) 0) then incr_boundvars ~1 f else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri May 07 14:47:09 2010 +0200 @@ -554,9 +554,9 @@ (* test for finiteness of domain definitions *) local val types = [@{type_name ssum}, @{type_name sprod}]; - fun finite d T = if T mem absTs then d else finite' d T + fun finite d T = if member (op =) absTs T then d else finite' d T and finite' d (Type (c, Ts)) = - let val d' = d andalso c mem types; + let val d' = d andalso member (op =) types c; in forall (finite d') Ts end | finite' d _ = true; in diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri May 07 14:47:09 2010 +0200 @@ -292,7 +292,7 @@ it has a possibly indirectly recursive argument that isn't/is possibly indirectly lazy *) fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => - is_rec arg andalso not(rec_of arg mem ns) andalso + is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Provers/Arith/cancel_div_mod.ML --- a/src/Provers/Arith/cancel_div_mod.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/Provers/Arith/cancel_div_mod.ML Fri May 07 14:47:09 2010 +0200 @@ -62,7 +62,7 @@ let val ts = Data.dest_sum t; val dpq = Data.mk_binop Data.div_name pq val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq) - val d = if d1 mem ts then d1 else d2 + val d = if member (op =) ts d1 then d1 else d2 val m = Data.mk_binop Data.mod_name pq in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri May 07 14:47:09 2010 +0200 @@ -389,7 +389,7 @@ |> sort (int_ord o pairself abs) |> hd val (eq as Lineq(_,_,ceq,_),othereqs) = - extract_first (fn Lineq(_,_,l,_) => c mem l) eqs + extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs val v = find_index (fn v => v = c) ceq val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) (othereqs @ noneqs) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Provers/order.ML --- a/src/Provers/order.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/Provers/order.ML Fri May 07 14:47:09 2010 +0200 @@ -871,8 +871,8 @@ val vi = getIndex v ntc in - if ui mem xreachable andalso vi mem xreachable andalso - ui mem yreachable andalso vi mem yreachable then ( + if member (op =) xreachable ui andalso member (op =) xreachable vi andalso + member (op =) yreachable ui andalso member (op =) yreachable vi then ( (case e of (Less (_, _, _)) => let diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Provers/trancl.ML --- a/src/Provers/trancl.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/Provers/trancl.ML Fri May 07 14:47:09 2010 +0200 @@ -452,8 +452,8 @@ fun processTranclEdges [] = raise Cannot | processTranclEdges (e::es) = - if (upper e) mem Vx andalso (lower e) mem Vx - andalso (upper e) mem Vy andalso (lower e) mem Vy + if member (op =) Vx (upper e) andalso member (op =) Vx (lower e) + andalso member (op =) Vy (upper e) andalso member (op =) Vy (lower e) then ( diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Pure/ProofGeneral/pgip_input.ML --- a/src/Pure/ProofGeneral/pgip_input.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/Pure/ProofGeneral/pgip_input.ML Fri May 07 14:47:09 2010 +0200 @@ -227,8 +227,8 @@ (* We allow sending proper document markup too; we map it back to dostep *) (* and strip out metainfo elements. Markup correctness isn't checked: this *) (* is a compatibility measure to make it easy for interfaces. *) - | x => if (x mem PgipMarkup.doc_markup_elements) then - if (x mem PgipMarkup.doc_markup_elements_ignored) then + | x => if member (op =) PgipMarkup.doc_markup_elements x then + if member (op =) PgipMarkup.doc_markup_elements_ignored x then raise NoAction else Dostep { text = xmltext data } (* could separate out Doitem too *) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Pure/library.ML --- a/src/Pure/library.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/Pure/library.ML Fri May 07 14:47:09 2010 +0200 @@ -11,7 +11,7 @@ infix 2 ? infix 3 o oo ooo oooo infix 4 ~~ upto downto -infix orf andf mem mem_int mem_string +infix orf andf signature BASIC_LIBRARY = sig @@ -164,9 +164,6 @@ val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list - val mem: ''a * ''a list -> bool - val mem_int: int * int list -> bool - val mem_string: string * string list -> bool val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool val distinct: ('a * 'a -> bool) -> 'a list -> 'a list @@ -801,13 +798,6 @@ else fold_rev (insert eq) ys xs; -(* old-style infixes *) - -fun x mem xs = member (op =) xs x; -fun (x: int) mem_int xs = member (op =) xs x; -fun (x: string) mem_string xs = member (op =) xs x; - - (* subset and set equality *) fun subset eq (xs, ys) = forall (member eq ys) xs; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Tools/Code/lib/Tools/codegen --- a/src/Tools/Code/lib/Tools/codegen Thu May 06 23:57:55 2010 +0200 +++ b/src/Tools/Code/lib/Tools/codegen Fri May 07 14:47:09 2010 +0200 @@ -58,7 +58,7 @@ QND_CMD="reset" fi -CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";" +CTXT_CMD="ML_Context.eval_in (SOME (ProofContext.init_global (theory \"HOL\"))) false Position.none \"Code_Target.shell_command thyname cmd\";" FULL_CMD="Unsynchronized.$QND_CMD quick_and_dirty; val thyname = \"$THY\"; val cmd = \"$CODE_CMD\"; $CTXT_CMD" diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Tools/Metis/metis_env.ML --- a/src/Tools/Metis/metis_env.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/Tools/Metis/metis_env.ML Fri May 07 14:47:09 2010 +0200 @@ -1,5 +1,5 @@ (* Metis-specific ML environment *) -nonfix ++ -- RL mem; +nonfix ++ -- RL; val explode = String.explode; val implode = String.implode; val print = TextIO.print; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/Tools/WWW_Find/unicode_symbols.ML --- a/src/Tools/WWW_Find/unicode_symbols.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/Tools/WWW_Find/unicode_symbols.ML Fri May 07 14:47:09 2010 +0200 @@ -82,7 +82,7 @@ -- Scan.many (not o Symbol.is_ascii_blank o symbol) >> (token AsciiSymbol o op ::); -fun not_contains xs c = not ((symbol c) mem_string (explode xs)); +fun not_contains xs c = not (member (op =) (explode xs) (symbol c)); val scan_comment = $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n")) >> token Comment; diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/ZF/Tools/datatype_package.ML Fri May 07 14:47:09 2010 +0200 @@ -58,7 +58,7 @@ @{const_name nat} :: map (#1 o dest_Const) rec_hds val u = if co then @{const QUniv.quniv} else @{const Univ.univ} val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) - (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t + (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t | _ => I)) con_ty_lists []; in u $ Ind_Syntax.union_params (hd rec_tms, cs) end; @@ -193,7 +193,7 @@ | rec_args ((Const(@{const_name mem},_)$arg$X)::prems) = (case head_of X of Const(a,_) => (*recursive occurrence?*) - if a mem_string rec_names + if member (op =) rec_names a then arg :: rec_args prems else rec_args prems | _ => rec_args prems) diff -r 97d2780ad6f0 -r 51e3b38a5e41 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu May 06 23:57:55 2010 +0200 +++ b/src/ZF/Tools/inductive_package.ML Fri May 07 14:47:09 2010 +0200 @@ -86,7 +86,7 @@ local (*Checking the introduction rules*) val intr_sets = map (#2 o rule_concl_msg thy) intr_tms; fun intr_ok set = - case head_of set of Const(a,recT) => a mem rec_names | _ => false; + case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false; in val dummy = assert_all intr_ok intr_sets (fn t => "Conclusion of rule does not name a recursive set: " ^