src/HOL/Groebner_Basis.thy
changeset 26314 9c39fc898fff
parent 26199 04817a8802f2
child 26462 dac4e2bce00d
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Mar 17 22:34:27 2008 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 18 20:33:28 2008 +0100
     1.3 @@ -159,10 +159,10 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -lemma "axioms" [normalizer
     1.8 +lemmas gb_semiring_axioms =
     1.9 +  gb_semiring_axioms [normalizer
    1.10      semiring ops: semiring_ops
    1.11 -    semiring rules: semiring_rules]:
    1.12 -  "gb_semiring add mul pwr r0 r1" by (rule gb_semiring_axioms)
    1.13 +    semiring rules: semiring_rules]
    1.14  
    1.15  end
    1.16  
    1.17 @@ -216,7 +216,7 @@
    1.18  end
    1.19  *}
    1.20  
    1.21 -declaration {* normalizer_funs @{thm class_semiring.axioms} *}
    1.22 +declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms} *}
    1.23  
    1.24  
    1.25  locale gb_ring = gb_semiring +
    1.26 @@ -232,12 +232,12 @@
    1.27  
    1.28  lemmas ring_rules = neg_mul sub_add
    1.29  
    1.30 -lemma "axioms" [normalizer
    1.31 -  semiring ops: semiring_ops
    1.32 -  semiring rules: semiring_rules
    1.33 -  ring ops: ring_ops
    1.34 -  ring rules: ring_rules]:
    1.35 -  "gb_ring add mul pwr r0 r1 sub neg" by (rule gb_ring_axioms)
    1.36 +lemmas gb_ring_axioms =
    1.37 +  gb_ring_axioms [normalizer
    1.38 +    semiring ops: semiring_ops
    1.39 +    semiring rules: semiring_rules
    1.40 +    ring ops: ring_ops
    1.41 +    ring rules: ring_rules]
    1.42  
    1.43  end
    1.44  
    1.45 @@ -247,7 +247,7 @@
    1.46    by unfold_locales simp_all
    1.47  
    1.48  
    1.49 -declaration {* normalizer_funs @{thm class_ring.axioms} *}
    1.50 +declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms} *}
    1.51  
    1.52  use "Tools/Groebner_Basis/normalizer.ML"
    1.53  
    1.54 @@ -263,12 +263,12 @@
    1.55       and inverse: "inverse x = divide r1 x"
    1.56  begin
    1.57  
    1.58 -lemma "axioms" [normalizer
    1.59 -  semiring ops: semiring_ops
    1.60 -  semiring rules: semiring_rules
    1.61 -  ring ops: ring_ops
    1.62 -  ring rules: ring_rules]:
    1.63 -  "gb_field add mul pwr r0 r1 sub neg divide inverse" by (rule gb_field_axioms)
    1.64 +lemmas gb_field_axioms =
    1.65 +  gb_field_axioms [normalizer
    1.66 +    semiring ops: semiring_ops
    1.67 +    semiring rules: semiring_rules
    1.68 +    ring ops: ring_ops
    1.69 +    ring rules: ring_rules]
    1.70  
    1.71  end
    1.72  
    1.73 @@ -307,13 +307,12 @@
    1.74    thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
    1.75  qed
    1.76  
    1.77 -declare "axioms" [normalizer del]
    1.78 +declare gb_semiring_axioms [normalizer del]
    1.79  
    1.80 -lemma "axioms" [normalizer
    1.81 +lemmas semiringb_axioms = semiringb_axioms [normalizer
    1.82    semiring ops: semiring_ops
    1.83    semiring rules: semiring_rules
    1.84 -  idom rules: noteq_reduce add_scale_eq_noteq]:
    1.85 -  "semiringb add mul pwr r0 r1" by (rule semiringb_axioms)
    1.86 +  idom rules: noteq_reduce add_scale_eq_noteq]
    1.87  
    1.88  end
    1.89  
    1.90 @@ -321,16 +320,15 @@
    1.91    assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
    1.92  begin
    1.93  
    1.94 -declare "axioms" [normalizer del]
    1.95 +declare gb_ring_axioms [normalizer del]
    1.96  
    1.97 -lemma "axioms" [normalizer
    1.98 +lemmas ringb_axioms = ringb_axioms [normalizer
    1.99    semiring ops: semiring_ops
   1.100    semiring rules: semiring_rules
   1.101    ring ops: ring_ops
   1.102    ring rules: ring_rules
   1.103    idom rules: noteq_reduce add_scale_eq_noteq
   1.104 -  ideal rules: subr0_iff add_r0_iff]:
   1.105 -  "ringb add mul pwr r0 r1 sub neg" by (rule ringb_axioms)
   1.106 +  ideal rules: subr0_iff add_r0_iff]
   1.107  
   1.108  end
   1.109  
   1.110 @@ -358,7 +356,7 @@
   1.111    thus "w = x"  by simp
   1.112  qed
   1.113  
   1.114 -declaration {* normalizer_funs @{thm class_ringb.axioms} *}
   1.115 +declaration {* normalizer_funs @{thm class_ringb.ringb_axioms} *}
   1.116  
   1.117  interpretation natgb: semiringb
   1.118    ["op +" "op *" "op ^" "0::nat" "1"]
   1.119 @@ -382,21 +380,21 @@
   1.120    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
   1.121  qed
   1.122  
   1.123 -declaration {* normalizer_funs @{thm natgb.axioms} *}
   1.124 +declaration {* normalizer_funs @{thm natgb.semiringb_axioms} *}
   1.125  
   1.126  locale fieldgb = ringb + gb_field
   1.127  begin
   1.128  
   1.129 -declare "axioms" [normalizer del]
   1.130 +declare gb_field_axioms [normalizer del]
   1.131  
   1.132 -lemma "axioms" [normalizer
   1.133 +lemmas fieldgb_axioms = fieldgb_axioms [normalizer
   1.134    semiring ops: semiring_ops
   1.135    semiring rules: semiring_rules
   1.136    ring ops: ring_ops
   1.137    ring rules: ring_rules
   1.138    idom rules: noteq_reduce add_scale_eq_noteq
   1.139 -  ideal rules: subr0_iff add_r0_iff]:
   1.140 -  "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
   1.141 +  ideal rules: subr0_iff add_r0_iff]
   1.142 +
   1.143  end
   1.144  
   1.145