Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: range.pvs Sprache: Isabelle

Original von: Isabelle^©

section \<open>Extending FOL by a modified version of HOL set theory\<close>

theory Set
imports FOL
begin

declare [[eta_contract]]

typedecl 'a set
instance set :: ("term") "term" ..

subsection \<open>Set comprehension and membership\<close>

axiomatization Collect :: "['a \ o] \ 'a set"
  and mem :: "['a, 'a set] \ o" (infixl ":" 50)
where mem_Collect_iff: "(a : Collect(P)) \ P(a)"
  and set_extension: "A = B \ (ALL x. x:A \ x:B)"

syntax
  "_Coll" :: "[idt, o] \ 'a set" ("(1{_./ _})")
translations
  "{x. P}" == "CONST Collect(\x. P)"

lemma CollectI: "P(a) \ a : {x. P(x)}"
  apply (rule mem_Collect_iff [THEN iffD2])
  apply assumption
  done

lemma CollectD: "a : {x. P(x)} \ P(a)"
  apply (erule mem_Collect_iff [THEN iffD1])
  done

lemmas CollectE = CollectD [elim_format]

lemma set_ext: "(\x. x:A \ x:B) \ A = B"
  apply (rule set_extension [THEN iffD2])
  apply simp
  done

subsection \<open>Bounded quantifiers\<close>

definition Ball :: "['a set, 'a \ o] \ o"
  where "Ball(A, P) == ALL x. x:A \ P(x)"

definition Bex :: "['a set, 'a \ o] \ o"
  where "Bex(A, P) == EX x. x:A \ P(x)"

syntax
  "_Ball" :: "[idt, 'a set, o] \ o" ("(ALL _:_./ _)" [0, 0, 0] 10)
  "_Bex" :: "[idt, 'a set, o] \ o" ("(EX _:_./ _)" [0, 0, 0] 10)
translations
  "ALL x:A. P"  == "CONST Ball(A, \x. P)"
  "EX x:A. P"   == "CONST Bex(A, \x. P)"

lemma ballI: "(\x. x:A \ P(x)) \ ALL x:A. P(x)"
  by (simp add: Ball_def)

lemma bspec: "\ALL x:A. P(x); x:A\ \ P(x)"
  by (simp add: Ball_def)

lemma ballE: "\ALL x:A. P(x); P(x) \ Q; \ x:A \ Q\ \ Q"
  unfolding Ball_def by blast

lemma bexI: "\P(x); x:A\ \ EX x:A. P(x)"
  unfolding Bex_def by blast

lemma bexCI: "\EX x:A. \P(x) \ P(a); a:A\ \ EX x:A. P(x)"
  unfolding Bex_def by blast

lemma bexE: "\EX x:A. P(x); \x. \x:A; P(x)\ \ Q\ \ Q"
  unfolding Bex_def by blast

