# Theory Map

Up to index of Isabelle/ZF/Coind

theory Map
imports Main
begin

    (*  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)