(* Title: HOL/Nonstandard_Analysis/StarDef.thy
Author: Jacques D. Fleuriot and Brian Huffman
*)
section ‹Construction of Star
Types Using Ultrafilters
›
theory StarDef
imports Free_Ultrafilter
begin
subsection ‹A Free Ultrafilter over the Naturals
›
definition FreeUltrafilterNat ::
"nat filter" (
‹U›)
where "\ = (SOME U. freeultrafilter U)"
lemma freeultrafilter_FreeUltrafilterNat:
"freeultrafilter \"
unfolding FreeUltrafilterNat_def
by (simp add: freeultrafilter_Ex someI_ex)
interpretation FreeUltrafilterNat: freeultrafilter
U
by (rule freeultrafilter_FreeUltrafilterNat)
subsection ‹Definition of
‹star
› type constructor
›
definition starrel ::
"((nat \ 'a) \ (nat \ 'a)) set"
where "starrel = {(X, Y). eventually (\n. X n = Y n) \}"
definition "star = (UNIV :: (nat \ 'a) set) // starrel"
typedef 'a star = "star :: (nat \ 'a) set set
"
by (auto simp: star_def intro: quotientI)
definition star_n ::
"(nat \ 'a) \ 'a star"
where "star_n X = Abs_star (starrel `` {X})"
theorem star_cases [case_names star_n, cases type: star]:
obtains X
where "x = star_n X"
by (cases x) (auto simp: star_n_def star_def elim: quotientE)
lemma all_star_eq:
"(\x. P x) \ (\X. P (star_n X))"
by (metis star_cases)
lemma ex_star_eq:
"(\x. P x) \ (\X. P (star_n X))"
by (metis star_cases)
text ‹Proving that
🍋‹starrel
› is an equivalence relation.
›
lemma starrel_iff [iff]:
"(X, Y) \ starrel \ eventually (\n. X n = Y n) \"
by (simp add: starrel_def)
lemma equiv_starrel:
"equiv UNIV starrel"
proof (rule equivI)
show "starrel \ UNIV \ UNIV" by simp
show "refl starrel" by (simp add: refl_on_def)
show "sym starrel" by (simp add: sym_def eq_commute)
show "trans starrel" by (intro transI) (auto elim: eventually_elim2)
qed
lemmas equiv_starrel_iff = eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I]
lemma starrel_in_star:
"starrel``{x} \ star"
by (simp add: star_def quotientI)
lemma star_n_eq_iff:
"star_n X = star_n Y \ eventually (\n. X n = Y n) \"
by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
subsection ‹Transfer principle
›
text ‹This introduction rule starts each transfer
proof.
›
lemma transfer_start:
"P \ eventually (\n. Q) \ \ Trueprop P \ Trueprop Q"
by (simp add: FreeUltrafilterNat.proper)
text ‹Standard principles that play a central role
in the transfer tactic.
›
definition Ifun ::
"('a \ 'b) star \ 'a star \ 'b star"
(
‹(
‹notation=
‹infix ⋆››_
⋆/ _)
› [300, 301] 300)
where "Ifun f \
λx. Abs_star (
∪F
∈Rep_star f.
∪X
∈Rep_star x. starrel``{λn. F n (X n)})
"
lemma Ifun_congruent2:
"congruent2 starrel starrel (\F X. starrel``{\n. F n (X n)})"
by (auto simp add: congruent2_def equiv_starrel_iff elim!: eventually_rev_mp)
lemma Ifun_star_n:
"star_n F \ star_n X = star_n (\n. F n (X n))"
by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
lemma transfer_Ifun:
"f \ star_n F \ x \ star_n X \ f \ x \ star_n (\n. F n (X n))"
by (simp only: Ifun_star_n)
definition star_of ::
"'a \ 'a star"
where "star_of x \ star_n (\n. x)"
text ‹Initialize transfer tactic.
›
ML_file
‹transfer_principle.ML
›
method_setup transfer =
‹Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD
' (Transfer_Principle.transfer_tac ctxt ths))\
"transfer principle"
text ‹Transfer introduction rules.
›
lemma transfer_ex [transfer_intro]:
"(\X. p (star_n X) \ eventually (\n. P n (X n)) \) \
∃x::
'a star. p x \ eventually (\n. \x. P n x) \"
by (simp only: ex_star_eq eventually_ex)
lemma transfer_all [transfer_intro]:
"(\X. p (star_n X) \ eventually (\n. P n (X n)) \) \
∀x::
'a star. p x \ eventually (\n. \x. P n x) \"
by (simp only: all_star_eq FreeUltrafilterNat.eventually_all_iff)
lemma transfer_not [transfer_intro]:
"p \ eventually P \ \ \ p \ eventually (\n. \ P n) \"
by (simp only: FreeUltrafilterNat.eventually_not_iff)
lemma transfer_conj [transfer_intro]:
"p \ eventually P \ \ q \ eventually Q \ \ p \ q \ eventually (\n. P n \ Q n) \"
by (simp only: eventually_conj_iff)
lemma transfer_disj [transfer_intro]:
"p \ eventually P \ \ q \ eventually Q \ \ p \ q \ eventually (\n. P n \ Q n) \"
by (simp only: FreeUltrafilterNat.eventually_disj_iff)
lemma transfer_imp [transfer_intro]:
"p \ eventually P \ \ q \ eventually Q \ \ p \ q \ eventually (\n. P n \ Q n) \"
by (simp only: FreeUltrafilterNat.eventually_imp_iff)
lemma transfer_iff [transfer_intro]:
"p \ eventually P \ \ q \ eventually Q \ \ p = q \ eventually (\n. P n = Q n) \"
by (simp only: FreeUltrafilterNat.eventually_iff_iff)
lemma transfer_if_bool [transfer_intro]:
"p \ eventually P \ \ x \ eventually X \ \ y \ eventually Y \ \
(
if p
then x else y)
≡ eventually (λn.
if P n
then X n else Y n)
U"
by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
lemma transfer_eq [transfer_intro]:
"x \ star_n X \ y \ star_n Y \ x = y \ eventually (\n. X n = Y n) \"
by (simp only: star_n_eq_iff)
lemma transfer_if [transfer_intro]:
"p \ eventually (\n. P n) \ \ x \ star_n X \ y \ star_n Y \
(
if p
then x else y)
≡ star_n (λn.
if P n
then X n else Y n)
"
by (rule eq_reflection) (auto simp: star_n_eq_iff transfer_not elim!: eventually_mono)
lemma transfer_fun_eq [transfer_intro]:
"(\X. f (star_n X) = g (star_n X) \ eventually (\n. F n (X n) = G n (X n)) \) \
f = g
≡ eventually (λn. F n = G n)
U"
by (simp only: fun_eq_iff transfer_all)
lemma transfer_star_n [transfer_intro]:
"star_n X \ star_n (\n. X n)"
by (rule reflexive)
lemma transfer_bool [transfer_intro]:
"p \ eventually (\n. p) \"
by (simp add: FreeUltrafilterNat.proper)
subsection ‹Standard elements
›
definition Standard ::
"'a star set"
where "Standard = range star_of"
text ‹Transfer tactic should remove occurrences of
🍋‹star_of
›.
›
setup ‹Transfer_Principle.add_const
🍋‹star_of
››
lemma star_of_inject:
"star_of x = star_of y \ x = y"
by transfer (rule refl)
lemma Standard_star_of [simp]:
"star_of x \ Standard"
by (simp add: Standard_def)
subsection ‹Internal functions
›
text ‹Transfer tactic should remove occurrences of
🍋‹Ifun
›.
›
setup ‹Transfer_Principle.add_const
🍋‹Ifun
››
lemma Ifun_star_of [simp]:
"star_of f \ star_of x = star_of (f x)"
by transfer (rule refl)
lemma Standard_Ifun [simp]:
"f \ Standard \ x \ Standard \ f \ x \ Standard"
by (auto simp add: Standard_def)
text ‹Nonstandard extensions of functions.
›
definition starfun ::
"('a \ 'b) \ 'a star \ 'b star"
(
‹(
‹open_block
notation=
‹prefix starfun
››*f* _)
› [80] 80)
where "starfun f \ \x. star_of f \ x"
definition starfun2 ::
"('a \ 'b \ 'c) \ 'a star \ 'b star \ 'c star"
(
‹(
‹open_block
notation=
‹prefix starfun2
››*f2* _)
› [80] 80)
where "starfun2 f \ \x y. star_of f \ x \ y"
declare starfun_def [transfer_unfold]
declare starfun2_def [transfer_unfold]
lemma starfun_star_n:
"( *f* f) (star_n X) = star_n (\n. f (X n))"
by (simp only: starfun_def star_of_def Ifun_star_n)
lemma starfun2_star_n:
"( *f2* f) (star_n X) (star_n Y) = star_n (\n. f (X n) (Y n))"
by (simp only: starfun2_def star_of_def Ifun_star_n)
lemma starfun_star_of [simp]:
"( *f* f) (star_of x) = star_of (f x)"
by transfer (rule refl)
lemma starfun2_star_of [simp]:
"( *f2* f) (star_of x) = *f* f x"
by transfer (rule refl)
lemma Standard_starfun [simp]:
"x \ Standard \ starfun f x \ Standard"
by (simp add: starfun_def)
lemma Standard_starfun2 [simp]:
"x \ Standard \ y \ Standard \ starfun2 f x y \ Standard"
by (simp add: starfun2_def)
lemma Standard_starfun_iff:
assumes inj:
"\x y. f x = f y \ x = y"
shows "starfun f x \ Standard \ x \ Standard"
proof
assume "x \ Standard"
then show "starfun f x \ Standard" by simp
next
from inj
have inj
': "\x y. starfun f x = starfun f y \ x = y"
by transfer
assume "starfun f x \ Standard"
then obtain b
where b:
"starfun f x = star_of b"
unfolding Standard_def ..
then have "\x. starfun f x = star_of b" ..
then have "\a. f a = b" by transfer
then obtain a
where "f a = b" ..
then have "starfun f (star_of a) = star_of b" by transfer
with b
have "starfun f x = starfun f (star_of a)" by simp
then have "x = star_of a" by (rule inj
')
then show "x \ Standard" by (simp add: Standard_def)
qed
lemma Standard_starfun2_iff:
assumes inj:
"\a b a' b'. f a b = f a' b' \ a = a' \ b = b'"
shows "starfun2 f x y \ Standard \ x \ Standard \ y \ Standard"
proof
assume "x \ Standard \ y \ Standard"
then show "starfun2 f x y \ Standard" by simp
next
have inj
': "\x y z w. starfun2 f x y = starfun2 f z w \ x = z \ y = w"
using inj
by transfer
assume "starfun2 f x y \ Standard"
then obtain c
where c:
"starfun2 f x y = star_of c"
unfolding Standard_def ..
then have "\x y. starfun2 f x y = star_of c" by auto
then have "\a b. f a b = c" by transfer
then obtain a b
where "f a b = c" by auto
then have "starfun2 f (star_of a) (star_of b) = star_of c" by transfer
with c
have "starfun2 f x y = starfun2 f (star_of a) (star_of b)" by simp
then have "x = star_of a \ y = star_of b" by (rule inj
')
then show "x \ Standard \ y \ Standard" by (simp add: Standard_def)
qed
subsection ‹Internal predicates
›
definition unstar ::
"bool star \ bool"
where "unstar b \ b = star_of True"
lemma unstar_star_n:
"unstar (star_n P) \ eventually P \"
by (simp add: unstar_def star_of_def star_n_eq_iff)
lemma unstar_star_of [simp]:
"unstar (star_of p) = p"
by (simp add: unstar_def star_of_inject)
text ‹Transfer tactic should remove occurrences of
🍋‹unstar
›.
›
setup ‹Transfer_Principle.add_const
🍋‹unstar
››
lemma transfer_unstar [transfer_intro]:
"p \ star_n P \ unstar p \ eventually P \"
by (simp only: unstar_star_n)
definition starP ::
"('a \ bool) \ 'a star \ bool"
(
‹(
‹open_block
notation=
‹prefix starP
››*p* _)
› [80] 80)
where "*p* P = (\x. unstar (star_of P \ x))"
definition starP2 ::
"('a \ 'b \ bool) \ 'a star \ 'b star \ bool"
(
‹(
‹open_block
notation=
‹prefix starP2
››*p2* _)
› [80] 80)
where "*p2* P = (\x y. unstar (star_of P \ x \ y))"
declare starP_def [transfer_unfold]
declare starP2_def [transfer_unfold]
lemma starP_star_n:
"( *p* P) (star_n X) = eventually (\n. P (X n)) \"
by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
lemma starP2_star_n:
"( *p2* P) (star_n X) (star_n Y) = (eventually (\n. P (X n) (Y n)) \)"
by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
lemma starP_star_of [simp]:
"( *p* P) (star_of x) = P x"
by transfer (rule refl)
lemma starP2_star_of [simp]:
"( *p2* P) (star_of x) = *p* P x"
by transfer (rule refl)
subsection ‹Internal sets
›
definition Iset ::
"'a set star \ 'a star set"
where "Iset A = {x. ( *p2* (\)) x A}"
lemma Iset_star_n:
"(star_n X \ Iset (star_n A)) = (eventually (\n. X n \ A n) \)"
by (simp add: Iset_def starP2_star_n)
text ‹Transfer tactic should remove occurrences of
🍋‹Iset
›.
›
setup ‹Transfer_Principle.add_const
🍋‹Iset
››
lemma transfer_mem [transfer_intro]:
"x \ star_n X \ a \ Iset (star_n A) \ x \ a \ eventually (\n. X n \ A n) \"
by (simp only: Iset_star_n)
lemma transfer_Collect [transfer_intro]:
"(\X. p (star_n X) \ eventually (\n. P n (X n)) \) \
Collect p
≡ Iset (star_n (λn. Collect (P n)))
"
by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n)
lemma transfer_set_eq [transfer_intro]:
"a \ Iset (star_n A) \ b \ Iset (star_n B) \ a = b \ eventually (\n. A n = B n) \"
by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem)
lemma transfer_ball [transfer_intro]:
"a \ Iset (star_n A) \ (\X. p (star_n X) \ eventually (\n. P n (X n)) \) \
∀x
∈a. p x
≡ eventually (λn.
∀x
∈A n. P n x)
U"
by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
lemma transfer_bex [transfer_intro]:
"a \ Iset (star_n A) \ (\X. p (star_n X) \ eventually (\n. P n (X n)) \) \
∃x
∈a. p x
≡ eventually (λn.
∃x
∈A n. P n x)
U"
by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
lemma transfer_Iset [transfer_intro]:
"a \ star_n A \ Iset a \ Iset (star_n (\n. A n))"
by simp
text ‹Nonstandard extensions of sets.
›
definition starset ::
"'a set \ 'a star set"
(
‹(
‹open_block
notation=
‹prefix starset
››*s* _)
› [80] 80)
where "starset A = Iset (star_of A)"
declare starset_def [transfer_unfold]
lemma starset_mem:
"star_of x \ *s* A \ x \ A"
by transfer (rule refl)
lemma starset_UNIV:
"*s* (UNIV::'a set) = (UNIV::'a star set)"
by (transfer UNIV_def) (rule refl)
lemma starset_empty:
"*s* {} = {}"
by (transfer empty_def) (rule refl)
lemma starset_insert:
"*s* (insert x A) = insert (star_of x) ( *s* A)"
by (transfer insert_def Un_def) (rule refl)
lemma starset_Un:
"*s* (A \ B) = *s* A \ *s* B"
by (transfer Un_def) (rule refl)
lemma starset_Int:
"*s* (A \ B) = *s* A \ *s* B"
by (transfer Int_def) (rule refl)
lemma starset_Compl:
"*s* -A = -( *s* A)"
by (transfer Compl_eq) (rule refl)
lemma starset_diff:
"*s* (A - B) = *s* A - *s* B"
by (transfer set_diff_eq) (rule refl)
lemma starset_image:
"*s* (f ` A) = ( *f* f) ` ( *s* A)"
by (transfer image_def) (rule refl)
lemma starset_vimage:
"*s* (f -` A) = ( *f* f) -` ( *s* A)"
by (transfer vimage_def) (rule refl)
lemma starset_subset:
"( *s* A \ *s* B) \ A \ B"
by (transfer subset_eq) (rule refl)
lemma starset_eq:
"( *s* A = *s* B) \ A = B"
by transfer (rule refl)
lemmas starset_simps [simp] =
starset_mem starset_UNIV
starset_empty starset_insert
starset_Un starset_Int
starset_Compl starset_diff
starset_image starset_vimage
starset_subset starset_eq
subsection ‹Syntactic
classes›
instantiation star :: (zero) zero
begin
definition star_zero_def:
"0 \ star_of 0"
instance ..
end
instantiation star :: (one) one
begin
definition star_one_def:
"1 \ star_of 1"
instance ..
end
instantiation star :: (plus) plus
begin
definition star_add_def:
"(+) \ *f2* (+)"
instance ..
end
instantiation star :: (times) times
begin
definition star_mult_def:
"((*)) \ *f2* ((*))"
instance ..
end
instantiation star :: (uminus) uminus
begin
definition star_minus_def:
"uminus \ *f* uminus"
instance ..
end
instantiation star :: (minus) minus
begin
definition star_diff_def:
"(-) \ *f2* (-)"
instance ..
end
instantiation star :: (abs) abs
begin
definition star_abs_def:
"abs \ *f* abs"
instance ..
end
instantiation star :: (sgn) sgn
begin
definition star_sgn_def:
"sgn \ *f* sgn"
instance ..
end
instantiation star :: (divide) divide
begin
definition star_divide_def:
"divide \ *f2* divide"
instance ..
end
instantiation star :: (inverse) inverse
begin
definition star_inverse_def:
"inverse \ *f* inverse"
instance ..
end
instance star :: (Rings.dvd) Rings.dvd ..
instantiation star :: (modulo) modulo
begin
definition star_mod_def:
"(mod) \ *f2* (mod)"
instance ..
end
instantiation star :: (ord) ord
begin
definition star_le_def:
"(\) \ *p2* (\)"
definition star_less_def:
"(<) \ *p2* (<)"
instance ..
end
lemmas star_class_defs [transfer_unfold] =
star_zero_def star_one_def
star_add_def star_diff_def star_minus_def
star_mult_def star_divide_def star_inverse_def
star_le_def star_less_def star_abs_def star_sgn_def
star_mod_def
text ‹Class operations preserve standard elements.
›
lemma Standard_zero:
"0 \ Standard"
by (simp add: star_zero_def)
lemma Standard_one:
"1 \ Standard"
by (simp add: star_one_def)
lemma Standard_add:
"x \ Standard \ y \ Standard \ x + y \ Standard"
by (simp add: star_add_def)
lemma Standard_diff:
"x \ Standard \ y \ Standard \ x - y \ Standard"
by (simp add: star_diff_def)
lemma Standard_minus:
"x \ Standard \ - x \ Standard"
by (simp add: star_minus_def)
lemma Standard_mult:
"x \ Standard \ y \ Standard \ x * y \ Standard"
by (simp add: star_mult_def)
lemma Standard_divide:
"x \ Standard \ y \ Standard \ x / y \ Standard"
by (simp add: star_divide_def)
lemma Standard_inverse:
"x \ Standard \ inverse x \ Standard"
by (simp add: star_inverse_def)
lemma Standard_abs:
"x \ Standard \ \x\ \ Standard"
by (simp add: star_abs_def)
lemma Standard_mod:
"x \ Standard \ y \ Standard \ x mod y \ Standard"
by (simp add: star_mod_def)
lemmas Standard_simps [simp] =
Standard_zero Standard_one
Standard_add Standard_diff Standard_minus
Standard_mult Standard_divide Standard_inverse
Standard_abs Standard_mod
text ‹🍋‹star_of
› preserves
class operations.
›
lemma star_of_add:
"star_of (x + y) = star_of x + star_of y"
by transfer (rule refl)
lemma star_of_diff:
"star_of (x - y) = star_of x - star_of y"
by transfer (rule refl)
lemma star_of_minus:
"star_of (-x) = - star_of x"
by transfer (rule refl)
lemma star_of_mult:
"star_of (x * y) = star_of x * star_of y"
by transfer (rule refl)
lemma star_of_divide:
"star_of (x / y) = star_of x / star_of y"
by transfer (rule refl)
lemma star_of_inverse:
"star_of (inverse x) = inverse (star_of x)"
by transfer (rule refl)
lemma star_of_mod:
"star_of (x mod y) = star_of x mod star_of y"
by transfer (rule refl)
lemma star_of_abs:
"star_of \x\ = \star_of x\"
by transfer (rule refl)
text ‹🍋‹star_of
› preserves numerals.
›
lemma star_of_zero:
"star_of 0 = 0"
by transfer (rule refl)
lemma star_of_one:
"star_of 1 = 1"
by transfer (rule refl)
text ‹🍋‹star_of
› preserves orderings.
›
lemma star_of_less:
"(star_of x < star_of y) = (x < y)"
by transfer (rule refl)
lemma star_of_le:
"(star_of x \ star_of y) = (x \ y)"
by transfer (rule refl)
lemma star_of_eq:
"(star_of x = star_of y) = (x = y)"
by transfer (rule refl)
text ‹As above,
for ‹0
›.
›
lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero]
lemmas star_of_0_eq = star_of_eq [of 0, simplified star_of_zero]
lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero]
lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero]
text ‹As above,
for ‹1
›.
›
lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one]
lemmas star_of_1_eq = star_of_eq [of 1, simplified star_of_one]
lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
lemmas star_of_le_1 = star_of_le [of _ 1, simplified star_of_one]
lemmas star_of_eq_1 = star_of_eq [of _ 1, simplified star_of_one]
lemmas star_of_simps [simp] =
star_of_add star_of_diff star_of_minus
star_of_mult star_of_divide star_of_inverse
star_of_mod star_of_abs
star_of_zero star_of_one
star_of_less star_of_le star_of_eq
star_of_0_less star_of_0_le star_of_0_eq
star_of_less_0 star_of_le_0 star_of_eq_0
star_of_1_less star_of_1_le star_of_1_eq
star_of_less_1 star_of_le_1 star_of_eq_1
subsection ‹Ordering
and lattice
classes›
instance star :: (order) order
proof
show "\x y::'a star. (x < y) = (x \ y \ \ y \ x)"
by transfer (rule less_le_not_le)
show "\x::'a star. x \ x"
by transfer (rule order_refl)
show "\x y z::'a star. \x \ y; y \ z\ \ x \ z"
by transfer (rule order_trans)
show "\x y::'a star. \x \ y; y \ x\ \ x = y"
by transfer (rule order_antisym)
qed
instantiation star :: (semilattice_inf) semilattice_inf
begin
definition star_inf_def [transfer_unfold]:
"inf \ *f2* inf"
instance by (standard; transfer) auto
end
instantiation star :: (semilattice_sup) semilattice_sup
begin
definition star_sup_def [transfer_unfold]:
"sup \ *f2* sup"
instance by (standard; transfer) auto
end
instance star :: (lattice) lattice ..
instance star :: (distrib_lattice) distrib_lattice
by (standard; transfer) (auto simp add: sup_inf_distrib1)
lemma Standard_inf [simp]:
"x \ Standard \ y \ Standard \ inf x y \ Standard"
by (simp add: star_inf_def)
lemma Standard_sup [simp]:
"x \ Standard \ y \ Standard \ sup x y \ Standard"
by (simp add: star_sup_def)
lemma star_of_inf [simp]:
"star_of (inf x y) = inf (star_of x) (star_of y)"
by transfer (rule refl)
lemma star_of_sup [simp]:
"star_of (sup x y) = sup (star_of x) (star_of y)"
by transfer (rule refl)
instance star :: (linorder) linorder
by (intro_classes, transfer, rule linorder_linear)
lemma star_max_def [transfer_unfold]:
"max = *f2* max"
unfolding max_def
by (intro ext, transfer, simp)
lemma star_min_def [transfer_unfold]:
"min = *f2* min"
unfolding min_def
by (intro ext, transfer, simp)
lemma Standard_max [simp]:
"x \ Standard \ y \ Standard \ max x y \ Standard"
by (simp add: star_max_def)
lemma Standard_min [simp]:
"x \ Standard \ y \ Standard \ min x y \ Standard"
by (simp add: star_min_def)
lemma star_of_max [simp]:
"star_of (max x y) = max (star_of x) (star_of y)"
by transfer (rule refl)
lemma star_of_min [simp]:
"star_of (min x y) = min (star_of x) (star_of y)"
by transfer (rule refl)
subsection ‹Ordered group
classes›
instance star :: (semigroup_add) semigroup_add
by (intro_classes, transfer, rule add.assoc)
instance star :: (ab_semigroup_add) ab_semigroup_add
by (intro_classes, transfer, rule add.commute)
instance star :: (semigroup_mult) semigroup_mult
by (intro_classes, transfer, rule mult.assoc)
instance star :: (ab_semigroup_mult) ab_semigroup_mult
by (intro_classes, transfer, rule mult.commute)
instance star :: (comm_monoid_add) comm_monoid_add
by (intro_classes, transfer, rule comm_monoid_add_class.add_0)
instance star :: (monoid_mult) monoid_mult
apply intro_classes
apply (transfer, rule mult_1_left)
apply (transfer, rule mult_1_right)
done
instance star :: (power) power ..
instance star :: (comm_monoid_mult) comm_monoid_mult
by (intro_classes, transfer, rule mult_1)
instance star :: (cancel_semigroup_add) cancel_semigroup_add
apply intro_classes
apply (transfer, erule add_left_imp_eq)
apply (transfer, erule add_right_imp_eq)
done
instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
by intro_classes (transfer, simp add: diff_diff_eq)+
instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
instance star :: (ab_group_add) ab_group_add
apply intro_classes
apply (transfer, rule left_minus)
apply (transfer, rule diff_conv_add_uminus)
done
instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add
by (intro_classes, transfer, rule add_left_mono)
instance star :: (ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
instance star :: (ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
by (intro_classes, transfer, rule add_le_imp_le_left)
instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add ..
instance star :: (ordered_ab_semigroup_monoid_add_imp_le) ordered_ab_semigroup_monoi
d_add_imp_le ..
instance star :: (ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
instance star :: (ordered_ab_group_add) ordered_ab_group_add ..
instance star :: (ordered_ab_group_add_abs) ordered_ab_group_add_abs
by intro_classes (transfer, simp add: abs_ge_self abs_leI abs_triangle_ineq)+
instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add ..
subsection ‹Ring and field classes›
instance star :: (semiring) semiring
by (intro_classes; transfer) (fact distrib_right distrib_left)+
instance star :: (semiring_0) semiring_0
by (intro_classes; transfer) simp_all
instance star :: (semiring_0_cancel) semiring_0_cancel ..
instance star :: (comm_semiring) comm_semiring
by (intro_classes; transfer) (fact distrib_right)
instance star :: (comm_semiring_0) comm_semiring_0 ..
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
instance star :: (zero_neq_one) zero_neq_one
by (intro_classes; transfer) (fact zero_neq_one)
instance star :: (semiring_1) semiring_1 ..
instance star :: (comm_semiring_1) comm_semiring_1 ..
declare dvd_def [transfer_refold]
instance star :: (comm_semiring_1_cancel) comm_semiring_1_cancel
by (intro_classes; transfer) (fact right_diff_distrib')
instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
by (intro_classes; transfer) (fact no_zero_divisors)
instance star :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..
instance star :: (semiring_no_zero_divisors_cancel) semiring_no_zero_divisors_cancel
by (intro_classes; transfer) simp_all
instance star :: (semiring_1_cancel) semiring_1_cancel ..
instance star :: (ring) ring ..
instance star :: (comm_ring) comm_ring ..
instance star :: (ring_1) ring_1 ..
instance star :: (comm_ring_1) comm_ring_1 ..
instance star :: (semidom) semidom ..
instance star :: (semidom_divide) semidom_divide
by (intro_classes; transfer) simp_all
instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
instance star :: (idom) idom ..
instance star :: (idom_divide) idom_divide ..
instance star :: (divide_trivial) divide_trivial
by (intro_classes; transfer) simp_all
instance star :: (division_ring) division_ring
by (intro_classes; transfer) (simp_all add: divide_inverse)
instance star :: (field) field
by (intro_classes; transfer) (simp_all add: divide_inverse)
instance star :: (ordered_semiring) ordered_semiring
by (intro_classes; transfer) (fact mult_left_mono mult_right_mono)+
instance star :: (ordered_cancel_semiring) ordered_cancel_semiring ..
instance star :: (linordered_semiring_strict) linordered_semiring_strict
by (intro_classes; transfer) (fact mult_strict_left_mono mult_strict_right_mono)+
instance star :: (ordered_comm_semiring) ordered_comm_semiring
by (intro_classes; transfer) (fact mult_left_mono)
instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
by (intro_classes; transfer) (fact mult_strict_left_mono)
instance star :: (ordered_ring) ordered_ring ..
instance star :: (ordered_ring_abs) ordered_ring_abs
by (intro_classes; transfer) (fact abs_eq_mult)
instance star :: (abs_if) abs_if
by (intro_classes; transfer) (fact abs_if)
instance star :: (linordered_ring_strict) linordered_ring_strict ..
instance star :: (ordered_comm_ring) ordered_comm_ring ..
instance star :: (linordered_semidom) linordered_semidom
by (intro_classes; transfer) (fact zero_less_one le_add_diff_inverse2)+
instance star :: (linordered_idom) linordered_idom
by (intro_classes; transfer) (fact sgn_if)
instance star :: (linordered_field) linordered_field ..
instance star :: (algebraic_semidom) algebraic_semidom ..
instantiation star :: (normalization_semidom) normalization_semidom
begin
definition unit_factor_star :: "'a star \ 'a star"
where [transfer_unfold]: "unit_factor_star = *f* unit_factor"
definition normalize_star :: "'a star \ 'a star"
where [transfer_unfold]: "normalize_star = *f* normalize"
instance
by standard (transfer; simp add: is_unit_unit_factor unit_factor_mult)+
end
instance star :: (semidom_modulo) semidom_modulo
by standard (transfer; simp)
subsection ‹Power›
lemma star_power_def [transfer_unfold]: "(^) \ \x n. ( *f* (\x. x ^ n)) x"
proof (rule eq_reflection, rule ext, rule ext)
show "x ^ n = ( *f* (\x. x ^ n)) x" for n :: nat and x :: "'a star"
proof (induct n arbitrary: x)
case 0
have "\x::'a star. ( *f* (\x. 1)) x = 1"
by transfer simp
then show ?case by simp
next
case (Suc n)
have "\x::'a star. x * ( *f* (\x::'a. x ^ n)) x = ( *f* (\x::'a. x * x ^ n)) x"
by transfer simp
with Suc show ?case by simp
qed
qed
lemma Standard_power [simp]: "x \ Standard \ x ^ n \ Standard"
by (simp add: star_power_def)
lemma star_of_power [simp]: "star_of (x ^ n) = star_of x ^ n"
by transfer (rule refl)
subsection ‹Number classes›
instance star :: (numeral) numeral ..
lemma star_numeral_def [transfer_unfold]: "numeral k = star_of (numeral k)"
by (induct k) (simp_all only: numeral.simps star_of_one star_of_add)
lemma Standard_numeral [simp]: "numeral k \ Standard"
by (simp add: star_numeral_def)
lemma star_of_numeral [simp]: "star_of (numeral k) = numeral k"
by transfer (rule refl)
lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
by (induct n) simp_all
lemmas star_of_compare_numeral [simp] =
star_of_less [of "numeral k", simplified star_of_numeral]
star_of_le [of "numeral k", simplified star_of_numeral]
star_of_eq [of "numeral k", simplified star_of_numeral]
star_of_less [of _ "numeral k", simplified star_of_numeral]
star_of_le [of _ "numeral k", simplified star_of_numeral]
star_of_eq [of _ "numeral k", simplified star_of_numeral]
star_of_less [of "- numeral k", simplified star_of_numeral]
star_of_le [of "- numeral k", simplified star_of_numeral]
star_of_eq [of "- numeral k", simplified star_of_numeral]
star_of_less [of _ "- numeral k", simplified star_of_numeral]
star_of_le [of _ "- numeral k", simplified star_of_numeral]
star_of_eq [of _ "- numeral k", simplified star_of_numeral] for k
lemma Standard_of_nat [simp]: "of_nat n \ Standard"
by (simp add: star_of_nat_def)
lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
by transfer (rule refl)
lemma star_of_int_def [transfer_unfold]: "of_int z = star_of (of_int z)"
by (rule int_diff_cases [of z]) simp
lemma Standard_of_int [simp]: "of_int z \ Standard"
by (simp add: star_of_int_def)
lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
by transfer (rule refl)
instance star :: (semiring_char_0) semiring_char_0
proof
have "inj (star_of :: 'a \ 'a star)"
by (rule injI) simp
then have "inj (star_of \ of_nat :: nat \ 'a star)"
using inj_of_nat by (rule inj_compose)
then show "inj (of_nat :: nat \ 'a star)"
by (simp add: comp_def)
qed
instance star :: (ring_char_0) ring_char_0 ..
subsection ‹Finite class›
lemma starset_finite: "finite A \ *s* A = star_of ` A"
by (erule finite_induct) simp_all
instance star :: (finite) finite
proof intro_classes
show "finite (UNIV::'a star set)"
by (metis starset_UNIV finite finite_imageI starset_finite)
qed
end
