Quelle Zet.thy Sprache: Isabelle

(*  Title:      HOL/ZF/Zet.thy
    Author:     Steven Obua

    Introduces a type 'a zet of ZF representable sets.
    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
*)

theory Zet
imports HOLZF
begin

definition "zet = {A :: 'a set | A f z. inj_on f A \ f ` A \ explode z}"

typedef 'a zet = "zet :: 'a set set"
  unfolding zet_def by blast

definition zin :: "'a \ 'a zet \ bool" where
  "zin x A == x \ (Rep_zet A)"

lemma zet_ext_eq: "(A = B) = (\x. zin x A = zin x B)"
  by (auto simp add: Rep_zet_inject[symmetric] zin_def)

definition zimage :: "('a \ 'b) \ 'a zet \ 'b zet" where
  "zimage f A == Abs_zet (image f (Rep_zet A))"

lemma zet_def': "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A = explode z}"
  apply (rule set_eqI)
  apply (auto simp add: zet_def)
  apply (rule_tac x=f in exI)
  apply auto
  apply (rule_tac x="Sep z (\ y. y \ (f ` x))" in exI)
  apply (auto simp add: explode_def Sep)
  done

lemma image_zet_rep: "A \ zet \ \z . g ` A = explode z"
  apply (auto simp add: zet_def')
  apply (rule_tac x="Repl z (g o (inv_into A f))" in exI)
  apply (simp add: explode_Repl_eq)
  apply (subgoal_tac "explode z = f ` A")
  apply (simp_all add: image_image cong: image_cong_simp)
  done

lemma zet_image_mem:
  assumes Azet: "A \ zet"
  shows "g ` A \ zet"
proof -
  from Azet have "\(f :: _ \ ZF). inj_on f A"
    by (auto simp add: zet_def')
  then obtain f where injf: "inj_on (f :: _ \ ZF) A"
    by auto
  let ?w = "f o (inv_into A g)"
  have subset: "(inv_into A g) ` (g ` A) \ A"
    by (auto simp add: inv_into_into)
  have "inj_on (inv_into A g) (g ` A)" by (simp add: inj_on_inv_into)
  then have injw: "inj_on ?w (g ` A)"
    apply (rule comp_inj_on)
    apply (rule inj_on_subset[where A=A])
    apply (auto simp add: subset injf)
    done
  show ?thesis
    apply (simp add: zet_def' image_comp)
    apply (rule exI[where x="?w"])
    apply (simp add: injw image_zet_rep Azet)
    done
qed

lemma Rep_zimage_eq: "Rep_zet (zimage f A) = image f (Rep_zet A)"
  apply (simp add: zimage_def)
  apply (subst Abs_zet_inverse)
  apply (simp_all add: Rep_zet zet_image_mem)
  done

lemma zimage_iff: "zin y (zimage f A) = (\x. zin x A \ y = f x)"
  by (auto simp add: zin_def Rep_zimage_eq)

definition zimplode :: "ZF zet \ ZF" where
  "zimplode A == implode (Rep_zet A)"

definition zexplode :: "ZF \ ZF zet" where
  "zexplode z == Abs_zet (explode z)"

lemma Rep_zet_eq_explode: "\z. Rep_zet A = explode z"
  by (rule image_zet_rep[where g="\ x. x",OF Rep_zet, simplified])

lemma zexplode_zimplode: "zexplode (zimplode A) = A"
  apply (simp add: zimplode_def zexplode_def)
  apply (simp add: implode_def)
  apply (subst f_inv_into_f[where y="Rep_zet A"])
  apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
  done

lemma explode_mem_zet: "explode z \ zet"
  apply (simp add: zet_def')
  apply (rule_tac x="% x. x" in exI)
  apply (auto simp add: inj_on_def)
  done

lemma zimplode_zexplode: "zimplode (zexplode z) = z"
  apply (simp add: zimplode_def zexplode_def)
  apply (subst Abs_zet_inverse)
  apply (auto simp add: explode_mem_zet)
  done

lemma zin_zexplode_eq: "zin x (zexplode A) = Elem x A"
  apply (simp add: zin_def zexplode_def)
  apply (subst Abs_zet_inverse)
  apply (simp_all add: explode_Elem explode_mem_zet)
  done

lemma comp_zimage_eq: "zimage g (zimage f A) = zimage (g o f) A"
  apply (simp add: zimage_def)
  apply (subst Abs_zet_inverse)
  apply (simp_all add: image_comp zet_image_mem Rep_zet)
  done

definition zunion :: "'a zet \ 'a zet \ 'a zet" where
  "zunion a b \ Abs_zet ((Rep_zet a) \ (Rep_zet b))"

definition zsubset :: "'a zet \ 'a zet \ bool" where
  "zsubset a b \ \x. zin x a \ zin x b"

lemma explode_union: "explode (union a b) = (explode a) \ (explode b)"
  apply (rule set_eqI)
  apply (simp add: explode_def union)
  done

lemma Rep_zet_zunion: "Rep_zet (zunion a b) = (Rep_zet a) \ (Rep_zet b)"
proof -
  from Rep_zet[of a] have "\f z. inj_on f (Rep_zet a) \ f ` (Rep_zet a) = explode z"
    by (auto simp add: zet_def')
  then obtain fa za where a:"inj_on fa (Rep_zet a) \ fa ` (Rep_zet a) = explode za"
    by blast
  from a have fa: "inj_on fa (Rep_zet a)" by blast
  from a have za: "fa ` (Rep_zet a) = explode za" by blast
  from Rep_zet[of b] have "\f z. inj_on f (Rep_zet b) \ f ` (Rep_zet b) = explode z"
    by (auto simp add: zet_def')
  then obtain fb zb where b:"inj_on fb (Rep_zet b) \ fb ` (Rep_zet b) = explode zb"
    by blast
  from b have fb: "inj_on fb (Rep_zet b)" by blast
  from b have zb: "fb ` (Rep_zet b) = explode zb" by blast
  let ?f = "(\ x. if x \ (Rep_zet a) then Opair (fa x) (Empty) else Opair (fb x) (Singleton Empty))"
  let ?z = "CartProd (union za zb) (Upair Empty (Singleton Empty))"
  have se: "Singleton Empty \ Empty"
    apply (auto simp add: Ext Singleton)
    apply (rule exI[where x=Empty])
    apply (simp add: Empty)
    done
  show ?thesis
    apply (simp add: zunion_def)
    apply (subst Abs_zet_inverse)
    apply (auto simp add: zet_def)
    apply (rule exI[where x = ?f])
    apply (rule conjI)
    apply (auto simp add: inj_on_def Opair inj_onD[OF fa] inj_onD[OF fb] se se[symmetric])
    apply (rule exI[where x = ?z])
    apply (insert za zb)
    apply (auto simp add: explode_def CartProd union Upair Opair)
    done
qed

lemma zunion: "zin x (zunion a b) = ((zin x a) \ (zin x b))"
  by (auto simp add: zin_def Rep_zet_zunion)

lemma zimage_zexplode_eq: "zimage f (zexplode z) = zexplode (Repl z f)"
  by (simp add: zet_ext_eq zin_zexplode_eq Repl zimage_iff)

lemma range_explode_eq_zet: "range explode = zet"
  apply (rule set_eqI)
  apply (auto simp add: explode_mem_zet)
  apply (drule image_zet_rep)
  apply (simp add: image_def)
  apply auto
  apply (rule_tac x=z in exI)
  apply auto
  done

lemma Elem_zimplode: "(Elem x (zimplode z)) = (zin x z)"
  apply (simp add: zimplode_def)
  apply (subst Elem_implode)
  apply (simp_all add: zin_def Rep_zet range_explode_eq_zet)
  done

definition zempty :: "'a zet" where
  "zempty \ Abs_zet {}"

lemma zempty[simp]: "\ (zin x zempty)"
  by (auto simp add: zin_def zempty_def Abs_zet_inverse zet_def)

lemma zimage_zempty[simp]: "zimage f zempty = zempty"
  by (auto simp add: zet_ext_eq zimage_iff)

lemma zunion_zempty_left[simp]: "zunion zempty a = a"
  by (simp add: zet_ext_eq zunion)

lemma zunion_zempty_right[simp]: "zunion a zempty = a"
  by (simp add: zet_ext_eq zunion)

lemma zimage_id[simp]: "zimage id A = A"
  by (simp add: zet_ext_eq zimage_iff)

lemma zimage_cong[fundef_cong]: "\ M = N; !! x. zin x N \ f x = g x \ \ zimage f M = zimage g N"
  by (auto simp add: zet_ext_eq zimage_iff)

end

quality100%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.