Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Domain.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Domain package\<close>

theory Domain
imports Representable Domain_Aux
keywords
  "lazy" "unsafe" and
  "domaindef" "domain" :: thy_defn and
  "domain_isomorphism" :: thy_decl
begin

default_sort "domain"

subsection \<open>Representations of types\<close>

lemma emb_prj: "emb\((prj\x)::'a) = cast\DEFL('a)\x"
by (simp add: cast_DEFL)

lemma emb_prj_emb:
  fixes x :: "'a"
  assumes "DEFL('a) \ DEFL('b)"
  shows "emb\(prj\(emb\x) :: 'b) = emb\x"
unfolding emb_prj
apply (rule cast.belowD)
apply (rule monofun_cfun_arg [OF assms])
apply (simp add: cast_DEFL)
done

lemma prj_emb_prj:
  assumes "DEFL('a) \ DEFL('b)"
  shows "prj\(emb\(prj\x :: 'b)) = (prj\x :: 'a)"
apply (rule emb_eq_iff [THEN iffD1])
apply (simp only: emb_prj)
apply (rule deflation_below_comp1)
   apply (rule deflation_cast)
  apply (rule deflation_cast)
apply (rule monofun_cfun_arg [OF assms])
done

text \<open>Isomorphism lemmas used internally by the domain package:\<close>

lemma domain_abs_iso:
  fixes abs and rep
  assumes DEFL: "DEFL('b) = DEFL('a)"
  assumes abs_def: "(abs :: 'a \ 'b) \ prj oo emb"
  assumes rep_def: "(rep :: 'b \ 'a) \ prj oo emb"
  shows "rep\(abs\x) = x"
unfolding abs_def rep_def
by (simp add: emb_prj_emb DEFL)

lemma domain_rep_iso:
  fixes abs and rep
  assumes DEFL: "DEFL('b) = DEFL('a)"
  assumes abs_def: "(abs :: 'a \ 'b) \ prj oo emb"
  assumes rep_def: "(rep :: 'b \ 'a) \ prj oo emb"
  shows "abs\(rep\x) = x"
unfolding abs_def rep_def
by (simp add: emb_prj_emb DEFL)

subsection \<open>Deflations as sets\<close>

definition defl_set :: "'a::bifinite defl \ 'a set"
where "defl_set A = {x. cast\A\x = x}"

lemma adm_defl_set: "adm (\x. x \ defl_set A)"
unfolding defl_set_def by simp

lemma defl_set_bottom: "\ \ defl_set A"
unfolding defl_set_def by simp

lemma defl_set_cast [simp]: "cast\A\x \ defl_set A"
unfolding defl_set_def by simp

lemma defl_set_subset_iff: "defl_set A \ defl_set B \ A \ B"
apply (simp add: defl_set_def subset_eq cast_below_cast [symmetric])
apply (auto simp add: cast.belowI cast.belowD)
done

subsection \<open>Proving a subtype is representable\<close>

text \<open>Temporarily relax type constraints.\<close>

