Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Zet.thy   Sprache: Isabelle

Original von: 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 subset_inj_on[where B=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

¤ Dauer der Verarbeitung: 0.20 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik