avoid rebinding of existing facts;
authorwenzelm
Tue Mar 18 20:33:28 2008 +0100 (2008-03-18)
changeset 263149c39fc898fff
parent 26313 8590bf5ef343
child 26315 cb3badaa192e
avoid rebinding of existing facts;
src/HOL/Arith_Tools.thy
src/HOL/Groebner_Basis.thy
     1.1 --- a/src/HOL/Arith_Tools.thy	Mon Mar 17 22:34:27 2008 +0100
     1.2 +++ b/src/HOL/Arith_Tools.thy	Tue Mar 18 20:33:28 2008 +0100
     1.3 @@ -327,24 +327,12 @@
     1.4  
     1.5  text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
     1.6  
     1.7 -lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard]
     1.8 -declare le_divide_eq_number_of [simp]
     1.9 -
    1.10 -lemmas divide_le_eq_number_of = divide_le_eq [of _ "number_of w", standard]
    1.11 -declare divide_le_eq_number_of [simp]
    1.12 -
    1.13 -lemmas less_divide_eq_number_of = less_divide_eq [of _ _ "number_of w", standard]
    1.14 -declare less_divide_eq_number_of [simp]
    1.15 -
    1.16 -lemmas divide_less_eq_number_of = divide_less_eq [of _ "number_of w", standard]
    1.17 -declare divide_less_eq_number_of [simp]
    1.18 -
    1.19 -lemmas eq_divide_eq_number_of = eq_divide_eq [of _ _ "number_of w", standard]
    1.20 -declare eq_divide_eq_number_of [simp]
    1.21 -
    1.22 -lemmas divide_eq_eq_number_of = divide_eq_eq [of _ "number_of w", standard]
    1.23 -declare divide_eq_eq_number_of [simp]
    1.24 -
    1.25 +lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
    1.26 +lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
    1.27 +lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
    1.28 +lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
    1.29 +lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
    1.30 +lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
    1.31  
    1.32  
    1.33  subsubsection{*Optional Simplification Rules Involving Constants*}
    1.34 @@ -600,7 +588,7 @@
    1.35  in
    1.36   val field_comp_conv = comp_conv;
    1.37   val fieldgb_declaration = 
    1.38 -  NormalizerData.funs @{thm class_fieldgb.axioms}
    1.39 +  NormalizerData.funs @{thm class_fieldgb.fieldgb_axioms}
    1.40     {is_const = K numeral_is_const,
    1.41      dest_const = K dest_const,
    1.42      mk_const = mk_const,
     2.1 --- a/src/HOL/Groebner_Basis.thy	Mon Mar 17 22:34:27 2008 +0100
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 18 20:33:28 2008 +0100
     2.3 @@ -159,10 +159,10 @@
     2.4  qed
     2.5  
     2.6  
     2.7 -lemma "axioms" [normalizer
     2.8 +lemmas gb_semiring_axioms =
     2.9 +  gb_semiring_axioms [normalizer
    2.10      semiring ops: semiring_ops
    2.11 -    semiring rules: semiring_rules]:
    2.12 -  "gb_semiring add mul pwr r0 r1" by (rule gb_semiring_axioms)
    2.13 +    semiring rules: semiring_rules]
    2.14  
    2.15  end
    2.16  
    2.17 @@ -216,7 +216,7 @@
    2.18  end
    2.19  *}
    2.20  
    2.21 -declaration {* normalizer_funs @{thm class_semiring.axioms} *}
    2.22 +declaration {* normalizer_funs @{thm class_semiring.gb_semiring_axioms} *}
    2.23  
    2.24  
    2.25  locale gb_ring = gb_semiring +
    2.26 @@ -232,12 +232,12 @@
    2.27  
    2.28  lemmas ring_rules = neg_mul sub_add
    2.29  
    2.30 -lemma "axioms" [normalizer
    2.31 -  semiring ops: semiring_ops
    2.32 -  semiring rules: semiring_rules
    2.33 -  ring ops: ring_ops
    2.34 -  ring rules: ring_rules]:
    2.35 -  "gb_ring add mul pwr r0 r1 sub neg" by (rule gb_ring_axioms)
    2.36 +lemmas gb_ring_axioms =
    2.37 +  gb_ring_axioms [normalizer
    2.38 +    semiring ops: semiring_ops
    2.39 +    semiring rules: semiring_rules
    2.40 +    ring ops: ring_ops
    2.41 +    ring rules: ring_rules]
    2.42  
    2.43  end
    2.44  
    2.45 @@ -247,7 +247,7 @@
    2.46    by unfold_locales simp_all
    2.47  
    2.48  
    2.49 -declaration {* normalizer_funs @{thm class_ring.axioms} *}
    2.50 +declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms} *}
    2.51  
    2.52  use "Tools/Groebner_Basis/normalizer.ML"
    2.53  
    2.54 @@ -263,12 +263,12 @@
    2.55       and inverse: "inverse x = divide r1 x"
    2.56  begin
    2.57  
    2.58 -lemma "axioms" [normalizer
    2.59 -  semiring ops: semiring_ops
    2.60 -  semiring rules: semiring_rules
    2.61 -  ring ops: ring_ops
    2.62 -  ring rules: ring_rules]:
    2.63 -  "gb_field add mul pwr r0 r1 sub neg divide inverse" by (rule gb_field_axioms)
    2.64 +lemmas gb_field_axioms =
    2.65 +  gb_field_axioms [normalizer
    2.66 +    semiring ops: semiring_ops
    2.67 +    semiring rules: semiring_rules
    2.68 +    ring ops: ring_ops
    2.69 +    ring rules: ring_rules]
    2.70  
    2.71  end
    2.72  
    2.73 @@ -307,13 +307,12 @@
    2.74    thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
    2.75  qed
    2.76  
    2.77 -declare "axioms" [normalizer del]
    2.78 +declare gb_semiring_axioms [normalizer del]
    2.79  
    2.80 -lemma "axioms" [normalizer
    2.81 +lemmas semiringb_axioms = semiringb_axioms [normalizer
    2.82    semiring ops: semiring_ops
    2.83    semiring rules: semiring_rules
    2.84 -  idom rules: noteq_reduce add_scale_eq_noteq]:
    2.85 -  "semiringb add mul pwr r0 r1" by (rule semiringb_axioms)
    2.86 +  idom rules: noteq_reduce add_scale_eq_noteq]
    2.87  
    2.88  end
    2.89  
    2.90 @@ -321,16 +320,15 @@
    2.91    assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
    2.92  begin
    2.93  
    2.94 -declare "axioms" [normalizer del]
    2.95 +declare gb_ring_axioms [normalizer del]
    2.96  
    2.97 -lemma "axioms" [normalizer
    2.98 +lemmas ringb_axioms = ringb_axioms [normalizer
    2.99    semiring ops: semiring_ops
   2.100    semiring rules: semiring_rules
   2.101    ring ops: ring_ops
   2.102    ring rules: ring_rules
   2.103    idom rules: noteq_reduce add_scale_eq_noteq
   2.104 -  ideal rules: subr0_iff add_r0_iff]:
   2.105 -  "ringb add mul pwr r0 r1 sub neg" by (rule ringb_axioms)
   2.106 +  ideal rules: subr0_iff add_r0_iff]
   2.107  
   2.108  end
   2.109  
   2.110 @@ -358,7 +356,7 @@
   2.111    thus "w = x"  by simp
   2.112  qed
   2.113  
   2.114 -declaration {* normalizer_funs @{thm class_ringb.axioms} *}
   2.115 +declaration {* normalizer_funs @{thm class_ringb.ringb_axioms} *}
   2.116  
   2.117  interpretation natgb: semiringb
   2.118    ["op +" "op *" "op ^" "0::nat" "1"]
   2.119 @@ -382,21 +380,21 @@
   2.120    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
   2.121  qed
   2.122  
   2.123 -declaration {* normalizer_funs @{thm natgb.axioms} *}
   2.124 +declaration {* normalizer_funs @{thm natgb.semiringb_axioms} *}
   2.125  
   2.126  locale fieldgb = ringb + gb_field
   2.127  begin
   2.128  
   2.129 -declare "axioms" [normalizer del]
   2.130 +declare gb_field_axioms [normalizer del]
   2.131  
   2.132 -lemma "axioms" [normalizer
   2.133 +lemmas fieldgb_axioms = fieldgb_axioms [normalizer
   2.134    semiring ops: semiring_ops
   2.135    semiring rules: semiring_rules
   2.136    ring ops: ring_ops
   2.137    ring rules: ring_rules
   2.138    idom rules: noteq_reduce add_scale_eq_noteq
   2.139 -  ideal rules: subr0_iff add_r0_iff]:
   2.140 -  "fieldgb add mul pwr r0 r1 sub neg divide inverse" by unfold_locales
   2.141 +  ideal rules: subr0_iff add_r0_iff]
   2.142 +
   2.143  end
   2.144  
   2.145