1(*  Title:      ZF/Induct/ListN.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1994  University of Cambridge
4*)
5
6section \<open>Lists of n elements\<close>
7
8theory ListN imports ZF begin
9
10text \<open>
11  Inductive definition of lists of \<open>n\<close> elements; see
12  @{cite "paulin-tlca"}.
13\<close>
14
15consts listn :: "i=>i"
16inductive
17  domains "listn(A)" \<subseteq> "nat \<times> list(A)"
18  intros
19    NilI: "<0,Nil> \<in> listn(A)"
20    ConsI: "[| a \<in> A; <n,l> \<in> listn(A) |] ==> <succ(n), Cons(a,l)> \<in> listn(A)"
21  type_intros nat_typechecks list.intros
22
23
24lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)"
25  by (induct set: list) (simp_all add: listn.intros)
26
27lemma listn_iff: "<n,l> \<in> listn(A) \<longleftrightarrow> l \<in> list(A) & length(l)=n"
28  apply (rule iffI)
29   apply (erule listn.induct)
30    apply auto
31  apply (blast intro: list_into_listn)
32  done
33
34lemma listn_image_eq: "listn(A)``{n} = {l \<in> list(A). length(l)=n}"
35  apply (rule equality_iffI)
36  apply (simp add: listn_iff separation image_singleton_iff)
37  done
38
39lemma listn_mono: "A \<subseteq> B ==> listn(A) \<subseteq> listn(B)"
40  apply (unfold listn.defs)
41  apply (rule lfp_mono)
42    apply (rule listn.bnd_mono)+
43  apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+
44  done
45
46lemma listn_append:
47    "[| <n,l> \<in> listn(A); <n',l'> \<in> listn(A) |] ==> <n#+n', l@l'> \<in> listn(A)"
48  apply (erule listn.induct)
49   apply (frule listn.dom_subset [THEN subsetD])
50   apply (simp_all add: listn.intros)
51  done
52
53inductive_cases
54      Nil_listn_case: "<i,Nil> \<in> listn(A)"
55  and Cons_listn_case: "<i,Cons(x,l)> \<in> listn(A)"
56
57inductive_cases
58      zero_listn_case: "<0,l> \<in> listn(A)"
59  and succ_listn_case: "<succ(i),l> \<in> listn(A)"
60
61end
62