huffman@17296: (* Title : HOL/Hyperreal/StarClasses.thy huffman@17296: ID : $Id$ huffman@17296: Author : Brian Huffman huffman@17296: *) huffman@17296: huffman@17296: header {* Class Instances *} huffman@17296: huffman@17296: theory StarClasses huffman@17429: imports StarDef huffman@17296: begin huffman@17296: huffman@17332: subsection {* Syntactic classes *} huffman@17332: haftmann@25571: instantiation star :: (zero) zero haftmann@25571: begin haftmann@25571: haftmann@25571: definition haftmann@25571: star_zero_def: "0 \ star_of 0" haftmann@25571: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (one) one haftmann@25571: begin haftmann@25571: haftmann@25571: definition haftmann@25571: star_one_def: "1 \ star_of 1" haftmann@22316: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (plus) plus haftmann@25571: begin haftmann@22316: haftmann@25571: definition haftmann@25571: star_add_def: "(op +) \ *f2* (op +)" haftmann@25571: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (times) times haftmann@25571: begin haftmann@22316: haftmann@25571: definition haftmann@25571: star_mult_def: "(op *) \ *f2* (op *)" haftmann@25571: haftmann@25571: instance .. huffman@17332: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (minus) minus haftmann@25571: begin haftmann@25571: haftmann@25571: definition huffman@17429: star_minus_def: "uminus \ *f* uminus" haftmann@25571: haftmann@25571: definition haftmann@25571: star_diff_def: "(op -) \ *f2* (op -)" haftmann@25571: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@23879: haftmann@25571: instantiation star :: (abs) abs haftmann@25571: begin haftmann@25571: haftmann@25571: definition haftmann@25571: star_abs_def: "abs \ *f* abs" haftmann@25571: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (sgn) sgn haftmann@25571: begin haftmann@22316: haftmann@25571: definition haftmann@25571: star_sgn_def: "sgn \ *f* sgn" haftmann@25571: haftmann@25571: instance .. nipkow@24506: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (inverse) inverse haftmann@25571: begin haftmann@25571: haftmann@25571: definition huffman@17429: star_divide_def: "(op /) \ *f2* (op /)" haftmann@25571: haftmann@25571: definition haftmann@25571: star_inverse_def: "inverse \ *f* inverse" haftmann@25571: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@22316: haftmann@25571: instantiation star :: (number) number haftmann@25571: begin haftmann@25571: haftmann@25571: definition haftmann@25571: star_number_def: "number_of b \ star_of (number_of b)" haftmann@25571: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (Divides.div) Divides.div haftmann@25571: begin haftmann@22316: haftmann@25571: definition huffman@17429: star_div_def: "(op div) \ *f2* (op div)" haftmann@25571: haftmann@25571: definition haftmann@25571: star_mod_def: "(op mod) \ *f2* (op mod)" haftmann@25571: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (power) power haftmann@25571: begin haftmann@25571: haftmann@25571: definition haftmann@25571: star_power_def: "(op ^) \ \x n. ( *f* (\x. x ^ n)) x" haftmann@22316: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (ord) ord haftmann@25571: begin huffman@17332: haftmann@25571: definition haftmann@22452: star_le_def: "(op \) \ *p2* (op \)" haftmann@25571: haftmann@25571: definition haftmann@25571: star_less_def: "(op <) \ *p2* (op <)" haftmann@25571: haftmann@25571: instance .. haftmann@25571: haftmann@25571: end haftmann@22452: huffman@17332: lemmas star_class_defs [transfer_unfold] = huffman@17332: star_zero_def star_one_def star_number_def huffman@17332: star_add_def star_diff_def star_minus_def huffman@17332: star_mult_def star_divide_def star_inverse_def nipkow@24506: star_le_def star_less_def star_abs_def star_sgn_def huffman@17332: star_div_def star_mod_def star_power_def huffman@17332: huffman@20719: text {* Class operations preserve standard elements *} huffman@20719: huffman@20719: lemma Standard_zero: "0 \ Standard" huffman@20719: by (simp add: star_zero_def) huffman@20719: huffman@20719: lemma Standard_one: "1 \ Standard" huffman@20719: by (simp add: star_one_def) huffman@20719: huffman@20719: lemma Standard_number_of: "number_of b \ Standard" huffman@20719: by (simp add: star_number_def) huffman@20719: huffman@20719: lemma Standard_add: "\x \ Standard; y \ Standard\ \ x + y \ Standard" huffman@20719: by (simp add: star_add_def) huffman@20719: huffman@20719: lemma Standard_diff: "\x \ Standard; y \ Standard\ \ x - y \ Standard" huffman@20719: by (simp add: star_diff_def) huffman@20719: huffman@20719: lemma Standard_minus: "x \ Standard \ - x \ Standard" huffman@20719: by (simp add: star_minus_def) huffman@20719: huffman@20719: lemma Standard_mult: "\x \ Standard; y \ Standard\ \ x * y \ Standard" huffman@20719: by (simp add: star_mult_def) huffman@20719: huffman@20719: lemma Standard_divide: "\x \ Standard; y \ Standard\ \ x / y \ Standard" huffman@20719: by (simp add: star_divide_def) huffman@20719: huffman@20719: lemma Standard_inverse: "x \ Standard \ inverse x \ Standard" huffman@20719: by (simp add: star_inverse_def) huffman@20719: huffman@20719: lemma Standard_abs: "x \ Standard \ abs x \ Standard" huffman@20719: by (simp add: star_abs_def) huffman@20719: huffman@20719: lemma Standard_div: "\x \ Standard; y \ Standard\ \ x div y \ Standard" huffman@20719: by (simp add: star_div_def) huffman@20719: huffman@20719: lemma Standard_mod: "\x \ Standard; y \ Standard\ \ x mod y \ Standard" huffman@20719: by (simp add: star_mod_def) huffman@20719: huffman@20719: lemma Standard_power: "x \ Standard \ x ^ n \ Standard" huffman@20719: by (simp add: star_power_def) huffman@20719: huffman@20719: lemmas Standard_simps [simp] = huffman@20719: Standard_zero Standard_one Standard_number_of huffman@20719: Standard_add Standard_diff Standard_minus huffman@20719: Standard_mult Standard_divide Standard_inverse huffman@20719: Standard_abs Standard_div Standard_mod huffman@20719: Standard_power huffman@20719: huffman@17332: text {* @{term star_of} preserves class operations *} huffman@17332: huffman@17332: lemma star_of_add: "star_of (x + y) = star_of x + star_of y" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_diff: "star_of (x - y) = star_of x - star_of y" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_minus: "star_of (-x) = - star_of x" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_mult: "star_of (x * y) = star_of x * star_of y" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_divide: "star_of (x / y) = star_of x / star_of y" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_div: "star_of (x div y) = star_of x div star_of y" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_power: "star_of (x ^ n) = star_of x ^ n" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_abs: "star_of (abs x) = abs (star_of x)" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: text {* @{term star_of} preserves numerals *} huffman@17332: huffman@17332: lemma star_of_zero: "star_of 0 = 0" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_one: "star_of 1 = 1" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_number_of: "star_of (number_of x) = number_of x" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: text {* @{term star_of} preserves orderings *} huffman@17332: huffman@17332: lemma star_of_less: "(star_of x < star_of y) = (x < y)" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_le: "(star_of x \ star_of y) = (x \ y)" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: lemma star_of_eq: "(star_of x = star_of y) = (x = y)" huffman@17332: by transfer (rule refl) huffman@17332: huffman@17332: text{*As above, for 0*} huffman@17332: huffman@17332: lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero] huffman@17332: lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero] huffman@17332: lemmas star_of_0_eq = star_of_eq [of 0, simplified star_of_zero] huffman@17332: huffman@17332: lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero] huffman@17332: lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero] huffman@17332: lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero] huffman@17332: huffman@17332: text{*As above, for 1*} huffman@17332: huffman@17332: lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one] huffman@17332: lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one] huffman@17332: lemmas star_of_1_eq = star_of_eq [of 1, simplified star_of_one] huffman@17332: huffman@17332: lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one] huffman@17332: lemmas star_of_le_1 = star_of_le [of _ 1, simplified star_of_one] huffman@17332: lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one] huffman@17332: huffman@17332: text{*As above, for numerals*} huffman@17332: huffman@17332: lemmas star_of_number_less = huffman@17332: star_of_less [of "number_of w", standard, simplified star_of_number_of] huffman@17332: lemmas star_of_number_le = huffman@17332: star_of_le [of "number_of w", standard, simplified star_of_number_of] huffman@17332: lemmas star_of_number_eq = huffman@17332: star_of_eq [of "number_of w", standard, simplified star_of_number_of] huffman@17332: huffman@17332: lemmas star_of_less_number = huffman@17332: star_of_less [of _ "number_of w", standard, simplified star_of_number_of] huffman@17332: lemmas star_of_le_number = huffman@17332: star_of_le [of _ "number_of w", standard, simplified star_of_number_of] huffman@17332: lemmas star_of_eq_number = huffman@17332: star_of_eq [of _ "number_of w", standard, simplified star_of_number_of] huffman@17332: huffman@17332: lemmas star_of_simps [simp] = huffman@17332: star_of_add star_of_diff star_of_minus huffman@17332: star_of_mult star_of_divide star_of_inverse huffman@17332: star_of_div star_of_mod huffman@17332: star_of_power star_of_abs huffman@17332: star_of_zero star_of_one star_of_number_of huffman@17332: star_of_less star_of_le star_of_eq huffman@17332: star_of_0_less star_of_0_le star_of_0_eq huffman@17332: star_of_less_0 star_of_le_0 star_of_eq_0 huffman@17332: star_of_1_less star_of_1_le star_of_1_eq huffman@17332: star_of_less_1 star_of_le_1 star_of_eq_1 huffman@17332: star_of_number_less star_of_number_le star_of_number_eq huffman@17332: star_of_less_number star_of_le_number star_of_eq_number huffman@17332: haftmann@22452: subsection {* Ordering and lattice classes *} huffman@17296: huffman@17296: instance star :: (order) order huffman@17296: apply (intro_classes) haftmann@22316: apply (transfer, rule order_less_le) huffman@17296: apply (transfer, rule order_refl) huffman@17296: apply (transfer, erule (1) order_trans) huffman@17296: apply (transfer, erule (1) order_antisym) huffman@17296: done huffman@17296: haftmann@25571: instantiation star :: (lower_semilattice) lower_semilattice haftmann@25571: begin haftmann@25571: haftmann@25571: definition haftmann@22452: star_inf_def [transfer_unfold]: "inf \ *f2* inf" haftmann@25571: haftmann@25571: instance haftmann@22452: by default (transfer star_inf_def, auto)+ haftmann@22452: haftmann@25571: end haftmann@25571: haftmann@25571: instantiation star :: (upper_semilattice) upper_semilattice haftmann@25571: begin haftmann@25571: haftmann@25571: definition haftmann@22452: star_sup_def [transfer_unfold]: "sup \ *f2* sup" haftmann@25571: haftmann@25571: instance haftmann@22452: by default (transfer star_sup_def, auto)+ haftmann@22452: haftmann@25571: end haftmann@25571: haftmann@22452: instance star :: (lattice) lattice .. haftmann@22452: haftmann@22452: instance star :: (distrib_lattice) distrib_lattice haftmann@22452: by default (transfer, auto simp add: sup_inf_distrib1) haftmann@22452: haftmann@22452: lemma Standard_inf [simp]: haftmann@22452: "\x \ Standard; y \ Standard\ \ inf x y \ Standard" haftmann@22452: by (simp add: star_inf_def) haftmann@22452: haftmann@22452: lemma Standard_sup [simp]: haftmann@22452: "\x \ Standard; y \ Standard\ \ sup x y \ Standard" haftmann@22452: by (simp add: star_sup_def) haftmann@22452: haftmann@22452: lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)" haftmann@22452: by transfer (rule refl) haftmann@22452: haftmann@22452: lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)" haftmann@22452: by transfer (rule refl) haftmann@22452: huffman@17296: instance star :: (linorder) linorder huffman@17296: by (intro_classes, transfer, rule linorder_linear) huffman@17296: huffman@20720: lemma star_max_def [transfer_unfold]: "max = *f2* max" huffman@20720: apply (rule ext, rule ext) huffman@20720: apply (unfold max_def, transfer, fold max_def) huffman@20720: apply (rule refl) huffman@20720: done huffman@20720: huffman@20720: lemma star_min_def [transfer_unfold]: "min = *f2* min" huffman@20720: apply (rule ext, rule ext) huffman@20720: apply (unfold min_def, transfer, fold min_def) huffman@20720: apply (rule refl) huffman@20720: done huffman@20720: huffman@20720: lemma Standard_max [simp]: huffman@20720: "\x \ Standard; y \ Standard\ \ max x y \ Standard" huffman@20720: by (simp add: star_max_def) huffman@20720: huffman@20720: lemma Standard_min [simp]: huffman@20720: "\x \ Standard; y \ Standard\ \ min x y \ Standard" huffman@20720: by (simp add: star_min_def) huffman@20720: huffman@20720: lemma star_of_max [simp]: "star_of (max x y) = max (star_of x) (star_of y)" huffman@20720: by transfer (rule refl) huffman@20720: huffman@20720: lemma star_of_min [simp]: "star_of (min x y) = min (star_of x) (star_of y)" huffman@20720: by transfer (rule refl) huffman@20720: huffman@17296: huffman@17332: subsection {* Ordered group classes *} huffman@17296: huffman@17296: instance star :: (semigroup_add) semigroup_add huffman@17296: by (intro_classes, transfer, rule add_assoc) huffman@17296: huffman@17296: instance star :: (ab_semigroup_add) ab_semigroup_add huffman@17296: by (intro_classes, transfer, rule add_commute) huffman@17296: huffman@17296: instance star :: (semigroup_mult) semigroup_mult huffman@17296: by (intro_classes, transfer, rule mult_assoc) huffman@17296: huffman@17296: instance star :: (ab_semigroup_mult) ab_semigroup_mult huffman@17296: by (intro_classes, transfer, rule mult_commute) huffman@17296: huffman@17296: instance star :: (comm_monoid_add) comm_monoid_add haftmann@22384: by (intro_classes, transfer, rule comm_monoid_add_class.zero_plus.add_0) huffman@17296: huffman@17296: instance star :: (monoid_mult) monoid_mult huffman@17296: apply (intro_classes) huffman@17296: apply (transfer, rule mult_1_left) huffman@17296: apply (transfer, rule mult_1_right) huffman@17296: done huffman@17296: huffman@17296: instance star :: (comm_monoid_mult) comm_monoid_mult huffman@17296: by (intro_classes, transfer, rule mult_1) huffman@17296: huffman@17296: instance star :: (cancel_semigroup_add) cancel_semigroup_add huffman@17296: apply (intro_classes) huffman@17296: apply (transfer, erule add_left_imp_eq) huffman@17296: apply (transfer, erule add_right_imp_eq) huffman@17296: done huffman@17296: huffman@17296: instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add huffman@17296: by (intro_classes, transfer, rule add_imp_eq) huffman@17296: huffman@17296: instance star :: (ab_group_add) ab_group_add huffman@17296: apply (intro_classes) huffman@17296: apply (transfer, rule left_minus) huffman@17296: apply (transfer, rule diff_minus) huffman@17296: done huffman@17296: huffman@17296: instance star :: (pordered_ab_semigroup_add) pordered_ab_semigroup_add huffman@17296: by (intro_classes, transfer, rule add_left_mono) huffman@17296: huffman@17296: instance star :: (pordered_cancel_ab_semigroup_add) pordered_cancel_ab_semigroup_add .. huffman@17296: huffman@17296: instance star :: (pordered_ab_semigroup_add_imp_le) pordered_ab_semigroup_add_imp_le huffman@17296: by (intro_classes, transfer, rule add_le_imp_le_left) huffman@17296: haftmann@25304: instance star :: (pordered_comm_monoid_add) pordered_comm_monoid_add .. huffman@17296: instance star :: (pordered_ab_group_add) pordered_ab_group_add .. haftmann@25304: haftmann@25304: instance star :: (pordered_ab_group_add_abs) pordered_ab_group_add_abs haftmann@25304: by intro_classes (transfer, haftmann@25304: simp add: abs_ge_self abs_leI abs_triangle_ineq)+ haftmann@25304: huffman@17296: instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add .. haftmann@25304: instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet .. haftmann@25304: instance star :: (lordered_ab_group_add_meet) lordered_ab_group_add_meet .. haftmann@25304: instance star :: (lordered_ab_group_add) lordered_ab_group_add .. huffman@17296: haftmann@25304: instance star :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs huffman@17332: by (intro_classes, transfer, rule abs_lattice) huffman@17296: huffman@17429: subsection {* Ring and field classes *} huffman@17296: huffman@17296: instance star :: (semiring) semiring huffman@17296: apply (intro_classes) huffman@17296: apply (transfer, rule left_distrib) huffman@17296: apply (transfer, rule right_distrib) huffman@17296: done huffman@17296: krauss@21199: instance star :: (semiring_0) semiring_0 krauss@21199: by intro_classes (transfer, simp)+ krauss@21199: huffman@17296: instance star :: (semiring_0_cancel) semiring_0_cancel .. huffman@17296: paulson@24742: instance star :: (comm_semiring) comm_semiring paulson@24742: by (intro_classes, transfer, rule left_distrib) huffman@17296: huffman@17296: instance star :: (comm_semiring_0) comm_semiring_0 .. huffman@17296: instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. huffman@17296: wenzelm@20633: instance star :: (zero_neq_one) zero_neq_one huffman@17296: by (intro_classes, transfer, rule zero_neq_one) huffman@17296: huffman@17296: instance star :: (semiring_1) semiring_1 .. huffman@17296: instance star :: (comm_semiring_1) comm_semiring_1 .. huffman@17296: wenzelm@20633: instance star :: (no_zero_divisors) no_zero_divisors huffman@17296: by (intro_classes, transfer, rule no_zero_divisors) huffman@17296: huffman@17296: instance star :: (semiring_1_cancel) semiring_1_cancel .. huffman@17296: instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel .. huffman@17296: instance star :: (ring) ring .. huffman@17296: instance star :: (comm_ring) comm_ring .. huffman@17296: instance star :: (ring_1) ring_1 .. huffman@17296: instance star :: (comm_ring_1) comm_ring_1 .. huffman@22992: instance star :: (ring_no_zero_divisors) ring_no_zero_divisors .. wenzelm@23551: instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. huffman@17296: instance star :: (idom) idom .. huffman@17296: huffman@20540: instance star :: (division_ring) division_ring huffman@20540: apply (intro_classes) huffman@20540: apply (transfer, erule left_inverse) huffman@20540: apply (transfer, erule right_inverse) huffman@20540: done huffman@20540: huffman@17296: instance star :: (field) field huffman@17296: apply (intro_classes) huffman@17296: apply (transfer, erule left_inverse) huffman@17296: apply (transfer, rule divide_inverse) huffman@17296: done huffman@17296: huffman@17296: instance star :: (division_by_zero) division_by_zero huffman@17296: by (intro_classes, transfer, rule inverse_zero) huffman@17296: huffman@17296: instance star :: (pordered_semiring) pordered_semiring huffman@17296: apply (intro_classes) huffman@17296: apply (transfer, erule (1) mult_left_mono) huffman@17296: apply (transfer, erule (1) mult_right_mono) huffman@17296: done huffman@17296: huffman@17296: instance star :: (pordered_cancel_semiring) pordered_cancel_semiring .. huffman@17296: huffman@17296: instance star :: (ordered_semiring_strict) ordered_semiring_strict huffman@17296: apply (intro_classes) huffman@17296: apply (transfer, erule (1) mult_strict_left_mono) huffman@17296: apply (transfer, erule (1) mult_strict_right_mono) huffman@17296: done huffman@17296: huffman@17296: instance star :: (pordered_comm_semiring) pordered_comm_semiring haftmann@25230: by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono1) huffman@17296: huffman@17296: instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring .. huffman@17296: huffman@17296: instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict haftmann@25208: by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono) huffman@17296: huffman@17296: instance star :: (pordered_ring) pordered_ring .. haftmann@25304: instance star :: (pordered_ring_abs) pordered_ring_abs haftmann@25304: by intro_classes (transfer, rule abs_eq_mult) huffman@17296: instance star :: (lordered_ring) lordered_ring .. huffman@17296: wenzelm@20633: instance star :: (abs_if) abs_if huffman@17296: by (intro_classes, transfer, rule abs_if) huffman@17296: nipkow@24506: instance star :: (sgn_if) sgn_if nipkow@24506: by (intro_classes, transfer, rule sgn_if) nipkow@24506: huffman@17296: instance star :: (ordered_ring_strict) ordered_ring_strict .. huffman@17296: instance star :: (pordered_comm_ring) pordered_comm_ring .. huffman@17296: huffman@17296: instance star :: (ordered_semidom) ordered_semidom huffman@17296: by (intro_classes, transfer, rule zero_less_one) huffman@17296: huffman@17296: instance star :: (ordered_idom) ordered_idom .. huffman@17296: instance star :: (ordered_field) ordered_field .. huffman@17296: huffman@17332: subsection {* Power classes *} huffman@17296: huffman@17296: text {* huffman@17296: Proving the class axiom @{thm [source] power_Suc} for type huffman@17296: @{typ "'a star"} is a little tricky, because it quantifies huffman@17296: over values of type @{typ nat}. The transfer principle does huffman@17296: not handle quantification over non-star types in general, huffman@17296: but we can work around this by fixing an arbitrary @{typ nat} huffman@17296: value, and then applying the transfer principle. huffman@17296: *} huffman@17296: huffman@17296: instance star :: (recpower) recpower huffman@17296: proof huffman@17296: show "\a::'a star. a ^ 0 = 1" huffman@17296: by transfer (rule power_0) huffman@17296: next huffman@17296: fix n show "\a::'a star. a ^ Suc n = a * a ^ n" huffman@17296: by transfer (rule power_Suc) huffman@17296: qed huffman@17296: huffman@17332: subsection {* Number classes *} huffman@17296: huffman@20720: lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)" haftmann@25230: by (induct n, simp_all) huffman@20720: huffman@20720: lemma Standard_of_nat [simp]: "of_nat n \ Standard" huffman@20720: by (simp add: star_of_nat_def) huffman@17296: huffman@17332: lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n" huffman@17332: by transfer (rule refl) huffman@17332: huffman@20720: lemma star_of_int_def [transfer_unfold]: "of_int z = star_of (of_int z)" huffman@20720: by (rule_tac z=z in int_diff_cases, simp) huffman@20720: huffman@20720: lemma Standard_of_int [simp]: "of_int z \ Standard" huffman@20720: by (simp add: star_of_int_def) huffman@17332: huffman@17332: lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z" huffman@17332: by transfer (rule refl) huffman@17296: huffman@23282: instance star :: (semiring_char_0) semiring_char_0 haftmann@24195: by intro_classes (simp only: star_of_nat_def star_of_eq of_nat_eq_iff) huffman@23282: huffman@23282: instance star :: (ring_char_0) ring_char_0 .. huffman@22911: huffman@17296: instance star :: (number_ring) number_ring huffman@17296: by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq) huffman@17296: huffman@17429: subsection {* Finite class *} huffman@17429: huffman@17429: lemma starset_finite: "finite A \ *s* A = star_of ` A" huffman@17429: by (erule finite_induct, simp_all) huffman@17429: huffman@17429: instance star :: (finite) finite huffman@17429: apply (intro_classes) huffman@17429: apply (subst starset_UNIV [symmetric]) huffman@17429: apply (subst starset_finite [OF finite]) huffman@17429: apply (rule finite_imageI [OF finite]) huffman@17429: done huffman@17429: huffman@17296: end