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.5  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
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.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")
```