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/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 30 kB

Quelle equalities.thy Sprache: Isabelle

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

section\<open>Basic Equalities and Inclusions\<close>

theory equalities imports pair begin

text\<open>These cover union, intersection, converse, domain, range, etc.  Philippe
de Groote proved many of the inclusions.\<close>

lemma in_mono: "A\B \ x\A \ x\B"
by blast

lemma the_eq_0 [simp]: "(THE x. False) = 0"
by (blast intro: the_0)

subsection\<open>Bounded Quantifiers\<close>
text \<open>\medskip

  The following are not added to the default simpset because
  (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close>

lemma ball_Un: "(\x \ A\B. P(x)) \ (\x \ A. P(x)) \ (\x \ B. P(x))"
  by blast

lemma bex_Un: "(\x \ A\B. P(x)) \ (\x \ A. P(x)) | (\x \ B. P(x))"
  by blast

lemma ball_UN: "(\z \ (\x\A. B(x)). P(z)) \ (\x\A. \z \ B(x). P(z))"
  by blast

lemma bex_UN: "(\z \ (\x\A. B(x)). P(z)) \ (\x\A. \z\B(x). P(z))"
  by blast

subsection\<open>Converse of a Relation\<close>

lemma converse_iff [simp]: "\a,b\\ converse(r) \ \b,a\\r"
by (unfold converse_def, blast)

lemma converseI [intro!]: "\a,b\\r \ \b,a\\converse(r)"
by (unfold converse_def, blast)

lemma converseD: "\a,b\ \ converse(r) \ \b,a\ \ r"
by (unfold converse_def, blast)

lemma converseE [elim!]:
    "\yx \ converse(r);
        \<And>x y. \<lbrakk>yx=\<langle>y,x\<rangle>;  \<langle>x,y\<rangle>\<in>r\<rbrakk> \<Longrightarrow> P\<rbrakk>
     \<Longrightarrow> P"
by (unfold converse_def, blast)

lemma converse_converse: "r\Sigma(A,B) \ converse(converse(r)) = r"
by blast

lemma converse_type: "r\A*B \ converse(r)\B*A"
by blast

lemma converse_prod [simp]: "converse(A*B) = B*A"
by blast

lemma converse_empty [simp]: "converse(0) = 0"
by blast

lemma converse_subset_iff:
     "A \ Sigma(X,Y) \ converse(A) \ converse(B) \ A \ B"
by blast

subsection\<open>Finite Set Constructions Using \<^term>\<open>cons\<close>\<close>

lemma cons_subsetI: "\a\C; B\C\ \ cons(a,B) \ C"
by blast

lemma subset_consI: "B \ cons(a,B)"
by blast

lemma cons_subset_iff [iff]: "cons(a,B)\C \ a\C \ B\C"
by blast

(*A safe special case of subset elimination, adding no new variables
  \<lbrakk>cons(a,B) \<subseteq> C; \<lbrakk>a \<in> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R *)
lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]

lemma subset_empty_iff: "A\0 \ A=0"
by blast

lemma subset_cons_iff: "C\cons(a,B) \ C\B | (a\C \ C-{a} \ B)"
by blast

