products/sources/formale sprachen/Isabelle/HOL/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Order_Relation.thy   Sprache: Isabelle

Original von: Isabelle©
(*  Title:      HOL/Order_Relation.thy
    Author:     Tobias Nipkow
    Author:     Andrei Popescu, TU Muenchen
*)

section \<open>Orders as Relations\<close>

theory Order_Relation
imports Wfrec
begin

subsection \<open>Orders on a set\<close>

definition "preorder_on A r \ refl_on A r \ trans r"

definition "partial_order_on A r \ preorder_on A r \ antisym r"

definition "linear_order_on A r \ partial_order_on A r \ total_on A r"

definition "strict_linear_order_on A r \ trans r \ irrefl r \ total_on A r"

definition "well_order_on A r \ linear_order_on A r \ wf(r - Id)"

lemmas order_on_defs =
  preorder_on_def partial_order_on_def linear_order_on_def
  strict_linear_order_on_def well_order_on_def

lemma partial_order_onD:
  assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
  using assms unfolding partial_order_on_def preorder_on_def by auto

lemma preorder_on_empty[simp]: "preorder_on {} {}"
  by (simp add: preorder_on_def trans_def)

lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
  by (simp add: partial_order_on_def)

lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
  by (simp add: linear_order_on_def)

lemma well_order_on_empty[simp]: "well_order_on {} {}"
  by (simp add: well_order_on_def)


lemma preorder_on_converse[simp]: "preorder_on A (r\) = preorder_on A r"
  by (simp add: preorder_on_def)

lemma partial_order_on_converse[simp]: "partial_order_on A (r\) = partial_order_on A r"
  by (simp add: partial_order_on_def)

lemma linear_order_on_converse[simp]: "linear_order_on A (r\) = linear_order_on A r"
  by (simp add: linear_order_on_def)


lemma partial_order_on_acyclic:
  "partial_order_on A r \ acyclic (r - Id)"
  by (simp add: acyclic_irrefl partial_order_on_def preorder_on_def trans_diff_Id)

lemma partial_order_on_well_order_on:               
  "finite r \ partial_order_on A r \ wf (r - Id)"
  by (simp add: finite_acyclic_wf partial_order_on_acyclic) 

lemma strict_linear_order_on_diff_Id: "linear_order_on A r \ strict_linear_order_on A (r - Id)"
  by (simp add: order_on_defs trans_diff_Id)

lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}"
  by (simp add: order_on_defs)

lemma linear_order_on_acyclic:
  assumes "linear_order_on A r"
  shows "acyclic (r - Id)"
  using strict_linear_order_on_diff_Id[OF assms]
  by (auto simp add: acyclic_irrefl strict_linear_order_on_def)

lemma linear_order_on_well_order_on:
  assumes "finite r"
  shows "linear_order_on A r \ well_order_on A r"
  unfolding well_order_on_def
  using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast


subsection \<open>Orders on the field\<close>

abbreviation "Refl r \ refl_on (Field r) r"

abbreviation "Preorder r \ preorder_on (Field r) r"

abbreviation "Partial_order r \ partial_order_on (Field r) r"

abbreviation "Total r \ total_on (Field r) r"

abbreviation "Linear_order r \ linear_order_on (Field r) r"

abbreviation "Well_order r \ well_order_on (Field r) r"


lemma subset_Image_Image_iff:
  "Preorder r \ A \ Field r \ B \ Field r \
    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b, a) \<in> r)"
  apply (simp add: preorder_on_def refl_on_def Image_def subset_eq)
  apply (simp only: trans_def)
  apply fast
  done

lemma subset_Image1_Image1_iff:
  "Preorder r \ a \ Field r \ b \ Field r \ r `` {a} \ r `` {b} \ (b, a) \ r"
  by (simp add: subset_Image_Image_iff)

lemma Refl_antisym_eq_Image1_Image1_iff:
  assumes "Refl r"
    and as: "antisym r"
    and abf: "a \ Field r" "b \ Field r"
  shows "r `` {a} = r `` {b} \ a = b"
    (is "?lhs \ ?rhs")
proof
  assume ?lhs
  then have *: "\x. (a, x) \ r \ (b, x) \ r"
    by (simp add: set_eq_iff)
  have "(a, a) \ r" "(b, b) \ r" using \Refl r\ abf by (simp_all add: refl_on_def)
  then have "(a, b) \ r" "(b, a) \ r" using *[of a] *[of b] by simp_all
  then show ?rhs
    using \<open>antisym r\<close>[unfolded antisym_def] by blast
