(* Title: ZF/Induct/ListN.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge \<open>Lists of n elements\<close> theory ListN imports ZF begin text \<open> Inductive definition of lists of \<open>n\<close> elements; see \<^cite>\<open>"paulin-tlca"\<close>. \<close> consts listn :: "i\i" inductive "listn(A)" \<subseteq> "nat \<times> list(A)" intros "\0,Nil\ \ listn(A)" "\a \ A; \n,l\ \ listn(A)\ \ \ listn(A)" 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 autoapply (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 "\i,Nil\ \ listn(A)" and Cons_listn_case: " \ listn(A)" inductive_cases "\0,l\ \ listn(A)" and succ_listn_case: " \ listn(A)" end quality 97%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
