# Theory ListN

Up to index of Isabelle/ZF/Induct

theory ListN
imports Main
begin

    (*  Title:      ZF/Induct/ListN.thy
        ID:         $Id: ListN.thy,v 1.4 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header {* Lists of n elements *}

    theory ListN imports Main begin

    text {*
      Inductive definition of lists of @{text n} elements; see
      \cite{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) |] ==> <succ(n), Cons(a,l)> ∈ listn(A)"
      type_intros nat_typechecks list.intros

    lemma list_into_listn: "l ∈ list(A) ==> <length(l),l> ∈ listn(A)"
      by (erule list.induct) (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)"
      apply (unfold 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); <n',l'> ∈ listn(A) |] ==> <n#+n', l@l'> ∈ 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: "<i,Cons(x,l)> ∈ listn(A)"

    inductive_cases
          zero_listn_case: "<0,l> ∈ listn(A)"
      and succ_listn_case: "<succ(i),l> ∈ listn(A)"

    end

lemma list_into_listn:

      l ∈ list(A) ==> ⟨length(l), l⟩ ∈ listn(A)

lemma listn_iff:

      ⟨n, l⟩ ∈ listn(A) <-> l ∈ list(A) ∧ length(l) = n

lemma listn_image_eq:

      listn(A) `` {n} = {l ∈ list(A) . length(l) = n}

lemma listn_mono:

      A ⊆ B ==> listn(A) ⊆ listn(B)

lemma listn_append:

      [| ⟨n, l⟩ ∈ listn(A); ⟨n', l'⟩ ∈ listn(A) |] ==> ⟨n #+ n', l @ l'⟩ ∈ listn(A)

lemmas Nil_listn_case:

      [| ⟨i, []⟩ ∈ listn(A); i = 0 ==> Q |] ==> Q

and Cons_listn_case:

      [| ⟨i, Cons(x, l)⟩ ∈ listn(A);
         !!n. [| x ∈ A; ⟨n, l⟩ ∈ listn(A); i = succ(n) |] ==> Q |]
      ==> Q

lemmas zero_listn_case:

      [| ⟨0, l⟩ ∈ listn(A); l = [] ==> Q |] ==> Q

and succ_listn_case:

      [| ⟨succ(i), l⟩ ∈ listn(A);
         !!a l. [| a ∈ A; ⟨i, l⟩ ∈ listn(A); l = Cons(a, l) |] ==> Q |]
      ==> Q