# HG changeset patch # User haftmann # Date 1265788166 -3600 # Node ID e25eedfc15ce053ea499e97064e7fdc7aac6da21 # Parent 3246e66b08749f2cb88ae62ba40e99077b95743b moved constants inverse and divide to Ring.thy diff -r 3246e66b0874 -r e25eedfc15ce NEWS --- a/NEWS Wed Feb 10 08:49:26 2010 +0100 +++ b/NEWS Wed Feb 10 08:49:26 2010 +0100 @@ -20,6 +20,15 @@ consistent names suitable for name prefixes within the HOL theories. INCOMPATIBILITY. +* Some generic constants have been put to appropriate theories: + + inverse, divide: Rings + +INCOMPATIBILITY. + +* Class division ring also requires proof of fact divide_inverse. However instantiation +of parameter divide has also been required previously. INCOMPATIBILITY. + * More consistent naming of type classes involving orderings (and lattices): lower_semilattice ~> semilattice_inf @@ -76,7 +85,7 @@ * New theory Algebras contains generic algebraic structures and generic algebraic operations. INCOMPATIBILTY: constants zero, one, -plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and +plus, minus, uminus, times, abs, sgn, less_eq and less have been moved from HOL.thy to Algebras.thy. * HOLogic.strip_psplit: types are returned in syntactic order, similar diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Algebras.thy --- a/src/HOL/Algebras.thy Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Algebras.thy Wed Feb 10 08:49:26 2010 +0100 @@ -103,10 +103,6 @@ class times = fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) -class inverse = - fixes inverse :: "'a \ 'a" - and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) - class abs = fixes abs :: "'a \ 'a" begin diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Feb 10 08:49:26 2010 +0100 @@ -655,7 +655,7 @@ if h aconvc y then false else if h aconvc x then true else earlier t x y; fun dest_frac ct = case term_of ct of - Const (@{const_name Algebras.divide},_) $ a $ b=> + Const (@{const_name Rings.divide},_) $ a $ b=> Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd) | t => Rat.rat_of_int (snd (HOLogic.dest_number t)) diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Feb 10 08:49:26 2010 +0100 @@ -2946,7 +2946,7 @@ fun num rT x = HOLogic.mk_number rT x; fun rrelT rT = [rT,rT] ---> rT; fun rrT rT = [rT, rT] ---> bT; -fun divt rT = Const(@{const_name Algebras.divide},rrelT rT); +fun divt rT = Const(@{const_name Rings.divide},rrelT rT); fun timest rT = Const(@{const_name Algebras.times},rrelT rT); fun plust rT = Const(@{const_name Algebras.plus},rrelT rT); fun minust rT = Const(@{const_name Algebras.minus},rrelT rT); @@ -2974,7 +2974,7 @@ | Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b) | Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b) | Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n) - | Const(@{const_name Algebras.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) + | Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1) handle TERM _ => @{code poly.Bound} (AList.lookup (op aconv) m t |> the)); diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Fields.thy --- a/src/HOL/Fields.thy Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Fields.thy Wed Feb 10 08:49:26 2010 +0100 @@ -14,8 +14,8 @@ begin class field = comm_ring_1 + inverse + - assumes field_inverse: "a \ 0 \ inverse a * a = 1" - assumes divide_inverse: "a / b = a * inverse b" + assumes field_inverse: "a \ 0 \ inverse a * a = 1" + assumes field_divide_inverse: "a / b = a * inverse b" begin subclass division_ring @@ -24,6 +24,9 @@ assume "a \ 0" thus "inverse a * a = 1" by (rule field_inverse) thus "a * inverse a = 1" by (simp only: mult_commute) +next + fix a b :: 'a + show "a / b = a * inverse b" by (rule field_divide_inverse) qed subclass idom .. diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Groebner_Basis.thy Wed Feb 10 08:49:26 2010 +0100 @@ -489,7 +489,13 @@ by (simp add: add_divide_distrib) lemma add_num_frac: "y\ 0 \ z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y" by (simp add: add_divide_distrib) -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*} + +ML {* +let open Conv +in fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) (@{thm field_divide_inverse} RS sym) +end +*} + ML{* local val zr = @{cpat "0"} @@ -527,13 +533,13 @@ val (l,r) = Thm.dest_binop ct val T = ctyp_of_term l in (case (term_of l, term_of r) of - (Const(@{const_name Algebras.divide},_)$_$_, _) => + (Const(@{const_name Rings.divide},_)$_$_, _) => let val (x,y) = Thm.dest_binop l val z = r val _ = map (HOLogic.dest_number o term_of) [x,y,z] val ynz = prove_nz ss T y in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) end - | (_, Const (@{const_name Algebras.divide},_)$_$_) => + | (_, Const (@{const_name Rings.divide},_)$_$_) => let val (x,y) = Thm.dest_binop r val z = l val _ = map (HOLogic.dest_number o term_of) [x,y,z] val ynz = prove_nz ss T y @@ -543,49 +549,49 @@ end handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE - fun is_number (Const(@{const_name Algebras.divide},_)$a$b) = is_number a andalso is_number b + fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b | is_number t = can HOLogic.dest_number t val is_number = is_number o term_of fun proc3 phi ss ct = (case term_of ct of - Const(@{const_name Algebras.less},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ => + Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => let val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop val _ = map is_number [a,b,c] val T = ctyp_of_term c val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} in SOME (mk_meta_eq th) end - | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ => + | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => let val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop val _ = map is_number [a,b,c] val T = ctyp_of_term c val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} in SOME (mk_meta_eq th) end - | Const("op =",_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ => + | Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => let val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop val _ = map is_number [a,b,c] val T = ctyp_of_term c val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} in SOME (mk_meta_eq th) end - | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) => + | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => let val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop val _ = map is_number [a,b,c] val T = ctyp_of_term c val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} in SOME (mk_meta_eq th) end - | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) => + | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => let val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop val _ = map is_number [a,b,c] val T = ctyp_of_term c val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} in SOME (mk_meta_eq th) end - | Const("op =",_)$_$(Const(@{const_name Algebras.divide},_)$_$_) => + | Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) => let val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop val _ = map is_number [a,b,c] @@ -628,9 +634,9 @@ @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, @{thm "diff_def"}, @{thm "minus_divide_left"}, @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, - @{thm divide_inverse} RS sym, @{thm inverse_divide}, + @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, fconv_rule (arg_conv (arg1_conv (rewr_conv (mk_meta_eq @{thm mult_commute})))) - (@{thm divide_inverse} RS sym)] + (@{thm field_divide_inverse} RS sym)] val comp_conv = (Simplifier.rewrite (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} @@ -645,15 +651,15 @@ fun numeral_is_const ct = case term_of ct of - Const (@{const_name Algebras.divide},_) $ a $ b => + Const (@{const_name Rings.divide},_) $ a $ b => can HOLogic.dest_number a andalso can HOLogic.dest_number b - | Const (@{const_name Algebras.inverse},_)$t => can HOLogic.dest_number t + | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t | t => can HOLogic.dest_number t fun dest_const ct = ((case term_of ct of - Const (@{const_name Algebras.divide},_) $ a $ b=> + Const (@{const_name Rings.divide},_) $ a $ b=> Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) - | Const (@{const_name Algebras.inverse},_)$t => + | Const (@{const_name Rings.inverse},_)$t => Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) handle TERM _ => error "ring_dest_const") diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Import/HOL/realax.imp --- a/src/HOL/Import/HOL/realax.imp Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Import/HOL/realax.imp Wed Feb 10 08:49:26 2010 +0100 @@ -33,7 +33,7 @@ "real_add" > "Algebras.plus_class.plus" :: "real => real => real" "real_1" > "Algebras.one_class.one" :: "real" "real_0" > "Algebras.zero_class.zero" :: "real" - "inv" > "Algebras.divide_class.inverse" :: "real => real" + "inv" > "Ring.inverse" :: "real => real" "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal" thm_maps diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 08:49:26 2010 +0100 @@ -78,7 +78,7 @@ Const (atom_name "" T j, T) (* term -> real *) -fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) = +fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) = real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2)) | extract_real_number t = real (snd (HOLogic.dest_number t)) (* term * term -> order *) @@ -446,7 +446,7 @@ 0 => mk_num 0 | n1 => case HOLogic.dest_number t2 |> snd of 1 => mk_num n1 - | n2 => Const (@{const_name Algebras.divide}, + | n2 => Const (@{const_name Rings.divide}, num_T --> num_T --> num_T) $ mk_num n1 $ mk_num n2) | _ => raise TERM ("Nitpick_Model.reconstruct_term.\ diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Tools/lin_arith.ML Wed Feb 10 08:49:26 2010 +0100 @@ -150,7 +150,7 @@ (SOME t', m'') => (SOME (mC $ s' $ t'), m'') | (NONE, m'') => (SOME s', m'')) | (NONE, m') => demult (t, m'))) - | demult ((mC as Const (@{const_name Algebras.divide}, _)) $ s $ t, m) = + | demult ((mC as Const (@{const_name Rings.divide}, _)) $ s $ t, m) = (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ? Note that if we choose to do so here, the simpset used by arith must be able to @@ -212,7 +212,7 @@ (case demult inj_consts (all, m) of (NONE, m') => (p, Rat.add i m') | (SOME u, m') => add_atom u m' pi) - | poly (all as Const (@{const_name Algebras.divide}, _) $ _ $ _, m, pi as (p, i)) = + | poly (all as Const (@{const_name Rings.divide}, _) $ _ $ _, m, pi as (p, i)) = (case demult inj_consts (all, m) of (NONE, m') => (p, Rat.add i m') | (SOME u, m') => add_atom u m' pi) diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Wed Feb 10 08:49:26 2010 +0100 @@ -96,7 +96,7 @@ Fractions are reduced later by the cancel_numeral_factor simproc.*) fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); -val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide}; +val mk_divide = HOLogic.mk_binop @{const_name Rings.divide}; (*Build term (p / q) * t*) fun mk_fcoeff ((p, q), t) = @@ -105,7 +105,7 @@ (*Express t as a product of a fraction with other sorted terms*) fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t - | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) $ t $ u) = + | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) = let val (p, t') = dest_coeff sign t val (q, u') = dest_coeff 1 u in (mk_frac (p, q), mk_divide (t', u')) end @@ -391,8 +391,8 @@ structure DivideCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Algebras.divide} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT + val mk_bal = HOLogic.mk_binop @{const_name Rings.divide} + val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT val cancel = @{thm mult_divide_mult_cancel_left} RS trans val neg_exchanges = false ) @@ -570,8 +570,8 @@ structure DivideCancelFactor = ExtractCommonTermFun (open CancelFactorCommon val prove_conv = Arith_Data.prove_conv - val mk_bal = HOLogic.mk_binop @{const_name Algebras.divide} - val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT + val mk_bal = HOLogic.mk_binop @{const_name Rings.divide} + val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} ); diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 08:49:26 2010 +0100 @@ -65,7 +65,7 @@ (*abstraction of a real/rational expression*) fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y) - | rat ((c as Const(@{const_name Algebras.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) + | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x) | rat t = lit t diff -r 3246e66b0874 -r e25eedfc15ce src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Wed Feb 10 08:49:26 2010 +0100 +++ b/src/HOL/ex/svc_funcs.ML Wed Feb 10 08:49:26 2010 +0100 @@ -173,7 +173,7 @@ | tm (Const(@{const_name Algebras.times}, T) $ x $ y) = if is_numeric_op T then Interp("*", [tm x, tm y]) else fail t - | tm (Const(@{const_name Algebras.inverse}, T) $ x) = + | tm (Const(@{const_name Rings.inverse}, T) $ x) = if domain_type T = HOLogic.realT then Rat(1, litExp x) else fail t