Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/ZF/Induct/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

Quellcode-Bibliothek ListN.thy Sprache: Isabelle

(*  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>\<open>"paulin-tlca"\<close>.
\<close>

consts listn :: "i\i"
inductive
  domains "listn(A)" \<subseteq> "nat \<times> list(A)"
  intros
    NilI: "\0,Nil\ \ listn(A)"
    ConsI: "\a \ A; \n,l\ \ 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: "\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)"
    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
      Nil_listn_case: "\i,Nil\ \ listn(A)"
  and Cons_listn_case: " \ listn(A)"

inductive_cases
      zero_listn_case: "\0,l\ \ listn(A)"
  and succ_listn_case: " \ listn(A)"

end

quality97%

¤ 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.0.14Bemerkung: (vorverarbeitet) ¤

Versionsinformation zu Columbo

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.