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

Quelle Deflation.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/Deflation.thy
    Author:     Brian Huffman
*)

section \<open>Continuous deflations and ep-pairs\<close>

theory Deflation
  imports Cfun
begin

subsection \<open>Continuous deflations\<close>

locale deflation =
  fixes d :: "'a \ 'a"
  assumes idem: "\x. d\(d\x) = d\x"
  assumes below: "\x. d\x \ x"
begin

lemma below_ID: "d \ ID"
  by (rule cfun_belowI) (simp add: below)

text \<open>The set of fixed points is the same as the range.\<close>

lemma fixes_eq_range: "{x. d\x = x} = range (\x. d\x)"
  by (auto simp add: eq_sym_conv idem)

lemma range_eq_fixes: "range (\x. d\x) = {x. d\x = x}"
  by (auto simp add: eq_sym_conv idem)

text \<open>
  The pointwise ordering on deflation functions coincides with
  the subset ordering of their sets of fixed-points.
\<close>

lemma belowI:
  assumes f: "\x. d\x = x \ f\x = x"
  shows "d \ f"
proof (rule cfun_belowI)
  fix x
  from below have "f\(d\x) \ f\x"
    by (rule monofun_cfun_arg)
  also from idem have "f\(d\x) = d\x"
    by (rule f)
  finally show "d\x \ f\x" .
qed

lemma belowD: "\f \ d; f\x = x\ \ d\x = x"
proof (rule below_antisym)
  from below show "d\x \ x" .
  assume "f \ d"
  then have "f\x \ d\x" by (rule monofun_cfun_fun)
  also assume "f\x = x"
  finally show "x \ d\x" .
qed

end

lemma deflation_strict: "deflation d \ d\\ = \"
  by (rule deflation.below [THEN bottomI])

lemma adm_deflation: "adm (\d. deflation d)"
  by (simp add: deflation_def)

lemma deflation_ID: "deflation ID"
  by (simp add: deflation.intro)

lemma deflation_bottom: "deflation \"
  by (simp add: deflation.intro)

lemma deflation_below_iff: "deflation p \ deflation q \ p \ q \ (\x. p\x = x \ q\x = x)"
  apply safe
   apply (simp add: deflation.belowD)
  apply (simp add: deflation.belowI)
  done

text \<open>
  The composition of two deflations is equal to
  the lesser of the two (if they are comparable).
\<close>

lemma deflation_below_comp1:
  assumes "deflation f"
  assumes "deflation g"
  shows "f \ g \ f\(g\x) = f\x"
proof (rule below_antisym)
  interpret g: deflation g by fact
  from g.below show "f\(g\x) \ f\x" by (rule monofun_cfun_arg)
next
  interpret f: deflation f by fact
  assume "f \ g"
  then have "f\x \ g\x" by (rule monofun_cfun_fun)
  then have "f\(f\x) \ f\(g\x)" by (rule monofun_cfun_arg)
  also have "f\(f\x) = f\x" by (rule f.idem)
  finally show "f\x \ f\(g\x)" .
qed

lemma deflation_below_comp2: "deflation f \ deflation g \ f \ g \ g\(f\x) = f\x"
  by (simp only: deflation.belowD deflation.idem)

subsection \<open>Deflations with finite range\<close>

lemma finite_range_imp_finite_fixes:
  assumes "finite (range f)"
  shows "finite {x. f x = x}"
proof -
  have "{x. f x = x} \ range f"
    by (clarify, erule subst, rule rangeI)
  from this assms show "finite {x. f x = x}"
    by (rule finite_subset)
qed

locale finite_deflation = deflation +
  assumes finite_fixes: "finite {x. d\x = x}"
begin

lemma finite_range: "finite (range (\x. d\x))"
  by (simp add: range_eq_fixes finite_fixes)

lemma finite_image: "finite ((\x. d\x) ` A)"
  by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range])

lemma compact: "compact (d\x)"
proof (rule compactI2)
  fix Y :: "nat \ 'a"
  assume Y: "chain Y"
  have "finite_chain (\i. d\(Y i))"
  proof (rule finite_range_imp_finch)
    from Y show "chain (\i. d\(Y i))" by simp
    have "range (\i. d\(Y i)) \ range (\x. d\x)" by auto
    then show "finite (range (\i. d\(Y i)))"
      using finite_range by (rule finite_subset)
  qed
  then have "\j. (\i. d\(Y i)) = d\(Y j)"
    by (simp add: finite_chain_def maxinch_is_thelub Y)
  then obtain j where j: "(\i. d\(Y i)) = d\(Y j)" ..

  assume "d\x \ (\i. Y i)"
  then have "d\(d\x) \ d\(\i. Y i)"
    by (rule monofun_cfun_arg)
  then have "d\x \ (\i. d\(Y i))"
    by (simp add: contlub_cfun_arg Y idem)
  with j have "d\x \ d\(Y j)" by simp
  then have "d\x \ Y j"
    using below by (rule below_trans)
  then show "\j. d\x \ Y j" ..
qed

end

lemma finite_deflation_intro: "deflation d \ finite {x. d\x = x} \ finite_deflation d"
  by (intro finite_deflation.intro finite_deflation_axioms.intro)

lemma finite_deflation_imp_deflation: "finite_deflation d \ deflation d"
  by (simp add: finite_deflation_def)

lemma finite_deflation_bottom: "finite_deflation \"
  by standard simp_all

subsection \<open>Continuous embedding-projection pairs\<close>

locale ep_pair =
  fixes e :: "'a \ 'b" and p :: "'b \ 'a"
  assumes e_inverse [simp]: "\x. p\(e\x) = x"
  and e_p_below: "\y. e\(p\y) \ y"
begin

lemma e_below_iff [simp]: "e\x \ e\y \ x \ y"
proof
  assume "e\x \ e\y"
  then have "p\(e\x) \ p\(e\y)" by (rule monofun_cfun_arg)
  then show "x \ y" by simp
next
  assume "x \ y"
  then show "e\x \ e\y" by (rule monofun_cfun_arg)
qed

lemma e_eq_iff [simp]: "e\x = e\y \ x = y"
  unfolding po_eq_conv e_below_iff ..

lemma p_eq_iff: "e\(p\x) = x \ e\(p\y) = y \ p\x = p\y \ x = y"
  by (safe, erule subst, erule subst, simp)

lemma p_inverse: "(\x. y = e\x) \ e\(p\y) = y"
  by (auto, rule exI, erule sym)

lemma e_below_iff_below_p: "e\x \ y \ x \ p\y"
proof
  assume "e\x \ y"
  then have "p\(e\x) \ p\y" by (rule monofun_cfun_arg)
  then show "x \ p\y" by simp
next
  assume "x \ p\y"
  then have "e\x \ e\(p\y)" by (rule monofun_cfun_arg)
  then show "e\x \ y" using e_p_below by (rule below_trans)
qed

lemma compact_e_rev: "compact (e\x) \ compact x"
proof -
  assume "compact (e\x)"
  then have "adm (\y. e\x \ y)" by (rule compactD)
  then have "adm (\y. e\x \ e\y)" by (rule adm_subst [OF cont_Rep_cfun2])
  then have "adm (\y. x \ y)" by simp
  then show "compact x" by (rule compactI)
qed

lemma compact_e:
  assumes "compact x"
  shows "compact (e\x)"
proof -
  from assms have "adm (\y. x \ y)" by (rule compactD)
  then have "adm (\y. x \ p\y)" by (rule adm_subst [OF cont_Rep_cfun2])
  then have "adm (\y. e\x \ y)" by (simp add: e_below_iff_below_p)
  then show "compact (e\x)" by (rule compactI)
qed

lemma compact_e_iff: "compact (e\x) \ compact x"
  by (rule iffI [OF compact_e_rev compact_e])

text \<open>Deflations from ep-pairs\<close>

lemma deflation_e_p: "deflation (e oo p)"
  by (simp add: deflation.intro e_p_below)

lemma deflation_e_d_p:
  assumes "deflation d"
  shows "deflation (e oo d oo p)"
proof
  interpret deflation d by fact
  fix x :: 'b
  show "(e oo d oo p)\((e oo d oo p)\x) = (e oo d oo p)\x"
    by (simp add: idem)
  show "(e oo d oo p)\x \ x"
    by (simp add: e_below_iff_below_p below)
qed

lemma finite_deflation_e_d_p:
  assumes "finite_deflation d"
  shows "finite_deflation (e oo d oo p)"
proof
  interpret finite_deflation d by fact
  fix x :: 'b
  show "(e oo d oo p)\((e oo d oo p)\x) = (e oo d oo p)\x"
    by (simp add: idem)
  show "(e oo d oo p)\x \ x"
    by (simp add: e_below_iff_below_p below)
  have "finite ((\x. e\x) ` (\x. d\x) ` range (\x. p\x))"
    by (simp add: finite_image)
  then have "finite (range (\x. (e oo d oo p)\x))"
    by (simp add: image_image)
  then show "finite {x. (e oo d oo p)\x = x}"
    by (rule finite_range_imp_finite_fixes)
qed

lemma deflation_p_d_e:
  assumes "deflation d"
  assumes d: "\x. d\x \ e\(p\x)"
  shows "deflation (p oo d oo e)"
proof -
  interpret d: deflation d by fact
  have p_d_e_below: "(p oo d oo e)\x \ x" for x
  proof -
    have "d\(e\x) \ e\x"
      by (rule d.below)
    then have "p\(d\(e\x)) \ p\(e\x)"
      by (rule monofun_cfun_arg)
    then show ?thesis by simp
  qed
  show ?thesis
  proof
    show "(p oo d oo e)\x \ x" for x
      by (rule p_d_e_below)
    show "(p oo d oo e)\((p oo d oo e)\x) = (p oo d oo e)\x" for x
    proof (rule below_antisym)
      show "(p oo d oo e)\((p oo d oo e)\x) \ (p oo d oo e)\x"
        by (rule p_d_e_below)
      have "p\(d\(d\(d\(e\x)))) \ p\(d\(e\(p\(d\(e\x)))))"
        by (intro monofun_cfun_arg d)
      then have "p\(d\(e\x)) \ p\(d\(e\(p\(d\(e\x)))))"
        by (simp only: d.idem)
      then show "(p oo d oo e)\x \ (p oo d oo e)\((p oo d oo e)\x)"
        by simp
    qed
  qed
qed

lemma finite_deflation_p_d_e:
  assumes "finite_deflation d"
  assumes d: "\x. d\x \ e\(p\x)"
  shows "finite_deflation (p oo d oo e)"
proof -
  interpret d: finite_deflation d by fact
  show ?thesis
  proof (rule finite_deflation_intro)
    have "deflation d" ..
    then show "deflation (p oo d oo e)"
      using d by (rule deflation_p_d_e)
  next
    have "finite ((\x. d\x) ` range (\x. e\x))"
      by (rule d.finite_image)
    then have "finite ((\x. p\x) ` (\x. d\x) ` range (\x. e\x))"
      by (rule finite_imageI)
    then have "finite (range (\x. (p oo d oo e)\x))"
      by (simp add: image_image)
    then show "finite {x. (p oo d oo e)\x = x}"
      by (rule finite_range_imp_finite_fixes)
  qed
qed

end

subsection \<open>Uniqueness of ep-pairs\<close>

lemma ep_pair_unique_e_lemma:
  assumes 1: "ep_pair e1 p"
    and 2: "ep_pair e2 p"
  shows "e1 \ e2"
proof (rule cfun_belowI)
  fix x
  have "e1\(p\(e2\x)) \ e2\x"
    by (rule ep_pair.e_p_below [OF 1])
  then show "e1\x \ e2\x"
    by (simp only: ep_pair.e_inverse [OF 2])
qed

lemma ep_pair_unique_e: "ep_pair e1 p \ ep_pair e2 p \ e1 = e2"
  by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)

lemma ep_pair_unique_p_lemma:
  assumes 1: "ep_pair e p1"
    and 2: "ep_pair e p2"
  shows "p1 \ p2"
proof (rule cfun_belowI)
  fix x
  have "e\(p1\x) \ x"
    by (rule ep_pair.e_p_below [OF 1])
  then have "p2\(e\(p1\x)) \ p2\x"
    by (rule monofun_cfun_arg)
  then show "p1\x \ p2\x"
    by (simp only: ep_pair.e_inverse [OF 2])
qed

lemma ep_pair_unique_p: "ep_pair e p1 \ ep_pair e p2 \ p1 = p2"
  by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)

subsection \<open>Composing ep-pairs\<close>

lemma ep_pair_ID_ID: "ep_pair ID ID"
  by standard simp_all

lemma ep_pair_comp:
  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
  shows "ep_pair (e2 oo e1) (p1 oo p2)"
proof
  interpret ep1: ep_pair e1 p1 by fact
  interpret ep2: ep_pair e2 p2 by fact
  fix x y
  show "(p1 oo p2)\((e2 oo e1)\x) = x"
    by simp
  have "e1\(p1\(p2\y)) \ p2\y"
    by (rule ep1.e_p_below)
  then have "e2\(e1\(p1\(p2\y))) \ e2\(p2\y)"
    by (rule monofun_cfun_arg)
  also have "e2\(p2\y) \ y"
    by (rule ep2.e_p_below)
  finally show "(e2 oo e1)\((p1 oo p2)\y) \ y"
    by simp
qed

locale pcpo_ep_pair = ep_pair e p
  for e :: "'a::pcpo \ 'b::pcpo"
  and p :: "'b::pcpo \ 'a::pcpo"
begin

lemma e_strict [simp]: "e\\ = \"
proof -
  have "\ \ p\\" by (rule minimal)
  then have "e\\ \ e\(p\\)" by (rule monofun_cfun_arg)
  also have "e\(p\\) \ \" by (rule e_p_below)
  finally show "e\\ = \" by simp
qed

lemma e_bottom_iff [simp]: "e\x = \ \ x = \"
  by (rule e_eq_iff [where y="\", unfolded e_strict])

lemma e_defined: "x \ \ \ e\x \ \"
  by simp

lemma p_strict [simp]: "p\\ = \"
  by (rule e_inverse [where x="\", unfolded e_strict])

lemmas stricts = e_strict p_strict

end

end

quality99%

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