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/PVS/lnexp/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 28.9.2014 mit Größe 537 kB

Quelle Domain.thy Sprache: Isabelle

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

section \<open>Domain package\<close>

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

subsection \<open>Continuous isomorphisms\<close>

text \<open>A locale for continuous isomorphisms\<close>

locale iso =
  fixes abs :: "'a::pcpo \ 'b::pcpo"
  fixes rep :: "'b \ 'a"
  assumes abs_iso [simp]: "rep$abs\x) = x"
  assumes rep_iso [simp]: "abs\(rep\y) = y"
begin

lemma swap: "iso rep abs"
  by (rule iso.intro [OF rep_iso abs_iso])

lemma abs_below: "(abs\x \ abs\y) = (x \ y)"
proof
  assume "abs\x \ abs\y"
  then have "rep\(abs\x) \ rep\(abs\y)" by (rule monofun_cfun_arg)
  then show "x \ y" by simp
next
  assume "x \ y"
  then show "abs\x \ abs\y" by (rule monofun_cfun_arg)
qed

lemma rep_below: "(rep\x \ rep\y) = (x \ y)"
  by (rule iso.abs_below [OF swap])

lemma abs_eq: "(abs\x = abs\y) = (x = y)"
  by (simp add: po_eq_conv abs_below)

lemma rep_eq: "(rep\x = rep\y) = (x = y)"
  by (rule iso.abs_eq [OF swap])

lemma abs_strict: "abs\\ = \"
proof -
  have "\ \ rep\\" ..
  then have "abs\\ \ abs\(rep\$" by (rule monofun_cfun_arg)
  then have "abs\\ \ \" by simp
  then show ?thesis by (rule bottomI)
qed

lemma rep_strict: "rep\\ = \"
  by (rule iso.abs_strict [OF swap])

lemma abs_defin': "abs\x = \ \ x = \"
proof -
  have "x = rep$abs\x)" by simp
  also assume "abs\x = \"
  also note rep_strict
  finally show "x = \" .
qed

lemma rep_defin': "rep\z = \ \ z = \"
  by (rule iso.abs_defin' [OF swap])

lemma abs_defined: "z \ \ \ abs\z \ \"
  by (erule contrapos_nn, erule abs_defin')

lemma rep_defined: "z \ \ \ rep\z \ \"
  by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)

lemma abs_bottom_iff: "(abs\x = $ = (x = \)"
  by (auto elim: abs_defin' intro: abs_strict)

lemma rep_bottom_iff: "(rep\x = \) = (x = \)"
  by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms)

lemma casedist_rule: "rep\x = \ \ P \ x = \ \ P"
  by (simp add: rep_bottom_iff)

lemma compact_abs_rev: "compact (abs\x) \ compact x"
proof (unfold compact_def)
  assume "adm (\y. abs\x \ y)"
  with cont_Rep_cfun2
  have "adm (\y. abs\x \ abs\y)" by (rule adm_subst)
  then show "adm (\y. x \ y)" using abs_below by simp
qed

lemma compact_rep_rev: "compact (rep\x) \ compact x"
  by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)

lemma compact_abs: "compact x \ compact (abs\x)"
  by (rule compact_rep_rev) simp

lemma compact_rep: "compact x \ compact (rep\x)"
  by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)

lemma iso_swap: "(x = abs\y) = (rep\x = y)"
proof
  assume "x = abs\y"
  then have "rep\x = rep\(abs\y)" by simp
  then show "rep\x = y" by simp
next
  assume "rep\x = y"
  then have "abs\(rep\x) = abs\y" by simp
  then show "x = abs\y" by simp
qed

end

subsection \<open>Proofs about take functions\<close>

text \<open>
  This section contains lemmas that are used in a module that supports
  the domain isomorphism package; the module contains proofs related
  to take functions and the finiteness predicate.
\<close>

lemma deflation_abs_rep:
  fixes abs and rep and d
  assumes abs_iso: "\x. rep\(abs\x) = x"
  assumes rep_iso: "\y. abs\(rep\y) = y"
  shows "deflation d \ deflation (abs oo d oo rep)"
by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)

lemma deflation_chain_min:
  assumes chain: "chain d"
  assumes defl: "\n. deflation (d n)"
  shows "d m\(d n\x) = d (min m n)\x"
