Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: more_thm.ML Sprache: PVS

Original von: Isabelle^©

(*  Title:      HOL/Relation.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Stefan Berghofer, TU Muenchen
*)

section \<open>Relations -- as sets of pairs, and binary predicates\<close>

theory Relation
  imports Finite_Set
begin

text \<open>A preliminary: classical rules for reasoning on predicates\<close>

declare predicate1I [Pure.intro!, intro!]
declare predicate1D [Pure.dest, dest]
declare predicate2I [Pure.intro!, intro!]
declare predicate2D [Pure.dest, dest]
declare bot1E [elim!]
declare bot2E [elim!]
declare top1I [intro!]
declare top2I [intro!]
declare inf1I [intro!]
declare inf2I [intro!]
declare inf1E [elim!]
declare inf2E [elim!]
declare sup1I1 [intro?]
declare sup2I1 [intro?]
declare sup1I2 [intro?]
declare sup2I2 [intro?]
declare sup1E [elim!]
declare sup2E [elim!]
declare sup1CI [intro!]
declare sup2CI [intro!]
declare Inf1_I [intro!]
declare INF1_I [intro!]
declare Inf2_I [intro!]
declare INF2_I [intro!]
declare Inf1_D [elim]
declare INF1_D [elim]
declare Inf2_D [elim]
declare INF2_D [elim]
declare Inf1_E [elim]
declare INF1_E [elim]
declare Inf2_E [elim]
declare INF2_E [elim]
declare Sup1_I [intro]
declare SUP1_I [intro]
declare Sup2_I [intro]
declare SUP2_I [intro]
declare Sup1_E [elim!]
declare SUP1_E [elim!]
declare Sup2_E [elim!]
declare SUP2_E [elim!]

subsection \<open>Fundamental\<close>

subsubsection \<open>Relations as sets of pairs\<close>

type_synonym 'a rel = "('a \<times> 'a) set"

lemma subrelI: "(\x y. (x, y) \ r \ (x, y) \ s) \ r \ s"
  \<comment> \<open>Version of @{thm [source] subsetI} for binary relations\<close>
  by auto

lemma lfp_induct2:
  "(a, b) \ lfp f \ mono f \
    (\<And>a b. (a, b) \<in> f (lfp f \<inter> {(x, y). P x y}) \<Longrightarrow> P a b) \<Longrightarrow> P a b"
  \<comment> \<open>Version of @{thm [source] lfp_induct} for binary relations\<close>
  using lfp_induct_set [of "(a, b)" f "case_prod P"] by auto

subsubsection \<open>Conversions between set and predicate relations\<close>

lemma pred_equals_eq [pred_set_conv]: "(\x. x \ R) = (\x. x \ S) \ R = S"
  by (simp add: set_eq_iff fun_eq_iff)

lemma pred_equals_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) = (\x y. (x, y) \ S) \ R = S"
  by (simp add: set_eq_iff fun_eq_iff)

lemma pred_subset_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) \ R \ S"
  by (simp add: subset_iff le_fun_def)

lemma pred_subset_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) \ R \ S"
  by (simp add: subset_iff le_fun_def)

lemma bot_empty_eq [pred_set_conv]: "\ = (\x. x \ {})"
  by (auto simp add: fun_eq_iff)

lemma bot_empty_eq2 [pred_set_conv]: "\ = (\x y. (x, y) \ {})"
  by (auto simp add: fun_eq_iff)

lemma top_empty_eq [pred_set_conv]: "\ = (\x. x \ UNIV)"
  by (auto simp add: fun_eq_iff)

lemma top_empty_eq2 [pred_set_conv]: "\ = (\x y. (x, y) \ UNIV)"
  by (auto simp add: fun_eq_iff)

lemma inf_Int_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)"
  by (simp add: inf_fun_def)

lemma inf_Int_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)"
  by (simp add: inf_fun_def)

lemma sup_Un_eq [pred_set_conv]: "(\x. x \ R) \ (\x. x \ S) = (\x. x \ R \ S)"
  by (simp add: sup_fun_def)

lemma sup_Un_eq2 [pred_set_conv]: "(\x y. (x, y) \ R) \ (\x y. (x, y) \ S) = (\x y. (x, y) \ R \ S)"
  by (simp add: sup_fun_def)

lemma INF_INT_eq [pred_set_conv]: "(\i\S. (\x. x \ r i)) = (\x. x \ (\i\S. r i))"
  by (simp add: fun_eq_iff)

lemma INF_INT_eq2 [pred_set_conv]: "(\i\S. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (\i\S. r i))"
  by (simp add: fun_eq_iff)

lemma SUP_UN_eq [pred_set_conv]: "(\i\S. (\x. x \ r i)) = (\x. x \ (\i\S. r i))"
  by (simp add: fun_eq_iff)

lemma SUP_UN_eq2 [pred_set_conv]: "(\i\S. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (\i\S. r i))"
  by (simp add: fun_eq_iff)

lemma Inf_INT_eq [pred_set_conv]: "\S = (\x. x \ (\(Collect ` S)))"
  by (simp add: fun_eq_iff)

lemma INF_Int_eq [pred_set_conv]: "(\i\S. (\x. x \ i)) = (\x. x \ \S)"
  by (simp add: fun_eq_iff)

lemma Inf_INT_eq2 [pred_set_conv]: "\S = (\x y. (x, y) \ (\(Collect ` case_prod ` S)))"
  by (simp add: fun_eq_iff)

lemma INF_Int_eq2 [pred_set_conv]: "(\i\S. (\x y. (x, y) \ i)) = (\x y. (x, y) \ \S)"
  by (simp add: fun_eq_iff)

