Quelle  ListN.thy

(*  Title:      ZF/Induct/ListN.thy
  Author: Lawrence C Paulson, Cambridge University Computer Laboratory
  Copyright 1994 University of Cambridge
*)

section ‹Lists of n elements›

theory ListN imports ZF begin

text ‹
  Inductive definition of lists of ‹n› elements; see
  🍋‹"paulin-tlca"›.
 ›

consts listn :: "i==>i"
inductive
  domains "listn(A)" ⊆ "nat × list(A)"
  intros
    NilI: "⟨0,Nil⟩ ∈ listn(A)"
    ConsI: "[a ∈ A; ⟨n,l⟩ ∈ listn(A)] ==> ∈ listn(A)"
  type_intros nat_typechecks list.intros


lemma list_into_listn: "l ∈ list(A) ==> ∈ listn(A)"
  by (induct set: list) (simp_all add: listn.intros)

lemma listn_iff: "⟨n,l⟩ ∈ listn(A) ⟷ l ∈ list(A) ∧ length(l)=n"
  apply (rule iffI)
   apply (erule listn.induct)
    apply auto
  apply (blast intro: list_into_listn)
  done

lemma listn_image_eq: "listn(A)``{n} = {l ∈ list(A). length(l)=n}"
  apply (rule equality_iffI)
  apply (simp add: listn_iff separation image_singleton_iff)
  done

lemma listn_mono: "A ⊆ B ==> listn(A) ⊆ listn(B)"
    unfolding listn.defs
  apply (rule lfp_mono)
    apply (rule listn.bnd_mono)+
  apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+
  done

lemma listn_append:
    "[⟨n,l⟩ ∈ listn(A); ∈ listn(A)] ==> ∈ listn(A)"
  apply (erule listn.induct)
   apply (frule listn.dom_subset [THEN subsetD])
   apply (simp_all add: listn.intros)
  done

inductive_cases
      Nil_listn_case: "⟨i,Nil⟩ ∈ listn(A)"
  and Cons_listn_case: " ∈ listn(A)"

inductive_cases
      zero_listn_case: "⟨0,l⟩ ∈ listn(A)"
  and succ_listn_case: " ∈ listn(A)"

end