# Theory StarDef

```(*  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"  (‹𝒰›)
where "𝒰 = (SOME U. freeultrafilter U)"

lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter 𝒰"
unfolding FreeUltrafilterNat_def

interpretation FreeUltrafilterNat: freeultrafilter 𝒰
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 \<^term>‹starrel› is an equivalence relation.›

lemma starrel_iff [iff]: "(X, Y) ∈ starrel ⟷ eventually (λn. X n = Y n) 𝒰"

lemma equiv_starrel: "equiv UNIV starrel"
proof (rule equivI)
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"

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"

text ‹Standard principles that play a central role in the transfer tactic.›
definition Ifun :: "('a ⇒ 'b) star ⇒ 'a star ⇒ 'b star" (‹(_ ⋆/ _)› [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) 𝒰"
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) 𝒰"
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) 𝒰"

subsection ‹Standard elements›

definition Standard :: "'a star set"
where "Standard = range star_of"

text ‹Transfer tactic should remove occurrences of \<^term>‹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"

subsection ‹Internal functions›

text ‹Transfer tactic should remove occurrences of \<^term>‹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"

text ‹Nonstandard extensions of functions.›

definition starfun :: "('a ⇒ 'b) ⇒ 'a star ⇒ 'b star"  (‹*f* _› [80] 80)
where "starfun f ≡ λx. star_of f ⋆ x"

definition starfun2 :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a star ⇒ 'b star ⇒ 'c star"  (‹*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"

lemma Standard_starfun2 [simp]: "x ∈ Standard ⟹ y ∈ Standard ⟹ starfun2 f x y ∈ Standard"

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"

text ‹Transfer tactic should remove occurrences of \<^term>‹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"  (‹*p* _› [80] 80)
where "*p* P = (λx. unstar (star_of P ⋆ x))"

definition starP2 :: "('a ⇒ 'b ⇒ bool) ⇒ 'a star ⇒ 'b star ⇒ bool"  (‹*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) 𝒰)"

text ‹Transfer tactic should remove occurrences of \<^term>‹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) 𝒰"
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) 𝒰"
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" (‹*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_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"

lemma Standard_one: "1 ∈ Standard"

lemma Standard_add: "x ∈ Standard ⟹ y ∈ Standard ⟹ x + y ∈ Standard"

lemma Standard_diff: "x ∈ Standard ⟹ y ∈ Standard ⟹ x - y ∈ Standard"

lemma Standard_minus: "x ∈ Standard ⟹ - x ∈ Standard"

lemma Standard_mult: "x ∈ Standard ⟹ y ∈ Standard ⟹ x * y ∈ Standard"

lemma Standard_divide: "x ∈ Standard ⟹ y ∈ Standard ⟹ x / y ∈ Standard"

lemma Standard_inverse: "x ∈ Standard ⟹ inverse x ∈ Standard"

lemma Standard_abs: "x ∈ Standard ⟹ ¦x¦ ∈ Standard"

lemma Standard_mod: "x ∈ Standard ⟹ y ∈ Standard ⟹ x mod y ∈ Standard"

lemmas Standard_simps [simp] =
Standard_zero  Standard_one
Standard_mult  Standard_divide  Standard_inverse
Standard_abs   Standard_mod

text ‹\<^term>‹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 ‹\<^term>‹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 ‹\<^term>‹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_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"

lemma Standard_sup [simp]: "x ∈ Standard ⟹ y ∈ Standard ⟹ sup x y ∈ Standard"

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"

lemma Standard_min [simp]: "x ∈ Standard ⟹ y ∈ Standard ⟹ min x y ∈ Standard"

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_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 :: (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)

apply intro_classes
done

by intro_classes (transfer, simp add: diff_diff_eq)+

apply intro_classes
apply (transfer, rule left_minus)
done

by intro_classes (transfer, simp add: abs_ge_self abs_leI abs_triangle_ineq)+

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 :: (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"

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"

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"

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"

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)"
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
```