(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
lemma cons_eq: "{a} \ B = cons(a,B)"
by blast

lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"
by blast

lemma cons_absorb: "a: B \ cons(a,B) = B"
by blast

lemma cons_Diff: "a: B \ cons(a, B-{a}) = B"
by blast

lemma Diff_cons_eq: "cons(a,B) - C = (if a\C then B-C else cons(a,B-C))"
by auto

lemma equal_singleton: "\a: C; \y. y \C \ y=b\ \ C = {b}"
by blast

lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
by blast

(** singletons **)

lemma singleton_subsetI: "a\C \ {a} \ C"
by blast

lemma singleton_subsetD: "{a} \ C \ a\C"
by blast

(** succ **)

lemma subset_succI: "i \ succ(i)"
by blast

(*But if j is an ordinal or is transitive, then @{term"i\<in>j"} implies @{term"i\<subseteq>j"}!
  See @{text"Ord_succ_subsetI}*)
lemma succ_subsetI: "\i\j; i\j\ \ succ(i)\j"
by (unfold succ_def, blast)

lemma succ_subsetE:
    "\succ(i) \ j; \i\j; i\j\ \ P\ \ P"
by (unfold succ_def, blast)

lemma succ_subset_iff: "succ(a) \ B \ (a \ B \ a \ B)"
by (unfold succ_def, blast)

subsection\<open>Binary Intersection\<close>

(** Intersection is the greatest lower bound of two sets **)

lemma Int_subset_iff: "C \ A \ B \ C \ A \ C \ B"
by blast

lemma Int_lower1: "A \ B \ A"
by blast

lemma Int_lower2: "A \ B \ B"
by blast

lemma Int_greatest: "\C\A; C\B\ \ C \ A \ B"
by blast

lemma Int_cons: "cons(a,B) \ C \ cons(a, B \ C)"
by blast

lemma Int_absorb [simp]: "A \ A = A"
by blast

lemma Int_left_absorb: "A \ (A \ B) = A \ B"
by blast

lemma Int_commute: "A \ B = B \ A"
by blast

lemma Int_left_commute: "A \ (B \ C) = B \ (A \ C)"
by blast

lemma Int_assoc: "(A \ B) \ C = A \ (B \ C)"
by blast

(*Intersection is an AC-operator*)
lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute

lemma Int_absorb1: "B \ A \ A \ B = B"
  by blast

lemma Int_absorb2: "A \ B \ A \ B = A"
  by blast

lemma Int_Un_distrib: "A \ (B \ C) = (A \ B) \ (A \ C)"
by blast

lemma Int_Un_distrib2: "(B \ C) \ A = (B \ A) \ (C \ A)"
by blast

lemma subset_Int_iff: "A\B \ A \ B = A"
by (blast elim!: equalityE)

lemma subset_Int_iff2: "A\B \ B \ A = A"
by (blast elim!: equalityE)

lemma Int_Diff_eq: "C\A \ (A-B) \ C = C-B"
by blast

lemma Int_cons_left:
     "cons(a,A) \ B = (if a \ B then cons(a, A \ B) else A \ B)"
by auto

lemma Int_cons_right:
     "A \ cons(a, B) = (if a \ A then cons(a, A \ B) else A \ B)"
by auto

lemma cons_Int_distrib: "cons(x, A \ B) = cons(x, A) \ cons(x, B)"
by auto

subsection\<open>Binary Union\<close>

(** Union is the least upper bound of two sets *)

lemma Un_subset_iff: "A \ B \ C \ A \ C \ B \ C"
by blast

lemma Un_upper1: "A \ A \ B"
by blast

lemma Un_upper2: "B \ A \ B"
by blast

lemma Un_least: "\A\C; B\C\ \ A \ B \ C"
by blast

lemma Un_cons: "cons(a,B) \ C = cons(a, B \ C)"
by blast

lemma Un_absorb [simp]: "A \ A = A"
by blast

lemma Un_left_absorb: "A \ (A \ B) = A \ B"
by blast

lemma Un_commute: "A \ B = B \ A"
by blast

lemma Un_left_commute: "A \ (B \ C) = B \ (A \ C)"
by blast

lemma Un_assoc: "(A \ B) \ C = A \ (B \ C)"
by blast

(*Union is an AC-operator*)
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute

lemma Un_absorb1: "A \ B \ A \ B = B"
  by blast

lemma Un_absorb2: "B \ A \ A \ B = A"
  by blast

lemma Un_Int_distrib: "(A \ B) \ C = (A \ C) \ (B \ C)"
by blast

lemma subset_Un_iff: "A\B \ A \ B = B"
by (blast elim!: equalityE)

lemma subset_Un_iff2: "A\B \ B \ A = B"
by (blast elim!: equalityE)

lemma Un_empty [iff]: "(A \ B = 0) \ (A = 0 \ B = 0)"
by blast

lemma Un_eq_Union: "A \ B = \({A, B})"
by blast

subsection\<open>Set Difference\<close>

lemma Diff_subset: "A-B \ A"
by blast

lemma Diff_contains: "\C\A; C \ B = 0\ \ C \ A-B"
by blast

lemma subset_Diff_cons_iff: "B \ A - cons(c,C) \ B\A-C \ c \ B"
by blast

lemma Diff_cancel: "A - A = 0"
by blast

lemma Diff_triv: "A \ B = 0 \ A - B = A"
by blast

lemma empty_Diff [simp]: "0 - A = 0"
by blast

lemma Diff_0 [simp]: "A - 0 = A"
by blast

lemma Diff_eq_0_iff: "A - B = 0 \ A \ B"
by (blast elim: equalityE)

(*NOT SUITABLE FOR REWRITING since {a} \<equiv> cons(a,0)*)
lemma Diff_cons: "A - cons(a,B) = A - B - {a}"
by blast

(*NOT SUITABLE FOR REWRITING since {a} \<equiv> cons(a,0)*)
lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"
by blast

lemma Diff_disjoint: "A \ (B-A) = 0"
by blast

lemma Diff_partition: "A\B \ A \ (B-A) = B"
by blast

lemma subset_Un_Diff: "A \ B \ (A - B)"
by blast

lemma double_complement: "\A\B; B\C\ \ B-(C-A) = A"
by blast

lemma double_complement_Un: "(A \ B) - (B-A) = A"
by blast

lemma Un_Int_crazy:
"(A \ B) \ (B \ C) \ (C \ A) = (A \ B) \ (B \ C) \ (C \ A)"
apply blast
done

lemma Diff_Un: "A - (B \ C) = (A-B) \ (A-C)"
by blast

lemma Diff_Int: "A - (B \ C) = (A-B) \ (A-C)"
by blast

lemma Un_Diff: "(A \ B) - C = (A - C) \ (B - C)"
by blast

lemma Int_Diff: "(A \ B) - C = A \ (B - C)"
by blast

lemma Diff_Int_distrib: "C \ (A-B) = (C \ A) - (C \ B)"
by blast

lemma Diff_Int_distrib2: "(A-B) \ C = (A \ C) - (B \ C)"
by blast

(*Halmos, Naive Set Theory, page 16.*)
lemma Un_Int_assoc_iff: "(A \ B) \ C = A \ (B \ C) \ C\A"
by (blast elim!: equalityE)

subsection\<open>Big Union and Intersection\<close>

(** Big Union is the least upper bound of a set  **)

lemma Union_subset_iff: "\(A) \ C \ (\x\A. x \ C)"
by blast

lemma Union_upper: "B\A \ B \ \(A)"
by blast

lemma Union_least: "\\x. x\A \ x\C\ \ \(A) \ C"
by blast

lemma Union_cons [simp]: "\(cons(a,B)) = a \ \(B)"
by blast

lemma Union_Un_distrib: "\(A \ B) = \(A) \ \(B)"
by blast

lemma Union_Int_subset: "\(A \ B) \ \(A) \ \(B)"
by blast

lemma Union_disjoint: "\(C) \ A = 0 \ (\B\C. B \ A = 0)"
by (blast elim!: equalityE)

lemma Union_empty_iff: "\(A) = 0 \ (\B\A. B=0)"
by blast

lemma Int_Union2: "\(B) \ A = (\C\B. C \ A)"
by blast

(** Big Intersection is the greatest lower bound of a nonempty set **)

lemma Inter_subset_iff: "A\0 \ C \ \(A) \ (\x\A. C \ x)"
by blast

lemma Inter_lower: "B\A \ \(A) \ B"
by blast

lemma Inter_greatest: "\A\0; \x. x\A \ C\x\ \ C \ \(A)"
by blast

(** Intersection of a family of sets  **)

lemma INT_lower: "x\A \ (\x\A. B(x)) \ B(x)"
by blast

lemma INT_greatest: "\A\0; \x. x\A \ C\B(x)\ \ C \ (\x\A. B(x))"
by force

lemma Inter_0 [simp]: "\(0) = 0"
by (unfold Inter_def, blast)

lemma Inter_Un_subset:
     "\z\A; z\B\ \ \(A) \ \(B) \ \(A \ B)"
by blast

(* A good challenge: Inter is ill-behaved on the empty set *)
lemma Inter_Un_distrib:
     "\A\0; B\0\ \ \(A \ B) = \(A) \ \(B)"
by blast

lemma Union_singleton: "\({b}) = b"
by blast

lemma Inter_singleton: "\({b}) = b"
by blast

lemma Inter_cons [simp]:
     "\(cons(a,B)) = (if B=0 then a else a \ \(B))"
by force

subsection\<open>Unions and Intersections of Families\<close>

lemma subset_UN_iff_eq: "A \ (\i\I. B(i)) \ A = (\i\I. A \ B(i))"
by (blast elim!: equalityE)

lemma UN_subset_iff: "(\x\A. B(x)) \ C \ (\x\A. B(x) \ C)"
by blast

lemma UN_upper: "x\A \ B(x) \ (\x\A. B(x))"
by (erule RepFunI [THEN Union_upper])

lemma UN_least: "\\x. x\A \ B(x)\C\ \ (\x\A. B(x)) \ C"
by blast

lemma Union_eq_UN: "\(A) = (\x\A. x)"
by blast

lemma Inter_eq_INT: "\(A) = (\x\A. x)"
by (unfold Inter_def, blast)

lemma UN_0 [simp]: "(\i\0. A(i)) = 0"
by blast

lemma UN_singleton: "(\x\A. {x}) = A"
by blast

lemma UN_Un: "(\i\ A \ B. C(i)) = (\i\ A. C(i)) \ (\i\B. C(i))"
by blast

lemma INT_Un: "(\i\I \ J. A(i)) =
               (if I=0 then \<Inter>j\<in>J. A(j)
                       else if J=0 then \<Inter>i\<in>I. A(i)
                       else ((\<Inter>i\<in>I. A(i)) \<inter>  (\<Inter>j\<in>J. A(j))))"
by (simp, blast intro!: equalityI)

lemma UN_UN_flatten: "(\x \ (\y\A. B(y)). C(x)) = (\y\A. \x\ B(y). C(x))"
by blast

(*Halmos, Naive Set Theory, page 35.*)
lemma Int_UN_distrib: "B \ (\i\I. A(i)) = (\i\I. B \ A(i))"
by blast

lemma Un_INT_distrib: "I\0 \ B \ (\i\I. A(i)) = (\i\I. B \ A(i))"
by auto

lemma Int_UN_distrib2:
     "(\i\I. A(i)) \ (\j\J. B(j)) = (\i\I. \j\J. A(i) \ B(j))"
by blast

lemma Un_INT_distrib2: "\I\0; J\0\ \
      (\<Inter>i\<in>I. A(i)) \<union> (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) \<union> B(j))"
by auto

lemma UN_constant [simp]: "(\y\A. c) = (if A=0 then 0 else c)"
by force

lemma INT_constant [simp]: "(\y\A. c) = (if A=0 then 0 else c)"
by force

lemma UN_RepFun [simp]: "(\y\ RepFun(A,f). B(y)) = (\x\A. B(f(x)))"
by blast

lemma INT_RepFun [simp]: "(\x\RepFun(A,f). B(x)) = (\a\A. B(f(a)))"
by (auto simp add: Inter_def)

lemma INT_Union_eq:
     "0 \ A \ (\x\ \(A). B(x)) = (\y\A. \x\y. B(x))"
apply (subgoal_tac "\x\A. x\0")
   prefer 2 apply blast
apply (force simp add: Inter_def ball_conj_distrib)
done

lemma INT_UN_eq:
     "(\x\A. B(x) \ 0)
      \<Longrightarrow> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))"
apply (subst INT_Union_eq, blast)
apply (simp add: Inter_def)
done

(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
    Union of a family of unions **)

lemma UN_Un_distrib:
     "(\i\I. A(i) \ B(i)) = (\i\I. A(i)) \ (\i\I. B(i))"
by blast

lemma INT_Int_distrib:
     "I\0 \ (\i\I. A(i) \ B(i)) = (\i\I. A(i)) \ (\i\I. B(i))"
by (blast elim!: not_emptyE)

lemma UN_Int_subset:
     "(\z\I \ J. A(z)) \ (\z\I. A(z)) \ (\z\J. A(z))"
by blast

(** Devlin, page 12, exercise 5: Complements **)

lemma Diff_UN: "I\0 \ B - (\i\I. A(i)) = (\i\I. B - A(i))"
by (blast elim!: not_emptyE)

lemma Diff_INT: "I\0 \ B - (\i\I. A(i)) = (\i\I. B - A(i))"
by (blast elim!: not_emptyE)

(** Unions and Intersections with General Sum **)

(*Not suitable for rewriting: LOOPS!*)
lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) \ Sigma(B,C)"
by blast