next
  assume ?rhs
  then show ?lhs by fast
qed

lemma Partial_order_eq_Image1_Image1_iff:
  "Partial_order r \ a \ Field r \ b \ Field r \ r `` {a} = r `` {b} \ a = b"
  by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff)

lemma Total_Id_Field:
  assumes "Total r"
    and not_Id: "\ r \ Id"
  shows "Field r = Field (r - Id)"
  using mono_Field[of "r - Id" r] Diff_subset[of r Id]
proof auto
  fix a assume *: "a \ Field r"
  from not_Id have "r \ {}" by fast
  with not_Id obtain b and c where "b \ c \ (b,c) \ r" by auto
  then have "b \ c \ {b, c} \ Field r" by (auto simp: Field_def)
  with * obtain d where "d \ Field r" "d \ a" by auto
  with * \<open>Total r\<close> have "(a, d) \<in> r \<or> (d, a) \<in> r" by (simp add: total_on_def)
  with \<open>d \<noteq> a\<close> show "a \<in> Field (r - Id)" unfolding Field_def by blast
qed

subsection\<open>Relations given by a predicate and the field\<close>

definition relation_of :: "('a \ 'a \ bool) \ 'a set \ ('a \ 'a) set"
  where "relation_of P A \ { (a, b) \ A \ A. P a b }"

lemma Field_relation_of:
  assumes "refl_on A (relation_of P A)" shows "Field (relation_of P A) = A"
  using assms unfolding refl_on_def Field_def by auto

lemma partial_order_on_relation_ofI:
  assumes refl: "\a. a \ A \ P a a"
    and trans: "\a b c. \ a \ A; b \ A; c \ A \ \ P a b \ P b c \ P a c"
    and antisym: "\a b. \ a \ A; b \ A \ \ P a b \ P b a \ a = b"
  shows "partial_order_on A (relation_of P A)"
proof -
  from refl have "refl_on A (relation_of P A)"
    unfolding refl_on_def relation_of_def by auto
  moreover have "trans (relation_of P A)" and "antisym (relation_of P A)"
    unfolding relation_of_def
    by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
  ultimately show ?thesis
    unfolding partial_order_on_def preorder_on_def by simp
qed

lemma Partial_order_relation_ofI:
  assumes "partial_order_on A (relation_of P A)" shows "Partial_order (relation_of P A)"
  using Field_relation_of assms partial_order_on_def preorder_on_def by fastforce


subsection \<open>Orders on a type\<close>

abbreviation "strict_linear_order \ strict_linear_order_on UNIV"

abbreviation "linear_order \ linear_order_on UNIV"

abbreviation "well_order \ well_order_on UNIV"


subsection \<open>Order-like relations\<close>

text \<open>
  In this subsection, we develop basic concepts and results pertaining
  to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
  total relations. We also further define upper and lower bounds operators.
\<close>


subsubsection \<open>Auxiliaries\<close>

lemma refl_on_domain: "refl_on A r \ (a, b) \ r \ a \ A \ b \ A"
  by (auto simp add: refl_on_def)

corollary well_order_on_domain: "well_order_on A r \ (a, b) \ r \ a \ A \ b \ A"
  by (auto simp add: refl_on_domain order_on_defs)

lemma well_order_on_Field: "well_order_on A r \ A = Field r"
  by (auto simp add: refl_on_def Field_def order_on_defs)

lemma well_order_on_Well_order: "well_order_on A r \ A = Field r \ Well_order r"
  using well_order_on_Field [of A] by auto

lemma Total_subset_Id:
  assumes "Total r"
    and "r \ Id"
  shows "r = {} \ (\a. r = {(a, a)})"
proof -
  have "\a. r = {(a, a)}" if "r \ {}"
  proof -
    from that obtain a b where ab: "(a, b) \ r" by fast
    with \<open>r \<subseteq> Id\<close> have "a = b" by blast
    with ab have aa: "(a, a) \ r" by simp
    have "a = c \ a = d" if "(c, d) \ r" for c d
    proof -
      from that have "{a, c, d} \ Field r"
        using ab unfolding Field_def by blast
      then have "((a, c) \ r \ (c, a) \ r \ a = c) \ ((a, d) \ r \ (d, a) \ r \ a = d)"
        using \<open>Total r\<close> unfolding total_on_def by blast
      with \<open>r \<subseteq> Id\<close> show ?thesis by blast
    qed
    then have "r \ {(a, a)}" by auto
    with aa show ?thesis by blast
  qed
  then show ?thesis by blast