(*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
lemma ball_rew: "(ALL x:A. True) \ True"
  by (blast intro: ballI)

subsubsection \<open>Congruence rules\<close>

lemma ball_cong:
  "\A = A'; \x. x:A' \ P(x) \ P'(x)\ \
    (ALL x:A. P(x)) \<longleftrightarrow> (ALL x:A'. P'(x))"
  by (blast intro: ballI elim: ballE)

lemma bex_cong:
  "\A = A'; \x. x:A' \ P(x) \ P'(x)\ \
    (EX x:A. P(x)) \<longleftrightarrow> (EX x:A'. P'(x))"
  by (blast intro: bexI elim: bexE)

subsection \<open>Further operations\<close>

definition subset :: "['a set, 'a set] \ o" (infixl "<=" 50)
  where "A <= B == ALL x:A. x:B"

definition mono :: "['a set \ 'b set] \ o"
  where "mono(f) == (ALL A B. A <= B \ f(A) <= f(B))"

definition singleton :: "'a \ 'a set" ("{_}")
  where "{a} == {x. x=a}"

definition empty :: "'a set"  ("{}")
  where "{} == {x. False}"

definition Un :: "['a set, 'a set] \ 'a set" (infixl "Un" 65)
  where "A Un B == {x. x:A | x:B}"

definition Int :: "['a set, 'a set] \ 'a set" (infixl "Int" 70)
  where "A Int B == {x. x:A \ x:B}"

definition Compl :: "('a set) \ 'a set"
  where "Compl(A) == {x. \x:A}"

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

definition INTER :: "['a set, 'a \ 'b set] \ 'b set"
  where "INTER(A, B) == {y. ALL x:A. y: B(x)}"

definition UNION :: "['a set, 'a \ 'b set] \ 'b set"
  where "UNION(A, B) == {y. EX x:A. y: B(x)}"

syntax
  "_INTER" :: "[idt, 'a set, 'b set] \ 'b set" ("(INT _:_./ _)" [0, 0, 0] 10)
  "_UNION" :: "[idt, 'a set, 'b set] \ 'b set" ("(UN _:_./ _)" [0, 0, 0] 10)
translations
  "INT x:A. B" == "CONST INTER(A, \x. B)"
  "UN x:A. B" == "CONST UNION(A, \x. B)"

definition Inter :: "(('a set)set) \ 'a set"
  where "Inter(S) == (INT x:S. x)"

definition Union :: "(('a set)set) \ 'a set"
  where "Union(S) == (UN x:S. x)"

subsection \<open>Rules for subsets\<close>

lemma subsetI: "(\x. x:A \ x:B) \ A <= B"
  unfolding subset_def by (blast intro: ballI)

(*Rule in Modus Ponens style*)
lemma subsetD: "\A <= B; c:A\ \ c:B"
  unfolding subset_def by (blast elim: ballE)

(*Classical elimination rule*)
lemma subsetCE: "\A <= B; \(c:A) \ P; c:B \ P\ \ P"
  by (blast dest: subsetD)

lemma subset_refl: "A <= A"
  by (blast intro: subsetI)

lemma subset_trans: "\A <= B; B <= C\ \ A <= C"
  by (blast intro: subsetI dest: subsetD)

subsection \<open>Rules for equality\<close>

(*Anti-symmetry of the subset relation*)
lemma subset_antisym: "\A <= B; B <= A\ \ A = B"
  by (blast intro: set_ext dest: subsetD)

lemmas equalityI = subset_antisym

(* Equality rules from ZF set theory -- are they appropriate here? *)
lemma equalityD1: "A = B \ A<=B"
  and equalityD2: "A = B \ B<=A"
  by (simp_all add: subset_refl)

lemma equalityE: "\A = B; \A <= B; B <= A\ \ P\ \ P"
  by (simp add: subset_refl)

lemma equalityCE: "\A = B; \c:A; c:B\ \ P; \\ c:A; \ c:B\ \ P\ \ P"
  by (blast elim: equalityE subsetCE)

lemma trivial_set: "{x. x:A} = A"
  by (blast intro: equalityI subsetI CollectI dest: CollectD)

subsection \<open>Rules for binary union\<close>

lemma UnI1: "c:A \ c : A Un B"
  and UnI2: "c:B \ c : A Un B"
  unfolding Un_def by (blast intro: CollectI)+

(*Classical introduction rule: no commitment to A vs B*)
lemma UnCI: "(\c:B \ c:A) \ c : A Un B"
  by (blast intro: UnI1 UnI2)

lemma UnE: "\c : A Un B; c:A \ P; c:B \ P\ \ P"
  unfolding Un_def by (blast dest: CollectD)

subsection \<open>Rules for small intersection\<close>

lemma IntI: "\c:A; c:B\ \ c : A Int B"
  unfolding Int_def by (blast intro: CollectI)

lemma IntD1: "c : A Int B \ c:A"
  and IntD2: "c : A Int B \ c:B"
  unfolding Int_def by (blast dest: CollectD)+

lemma IntE: "\c : A Int B; \c:A; c:B\ \ P\ \ P"
  by (blast dest: IntD1 IntD2)

subsection \<open>Rules for set complement\<close>

lemma ComplI: "(c:A \ False) \ c : Compl(A)"
  unfolding Compl_def by (blast intro: CollectI)

(*This form, with negated conclusion, works well with the Classical prover.
  Negated assumptions behave like formulae on the right side of the notional
  turnstile...*)
lemma ComplD: "c : Compl(A) \ \c:A"
  unfolding Compl_def by (blast dest: CollectD)

lemmas ComplE = ComplD [elim_format]

subsection \<open>Empty sets\<close>

lemma empty_eq: "{x. False} = {}"
  by (simp add: empty_def)

lemma emptyD: "a : {} \ P"
  unfolding empty_def by (blast dest: CollectD)

lemmas emptyE = emptyD [elim_format]

lemma not_emptyD:
  assumes "\ A={}"
  shows "EX x. x:A"
proof -
  have "\ (EX x. x:A) \ A = {}"
    by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+
  with assms show ?thesis by blast
qed

subsection \<open>Singleton sets\<close>

lemma singletonI: "a : {a}"
  unfolding singleton_def by (blast intro: CollectI)

lemma singletonD: "b : {a} \ b=a"
  unfolding singleton_def by (blast dest: CollectD)

lemmas singletonE = singletonD [elim_format]

subsection \<open>Unions of families\<close>

(*The order of the premises presupposes that A is rigid; b may be flexible*)
lemma UN_I: "\a:A; b: B(a)\ \ b: (UN x:A. B(x))"
  unfolding UNION_def by (blast intro: bexI CollectI)

lemma UN_E: "\b : (UN x:A. B(x)); \x. \x:A; b: B(x)\ \ R\ \ R"
  unfolding UNION_def by (blast dest: CollectD elim: bexE)

lemma UN_cong: "\A = B; \x. x:B \ C(x) = D(x)\ \ (UN x:A. C(x)) = (UN x:B. D(x))"
  by (simp add: UNION_def cong: bex_cong)

subsection \<open>Intersections of families\<close>

lemma INT_I: "(\x. x:A \ b: B(x)) \ b : (INT x:A. B(x))"
  unfolding INTER_def by (blast intro: CollectI ballI)

lemma INT_D: "\b : (INT x:A. B(x)); a:A\ \ b: B(a)"
  unfolding INTER_def by (blast dest: CollectD bspec)

(*"Classical" elimination rule -- does not require proving X:C *)
lemma INT_E: "\b : (INT x:A. B(x)); b: B(a) \ R; \ a:A \ R\ \ R"
  unfolding INTER_def by (blast dest: CollectD bspec)

lemma INT_cong: "\A = B; \x. x:B \ C(x) = D(x)\ \ (INT x:A. C(x)) = (INT x:B. D(x))"
  by (simp add: INTER_def cong: ball_cong)

subsection \<open>Rules for Unions\<close>

(*The order of the premises presupposes that C is rigid; A may be flexible*)
lemma UnionI: "\X:C; A:X\ \ A : Union(C)"
  unfolding Union_def by (blast intro: UN_I)

lemma UnionE: "\A : Union(C); \X. \ A:X; X:C\ \ R\ \ R"
  unfolding Union_def by (blast elim: UN_E)

subsection \<open>Rules for Inter\<close>

lemma InterI: "(\X. X:C \ A:X) \ A : Inter(C)"
  unfolding Inter_def by (blast intro: INT_I)

(*A "destruct" rule -- every X in C contains A as an element, but
  A:X can hold when X:C does not!  This rule is analogous to "spec". *)
lemma InterD: "\A : Inter(C); X:C\ \ A:X"
  unfolding Inter_def by (blast dest: INT_D)

(*"Classical" elimination rule -- does not require proving X:C *)
lemma InterE: "\A : Inter(C); A:X \ R; \ X:C \ R\ \ R"
  unfolding Inter_def by (blast elim: INT_E)

section \<open>Derived rules involving subsets; Union and Intersection as lattice operations\<close>

subsection \<open>Big Union -- least upper bound of a set\<close>

lemma Union_upper: "B:A \ B <= Union(A)"
  by (blast intro: subsetI UnionI)

lemma Union_least: "(\X. X:A \ X<=C) \ Union(A) <= C"
  by (blast intro: subsetI dest: subsetD elim: UnionE)

subsection \<open>Big Intersection -- greatest lower bound of a set\<close>

lemma Inter_lower: "B:A \ Inter(A) <= B"
  by (blast intro: subsetI dest: InterD)

lemma Inter_greatest: "(\X. X:A \ C<=X) \ C <= Inter(A)"
  by (blast intro: subsetI InterI dest: subsetD)

subsection \<open>Finite Union -- the least upper bound of 2 sets\<close>

lemma Un_upper1: "A <= A Un B"
  by (blast intro: subsetI UnI1)

lemma Un_upper2: "B <= A Un B"
  by (blast intro: subsetI UnI2)

lemma Un_least: "\A<=C; B<=C\ \ A Un B <= C"
  by (blast intro: subsetI elim: UnE dest: subsetD)

subsection \<open>Finite Intersection -- the greatest lower bound of 2 sets\<close>

lemma Int_lower1: "A Int B <= A"
  by (blast intro: subsetI elim: IntE)

lemma Int_lower2: "A Int B <= B"
  by (blast intro: subsetI elim: IntE)

lemma Int_greatest: "\C<=A; C<=B\ \ C <= A Int B"
  by (blast intro: subsetI IntI dest: subsetD)

subsection \<open>Monotonicity\<close>

lemma monoI: "(\A B. A <= B \ f(A) <= f(B)) \ mono(f)"
  unfolding mono_def by blast

lemma monoD: "\mono(f); A <= B\ \ f(A) <= f(B)"
  unfolding mono_def by blast

lemma mono_Un: "mono(f) \ f(A) Un f(B) <= f(A Un B)"
  by (blast intro: Un_least dest: monoD intro: Un_upper1 Un_upper2)

lemma mono_Int: "mono(f) \ f(A Int B) <= f(A) Int f(B)"
  by (blast intro: Int_greatest dest: monoD intro: Int_lower1 Int_lower2)

subsection \<open>Automated reasoning setup\<close>

lemmas [intro!] = ballI subsetI InterI INT_I CollectI ComplI IntI UnCI singletonI
  and [intro] = bexI UnionI UN_I
  and [elim!] = bexE UnionE UN_E CollectE ComplE IntE UnE emptyE singletonE
  and [elim] = ballE InterD InterE INT_D INT_E subsetD subsetCE

lemma mem_rews:
  "(a : A Un B) \ (a:A | a:B)"
  "(a : A Int B) \ (a:A \ a:B)"
  "(a : Compl(B)) \ (\a:B)"
  "(a : {b}) \ (a=b)"
  "(a : {}) \ False"
  "(a : {x. P(x)}) \ P(a)"
  by blast+

lemmas [simp] = trivial_set empty_eq mem_rews
  and [cong] = ball_cong bex_cong INT_cong UN_cong

section \<open>Equalities involving union, intersection, inclusion, etc.\<close>

subsection \<open>Binary Intersection\<close>

lemma Int_absorb: "A Int A = A"
  by (blast intro: equalityI)

lemma Int_commute: "A Int B = B Int A"
  by (blast intro: equalityI)

lemma Int_assoc: "(A Int B) Int C = A Int (B Int C)"
  by (blast intro: equalityI)

lemma Int_Un_distrib: "(A Un B) Int C = (A Int C) Un (B Int C)"
  by (blast intro: equalityI)

lemma subset_Int_eq: "(A<=B) \ (A Int B = A)"
  by (blast intro: equalityI elim: equalityE)

subsection \<open>Binary Union\<close>

lemma Un_absorb: "A Un A = A"
  by (blast intro: equalityI)

lemma Un_commute: "A Un B = B Un A"
  by (blast intro: equalityI)

lemma Un_assoc: "(A Un B) Un C = A Un (B Un C)"
  by (blast intro: equalityI)

lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)"
  by (blast intro: equalityI)

