Theory Omega

header {* Omega *}

theory Omega
imports StarClasses HypNat
begin

subsection {* An infinite natural number *}

constdefs
  infnat :: "nat star"
  "infnat ≡ SOME x. nonstandard x"

lemma nonstandard_infnat: "nonstandard infnat"
by (unfold infnat_def, rule ex_nonstandard_nat [THEN someI_ex])

lemma infnat_neq_star_of: "infnat ≠ star_of n"
by (rule nonstandard_infnat [THEN nonstandardD])

lemma star_of_neq_infnat: "star_of n ≠ infnat"
by (rule infnat_neq_star_of [symmetric])

lemma infnat_neq_0 [simp]: "infnat ≠ 0"
by (cut_tac infnat_neq_star_of[of 0], simp)

lemma infnat_neq_1 [simp]: "infnat ≠ 1"
by (cut_tac infnat_neq_star_of[of 1], simp del: One_nat_def)

lemma less_nonstandard_nat:
assumes "nonstandard k"
shows "star_of (n::nat) < k"
proof (induct n)
  have "star_of 0 ≠ k" by (rule nonstandardD [symmetric])
  thus "star_of 0 < k" by simp
next
  case (Suc n)
  have Suc_lessI':
    "!!k. [|star_of n < k; star_of (Suc n) ≠ k|] ==> star_of (Suc n) < k"
    by transfer (rule Suc_lessI)
  have "star_of (Suc n) ≠ k" by (rule nonstandardD [symmetric])
  with Suc show "star_of (Suc n) < k" by (rule Suc_lessI')
qed

lemma star_of_less_infnat: "star_of n < infnat"
by (rule nonstandard_infnat [THEN less_nonstandard_nat])


subsection {* Omega *}

constdefs
  omega :: "'a::ordered_semidom star"
  "omega ≡ Ifun_of of_nat infnat"

syntax (xsymbols)    omega :: "'a star"  ("ω")
syntax (HTML output) omega :: "'a star"  ("ω")

lemma nonstandard_Ifun_of:
assumes inj: "inj f" and ns: "nonstandard x"
shows "nonstandard (Ifun_of f x)"
proof (rule nonstandardI)
  fix a show "Ifun_of f x ≠ star_of a"
  proof (cases)
    assume "a ∈ range f"
    then obtain b where [simp]: "a = f b" ..
    from inj have inj': "inj (Ifun_of f)" by (transfer inj_def)
    from ns have "x ≠ star_of b" by (rule nonstandardD)
    hence "Ifun_of f x ≠ Ifun_of f (star_of b)"
      by (subst inj' [THEN inj_eq])
    thus "Ifun_of f x ≠ star_of a" by simp
  next
    assume "a ∉ range f"
    hence "∀b. f b ≠ a" by fast
    hence "∀b. Ifun_of f b ≠ star_of a" by transfer
    thus "Ifun_of f x ≠ star_of a" ..
  qed
qed

lemma less_Ifun_of_of_natI:
  "!!n::nat star. star_of m < n
   ==> (of_nat m::'a::ordered_semidom star) < Ifun_of of_nat n"
by (transfer star_of_nat_def) (rule less_imp_of_nat_less)

lemma of_nat_less_omega: "of_nat n < ω"
 apply (unfold omega_def)
 apply (rule less_Ifun_of_of_natI)
 apply (rule star_of_less_infnat)
done

lemma zero_less_omega [simp]: "0 < ω"
by (cut_tac of_nat_less_omega [of 0], simp)

lemma one_less_omega [simp]: "1 < ω"
by (cut_tac of_nat_less_omega [of 1], simp)

lemma omega_neq_of_nat: "ω ≠ of_nat n"
by (simp add: order_less_imp_not_eq2 of_nat_less_omega)

lemma omega_not_zero [simp]: "ω ≠ 0"
by (cut_tac omega_neq_of_nat [of 0], simp)

lemma omega_not_one [simp]: "ω ≠ 1"
by (cut_tac omega_neq_of_nat [of 1], simp)

lemma omega_not_mem_Nats: "ω ∉ Nats"
by (simp add: Nats_def image_def omega_neq_of_nat)

lemma nonstandard_omega: "nonstandard ω"
 apply (unfold omega_def)
 apply (rule nonstandard_Ifun_of)
  apply (simp add: inj_on_def)
 apply (rule nonstandard_infnat)
done

lemma omega_neq_star_of: "ω ≠ star_of n"
by (rule nonstandard_omega [THEN nonstandardD])

lemma star_of_neq_omega: "star_of n ≠ ω"
by (rule omega_neq_star_of [symmetric])


subsection {* Epsilon *}

constdefs
  epsilon :: "'a::ordered_field star"
  "epsilon ≡ inverse omega"

syntax (xsymbols)    epsilon :: "'a star"  ("ε")
syntax (HTML output) epsilon :: "'a star"  ("ε")

lemma inverse_epsilon: "inverse ε = ω"
by (unfold epsilon_def, rule nonzero_inverse_inverse_eq [OF omega_not_zero])

lemma epsilon_times_omega: "ε * ω = 1"
by (simp add: epsilon_def)

lemma omega_times_epsilon: "ω * ε = 1"
by (simp add: epsilon_def)

lemma zero_less_epsilon: "0 < ε"
by (simp add: epsilon_def positive_imp_inverse_positive)

lemma epsilon_neq_star_of: "ε ≠ star_of x"
proof
  assume "ε = star_of x"
  hence "inverse ε = star_of (inverse x)" by simp
  hence "ω = star_of (inverse x)" by (simp add: inverse_epsilon)
  thus "False" by (simp only: omega_neq_star_of)
qed

lemma nonstandard_epsilon: "nonstandard ε"
by (rule epsilon_neq_star_of [THEN nonstandardI])

end