src/HOL/Groebner_Basis.thy
changeset 30866 dd5117e2d73e
parent 30729 461ee3e49ad3
child 30869 71fde5b7b43c
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Apr 03 18:03:29 2009 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Apr 05 05:07:10 2009 +0100
     1.3 @@ -191,8 +191,7 @@
     1.4  
     1.5  open Conv;
     1.6  
     1.7 -fun numeral_is_const ct =
     1.8 -  can HOLogic.dest_number (Thm.term_of ct);
     1.9 +fun numeral_is_const ct = can HOLogic.dest_number (Thm.term_of ct);
    1.10  
    1.11  fun int_of_rat x =
    1.12    (case Rat.quotient_of_rat x of (i, 1) => i
    1.13 @@ -260,16 +259,22 @@
    1.14  locale gb_field = gb_ring +
    1.15    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.16      and inverse:: "'a \<Rightarrow> 'a"
    1.17 -  assumes divide: "divide x y = mul x (inverse y)"
    1.18 -     and inverse: "inverse x = divide r1 x"
    1.19 +  assumes divide_inverse: "divide x y = mul x (inverse y)"
    1.20 +     and inverse_divide: "inverse x = divide r1 x"
    1.21  begin
    1.22  
    1.23 +lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
    1.24 +
    1.25 +lemmas field_rules = divide_inverse inverse_divide
    1.26 +
    1.27  lemmas gb_field_axioms' =
    1.28    gb_field_axioms [normalizer
    1.29      semiring ops: semiring_ops
    1.30      semiring rules: semiring_rules
    1.31      ring ops: ring_ops
    1.32 -    ring rules: ring_rules]
    1.33 +    ring rules: ring_rules
    1.34 +    field ops: field_ops
    1.35 +    field rules: field_rules]
    1.36  
    1.37  end
    1.38  
    1.39 @@ -393,6 +398,8 @@
    1.40    semiring rules: semiring_rules
    1.41    ring ops: ring_ops
    1.42    ring rules: ring_rules
    1.43 +  field ops: field_ops
    1.44 +  field rules: field_rules
    1.45    idom rules: noteq_reduce add_scale_eq_noteq
    1.46    ideal rules: subr0_iff add_r0_iff]
    1.47  
    1.48 @@ -636,8 +643,8 @@
    1.49  fun numeral_is_const ct =
    1.50    case term_of ct of
    1.51     Const (@{const_name "HOL.divide"},_) $ a $ b =>
    1.52 -     numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct)
    1.53 - | Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct)
    1.54 +     can HOLogic.dest_number a andalso can HOLogic.dest_number b
    1.55 + | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t
    1.56   | t => can HOLogic.dest_number t
    1.57  
    1.58  fun dest_const ct = ((case term_of ct of