Quelle Algebraic.thy Sprache: Isabelle

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

section \<open>Algebraic deflations\<close>

theory Algebraic
imports Universal Map_Functions
begin

subsection \<open>Type constructor for finite deflations\<close>

typedef 'a::bifinite fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
by (fast intro: finite_deflation_bottom)

instantiation fin_defl :: (bifinite) below
begin

definition below_fin_defl_def:
  "below \ \x y. Rep_fin_defl x \ Rep_fin_defl y"

instance ..
end

instance fin_defl :: (bifinite) po
using type_definition_fin_defl below_fin_defl_def
by (rule typedef_po_class)

lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
using Rep_fin_defl by simp

lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
using finite_deflation_Rep_fin_defl
by (rule finite_deflation_imp_deflation)

interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
by (rule finite_deflation_Rep_fin_defl)

lemma fin_defl_belowI:
  "(\x. Rep_fin_defl a\x = x \ Rep_fin_defl b\x = x) \ a \ b"
unfolding below_fin_defl_def
by (rule Rep_fin_defl.belowI)

lemma fin_defl_belowD:
  "\a \ b; Rep_fin_defl a\x = x\ \ Rep_fin_defl b\x = x"
unfolding below_fin_defl_def
by (rule Rep_fin_defl.belowD)

lemma fin_defl_eqI:
  "a = b" if "(\x. Rep_fin_defl a\x = x \ Rep_fin_defl b\x = x)"
proof (rule below_antisym)
  show "a \ b" by (rule fin_defl_belowI) (simp add: that)
  show "b \ a" by (rule fin_defl_belowI) (simp add: that)
qed

lemma Rep_fin_defl_mono: "a \ b \ Rep_fin_defl a \ Rep_fin_defl b"
unfolding below_fin_defl_def .

lemma Abs_fin_defl_mono:
  "\finite_deflation a; finite_deflation b; a \ b\
    \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
unfolding below_fin_defl_def
by (simp add: Abs_fin_defl_inverse)

lemma (in finite_deflation) compact_belowI:
  "d \ f" if "\x. compact x \ d\x = x \ f\x = x"
  by (rule belowI, rule that, erule subst, rule compact)

lemma compact_Rep_fin_defl [simp]: "compact (Rep_fin_defl a)"
using finite_deflation_Rep_fin_defl
by (rule finite_deflation_imp_compact)

subsection \<open>Defining algebraic deflations by ideal completion\<close>

typedef 'a::bifinite defl = "{S::'a fin_defl set. below.ideal S}"
by (rule below.ex_ideal)

instantiation defl :: (bifinite) below
begin

definition "x \ y \ Rep_defl x \ Rep_defl y"

instance ..

end

instance defl :: (bifinite) po
using type_definition_defl below_defl_def
by (rule below.typedef_ideal_po)

instance defl :: (bifinite) cpo
using type_definition_defl below_defl_def
by (rule below.typedef_ideal_cpo)

definition defl_principal :: "'a::bifinite fin_defl \ 'a defl"
  where "defl_principal t = Abs_defl {u. u \ t}"

lemma fin_defl_countable: "\f::'a::bifinite fin_defl \ nat. inj f"
proof -
  obtain f :: "'a compact_basis \ nat" where inj_f: "inj f"
    using compact_basis.countable ..
  have *: "\d. finite (f ` Rep_compact_basis -` {x. Rep_fin_defl d\x = x})"
    apply (rule finite_imageI)
    apply (rule finite_vimageI)
    apply (rule Rep_fin_defl.finite_fixes)
    apply (simp add: inj_on_def Rep_compact_basis_inject)
    done
  have range_eq: "range Rep_compact_basis = {x. compact x}"
    using type_definition_compact_basis by (rule type_definition.Rep_range)
  have "inj (\d. set_encode
    (f ` Rep_compact_basis -` {x. Rep_fin_defl d\<cdot>x = x}))"
    apply (rule inj_onI)
    apply (simp only: set_encode_eq *)
    apply (simp only: inj_image_eq_iff inj_f)
    apply (drule_tac f="image Rep_compact_basis" in arg_cong)
    apply (simp del: vimage_Collect_eq add: range_eq set_eq_iff)
    apply (rule Rep_fin_defl_inject [THEN iffD1])
    apply (rule below_antisym)
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
    apply (drule_tac x=z in spec, simp)
    apply (rule Rep_fin_defl.compact_belowI, rename_tac z)
    apply (drule_tac x=z in spec, simp)
    done
  thus ?thesis by - (rule exI)
qed

interpretation defl: ideal_completion below defl_principal Rep_defl
using type_definition_defl below_defl_def
using defl_principal_def fin_defl_countable
by (rule below.typedef_ideal_completion)

text \<open>Algebraic deflations are pointed\<close>

lemma defl_minimal: "defl_principal (Abs_fin_defl \) \ x"
proof (induct x rule: defl.principal_induct)
  fix a :: "'a fin_defl"
  have "Abs_fin_defl \ \ a"
    by (simp add: below_fin_defl_def Abs_fin_defl_inverse finite_deflation_bottom)
  then show "defl_principal (Abs_fin_defl \) \ defl_principal a"
    by (rule defl.principal_mono)
qed simp