lemma Un_Int_crazy:
    "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
  by (blast intro: equalityI)

lemma subset_Un_eq: "(A<=B) \ (A Un B = B)"
  by (blast intro: equalityI elim: equalityE)

subsection \<open>Simple properties of \<open>Compl\<close> -- complement of a set\<close>

lemma Compl_disjoint: "A Int Compl(A) = {x. False}"
  by (blast intro: equalityI)

lemma Compl_partition: "A Un Compl(A) = {x. True}"
  by (blast intro: equalityI)

lemma double_complement: "Compl(Compl(A)) = A"
  by (blast intro: equalityI)

lemma Compl_Un: "Compl(A Un B) = Compl(A) Int Compl(B)"
  by (blast intro: equalityI)

lemma Compl_Int: "Compl(A Int B) = Compl(A) Un Compl(B)"
  by (blast intro: equalityI)

lemma Compl_UN: "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))"
  by (blast intro: equalityI)

lemma Compl_INT: "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))"
  by (blast intro: equalityI)

(*Halmos, Naive Set Theory, page 16.*)
lemma Un_Int_assoc_eq: "((A Int B) Un C = A Int (B Un C)) \ (C<=A)"
  by (blast intro: equalityI elim: equalityE)

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

lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
  by (blast intro: equalityI)

