(* Title: HOL/HOLCF/Domain_Aux.thy Author: Brian Huffman *) section ‹Domain package support› theory Domain_Aux imports Map_Functions Fixrec begin subsection ‹Continuous isomorphisms› text ‹A locale for continuous isomorphisms› locale iso = fixes abs :: "'a → 'b" 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 \<notsqsubseteq> y)" with cont_Rep_cfun2 have "adm (λy. abs⋅x \<notsqsubseteq> abs⋅y)" by (rule adm_subst) then show "adm (λy. x \<notsqsubseteq> 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 ‹Proofs about take functions› text ‹ 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. › 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 ‹m ≤ n› 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 ‹n ≤ m› 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 ‹chain t› have "chain (λn. t n⋅x)" by simp from ‹adm P› this ‹⋀n. P (t n⋅x)› have "P (⨆n. t n⋅x)" by (rule admD) with ‹chain t› ‹(⨆n. t n) = ID› show "P x" by (simp add: lub_distribs) qed subsection ‹Finiteness› text ‹ 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. › 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 ‹Proofs about constructor functions› text ‹Lemmas for proving nchotomy rule:› 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 ≠ ⊥) = (∃x y. (P (:x, y:) ∧ x ≠ ⊥) ∧ y ≠ ⊥)" by (safe, case_tac y, auto) lemma ex_sprod_up_bottom_iff: "(∃y. P y ∧ y ≠ ⊥) = (∃x y. P (:up⋅x, y:) ∧ y ≠ ⊥)" by (safe, case_tac y, simp, case_tac x, auto) lemma ex_ssum_bottom_iff: "(∃x. P x ∧ x ≠ ⊥) = ((∃x. P (sinl⋅x) ∧ x ≠ ⊥) ∨ (∃x. P (sinr⋅x) ∧ x ≠ ⊥))" 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 ‹Rules for turning nchotomy into exhaust:› 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 ‹Rules for proving constructor properties› 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 ‹ML setup› named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)" and domain_map_ID "theorems like foo_map$ID = ID" ML_file ‹Tools/Domain/domain_take_proofs.ML› ML_file ‹Tools/cont_consts.ML› ML_file ‹Tools/cont_proc.ML› ML_file ‹Tools/Domain/domain_constructors.ML› ML_file ‹Tools/Domain/domain_induction.ML› end