# Theory InfDatatype

Up to index of Isabelle/ZF

theory InfDatatype
imports Datatype Univ Finite Cardinal_AC
begin

    (*  Title:      ZF/InfDatatype.ML
        ID:         $Id: InfDatatype.thy,v 1.7 2005/06/17 14:15:09 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge

    *)

    header{*Infinite-Branching Datatype Definitions*}

    theory InfDatatype imports Datatype Univ Finite Cardinal_AC begin

    lemmas fun_Limit_VfromE =
        Limit_VfromE [OF apply_funtype InfCard_csucc [THEN InfCard_is_Limit]]

    lemma fun_Vcsucc_lemma:
         "[| f: D -> Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]
          ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)"
    apply (rule_tac x = "\<Union>d∈D. LEAST i. f`d : Vfrom (A,i) " in exI)
    apply (rule conjI)
    apply (rule_tac [2] le_UN_Ord_lt_csucc)
    apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all)
     prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE)
    apply (rule Pi_type)
    apply (rename_tac [2] d)
    apply (erule_tac [2] fun_Limit_VfromE, simp_all)
    apply (subgoal_tac "f`d : Vfrom (A, LEAST i. f`d : Vfrom (A,i))")
     apply (erule Vfrom_mono [OF subset_refl UN_upper, THEN subsetD])
     apply assumption
    apply (fast elim: LeastI ltE)
    done

    lemma subset_Vcsucc:
         "[| D <= Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]
          ==> EX j. D <= Vfrom(A,j) & j < csucc(K)"
    by (simp add: subset_iff_id fun_Vcsucc_lemma)

    (*Version for arbitrary index sets*)
    lemma fun_Vcsucc:
         "[| |D| le K;  InfCard(K);  D <= Vfrom(A,csucc(K)) |] ==>
              D -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"
    apply (safe dest!: fun_Vcsucc_lemma subset_Vcsucc)
    apply (rule Vfrom [THEN ssubst])
    apply (drule fun_is_rel)
    (*This level includes the function, and is below csucc(K)*)
    apply (rule_tac a1 = "succ (succ (j Un ja))" in UN_I [THEN UnI2])
    apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ
                        Un_least_lt)
    apply (erule subset_trans [THEN PowI])
    apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2)
    done

    lemma fun_in_Vcsucc:
         "[| f: D -> Vfrom(A, csucc(K));  |D| le K;  InfCard(K);
             D <= Vfrom(A,csucc(K)) |]
           ==> f: Vfrom(A,csucc(K))"
    by (blast intro: fun_Vcsucc [THEN subsetD])

    (*Remove <= from the rule above*)
    lemmas fun_in_Vcsucc' = fun_in_Vcsucc [OF _ _ _ subsetI]

    (** Version where K itself is the index set **)

    lemma Card_fun_Vcsucc:
         "InfCard(K) ==> K -> Vfrom(A,csucc(K)) <= Vfrom(A,csucc(K))"
    apply (frule InfCard_is_Card [THEN Card_is_Ord])
    apply (blast del: subsetI
                 intro: fun_Vcsucc Ord_cardinal_le i_subset_Vfrom
                       lt_csucc [THEN leI, THEN le_imp_subset, THEN subset_trans])
    done

    lemma Card_fun_in_Vcsucc:
         "[| f: K -> Vfrom(A, csucc(K));  InfCard(K) |] ==> f: Vfrom(A,csucc(K))"
    by (blast intro: Card_fun_Vcsucc [THEN subsetD])

    lemma Limit_csucc: "InfCard(K) ==> Limit(csucc(K))"
    by (erule InfCard_csucc [THEN InfCard_is_Limit])

    lemmas Pair_in_Vcsucc = Pair_in_VLimit [OF _ _ Limit_csucc]
    lemmas Inl_in_Vcsucc = Inl_in_VLimit [OF _ Limit_csucc]
    lemmas Inr_in_Vcsucc = Inr_in_VLimit [OF _ Limit_csucc]
    lemmas zero_in_Vcsucc = Limit_csucc [THEN zero_in_VLimit]
    lemmas nat_into_Vcsucc = nat_into_VLimit [OF _ Limit_csucc]

    (*For handling Cardinals of the form  (nat Un |X|) *)

    lemmas InfCard_nat_Un_cardinal = InfCard_Un [OF InfCard_nat Card_cardinal]

    lemmas le_nat_Un_cardinal =
         Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]]

    lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le]

    (*The new version of Data_Arg.intrs, declared in Datatype.ML*)
    lemmas Data_Arg_intros =
           SigmaI InlI InrI
           Pair_in_univ Inl_in_univ Inr_in_univ
           zero_in_univ A_into_univ nat_into_univ UnCI

    (*For most K-branching datatypes with domain Vfrom(A, csucc(K)) *)
    lemmas inf_datatype_intros =
         InfCard_nat InfCard_nat_Un_cardinal
         Pair_in_Vcsucc Inl_in_Vcsucc Inr_in_Vcsucc
         zero_in_Vcsucc A_into_Vfrom nat_into_Vcsucc
         Card_fun_in_Vcsucc fun_in_Vcsucc' UN_I

    end

lemmas fun_Limit_VfromE:

      [| f3 ∈ A3 -> Vfrom(A, csucc(K2)); a3 ∈ A3; ¬ R ==> InfCard(K2);
         !!x. [| x < csucc(K2); f3 ` a3 ∈ Vfrom(A, x) |] ==> R |]
      ==> R

lemmas fun_Limit_VfromE:

      [| f3 ∈ A3 -> Vfrom(A, csucc(K2)); a3 ∈ A3; ¬ R ==> InfCard(K2);
         !!x. [| x < csucc(K2); f3 ` a3 ∈ Vfrom(A, x) |] ==> R |]
      ==> R

lemma fun_Vcsucc_lemma:

      [| f ∈ D -> Vfrom(A, csucc(K)); |D| ≤ K; InfCard(K) |]
      ==> ∃j. f ∈ D -> Vfrom(A, j) ∧ j < csucc(K)

lemma subset_Vcsucc:

      [| D ⊆ Vfrom(A, csucc(K)); |D| ≤ K; InfCard(K) |]
      ==> ∃j. D ⊆ Vfrom(A, j) ∧ j < csucc(K)

lemma fun_Vcsucc:

      [| |D| ≤ K; InfCard(K); D ⊆ Vfrom(A, csucc(K)) |]
      ==> D -> Vfrom(A, csucc(K)) ⊆ Vfrom(A, csucc(K))

lemma fun_in_Vcsucc:

      [| f ∈ D -> Vfrom(A, csucc(K)); |D| ≤ K; InfCard(K); D ⊆ Vfrom(A, csucc(K)) |]
      ==> f ∈ Vfrom(A, csucc(K))

lemmas fun_in_Vcsucc':

      [| f ∈ D -> Vfrom(A, csucc(K)); |D| ≤ K; InfCard(K);
         !!x. x ∈ D ==> x ∈ Vfrom(A, csucc(K)) |]
      ==> f ∈ Vfrom(A, csucc(K))

lemmas fun_in_Vcsucc':

      [| f ∈ D -> Vfrom(A, csucc(K)); |D| ≤ K; InfCard(K);
         !!x. x ∈ D ==> x ∈ Vfrom(A, csucc(K)) |]
      ==> f ∈ Vfrom(A, csucc(K))

lemma Card_fun_Vcsucc:

      InfCard(K) ==> K -> Vfrom(A, csucc(K)) ⊆ Vfrom(A, csucc(K))

lemma Card_fun_in_Vcsucc:

      [| f ∈ K -> Vfrom(A, csucc(K)); InfCard(K) |] ==> f ∈ Vfrom(A, csucc(K))

lemma Limit_csucc:

      InfCard(K) ==> Limit(csucc(K))

lemmas Pair_in_Vcsucc:

      [| a ∈ Vfrom(A, csucc(K1)); b ∈ Vfrom(A, csucc(K1)); InfCard(K1) |]
      ==> ⟨a, b⟩ ∈ Vfrom(A, csucc(K1))

lemmas Pair_in_Vcsucc:

      [| a ∈ Vfrom(A, csucc(K1)); b ∈ Vfrom(A, csucc(K1)); InfCard(K1) |]
      ==> ⟨a, b⟩ ∈ Vfrom(A, csucc(K1))

lemmas Inl_in_Vcsucc:

      [| a ∈ Vfrom(A, csucc(K1)); InfCard(K1) |] ==> Inl(a) ∈ Vfrom(A, csucc(K1))

lemmas Inl_in_Vcsucc:

      [| a ∈ Vfrom(A, csucc(K1)); InfCard(K1) |] ==> Inl(a) ∈ Vfrom(A, csucc(K1))

lemmas Inr_in_Vcsucc:

      [| b ∈ Vfrom(A, csucc(K1)); InfCard(K1) |] ==> Inr(b) ∈ Vfrom(A, csucc(K1))

lemmas Inr_in_Vcsucc:

      [| b ∈ Vfrom(A, csucc(K1)); InfCard(K1) |] ==> Inr(b) ∈ Vfrom(A, csucc(K1))

lemmas zero_in_Vcsucc:

      InfCard(K1) ==> 0 ∈ Vfrom(A, csucc(K1))

lemmas zero_in_Vcsucc:

      InfCard(K1) ==> 0 ∈ Vfrom(A, csucc(K1))

lemmas nat_into_Vcsucc:

      [| n ∈ nat; InfCard(K1) |] ==> n ∈ Vfrom(A, csucc(K1))

lemmas nat_into_Vcsucc:

      [| n ∈ nat; InfCard(K1) |] ==> n ∈ Vfrom(A, csucc(K1))

lemmas InfCard_nat_Un_cardinal:

      InfCard(nat ∪ |A1|)

lemmas InfCard_nat_Un_cardinal:

      InfCard(nat ∪ |A1|)

lemmas le_nat_Un_cardinal:

      |A2| ≤ nat ∪ |A2|

lemmas le_nat_Un_cardinal:

      |A2| ≤ nat ∪ |A2|

lemmas UN_upper_cardinal:

      x2 ∈ A2 ==> |B2(x2)| ≤ |\<Union>x∈A2. B2(x)|

lemmas UN_upper_cardinal:

      x2 ∈ A2 ==> |B2(x2)| ≤ |\<Union>x∈A2. B2(x)|

lemmas Data_Arg_intros:

      [| a ∈ A; b ∈ B(a) |] ==> ⟨a, b⟩ ∈ Sigma(A, B)

      a ∈ A ==> Inl(a) ∈ A + B

      b ∈ B ==> Inr(b) ∈ A + B

      [| a ∈ univ(A); b ∈ univ(A) |] ==> ⟨a, b⟩ ∈ univ(A)

      a ∈ univ(A) ==> Inl(a) ∈ univ(A)

      b ∈ univ(A) ==> Inr(b) ∈ univ(A)

      0 ∈ univ(A)

      c ∈ A ==> c ∈ univ(A)

      c ∈ nat ==> c ∈ univ(A)

      (c ∉ B ==> c ∈ A) ==> c ∈ A ∪ B

lemmas Data_Arg_intros:

      [| a ∈ A; b ∈ B(a) |] ==> ⟨a, b⟩ ∈ Sigma(A, B)

      a ∈ A ==> Inl(a) ∈ A + B

      b ∈ B ==> Inr(b) ∈ A + B

      [| a ∈ univ(A); b ∈ univ(A) |] ==> ⟨a, b⟩ ∈ univ(A)

      a ∈ univ(A) ==> Inl(a) ∈ univ(A)

      b ∈ univ(A) ==> Inr(b) ∈ univ(A)

      0 ∈ univ(A)

      c ∈ A ==> c ∈ univ(A)

      c ∈ nat ==> c ∈ univ(A)

      (c ∉ B ==> c ∈ A) ==> c ∈ A ∪ B

lemmas inf_datatype_intros:

      InfCard(nat)

      InfCard(nat ∪ |A1|)

      [| a ∈ Vfrom(A, csucc(K1)); b ∈ Vfrom(A, csucc(K1)); InfCard(K1) |]
      ==> ⟨a, b⟩ ∈ Vfrom(A, csucc(K1))

      [| a ∈ Vfrom(A, csucc(K1)); InfCard(K1) |] ==> Inl(a) ∈ Vfrom(A, csucc(K1))

      [| b ∈ Vfrom(A, csucc(K1)); InfCard(K1) |] ==> Inr(b) ∈ Vfrom(A, csucc(K1))

      InfCard(K1) ==> 0 ∈ Vfrom(A, csucc(K1))

      c ∈ A ==> c ∈ Vfrom(A, i1)

      [| n ∈ nat; InfCard(K1) |] ==> n ∈ Vfrom(A, csucc(K1))

      [| f ∈ K -> Vfrom(A, csucc(K)); InfCard(K) |] ==> f ∈ Vfrom(A, csucc(K))

      [| f ∈ D -> Vfrom(A, csucc(K)); |D| ≤ K; InfCard(K);
         !!x. x ∈ D ==> x ∈ Vfrom(A, csucc(K)) |]
      ==> f ∈ Vfrom(A, csucc(K))

      [| a ∈ A; b ∈ B(a) |] ==> b ∈ (\<Union>x∈A. B(x))

lemmas inf_datatype_intros:

      InfCard(nat)

      InfCard(nat ∪ |A1|)

      [| a ∈ Vfrom(A, csucc(K1)); b ∈ Vfrom(A, csucc(K1)); InfCard(K1) |]
      ==> ⟨a, b⟩ ∈ Vfrom(A, csucc(K1))

      [| a ∈ Vfrom(A, csucc(K1)); InfCard(K1) |] ==> Inl(a) ∈ Vfrom(A, csucc(K1))

      [| b ∈ Vfrom(A, csucc(K1)); InfCard(K1) |] ==> Inr(b) ∈ Vfrom(A, csucc(K1))

      InfCard(K1) ==> 0 ∈ Vfrom(A, csucc(K1))

      c ∈ A ==> c ∈ Vfrom(A, i1)

      [| n ∈ nat; InfCard(K1) |] ==> n ∈ Vfrom(A, csucc(K1))

      [| f ∈ K -> Vfrom(A, csucc(K)); InfCard(K) |] ==> f ∈ Vfrom(A, csucc(K))

      [| f ∈ D -> Vfrom(A, csucc(K)); |D| ≤ K; InfCard(K);
         !!x. x ∈ D ==> x ∈ Vfrom(A, csucc(K)) |]
      ==> f ∈ Vfrom(A, csucc(K))

      [| a ∈ A; b ∈ B(a) |] ==> b ∈ (\<Union>x∈A. B(x))