(*Not suitable for rewriting: LOOPS!*)
lemma Sigma_cons2: "A * cons(b,B) = A*{b} \ A*B"
by blast

lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) \ Sigma(A,B)"
by blast

lemma Sigma_succ2: "A * succ(B) = A*{B} \ A*B"
by blast

lemma SUM_UN_distrib1:
     "(\x \ (\y\A. C(y)). B(x)) = (\y\A. \x\C(y). B(x))"
by blast

lemma SUM_UN_distrib2:
     "(\i\I. \j\J. C(i,j)) = (\j\J. \i\I. C(i,j))"
by blast

lemma SUM_Un_distrib1:
     "(\i\I \ J. C(i)) = (\i\I. C(i)) \ (\j\J. C(j))"
by blast

lemma SUM_Un_distrib2:
     "(\i\I. A(i) \ B(i)) = (\i\I. A(i)) \ (\i\I. B(i))"
by blast

(*First-order version of the above, for rewriting*)
lemma prod_Un_distrib2: "I * (A \ B) = I*A \ I*B"
by (rule SUM_Un_distrib2)

lemma SUM_Int_distrib1:
     "(\i\I \ J. C(i)) = (\i\I. C(i)) \ (\j\J. C(j))"
by blast

lemma SUM_Int_distrib2:
     "(\i\I. A(i) \ B(i)) = (\i\I. A(i)) \ (\i\I. B(i))"
