author haftmann Wed Feb 10 08:49:26 2010 +0100 (2010-02-10) changeset 35084 e25eedfc15ce parent 35083 3246e66b0874 child 35085 22bdb7f86a1e
moved constants inverse and divide to Ring.thy
 NEWS file | annotate | diff | revisions src/HOL/Algebras.thy file | annotate | diff | revisions src/HOL/Decision_Procs/Dense_Linear_Order.thy file | annotate | diff | revisions src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy file | annotate | diff | revisions src/HOL/Fields.thy file | annotate | diff | revisions src/HOL/Groebner_Basis.thy file | annotate | diff | revisions src/HOL/Import/HOL/realax.imp file | annotate | diff | revisions src/HOL/Tools/Nitpick/nitpick_model.ML file | annotate | diff | revisions src/HOL/Tools/lin_arith.ML file | annotate | diff | revisions src/HOL/Tools/numeral_simprocs.ML file | annotate | diff | revisions src/HOL/ex/SVC_Oracle.thy file | annotate | diff | revisions src/HOL/ex/svc_funcs.ML file | annotate | diff | revisions
```     1.1 --- a/NEWS	Wed Feb 10 08:49:26 2010 +0100
1.2 +++ b/NEWS	Wed Feb 10 08:49:26 2010 +0100
1.3 @@ -20,6 +20,15 @@
1.4  consistent names suitable for name prefixes within the HOL theories.
1.5  INCOMPATIBILITY.
1.6
1.7 +* Some generic constants have been put to appropriate theories:
1.8 +
1.9 +    inverse, divide: Rings
1.10 +
1.11 +INCOMPATIBILITY.
1.12 +
1.13 +* Class division ring also requires proof of fact divide_inverse.  However instantiation
1.14 +of parameter divide has also been required previously.  INCOMPATIBILITY.
1.15 +
1.16  * More consistent naming of type classes involving orderings (and lattices):
1.17
1.18      lower_semilattice                   ~> semilattice_inf
1.19 @@ -76,7 +85,7 @@
1.20
1.21  * New theory Algebras contains generic algebraic structures and
1.22  generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
1.23 -plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and
1.24 +plus, minus, uminus, times, abs, sgn, less_eq and
1.25  less have been moved from HOL.thy to Algebras.thy.
1.26
1.27  * HOLogic.strip_psplit: types are returned in syntactic order, similar
```
```     2.1 --- a/src/HOL/Algebras.thy	Wed Feb 10 08:49:26 2010 +0100
2.2 +++ b/src/HOL/Algebras.thy	Wed Feb 10 08:49:26 2010 +0100
2.3 @@ -103,10 +103,6 @@
2.4  class times =
2.5    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
2.6
2.7 -class inverse =
2.8 -  fixes inverse :: "'a \<Rightarrow> 'a"
2.9 -    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
2.10 -
2.11  class abs =
2.12    fixes abs :: "'a \<Rightarrow> 'a"
2.13  begin
```
```     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 08:49:26 2010 +0100
3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 08:49:26 2010 +0100
3.3 @@ -655,7 +655,7 @@
3.4      if h aconvc y then false else if h aconvc x then true else earlier t x y;
3.5
3.6  fun dest_frac ct = case term_of ct of
3.7 -   Const (@{const_name Algebras.divide},_) \$ a \$ b=>
3.8 +   Const (@{const_name Rings.divide},_) \$ a \$ b=>
3.9      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
3.10   | Const(@{const_name inverse}, _)\$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
3.11   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
```
```     4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 08:49:26 2010 +0100
4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 08:49:26 2010 +0100
4.3 @@ -2946,7 +2946,7 @@
4.4  fun num rT x = HOLogic.mk_number rT x;
4.5  fun rrelT rT = [rT,rT] ---> rT;
4.6  fun rrT rT = [rT, rT] ---> bT;
4.7 -fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
4.8 +fun divt rT = Const(@{const_name Rings.divide},rrelT rT);
4.9  fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
4.10  fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
4.11  fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
4.12 @@ -2974,7 +2974,7 @@
4.13   | Const(@{const_name Algebras.minus},_)\$a\$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
4.14   | Const(@{const_name Algebras.times},_)\$a\$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
4.15   | Const(@{const_name Power.power},_)\$a\$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
4.16 - | Const(@{const_name Algebras.divide},_)\$a\$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
4.17 + | Const(@{const_name Rings.divide},_)\$a\$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
4.18   | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1)
4.19           handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the));
4.20
```
```     5.1 --- a/src/HOL/Fields.thy	Wed Feb 10 08:49:26 2010 +0100
5.2 +++ b/src/HOL/Fields.thy	Wed Feb 10 08:49:26 2010 +0100
5.3 @@ -14,8 +14,8 @@
5.4  begin
5.5
5.6  class field = comm_ring_1 + inverse +
5.7 -  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
5.8 -  assumes divide_inverse: "a / b = a * inverse b"
5.9 +  assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
5.10 +  assumes field_divide_inverse: "a / b = a * inverse b"
5.11  begin
5.12
5.13  subclass division_ring
5.14 @@ -24,6 +24,9 @@
5.15    assume "a \<noteq> 0"
5.16    thus "inverse a * a = 1" by (rule field_inverse)
5.17    thus "a * inverse a = 1" by (simp only: mult_commute)
5.18 +next
5.19 +  fix a b :: 'a
5.20 +  show "a / b = a * inverse b" by (rule field_divide_inverse)
5.21  qed
5.22
5.23  subclass idom ..
```
```     6.1 --- a/src/HOL/Groebner_Basis.thy	Wed Feb 10 08:49:26 2010 +0100
6.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Feb 10 08:49:26 2010 +0100
6.3 @@ -489,7 +489,13 @@
6.5  lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y"
6.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*}
6.8 +
6.9 +ML {*
6.10 +let open Conv
6.11 +in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym)
6.12 +end
6.13 +*}
6.14 +
6.15  ML{*
6.16  local
6.17   val zr = @{cpat "0"}
6.18 @@ -527,13 +533,13 @@
6.19      val (l,r) = Thm.dest_binop ct
6.20      val T = ctyp_of_term l
6.21    in (case (term_of l, term_of r) of
6.22 -      (Const(@{const_name Algebras.divide},_)\$_\$_, _) =>
6.23 +      (Const(@{const_name Rings.divide},_)\$_\$_, _) =>
6.24          let val (x,y) = Thm.dest_binop l val z = r
6.25              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
6.26              val ynz = prove_nz ss T y
6.27          in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
6.28          end
6.29 -     | (_, Const (@{const_name Algebras.divide},_)\$_\$_) =>
6.30 +     | (_, Const (@{const_name Rings.divide},_)\$_\$_) =>
6.31          let val (x,y) = Thm.dest_binop r val z = l
6.32              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
6.33              val ynz = prove_nz ss T y
6.34 @@ -543,49 +549,49 @@
6.35    end
6.36    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
6.37
6.38 - fun is_number (Const(@{const_name Algebras.divide},_)\$a\$b) = is_number a andalso is_number b
6.39 + fun is_number (Const(@{const_name Rings.divide},_)\$a\$b) = is_number a andalso is_number b
6.40     | is_number t = can HOLogic.dest_number t
6.41
6.42   val is_number = is_number o term_of
6.43
6.44   fun proc3 phi ss ct =
6.45    (case term_of ct of
6.46 -    Const(@{const_name Algebras.less},_)\$(Const(@{const_name Algebras.divide},_)\$_\$_)\$_ =>
6.47 +    Const(@{const_name Algebras.less},_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
6.48        let
6.49          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
6.50          val _ = map is_number [a,b,c]
6.51          val T = ctyp_of_term c
6.52          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
6.53        in SOME (mk_meta_eq th) end
6.54 -  | Const(@{const_name Algebras.less_eq},_)\$(Const(@{const_name Algebras.divide},_)\$_\$_)\$_ =>
6.55 +  | Const(@{const_name Algebras.less_eq},_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
6.56        let
6.57          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
6.58          val _ = map is_number [a,b,c]
6.59          val T = ctyp_of_term c
6.60          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
6.61        in SOME (mk_meta_eq th) end
6.62 -  | Const("op =",_)\$(Const(@{const_name Algebras.divide},_)\$_\$_)\$_ =>
6.63 +  | Const("op =",_)\$(Const(@{const_name Rings.divide},_)\$_\$_)\$_ =>
6.64        let
6.65          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
6.66          val _ = map is_number [a,b,c]
6.67          val T = ctyp_of_term c
6.68          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
6.69        in SOME (mk_meta_eq th) end
6.70 -  | Const(@{const_name Algebras.less},_)\$_\$(Const(@{const_name Algebras.divide},_)\$_\$_) =>
6.71 +  | Const(@{const_name Algebras.less},_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
6.72      let
6.73        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
6.74          val _ = map is_number [a,b,c]
6.75          val T = ctyp_of_term c
6.76          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
6.77        in SOME (mk_meta_eq th) end
6.78 -  | Const(@{const_name Algebras.less_eq},_)\$_\$(Const(@{const_name Algebras.divide},_)\$_\$_) =>
6.79 +  | Const(@{const_name Algebras.less_eq},_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
6.80      let
6.81        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
6.82          val _ = map is_number [a,b,c]
6.83          val T = ctyp_of_term c
6.84          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
6.85        in SOME (mk_meta_eq th) end
6.86 -  | Const("op =",_)\$_\$(Const(@{const_name Algebras.divide},_)\$_\$_) =>
6.87 +  | Const("op =",_)\$_\$(Const(@{const_name Rings.divide},_)\$_\$_) =>
6.88      let
6.89        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
6.90          val _ = map is_number [a,b,c]
6.91 @@ -628,9 +634,9 @@
6.92             @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
6.93             @{thm "diff_def"}, @{thm "minus_divide_left"},
6.94             @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
6.95 -           @{thm divide_inverse} RS sym, @{thm inverse_divide},
6.96 +           @{thm field_divide_inverse} RS sym, @{thm inverse_divide},
6.97             fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute}))))
6.98 -           (@{thm divide_inverse} RS sym)]
6.99 +           (@{thm field_divide_inverse} RS sym)]
6.100
6.101  val comp_conv = (Simplifier.rewrite
6.103 @@ -645,15 +651,15 @@
6.104
6.105  fun numeral_is_const ct =
6.106    case term_of ct of
6.107 -   Const (@{const_name Algebras.divide},_) \$ a \$ b =>
6.108 +   Const (@{const_name Rings.divide},_) \$ a \$ b =>
6.109       can HOLogic.dest_number a andalso can HOLogic.dest_number b
6.110 - | Const (@{const_name Algebras.inverse},_)\$t => can HOLogic.dest_number t
6.111 + | Const (@{const_name Rings.inverse},_)\$t => can HOLogic.dest_number t
6.112   | t => can HOLogic.dest_number t
6.113
6.114  fun dest_const ct = ((case term_of ct of
6.115 -   Const (@{const_name Algebras.divide},_) \$ a \$ b=>
6.116 +   Const (@{const_name Rings.divide},_) \$ a \$ b=>
6.117      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
6.118 - | Const (@{const_name Algebras.inverse},_)\$t =>
6.119 + | Const (@{const_name Rings.inverse},_)\$t =>
6.120                 Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
6.121   | t => Rat.rat_of_int (snd (HOLogic.dest_number t)))
6.122     handle TERM _ => error "ring_dest_const")
```
```     7.1 --- a/src/HOL/Import/HOL/realax.imp	Wed Feb 10 08:49:26 2010 +0100
7.2 +++ b/src/HOL/Import/HOL/realax.imp	Wed Feb 10 08:49:26 2010 +0100
7.3 @@ -33,7 +33,7 @@
7.4    "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
7.5    "real_1" > "Algebras.one_class.one" :: "real"
7.6    "real_0" > "Algebras.zero_class.zero" :: "real"
7.7 -  "inv" > "Algebras.divide_class.inverse" :: "real => real"
7.8 +  "inv" > "Ring.inverse" :: "real => real"
7.9    "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
7.10
7.11  thm_maps
```
```     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 08:49:26 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 08:49:26 2010 +0100
8.3 @@ -78,7 +78,7 @@
8.4      Const (atom_name "" T j, T)
8.5
8.6  (* term -> real *)
8.7 -fun extract_real_number (Const (@{const_name Algebras.divide}, _) \$ t1 \$ t2) =
8.8 +fun extract_real_number (Const (@{const_name Rings.divide}, _) \$ t1 \$ t2) =
8.9      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
8.10    | extract_real_number t = real (snd (HOLogic.dest_number t))
8.11  (* term * term -> order *)
8.12 @@ -446,7 +446,7 @@
8.13                             0 => mk_num 0
8.14                           | n1 => case HOLogic.dest_number t2 |> snd of
8.15                                     1 => mk_num n1
8.16 -                                 | n2 => Const (@{const_name Algebras.divide},
8.17 +                                 | n2 => Const (@{const_name Rings.divide},
8.18                                                  num_T --> num_T --> num_T)
8.19                                           \$ mk_num n1 \$ mk_num n2)
8.20                        | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
```
```     9.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Feb 10 08:49:26 2010 +0100
9.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 10 08:49:26 2010 +0100
9.3 @@ -150,7 +150,7 @@
9.4                (SOME t', m'') => (SOME (mC \$ s' \$ t'), m'')
9.5              | (NONE,    m'') => (SOME s', m''))
9.6          | (NONE,    m') => demult (t, m')))
9.7 -    | demult ((mC as Const (@{const_name Algebras.divide}, _)) \$ s \$ t, m) =
9.8 +    | demult ((mC as Const (@{const_name Rings.divide}, _)) \$ s \$ t, m) =
9.9        (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
9.10           become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
9.11           if we choose to do so here, the simpset used by arith must be able to
9.12 @@ -212,7 +212,7 @@
9.13          (case demult inj_consts (all, m) of
9.14             (NONE,   m') => (p, Rat.add i m')
9.15           | (SOME u, m') => add_atom u m' pi)
9.16 -    | poly (all as Const (@{const_name Algebras.divide}, _) \$ _ \$ _, m, pi as (p, i)) =
9.17 +    | poly (all as Const (@{const_name Rings.divide}, _) \$ _ \$ _, m, pi as (p, i)) =
9.18          (case demult inj_consts (all, m) of
9.19             (NONE,   m') => (p, Rat.add i m')
9.20           | (SOME u, m') => add_atom u m' pi)
```
```    10.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 08:49:26 2010 +0100
10.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 08:49:26 2010 +0100
10.3 @@ -96,7 +96,7 @@
10.4    Fractions are reduced later by the cancel_numeral_factor simproc.*)
10.5  fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
10.6
10.7 -val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide};
10.8 +val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
10.9
10.10  (*Build term (p / q) * t*)
10.11  fun mk_fcoeff ((p, q), t) =
10.12 @@ -105,7 +105,7 @@
10.13
10.14  (*Express t as a product of a fraction with other sorted terms*)
10.15  fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) \$ t) = dest_fcoeff (~sign) t
10.16 -  | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) \$ t \$ u) =
10.17 +  | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) \$ t \$ u) =
10.18      let val (p, t') = dest_coeff sign t
10.19          val (q, u') = dest_coeff 1 u
10.20      in (mk_frac (p, q), mk_divide (t', u')) end
10.21 @@ -391,8 +391,8 @@
10.22  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
10.23   (open CancelNumeralFactorCommon
10.24    val prove_conv = Arith_Data.prove_conv
10.25 -  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
10.26 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
10.27 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
10.28 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
10.29    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
10.30    val neg_exchanges = false
10.31  )
10.32 @@ -570,8 +570,8 @@
10.33  structure DivideCancelFactor = ExtractCommonTermFun
10.34   (open CancelFactorCommon
10.35    val prove_conv = Arith_Data.prove_conv
10.36 -  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
10.37 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
10.38 +  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
10.39 +  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
10.40    fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
10.41  );
10.42
```
```    11.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 08:49:26 2010 +0100
11.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 08:49:26 2010 +0100
11.3 @@ -65,7 +65,7 @@
11.4      (*abstraction of a real/rational expression*)
11.5      fun rat ((c as Const(@{const_name Algebras.plus}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
11.6        | rat ((c as Const(@{const_name Algebras.minus}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
11.7 -      | rat ((c as Const(@{const_name Algebras.divide}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
11.8 +      | rat ((c as Const(@{const_name Rings.divide}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
11.9        | rat ((c as Const(@{const_name Algebras.times}, _)) \$ x \$ y) = c \$ (rat x) \$ (rat y)
11.10        | rat ((c as Const(@{const_name Algebras.uminus}, _)) \$ x) = c \$ (rat x)
11.11        | rat t = lit t
```
```    12.1 --- a/src/HOL/ex/svc_funcs.ML	Wed Feb 10 08:49:26 2010 +0100
12.2 +++ b/src/HOL/ex/svc_funcs.ML	Wed Feb 10 08:49:26 2010 +0100
12.3 @@ -173,7 +173,7 @@
12.4        | tm (Const(@{const_name Algebras.times}, T) \$ x \$ y) =
12.5            if is_numeric_op T then Interp("*", [tm x, tm y])
12.6            else fail t
12.7 -      | tm (Const(@{const_name Algebras.inverse}, T) \$ x) =
12.8 +      | tm (Const(@{const_name Rings.inverse}, T) \$ x) =
12.9            if domain_type T = HOLogic.realT then
12.10                Rat(1, litExp x)
12.11            else fail t
```