lemma Sup_SUP_eq [pred_set_conv]: "\S = (\x. x \ \(Collect ` S))"
  by (simp add: fun_eq_iff)

lemma SUP_Sup_eq [pred_set_conv]: "(\i\S. (\x. x \ i)) = (\x. x \ \S)"
  by (simp add: fun_eq_iff)

lemma Sup_SUP_eq2 [pred_set_conv]: "\S = (\x y. (x, y) \ (\(Collect ` case_prod ` S)))"
  by (simp add: fun_eq_iff)

lemma SUP_Sup_eq2 [pred_set_conv]: "(\i\S. (\x y. (x, y) \ i)) = (\x y. (x, y) \ \S)"
  by (simp add: fun_eq_iff)

subsection \<open>Properties of relations\<close>

subsubsection \<open>Reflexivity\<close>

definition refl_on :: "'a set \ 'a rel \ bool"
  where "refl_on A r \ r \ A \ A \ (\x\A. (x, x) \ r)"

abbreviation refl :: "'a rel \ bool" \ \reflexivity over a type\
  where "refl \ refl_on UNIV"

definition reflp :: "('a \ 'a \ bool) \ bool"
  where "reflp r \ (\x. r x x)"

lemma reflp_refl_eq [pred_set_conv]: "reflp (\x y. (x, y) \ r) \ refl r"
  by (simp add: refl_on_def reflp_def)

lemma refl_onI [intro?]: "r \ A \ A \ (\x. x \ A \ (x, x) \ r) \ refl_on A r"
  unfolding refl_on_def by (iprover intro!: ballI)

lemma refl_onD: "refl_on A r \ a \ A \ (a, a) \ r"
  unfolding refl_on_def by blast

lemma refl_onD1: "refl_on A r \ (x, y) \ r \ x \ A"
  unfolding refl_on_def by blast

lemma refl_onD2: "refl_on A r \ (x, y) \ r \ y \ A"
  unfolding refl_on_def by blast

lemma reflpI [intro?]: "(\x. r x x) \ reflp r"
  by (auto intro: refl_onI simp add: reflp_def)

lemma reflpE:
  assumes "reflp r"
  obtains "r x x"
  using assms by (auto dest: refl_onD simp add: reflp_def)

lemma reflpD [dest?]:
  assumes "reflp r"
  shows "r x x"
  using assms by (auto elim: reflpE)

lemma refl_on_Int: "refl_on A r \ refl_on B s \ refl_on (A \ B) (r \ s)"
  unfolding refl_on_def by blast

lemma reflp_inf: "reflp r \ reflp s \ reflp (r \ s)"
  by (auto intro: reflpI elim: reflpE)

lemma refl_on_Un: "refl_on A r \ refl_on B s \ refl_on (A \ B) (r \ s)"
  unfolding refl_on_def by blast

lemma reflp_sup: "reflp r \ reflp s \ reflp (r \ s)"
  by (auto intro: reflpI elim: reflpE)

lemma refl_on_INTER: "\x\S. refl_on (A x) (r x) \ refl_on (\(A ` S)) (\(r ` S))"
  unfolding refl_on_def by fast

lemma refl_on_UNION: "\x\S. refl_on (A x) (r x) \ refl_on (\(A ` S)) (\(r ` S))"
  unfolding refl_on_def by blast

lemma refl_on_empty [simp]: "refl_on {} {}"
  by (simp add: refl_on_def)

lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
by (blast intro: refl_onI)

lemma refl_on_def' [nitpick_unfold, code]:
  "refl_on A r \ (\(x, y) \ r. x \ A \ y \ A) \ (\x \ A. (x, x) \ r)"
  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)

lemma reflp_equality [simp]: "reflp (=)"
  by (simp add: reflp_def)

lemma reflp_mono: "reflp R \ (\x y. R x y \ Q x y) \ reflp Q"
  by (auto intro: reflpI dest: reflpD)

subsubsection \<open>Irreflexivity\<close>

definition irrefl :: "'a rel \ bool"
  where "irrefl r \ (\a. (a, a) \ r)"

definition irreflp :: "('a \ 'a \ bool) \ bool"
  where "irreflp R \ (\a. \ R a a)"

lemma irreflp_irrefl_eq [pred_set_conv]: "irreflp (\a b. (a, b) \ R) \ irrefl R"
  by (simp add: irrefl_def irreflp_def)

lemma irreflI [intro?]: "(\a. (a, a) \ R) \ irrefl R"
  by (simp add: irrefl_def)

lemma irreflpI [intro?]: "(\a. \ R a a) \ irreflp R"
  by (fact irreflI [to_pred])

lemma irrefl_distinct [code]: "irrefl r \ (\(a, b) \ r. a \ b)"
  by (auto simp add: irrefl_def)

subsubsection \<open>Asymmetry\<close>

inductive asym :: "'a rel \ bool"
  where asymI: "(\a b. (a, b) \ R \ (b, a) \ R) \ asym R"

inductive asymp :: "('a \ 'a \ bool) \ bool"
  where asympI: "(\a b. R a b \ \ R b a) \ asymp R"

lemma asymp_asym_eq [pred_set_conv]: "asymp (\a b. (a, b) \ R) \ asym R"
  by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq)

lemma asymD: "\asym R; (x,y) \ R\ \ (y,x) \ R"
  by (simp add: asym.simps)

lemma asym_iff: "asym R \ (\x y. (x,y) \ R \ (y,x) \ R)"
  by (blast intro: asymI dest: asymD)

subsubsection \<open>Symmetry\<close>

definition sym :: "'a rel \ bool"
  where "sym r \ (\x y. (x, y) \ r \ (y, x) \ r)"

definition symp :: "('a \ 'a \ bool) \ bool"
  where "symp r \ (\x y. r x y \ r y x)"