by blast

(*First-order version of the above, for rewriting*)
lemma prod_Int_distrib2: "I * (A \ B) = I*A \ I*B"
by (rule SUM_Int_distrib2)

(*Cf Aczel, Non-Well-Founded Sets, page 115*)
lemma SUM_eq_UN: "(\i\I. A(i)) = (\i\I. {i} * A(i))"
by blast

lemma times_subset_iff:
     "(A'*B' \ A*B) \ (A' = 0 | B' = 0 | (A'\A) \ (B'\B))"
by blast

lemma Int_Sigma_eq:
     "(\x \ A'. B'(x)) \ (\x \ A. B(x)) = (\x \ A' \ A. B'(x) \ B(x))"
by blast

(** Domain **)

lemma domain_iff: "a: domain(r) \ (\y. \a,y\\ r)"
by (unfold domain_def, blast)

lemma domainI [intro]: "\a,b\\ r \ a: domain(r)"
by (unfold domain_def, blast)

lemma domainE [elim!]:
    "\a \ domain(r); \y. \a,y\\ r \ P\ \ P"
by (unfold domain_def, blast)

lemma domain_subset: "domain(Sigma(A,B)) \ A"
by blast

lemma domain_of_prod: "b\B \ domain(A*B) = A"
by blast

lemma domain_0 [simp]: "domain(0) = 0"
by blast

