--- a/src/HOL/Algebra/abstract/Factor.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Algebra/abstract/Factor.ML Sat Nov 18 00:20:24 2006 +0100
@@ -18,7 +18,7 @@
by (induct_tac "factors" 1);
(* Base case: c dvd a contradicts irred c *)
by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1);
-by (blast_tac (claset() addIs [dvd_trans_ring]) 1);
+by (blast_tac (claset() addIs [thm "dvd_trans_ring"]) 1);
(* Induction step *)
by (ftac (thm "factorial_prime") 1);
by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1);
--- a/src/HOL/Algebra/abstract/Ideal2.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.ML Sat Nov 18 00:20:24 2006 +0100
@@ -124,7 +124,7 @@
Goal "ideal_of {0::'a::ring} = {0}";
by (simp_tac (simpset() addsimps [pideal_structure]) 1);
by (rtac subset_antisym 1);
-by (auto_tac (claset() addIs [dvd_zero_left], simpset()));
+by (auto_tac (claset() addIs [thm "dvd_zero_left"], simpset()));
qed "ideal_of_zero_eq";
Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I";
@@ -149,7 +149,7 @@
(* Ideals and divisibility *)
Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}";
-by (auto_tac (claset() addIs [dvd_trans_ring],
+by (auto_tac (claset() addIs [thm "dvd_trans_ring"],
simpset() addsimps [pideal_structure]));
qed "dvd_imp_subideal";
@@ -167,7 +167,7 @@
by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
by (etac conjE 1);
by (dres_inst_tac [("c", "a")] subsetD 1);
-by (auto_tac (claset() addIs [dvd_trans_ring],
+by (auto_tac (claset() addIs [thm "dvd_trans_ring"],
simpset()));
qed "psubideal_not_dvd";
--- a/src/HOL/Algebra/abstract/Ring2.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.ML Sat Nov 18 00:20:24 2006 +0100
@@ -164,61 +164,7 @@
*)
-(* Power *)
-
-Goal "!!a::'a::ring. a ^ 0 = 1";
-by (simp_tac (simpset() addsimps [power_def]) 1);
-qed "power_0";
-
-Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a";
-by (simp_tac (simpset() addsimps [power_def]) 1);
-qed "power_Suc";
-
-Addsimps [power_0, power_Suc];
-
-Goal "1 ^ n = (1::'a::ring)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "power_one";
-
-Goal "!!n. n ~= 0 ==> 0 ^ n = (0::'a::ring)";
-by (etac rev_mp 1);
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "power_zero";
-
-Addsimps [power_zero, power_one];
-
-Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)";
-by (induct_tac "m" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "power_mult";
-
-(* Divisibility *)
-section "Divisibility";
-
-Goalw [dvd_def] "!! a::'a::ring. a dvd 0";
-by (res_inst_tac [("x", "0")] exI 1);
-by (Simp_tac 1);
-qed "dvd_zero_right";
-
-Goalw [dvd_def] "!! a::'a::ring. 0 dvd a ==> a = 0";
-by Auto_tac;
-qed "dvd_zero_left";
-
-Goalw [dvd_def] "!! a::'a::ring. a dvd a";
-by (res_inst_tac [("x", "1")] exI 1);
-by (Simp_tac 1);
-qed "dvd_refl_ring";
-
-Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c";
-by (Step_tac 1);
-by (res_inst_tac [("x", "k * ka")] exI 1);
-by (Asm_simp_tac 1);
-qed "dvd_trans_ring";
-
-Addsimps [dvd_zero_right, dvd_refl_ring];
+val dvd_def = thm "dvd_def'";
Goalw [dvd_def]
"!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1";
@@ -366,7 +312,7 @@
section "Fields";
Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)";
-by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left],
+by (auto_tac (claset() addDs [thm "field_ax", thm "dvd_zero_left"],
simpset() addsimps [thm "field_one_not_zero"]));
qed "field_unit";
--- a/src/HOL/Algebra/abstract/Ring2.thy Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sat Nov 18 00:20:24 2006 +0100
@@ -231,4 +231,54 @@
"(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)"
by (simp add: m_lcancel)
+lemma power_0 [simp]:
+ "(a::'a::ring) ^ 0 = 1" unfolding power_def by simp
+
+lemma power_Suc [simp]:
+ "(a::'a::ring) ^ Suc n = a ^ n * a" unfolding power_def by simp
+
+lemma power_one [simp]:
+ "1 ^ n = (1::'a::ring)" by (induct n) simp_all
+
+lemma power_zero [simp]:
+ "n \<noteq> 0 \<Longrightarrow> 0 ^ n = (0::'a::ring)" by (induct n) simp_all
+
+lemma power_mult [simp]:
+ "(a::'a::ring) ^ m * a ^ n = a ^ (m + n)"
+ by (induct m) simp_all
+
+
+section "Divisibility"
+
+lemma dvd_zero_right [simp]:
+ "(a::'a::ring) dvd 0"
+proof
+ show "0 = a * 0" by simp
+qed
+
+lemma dvd_zero_left:
+ "0 dvd (a::'a::ring) \<Longrightarrow> a = 0" unfolding dvd_def by simp
+
+lemma dvd_refl_ring [simp]:
+ "(a::'a::ring) dvd a"
+proof
+ show "a = a * 1" by simp
+qed
+
+lemma dvd_trans_ring:
+ fixes a b c :: "'a::ring"
+ assumes a_dvd_b: "a dvd b"
+ and b_dvd_c: "b dvd c"
+ shows "a dvd c"
+proof -
+ from a_dvd_b obtain l where "b = a * l" using dvd_def by blast
+ moreover from b_dvd_c obtain j where "c = b * j" using dvd_def by blast
+ ultimately have "c = a * (l * j)" by simp
+ then have "\<exists>k. c = a * k" ..
+ then show ?thesis using dvd_def by blast
+qed
+
+lemma dvd_def':
+ "m dvd n \<equiv> \<exists>k. n = m * k" unfolding dvd_def by simp
+
end
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sat Nov 18 00:20:24 2006 +0100
@@ -187,8 +187,8 @@
"-" > "HOL.minus" :: "[nat,nat]=>nat"
MIN > Orderings.min :: "[nat,nat]=>nat"
MAX > Orderings.max :: "[nat,nat]=>nat"
- DIV > "Divides.op div" :: "[nat,nat]=>nat"
- MOD > "Divides.op mod" :: "[nat,nat]=>nat"
+ DIV > "Divides.div" :: "[nat,nat]=>nat"
+ MOD > "Divides.mod" :: "[nat,nat]=>nat"
EXP > Nat.power :: "[nat,nat]=>nat";
end_import;
@@ -208,7 +208,7 @@
import_theory divides;
const_maps
- divides > "Divides.op dvd" :: "[nat,nat]=>bool";
+ divides > "Divides.dvd" :: "[nat,nat]=>bool";
end_import;
--- a/src/HOL/Import/HOL/arithmetic.imp Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Sat Nov 18 00:20:24 2006 +0100
@@ -14,12 +14,12 @@
"NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
"NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
"NUMERAL" > "HOL4Compat.NUMERAL"
- "MOD" > "Divides.op mod" :: "nat => nat => nat"
+ "MOD" > "Divides.mod" :: "nat => nat => nat"
"MIN" > "Orderings.min" :: "nat => nat => nat"
"MAX" > "Orderings.max" :: "nat => nat => nat"
"FUNPOW" > "HOL4Compat.FUNPOW"
"EXP" > "Nat.power" :: "nat => nat => nat"
- "DIV" > "Divides.op div" :: "nat => nat => nat"
+ "DIV" > "Divides.div" :: "nat => nat => nat"
"ALT_ZERO" > "HOL4Compat.ALT_ZERO"
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
--- a/src/HOL/Import/HOL/divides.imp Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Import/HOL/divides.imp Sat Nov 18 00:20:24 2006 +0100
@@ -3,7 +3,7 @@
import_segment "hol4"
const_maps
- "divides" > "Divides.op dvd" :: "nat => nat => bool"
+ "divides" > "Divides.dvd" :: "nat => nat => bool"
thm_maps
"divides_def" > "HOL4Compat.divides_def"
--- a/src/HOL/Integ/IntDiv_setup.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/IntDiv_setup.ML Sat Nov 18 00:20:24 2006 +0100
@@ -10,8 +10,8 @@
structure CancelDivModData =
struct
-val div_name = "Divides.op div";
-val mod_name = "Divides.op mod";
+val div_name = "Divides.div";
+val mod_name = "Divides.mod";
val mk_binop = HOLogic.mk_binop;
val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
val dest_sum = Int_Numeral_Simprocs.dest_sum;
--- a/src/HOL/Integ/cooper_dec.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/cooper_dec.ML Sat Nov 18 00:20:24 2006 +0100
@@ -203,10 +203,10 @@
fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t);
-fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =
+fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
if is_numeral c then
let val c' = (mk_numeral(abs(dest_numeral c)))
- in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t))
+ in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t))
end
else (warning "Nonlinear term --- Non numeral leftside at dvd"
;raise COOPER)
@@ -283,7 +283,7 @@
let val xp = (HOLogic.mk_binop "HOL.plus"
((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
in
- HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm)
+ HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm)
end
end;
@@ -354,7 +354,7 @@
(* The LCM of all the divisors that involve x. *)
(* ------------------------------------------------------------------------- *)
-fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
+fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
if x = y then abs(dest_numeral d) else 1
|divlcm x ( Const ("Not", _) $ p) = divlcm x p
|divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q)
@@ -450,7 +450,7 @@
val operations =
[("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) ,
("op >=",IntInf.>=),
- ("Divides.op dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))];
+ ("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))];
fun applyoperation (SOME f) (a,b) = f (a, b)
|applyoperation _ (_, _) = false;
@@ -460,7 +460,7 @@
(*
fun evalc_atom at = case at of
(Const (p,_) $ s $ t) =>
- (if p="Divides.op dvd" then
+ (if p="Divides.dvd" then
((if dvd_op(s,t) then HOLogic.true_const
else HOLogic.false_const)
handle _ => at)
--- a/src/HOL/Integ/cooper_proof.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/cooper_proof.ML Sat Nov 18 00:20:24 2006 +0100
@@ -300,7 +300,7 @@
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
- |"Divides.op dvd" =>
+ |"Divides.dvd" =>
let val pre = prove_elementar sg "lf"
(HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
@@ -346,16 +346,16 @@
(instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+ |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
c $ y ) $ z))) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
@@ -384,7 +384,7 @@
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf))
@@ -392,7 +392,7 @@
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -444,16 +444,16 @@
else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+ |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
c $ y ) $ z))) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
@@ -483,7 +483,7 @@
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf))
@@ -491,7 +491,7 @@
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -595,18 +595,18 @@
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -685,18 +685,18 @@
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -772,7 +772,7 @@
|(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
|(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
- |(Const("Divides.op dvd",_)$d$r) =>
+ |(Const("Divides.dvd",_)$d$r) =>
if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
else (warning "Nonlinear Term --- Non numeral leftside at dvd";
raise COOPER)
--- a/src/HOL/Integ/int_factor_simprocs.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML Sat Nov 18 00:20:24 2006 +0100
@@ -64,8 +64,8 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.op div"
- val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
+ val mk_bal = HOLogic.mk_binop "Divides.div"
+ val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
val cancel = int_mult_div_cancel1 RS trans
val neg_exchanges = false
)
@@ -272,8 +272,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.op div"
- val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
+ val mk_bal = HOLogic.mk_binop "Divides.div"
+ val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.intT
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj
);
--- a/src/HOL/Integ/nat_simprocs.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Sat Nov 18 00:20:24 2006 +0100
@@ -294,8 +294,8 @@
structure DivCancelNumeralFactor = CancelNumeralFactorFun
(open CancelNumeralFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.op div"
- val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
+ val mk_bal = HOLogic.mk_binop "Divides.div"
+ val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.natT
val cancel = nat_mult_div_cancel1 RS trans
val neg_exchanges = false
)
@@ -404,8 +404,8 @@
structure DivideCancelFactor = ExtractCommonTermFun
(open CancelFactorCommon
val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
- val mk_bal = HOLogic.mk_binop "Divides.op div"
- val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
+ val mk_bal = HOLogic.mk_binop "Divides.div"
+ val dest_bal = HOLogic.dest_bin "Divides.div" HOLogic.natT
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_div_cancel_disj
);
--- a/src/HOL/Integ/presburger.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/presburger.ML Sat Nov 18 00:20:24 2006 +0100
@@ -135,9 +135,9 @@
("Orderings.less_eq", iT --> iT --> bT),
("op =", iT --> iT --> bT),
("Orderings.less", iT --> iT --> bT),
- ("Divides.op dvd", iT --> iT --> bT),
- ("Divides.op div", iT --> iT --> iT),
- ("Divides.op mod", iT --> iT --> iT),
+ ("Divides.dvd", iT --> iT --> bT),
+ ("Divides.div", iT --> iT --> iT),
+ ("Divides.mod", iT --> iT --> iT),
("HOL.plus", iT --> iT --> iT),
("HOL.minus", iT --> iT --> iT),
("HOL.times", iT --> iT --> iT),
@@ -149,9 +149,9 @@
("Orderings.less_eq", nT --> nT --> bT),
("op =", nT --> nT --> bT),
("Orderings.less", nT --> nT --> bT),
- ("Divides.op dvd", nT --> nT --> bT),
- ("Divides.op div", nT --> nT --> nT),
- ("Divides.op mod", nT --> nT --> nT),
+ ("Divides.dvd", nT --> nT --> bT),
+ ("Divides.div", nT --> nT --> nT),
+ ("Divides.mod", nT --> nT --> nT),
("HOL.plus", nT --> nT --> nT),
("HOL.minus", nT --> nT --> nT),
("HOL.times", nT --> nT --> nT),
--- a/src/HOL/Integ/reflected_cooper.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Integ/reflected_cooper.ML Sat Nov 18 00:20:24 2006 +0100
@@ -31,7 +31,7 @@
| Const("False",_) => F
| Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
| Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
- | Const ("Divides.op dvd",_)$t1$t2 =>
+ | Const ("Divides.dvd",_)$t1$t2 =>
Divides(i_of_term vs t1,i_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
if (domain_type eqT = HOLogic.intT)
@@ -99,7 +99,7 @@
(term_of_i vs t2)$(term_of_i vs t1)
| Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Divides(t1,t2) => Const("Divides.op dvd",[iT,iT] ---> bT)$
+ | Divides(t1,t2) => Const("Divides.dvd",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
| NOT t' => HOLogic.Not$(term_of_qf vs t')
| And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2)
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Sat Nov 18 00:20:24 2006 +0100
@@ -203,10 +203,10 @@
fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t);
-fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =
+fun linform vars (Const ("Divides.dvd",_) $ c $ t) =
if is_numeral c then
let val c' = (mk_numeral(abs(dest_numeral c)))
- in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t))
+ in (HOLogic.mk_binrel "Divides.dvd" (c,lint vars t))
end
else (warning "Nonlinear term --- Non numeral leftside at dvd"
;raise COOPER)
@@ -283,7 +283,7 @@
let val xp = (HOLogic.mk_binop "HOL.plus"
((HOLogic.mk_binop "HOL.times" ((mk_numeral 1), x )), zero))
in
- HOLogic.conj $(HOLogic.mk_binrel "Divides.op dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm)
+ HOLogic.conj $(HOLogic.mk_binrel "Divides.dvd" ((mk_numeral l) , xp )) $ (adjustcoeff x l fm)
end
end;
@@ -354,7 +354,7 @@
(* The LCM of all the divisors that involve x. *)
(* ------------------------------------------------------------------------- *)
-fun divlcm x (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
+fun divlcm x (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z ) ) =
if x = y then abs(dest_numeral d) else 1
|divlcm x ( Const ("Not", _) $ p) = divlcm x p
|divlcm x ( Const ("op &",_) $ p $ q) = lcm_num (divlcm x p) (divlcm x q)
@@ -450,7 +450,7 @@
val operations =
[("op =",op=), ("Orderings.less",IntInf.<), ("op >",IntInf.>), ("Orderings.less_eq",IntInf.<=) ,
("op >=",IntInf.>=),
- ("Divides.op dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))];
+ ("Divides.dvd",fn (x,y) =>((IntInf.mod(y, x)) = 0))];
fun applyoperation (SOME f) (a,b) = f (a, b)
|applyoperation _ (_, _) = false;
@@ -460,7 +460,7 @@
(*
fun evalc_atom at = case at of
(Const (p,_) $ s $ t) =>
- (if p="Divides.op dvd" then
+ (if p="Divides.dvd" then
((if dvd_op(s,t) then HOLogic.true_const
else HOLogic.false_const)
handle _ => at)
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Sat Nov 18 00:20:24 2006 +0100
@@ -300,7 +300,7 @@
in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
end
- |"Divides.op dvd" =>
+ |"Divides.dvd" =>
let val pre = prove_elementar sg "lf"
(HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("HOL.zero",HOLogic.intT),(mk_numeral k))))
val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
@@ -346,16 +346,16 @@
(instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
- |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+ |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
c $ y ) $ z))) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
@@ -384,7 +384,7 @@
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_minf))
@@ -392,7 +392,7 @@
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
- |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
@@ -444,16 +444,16 @@
else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
- |(Const("Divides.op dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
+ |(Const("Divides.dvd",_)$ d $ (db as (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $
c $ y ) $ z))) =>
if y=x then let val cz = cterm_of sg (norm_zero_one z)
- val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
+ val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero)
in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
end
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
@@ -483,7 +483,7 @@
if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
(instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz] (not_dvd_eq_pinf))
@@ -491,7 +491,7 @@
else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
- |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then let val cd = cterm_of sg (norm_zero_one d)
val cz = cterm_of sg (norm_zero_one z)
in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
@@ -595,18 +595,18 @@
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
- |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
@@ -685,18 +685,18 @@
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |Const ("Not",_) $ (Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
- |(Const("Divides.op dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
+ |(Const("Divides.dvd",_)$ d $ (Const ("HOL.plus",_) $ (Const ("HOL.times",_) $ c $ y ) $ z)) =>
if y=x then
let val cz = cterm_of sg (norm_zero_one z)
- val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
+ val th1 = (prove_elementar sg "ss" (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
in (instantiate' [] [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
end
else (instantiate' [] [SOME cfma, SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
@@ -772,7 +772,7 @@
|(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
|(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
- |(Const("Divides.op dvd",_)$d$r) =>
+ |(Const("Divides.dvd",_)$d$r) =>
if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
else (warning "Nonlinear Term --- Non numeral leftside at dvd";
raise COOPER)
--- a/src/HOL/Tools/Presburger/presburger.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML Sat Nov 18 00:20:24 2006 +0100
@@ -135,9 +135,9 @@
("Orderings.less_eq", iT --> iT --> bT),
("op =", iT --> iT --> bT),
("Orderings.less", iT --> iT --> bT),
- ("Divides.op dvd", iT --> iT --> bT),
- ("Divides.op div", iT --> iT --> iT),
- ("Divides.op mod", iT --> iT --> iT),
+ ("Divides.dvd", iT --> iT --> bT),
+ ("Divides.div", iT --> iT --> iT),
+ ("Divides.mod", iT --> iT --> iT),
("HOL.plus", iT --> iT --> iT),
("HOL.minus", iT --> iT --> iT),
("HOL.times", iT --> iT --> iT),
@@ -149,9 +149,9 @@
("Orderings.less_eq", nT --> nT --> bT),
("op =", nT --> nT --> bT),
("Orderings.less", nT --> nT --> bT),
- ("Divides.op dvd", nT --> nT --> bT),
- ("Divides.op div", nT --> nT --> nT),
- ("Divides.op mod", nT --> nT --> nT),
+ ("Divides.dvd", nT --> nT --> bT),
+ ("Divides.div", nT --> nT --> nT),
+ ("Divides.mod", nT --> nT --> nT),
("HOL.plus", nT --> nT --> nT),
("HOL.minus", nT --> nT --> nT),
("HOL.times", nT --> nT --> nT),
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML Sat Nov 18 00:20:24 2006 +0100
@@ -31,7 +31,7 @@
| Const("False",_) => F
| Const("Orderings.less",_)$t1$t2 => Lt (i_of_term vs t1,i_of_term vs t2)
| Const("Orderings.less_eq",_)$t1$t2 => Le (i_of_term vs t1,i_of_term vs t2)
- | Const ("Divides.op dvd",_)$t1$t2 =>
+ | Const ("Divides.dvd",_)$t1$t2 =>
Divides(i_of_term vs t1,i_of_term vs t2)
| Const("op =",eqT)$t1$t2 =>
if (domain_type eqT = HOLogic.intT)
@@ -99,7 +99,7 @@
(term_of_i vs t2)$(term_of_i vs t1)
| Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
- | Divides(t1,t2) => Const("Divides.op dvd",[iT,iT] ---> bT)$
+ | Divides(t1,t2) => Const("Divides.dvd",[iT,iT] ---> bT)$
(term_of_i vs t1)$(term_of_i vs t2)
| NOT t' => HOLogic.Not$(term_of_qf vs t')
| And(t1,t2) => HOLogic.conj$(term_of_qf vs t1)$(term_of_qf vs t2)
--- a/src/HOL/Tools/res_clause.ML Sat Nov 18 00:20:22 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML Sat Nov 18 00:20:24 2006 +0100
@@ -117,7 +117,7 @@
("HOL.plus", "plus"),
("HOL.minus", "minus"),
("HOL.times", "times"),
- ("Divides.op div", "div"),
+ ("Divides.div", "div"),
("HOL.divide", "divide"),
("op -->", "implies"),
("{}", "emptyset"),