lemma symp_sym_eq [pred_set_conv]: "symp (\x y. (x, y) \ r) \ sym r"
  by (simp add: sym_def symp_def)

lemma symI [intro?]: "(\a b. (a, b) \ r \ (b, a) \ r) \ sym r"
  by (unfold sym_def) iprover

lemma sympI [intro?]: "(\a b. r a b \ r b a) \ symp r"
  by (fact symI [to_pred])

lemma symE:
  assumes "sym r" and "(b, a) \ r"
  obtains "(a, b) \ r"
  using assms by (simp add: sym_def)

lemma sympE:
  assumes "symp r" and "r b a"
  obtains "r a b"
  using assms by (rule symE [to_pred])

lemma symD [dest?]:
  assumes "sym r" and "(b, a) \ r"
  shows "(a, b) \ r"
  using assms by (rule symE)

lemma sympD [dest?]:
  assumes "symp r" and "r b a"
  shows "r a b"
  using assms by (rule symD [to_pred])

lemma sym_Int: "sym r \ sym s \ sym (r \ s)"
  by (fast intro: symI elim: symE)

lemma symp_inf: "symp r \ symp s \ symp (r \ s)"
  by (fact sym_Int [to_pred])

lemma sym_Un: "sym r \ sym s \ sym (r \ s)"
  by (fast intro: symI elim: symE)

lemma symp_sup: "symp r \ symp s \ symp (r \ s)"
  by (fact sym_Un [to_pred])

lemma sym_INTER: "\x\S. sym (r x) \ sym (\(r ` S))"
  by (fast intro: symI elim: symE)

lemma symp_INF: "\x\S. symp (r x) \ symp (\(r ` S))"
  by (fact sym_INTER [to_pred])

lemma sym_UNION: "\x\S. sym (r x) \ sym (\(r ` S))"
  by (fast intro: symI elim: symE)

lemma symp_SUP: "\x\S. symp (r x) \ symp (\(r ` S))"
  by (fact sym_UNION [to_pred])

subsubsection \<open>Antisymmetry\<close>

definition antisym :: "'a rel \ bool"
  where "antisym r \ (\x y. (x, y) \ r \ (y, x) \ r \ x = y)"

definition antisymp :: "('a \ 'a \ bool) \ bool"
  where "antisymp r \ (\x y. r x y \ r y x \ x = y)"

lemma antisymp_antisym_eq [pred_set_conv]: "antisymp (\x y. (x, y) \ r) \ antisym r"
  by (simp add: antisym_def antisymp_def)

lemma antisymI [intro?]:
  "(\x y. (x, y) \ r \ (y, x) \ r \ x = y) \ antisym r"
  unfolding antisym_def by iprover

lemma antisympI [intro?]:
  "(\x y. r x y \ r y x \ x = y) \ antisymp r"
  by (fact antisymI [to_pred])

lemma antisymD [dest?]:
  "antisym r \ (a, b) \ r \ (b, a) \ r \ a = b"
  unfolding antisym_def by iprover

lemma antisympD [dest?]:
  "antisymp r \ r a b \ r b a \ a = b"
  by (fact antisymD [to_pred])

lemma antisym_subset:
  "r \ s \ antisym s \ antisym r"
  unfolding antisym_def by blast

lemma antisymp_less_eq:
  "r \ s \ antisymp s \ antisymp r"
  by (fact antisym_subset [to_pred])

lemma antisym_empty [simp]:
  "antisym {}"
  unfolding antisym_def by blast

lemma antisym_bot [simp]:
  "antisymp \"
  by (fact antisym_empty [to_pred])

lemma antisymp_equality [simp]:
  "antisymp HOL.eq"
  by (auto intro: antisympI)

lemma antisym_singleton [simp]:
  "antisym {x}"
  by (blast intro: antisymI)

subsubsection \<open>Transitivity\<close>

definition trans :: "'a rel \ bool"
  where "trans r \ (\x y z. (x, y) \ r \ (y, z) \ r \ (x, z) \ r)"

definition transp :: "('a \ 'a \ bool) \ bool"
  where "transp r \ (\x y z. r x y \ r y z \ r x z)"

lemma transp_trans_eq [pred_set_conv]: "transp (\x y. (x, y) \ r) \ trans r"
  by (simp add: trans_def transp_def)

lemma transI [intro?]: "(\x y z. (x, y) \ r \ (y, z) \ r \ (x, z) \ r) \ trans r"
  by (unfold trans_def) iprover

lemma transpI [intro?]: "(\x y z. r x y \ r y z \ r x z) \ transp r"
  by (fact transI [to_pred])

lemma transE:
  assumes "trans r" and "(x, y) \ r" and "(y, z) \ r"
  obtains "(x, z) \ r"
  using assms by (unfold trans_def) iprover

lemma transpE:
  assumes "transp r" and "r x y" and "r y z"
  obtains "r x z"
  using assms by (rule transE [to_pred])

lemma transD [dest?]:
  assumes "trans r" and "(x, y) \ r" and "(y, z) \ r"
  shows "(x, z) \ r"
  using assms by (rule transE)

lemma transpD [dest?]:
  assumes "transp r" and "r x y" and "r y z"
  shows "r x z"
  using assms by (rule transD [to_pred])

lemma trans_Int: "trans r \ trans s \ trans (r \ s)"
  by (fast intro: transI elim: transE)

lemma transp_inf: "transp r \ transp s \ transp (r \ s)"
  by (fact trans_Int [to_pred])

lemma trans_INTER: "\x\S. trans (r x) \ trans (\(r ` S))"
  by (fast intro: transI elim: transD)

lemma transp_INF: "\x\S. transp (r x) \ transp (\(r ` S))"
  by (fact trans_INTER [to_pred])