proof (rule linorder_le_cases)
  assume "m \ n"
  with chain have "d m \ d n" by (rule chain_mono)
  then have "d m\(d n\x) = d m\x"
    by (rule deflation_below_comp1 [OF defl defl])
  moreover from \<open>m \<le> n\<close> have "min m n = m" by simp
  ultimately show ?thesis by simp
next
  assume "n \ m"
  with chain have "d n \ d m" by (rule chain_mono)
  then have "d m\(d n\x) = d n\x"
    by (rule deflation_below_comp2 [OF defl defl])
  moreover from \<open>n \<le> m\<close> have "min m n = n" by simp
  ultimately show ?thesis by simp
qed

lemma lub_ID_take_lemma:
  assumes "chain t" and "(\n. t n) = ID"
  assumes "\n. t n\x = t n\y" shows "x = y"
proof -
  have "(\n. t n\x) = (\n. t n\y)"
    using assms(3) by simp
  then have "(\n. t n)\x = (\n. t n)\y"
    using assms(1) by (simp add: lub_distribs)
  then show "x = y"
    using assms(2) by simp
qed

lemma lub_ID_reach:
  assumes "chain t" and "(\n. t n) = ID"
  shows "(\n. t n\x) = x"
using assms by (simp add: lub_distribs)

lemma lub_ID_take_induct:
  assumes "chain t" and "(\n. t n) = ID"
  assumes "adm P" and "\n. P (t n\x)" shows "P x"
proof -
  from \<open>chain t\<close> have "chain (\<lambda>n. t n\<cdot>x)" by simp
  from \<open>adm P\<close> this \<open>\<And>n. P (t n\<cdot>x)\<close> have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD)
  with \<open>chain t\<close> \<open>(\<Squnion>n. t n) = ID\<close> show "P x" by (simp add: lub_distribs)
qed

subsection \<open>Finiteness\<close>

text \<open>
  Let a ``decisive'' function be a deflation that maps every input to
  either itself or bottom.  Then if a domain's take functions are all
  decisive, then all values in the domain are finite.
\<close>

definition
  decisive :: "('a::pcpo \ 'a) \ bool"
where
  "decisive d \ (\x. d\x = x \ d\x = \)"

lemma decisiveI: "(\x. d\x = x \ d\x = \) \ decisive d"
  unfolding decisive_def by simp

lemma decisive_cases:
  assumes "decisive d" obtains "d\x = x" | "d\x = \"
using assms unfolding decisive_def by auto

lemma decisive_bottom: "decisive \"
  unfolding decisive_def by simp

lemma decisive_ID: "decisive ID"
  unfolding decisive_def by simp

lemma decisive_ssum_map:
  assumes f: "decisive f"
  assumes g: "decisive g"
  shows "decisive (ssum_map\f\g)"
  apply (rule decisiveI)
  subgoal for s
    apply (cases s, simp_all)
     apply (rule_tac x=x in decisive_cases [OF f], simp_all)
    apply (rule_tac x=y in decisive_cases [OF g], simp_all)
    done
  done

lemma decisive_sprod_map:
  assumes f: "decisive f"
  assumes g: "decisive g"
  shows "decisive (sprod_map\f\g)"
  apply (rule decisiveI)
  subgoal for s
    apply (cases s, simp)
    subgoal for x y
      apply (rule decisive_cases [OF f, where x = x], simp_all)
      apply (rule decisive_cases [OF g, where x = y], simp_all)
      done
    done
  done

lemma decisive_abs_rep:
  fixes abs rep
  assumes iso: "iso abs rep"
  assumes d: "decisive d"
  shows "decisive (abs oo d oo rep)"
  apply (rule decisiveI)
  subgoal for s
    apply (rule decisive_cases [OF d, where x="rep\s"])
     apply (simp add: iso.rep_iso [OF iso])
    apply (simp add: iso.abs_strict [OF iso])
    done
  done

lemma lub_ID_finite:
  assumes chain: "chain d"
  assumes lub: "(\n. d n) = ID"
  assumes decisive: "\n. decisive (d n)"
  shows "\n. d n\x = x"
proof -
  have 1: "chain (\n. d n\x)" using chain by simp
  have 2: "(\n. d n\x) = x" using chain lub by (rule lub_ID_reach)
  have "\n. d n\x = x \ d n\x = \"
    using decisive unfolding decisive_def by simp
  hence "range (\n. d n\x) \ {x, \}"
    by auto
  hence "finite (range (\n. d n\x))"
    by (rule finite_subset, simp)
  with 1 have "finite_chain (\n. d n\x)"
    by (rule finite_range_imp_finch)
  then have "\n. (\n. d n\x) = d n\x"
    unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
  with 2 show "\n. d n\x = x" by (auto elim: sym)