qed

lemma Linear_order_in_diff_Id:
  assumes "Linear_order r"
    and "a \ Field r"
    and "b \ Field r"
  shows "(a, b) \ r \ (b, a) \ r - Id"
  using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force


subsubsection \<open>The upper and lower bounds operators\<close>

text \<open>
  Here we define upper (``above") and lower (``below") bounds operators. We
  think of \<open>r\<close> as a \<^emph>\<open>non-strict\<close> relation. The suffix \<open>S\<close> at the names of
  some operators indicates that the bounds are strict -- e.g., \<open>underS a\<close> is
  the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>). Capitalization of
  the first letter in the name reminds that the operator acts on sets, rather
  than on individual elements.
\<close>

definition under :: "'a rel \ 'a \ 'a set"
  where "under r a \ {b. (b, a) \ r}"

definition underS :: "'a rel \ 'a \ 'a set"
  where "underS r a \ {b. b \ a \ (b, a) \ r}"

definition Under :: "'a rel \ 'a set \ 'a set"
  where "Under r A \ {b \ Field r. \a \ A. (b, a) \ r}"

definition UnderS :: "'a rel \ 'a set \ 'a set"
  where "UnderS r A \ {b \ Field r. \a \ A. b \ a \ (b, a) \ r}"

definition above :: "'a rel \ 'a \ 'a set"
  where "above r a \ {b. (a, b) \ r}"

definition aboveS :: "'a rel \ 'a \ 'a set"
  where "aboveS r a \ {b. b \ a \ (a, b) \ r}"

definition Above :: "'a rel \ 'a set \ 'a set"
  where "Above r A \ {b \ Field r. \a \ A. (a, b) \ r}"

definition AboveS :: "'a rel \ 'a set \ 'a set"
  where "AboveS r A \ {b \ Field r. \a \ A. b \ a \ (a, b) \ r}"

definition ofilter :: "'a rel \ 'a set \ bool"
  where "ofilter r A \ A \ Field r \ (\a \ A. under r a \ A)"

text \<open>
  Note: In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>, we bounded
  comprehension by \<open>Field r\<close> in order to properly cover the case of \<open>A\<close> being
  empty.
\<close>

lemma underS_subset_under: "underS r a \ under r a"
  by (auto simp add: underS_def under_def)

lemma underS_notIn: "a \ underS r a"
  by (simp add: underS_def)

lemma Refl_under_in: "Refl r \ a \ Field r \ a \ under r a"
  by (simp add: refl_on_def under_def)

lemma AboveS_disjoint: "A \ (AboveS r A) = {}"
  by (auto simp add: AboveS_def)

lemma in_AboveS_underS: "a \ Field r \ a \ AboveS r (underS r a)"
  by (auto simp add: AboveS_def underS_def)

lemma Refl_under_underS: "Refl r \ a \ Field r \ under r a = underS r a \ {a}"
  unfolding under_def underS_def
  using refl_on_def[of _ r] by fastforce

lemma underS_empty: "a \ Field r \ underS r a = {}"
  by (auto simp: Field_def underS_def)

lemma under_Field: "under r a \ Field r"
  by (auto simp: under_def Field_def)

lemma underS_Field: "underS r a \ Field r"
  by (auto simp: underS_def Field_def)

lemma underS_Field2: "a \ Field r \ underS r a \ Field r"
  using underS_notIn underS_Field by fast

lemma underS_Field3: "Field r \ {} \ underS r a \ Field r"
  by (cases "a \ Field r") (auto simp: underS_Field2 underS_empty)

lemma AboveS_Field: "AboveS r A \ Field r"
  by (auto simp: AboveS_def Field_def)

lemma under_incr:
  assumes "trans r"
    and "(a, b) \ r"
  shows "under r a \ under r b"
  unfolding under_def
proof auto
  fix x assume "(x, a) \ r"
  with assms trans_def[of r] show "(x, b) \ r" by blast
qed

lemma underS_incr:
  assumes "trans r"
    and "antisym r"
    and ab: "(a, b) \ r"
  shows "underS r a \ underS r b"
  unfolding underS_def
proof auto
  assume *: "b \ a" and **: "(b, a) \ r"
  with \<open>antisym r\<close> antisym_def[of r] ab show False
    by blast
next
  fix x assume "x \ a" "(x, a) \ r"
  with ab \<open>trans r\<close> trans_def[of r] show "(x, b) \<in> r"
    by blast
qed

