(* Title: ZF/Coind/Map.thy ID: $Id: Map.thy,v 1.12 2005/06/17 14:15:10 haftmann Exp $ Author: Jacob Frost, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge Some sample proofs of inclusions for the final coalgebra "U" (by lcp) *) theory Map imports Main begin constdefs TMap :: "[i,i] => i" "TMap(A,B) == {m ∈ Pow(A*Union(B)).∀a ∈ A. m``{a} ∈ B}" PMap :: "[i,i] => i" "PMap(A,B) == TMap(A,cons(0,B))" (* Note: 0 ∈ B ==> TMap(A,B) = PMap(A,B) *) map_emp :: i "map_emp == 0" map_owr :: "[i,i,i]=>i" "map_owr(m,a,b) == Σ x ∈ {a} Un domain(m). if x=a then b else m``{x}" map_app :: "[i,i]=>i" "map_app(m,a) == m``{a}" lemma "{0,1} ⊆ {1} Un TMap(I, {0,1})" by (unfold TMap_def, blast) lemma "{0} Un TMap(I,1) ⊆ {1} Un TMap(I, {0} Un TMap(I,1))" by (unfold TMap_def, blast) lemma "{0,1} Un TMap(I,2) ⊆ {1} Un TMap(I, {0,1} Un TMap(I,2))" by (unfold TMap_def, blast) (*A bit too slow. lemma "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) ⊆ {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))" by (unfold TMap_def, blast) *) (* ############################################################ *) (* Lemmas *) (* ############################################################ *) lemma qbeta_if: "Sigma(A,B)``{a} = (if a ∈ A then B(a) else 0)" by auto lemma qbeta: "a ∈ A ==> Sigma(A,B)``{a} = B(a)" by fast lemma qbeta_emp: "a∉A ==> Sigma(A,B)``{a} = 0" by fast lemma image_Sigma1: "a ∉ A ==> Sigma(A,B)``{a}=0" by fast (* ############################################################ *) (* Inclusion in Quine Universes *) (* ############################################################ *) (* Lemmas *) lemma MapQU_lemma: "A ⊆ univ(X) ==> Pow(A * Union(quniv(X))) ⊆ quniv(X)" apply (unfold quniv_def) apply (rule Pow_mono) apply (rule subset_trans [OF Sigma_mono product_univ]) apply (erule subset_trans) apply (rule arg_subset_eclose [THEN univ_mono]) apply (simp add: Union_Pow_eq) done (* Theorems *) lemma mapQU: "[| m ∈ PMap(A,quniv(B)); !!x. x ∈ A ==> x ∈ univ(B) |] ==> m ∈ quniv(B)" apply (unfold PMap_def TMap_def) apply (blast intro!: MapQU_lemma [THEN subsetD]) done (* ############################################################ *) (* Monotonicity *) (* ############################################################ *) lemma PMap_mono: "B ⊆ C ==> PMap(A,B)<=PMap(A,C)" by (unfold PMap_def TMap_def, blast) (* ############################################################ *) (* Introduction Rules *) (* ############################################################ *) (** map_emp **) lemma pmap_empI: "map_emp ∈ PMap(A,B)" by (unfold map_emp_def PMap_def TMap_def, auto) (** map_owr **) lemma pmap_owrI: "[| m ∈ PMap(A,B); a ∈ A; b ∈ B |] ==> map_owr(m,a,b):PMap(A,B)" apply (unfold map_owr_def PMap_def TMap_def, safe) apply (simp_all add: if_iff, auto) (*Remaining subgoal*) apply (rule excluded_middle [THEN disjE]) apply (erule image_Sigma1) apply (drule_tac psi = "?uu ∉ B" in asm_rl) apply (auto simp add: qbeta) done (** map_app **) lemma tmap_app_notempty: "[| m ∈ TMap(A,B); a ∈ domain(m) |] ==> map_app(m,a) ≠0" by (unfold TMap_def map_app_def, blast) lemma tmap_appI: "[| m ∈ TMap(A,B); a ∈ domain(m) |] ==> map_app(m,a):B" by (unfold TMap_def map_app_def domain_def, blast) lemma pmap_appI: "[| m ∈ PMap(A,B); a ∈ domain(m) |] ==> map_app(m,a):B" apply (unfold PMap_def) apply (frule tmap_app_notempty, assumption) apply (drule tmap_appI, auto) done (** domain **) lemma tmap_domainD: "[| m ∈ TMap(A,B); a ∈ domain(m) |] ==> a ∈ A" by (unfold TMap_def, blast) lemma pmap_domainD: "[| m ∈ PMap(A,B); a ∈ domain(m) |] ==> a ∈ A" by (unfold PMap_def TMap_def, blast) (* ############################################################ *) (* Equalities *) (* ############################################################ *) (** Domain **) (* Lemmas *) lemma domain_UN: "domain(\<Union>x ∈ A. B(x)) = (\<Union>x ∈ A. domain(B(x)))" by fast lemma domain_Sigma: "domain(Sigma(A,B)) = {x ∈ A. ∃y. y ∈ B(x)}" by blast (* Theorems *) lemma map_domain_emp: "domain(map_emp) = 0" by (unfold map_emp_def, blast) lemma map_domain_owr: "b ≠ 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)" apply (unfold map_owr_def) apply (auto simp add: domain_Sigma) done (** Application **) lemma map_app_owr: "map_app(map_owr(f,a,b),c) = (if c=a then b else map_app(f,c))" by (simp add: qbeta_if map_app_def map_owr_def, blast) lemma map_app_owr1: "map_app(map_owr(f,a,b),a) = b" by (simp add: map_app_owr) lemma map_app_owr2: "c ≠ a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)" by (simp add: map_app_owr) end
lemma
{0, 1} ⊆ {1} ∪ TMap(I, {0, 1})
lemma
{0} ∪ TMap(I, 1) ⊆ {1} ∪ TMap(I, {0} ∪ TMap(I, 1))
lemma
{0, 1} ∪ TMap(I, 2) ⊆ {1} ∪ TMap(I, {0, 1} ∪ TMap(I, 2))
lemma qbeta_if:
Sigma(A, B) `` {a} = (if a ∈ A then B(a) else 0)
lemma qbeta:
a ∈ A ==> Sigma(A, B) `` {a} = B(a)
lemma qbeta_emp:
a ∉ A ==> Sigma(A, B) `` {a} = 0
lemma image_Sigma1:
a ∉ A ==> Sigma(A, B) `` {a} = 0
lemma MapQU_lemma:
A ⊆ univ(X) ==> Pow(A × \<Union>quniv(X)) ⊆ quniv(X)
lemma mapQU:
[| m ∈ PMap(A, quniv(B)); !!x. x ∈ A ==> x ∈ univ(B) |] ==> m ∈ quniv(B)
lemma PMap_mono:
B ⊆ C ==> PMap(A, B) ⊆ PMap(A, C)
lemma pmap_empI:
map_emp ∈ PMap(A, B)
lemma pmap_owrI:
[| m ∈ PMap(A, B); a ∈ A; b ∈ B |] ==> map_owr(m, a, b) ∈ PMap(A, B)
lemma tmap_app_notempty:
[| m ∈ TMap(A, B); a ∈ domain(m) |] ==> map_app(m, a) ≠ 0
lemma tmap_appI:
[| m ∈ TMap(A, B); a ∈ domain(m) |] ==> map_app(m, a) ∈ B
lemma pmap_appI:
[| m ∈ PMap(A, B); a ∈ domain(m) |] ==> map_app(m, a) ∈ B
lemma tmap_domainD:
[| m ∈ TMap(A, B); a ∈ domain(m) |] ==> a ∈ A
lemma pmap_domainD:
[| m ∈ PMap(A, B); a ∈ domain(m) |] ==> a ∈ A
lemma domain_UN:
domain(\<Union>x∈A. B(x)) = (\<Union>x∈A. domain(B(x)))
lemma domain_Sigma:
domain(Sigma(A, B)) = {x ∈ A . ∃y. y ∈ B(x)}
lemma map_domain_emp:
domain(map_emp) = 0
lemma map_domain_owr:
b ≠ 0 ==> domain(map_owr(f, a, b)) = {a} ∪ domain(f)
lemma map_app_owr:
map_app(map_owr(f, a, b), c) = (if c = a then b else map_app(f, c))
lemma map_app_owr1:
map_app(map_owr(f, a, b), a) = b
lemma map_app_owr2:
c ≠ a ==> map_app(map_owr(f, a, b), c) = map_app(f, c)