header "Universe"
theory Universe
imports "~~/src/HOL/ZF/MainZF"
begin
locale Universe =
fixes U :: ZF (structure)
assumes Uempty : "Elem Empty U"
and Usubset : "Elem u U ==> subset u U"
and Usingle : "Elem u U ==> Elem (Singleton u) U"
and Upow : "Elem u U ==> Elem (Power u) U"
and Uim : "[|Elem I U ; Elem u (Fun I U) |] ==> Elem (Sum (Range u)) U"
and Unat : "Elem Nat U"
lemma ElemLambdaFun : "(!! x .Elem x u ==> Elem (f x) U) ==> Elem (Lambda u f) (Fun u U)"
apply (subst Elem_Lambda_Fun)
apply simp
done
lemma RangeRepl: "Range (Lambda A f) = Repl A f"
apply (subst Ext)
apply (subst Range)
apply (simp add: Repl Opair Lambda_def)
done
lemma (in Universe) Utrans: "[|Elem a U ; Elem b a|] ==> Elem b U"
apply (drule Usubset)
apply (insert HOLZF.subset_def [of a U])
apply (auto simp add: Usubset)
done
lemma ReplId: "Repl A id = A"
by (subst Ext, simp add: Repl)
lemma (in Universe) UniverseSum : "Elem u U ==> Elem (Sum u) U"
apply (frule_tac u = "Lambda u id" in Uim)
apply (subst Elem_Lambda_Fun)
apply (frule Usubset)
apply (simp add: subset_def)
apply (simp only: RangeRepl ReplId)
done
lemma (in Universe) UniverseUnion:
assumes "Elem u U" and "Elem v U"
shows "Elem (union u v) U"
proof-
let ?f = "(% x. if x = Empty then u else v)"
and ?S = "(Power (Power Empty))"
have 1: "(Upair u v) = Range (Lambda ?S ?f)"
by (subst RangeRepl, simp add: Upair_def)
have 2: "[|Elem u U; Elem v U|] ==> Elem (Lambda ?S ?f) (Fun ?S U)"
by (rule ElemLambdaFun, simp)
show ?thesis using assms
apply (subst HOLZF.union_def)
apply (subst 1)
apply (rule_tac I="?S" in Uim)
apply (rule Upow)+
apply (rule Uempty)
apply (rule 2)
apply simp+
done
qed
lemma UPairSingleton: "Upair u v = union (Singleton u) (Singleton v)"
apply (subst Ext)
apply (subst Upair)
apply (subst union)
apply (subst Singleton)+
apply (simp)
done
lemma (in Universe) UniverseUPair: "[|Elem u U ; Elem v U|] ==> Elem (Upair u v) U"
apply (subst UPairSingleton)
apply (rule UniverseUnion)
apply (rule Usingle, simp)+
done
lemma (in Universe) UniversePair: "[|Elem u U ; Elem v U|] ==> Elem (Opair u v) U"
apply (subst Opair_def)
apply ((rule UniverseUPair)+, simp+)+
done
lemma (in Universe) "[|Elem u U ; Elem v U|] ==> Elem (Sum (Repl u (%x . Singleton (Opair x v)))) U"
apply (rule RangeRepl [THEN subst])
apply (rule Uim [of u], simp)
apply (rule ElemLambdaFun)
apply (rule Usingle)
apply (rule UniversePair)
apply (rule Utrans)
apply simp+
done
lemma SumRepl: "Sum (Repl A (Singleton o f)) = Repl A f"
proof-
show ?thesis
apply (subst Ext)
apply (subst Sum)
apply (subst Repl)+
apply (auto simp add: Singleton)
proof-
fix a
show "Elem a A ==> ∃y. Elem (f a) y ∧ (∃a. Elem a A ∧ y = Singleton (f a))"
apply (rule exI [of _ "Singleton (f a)"])
apply (subst Singleton, simp+)
apply (rule exI [of _ "a"], simp+)
done
qed
qed
lemma (in Universe) UniverseProd:
assumes "Elem u U" and "Elem v U"
shows "Elem (CartProd u v) U"
proof-
show ?thesis using assms
apply (subst CartProd_def)
apply (rule RangeRepl [of u "% x . (Repl v (Opair x))", THEN subst])
apply (rule Uim [of u], simp)
apply (rule ElemLambdaFun)
proof-
fix x
show "[|Elem u U; Elem v U; Elem x u|] ==> Elem (Repl v (Opair x)) U"
apply (drule Utrans [of u x], simp)
apply (rule SumRepl [THEN subst])
apply (rule RangeRepl [THEN subst])
apply (rule Uim [of v], simp)
apply (rule ElemLambdaFun,simp)
apply (rule Usingle)
apply (rule UniversePair)
apply (drule Usubset, simp)
proof-
fix xa
show "[|Elem v U; Elem x u; Elem x U; Elem xa v|] ==> Elem xa U"
by (rule Utrans, simp+)
qed
qed
qed
lemma (in Universe) UniverseSubset: "[|subset u v ; Elem v U|] ==> Elem u U"
apply (drule_tac HOLZF.Power [of u v, THEN ssubst])
apply (drule Upow)
apply (rule Utrans, simp+)
done
definition
Product :: "ZF => ZF" where
"Product U = Sep (Fun U (Sum U)) (%f . (∀ u . Elem u U --> Elem (app f u) u))"
lemma SepSubset: "subset (Sep A p) A"
apply (subst subset_def)
apply (subst Sep, simp)
done
lemma SubsetSmall:
assumes "subset A' A" and "subset A B" shows "subset A' B"
proof-
have "(subset A' A ∧ subset A B) --> subset A' B"
by ((subst subset_def)+, simp+)
thus ?thesis using assms by simp
qed
lemma SubsetTrans:
assumes "(subset a b)" and "(subset b c)"
shows "(subset a c)"
proof-
have "(subset a b) ∧ (subset b c) --> (subset a c)"
by ((subst subset_def)+, simp)
thus ?thesis using assms by simp
qed
lemma SubsetSepTrans: "subset A B ==> subset (Sep A p) B"
apply (rule SubsetSmall [of "Sep A p" A B])
apply (rule SepSubset)
by simp
lemma ProductSubset: "subset (Product u) (Power (CartProd u (Sum u)))"
apply (subst Product_def)
apply (subst Fun_def)
apply (subst PFun_def)
apply (rule SubsetSepTrans)+
apply (subst subset_def)
by simp
lemma (in Universe) UniverseProduct: "Elem u U ==> Elem (Product u) U"
apply (rule_tac u="(Product u)" and v="Power (CartProd u (Sum u))" in UniverseSubset)
apply (rule ProductSubset)
apply (rule Upow)
apply (rule UniverseProd, simp)
apply (rule UniverseSum,simp)
done
lemma ZFImageRangeExplode: "x ∈ range explode ==> f ` x ∈ range explode"
proof-
assume "x ∈ range explode"
from this obtain y where "x = explode y" using range_ex1_eq by auto
hence "f ` x = explode (Repl y f)" using explode_Repl_eq by simp
thus "f ` x ∈ range explode" by auto
qed
definition "subsetFn X Y ≡ λ x . (if x ∈ Y then x else SOME y . y ∈ Y)"
lemma subsetFn: "[|Y ≠ {} ; Y ⊆ X |] ==> (subsetFn X Y) ` X = Y"
proof(auto simp add: subsetFn_def)
fix x assume "x ∈ Y"
thus "(SOME y. y ∈ Y) ∈ Y" using someI_ex[of "λ x . x ∈ Y"] by auto
qed
lemma ZFSubsetRangeExplode: "[|X ∈ range explode ; Y ⊆ X|] ==> Y ∈ range explode"
proof(cases "Y = {}", simp)
have "explode Empty = {}" using explode_Empty by simp
thus "{} ∈ range explode" by (auto simp add: explode_def)
assume "Y ≠ {}" and "Y ⊆ X" and "X ∈ range explode" thus "Y ∈ range explode"
using ZFImageRangeExplode[of X "subsetFn X Y"] subsetFn[of Y X] by simp
qed
lemma ZFUnionRangeExplode:
assumes "!! x . x ∈ A ==> f x ∈ range explode" and "A ∈ range explode"
shows "(\<Union> x ∈ A . f x) ∈ range explode"
proof-
let ?S = "Sep (Sum (Repl (implode A) (implode o f))) (λ y . ∃ x . (Elem x (implode A)) ∧ (Elem y (implode (f x))))"
have "explode ?S = (\<Union> x ∈ A . f x)"
proof(auto simp add: UNION_eq explode_def Sep Sum Repl assms Elem_implode)
fix x y assume a: "y ∈ A" and b: "x ∈ f y"
show "∃z. Elem x z ∧ (∃a. a ∈ A ∧ z = implode (f a))"
apply(rule exI[where ?x = "implode (f y)"])
apply(auto simp add: explode_def Sep Sum Repl assms Elem_implode a b)
by(rule exI[where ?x = y], simp add: a)
qed
thus ?thesis by auto
qed
lemma ZFUnionNatInRangeExplode: "(!! (n :: nat) . f n ∈ range explode) ==> (\<Union> n . f n) ∈ range explode"
proof-
assume a: "(!! (n :: nat) . f n ∈ range explode)"
have "explode Nat ∈ range explode" by simp
moreover have "!! n . n ∈ (explode Nat) ==> (f o Nat2nat) n ∈ range explode" using a
by(auto simp add: explode_def)
moreover have "(\<Union> n . f n) = (\<Union> n ∈ (explode Nat) . (f o Nat2nat) n)"
proof(auto simp add: Nat2nat_def)
fix x n assume aa: "x ∈ f n" show "∃ n ∈ (explode Nat) . x ∈ f (inv nat2Nat n)"
apply(rule bexI[where ?x = "nat2Nat n"])
by(auto simp add: aa inj_nat2Nat explode_Elem)
qed
ultimately show "(\<Union> n . f n) ∈ range explode" using ZFUnionRangeExplode by simp
qed
lemma ZFProdFnInRangeExplode: "[|A ∈ range explode ; B ∈ range explode|] ==> f ` (A × B) ∈ range explode"
proof-
assume a: "A ∈ range explode" and b: "B ∈ range explode"
let ?X = "(explode (CartProd (implode A) (implode B)))"
have "f ` (A × B) = (f o (λ z . (Fst z, Snd z))) ` ?X"
proof(auto simp add: explode_def CartProd image_def Fst Snd)
{
fix z y assume z: "z ∈ A" and y: "y ∈ B" show "∃x. (∃a. Elem a (implode A) ∧
(∃b. Elem b (implode B) ∧ x = Opair a b)) ∧ f (z, y) = f (Fst x, Snd x)"
apply(insert z y a b)
apply(rule exI[where ?x = "Opair z y"])
apply(auto simp add: Opair explode_Elem Fst Snd)
done
}
{
fix a b assume aa: "Elem a (implode A)" and bb: "Elem b (implode B)"
show "∃ x ∈ A . ∃ y ∈ B . f (a,b) = f (x,y)"
by(rule bexI[where ?x = a], rule bexI[where ?x = b], simp, insert a b aa bb, auto simp add: explode_Elem)
}
qed
moreover have "?X ∈ range explode" by simp
ultimately show "f ` (A × B) ∈ range explode" using ZFImageRangeExplode by simp
qed
lemma ZFUnionInRangeExplode: "[|A ∈ range explode ; B ∈ range explode|] ==> A ∪ B ∈ range explode"
proof-
assume "A ∈ range explode" and "B ∈ range explode"
from this obtain A' B' where A': "A = explode A'" and B': "B = explode B'" by auto
have "A ∪ B = explode (union (implode A) (implode B))"
by(auto simp add: explode_union union explode_Elem A' B')
thus "A ∪ B ∈ range explode" by auto
qed
lemma SingletonInRangeExplode: "{x} ∈ range explode"
proof-
have "explode (Singleton x) = {x}" by(auto simp add: explode_def Singleton)
thus ?thesis by auto
qed
definition ZFTriple :: "[ZF,ZF,ZF] => ZF" where
"ZFTriple a b c = Opair (Opair a b) c"
definition "ZFTFst = Fst o Fst"
definition "ZFTSnd = Snd o Fst"
definition "ZFTThd = Snd"
lemma ZFTFst: "ZFTFst (ZFTriple a b c) = a"
by(auto simp add: ZFTriple_def ZFTFst_def Fst)
lemma ZFTSnd: "ZFTSnd (ZFTriple a b c) = b"
by(auto simp add: ZFTriple_def ZFTSnd_def Snd Fst)
lemma ZFTThd: "ZFTThd (ZFTriple a b c) = c"
by(auto simp add: ZFTriple_def ZFTThd_def Snd Fst)
lemma ZFTriple: "ZFTriple a b c = ZFTriple a' b' c' ==> (a = a' ∧ b = b' ∧ c = c')"
by(auto simp add: ZFTriple_def Opair)
lemma ZFSucZero: "Nat2nat (SucNat Empty) = 1"
proof-
have "nat2Nat 0 = Empty" by auto
hence "(SucNat Empty) = nat2Nat (Suc 0)" by auto
hence "Nat2nat (SucNat Empty) = Nat2nat (nat2Nat (Suc 0))" by simp
also have "... = Suc 0" using Nat2nat_nat2Nat[of "Suc 0"] by simp
finally show ?thesis by simp
qed
lemma ZFZero: "Nat2nat Empty = 0"
proof-
have "nat2Nat 0 = Empty" by auto
hence "Nat2nat Empty = Nat2nat (nat2Nat 0)" by simp
thus ?thesis using Nat2nat_nat2Nat[of "0"] by simp
qed
lemma ZFSucNeq0: "Elem x Nat ==> Nat2nat (SucNat x) ≠ 0"
by(auto simp add: Nat2nat_SucNat)
end