lemma underS_incl_iff:
  assumes LO: "Linear_order r"
    and INa: "a \ Field r"
    and INb: "b \ Field r"
  shows "underS r a \ underS r b \ (a, b) \ r"
    (is "?lhs \ ?rhs")
proof
  assume ?rhs
  with \<open>Linear_order r\<close> show ?lhs
    by (simp add: order_on_defs underS_incr)
next
  assume *: ?lhs
  have "(a, b) \ r" if "a = b"
    using assms that by (simp add: order_on_defs refl_on_def)
  moreover have False if "a \ b" "(b, a) \ r"
  proof -
    from that have "b \ underS r a" unfolding underS_def by blast
    with * have "b \ underS r b" by blast
    then show ?thesis by (simp add: underS_notIn)
  qed
  ultimately show "(a,b) \ r"
    using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
qed

lemma finite_Partial_order_induct[consumes 3, case_names step]:
  assumes "Partial_order r"
    and "x \ Field r"
    and "finite r"
    and step: "\x. x \ Field r \ (\y. y \ aboveS r x \ P y) \ P x"
  shows "P x"
  using assms(2)
proof (induct rule: wf_induct[of "r\ - Id"])
  case 1
  from assms(1,3) show "wf (r\ - Id)"
    using partial_order_on_well_order_on partial_order_on_converse by blast
next
  case prems: (2 x)
  show ?case
    by (rule step) (use prems in \<open>auto simp: aboveS_def intro: FieldI2\<close>)
qed

lemma finite_Linear_order_induct[consumes 3, case_names step]:
  assumes "Linear_order r"
    and "x \ Field r"
    and "finite r"
    and step: "\x. x \ Field r \ (\y. y \ aboveS r x \ P y) \ P x"
  shows "P x"
  using assms(2)
proof (induct rule: wf_induct[of "r\ - Id"])
  case 1
  from assms(1,3) show "wf (r\ - Id)"
    using linear_order_on_well_order_on linear_order_on_converse
    unfolding well_order_on_def by blast
next
  case prems: (2 x)
  show ?case
    by (rule step) (use prems in \<open>auto simp: aboveS_def intro: FieldI2\<close>)
qed


subsection \<open>Variations on Well-Founded Relations\<close>

text \<open>
  This subsection contains some variations of the results from \<^theory>\<open>HOL.Wellfounded\<close>:
    \<^item> means for slightly more direct definitions by well-founded recursion;
    \<^item> variations of well-founded induction;
    \<^item> means for proving a linear order to be a well-order.
\<close>


subsubsection \<open>Characterizations of well-foundedness\<close>

text \<open>
  A transitive relation is well-founded iff it is ``locally'' well-founded,
  i.e., iff its restriction to the lower bounds of of any element is
  well-founded.
\<close>

lemma trans_wf_iff:
  assumes "trans r"
  shows "wf r \ (\a. wf (r \ (r\``{a} \ r\``{a})))"
proof -
  define R where "R a = r \ (r\``{a} \ r\``{a})" for a
  have "wf (R a)" if "wf r" for a
    using that R_def wf_subset[of r "R a"] by auto
  moreover
  have "wf r" if *: "\a. wf(R a)"
    unfolding wf_def
  proof clarify
    fix phi a
    assume **: "\a. (\b. (b, a) \ r \ phi b) \ phi a"
    define chi where "chi b \ (b, a) \ r \ phi b" for b
    with * have "wf (R a)" by auto
    then have "(\b. (\c. (c, b) \ R a \ chi c) \ chi b) \ (\b. chi b)"
      unfolding wf_def by blast
    also have "\b. (\c. (c, b) \ R a \ chi c) \ chi b"
    proof (auto simp add: chi_def R_def)
      fix b
      assume "(b, a) \ r" and "\c. (c, b) \ r \ (c, a) \ r \ phi c"
      then have "\c. (c, b) \ r \ phi c"
        using assms trans_def[of r] by blast
      with ** show "phi b" by blast
    qed
    finally have  "\b. chi b" .
    with ** chi_def show "phi a" by blast
  qed
  ultimately show ?thesis unfolding R_def by blast
qed

text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
corollary wf_finite_segments:
  assumes "irrefl r" and "trans r" and "\x. finite {y. (y, x) \ r}"
  shows "wf (r)"
proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
  fix a
  have "trans (r \ ({x. (x, a) \ r} \ {x. (x, a) \ r}))"
    using assms unfolding trans_def Field_def by blast
  then show "acyclic (r \ {x. (x, a) \ r} \ {x. (x, a) \ r})"
    using assms acyclic_def assms irrefl_def by fastforce
