|
(* Title: ZF/Coind/Map.thy
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 ZF begin
definition
TMap :: "[i,i] => i" where
"TMap(A,B) == {m \ Pow(A*\(B)).\a \ A. m``{a} \ B}"
definition
PMap :: "[i,i] => i" where
"PMap(A,B) == TMap(A,cons(0,B))"
(* Note: 0 \<in> B ==> TMap(A,B) = PMap(A,B) *)
definition
map_emp :: i where
"map_emp == 0"
definition
map_owr :: "[i,i,i]=>i" where
"map_owr(m,a,b) == \x \ {a} \ domain(m). if x=a then b else m``{x}"
definition
map_app :: "[i,i]=>i" where
"map_app(m,a) == m``{a}"
lemma "{0,1} \ {1} \ TMap(I, {0,1})"
by (unfold TMap_def, blast)
lemma "{0} \ TMap(I,1) \ {1} \ TMap(I, {0} \ TMap(I,1))"
by (unfold TMap_def, blast)
lemma "{0,1} \ TMap(I,2) \ {1} \ TMap(I, {0,1} \ TMap(I,2))"
by (unfold TMap_def, blast)
(*A bit too slow.
lemma "{0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2) \<subseteq>
{1} \<union> TMap(I, {0,1} \<union> TMap(I,TMap(I,2)) \<union> 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 * \(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" for uu 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(\x \ A. B(x)) = (\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} \ 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
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
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.
|