lemma domain_cons [simp]: "domain(cons(\a,b\,r)) = cons(a, domain(r))"
by blast

lemma domain_Un_eq [simp]: "domain(A \ B) = domain(A) \ domain(B)"
by blast

lemma domain_Int_subset: "domain(A \ B) \ domain(A) \ domain(B)"
by blast

lemma domain_Diff_subset: "domain(A) - domain(B) \ domain(A - B)"
by blast

lemma domain_UN: "domain(\x\A. B(x)) = (\x\A. domain(B(x)))"
by blast

lemma domain_Union: "domain(\(A)) = (\x\A. domain(x))"
by blast

(** Range **)

lemma rangeI [intro]: "\a,b\\ r \ b \ range(r)"
  unfolding range_def
apply (erule converseI [THEN domainI])
done

lemma rangeE [elim!]: "\b \ range(r); \x. \x,b\\ r \ P\ \ P"
by (unfold range_def, blast)

lemma range_subset: "range(A*B) \ B"
  unfolding range_def
apply (subst converse_prod)
apply (rule domain_subset)
done

lemma range_of_prod: "a\A \ range(A*B) = B"
by blast

lemma range_0 [simp]: "range(0) = 0"
by blast

lemma range_cons [simp]: "range(cons(\a,b\,r)) = cons(b, range(r))"
by blast

