Quelle Map.thy Sprache: Isabelle

(*  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 \<Longrightarrow> 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)"
  unfolding 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)"
  unfolding 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"
  unfolding 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)"
  unfolding 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

quality97%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.