Theory ListN

theory ListN
imports Main
(*  Title:      ZF/Induct/ListN.thy
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 (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)"
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