lemma range_Un_eq [simp]: "range(A \ B) = range(A) \ range(B)"
by blast

lemma range_Int_subset: "range(A \ B) \ range(A) \ range(B)"
by blast

lemma range_Diff_subset: "range(A) - range(B) \ range(A - B)"
by blast

lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
by blast

lemma range_converse [simp]: "range(converse(r)) = domain(r)"
by blast

(** Field **)

lemma fieldI1: "\a,b\\ r \ a \ field(r)"
by (unfold field_def, blast)

lemma fieldI2: "\a,b\\ r \ b \ field(r)"
by (unfold field_def, blast)

lemma fieldCI [intro]:
    "(\ \c,a\\r \ \a,b\\ r) \ a \ field(r)"
apply (unfold field_def, blast)
done

lemma fieldE [elim!]:
     "\a \ field(r);
         \<And>x. \<langle>a,x\<rangle>\<in> r \<Longrightarrow> P;
         \<And>x. \<langle>x,a\<rangle>\<in> r \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (unfold field_def, blast)

lemma field_subset: "field(A*B) \ A \ B"
by blast

lemma domain_subset_field: "domain(r) \ field(r)"
  unfolding field_def
apply (rule Un_upper1)
done

lemma range_subset_field: "range(r) \ field(r)"
  unfolding field_def
apply (rule Un_upper2)
done

lemma domain_times_range: "r \ Sigma(A,B) \ r \ domain(r)*range(r)"
by blast

lemma field_times_field: "r \ Sigma(A,B) \ r \ field(r)*field(r)"
by blast

lemma relation_field_times_field: "relation(r) \ r \ field(r)*field(r)"
by (simp add: relation_def, blast)

lemma field_of_prod: "field(A*A) = A"
by blast

lemma field_0 [simp]: "field(0) = 0"
by blast

lemma field_cons [simp]: "field(cons(\a,b\,r)) = cons(a, cons(b, field(r)))"
by blast

lemma field_Un_eq [simp]: "field(A \ B) = field(A) \ field(B)"
by blast

lemma field_Int_subset: "field(A \ B) \ field(A) \ field(B)"
by blast

lemma field_Diff_subset: "field(A) - field(B) \ field(A - B)"
by blast

lemma field_converse [simp]: "field(converse(r)) = field(r)"
by blast