qed

text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
  allowing one to assume the set included in the field.\<close>

lemma wf_eq_minimal2: "wf r \ (\A. A \ Field r \ A \ {} \ (\a \ A. \a' \ A. (a', a) \ r))"
proof-
  let ?phi = "\A. A \ {} \ (\a \ A. \a' \ A. (a',a) \ r)"
  have "wf r \ (\A. ?phi A)"
    apply (auto simp: ex_in_conv [THEN sym])
     apply (erule wfE_min)
      apply assumption
     apply blast
    apply (rule wfI_min)
    apply fast
    done
  also have "(\A. ?phi A) \ (\B \ Field r. ?phi B)"
  proof
    assume "\A. ?phi A"
    then show "\B \ Field r. ?phi B" by simp
  next
    assume *: "\B \ Field r. ?phi B"
    show "\A. ?phi A"
    proof clarify
      fix A :: "'a set"
      assume **: "A \ {}"
      define B where "B = A \ Field r"
      show "\a \ A. \a' \ A. (a', a) \ r"
      proof (cases "B = {}")
        case True
        with ** obtain a where a: "a \ A" "a \ Field r"
          unfolding B_def by blast
        with a have "\a' \ A. (a',a) \ r"
          unfolding Field_def by blast
        with a show ?thesis by blast
      next
        case False
        have "B \ Field r" unfolding B_def by blast
        with False * obtain a where a: "a \ B" "\a' \ B. (a', a) \ r"
          by blast
        have "(a', a) \ r" if "a' \ A" for a'
        proof
          assume a'a: "(a', a) \<in> r"
          with that have "a' \ B" unfolding B_def Field_def by blast
          with a a'a show False by blast
        qed
        with a show ?thesis unfolding B_def by blast
      qed
    qed
  qed
  finally show ?thesis by blast
qed


subsubsection \<open>Characterizations of well-foundedness\<close>

text \<open>
  The next lemma and its corollary enable one to prove that a linear order is
  a well-order in a way which is more standard than via well-foundedness of
  the strict version of the relation.
\<close>

lemma Linear_order_wf_diff_Id:
  assumes "Linear_order r"
  shows "wf (r - Id) \ (\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r))"
proof (cases "r \ Id")
  case True
  then have *: "r - Id = {}" by blast
  have "wf (r - Id)" by (simp add: *)
  moreover have "\a \ A. \a' \ A. (a, a') \ r"
    if *: "A \ Field r" and **: "A \ {}" for A
  proof -
    from \<open>Linear_order r\<close> True
    obtain a where a: "r = {} \ r = {(a, a)}"
      unfolding order_on_defs using Total_subset_Id [of r] by blast
    with * ** have "A = {a} \ r = {(a, a)}"
      unfolding Field_def by blast
    with a show ?thesis by blast
  qed
  ultimately show ?thesis by blast
next
  case False
  with \<open>Linear_order r\<close> have Field: "Field r = Field (r - Id)"
    unfolding order_on_defs using Total_Id_Field [of r] by blast
  show ?thesis
  proof
    assume *: "wf (r - Id)"
    show "\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r)"
    proof clarify
      fix A
      assume **: "A \ Field r" and ***: "A \ {}"
      then have "\a \ A. \a' \ A. (a',a) \ r - Id"
        using Field * unfolding wf_eq_minimal2 by simp
      moreover have "\a \ A. \a' \ A. (a, a') \ r \ (a', a) \ r - Id"
        using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** by blast
      ultimately show "\a \ A. \a' \ A. (a, a') \ r" by blast
    qed
  next
    assume *: "\A \ Field r. A \ {} \ (\a \ A. \a' \ A. (a, a') \ r)"
    show "wf (r - Id)"
      unfolding wf_eq_minimal2
    proof clarify
      fix A
      assume **: "A \ Field(r - Id)" and ***: "A \ {}"
      then have "\a \ A. \a' \ A. (a,a') \ r"
        using Field * by simp
      moreover have "\a \ A. \a' \ A. (a, a') \ r \ (a', a) \ r - Id"
        using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** mono_Field[of "r - Id" r] by blast
      ultimately show "\a \ A. \a' \ A. (a',a) \ r - Id"
        by blast
    qed
  qed
qed

corollary Linear_order_Well_order_iff:
  "Linear_order r \
    Well_order r \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
  unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast

end

¤ Dauer der Verarbeitung: 0.22 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff