--- a/src/HOL/Algebra/abstract/Factor.ML Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/Factor.ML Sat Sep 17 20:49:14 2005 +0200
@@ -33,14 +33,14 @@
by (Auto_tac);
qed "irred_dvd_list";
-Goalw [Factorisation_def] "!! c::'a::factorial. \
+Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \
\ [| irred c; Factorisation x factors u; c dvd x |] ==> \
\ EX d. c assoc d & d : set factors";
by (rtac (irred_dvd_list_lemma RS mp) 1);
by (Auto_tac);
qed "Factorisation_dvd";
-Goalw [Factorisation_def] "!! c::'a::factorial. \
+Goalw [thm "Factorisation_def"] "!! c::'a::factorial. \
\ [| Factorisation x factors u; a : set factors |] ==> irred a";
by (Blast_tac 1);
qed "Factorisation_irred";
--- a/src/HOL/Algebra/abstract/Factor.thy Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/Factor.thy Sat Sep 17 20:49:14 2005 +0200
@@ -4,15 +4,13 @@
Author: Clemens Ballarin, started 25 November 1997
*)
-Factor = Ring +
+theory Factor imports Ring begin
-consts
- Factorisation :: ['a::ring, 'a list, 'a] => bool
+constdefs
+ Factorisation :: "['a::ring, 'a list, 'a] => bool"
(* factorisation of x into a list of irred factors and a unit u *)
-
-defs
- Factorisation_def "Factorisation x factors u ==
- x = foldr op* factors u &
- (ALL a : set factors. irred a) & u dvd 1"
+ "Factorisation x factors u ==
+ x = foldr op* factors u &
+ (ALL a : set factors. irred a) & u dvd 1"
end
--- a/src/HOL/Algebra/abstract/Field.thy Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/Field.thy Sat Sep 17 20:49:14 2005 +0200
@@ -4,12 +4,18 @@
Author: Clemens Ballarin, started 15 November 1997
*)
-Field = Factor + PID +
+theory Field imports Factor PID begin
-instance
- field < domain (field_one_not_zero, field_integral)
+instance field < "domain"
+ apply intro_classes
+ apply (rule field_one_not_zero)
+ apply (erule field_integral)
+ done
-instance
- field < factorial (TrueI, field_fact_prime)
+instance field < factorial
+ apply intro_classes
+ apply (rule TrueI)
+ apply (erule field_fact_prime)
+ done
end
--- a/src/HOL/Algebra/abstract/Ideal.ML Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.ML Sat Sep 17 20:49:14 2005 +0200
@@ -6,38 +6,38 @@
(* is_ideal *)
-Goalw [is_ideal_def]
+Goalw [thm "is_ideal_def"]
"!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \
\ !! a. a:I ==> - a : I; 0 : I; \
\ !! a r. a:I ==> a * r : I |] ==> is_ideal I";
by Auto_tac;
qed "is_idealI";
-Goalw [is_ideal_def] "[| is_ideal I; a:I; b:I |] ==> a + b : I";
+Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I; b:I |] ==> a + b : I";
by (Fast_tac 1);
qed "is_ideal_add";
-Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> - a : I";
+Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> - a : I";
by (Fast_tac 1);
qed "is_ideal_uminus";
-Goalw [is_ideal_def] "[| is_ideal I |] ==> 0 : I";
+Goalw [thm "is_ideal_def"] "[| is_ideal I |] ==> 0 : I";
by (Fast_tac 1);
qed "is_ideal_zero";
-Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> a * r : I";
+Goalw [thm "is_ideal_def"] "[| is_ideal I; a:I |] ==> a * r : I";
by (Fast_tac 1);
qed "is_ideal_mult";
-Goalw [dvd_def, is_ideal_def] "[| a dvd b; is_ideal I; a:I |] ==> b:I";
+Goalw [dvd_def, thm "is_ideal_def"] "[| a dvd b; is_ideal I; a:I |] ==> b:I";
by (Fast_tac 1);
qed "is_ideal_dvd";
-Goalw [is_ideal_def] "is_ideal (UNIV::('a::ring) set)";
+Goalw [thm "is_ideal_def"] "is_ideal (UNIV::('a::ring) set)";
by Auto_tac;
qed "UNIV_is_ideal";
-Goalw [is_ideal_def] "is_ideal {0::'a::ring}";
+Goalw [thm "is_ideal_def"] "is_ideal {0::'a::ring}";
by Auto_tac;
qed "zero_is_ideal";
@@ -69,21 +69,21 @@
(* ideal_of *)
-Goalw [is_ideal_def, ideal_of_def] "is_ideal (ideal_of S)";
+Goalw [thm "is_ideal_def", thm "ideal_of_def"] "is_ideal (ideal_of S)";
by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *)
qed "ideal_of_is_ideal";
-Goalw [ideal_of_def] "a:S ==> a : (ideal_of S)";
+Goalw [thm "ideal_of_def"] "a:S ==> a : (ideal_of S)";
by Auto_tac;
qed "generator_in_ideal";
-Goalw [ideal_of_def] "ideal_of {1::'a::ring} = UNIV";
+Goalw [thm "ideal_of_def"] "ideal_of {1::'a::ring} = UNIV";
by (force_tac (claset() addDs [is_ideal_mult],
simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1);
(* FIXME: Zumkeller's order raises Domain exn *)
qed "ideal_of_one_eq";
-Goalw [ideal_of_def] "ideal_of {} = {0::'a::ring}";
+Goalw [thm "ideal_of_def"] "ideal_of {} = {0::'a::ring}";
by (rtac subset_antisym 1);
by (rtac subsetI 1);
by (dtac InterD 1);
@@ -91,7 +91,7 @@
by (auto_tac (claset(), simpset() addsimps [is_ideal_zero]));
qed "ideal_of_empty_eq";
-Goalw [ideal_of_def] "ideal_of {a} = {x::'a::ring. a dvd x}";
+Goalw [thm "ideal_of_def"] "ideal_of {a} = {x::'a::ring. a dvd x}";
by (rtac subset_antisym 1);
by (rtac subsetI 1);
by (dtac InterD 1);
@@ -100,7 +100,7 @@
by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1);
qed "pideal_structure";
-Goalw [ideal_of_def]
+Goalw [thm "ideal_of_def"]
"ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}";
by (rtac subset_antisym 1);
by (rtac subsetI 1);
@@ -117,7 +117,7 @@
by (Simp_tac 1);
qed "ideal_of_2_structure";
-Goalw [ideal_of_def] "A <= B ==> ideal_of A <= ideal_of B";
+Goalw [thm "ideal_of_def"] "A <= B ==> ideal_of A <= ideal_of B";
by Auto_tac;
qed "ideal_of_mono";
@@ -134,15 +134,15 @@
(* is_pideal *)
-Goalw [is_pideal_def] "is_pideal (I::('a::ring) set) ==> is_ideal I";
+Goalw [thm "is_pideal_def"] "is_pideal (I::('a::ring) set) ==> is_ideal I";
by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1);
qed "is_pideal_imp_is_ideal";
-Goalw [is_pideal_def] "is_pideal (ideal_of {a::'a::ring})";
+Goalw [thm "is_pideal_def"] "is_pideal (ideal_of {a::'a::ring})";
by (Fast_tac 1);
qed "pideal_is_pideal";
-Goalw [is_pideal_def] "is_pideal I ==> EX a. I = ideal_of {a}";
+Goalw [thm "is_pideal_def"] "is_pideal I ==> EX a. I = ideal_of {a}";
by (assume_tac 1);
qed "is_pidealD";
@@ -284,8 +284,8 @@
by (Clarify_tac 3);
by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")]
irred_imp_max_ideal 3);
-by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax],
- simpset() addsimps [thm "irred_def", not_dvd_psubideal, pid_ax]));
+by (auto_tac (claset() addIs [ideal_of_is_ideal, thm "pid_ax"],
+ simpset() addsimps [thm "irred_def", not_dvd_psubideal, thm "pid_ax"]));
by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1);
by (Clarify_tac 1);
by (dres_inst_tac [("f", "op* aa")] arg_cong 1);
@@ -311,7 +311,7 @@
by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1);
qed "proper_ideal";
-Goalw [is_pideal_def] "is_ideal (I::('a::field) set) ==> is_pideal I";
+Goalw [thm "is_pideal_def"] "is_ideal (I::('a::field) set) ==> is_pideal I";
by (case_tac "I = {0}" 1);
by (res_inst_tac [("x", "0")] exI 1);
by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1);
--- a/src/HOL/Algebra/abstract/Ideal.thy Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.thy Sat Sep 17 20:49:14 2005 +0200
@@ -4,25 +4,23 @@
Author: Clemens Ballarin, started 24 September 1999
*)
-Ideal = Ring +
+theory Ideal imports Ring begin
consts
- ideal_of :: ('a::ring) set => 'a set
- is_ideal :: ('a::ring) set => bool
- is_pideal :: ('a::ring) set => bool
+ ideal_of :: "('a::ring) set => 'a set"
+ is_ideal :: "('a::ring) set => bool"
+ is_pideal :: "('a::ring) set => bool"
defs
- is_ideal_def "is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
- (ALL a: I. - a : I) & 0 : I &
- (ALL a: I. ALL r. a * r : I)"
- ideal_of_def "ideal_of S == Inter {I. is_ideal I & S <= I}"
- is_pideal_def "is_pideal I == (EX a. I = ideal_of {a})"
+ is_ideal_def: "is_ideal I == (ALL a: I. ALL b: I. a + b : I) &
+ (ALL a: I. - a : I) & 0 : I &
+ (ALL a: I. ALL r. a * r : I)"
+ ideal_of_def: "ideal_of S == Inter {I. is_ideal I & S <= I}"
+ is_pideal_def: "is_pideal I == (EX a. I = ideal_of {a})"
-(* Principle ideal domains *)
+text {* Principle ideal domains *}
-axclass
- pid < domain
+axclass pid < "domain"
+ pid_ax: "is_ideal I ==> is_pideal I"
- pid_ax "is_ideal I ==> is_pideal I"
-
-end
\ No newline at end of file
+end
--- a/src/HOL/Algebra/abstract/PID.thy Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/PID.thy Sat Sep 17 20:49:14 2005 +0200
@@ -4,10 +4,12 @@
Author: Clemens Ballarin, started 5 October 1999
*)
-PID = Ideal +
+theory PID imports Ideal begin
-instance
- pid < factorial (TrueI, pid_irred_imp_prime)
+instance pid < factorial
+ apply intro_classes
+ apply (rule TrueI)
+ apply (erule pid_irred_imp_prime)
+ done
end
-
--- a/src/HOL/Algebra/abstract/RingHomo.ML Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/RingHomo.ML Sat Sep 17 20:49:14 2005 +0200
@@ -6,21 +6,21 @@
(* Ring homomorphism *)
-Goalw [homo_def]
+Goalw [thm "homo_def"]
"!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \
\ f 1 = 1 |] ==> homo f";
by Auto_tac;
qed "homoI";
-Goalw [homo_def] "!! f. homo f ==> f (a + b) = f a + f b";
+Goalw [thm "homo_def"] "!! f. homo f ==> f (a + b) = f a + f b";
by (Fast_tac 1);
qed "homo_add";
-Goalw [homo_def] "!! f. homo f ==> f (a * b) = f a * f b";
+Goalw [thm "homo_def"] "!! f. homo f ==> f (a * b) = f a * f b";
by (Fast_tac 1);
qed "homo_mult";
-Goalw [homo_def] "!! f. homo f ==> f 1 = 1";
+Goalw [thm "homo_def"] "!! f. homo f ==> f 1 = 1";
by (Fast_tac 1);
qed "homo_one";
--- a/src/HOL/Algebra/abstract/RingHomo.thy Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/abstract/RingHomo.thy Sat Sep 17 20:49:14 2005 +0200
@@ -4,14 +4,12 @@
Author: Clemens Ballarin, started 15 April 1997
*)
-RingHomo = Ring +
-
-consts
- homo :: ('a::ring => 'b::ring) => bool
+theory RingHomo imports Ring begin
-defs
- homo_def "homo f == (ALL a b. f (a + b) = f a + f b &
- f (a * b) = f a * f b) &
- f 1 = 1"
+constdefs
+ homo :: "('a::ring => 'b::ring) => bool"
+ "homo f == (ALL a b. f (a + b) = f a + f b &
+ f (a * b) = f a * f b) &
+ f 1 = 1"
end
--- a/src/HOL/Algebra/poly/PolyHomo.ML Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.ML Sat Sep 17 20:49:14 2005 +0200
@@ -111,7 +111,7 @@
Goal
"!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)";
by (rtac homoI 1);
-by (rewtac EVAL2_def);
+by (rewtac (thm "EVAL2_def"));
(* + commutes *)
(* degree estimations:
bound of all sums can be extended to max (deg aa) (deg b) *)
@@ -153,18 +153,18 @@
by (Asm_simp_tac 1);
qed "EVAL2_homo";
-Goalw [EVAL2_def]
+Goalw [thm "EVAL2_def"]
"!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b";
by (Simp_tac 1);
qed "EVAL2_const";
-Goalw [EVAL2_def]
+Goalw [thm "EVAL2_def"]
"!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a";
(* Must be able to distinguish 0 from 1, hence 'a::domain *)
by (Asm_simp_tac 1);
qed "EVAL2_monom1";
-Goalw [EVAL2_def]
+Goalw [thm "EVAL2_def"]
"!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n";
by (Simp_tac 1);
by (case_tac "n" 1);
@@ -194,23 +194,23 @@
addsimps [EVAL2_homo, EVAL2_const, EVAL2_monom]) 1);
qed "EVAL2_monom_n";
-Goalw [EVAL_def] "!! a::'a::ring. homo (EVAL a)";
+Goalw [thm "EVAL_def"] "!! a::'a::ring. homo (EVAL a)";
by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1);
qed "EVAL_homo";
-Goalw [EVAL_def] "!! a::'a::ring. EVAL a (monom b 0) = b";
+Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (monom b 0) = b";
by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1);
qed "EVAL_const";
-Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n";
+Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n";
by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1);
qed "EVAL_monom";
-Goalw [EVAL_def] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p";
+Goalw [thm "EVAL_def"] "!! a::'a::ring. EVAL a (b *s p) = b * EVAL a p";
by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1);
qed "EVAL_smult";
-Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n";
+Goalw [thm "EVAL_def"] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n";
by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1);
qed "EVAL_monom_n";
--- a/src/HOL/Algebra/poly/PolyHomo.thy Sat Sep 17 20:16:35 2005 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.thy Sat Sep 17 20:49:14 2005 +0200
@@ -4,15 +4,15 @@
Author: Clemens Ballarin, started 15 April 1997
*)
-PolyHomo = UnivPoly2 +
+theory PolyHomo imports UnivPoly2 begin
consts
EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
EVAL :: "['a::ring, 'a up] => 'a"
defs
- EVAL2_def "EVAL2 phi a p ==
+ EVAL2_def: "EVAL2 phi a p ==
setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
- EVAL_def "EVAL == EVAL2 (%x. x)"
+ EVAL_def: "EVAL == EVAL2 (%x. x)"
end