lemma trans_join [code]: "trans r \ (\(x, y1) \ r. \(y2, z) \ r. y1 = y2 \ (x, z) \ r)"
  by (auto simp add: trans_def)

lemma transp_trans: "transp r \ trans {(x, y). r x y}"
  by (simp add: trans_def transp_def)

lemma transp_equality [simp]: "transp (=)"
  by (auto intro: transpI)

lemma trans_empty [simp]: "trans {}"
  by (blast intro: transI)

lemma transp_empty [simp]: "transp (\x y. False)"
  using trans_empty[to_pred] by (simp add: bot_fun_def)

lemma trans_singleton [simp]: "trans {(a, a)}"
  by (blast intro: transI)

lemma transp_singleton [simp]: "transp (\x y. x = a \ y = a)"
  by (simp add: transp_def)

context preorder
begin

lemma transp_le[simp]: "transp (\)"
by(auto simp add: transp_def intro: order_trans)

lemma transp_less[simp]: "transp (<)"
by(auto simp add: transp_def intro: less_trans)

lemma transp_ge[simp]: "transp (\)"
by(auto simp add: transp_def intro: order_trans)

lemma transp_gr[simp]: "transp (>)"
by(auto simp add: transp_def intro: less_trans)

end

subsubsection \<open>Totality\<close>

definition total_on :: "'a set \ 'a rel \ bool"
  where "total_on A r \ (\x\A. \y\A. x \ y \ (x, y) \ r \ (y, x) \ r)"

lemma total_onI [intro?]:
  "(\x y. \x \ A; y \ A; x \ y\ \ (x, y) \ r \ (y, x) \ r) \ total_on A r"
  unfolding total_on_def by blast

abbreviation "total \ total_on UNIV"

lemma total_on_empty [simp]: "total_on {} r"
  by (simp add: total_on_def)

lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
  unfolding total_on_def by blast

subsubsection \<open>Single valued relations\<close>

definition single_valued :: "('a \ 'b) set \ bool"
  where "single_valued r \ (\x y. (x, y) \ r \ (\z. (x, z) \ r \ y = z))"

definition single_valuedp :: "('a \ 'b \ bool) \ bool"
  where "single_valuedp r \ (\x y. r x y \ (\z. r x z \ y = z))"

lemma single_valuedp_single_valued_eq [pred_set_conv]:
  "single_valuedp (\x y. (x, y) \ r) \ single_valued r"
  by (simp add: single_valued_def single_valuedp_def)

lemma single_valuedp_iff_Uniq:
  "single_valuedp r \ (\x. \\<^sub>\\<^sub>1y. r x y)"
  unfolding Uniq_def single_valuedp_def by auto

lemma single_valuedI:
  "(\x y. (x, y) \ r \ (\z. (x, z) \ r \ y = z)) \ single_valued r"
  unfolding single_valued_def by blast

lemma single_valuedpI:
  "(\x y. r x y \ (\z. r x z \ y = z)) \ single_valuedp r"
  by (fact single_valuedI [to_pred])

lemma single_valuedD:
  "single_valued r \ (x, y) \ r \ (x, z) \ r \ y = z"
  by (simp add: single_valued_def)

lemma single_valuedpD:
  "single_valuedp r \ r x y \ r x z \ y = z"
  by (fact single_valuedD [to_pred])

lemma single_valued_empty [simp]:
  "single_valued {}"
  by (simp add: single_valued_def)

lemma single_valuedp_bot [simp]:
  "single_valuedp \"
  by (fact single_valued_empty [to_pred])

lemma single_valued_subset:
  "r \ s \ single_valued s \ single_valued r"
  unfolding single_valued_def by blast

lemma single_valuedp_less_eq:
  "r \ s \ single_valuedp s \ single_valuedp r"
  by (fact single_valued_subset [to_pred])

subsection \<open>Relation operations\<close>

subsubsection \<open>The identity relation\<close>

definition Id :: "'a rel"
  where "Id = {p. \x. p = (x, x)}"

lemma IdI [intro]: "(a, a) \ Id"
  by (simp add: Id_def)

lemma IdE [elim!]: "p \ Id \ (\x. p = (x, x) \ P) \ P"
  unfolding Id_def by (iprover elim: CollectE)

lemma pair_in_Id_conv [iff]: "(a, b) \ Id \ a = b"
  unfolding Id_def by blast

lemma refl_Id: "refl Id"
  by (simp add: refl_on_def)

lemma antisym_Id: "antisym Id"
  \<comment> \<open>A strange result, since \<open>Id\<close> is also symmetric.\<close>
  by (simp add: antisym_def)

lemma sym_Id: "sym Id"
  by (simp add: sym_def)

lemma trans_Id: "trans Id"
  by (simp add: trans_def)

lemma single_valued_Id [simp]: "single_valued Id"
  by (unfold single_valued_def) blast

lemma irrefl_diff_Id [simp]: "irrefl (r - Id)"
  by (simp add: irrefl_def)

lemma trans_diff_Id: "trans r \ antisym r \ trans (r - Id)"
  unfolding antisym_def trans_def by blast

lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r"
  by (simp add: total_on_def)

lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}"
  by force

subsubsection \<open>Diagonal: identity over a set\<close>

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

lemma Id_on_empty [simp]: "Id_on {} = {}"
  by (simp add: Id_on_def)

lemma Id_on_eqI: "a = b \ a \ A \ (a, b) \ Id_on A"
  by (simp add: Id_on_def)

lemma Id_onI [intro!]: "a \ A \ (a, a) \ Id_on A"
  by (rule Id_on_eqI) (rule refl)