(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
lemma rel_Union: "(\x\S. \A B. x \ A*B) \
                  \<Union>(S) \<subseteq> domain(\<Union>(S)) * range(\<Union>(S))"
by blast

(** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
lemma rel_Un: "\r \ A*B; s \ C*D\ \ (r \ s) \ (A \ C) * (B \ D)"
by blast

lemma domain_Diff_eq: "\\a,c\ \ r; c\b\ \ domain(r-{\a,b\}) = domain(r)"
by blast

lemma range_Diff_eq: "\\c,b\ \ r; c\a\ \ range(r-{\a,b\}) = range(r)"
by blast

subsection\<open>Image of a Set under a Function or Relation\<close>

lemma image_iff: "b \ r``A \ (\x\A. \x,b\\r)"
by (unfold image_def, blast)

lemma image_singleton_iff: "b \ r``{a} \ \a,b\\r"
by (rule image_iff [THEN iff_trans], blast)

lemma imageI [intro]: "\\a,b\\ r; a\A\ \ b \ r``A"
by (unfold image_def, blast)

lemma imageE [elim!]:
    "\b: r``A; \x.\\x,b\\ r; x\A\ \ P\ \ P"
by (unfold image_def, blast)

lemma image_subset: "r \ A*B \ r``C \ B"
by blast

lemma image_0 [simp]: "r``0 = 0"
by blast

lemma image_Un [simp]: "r``(A \ B) = (r``A) \ (r``B)"
by blast

lemma image_UN: "r `` (\x\A. B(x)) = (\x\A. r `` B(x))"
by blast

lemma Collect_image_eq:
     "{z \ Sigma(A,B). P(z)} `` C = (\x \ A. {y \ B(x). x \ C \ P(\x,y\)})"
by blast

lemma image_Int_subset: "r``(A \ B) \ (r``A) \ (r``B)"
by blast

lemma image_Int_square_subset: "(r \ A*A)``B \ (r``B) \ A"
by blast

lemma image_Int_square: "B\A \ (r \ A*A)``B = (r``B) \ A"
by blast

(*Image laws for special relations*)
lemma image_0_left [simp]: "0``A = 0"
by blast

lemma image_Un_left: "(r \ s)``A = (r``A) \ (s``A)"
by blast

lemma image_Int_subset_left: "(r \ s)``A \ (r``A) \ (s``A)"
by blast

subsection\<open>Inverse Image of a Set under a Function or Relation\<close>

lemma vimage_iff:
    "a \ r-``B \ (\y\B. \a,y\\r)"
by (unfold vimage_def image_def converse_def, blast)

lemma vimage_singleton_iff: "a \ r-``{b} \ \a,b\\r"
by (rule vimage_iff [THEN iff_trans], blast)

lemma vimageI [intro]: "\\a,b\\ r; b\B\ \ a \ r-``B"
by (unfold vimage_def, blast)

lemma vimageE [elim!]:
    "\a: r-``B; \x.\\a,x\\ r; x\B\ \ P\ \ P"
apply (unfold vimage_def, blast)
done

lemma vimage_subset: "r \ A*B \ r-``C \ A"
  unfolding vimage_def
apply (erule converse_type [THEN image_subset])
done

lemma vimage_0 [simp]: "r-``0 = 0"
by blast

lemma vimage_Un [simp]: "r-``(A \ B) = (r-``A) \ (r-``B)"
by blast

lemma vimage_Int_subset: "r-``(A \ B) \ (r-``A) \ (r-``B)"
by blast

(*NOT suitable for rewriting*)
lemma vimage_eq_UN: "f -``B = (\y\B. f-``{y})"
by blast

lemma function_vimage_Int:
     "function(f) \ f-``(A \ B) = (f-``A) \ (f-``B)"
by (unfold function_def, blast)

lemma function_vimage_Diff: "function(f) \ f-``(A-B) = (f-``A) - (f-``B)"
by (unfold function_def, blast)

lemma function_image_vimage: "function(f) \ f `` (f-`` A) \ A"
by (unfold function_def, blast)

lemma vimage_Int_square_subset: "(r \ A*A)-``B \ (r-``B) \ A"
by blast

lemma vimage_Int_square: "B\A \ (r \ A*A)-``B = (r-``B) \ A"
by blast

(*Invese image laws for special relations*)
lemma vimage_0_left [simp]: "0-``A = 0"
by blast

lemma vimage_Un_left: "(r \ s)-``A = (r-``A) \ (s-``A)"
by blast

lemma vimage_Int_subset_left: "(r \ s)-``A \ (r-``A) \ (s-``A)"
by blast

(** Converse **)

lemma converse_Un [simp]: "converse(A \ B) = converse(A) \ converse(B)"
by blast

lemma converse_Int [simp]: "converse(A \ B) = converse(A) \ converse(B)"
by blast

lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
by blast

lemma converse_UN [simp]: "converse(\x\A. B(x)) = (\x\A. converse(B(x)))"
by blast

(*Unfolding Inter avoids using excluded middle on A=0*)
lemma converse_INT [simp]:
     "converse(\x\A. B(x)) = (\x\A. converse(B(x)))"
apply (unfold Inter_def, blast)
done

subsection\<open>Powerset Operator\<close>

lemma Pow_0 [simp]: "Pow(0) = {0}"
by blast

lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) \ {cons(a,X) . X: Pow(A)}"
apply (rule equalityI, safe)
apply (erule swap)
apply (rule_tac a = "x-{a}" in RepFun_eqI, auto)
done

lemma Un_Pow_subset: "Pow(A) \ Pow(B) \ Pow(A \ B)"
by blast

lemma UN_Pow_subset: "(\x\A. Pow(B(x))) \ Pow(\x\A. B(x))"
by blast

lemma subset_Pow_Union: "A \ Pow(\(A))"
by blast

lemma Union_Pow_eq [simp]: "\(Pow(A)) = A"
by blast

lemma Union_Pow_iff: "\(A) \ Pow(B) \ A \ Pow(Pow(B))"
by blast

lemma Pow_Int_eq [simp]: "Pow(A \ B) = Pow(A) \ Pow(B)"
by blast

lemma Pow_INT_eq: "A\0 \ Pow(\x\A. B(x)) = (\x\A. Pow(B(x)))"
by (blast elim!: not_emptyE)

subsection\<open>RepFun\<close>

lemma RepFun_subset: "\\x. x\A \ f(x) \ B\ \ {f(x). x\A} \ B"
by blast

lemma RepFun_eq_0_iff [simp]: "{f(x).x\A}=0 \ A=0"
by blast

lemma RepFun_constant [simp]: "{c. x\A} = (if A=0 then 0 else {c})"
by force

subsection\<open>Collect\<close>

lemma Collect_subset: "Collect(A,P) \ A"
by blast

lemma Collect_Un: "Collect(A \ B, P) = Collect(A,P) \ Collect(B,P)"
by blast

lemma Collect_Int: "Collect(A \ B, P) = Collect(A,P) \ Collect(B,P)"
by blast

lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"
by blast

lemma Collect_cons: "{x\cons(a,B). P(x)} =
      (if P(a) then cons(a, {x\<in>B. P(x)}) else {x\<in>B. P(x)})"
by (simp, blast)

lemma Int_Collect_self_eq: "A \ Collect(A,P) = Collect(A,P)"
by blast

lemma Collect_Collect_eq [simp]:
     "Collect(Collect(A,P), Q) = Collect(A, \x. P(x) \ Q(x))"
by blast

lemma Collect_Int_Collect_eq:
     "Collect(A,P) \ Collect(A,Q) = Collect(A, \x. P(x) \ Q(x))"
by blast

lemma Collect_Union_eq [simp]:
     "Collect(\x\A. B(x), P) = (\x\A. Collect(B(x), P))"
by blast

lemma Collect_Int_left: "{x\A. P(x)} \ B = {x \ A \ B. P(x)}"
by blast

lemma Collect_Int_right: "A \ {x\B. P(x)} = {x \ A \ B. P(x)}"
by blast

lemma Collect_disj_eq: "{x\A. P(x) | Q(x)} = Collect(A, P) \ Collect(A, Q)"
by blast

lemma Collect_conj_eq: "{x\A. P(x) \ Q(x)} = Collect(A, P) \ Collect(A, Q)"
by blast

lemmas subset_SIs = subset_refl cons_subsetI subset_consI
                    Union_least UN_least Un_least
                    Inter_greatest Int_greatest RepFun_subset
                    Un_upper1 Un_upper2 Int_lower1 Int_lower2

ML \<open>
val subset_cs =
  claset_of (\<^context>
    delrules [@{thm subsetI}, @{thm subsetCE}]
    addSIs @{thms subset_SIs}
    addIs  [@{thm Union_upper}, @{thm Inter_lower}]
    addSEs [@{thm cons_subsetE}]);

val ZF_cs = claset_of (\<^context> delrules [@{thm equalityI}]);
\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.17 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.