setup \<open>
  fold Sign.add_const_constraint
  [ (\<^const_name>\<open>defl\<close>, SOME \<^typ>\<open>'a::pcpo itself \<Rightarrow> udom defl\<close>)
  , (\<^const_name>\<open>emb\<close>, SOME \<^typ>\<open>'a::pcpo \<rightarrow> udom\<close>)
  , (\<^const_name>\<open>prj\<close>, SOME \<^typ>\<open>udom \<rightarrow> 'a::pcpo\<close>)
  , (\<^const_name>\<open>liftdefl\<close>, SOME \<^typ>\<open>'a::pcpo itself \<Rightarrow> udom u defl\<close>)
  , (\<^const_name>\<open>liftemb\<close>, SOME \<^typ>\<open>'a::pcpo u \<rightarrow> udom u\<close>)
  , (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::pcpo u\<close>) ]
\<close>

lemma typedef_domain_class:
  fixes Rep :: "'a::pcpo \ udom"
  fixes Abs :: "udom \ 'a::pcpo"
  fixes t :: "udom defl"
  assumes type: "type_definition Rep Abs (defl_set t)"
  assumes below: "(\) \ \x y. Rep x \ Rep y"
  assumes emb: "emb \ (\ x. Rep x)"
  assumes prj: "prj \ (\ x. Abs (cast\t\x))"
  assumes defl: "defl \ (\ a::'a itself. t)"
  assumes liftemb: "(liftemb :: 'a u \ udom u) \ u_map\emb"
  assumes liftprj: "(liftprj :: udom u \ 'a u) \ u_map\prj"
  assumes liftdefl: "(liftdefl :: 'a itself \ _) \ (\t. liftdefl_of\DEFL('a))"
  shows "OFCLASS('a, domain_class)"
proof
  have emb_beta: "\x. emb\x = Rep x"
    unfolding emb
    apply (rule beta_cfun)
    apply (rule typedef_cont_Rep [OF type below adm_defl_set cont_id])
    done
  have prj_beta: "\y. prj\y = Abs (cast\t\y)"
    unfolding prj
    apply (rule beta_cfun)
    apply (rule typedef_cont_Abs [OF type below adm_defl_set])
    apply simp_all
    done
  have prj_emb: "\x::'a. prj\(emb\x) = x"
    using type_definition.Rep [OF type]
    unfolding prj_beta emb_beta defl_set_def
    by (simp add: type_definition.Rep_inverse [OF type])
  have emb_prj: "\y. emb\(prj\y :: 'a) = cast\t\y"
    unfolding prj_beta emb_beta
    by (simp add: type_definition.Abs_inverse [OF type])
  show "ep_pair (emb :: 'a \ udom) prj"
    apply standard
    apply (simp add: prj_emb)
    apply (simp add: emb_prj cast.below)
    done
  show "cast\DEFL('a) = emb oo (prj :: udom \ 'a)"
    by (rule cfun_eqI, simp add: defl emb_prj)
qed (simp_all only: liftemb liftprj liftdefl)

lemma typedef_DEFL:
  assumes "defl \ (\a::'a::pcpo itself. t)"
  shows "DEFL('a::pcpo) = t"
unfolding assms ..

text \<open>Restore original typing constraints.\<close>

setup \<open>
  fold Sign.add_const_constraint
   [(\<^const_name>\<open>defl\<close>, SOME \<^typ>\<open>'a::domain itself \<Rightarrow> udom defl\<close>),
    (\<^const_name>\<open>emb\<close>, SOME \<^typ>\<open>'a::domain \<rightarrow> udom\<close>),
    (\<^const_name>\<open>prj\<close>, SOME \<^typ>\<open>udom \<rightarrow> 'a::domain\<close>),
    (\<^const_name>\<open>liftdefl\<close>, SOME \<^typ>\<open>'a::predomain itself \<Rightarrow> udom u defl\<close>),
    (\<^const_name>\<open>liftemb\<close>, SOME \<^typ>\<open>'a::predomain u \<rightarrow> udom u\<close>),
    (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::predomain u\<close>)]
\<close>

ML_file \<open>Tools/domaindef.ML\<close>

subsection \<open>Isomorphic deflations\<close>

definition isodefl :: "('a \ 'a) \ udom defl \ bool"
  where "isodefl d t \ cast\t = emb oo d oo prj"

definition isodefl' :: "('a::predomain \<rightarrow> 'a) \<Rightarrow> udom u defl \<Rightarrow> bool"
  where "isodefl' d t \ cast\t = liftemb oo u_map\d oo liftprj"

lemma isodeflI: "(\x. cast\t\x = emb\(d\(prj\x))) \ isodefl d t"
unfolding isodefl_def by (simp add: cfun_eqI)

lemma cast_isodefl: "isodefl d t \ cast\t = (\ x. emb\(d\(prj\x)))"
unfolding isodefl_def by (simp add: cfun_eqI)

lemma isodefl_strict: "isodefl d t \ d\\ = \"
unfolding isodefl_def
by (drule cfun_fun_cong [where x="\"], simp)

lemma isodefl_imp_deflation:
  fixes d :: "'a \ 'a"
  assumes "isodefl d t" shows "deflation d"
proof
  note assms [unfolded isodefl_def, simp]
  fix x :: 'a
  show "d\(d\x) = d\x"
    using cast.idem [of t "emb\x"] by simp
  show "d\x \ x"
    using cast.below [of t "emb\x"] by simp
qed

lemma isodefl_ID_DEFL: "isodefl (ID :: 'a \ 'a) DEFL('a)"
unfolding isodefl_def by (simp add: cast_DEFL)

lemma isodefl_LIFTDEFL:
  "isodefl' (ID :: 'a \ 'a) LIFTDEFL('a::predomain)"
unfolding isodefl'_def by (simp add: cast_liftdefl u_map_ID)

lemma isodefl_DEFL_imp_ID: "isodefl (d :: 'a \ 'a) DEFL('a) \ d = ID"
unfolding isodefl_def
apply (simp add: cast_DEFL)
apply (simp add: cfun_eq_iff)
apply (rule allI)
apply (drule_tac x="emb\x" in spec)
apply simp
done

lemma isodefl_bottom: "isodefl \ \"
unfolding isodefl_def by (simp add: cfun_eq_iff)

lemma adm_isodefl:
  "cont f \ cont g \ adm (\x. isodefl (f x) (g x))"
unfolding isodefl_def by simp

lemma isodefl_lub:
  assumes "chain d" and "chain t"
  assumes "\i. isodefl (d i) (t i)"
  shows "isodefl (\i. d i) (\i. t i)"
using assms unfolding isodefl_def
by (simp add: contlub_cfun_arg contlub_cfun_fun)

lemma isodefl_fix:
  assumes "\d t. isodefl d t \ isodefl (f\d) (g\t)"
  shows "isodefl (fix\f) (fix\g)"
unfolding fix_def2
apply (rule isodefl_lub, simp, simp)
apply (induct_tac i)
apply (simp add: isodefl_bottom)
apply (simp add: assms)
done

lemma isodefl_abs_rep:
  fixes abs and rep and d
  assumes DEFL: "DEFL('b) = DEFL('a)"
  assumes abs_def: "(abs :: 'a \ 'b) \ prj oo emb"
  assumes rep_def: "(rep :: 'b \ 'a) \ prj oo emb"
  shows "isodefl d t \ isodefl (abs oo d oo rep) t"
unfolding isodefl_def
by (simp add: cfun_eq_iff assms prj_emb_prj emb_prj_emb)

lemma isodefl'_liftdefl_of: "isodefl d t \ isodefl' d (liftdefl_of\t)"
unfolding isodefl_def isodefl'_def
by (simp add: cast_liftdefl_of u_map_oo liftemb_eq liftprj_eq)

lemma isodefl_sfun:
  "isodefl d1 t1 \ isodefl d2 t2 \
    isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
apply (simp add: cast_sfun_defl cast_isodefl)
apply (simp add: emb_sfun_def prj_sfun_def)
apply (simp add: sfun_map_map isodefl_strict)
done

lemma isodefl_ssum:
  "isodefl d1 t1 \ isodefl d2 t2 \
    isodefl (ssum_map\<cdot>d1\<cdot>d2) (ssum_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
apply (simp add: cast_ssum_defl cast_isodefl)
apply (simp add: emb_ssum_def prj_ssum_def)
apply (simp add: ssum_map_map isodefl_strict)
done

lemma isodefl_sprod:
  "isodefl d1 t1 \ isodefl d2 t2 \
    isodefl (sprod_map\<cdot>d1\<cdot>d2) (sprod_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
apply (simp add: cast_sprod_defl cast_isodefl)
apply (simp add: emb_sprod_def prj_sprod_def)
apply (simp add: sprod_map_map isodefl_strict)
done

lemma isodefl_prod:
  "isodefl d1 t1 \ isodefl d2 t2 \
    isodefl (prod_map\<cdot>d1\<cdot>d2) (prod_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
apply (simp add: cast_prod_defl cast_isodefl)
apply (simp add: emb_prod_def prj_prod_def)
apply (simp add: prod_map_map cfcomp1)
done

lemma isodefl_u:
  "isodefl d t \ isodefl (u_map\d) (u_defl\t)"
apply (rule isodeflI)
apply (simp add: cast_u_defl cast_isodefl)
apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq u_map_map)
done

lemma isodefl_u_liftdefl:
  "isodefl' d t \ isodefl (u_map\d) (u_liftdefl\t)"
apply (rule isodeflI)
apply (simp add: cast_u_liftdefl isodefl'_def)
apply (simp add: emb_u_def prj_u_def liftemb_eq liftprj_eq)
done

lemma encode_prod_u_map:
  "encode_prod_u\(u_map\(prod_map\f\g)\(decode_prod_u\x))
    = sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
unfolding encode_prod_u_def decode_prod_u_def
apply (case_tac x, simp, rename_tac a b)
apply (case_tac a, simp, case_tac b, simp, simp)
done

lemma isodefl_prod_u:
  assumes "isodefl' d1 t1" and "isodefl' d2 t2"
  shows "isodefl' (prod_map\d1\d2) (prod_liftdefl\t1\t2)"
using assms unfolding isodefl'_def
unfolding liftemb_prod_def liftprj_prod_def
by (simp add: cast_prod_liftdefl cfcomp1 encode_prod_u_map sprod_map_map)

lemma encode_cfun_map:
  "encode_cfun\(cfun_map\f\g\(decode_cfun\x))
    = sfun_map\<cdot>(u_map\<cdot>f)\<cdot>g\<cdot>x"
unfolding encode_cfun_def decode_cfun_def
apply (simp add: sfun_eq_iff cfun_map_def sfun_map_def)
apply (rule cfun_eqI, rename_tac y, case_tac y, simp_all)
done

lemma isodefl_cfun:
  assumes "isodefl (u_map\d1) t1" and "isodefl d2 t2"
  shows "isodefl (cfun_map\d1\d2) (sfun_defl\t1\t2)"
using isodefl_sfun [OF assms] unfolding isodefl_def
by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map)

subsection \<open>Setting up the domain package\<close>

named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
  and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"

ML_file \<open>Tools/Domain/domain_isomorphism.ML\<close>
ML_file \<open>Tools/Domain/domain_axioms.ML\<close>
ML_file \<open>Tools/Domain/domain.ML\<close>

lemmas [domain_defl_simps] =
  DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
  liftdefl_eq LIFTDEFL_prod u_liftdefl_liftdefl_of

lemmas [domain_map_ID] =
  cfun_map_ID sfun_map_ID ssum_map_ID sprod_map_ID prod_map_ID u_map_ID

lemmas [domain_isodefl] =
  isodefl_u isodefl_sfun isodefl_ssum isodefl_sprod
  isodefl_cfun isodefl_prod isodefl_prod_u isodefl'_liftdefl_of
  isodefl_u_liftdefl

lemmas [domain_deflation] =
  deflation_cfun_map deflation_sfun_map deflation_ssum_map
  deflation_sprod_map deflation_prod_map deflation_u_map

setup \<open>
  fold Domain_Take_Proofs.add_rec_type
    [(\<^type_name>\<open>cfun\<close>, [true, true]),
     (\<^type_name>\<open>sfun\<close>, [true, true]),
     (\<^type_name>\<open>ssum\<close>, [true, true]),
     (\<^type_name>\<open>sprod\<close>, [true, true]),
     (\<^type_name>\<open>prod\<close>, [true, true]),
     (\<^type_name>\<open>u\<close>, [true])]
\<close>

end

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