lemma Id_onE [elim!]: "c \ Id_on A \ (\x. x \ A \ c = (x, x) \ P) \ P"
  \<comment> \<open>The general elimination rule.\<close>
  unfolding Id_on_def by (iprover elim!: UN_E singletonE)

lemma Id_on_iff: "(x, y) \ Id_on A \ x = y \ x \ A"
  by blast

lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\(x, y). x = y \ A x)"
  by auto

lemma Id_on_subset_Times: "Id_on A \ A \ A"
  by blast

lemma refl_on_Id_on: "refl_on A (Id_on A)"
  by (rule refl_onI [OF Id_on_subset_Times Id_onI])

lemma antisym_Id_on [simp]: "antisym (Id_on A)"
  unfolding antisym_def by blast

lemma sym_Id_on [simp]: "sym (Id_on A)"
  by (rule symI) clarify

lemma trans_Id_on [simp]: "trans (Id_on A)"
  by (fast intro: transI elim: transD)

lemma single_valued_Id_on [simp]: "single_valued (Id_on A)"
  unfolding single_valued_def by blast

subsubsection \<open>Composition\<close>

inductive_set relcomp  :: "('a \ 'b) set \ ('b \ 'c) set \ ('a \ 'c) set" (infixr "O" 75)
  for r :: "('a \ 'b) set" and s :: "('b \ 'c) set"
  where relcompI [intro]: "(a, b) \ r \ (b, c) \ s \ (a, c) \ r O s"

notation relcompp (infixr "OO" 75)

lemmas relcomppI = relcompp.intros

text \<open>
  For historic reasons, the elimination rules are not wholly corresponding.
  Feel free to consolidate this.
\<close>

inductive_cases relcompEpair: "(a, c) \ r O s"
inductive_cases relcomppE [elim!]: "(r OO s) a c"

lemma relcompE [elim!]: "xz \ r O s \
  (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s  \<Longrightarrow> P) \<Longrightarrow> P"
  apply (cases xz)
  apply simp
  apply (erule relcompEpair)
  apply iprover
  done

lemma R_O_Id [simp]: "R O Id = R"
  by fast

lemma Id_O_R [simp]: "Id O R = R"
  by fast

lemma relcomp_empty1 [simp]: "{} O R = {}"
  by blast

lemma relcompp_bot1 [simp]: "\ OO R = \"
  by (fact relcomp_empty1 [to_pred])

lemma relcomp_empty2 [simp]: "R O {} = {}"
  by blast

lemma relcompp_bot2 [simp]: "R OO \ = \"
  by (fact relcomp_empty2 [to_pred])

lemma O_assoc: "(R O S) O T = R O (S O T)"
  by blast

lemma relcompp_assoc: "(r OO s) OO t = r OO (s OO t)"
  by (fact O_assoc [to_pred])

lemma trans_O_subset: "trans r \ r O r \ r"
  by (unfold trans_def) blast

lemma transp_relcompp_less_eq: "transp r \ r OO r \ r "
  by (fact trans_O_subset [to_pred])

lemma relcomp_mono: "r' \ r \ s' \ s \ r' O s' \ r O s"
  by blast

lemma relcompp_mono: "r' \ r \ s' \ s \ r' OO s' \ r OO s "
  by (fact relcomp_mono [to_pred])

lemma relcomp_subset_Sigma: "r \ A \ B \ s \ B \ C \ r O s \ A \ C"
  by blast

lemma relcomp_distrib [simp]: "R O (S \ T) = (R O S) \ (R O T)"
  by auto

lemma relcompp_distrib [simp]: "R OO (S \ T) = R OO S \ R OO T"
  by (fact relcomp_distrib [to_pred])

lemma relcomp_distrib2 [simp]: "(S \ T) O R = (S O R) \ (T O R)"
  by auto

lemma relcompp_distrib2 [simp]: "(S \ T) OO R = S OO R \ T OO R"
  by (fact relcomp_distrib2 [to_pred])

lemma relcomp_UNION_distrib: "s O \(r ` I) = (\i\I. s O r i) "
  by auto

lemma relcompp_SUP_distrib: "s OO \(r ` I) = (\i\I. s OO r i)"
  by (fact relcomp_UNION_distrib [to_pred])

lemma relcomp_UNION_distrib2: "\(r ` I) O s = (\i\I. r i O s) "
  by auto

lemma relcompp_SUP_distrib2: "\(r ` I) OO s = (\i\I. r i OO s)"
  by (fact relcomp_UNION_distrib2 [to_pred])

lemma single_valued_relcomp: "single_valued r \ single_valued s \ single_valued (r O s)"
  unfolding single_valued_def by blast

lemma relcomp_unfold: "r O s = {(x, z). \y. (x, y) \ r \ (y, z) \ s}"
  by (auto simp add: set_eq_iff)

lemma relcompp_apply: "(R OO S) a c \ (\b. R a b \ S b c)"
  unfolding relcomp_unfold [to_pred] ..

lemma eq_OO: "(=) OO R = R"
  by blast

lemma OO_eq: "R OO (=) = R"
  by blast

subsubsection \<open>Converse\<close>

inductive_set converse :: "('a \ 'b) set \ ('b \ 'a) set" ("(_\)" [1000] 999)
  for r :: "('a \ 'b) set"
  where "(a, b) \ r \ (b, a) \ r\"

notation conversep  ("(_\\)" [1000] 1000)

notation (ASCII)
  converse  ("(_^-1)" [1000] 999) and
  conversep ("(_^--1)" [1000] 1000)

lemma converseI [sym]: "(a, b) \ r \ (b, a) \ r\"
  by (fact converse.intros)

lemma conversepI (* CANDIDATE [sym] *): "r a b \<Longrightarrow> r\<inverse>\<inverse> b a"
  by (fact conversep.intros)

