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