Theory InternalSet

header {* Internal Sets *}

theory InternalSet
imports Omega
begin

subsection {* Properties of @{term Iset} *}

lemma Iset_empty: "Iset (star_of {}) = {}"
by (transfer empty_def) (rule refl)

lemma Iset_UNIV: "Iset (star_of UNIV) = UNIV"
by (transfer UNIV_def) (rule refl)

lemma Iset_insert:
"!!a A. insert a (Iset A) = Iset (Ifun2_of insert a A)"
by (unfold insert_def Un_def, transfer, fold insert_def Un_def, simp)

lemma Iset_Un:
"!!A B. Iset A ∪ Iset B = Iset (Ifun2_of (op ∪) A B)"
by (unfold Un_def, transfer, fold Un_def, simp)

lemma Iset_Int:
"!!A B. Iset A ∩ Iset B = Iset (Ifun2_of (op ∩) A B)"
by (unfold Int_def, transfer, fold Int_def, simp)

lemma Iset_UNION:
"!!A B. (\<Union>x∈Iset A. Iset (B ∗ x)) = Iset (Ifun2_of UNION A B)"
by (unfold UNION_def Bex_def, transfer, fold Bex_def UNION_def, simp)

lemma Iset_INTER:
"!!A B. (\<Inter>x∈Iset A. Iset (B ∗ x)) = Iset (Ifun2_of INTER A B)"
by (unfold INTER_def Ball_def, transfer, fold Ball_def INTER_def, simp)

lemma Iset_mem:
"!!x A. (x ∈ Iset A) = (Ipred2_of (op ∈) x A)"
by transfer simp

lemma Iset_subset:
"!!A B. (Iset A ⊆ Iset B) = Ipred2_of (op ⊆) A B"
by (unfold subset_def Ball_def, transfer, fold subset_def Ball_def, simp)

lemma Iset_diff:
"!!A B. (Iset A - Iset B) = Iset (Ifun2_of (op -) A B)"
by (unfold set_diff_def, transfer, fold set_diff_def, simp)

lemma Iset_Compl:
"!!A. (- Iset A) = Iset (Ifun_of uminus A)"
by (unfold Compl_def, transfer, fold Compl_def, simp)

lemma Iset_image:
"!!A f. Ifun f ` Iset A = Iset (Ifun2_of (op `) f A)"
by (unfold image_def Bex_def, transfer, fold image_def Bex_def, simp)


subsection {* Properties of @{term Iset_of} *}

lemma Iset_of [simp]:
"(star_of x ∈ Iset_of A) = (x ∈ A)"
by transfer simp

lemma Iset_of_inject: "(Iset_of A = Iset_of B) = (A = B)"
by transfer simp

lemma Iset_of_empty: "Iset_of {} = {}"
by (transfer empty_def) (rule refl)

lemma Iset_of_UNIV: "Iset_of UNIV = UNIV"
by (transfer UNIV_def) (rule refl)

lemma Iset_of_insert:
"Iset_of (insert x A) = insert (star_of x) (Iset_of A)"
by (transfer insert_def Un_def) (rule refl)

lemma Iset_of_Un: "Iset_of (A ∪ B) = Iset_of A ∪ Iset_of B"
by (transfer Un_def) (rule refl)

lemma Iset_of_Int: "Iset_of (A ∩ B) = Iset_of A ∩ Iset_of B"
by (transfer Int_def) (rule refl)

lemma Iset_of_diff: "Iset_of (A - B) = Iset_of A - Iset_of B"
by (transfer set_diff_def) (rule refl)

lemma Iset_of_Compl: "Iset_of (-A) = - Iset_of A"
by (transfer Compl_def) (rule refl)

lemma Iset_of_subset: "(Iset_of A ⊆ Iset_of B) = (A ⊆ B)"
by (transfer subset_def Ball_def) (rule refl)

lemma Iset_of_UNION:
"Iset_of (UNION A B) = (\<Union>x∈Iset_of A. Iset (Ifun_of B x))"
by (transfer UNION_def Bex_def) (rule refl)

lemma Iset_of_INTER:
"Iset_of (INTER A B) = (\<Inter>x∈Iset_of A. Iset (Ifun_of B x))"
by (transfer INTER_def Ball_def) (rule refl)

lemma Iset_of_image:
"Iset_of (f ` A) = Ifun_of f ` Iset_of A"
by (transfer image_def Bex_def) (rule refl)


subsection {* Finite internal sets *}

lemma finite_Iset_of: "finite A ==> Iset_of A = star_of ` A"
 apply (erule finite_induct)
  apply (simp add: Iset_of_empty)
 apply (simp add: Iset_of_insert)
done

lemma star_of_subset_Iset_of: "star_of ` A ⊆ Iset_of A"
by auto

lemma "Iset_of A ∩ range star_of = star_of ` A"
by auto

lemma infinite_Iset_of:
assumes "infinite (A::'a set)"
shows "∃x∈Iset_of A. nonstandard x"
proof -
  have "∃f::nat => 'a. inj f ∧ range f ⊆ A"
    by (rule infinite_countable_subset)
  then obtain f::"nat => 'a"
    where inj: "inj f" and sub: "range f ⊆ A" by fast
  show "∃x∈Iset_of A. nonstandard x"
  proof
    from inj nonstandard_infnat
    show "nonstandard (Ifun_of f infnat)"
      by (rule nonstandard_Ifun_of)
  next
    from sub have "!!x. f x ∈ A" by fast
    thus "!!x. Ifun_of f x ∈ Iset_of A" by transfer simp
  qed
qed

lemma "(Iset_of A = star_of ` A) = finite A"
 apply (case_tac "finite A")
  apply (simp add: finite_Iset_of)
 apply simp
 apply (drule infinite_Iset_of)
 apply (auto simp add: nonstandard_def)
done

instance star :: (finite) finite
proof
  let ?U = "UNIV :: 'a set"
  from finite have A: "finite ?U" .
  hence "finite (star_of ` ?U)" by (rule finite_imageI)
  also note finite_Iset_of [OF A, symmetric]
  also note Iset_of_UNIV
  finally show "finite (UNIV :: 'a star set)" .
qed

end