qed

lemma lub_ID_finite_take_induct:
  assumes "chain d" and "(\n. d n) = ID" and "\n. decisive (d n)"
  shows "(\n. P (d n\x)) \ P x"
using lub_ID_finite [OF assms] by metis

subsection \<open>Proofs about constructor functions\<close>

text \<open>Lemmas for proving nchotomy rule:\<close>

lemma ex_one_bottom_iff:
  "(\x. P x \ x \ \) = P ONE"
by simp

lemma ex_up_bottom_iff:
  "(\x. P x \ x \ \) = (\x. P (up\x))"
by (safe, case_tac x, auto)

lemma ex_sprod_bottom_iff:
"(\y. P y \ y \ \) =
  (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
by (safe, case_tac y, auto)

lemma ex_sprod_up_bottom_iff:
"(\y. P y \ y \ \) =
  (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
by (safe, case_tac y, simp, case_tac x, auto)

lemma ex_ssum_bottom_iff:
"(\x. P x \ x \ \) =
((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
  (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
by (safe, case_tac x, auto)

lemma exh_start: "p = \ \ (\x. p = x \ x \ \)"
  by auto

lemmas ex_bottom_iffs =
   ex_ssum_bottom_iff
   ex_sprod_up_bottom_iff
   ex_sprod_bottom_iff
   ex_up_bottom_iff
   ex_one_bottom_iff

text \<open>Rules for turning nchotomy into exhaust:\<close>

lemma exh_casedist0: "\R; R \ P\ \ P" (* like make_elim *)
  by auto

lemma exh_casedist1: "((P \ Q \ R) \ S) \ (\P \ R; Q \ R\ \ S)"
  by rule auto

lemma exh_casedist2: "(\x. P x \ Q) \ (\x. P x \ Q)"
  by rule auto

lemma exh_casedist3: "(P \ Q \ R) \ (P \ Q \ R)"
  by rule auto

lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3

text \<open>Rules for proving constructor properties\<close>

lemmas con_strict_rules =
  sinl_strict sinr_strict spair_strict1 spair_strict2

lemmas con_bottom_iff_rules =
  sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined

lemmas con_below_iff_rules =
  sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules

lemmas con_eq_iff_rules =
  sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules

lemmas sel_strict_rules =
  cfcomp2 sscase1 sfst_strict ssnd_strict fup1

lemma sel_app_extra_rules:
  "sscase\ID\\\(sinr\x) = \"
  "sscase\ID\\\(sinl\x) = x"
  "sscase\\\ID\(sinl\x) = \"
  "sscase\\\ID\(sinr\x) = x"
  "fup\ID\(up\x) = x"
by (cases "x = \", simp, simp)+

lemmas sel_app_rules =
  sel_strict_rules sel_app_extra_rules
  ssnd_spair sfst_spair up_defined spair_defined

lemmas sel_bottom_iff_rules =
  cfcomp2 sfst_bottom_iff ssnd_bottom_iff

lemmas take_con_rules =
  ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
  deflation_strict deflation_ID ID1 cfcomp2

subsection \<open>ML setup\<close>

named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
  and domain_map_ID "theorems like foo_map$ID = ID"

ML_file \<open>Tools/Domain/domain_take_proofs.ML\<close>
ML_file \<open>Tools/cont_consts.ML\<close>
ML_file \<open>Tools/cont_proc.ML\<close>
simproc_setup cont ("cont f") = \<open>K ContProc.cont_proc\<close>

ML_file \<open>Tools/Domain/domain_constructors.ML\<close>
ML_file \<open>Tools/Domain/domain_induction.ML\<close>

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

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

lemma emb_prj_emb:
  fixes x :: "'a::domain"
  assumes "DEFL('a) \ DEFL('b)"
  shows "emb\(prj\(emb\x) :: 'b::domain) = 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::domain) \ DEFL('b::domain)"
  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::domain) = DEFL('a::domain)"
  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::domain) = DEFL('a::domain)"
  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::domain \ '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::domain \ '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::domain)"
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::domain) \ 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::domain) = DEFL('a::domain)"
  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

quality96%

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