Theory StarType

(*  Title       : HOL/Real/Hyperreal/HyperDef.thy
    ID          : $Id: HyperDef.thy,v 1.29 2004/04/14 12:13:06 kleing Exp $
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    Generalization and additions by Brian Huffman, 2005
*)

header{*Construction of Star Types Using Ultrafilters*}

theory StarType
imports FreeUltrafilter
begin

subsection {* A Free Ultrafilter over the Naturals *}

constdefs
  FreeUltrafilterNat :: "nat set set"  ("\<U>")
    "\<U> ≡ SOME U. FreeUltrafilter U"

lemma FreeUltrafilter_FUFNat: "FreeUltrafilter \<U>"
 apply (unfold FreeUltrafilterNat_def)
 apply (rule someI_ex)
 apply (rule FreeUltrafilter_Ex)
 apply (rule nat_infinite)
done

lemmas Ultrafilter_FUFNat =
  FreeUltrafilter_FUFNat [THEN FreeUltrafilter.Ultrafilter]

lemmas Filter_FUFNat =
  FreeUltrafilter_FUFNat [THEN FreeUltrafilter.Filter]

lemmas FUFNat_empty [iff] =
  Filter_FUFNat [THEN Filter.empty]

lemmas FUFNat_UNIV [iff] =
  Filter_FUFNat [THEN Filter.UNIV]

text {* This rule takes the place of the old ultra tactic *}

lemma ultra:
  "[|{n. P n} ∈ \<U>; {n. P n --> Q n} ∈ \<U>|] ==> {n. Q n} ∈ \<U>"
by (simp add: Collect_imp_eq
    Ultrafilter_FUFNat [THEN Ultrafilter.Un_iff]
    Ultrafilter_FUFNat [THEN Ultrafilter.Compl_iff])


subsection {* Definition of @{text star} type constructor *}

constdefs
  starrel :: "((nat => 'a) × (nat => 'a)) set"
    "starrel ≡ {(X,Y). {n. X n = Y n} ∈ \<U>}"

typedef (Star) 'a star = "(UNIV::(nat => 'a) set)//starrel"
by (auto intro: quotientI)

text {* Proving that @{term starrel} is an equivalence relation *}

lemma starrel_iff [iff]: "((X,Y) ∈ starrel) = ({n. X n = Y n} ∈ \<U>)"
by (simp add: starrel_def)

lemma equiv_starrel: "equiv UNIV starrel"
proof (rule equiv.intro)
  show "reflexive starrel" by (simp add: refl_def)
  show "sym starrel" by (simp add: sym_def eq_commute)
  show "trans starrel" by (auto intro: transI elim!: ultra)
qed

lemmas equiv_starrel_iff =
  eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I]
  -- {* @{term "(starrel `` {x} = starrel `` {y}) = ((x,y) ∈ starrel)"} *}

lemma starrel_in_Star: "starrel``{x} ∈ Star"
by (simp add: Star_def starrel_def quotient_def, fast)

lemma eq_Abs_Star:
  "(!!x. z = Abs_Star(starrel``{x}) ==> P) ==> P"
 apply (rule_tac x=z in Abs_Star_cases)
 apply (unfold Star_def)
 apply (erule quotientE)
 apply simp
done


subsection {* Constructors for type @{typ "'a star"} *}

constdefs
  star_n :: "(nat => 'a) => 'a star"  (binder "STAR " 10)
  "star_n X ≡ Abs_Star (starrel `` {X})"

  star_of :: "'a => 'a star"
  "star_of x ≡ STAR n. x"

theorem star_cases:
  "(!!X. x = star_n X ==> P) ==> P"
by (unfold star_n_def, rule eq_Abs_Star[of x], blast)

lemma all_star_eq: "(∀x. P x) = (∀X. P (star_n X))"
by (auto, rule_tac x=x in star_cases, simp)

lemma ex_star_eq: "(∃x. P x) = (∃X. P (star_n X))"
by (auto, rule_tac x=x in star_cases, auto)

lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} ∈ \<U>)"
 apply (unfold star_n_def)
 apply (simp add: Abs_Star_inject starrel_in_Star equiv_starrel_iff)
done

lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
by (simp add: star_of_def star_n_eq_iff)


subsection {* Existence of a nonstandard natural number *}

constdefs
  nonstandard :: "'a star => bool"
  "nonstandard x ≡ ∀a. x ≠ star_of a"

lemma nonstandardI: "(!!a. x ≠ star_of a) ==> nonstandard x"
by (simp add: nonstandard_def)

lemma nonstandardD: "nonstandard x ==> x ≠ star_of a"
by (simp add: nonstandard_def)

lemma ex_nonstandard_nat: "∃x::nat star. nonstandard x"
proof
  have "!!n. {n} ∉ \<U>"
    by (simp add: FreeUltrafilter_FUFNat [THEN FreeUltrafilter.finite])
  hence "!!n. star_n id ≠ star_of n"
    by (simp add: star_of_def star_n_eq_iff)
  thus "nonstandard (star_n id)" by (rule nonstandardI)
qed


subsection {* Internal functions *}

constdefs
  Ifun :: "('a => 'b) star => 'a star => 'b star"
  "Ifun f ≡ λx. Abs_Star
       (\<Union>F∈Rep_Star f. \<Union>X∈Rep_Star x. starrel``{λn. F n (X n)})"

syntax "@Ifun" :: "('a => 'b) star => 'a star => 'b star" (infixl "∗" 300)
translations "f ∗ x" \<rightleftharpoons> "Ifun f x"

lemma Ifun_star_n: "star_n F ∗ star_n X = (STAR n. F n (X n))"
 apply (unfold Ifun_def star_n_def)
 apply (simp add: Abs_Star_inverse starrel_in_Star)
 apply (rule_tac f=Abs_Star in arg_cong)
 apply safe
  apply (erule ultra)+
  apply simp
 apply force
done

lemma Ifun [simp]: "star_of f ∗ star_of x = star_of (f x)"
by (simp only: star_of_def Ifun_star_n)


subsection {* Testing lifted booleans *}

constdefs
  Ibool :: "bool star => bool"
  "Ibool b ≡ b = star_of True"

lemma Ibool_star_n: "Ibool (star_n P) = ({n. P n} ∈ \<U>)"
by (simp add: Ibool_def star_of_def star_n_eq_iff)

lemma Ibool [simp]: "Ibool (star_of p) = p"
by (simp add: Ibool_def star_of_inject)


subsection {* Internal functions and predicates *}

constdefs
  Ifun_of :: "('a => 'b) => ('a star => 'b star)"
  "Ifun_of f ≡ Ifun (star_of f)"

  Ifun2 :: "('a => 'b => 'c) star => ('a star => 'b star => 'c star)"
  "Ifun2 f ≡ λx y. f ∗ x ∗ y"

  Ifun2_of :: "('a => 'b => 'c) => ('a star => 'b star => 'c star)"
  "Ifun2_of f ≡ λx y. star_of f ∗ x ∗ y"

  Ipred :: "('a => bool) star => ('a star => bool)"
  "Ipred P ≡ λx. Ibool (P ∗ x)"

  Ipred_of :: "('a => bool) => ('a star => bool)"
  "Ipred_of P ≡ λx. Ibool (star_of P ∗ x)"

  Ipred2 :: "('a => 'b => bool) star => ('a star => 'b star => bool)"
  "Ipred2 P ≡ λx y. Ibool (P ∗ x ∗ y)"

  Ipred2_of :: "('a => 'b => bool) => ('a star => 'b star => bool)"
  "Ipred2_of P ≡ λx y. Ibool (star_of P ∗ x ∗ y)"

lemma Ifun_of [simp]:
  "Ifun_of f (star_of x) = star_of (f x)"
by (simp only: Ifun_of_def Ifun)

lemma Ifun2_of [simp]:
  "Ifun2_of f (star_of x) (star_of y) = star_of (f x y)"
by (simp only: Ifun2_of_def Ifun)

lemma Ipred_of [simp]:
  "Ipred_of P (star_of x) = P x"
