moved class power to theory Power
authorhaftmann
Fri Oct 12 08:25:48 2007 +0200 (2007-10-12)
changeset 24996ebd5f4cc7118
parent 24995 c26e0166e568
child 24997 730d74336b4d
moved class power to theory Power
NEWS
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Real.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Import/HOL/real.imp
src/HOL/Library/comm_ring.ML
src/HOL/Power.thy
src/HOL/Relation_Power.thy
src/HOL/Tools/Qelim/presburger.ML
     1.1 --- a/NEWS	Fri Oct 12 08:25:47 2007 +0200
     1.2 +++ b/NEWS	Fri Oct 12 08:25:48 2007 +0200
     1.3 @@ -741,19 +741,21 @@
     1.4  
     1.5      HOL.abs ~> HOL.minus_class.abs
     1.6      HOL.divide ~> HOL.divide_class.divide
     1.7 -    Nat.power ~> Nat.power_class.power
     1.8 +    Nat.power ~> Power.power_class.power
     1.9      Nat.size ~> Nat.size_class.size
    1.10      Numeral.number_of ~> Numeral.number_class.number_of
    1.11 -    FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf
    1.12 -    FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
    1.13 +    FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf
    1.14 +    FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup
    1.15      Orderings.min ~> Orderings.ord_class.min
    1.16      Orderings.max ~> Orderings.ord_class.max
    1.17  
    1.18 +INCOMPATIBILITY.
    1.19 +
    1.20  * New class "default" with associated constant "default".
    1.21  
    1.22  * New constant "undefined" with axiom "undefined x = undefined".
    1.23  
    1.24 -* primrec: missing cases mapped to "undefined" instead of "arbitrary"
    1.25 +* primrec: missing cases mapped to "undefined" instead of "arbitrary".
    1.26  
    1.27  * New function listsum :: 'a list => 'a for arbitrary monoids.
    1.28  Special syntax: "SUM x <- xs. f x" (and latex variants)
     2.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Oct 12 08:25:47 2007 +0200
     2.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Oct 12 08:25:48 2007 +0200
     2.3 @@ -189,7 +189,7 @@
     2.4    MAX          > Orderings.ord_class.max    :: "[nat,nat]=>nat"
     2.5    DIV          > Divides.div_class.div :: "[nat,nat]=>nat"
     2.6    MOD          > Divides.div_class.mod :: "[nat,nat]=>nat"
     2.7 -  EXP          > Nat.power_class.power :: "[nat,nat]=>nat";
     2.8 +  EXP          > Power.power_class.power :: "[nat,nat]=>nat";
     2.9  
    2.10  end_import;
    2.11  
     3.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Oct 12 08:25:47 2007 +0200
     3.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Oct 12 08:25:48 2007 +0200
     3.3 @@ -54,7 +54,7 @@
     3.4    real_lte    > HOL.ord_class.less_eq :: "[real,real] => bool"
     3.5    real_sub    > HOL.minus    :: "[real,real] => real"
     3.6    "/"         > HOL.divide   :: "[real,real] => real"
     3.7 -  pow         > Nat.power    :: "[real,nat] => real"
     3.8 +  pow         > Power.power_class.power    :: "[real,nat] => real"
     3.9    abs         > HOL.abs      :: "real => real"
    3.10    real_of_num > RealDef.real :: "nat => real";
    3.11  
     4.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Fri Oct 12 08:25:47 2007 +0200
     4.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Oct 12 08:25:48 2007 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4    "MIN" > "Orderings.ord_class.min" :: "nat => nat => nat"
     4.5    "MAX" > "Orderings.ord_class.max" :: "nat => nat => nat"
     4.6    "FUNPOW" > "HOL4Compat.FUNPOW"
     4.7 -  "EXP" > "Nat.power_class.power" :: "nat => nat => nat"
     4.8 +  "EXP" > "Power.power_class.power" :: "nat => nat => nat"
     4.9    "DIV" > "Divides.div_class.div" :: "nat => nat => nat"
    4.10    "MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
    4.11    "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
     5.1 --- a/src/HOL/Import/HOL/real.imp	Fri Oct 12 08:25:47 2007 +0200
     5.2 +++ b/src/HOL/Import/HOL/real.imp	Fri Oct 12 08:25:48 2007 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4    "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool"
     5.5    "real_gt" > "HOL4Compat.real_gt"
     5.6    "real_ge" > "HOL4Compat.real_ge"
     5.7 -  "pow" > "Nat.power_class.power" :: "real => nat => real"
     5.8 +  "pow" > "Power.power_class.power" :: "real => nat => real"
     5.9    "abs" > "HOL.minus_class.abs" :: "real => real"
    5.10    "/" > "HOL.divides_class.divide" :: "real => real => real"
    5.11  
     6.1 --- a/src/HOL/Library/comm_ring.ML	Fri Oct 12 08:25:47 2007 +0200
     6.2 +++ b/src/HOL/Library/comm_ring.ML	Fri Oct 12 08:25:48 2007 +0200
     6.3 @@ -61,7 +61,7 @@
     6.4        polex_mul T $ reif_polex T vs a $ reif_polex T vs b
     6.5    | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
     6.6        polex_neg T $ reif_polex T vs a
     6.7 -  | reif_polex T vs (Const (@{const_name Nat.power}, _) $ a $ n) =
     6.8 +  | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
     6.9        polex_pow T $ reif_polex T vs a $ n
    6.10    | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
    6.11  
     7.1 --- a/src/HOL/Power.thy	Fri Oct 12 08:25:47 2007 +0200
     7.2 +++ b/src/HOL/Power.thy	Fri Oct 12 08:25:48 2007 +0200
     7.3 @@ -11,6 +11,9 @@
     7.4  imports Nat
     7.5  begin
     7.6  
     7.7 +class power = type +
     7.8 +  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
     7.9 +
    7.10  subsection{*Powers for Arbitrary Monoids*}
    7.11  
    7.12  class recpower = monoid_mult + power +
     8.1 --- a/src/HOL/Relation_Power.thy	Fri Oct 12 08:25:47 2007 +0200
     8.2 +++ b/src/HOL/Relation_Power.thy	Fri Oct 12 08:25:48 2007 +0200
     8.3 @@ -7,7 +7,7 @@
     8.4  header{*Powers of Relations and Functions*}
     8.5  
     8.6  theory Relation_Power
     8.7 -imports Nat
     8.8 +imports Power
     8.9  begin
    8.10  
    8.11  instance
     9.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Fri Oct 12 08:25:47 2007 +0200
     9.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Oct 12 08:25:48 2007 +0200
     9.3 @@ -62,7 +62,7 @@
     9.4   | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
     9.5   | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
     9.6   | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
     9.7 - | Const(@{const_name "Nat.power"},_)$l$r => isnum l andalso isnum r
     9.8 + | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
     9.9   | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
    9.10   | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
    9.11   | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t