instance defl :: (bifinite) pcpo
by intro_classes (fast intro: defl_minimal)

lemma inst_defl_pcpo: "\ = defl_principal (Abs_fin_defl \)"
by (rule defl_minimal [THEN bottomI, symmetric])

subsection \<open>Applying algebraic deflations\<close>

definition cast :: "'a::bifinite defl \ 'a \ 'a"
  where "cast = defl.extension Rep_fin_defl"

lemma cast_defl_principal: "cast\(defl_principal a) = Rep_fin_defl a"
  unfolding cast_def
  by (rule defl.extension_principal) (simp only: below_fin_defl_def)

lemma deflation_cast: "deflation (cast\d)"
apply (induct d rule: defl.principal_induct)
apply (rule adm_subst [OF _ adm_deflation], simp)
apply (simp add: cast_defl_principal)
apply (rule finite_deflation_imp_deflation)
apply (rule finite_deflation_Rep_fin_defl)
done

lemma finite_deflation_cast: "compact d \ finite_deflation (cast\d)"
  apply (drule defl.compact_imp_principal)
  apply clarify
  apply (simp add: cast_defl_principal)
  apply (rule finite_deflation_Rep_fin_defl)
  done

interpretation cast: deflation "cast\d"
by (rule deflation_cast)

declare cast.idem [simp]

lemma compact_cast [simp]: "compact (cast\d)" if "compact d"
  by (rule finite_deflation_imp_compact) (use that in \<open>rule finite_deflation_cast\<close>)

lemma cast_below_cast: "cast\A \ cast\B \ A \ B"
apply (induct A rule: defl.principal_induct, simp)
apply (induct B rule: defl.principal_induct, simp)
apply (simp add: cast_defl_principal below_fin_defl_def)
done

lemma compact_cast_iff: "compact (cast\d) \ compact d"
apply (rule iffI)
apply (simp only: compact_def cast_below_cast [symmetric])
apply (erule adm_subst [OF cont_Rep_cfun2])
apply (erule compact_cast)
done

lemma cast_below_imp_below: "cast\A \ cast\B \ A \ B"
by (simp only: cast_below_cast)

lemma cast_eq_imp_eq: "cast\A = cast\B \ A = B"
by (simp add: below_antisym cast_below_imp_below)

lemma cast_strict1 [simp]: "cast\\ = \"
apply (subst inst_defl_pcpo)
apply (subst cast_defl_principal)
apply (rule Abs_fin_defl_inverse)
apply (simp add: finite_deflation_bottom)
done

lemma cast_strict2 [simp]: "cast\A\\ = \"
by (rule cast.below [THEN bottomI])

subsection \<open>Deflation combinators\<close>

definition
  "defl_fun1 e p f =
    defl.extension (\<lambda>a.
      defl_principal (Abs_fin_defl
        (e oo f\<cdot>(Rep_fin_defl a) oo p)))"

definition
  "defl_fun2 e p f =
    defl.extension (\<lambda>a.
      defl.extension (\<lambda>b.
        defl_principal (Abs_fin_defl
          (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"

lemma cast_defl_fun1:
  assumes ep: "ep_pair e p"
  assumes f: "\a. finite_deflation a \ finite_deflation (f\a)"
  shows "cast\(defl_fun1 e p f\A) = e oo f\(cast\A) oo p"
proof -
  have 1: "finite_deflation (e oo f\(Rep_fin_defl a) oo p)" for a
  proof -
    have "finite_deflation (f\(Rep_fin_defl a))"
      using finite_deflation_Rep_fin_defl by (rule f)
    with ep show ?thesis
      by (rule ep_pair.finite_deflation_e_d_p)
  qed
  show ?thesis
    by (induct A rule: defl.principal_induct, simp)
       (simp only: defl_fun1_def
                   defl.extension_principal
                   defl.extension_mono
                   defl.principal_mono
                   Abs_fin_defl_mono [OF 1 1]
                   monofun_cfun below_refl
                   Rep_fin_defl_mono
                   cast_defl_principal
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed

lemma cast_defl_fun2:
  assumes ep: "ep_pair e p"
  assumes f: "\a b. finite_deflation a \ finite_deflation b \
                finite_deflation (f\<cdot>a\<cdot>b)"
  shows "cast\(defl_fun2 e p f\A\B) = e oo f\(cast\A)\(cast\B) oo p"
proof -
  have 1: "finite_deflation (e oo f\(Rep_fin_defl a)\(Rep_fin_defl b) oo p)" for a b
  proof -
    have "finite_deflation (f\(Rep_fin_defl a)\(Rep_fin_defl b))"
      using finite_deflation_Rep_fin_defl finite_deflation_Rep_fin_defl by (rule f)
    with ep show ?thesis
      by (rule ep_pair.finite_deflation_e_d_p)
  qed
  show ?thesis
    apply (induct A rule: defl.principal_induct, simp)
    apply (induct B rule: defl.principal_induct, simp)
    by (simp only: defl_fun2_def
                   defl.extension_principal
                   defl.extension_mono
                   defl.principal_mono
                   Abs_fin_defl_mono [OF 1 1]
                   monofun_cfun below_refl
                   Rep_fin_defl_mono
                   cast_defl_principal
                   Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed

end

quality100%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.