lemma Union_disjoint:
    "(Union(C) Int A = {x. False}) \ (ALL B:C. B Int A = {x. False})"
  by (blast intro: equalityI elim: equalityE)

lemma Inter_Un_distrib: "Inter(A Un B) = Inter(A) Int Inter(B)"
  by (blast intro: equalityI)

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

lemma UN_eq: "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})"
  by (blast intro: equalityI)

(*Look: it has an EXISTENTIAL quantifier*)
lemma INT_eq: "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})"
  by (blast intro: equalityI)

lemma Int_Union_image: "A Int Union(B) = (UN C:B. A Int C)"
  by (blast intro: equalityI)

lemma Un_Inter_image: "A Un Inter(B) = (INT C:B. A Un C)"
  by (blast intro: equalityI)

section \<open>Monotonicity of various operations\<close>

lemma Union_mono: "A<=B \ Union(A) <= Union(B)"
  by blast

lemma Inter_anti_mono: "B <= A \ Inter(A) <= Inter(B)"
  by blast

lemma UN_mono: "\A <= B; \x. x:A \ f(x)<=g(x)\ \ (UN x:A. f(x)) <= (UN x:B. g(x))"
  by blast

lemma INT_anti_mono: "\B <= A; \x. x:A \ f(x) <= g(x)\ \ (INT x:A. f(x)) <= (INT x:A. g(x))"
  by blast

lemma Un_mono: "\A <= C; B <= D\ \ A Un B <= C Un D"
  by blast

lemma Int_mono: "\A <= C; B <= D\ \ A Int B <= C Int D"
  by blast

lemma Compl_anti_mono: "A <= B \ Compl(B) <= Compl(A)"
  by blast

end

¤ Dauer der Verarbeitung: 0.7 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.