lemma converseD [sym]: "(a, b) \ r\ \ (b, a) \ r"
  by (erule converse.cases) iprover

lemma conversepD (* CANDIDATE [sym] *): "r\<inverse>\<inverse> b a \<Longrightarrow> r a b"
  by (fact converseD [to_pred])

lemma converseE [elim!]: "yx \ r\ \ (\x y. yx = (y, x) \ (x, y) \ r \ P) \ P"
  \<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close>
  apply (cases yx)
  apply simp
  apply (erule converse.cases)
  apply iprover
  done

lemmas conversepE [elim!] = conversep.cases

lemma converse_iff [iff]: "(a, b) \ r\ \ (b, a) \ r"
  by (auto intro: converseI)

lemma conversep_iff [iff]: "r\\ a b = r b a"
  by (fact converse_iff [to_pred])

lemma converse_converse [simp]: "(r\)\ = r"
  by (simp add: set_eq_iff)

lemma conversep_conversep [simp]: "(r\\)\\ = r"
  by (fact converse_converse [to_pred])

lemma converse_empty[simp]: "{}\ = {}"
  by auto

lemma converse_UNIV[simp]: "UNIV\ = UNIV"
  by auto

lemma converse_relcomp: "(r O s)\ = s\ O r\"
  by blast

lemma converse_relcompp: "(r OO s)\\ = s\\ OO r\\"
  by (iprover intro: order_antisym conversepI relcomppI elim: relcomppE dest: conversepD)

lemma converse_Int: "(r \ s)\ = r\ \ s\"
  by blast

lemma converse_meet: "(r \ s)\\ = r\\ \ s\\"
  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)

lemma converse_Un: "(r \ s)\ = r\ \ s\"
  by blast

lemma converse_join: "(r \ s)\\ = r\\ \ s\\"
  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)

lemma converse_INTER: "(\(r ` S))\ = (\x\S. (r x)\)"
  by fast

lemma converse_UNION: "(\(r ` S))\ = (\x\S. (r x)\)"
  by blast

lemma converse_mono[simp]: "r\ \ s \ \ r \ s"
  by auto

lemma conversep_mono[simp]: "r\\ \ s \\ \ r \ s"
  by (fact converse_mono[to_pred])

lemma converse_inject[simp]: "r\ = s \ \ r = s"
  by auto

lemma conversep_inject[simp]: "r\\ = s \\ \ r = s"
  by (fact converse_inject[to_pred])

lemma converse_subset_swap: "r \ s \ \ r \ \ s"
  by auto

lemma conversep_le_swap: "r \ s \\ \ r \\ \ s"
  by (fact converse_subset_swap[to_pred])

lemma converse_Id [simp]: "Id\ = Id"
  by blast

lemma converse_Id_on [simp]: "(Id_on A)\ = Id_on A"
  by blast

lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
  by (auto simp: refl_on_def)

lemma sym_converse [simp]: "sym (converse r) = sym r"
  unfolding sym_def by blast

lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
  unfolding antisym_def by blast

lemma trans_converse [simp]: "trans (converse r) = trans r"
  unfolding trans_def by blast

lemma sym_conv_converse_eq: "sym r \ r\ = r"
  unfolding sym_def by fast

lemma sym_Un_converse: "sym (r \ r\)"
  unfolding sym_def by blast

lemma sym_Int_converse: "sym (r \ r\)"
  unfolding sym_def by blast

lemma total_on_converse [simp]: "total_on A (r\) = total_on A r"
  by (auto simp: total_on_def)

lemma finite_converse [iff]: "finite (r\) = finite r"
unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
by (auto elim: finite_imageD simp: inj_on_def)

lemma card_inverse[simp]: "card (R\) = card R"
proof -
  have *: "\R. prod.swap ` R = R\" by auto
  {
    assume "\finite R"
    hence ?thesis
      by auto
  } moreover {
    assume "finite R"
    with card_image_le[of R prod.swap] card_image_le[of "R\" prod.swap]
    have ?thesis by (auto simp: *)
  } ultimately show ?thesis by blast
qed

lemma conversep_noteq [simp]: "(\)\\ = (\)"
  by (auto simp add: fun_eq_iff)

lemma conversep_eq [simp]: "(=)\\ = (=)"
  by (auto simp add: fun_eq_iff)

lemma converse_unfold [code]: "r\ = {(y, x). (x, y) \ r}"
  by (simp add: set_eq_iff)

subsubsection \<open>Domain, range and field\<close>

inductive_set Domain :: "('a \ 'b) set \ 'a set" for r :: "('a \ 'b) set"
  where DomainI [intro]: "(a, b) \ r \ a \ Domain r"

lemmas DomainPI = Domainp.DomainI

inductive_cases DomainE [elim!]: "a \ Domain r"
inductive_cases DomainpE [elim!]: "Domainp r a"

inductive_set Range :: "('a \ 'b) set \ 'b set" for r :: "('a \ 'b) set"
  where RangeI [intro]: "(a, b) \ r \ b \ Range r"

lemmas RangePI = Rangep.RangeI

inductive_cases RangeE [elim!]: "b \ Range r"
inductive_cases RangepE [elim!]: "Rangep r b"

definition Field :: "'a rel \ 'a set"
  where "Field r = Domain r \ Range r"

lemma FieldI1: "(i, j) \ R \ i \ Field R"
  unfolding Field_def by blast

lemma FieldI2: "(i, j) \ R \ j \ Field R"
  unfolding Field_def by auto

lemma Domain_fst [code]: "Domain r = fst ` r"
  by force

lemma Range_snd [code]: "Range r = snd ` r"
  by force

lemma fst_eq_Domain: "fst ` R = Domain R"
  by force

lemma snd_eq_Range: "snd ` R = Range R"
  by force

lemma range_fst [simp]: "range fst = UNIV"
  by (auto simp: fst_eq_Domain)

lemma range_snd [simp]: "range snd = UNIV"
  by (auto simp: snd_eq_Range)

lemma Domain_empty [simp]: "Domain {} = {}"
  by auto

lemma Range_empty [simp]: "Range {} = {}"
  by auto

lemma Field_empty [simp]: "Field {} = {}"
  by (simp add: Field_def)

lemma Domain_empty_iff: "Domain r = {} \ r = {}"
  by auto

lemma Range_empty_iff: "Range r = {} \ r = {}"
  by auto

lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)"
  by blast

lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)"
  by blast

lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \ Field r"
  by (auto simp add: Field_def)

lemma Domain_iff: "a \ Domain r \ (\y. (a, y) \ r)"
  by blast

lemma Range_iff: "a \ Range r \ (\y. (y, a) \ r)"
  by blast

lemma Domain_Id [simp]: "Domain Id = UNIV"
  by blast

lemma Range_Id [simp]: "Range Id = UNIV"
  by blast

lemma Domain_Id_on [simp]: "Domain (Id_on A) = A"
  by blast

lemma Range_Id_on [simp]: "Range (Id_on A) = A"
  by blast

lemma Domain_Un_eq: "Domain (A \ B) = Domain A \ Domain B"
  by blast

lemma Range_Un_eq: "Range (A \ B) = Range A \ Range B"
  by blast

lemma Field_Un [simp]: "Field (r \ s) = Field r \ Field s"
  by (auto simp: Field_def)

lemma Domain_Int_subset: "Domain (A \ B) \ Domain A \ Domain B"
  by blast

lemma Range_Int_subset: "Range (A \ B) \ Range A \ Range B"
  by blast

lemma Domain_Diff_subset: "Domain A - Domain B \ Domain (A - B)"
  by blast

lemma Range_Diff_subset: "Range A - Range B \ Range (A - B)"
  by blast

lemma Domain_Union: "Domain (\S) = (\A\S. Domain A)"
  by blast

lemma Range_Union: "Range (\S) = (\A\S. Range A)"
  by blast

lemma Field_Union [simp]: "Field (\R) = \(Field ` R)"
  by (auto simp: Field_def)

lemma Domain_converse [simp]: "Domain (r\) = Range r"
  by auto

lemma Range_converse [simp]: "Range (r\) = Domain r"
  by blast

lemma Field_converse [simp]: "Field (r\) = Field r"
  by (auto simp: Field_def)

lemma Domain_Collect_case_prod [simp]: "Domain {(x, y). P x y} = {x. \y. P x y}"
  by auto

lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. \x. P x y}"
  by auto

lemma finite_Domain: "finite r \ finite (Domain r)"
  by (induct set: finite) auto

lemma finite_Range: "finite r \ finite (Range r)"
  by (induct set: finite) auto

lemma finite_Field: "finite r \ finite (Field r)"
  by (simp add: Field_def finite_Domain finite_Range)

lemma Domain_mono: "r \ s \ Domain r \ Domain s"
  by blast

lemma Range_mono: "r \ s \ Range r \ Range s"
  by blast

lemma mono_Field: "r \ s \ Field r \ Field s"
  by (auto simp: Field_def Domain_def Range_def)

lemma Domain_unfold: "Domain r = {x. \y. (x, y) \ r}"
  by blast

lemma Field_square [simp]: "Field (x \ x) = x"
  unfolding Field_def by blast

subsubsection \<open>Image of a set under a relation\<close>

definition Image :: "('a \ 'b) set \ 'a set \ 'b set" (infixr "``" 90)
  where "r `` s = {y. \x\s. (x, y) \ r}"

lemma Image_iff: "b \ r``A \ (\x\A. (x, b) \ r)"
  by (simp add: Image_def)

lemma Image_singleton: "r``{a} = {b. (a, b) \ r}"
  by (simp add: Image_def)

lemma Image_singleton_iff [iff]: "b \ r``{a} \ (a, b) \ r"
  by (rule Image_iff [THEN trans]) simp

lemma ImageI [intro]: "(a, b) \ r \ a \ A \ b \ r``A"
  unfolding Image_def by blast

lemma ImageE [elim!]: "b \ r `` A \ (\x. (x, b) \ r \ x \ A \ P) \ P"
  unfolding Image_def by (iprover elim!: CollectE bexE)

lemma rev_ImageI: "a \ A \ (a, b) \ r \ b \ r `` A"
  \<comment> \<open>This version's more effective when we already have the required \<open>a\<close>\<close>
  by blast

lemma Image_empty1 [simp]: "{} `` X = {}"
by auto

lemma Image_empty2 [simp]: "R``{} = {}"
by blast

lemma Image_Id [simp]: "Id `` A = A"
  by blast

lemma Image_Id_on [simp]: "Id_on A `` B = A \ B"
  by blast

lemma Image_Int_subset: "R `` (A \ B) \ R `` A \ R `` B"
  by blast

lemma Image_Int_eq: "single_valued (converse R) \ R `` (A \ B) = R `` A \ R `` B"
  by (auto simp: single_valued_def)

lemma Image_Un: "R `` (A \ B) = R `` A \ R `` B"
  by blast

lemma Un_Image: "(R \ S) `` A = R `` A \ S `` A"
  by blast

lemma Image_subset: "r \ A \ B \ r``C \ B"
  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)

lemma Image_eq_UN: "r``B = (\y\ B. r``{y})"
  \<comment> \<open>NOT suitable for rewriting\<close>
  by blast

lemma Image_mono: "r' \ r \ A' \ A \ (r' `` A') \ (r `` A)"
  by blast

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

lemma UN_Image: "(\i\I. X i) `` S = (\i\I. X i `` S)"
  by auto

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

text \<open>Converse inclusion requires some assumptions\<close>
lemma Image_INT_eq: "single_valued (r\) \ A \ {} \ r `` (\(B ` A)) = (\x\A. r `` B x)"
  apply (rule equalityI)
   apply (rule Image_INT_subset)
  apply (auto simp add: single_valued_def)
  apply blast
  done

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

lemma Image_Collect_case_prod [simp]: "{(x, y). P x y} `` A = {y. \x\A. P x y}"
  by auto

lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\x\X \ A. B x)"
  by auto

lemma relcomp_Image: "(X O Y) `` Z = Y `` (X `` Z)"
  by auto

lemma finite_Image[simp]: assumes "finite R" shows "finite (R `` A)"
by(rule finite_subset[OF _ finite_Range[OF assms]]) auto

subsubsection \<open>Inverse image\<close>

definition inv_image :: "'b rel \ ('a \ 'b) \ 'a rel"
  where "inv_image r f = {(x, y). (f x, f y) \ r}"

definition inv_imagep :: "('b \ 'b \ bool) \ ('a \ 'b) \ 'a \ 'a \ bool"
  where "inv_imagep r f = (\x y. r (f x) (f y))"

lemma [pred_set_conv]: "inv_imagep (\x y. (x, y) \ r) f = (\x y. (x, y) \ inv_image r f)"
  by (simp add: inv_image_def inv_imagep_def)

lemma sym_inv_image: "sym r \ sym (inv_image r f)"
  unfolding sym_def inv_image_def by blast

lemma trans_inv_image: "trans r \ trans (inv_image r f)"
  unfolding trans_def inv_image_def
  by (simp (no_asm)) blast

lemma total_inv_image: "\inj f; total r\ \ total (inv_image r f)"
  unfolding inv_image_def total_on_def by (auto simp: inj_eq)

lemma asym_inv_image: "asym R \ asym (inv_image R f)"
  by (simp add: inv_image_def asym_iff)

lemma in_inv_image[simp]: "(x, y) \ inv_image r f \ (f x, f y) \ r"
  by (auto simp: inv_image_def)

lemma converse_inv_image[simp]: "(inv_image R f)\ = inv_image (R\) f"
  unfolding inv_image_def converse_unfold by auto

lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
  by (simp add: inv_imagep_def)

subsubsection \<open>Powerset\<close>

definition Powp :: "('a \ bool) \ 'a set \ bool"
  where "Powp A = (\B. \x \ B. A x)"

lemma Powp_Pow_eq [pred_set_conv]: "Powp (\x. x \ A) = (\x. x \ Pow A)"
  by (auto simp add: Powp_def fun_eq_iff)

lemmas Powp_mono [mono] = Pow_mono [to_pred]

subsubsection \<open>Expressing relation operations via \<^const>\<open>Finite_Set.fold\<close>\<close>

lemma Id_on_fold:
  assumes "finite A"
  shows "Id_on A = Finite_Set.fold (\x. Set.insert (Pair x x)) {} A"
proof -
  interpret comp_fun_commute "\x. Set.insert (Pair x x)"
    by standard auto
  from assms show ?thesis
    unfolding Id_on_def by (induct A) simp_all
qed

lemma comp_fun_commute_Image_fold:
  "comp_fun_commute (\(x,y) A. if x \ S then Set.insert y A else A)"
proof -
  interpret comp_fun_idem Set.insert
    by (fact comp_fun_idem_insert)
  show ?thesis
    by standard (auto simp: fun_eq_iff comp_fun_commute split: prod.split)
qed

lemma Image_fold:
  assumes "finite R"
  shows "R `` S = Finite_Set.fold (\(x,y) A. if x \ S then Set.insert y A else A) {} R"
proof -
  interpret comp_fun_commute "(\(x,y) A. if x \ S then Set.insert y A else A)"
    by (rule comp_fun_commute_Image_fold)
  have *: "\x F. Set.insert x F `` S = (if fst x \ S then Set.insert (snd x) (F `` S) else (F `` S))"
    by (force intro: rev_ImageI)
  show ?thesis
    using assms by (induct R) (auto simp: *)
qed

lemma insert_relcomp_union_fold:
  assumes "finite S"
  shows "{x} O S \ X = Finite_Set.fold (\(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S"
proof -
  interpret comp_fun_commute "\(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'"
  proof -
    interpret comp_fun_idem Set.insert
      by (fact comp_fun_idem_insert)
    show "comp_fun_commute (\(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')"
      by standard (auto simp add: fun_eq_iff split: prod.split)
  qed
  have *: "{x} O S = {(x', z). x' = fst x \ (snd x, z) \ S}"
    by (auto simp: relcomp_unfold intro!: exI)
  show ?thesis
    unfolding * using \<open>finite S\<close> by (induct S) (auto split: prod.split)
qed

lemma insert_relcomp_fold:
  assumes "finite S"
  shows "Set.insert x R O S =
    Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S"
proof -
  have "Set.insert x R O S = ({x} O S) \ (R O S)"
    by auto
  then show ?thesis
    by (auto simp: insert_relcomp_union_fold [OF assms])
qed

lemma comp_fun_commute_relcomp_fold:
  assumes "finite S"
  shows "comp_fun_commute (\(x,y) A.
    Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)"
proof -
  have *: "\a b A.
    Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A"
    by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong)
  show ?thesis
    by standard (auto simp: *)
qed

lemma relcomp_fold:
  assumes "finite R" "finite S"
  shows "R O S = Finite_Set.fold
    (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
  using assms
  by (induct R)
    (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
      cong: if_cong)

end

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