|
(* Title: ZF/Induct/ListN.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
section \<open>Lists of n elements\<close>
theory ListN imports ZF begin
text \<open>
Inductive definition of lists of \<open>n\<close> elements; see
@{cite "paulin-tlca"}.
\<close>
consts listn :: "i=>i"
inductive
domains "listn(A)" \<subseteq> "nat \<times> list(A)"
intros
NilI: "<0,Nil> \ listn(A)"
ConsI: "[| a \ A; \ listn(A) |] ==> \ listn(A)"
type_intros nat_typechecks list.intros
lemma list_into_listn: "l \ list(A) ==> \ listn(A)"
by (induct set: list) (simp_all add: listn.intros)
lemma listn_iff: " \ 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:
"[| \ 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
Nil_listn_case: " \ listn(A)"
and Cons_listn_case: " \ listn(A)"
inductive_cases
zero_listn_case: "<0,l> \ listn(A)"
and succ_listn_case: " \ listn(A)"
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
