Quelle Sum.thy Sprache: Isabelle

(*  Title:      ZF/Sum.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge
*)

section\<open>Disjoint Sums\<close>

theory Sum imports Bool equalities begin

text\<open>And the "Part" primitive for simultaneous recursive type definitions\<close>

definition sum :: "[i,i]\i" (infixr \+\ 65) where
     "A+B \ {0}*A \ {1}*B"

definition Inl :: "i\i" where
     "Inl(a) \ \0,a\"

definition Inr :: "i\i" where
     "Inr(b) \ \1,b\"

definition "case" :: "[i\i, i\i, i]\i" where
     "case(c,d) \ (\\y,z\. cond(y, d(z), c(z)))"

  (*operator for selecting out the various summands*)
definition Part :: "[i,i\i] \ i" where
     "Part(A,h) \ {x \ A. \z. x = h(z)}"

subsection\<open>Rules for the \<^term>\<open>Part\<close> Primitive\<close>

lemma Part_iff:
    "a \ Part(A,h) \ a \ A \ (\y. a=h(y))"
  unfolding Part_def
apply (rule separation)
done

lemma Part_eqI [intro]:
    "\a \ A; a=h(b)\ \ a \ Part(A,h)"
by (unfold Part_def, blast)

lemmas PartI = refl [THEN [2] Part_eqI]

lemma PartE [elim!]:
    "\a \ Part(A,h); \z. \a \ A; a=h(z)\ \ P
\<rbrakk> \<Longrightarrow> P"
apply (unfold Part_def, blast)
done

lemma Part_subset: "Part(A,h) \ A"
  unfolding Part_def
apply (rule Collect_subset)
done

subsection\<open>Rules for Disjoint Sums\<close>

lemmas sum_defs = sum_def Inl_def Inr_def case_def

lemma Sigma_bool: "Sigma(bool,C) = C(0) + C(1)"
by (unfold bool_def sum_def, blast)

(** Introduction rules for the injections **)

lemma InlI [intro!,simp,TC]: "a \ A \ Inl(a) \ A+B"
by (unfold sum_defs, blast)

lemma InrI [intro!,simp,TC]: "b \ B \ Inr(b) \ A+B"
by (unfold sum_defs, blast)

(** Elimination rules **)

lemma sumE [elim!]:
    "\u \ A+B;
        \<And>x. \<lbrakk>x \<in> A;  u=Inl(x)\<rbrakk> \<Longrightarrow> P;
        \<And>y. \<lbrakk>y \<in> B;  u=Inr(y)\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
by (unfold sum_defs, blast)

(** Injection and freeness equivalences, for rewriting **)

lemma Inl_iff [iff]: "Inl(a)=Inl(b) \ a=b"
by (simp add: sum_defs)

lemma Inr_iff [iff]: "Inr(a)=Inr(b) \ a=b"
by (simp add: sum_defs)

lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) \ False"
by (simp add: sum_defs)

lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) \ False"
by (simp add: sum_defs)

lemma sum_empty [simp]: "0+0 = 0"
by (simp add: sum_defs)

(*Injection and freeness rules*)

lemmas Inl_inject = Inl_iff [THEN iffD1]
lemmas Inr_inject = Inr_iff [THEN iffD1]
lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]

lemma InlD: "Inl(a): A+B \ a \ A"
by blast

lemma InrD: "Inr(b): A+B \ b \ B"
by blast

lemma sum_iff: "u \ A+B \ (\x. x \ A \ u=Inl(x)) | (\y. y \ B \ u=Inr(y))"
by blast

lemma Inl_in_sum_iff [simp]: "(Inl(x) \ A+B) \ (x \ A)"
by auto

lemma Inr_in_sum_iff [simp]: "(Inr(y) \ A+B) \ (y \ B)"
by auto

lemma sum_subset_iff: "A+B \ C+D \ A<=C \ B<=D"
by blast

lemma sum_equal_iff: "A+B = C+D \ A=C \ B=D"
by (simp add: extension sum_subset_iff, blast)

lemma sum_eq_2_times: "A+A = 2*A"
by (simp add: sum_def, blast)

subsection\<open>The Eliminator: \<^term>\<open>case\<close>\<close>

lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"
by (simp add: sum_defs)

lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)"
by (simp add: sum_defs)

lemma case_type [TC]:
    "\u \ A+B;
        \<And>x. x \<in> A \<Longrightarrow> c(x): C(Inl(x));
        \<And>y. y \<in> B \<Longrightarrow> d(y): C(Inr(y))
\<rbrakk> \<Longrightarrow> case(c,d,u) \<in> C(u)"
by auto

lemma expand_case: "u \ A+B \
        R(case(c,d,u)) \<longleftrightarrow>
        ((\<forall>x\<in>A. u = Inl(x) \<longrightarrow> R(c(x))) \<and>
        (\<forall>y\<in>B. u = Inr(y) \<longrightarrow> R(d(y))))"
by auto

lemma case_cong:
  "\z \ A+B;
      \<And>x. x \<in> A \<Longrightarrow> c(x)=c'(x);
      \<And>y. y \<in> B \<Longrightarrow> d(y)=d'(y)
\<rbrakk> \<Longrightarrow> case(c,d,z) = case(c',d',z)"
by auto

lemma case_case: "z \ A+B \
        case(c, d, case(\<lambda>x. Inl(c'(x)), \<lambda>y. Inr(d'(y)), z)) =
        case(\<lambda>x. c(c'(x)), \<lambda>y. d(d'(y)), z)"
by auto

subsection\<open>More Rules for \<^term>\<open>Part(A,h)\<close>\<close>

lemma Part_mono: "A<=B \ Part(A,h)<=Part(B,h)"
by blast

lemma Part_Collect: "Part(Collect(A,P), h) = Collect(Part(A,h), P)"
by blast

lemmas Part_CollectE =
     Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE]

lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x \ A}"
by blast

lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y \ B}"
by blast

lemma PartD1: "a \ Part(A,h) \ a \ A"
by (simp add: Part_def)

lemma Part_id: "Part(A,\x. x) = A"
by blast

lemma Part_Inr2: "Part(A+B, \x. Inr(h(x))) = {Inr(y). y \ Part(B,h)}"
by blast

lemma Part_sum_equality: "C \ A+B \ Part(C,Inl) \ Part(C,Inr) = C"
by blast

end

quality97%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.