src/HOL/Groebner_Basis.thy
changeset 35084 e25eedfc15ce
parent 35050 9f841f20dca6
child 35092 cfe605c54e50
     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Feb 10 08:49:26 2010 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Feb 10 08:49:26 2010 +0100
     1.3 @@ -489,7 +489,13 @@
     1.4    by (simp add: add_divide_distrib)
     1.5  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
     1.6    by (simp add: add_divide_distrib)
     1.7 -ML{* let open Conv in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))   (@{thm divide_inverse} RS sym)end*}
     1.8 +
     1.9 +ML {*
    1.10 +let open Conv
    1.11 +in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym)
    1.12 +end
    1.13 +*}
    1.14 +
    1.15  ML{* 
    1.16  local
    1.17   val zr = @{cpat "0"}
    1.18 @@ -527,13 +533,13 @@
    1.19      val (l,r) = Thm.dest_binop ct
    1.20      val T = ctyp_of_term l
    1.21    in (case (term_of l, term_of r) of
    1.22 -      (Const(@{const_name Algebras.divide},_)$_$_, _) =>
    1.23 +      (Const(@{const_name Rings.divide},_)$_$_, _) =>
    1.24          let val (x,y) = Thm.dest_binop l val z = r
    1.25              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    1.26              val ynz = prove_nz ss T y
    1.27          in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
    1.28          end
    1.29 -     | (_, Const (@{const_name Algebras.divide},_)$_$_) =>
    1.30 +     | (_, Const (@{const_name Rings.divide},_)$_$_) =>
    1.31          let val (x,y) = Thm.dest_binop r val z = l
    1.32              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    1.33              val ynz = prove_nz ss T y
    1.34 @@ -543,49 +549,49 @@
    1.35    end
    1.36    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    1.37  
    1.38 - fun is_number (Const(@{const_name Algebras.divide},_)$a$b) = is_number a andalso is_number b
    1.39 + fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
    1.40     | is_number t = can HOLogic.dest_number t
    1.41  
    1.42   val is_number = is_number o term_of
    1.43  
    1.44   fun proc3 phi ss ct =
    1.45    (case term_of ct of
    1.46 -    Const(@{const_name Algebras.less},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    1.47 +    Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    1.48        let
    1.49          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.50          val _ = map is_number [a,b,c]
    1.51          val T = ctyp_of_term c
    1.52          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    1.53        in SOME (mk_meta_eq th) end
    1.54 -  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    1.55 +  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    1.56        let
    1.57          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.58          val _ = map is_number [a,b,c]
    1.59          val T = ctyp_of_term c
    1.60          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
    1.61        in SOME (mk_meta_eq th) end
    1.62 -  | Const("op =",_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    1.63 +  | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    1.64        let
    1.65          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.66          val _ = map is_number [a,b,c]
    1.67          val T = ctyp_of_term c
    1.68          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
    1.69        in SOME (mk_meta_eq th) end
    1.70 -  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    1.71 +  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.72      let
    1.73        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.74          val _ = map is_number [a,b,c]
    1.75          val T = ctyp_of_term c
    1.76          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
    1.77        in SOME (mk_meta_eq th) end
    1.78 -  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    1.79 +  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.80      let
    1.81        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.82          val _ = map is_number [a,b,c]
    1.83          val T = ctyp_of_term c
    1.84          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
    1.85        in SOME (mk_meta_eq th) end
    1.86 -  | Const("op =",_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    1.87 +  | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.88      let
    1.89        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.90          val _ = map is_number [a,b,c]
    1.91 @@ -628,9 +634,9 @@
    1.92             @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
    1.93             @{thm "diff_def"}, @{thm "minus_divide_left"},
    1.94             @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
    1.95 -           @{thm divide_inverse} RS sym, @{thm inverse_divide}, 
    1.96 +           @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
    1.97             fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))   
    1.98 -           (@{thm divide_inverse} RS sym)]
    1.99 +           (@{thm field_divide_inverse} RS sym)]
   1.100  
   1.101  val comp_conv = (Simplifier.rewrite
   1.102  (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
   1.103 @@ -645,15 +651,15 @@
   1.104  
   1.105  fun numeral_is_const ct =
   1.106    case term_of ct of
   1.107 -   Const (@{const_name Algebras.divide},_) $ a $ b =>
   1.108 +   Const (@{const_name Rings.divide},_) $ a $ b =>
   1.109       can HOLogic.dest_number a andalso can HOLogic.dest_number b
   1.110 - | Const (@{const_name Algebras.inverse},_)$t => can HOLogic.dest_number t
   1.111 + | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
   1.112   | t => can HOLogic.dest_number t
   1.113  
   1.114  fun dest_const ct = ((case term_of ct of
   1.115 -   Const (@{const_name Algebras.divide},_) $ a $ b=>
   1.116 +   Const (@{const_name Rings.divide},_) $ a $ b=>
   1.117      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
   1.118 - | Const (@{const_name Algebras.inverse},_)$t => 
   1.119 + | Const (@{const_name Rings.inverse},_)$t => 
   1.120                 Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
   1.121   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
   1.122     handle TERM _ => error "ring_dest_const")