# HG changeset patch
# User wenzelm
# Date 1126982954 -7200
# Node ID 68a7acb5f22ebb1d3accb4f9a2d9f6a252a2daa9
# Parent  1865064ca82a74fb97ab960ce327c1172736af53
converted to Isar theory format;

diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/abstract/Factor.ML
--- 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";
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/abstract/Factor.thy
--- 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
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/abstract/Field.thy
--- 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
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/abstract/Ideal.ML
--- 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);
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/abstract/Ideal.thy
--- 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
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/abstract/PID.thy
--- 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
-
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/abstract/RingHomo.ML
--- 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";
 
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/abstract/RingHomo.thy
--- 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
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/poly/PolyHomo.ML
--- 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";
 
diff -r 1865064ca82a -r 68a7acb5f22e src/HOL/Algebra/poly/PolyHomo.thy
--- 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