by (simp only: Ipred_of_def Ifun Ibool)

lemma Ipred2_of [simp]:
  "Ipred2_of P (star_of x) (star_of y) = P x y"
by (simp only: Ipred2_of_def Ifun Ibool)

lemmas Ifun_defs =
  star_of_def Ifun_of_def Ifun2_def Ifun2_of_def
  Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def


subsection {* Internal sets *}

constdefs
  Iset :: "'a set star => 'a star set"
  "Iset A ≡ {x. Ipred2_of (op ∈) x A}"

  Iset_of :: "'a set => 'a star set"
  "Iset_of A ≡ Iset (star_of A)"

lemma Iset_star_n:
  "(star_n X ∈ Iset (star_n A)) = ({n. X n ∈ A n} ∈ \<U>)"
by (simp add: Iset_def Ipred2_of_def star_of_def Ifun_star_n Ibool_star_n)


subsection {* Class constants *}

instance star :: (ord) ord ..
instance star :: (zero) zero ..
instance star :: (one) one ..
instance star :: (plus) plus ..
instance star :: (times) times ..
instance star :: (minus) minus ..
instance star :: (inverse) inverse ..
instance star :: (number) number ..
instance star :: ("Divides.div") "Divides.div" ..
instance star :: (power) power ..

defs (overloaded)
  star_zero_def:    "0 ≡ star_of 0"
  star_one_def:     "1 ≡ star_of 1"
  star_number_def:  "number_of b ≡ star_of (number_of b)"
  star_add_def:     "(op +) ≡ Ifun2_of (op +)"
  star_diff_def:    "(op -) ≡ Ifun2_of (op -)"
  star_minus_def:   "uminus ≡ Ifun_of uminus"
  star_mult_def:    "(op *) ≡ Ifun2_of (op *)"
  star_divide_def:  "(op /) ≡ Ifun2_of (op /)"
  star_inverse_def: "inverse ≡ Ifun_of inverse"
  star_le_def:      "(op ≤) ≡ Ipred2_of (op ≤)"
  star_less_def:    "(op <) ≡ Ipred2_of (op <)"
  star_abs_def:     "abs ≡ Ifun_of abs"
  star_div_def:     "(op div) ≡ Ifun2_of (op div)"
  star_mod_def:     "(op mod) ≡ Ifun2_of (op mod)"
  star_power_def:   "(op ^) ≡ λx n. Ifun2_of (op ^) x (star_of n)"

lemmas star_class_defs =
  star_zero_def     star_one_def      star_number_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_div_def      star_mod_def      star_power_def

text {* @{term star_of} preserves class operations *}

lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
by (simp add: star_add_def)

lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
by (simp add: star_diff_def)

lemma star_of_minus: "star_of (-x) = - star_of x"
by (simp add: star_minus_def)

lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
by (simp add: star_mult_def)

lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
by (simp add: star_divide_def)

lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
by (simp add: star_inverse_def)

lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
by (simp add: star_div_def)

lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
by (simp add: star_mod_def)

lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
by (simp add: star_power_def)

lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
by (simp add: star_abs_def)

text {* @{term star_of} preserves numerals *}

lemma star_of_zero: "star_of 0 = 0"
by (simp add: star_zero_def)

lemma star_of_one: "star_of 1 = 1"
by (simp add: star_one_def)

lemma star_of_number_of: "star_of (number_of x) = number_of x"
by (simp add: star_number_def)

text {* @{term star_of} preserves orderings *}

lemma star_of_less: "(star_of x < star_of y) = (x < y)"
by (simp add: star_less_def)

lemma star_of_le: "(star_of x ≤ star_of y) = (x ≤ y)"
by (simp add: star_le_def)

lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
by (rule star_of_inject)

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 =
  star_of_add     star_of_diff    star_of_minus
  star_of_mult    star_of_divide  star_of_inverse
  star_of_div     star_of_mod
  star_of_power   star_of_abs
  star_of_zero    star_of_one     star_of_number_of
  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

declare star_of_simps [simp]

end