src/HOL/Groebner_Basis.thy
changeset 34974 18b41bba42b5
parent 33361 1f18de40b43f
child 35050 9f841f20dca6
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -527,13 +527,13 @@
     1.4      val (l,r) = Thm.dest_binop ct
     1.5      val T = ctyp_of_term l
     1.6    in (case (term_of l, term_of r) of
     1.7 -      (Const(@{const_name "HOL.divide"},_)$_$_, _) =>
     1.8 +      (Const(@{const_name Algebras.divide},_)$_$_, _) =>
     1.9          let val (x,y) = Thm.dest_binop l val z = r
    1.10              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    1.11              val ynz = prove_nz ss T y
    1.12          in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
    1.13          end
    1.14 -     | (_, Const (@{const_name "HOL.divide"},_)$_$_) =>
    1.15 +     | (_, Const (@{const_name Algebras.divide},_)$_$_) =>
    1.16          let val (x,y) = Thm.dest_binop r val z = l
    1.17              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    1.18              val ynz = prove_nz ss T y
    1.19 @@ -543,49 +543,49 @@
    1.20    end
    1.21    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    1.22  
    1.23 - fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b
    1.24 + fun is_number (Const(@{const_name Algebras.divide},_)$a$b) = is_number a andalso is_number b
    1.25     | is_number t = can HOLogic.dest_number t
    1.26  
    1.27   val is_number = is_number o term_of
    1.28  
    1.29   fun proc3 phi ss ct =
    1.30    (case term_of ct of
    1.31 -    Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
    1.32 +    Const(@{const_name Algebras.less},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    1.33        let
    1.34          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.35          val _ = map is_number [a,b,c]
    1.36          val T = ctyp_of_term c
    1.37          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    1.38        in SOME (mk_meta_eq th) end
    1.39 -  | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
    1.40 +  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    1.41        let
    1.42          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.43          val _ = map is_number [a,b,c]
    1.44          val T = ctyp_of_term c
    1.45          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
    1.46        in SOME (mk_meta_eq th) end
    1.47 -  | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
    1.48 +  | Const("op =",_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    1.49        let
    1.50          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.51          val _ = map is_number [a,b,c]
    1.52          val T = ctyp_of_term c
    1.53          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
    1.54        in SOME (mk_meta_eq th) end
    1.55 -  | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    1.56 +  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    1.57      let
    1.58        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.59          val _ = map is_number [a,b,c]
    1.60          val T = ctyp_of_term c
    1.61          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
    1.62        in SOME (mk_meta_eq th) end
    1.63 -  | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    1.64 +  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    1.65      let
    1.66        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.67          val _ = map is_number [a,b,c]
    1.68          val T = ctyp_of_term c
    1.69          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
    1.70        in SOME (mk_meta_eq th) end
    1.71 -  | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    1.72 +  | Const("op =",_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    1.73      let
    1.74        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.75          val _ = map is_number [a,b,c]
    1.76 @@ -645,15 +645,15 @@
    1.77  
    1.78  fun numeral_is_const ct =
    1.79    case term_of ct of
    1.80 -   Const (@{const_name "HOL.divide"},_) $ a $ b =>
    1.81 +   Const (@{const_name Algebras.divide},_) $ a $ b =>
    1.82       can HOLogic.dest_number a andalso can HOLogic.dest_number b
    1.83 - | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t
    1.84 + | Const (@{const_name Algebras.inverse},_)$t => can HOLogic.dest_number t
    1.85   | t => can HOLogic.dest_number t
    1.86  
    1.87  fun dest_const ct = ((case term_of ct of
    1.88 -   Const (@{const_name "HOL.divide"},_) $ a $ b=>
    1.89 +   Const (@{const_name Algebras.divide},_) $ a $ b=>
    1.90      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    1.91 - | Const (@{const_name "HOL.inverse"},_)$t => 
    1.92 + | Const (@{const_name Algebras.inverse},_)$t => 
    1.93                 Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
    1.94   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
    1.95     handle TERM _ => error "ring_dest_const")