--- 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.
--- 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
(*
--- 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
--- 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.
--- 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
--- 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;
--- 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;
--- 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;
--- 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 \<longleftrightarrow> b \<noteq> 0 \<and> 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 \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y"
+ by (simp add: add_divide_distrib)
+
+lemma add_num_frac:
+ "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
+ by (simp add: add_divide_distrib add.commute)
+
end
--- 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: "\<not> 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 \<Rightarrow> 'a \<Rightarrow> 'a"
and neg :: "'a \<Rightarrow> '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 \<Rightarrow> 'a \<Rightarrow> 'a"
and inverse:: "'a \<Rightarrow> '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 \<longleftrightarrow> y = z"
and add_mul_solve: "add (mul w y) (mul x z) =
add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
@@ -313,22 +245,23 @@
thus "x = add x a \<longleftrightarrow> 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 \<longleftrightarrow> 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) \<noteq> 0"
- and ab: "a*b = 0" shows "b = 0"
-proof -
- { assume bz: "b \<noteq> 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 \<longleftrightarrow> w = x \<or> 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 \<or> w - x = 0" by (rule divisors_zero)
+ then show "w = x \<or> 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 \<noteq> z"
- hence ynz': "y - z \<noteq> 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 \<or> 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 \<and> Q) = (Q \<and> P)" "(P \<or> Q) = (Q \<or> P)"
@@ -423,23 +357,16 @@
"P \<equiv> False \<Longrightarrow> \<not> P"
"\<not> P \<Longrightarrow> (P \<equiv> 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\<noteq> 0 \<Longrightarrow> (x::'a::field_inverse_zero) / y + z = (x + z*y) / y"
- by (simp add: add_divide_distrib)
-lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> 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 \<le> ?c"},
- @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
- @{cpat "?c \<le> (?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
--- 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)
--- 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
--- 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
--- 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))
--- 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\<Colon>semiring_1 \<Rightarrow> bool"
-where
+definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" where
"iszero z \<longleftrightarrow> 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: "\<not> iszero 1"
+ by (simp add: iszero_def)
+
+lemma not_iszero_Numeral1: "\<not> 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 *}
--- 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 \
--- 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) \<and> 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)
--- 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,
--- 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);
--- 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;
--- 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)
--- 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" ]]
--- 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: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
- have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
by (metis abs_mult)
@@ -70,7 +70,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
by (metis abs_mult)
have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
@@ -92,7 +92,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
@@ -111,7 +111,7 @@
proof -
fix c :: 'a and x :: 'b
assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
- have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+ have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" 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 "\<forall>x. lb x \<le> 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 -
--- 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
--- 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 \<in> 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 \<in> 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\<in>{x - ?d..x + ?d}"
have e:"e = setsum (\<lambda>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 \<le> 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:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
--- 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 "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
also have "\<dots> \<le> 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)) \<le> e / B * norm(g z - g y)" using d' k by auto
- also have "\<dots> \<le> e * norm(z - y)" unfolding mult_frac_num pos_divide_le_eq[OF `B>0`]
+ also have "\<dots> \<le> 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)) \<le> e * norm (z - y)" by simp qed(insert k, auto) qed qed
--- 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 \<ge> 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le)
qed have **:"norm (1::real) \<le> 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 "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x $ k - c\<bar> \<le> 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 "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
\<longrightarrow> 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]
--- 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
--- 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
--- 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)
--- 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
--- 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)
--- 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))
--- 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 (\<Union>X \<in> 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} \<in> preal"
-by (simp add: preal_def cut_of_rat)
-
-lemma rat_subset_imp_le:
- "[|{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x|] ==> x \<le> 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 \<in> 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 \<and> x < q}"
-by (simp add: preal_of_rat_def rat_mem_preal)
+lemma Rep_preal_one:
+ "Rep_preal 1 = {x. 0 < x \<and> 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) \<subseteq> Rep_preal(inverse R * R)"
-apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff
+ "Rep_preal 1 \<subseteq> 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) \<subseteq> 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) \<subseteq> 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 \<noteq> 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 \<le> S + T) = (R \<le> S)"
-by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right)
-
lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> 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 "\<exists>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 "\<exists>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 \<le> preal_of_rat y) = (x \<le> 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
--- 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) =
--- 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 \<in> space M"
{ fix m n :: nat assume "m \<le> 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))) \<le> 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 \<le> 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 (\<lambda>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)
--- 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 \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
+begin
+
+lemma divisors_zero:
+ assumes "a * b = 0"
+ shows "a = 0 \<or> b = 0"
+proof (rule classical)
+ assume "\<not> (a = 0 \<or> b = 0)"
+ then have "a \<noteq> 0" and "b \<noteq> 0" by auto
+ with no_zero_divisors have "a * b \<noteq> 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
--- 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]);
--- 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])
--- 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
--- 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
--- 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 =
--- 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
--- 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;
--- 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;
--- 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;
--- 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;
--- 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
--- 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 =
--- 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;
--- 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
--- 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
--- 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;
--- 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
--- 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
--- 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;
--- 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)
--- 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
--- 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)
--- 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, _), _), _), _), _) =>
--- 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
--- 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))
--- 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');
--- 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;
--- 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))
--- 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 =
--- 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,
--- 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\<twosuperior> + (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 \<Longrightarrow> x = z + 3 \<Longrightarrow> x = - y"
--- 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
--- 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);
--- 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
--- 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
--- 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))))
--- 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
--- 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)
--- 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
--- 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 (
--- 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 *)
--- 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;
--- 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"
--- 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;
--- 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;
--- 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)
--- 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: " ^