# HG changeset patch # User nipkow # Date 1733921075 -3600 # Node ID ecd6752956206e577575a57f23f42d049ff35c84 # Parent 8a360893360759efbe462e422c86226d7b29746b# Parent 1c2a68bb0ff16fee5d68114ab2ce8954208baead merged diff -r 1c2a68bb0ff1 -r ecd675295620 Admin/components/main --- a/Admin/components/main Wed Dec 11 13:44:16 2024 +0100 +++ b/Admin/components/main Wed Dec 11 13:44:35 2024 +0100 @@ -4,7 +4,7 @@ bib2xhtml-20190409 csdp-6.1.1 cvc4-1.8 -e-3.0.03-1 +e-3.1 easychair-3.5 eptcs-1.7.0 flatlaf-2.6 diff -r 1c2a68bb0ff1 -r ecd675295620 NEWS --- a/NEWS Wed Dec 11 13:44:16 2024 +0100 +++ b/NEWS Wed Dec 11 13:44:35 2024 +0100 @@ -106,6 +106,7 @@ unbundle no abs_syntax unbundle no floor_ceiling_syntax unbundle no uminus_syntax + unbundle no binomial_syntax unbundle no funcset_syntax This is more robust than individual 'no_syntax' / 'no_notation' diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/Binomial.thy Wed Dec 11 13:44:35 2024 +0100 @@ -18,8 +18,13 @@ text \Combinatorial definition\ -definition binomial :: "nat \ nat \ nat" (infix \choose\ 64) - where "n choose k = card {K\Pow {0.. nat \ nat" + where "binomial n k = card {K\Pow {0..choose\ 64) +end lemma binomial_right_mono: assumes "m \ n" shows "m choose k \ n choose k" diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Adm.thy --- a/src/HOL/HOLCF/Adm.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,179 +0,0 @@ -(* Title: HOL/HOLCF/Adm.thy - Author: Franz Regensburger and Brian Huffman -*) - -section \Admissibility and compactness\ - -theory Adm - imports Cont -begin - -default_sort cpo - -subsection \Definitions\ - -definition adm :: "('a::cpo \ bool) \ bool" - where "adm P \ (\Y. chain Y \ (\i. P (Y i)) \ P (\i. Y i))" - -lemma admI: "(\Y. \chain Y; \i. P (Y i)\ \ P (\i. Y i)) \ adm P" - unfolding adm_def by fast - -lemma admD: "adm P \ chain Y \ (\i. P (Y i)) \ P (\i. Y i)" - unfolding adm_def by fast - -lemma admD2: "adm (\x. \ P x) \ chain Y \ P (\i. Y i) \ \i. P (Y i)" - unfolding adm_def by fast - -lemma triv_admI: "\x. P x \ adm P" - by (rule admI) (erule spec) - - -subsection \Admissibility on chain-finite types\ - -text \For chain-finite (easy) types every formula is admissible.\ - -lemma adm_chfin [simp]: "adm P" - for P :: "'a::chfin \ bool" - by (rule admI, frule chfin, auto simp add: maxinch_is_thelub) - - -subsection \Admissibility of special formulae and propagation\ - -lemma adm_const [simp]: "adm (\x. t)" - by (rule admI, simp) - -lemma adm_conj [simp]: "adm (\x. P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)" - by (fast intro: admI elim: admD) - -lemma adm_all [simp]: "(\y. adm (\x. P x y)) \ adm (\x. \y. P x y)" - by (fast intro: admI elim: admD) - -lemma adm_ball [simp]: "(\y. y \ A \ adm (\x. P x y)) \ adm (\x. \y\A. P x y)" - by (fast intro: admI elim: admD) - -text \Admissibility for disjunction is hard to prove. It requires 2 lemmas.\ - -lemma adm_disj_lemma1: - assumes adm: "adm P" - assumes chain: "chain Y" - assumes P: "\i. \j\i. P (Y j)" - shows "P (\i. Y i)" -proof - - define f where "f i = (LEAST j. i \ j \ P (Y j))" for i - have chain': "chain (\i. Y (f i))" - unfolding f_def - apply (rule chainI) - apply (rule chain_mono [OF chain]) - apply (rule Least_le) - apply (rule LeastI2_ex) - apply (simp_all add: P) - done - have f1: "\i. i \ f i" and f2: "\i. P (Y (f i))" - using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def) - have lub_eq: "(\i. Y i) = (\i. Y (f i))" - apply (rule below_antisym) - apply (rule lub_mono [OF chain chain']) - apply (rule chain_mono [OF chain f1]) - apply (rule lub_range_mono [OF _ chain chain']) - apply clarsimp - done - show "P (\i. Y i)" - unfolding lub_eq using adm chain' f2 by (rule admD) -qed - -lemma adm_disj_lemma2: "\n::nat. P n \ Q n \ (\i. \j\i. P j) \ (\i. \j\i. Q j)" - apply (erule contrapos_pp) - apply (clarsimp, rename_tac a b) - apply (rule_tac x="max a b" in exI) - apply simp - done - -lemma adm_disj [simp]: "adm (\x. P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)" - apply (rule admI) - apply (erule adm_disj_lemma2 [THEN disjE]) - apply (erule (2) adm_disj_lemma1 [THEN disjI1]) - apply (erule (2) adm_disj_lemma1 [THEN disjI2]) - done - -lemma adm_imp [simp]: "adm (\x. \ P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)" - by (subst imp_conv_disj) (rule adm_disj) - -lemma adm_iff [simp]: "adm (\x. P x \ Q x) \ adm (\x. Q x \ P x) \ adm (\x. P x \ Q x)" - by (subst iff_conv_conj_imp) (rule adm_conj) - -text \admissibility and continuity\ - -lemma adm_below [simp]: "cont (\x. u x) \ cont (\x. v x) \ adm (\x. u x \ v x)" - by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont) - -lemma adm_eq [simp]: "cont (\x. u x) \ cont (\x. v x) \ adm (\x. u x = v x)" - by (simp add: po_eq_conv) - -lemma adm_subst: "cont (\x. t x) \ adm P \ adm (\x. P (t x))" - by (simp add: adm_def cont2contlubE ch2ch_cont) - -lemma adm_not_below [simp]: "cont (\x. t x) \ adm (\x. t x \ u)" - by (rule admI) (simp add: cont2contlubE ch2ch_cont lub_below_iff) - - -subsection \Compactness\ - -definition compact :: "'a::cpo \ bool" - where "compact k = adm (\x. k \ x)" - -lemma compactI: "adm (\x. k \ x) \ compact k" - unfolding compact_def . - -lemma compactD: "compact k \ adm (\x. k \ x)" - unfolding compact_def . - -lemma compactI2: "(\Y. \chain Y; x \ (\i. Y i)\ \ \i. x \ Y i) \ compact x" - unfolding compact_def adm_def by fast - -lemma compactD2: "compact x \ chain Y \ x \ (\i. Y i) \ \i. x \ Y i" - unfolding compact_def adm_def by fast - -lemma compact_below_lub_iff: "compact x \ chain Y \ x \ (\i. Y i) \ (\i. x \ Y i)" - by (fast intro: compactD2 elim: below_lub) - -lemma compact_chfin [simp]: "compact x" - for x :: "'a::chfin" - by (rule compactI [OF adm_chfin]) - -lemma compact_imp_max_in_chain: "chain Y \ compact (\i. Y i) \ \i. max_in_chain i Y" - apply (drule (1) compactD2, simp) - apply (erule exE, rule_tac x=i in exI) - apply (rule max_in_chainI) - apply (rule below_antisym) - apply (erule (1) chain_mono) - apply (erule (1) below_trans [OF is_ub_thelub]) - done - -text \admissibility and compactness\ - -lemma adm_compact_not_below [simp]: - "compact k \ cont (\x. t x) \ adm (\x. k \ t x)" - unfolding compact_def by (rule adm_subst) - -lemma adm_neq_compact [simp]: "compact k \ cont (\x. t x) \ adm (\x. t x \ k)" - by (simp add: po_eq_conv) - -lemma adm_compact_neq [simp]: "compact k \ cont (\x. t x) \ adm (\x. k \ t x)" - by (simp add: po_eq_conv) - -lemma compact_bottom [simp, intro]: "compact \" - by (rule compactI) simp - -text \Any upward-closed predicate is admissible.\ - -lemma adm_upward: - assumes P: "\x y. \P x; x \ y\ \ P y" - shows "adm P" - by (rule admI, drule spec, erule P, erule is_ub_thelub) - -lemmas adm_lemmas = - adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff - adm_below adm_eq adm_not_below - adm_compact_not_below adm_compact_neq adm_neq_compact - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Algebraic.thy --- a/src/HOL/HOLCF/Algebraic.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Algebraic.thy Wed Dec 11 13:44:35 2024 +0100 @@ -10,6 +10,7 @@ default_sort bifinite + subsection \Type constructor for finite deflations\ typedef 'a fin_defl = "{d::'a \ 'a. finite_deflation d}" @@ -72,6 +73,7 @@ using finite_deflation_Rep_fin_defl by (rule finite_deflation_imp_compact) + subsection \Defining algebraic deflations by ideal completion\ typedef 'a defl = "{S::'a fin_defl set. below.ideal S}" @@ -147,6 +149,7 @@ lemma inst_defl_pcpo: "\ = defl_principal (Abs_fin_defl \)" by (rule defl_minimal [THEN bottomI, symmetric]) + subsection \Applying algebraic deflations\ definition @@ -215,6 +218,7 @@ lemma cast_strict2 [simp]: "cast\A\\ = \" by (rule cast.below [THEN bottomI]) + subsection \Deflation combinators\ definition diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Bifinite.thy --- a/src/HOL/HOLCF/Bifinite.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Bifinite.thy Wed Dec 11 13:44:35 2024 +0100 @@ -10,6 +10,7 @@ default_sort cpo + subsection \Chains of finite deflations\ locale approx_chain = @@ -43,6 +44,7 @@ end + subsection \Omega-profinite and bifinite domains\ class bifinite = pcpo + @@ -51,6 +53,7 @@ class profinite = cpo + assumes profinite: "\(a::nat \ 'a\<^sub>\ \ 'a\<^sub>\). approx_chain a" + subsection \Building approx chains\ lemma approx_chain_iso: @@ -155,6 +158,7 @@ using chain_discr_approx lub_discr_approx finite_deflation_discr_approx by (rule approx_chain.intro) + subsection \Class instance proofs\ instance bifinite \ profinite diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Cfun.thy Wed Dec 11 13:44:35 2024 +0100 @@ -6,7 +6,7 @@ section \The type of continuous functions\ theory Cfun - imports Cpodef Fun_Cpo Product_Cpo + imports Cpodef begin default_sort cpo diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Compact_Basis.thy --- a/src/HOL/HOLCF/Compact_Basis.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Compact_Basis.thy Wed Dec 11 13:44:35 2024 +0100 @@ -10,6 +10,7 @@ default_sort bifinite + subsection \A compact basis for powerdomains\ definition "pd_basis = {S::'a compact_basis set. finite S \ S \ {}}" @@ -40,6 +41,7 @@ (* FIXME: why doesn't ".." or "by (rule exI)" work? *) qed + subsection \Unit and plus constructors\ definition @@ -91,6 +93,7 @@ apply (rule PDUnit, erule PDPlus [OF PDUnit]) done + subsection \Fold operator\ definition diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Completion.thy --- a/src/HOL/HOLCF/Completion.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Completion.thy Wed Dec 11 13:44:35 2024 +0100 @@ -128,6 +128,7 @@ apply (erule (1) below_trans) done + subsection \Lemmas about least upper bounds\ lemma is_ub_thelub_ex: "\\u. S <<| u; x \ S\ \ x \ lub S" @@ -184,6 +185,7 @@ "\i. Y i \ Y (Suc i) \ chain (\i. principal (Y i))" by (simp add: chainI principal_mono) + subsubsection \Principal ideals approximate all elements\ lemma compact_principal [simp]: "compact (principal a)" @@ -296,6 +298,7 @@ apply (drule (2) admD2, fast, simp) done + subsection \Defining functions in terms of basis elements\ definition diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Cont.thy --- a/src/HOL/HOLCF/Cont.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,223 +0,0 @@ -(* Title: HOL/HOLCF/Cont.thy - Author: Franz Regensburger - Author: Brian Huffman -*) - -section \Continuity and monotonicity\ - -theory Cont - imports Pcpo -begin - -text \ - Now we change the default class! Form now on all untyped type variables are - of default class po -\ - -default_sort po - -subsection \Definitions\ - -definition monofun :: "('a \ 'b) \ bool" \ \monotonicity\ - where "monofun f \ (\x y. x \ y \ f x \ f y)" - -definition cont :: "('a::cpo \ 'b::cpo) \ bool" - where "cont f = (\Y. chain Y \ range (\i. f (Y i)) <<| f (\i. Y i))" - -lemma contI: "(\Y. chain Y \ range (\i. f (Y i)) <<| f (\i. Y i)) \ cont f" - by (simp add: cont_def) - -lemma contE: "cont f \ chain Y \ range (\i. f (Y i)) <<| f (\i. Y i)" - by (simp add: cont_def) - -lemma monofunI: "(\x y. x \ y \ f x \ f y) \ monofun f" - by (simp add: monofun_def) - -lemma monofunE: "monofun f \ x \ y \ f x \ f y" - by (simp add: monofun_def) - - -subsection \Equivalence of alternate definition\ - -text \monotone functions map chains to chains\ - -lemma ch2ch_monofun: "monofun f \ chain Y \ chain (\i. f (Y i))" - apply (rule chainI) - apply (erule monofunE) - apply (erule chainE) - done - -text \monotone functions map upper bound to upper bounds\ - -lemma ub2ub_monofun: "monofun f \ range Y <| u \ range (\i. f (Y i)) <| f u" - apply (rule ub_rangeI) - apply (erule monofunE) - apply (erule ub_rangeD) - done - -text \a lemma about binary chains\ - -lemma binchain_cont: "cont f \ x \ y \ range (\i::nat. f (if i = 0 then x else y)) <<| f y" - apply (subgoal_tac "f (\i::nat. if i = 0 then x else y) = f y") - apply (erule subst) - apply (erule contE) - apply (erule bin_chain) - apply (rule_tac f=f in arg_cong) - apply (erule is_lub_bin_chain [THEN lub_eqI]) - done - -text \continuity implies monotonicity\ - -lemma cont2mono: "cont f \ monofun f" - apply (rule monofunI) - apply (drule (1) binchain_cont) - apply (drule_tac i=0 in is_lub_rangeD1) - apply simp - done - -lemmas cont2monofunE = cont2mono [THEN monofunE] - -lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun] - -text \continuity implies preservation of lubs\ - -lemma cont2contlubE: "cont f \ chain Y \ f (\i. Y i) = (\i. f (Y i))" - apply (rule lub_eqI [symmetric]) - apply (erule (1) contE) - done - -lemma contI2: - fixes f :: "'a::cpo \ 'b::cpo" - assumes mono: "monofun f" - assumes below: "\Y. \chain Y; chain (\i. f (Y i))\ \ f (\i. Y i) \ (\i. f (Y i))" - shows "cont f" -proof (rule contI) - fix Y :: "nat \ 'a" - assume Y: "chain Y" - with mono have fY: "chain (\i. f (Y i))" - by (rule ch2ch_monofun) - have "(\i. f (Y i)) = f (\i. Y i)" - apply (rule below_antisym) - apply (rule lub_below [OF fY]) - apply (rule monofunE [OF mono]) - apply (rule is_ub_thelub [OF Y]) - apply (rule below [OF Y fY]) - done - with fY show "range (\i. f (Y i)) <<| f (\i. Y i)" - by (rule thelubE) -qed - - -subsection \Collection of continuity rules\ - -named_theorems cont2cont "continuity intro rule" - - -subsection \Continuity of basic functions\ - -text \The identity function is continuous\ - -lemma cont_id [simp, cont2cont]: "cont (\x. x)" - apply (rule contI) - apply (erule cpo_lubI) - done - -text \constant functions are continuous\ - -lemma cont_const [simp, cont2cont]: "cont (\x. c)" - using is_lub_const by (rule contI) - -text \application of functions is continuous\ - -lemma cont_apply: - fixes f :: "'a::cpo \ 'b::cpo \ 'c::cpo" and t :: "'a \ 'b" - assumes 1: "cont (\x. t x)" - assumes 2: "\x. cont (\y. f x y)" - assumes 3: "\y. cont (\x. f x y)" - shows "cont (\x. (f x) (t x))" -proof (rule contI2 [OF monofunI]) - fix x y :: "'a" - assume "x \ y" - then show "f x (t x) \ f y (t y)" - by (auto intro: cont2monofunE [OF 1] - cont2monofunE [OF 2] - cont2monofunE [OF 3] - below_trans) -next - fix Y :: "nat \ 'a" - assume "chain Y" - then show "f (\i. Y i) (t (\i. Y i)) \ (\i. f (Y i) (t (Y i)))" - by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1] - cont2contlubE [OF 2] ch2ch_cont [OF 2] - cont2contlubE [OF 3] ch2ch_cont [OF 3] - diag_lub below_refl) -qed - -lemma cont_compose: "cont c \ cont (\x. f x) \ cont (\x. c (f x))" - by (rule cont_apply [OF _ _ cont_const]) - -text \Least upper bounds preserve continuity\ - -lemma cont2cont_lub [simp]: - assumes chain: "\x. chain (\i. F i x)" - and cont: "\i. cont (\x. F i x)" - shows "cont (\x. \i. F i x)" - apply (rule contI2) - apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain) - apply (simp add: cont2contlubE [OF cont]) - apply (simp add: diag_lub ch2ch_cont [OF cont] chain) - done - -text \if-then-else is continuous\ - -lemma cont_if [simp, cont2cont]: "cont f \ cont g \ cont (\x. if b then f x else g x)" - by (induct b) simp_all - - -subsection \Finite chains and flat pcpos\ - -text \Monotone functions map finite chains to finite chains.\ - -lemma monofun_finch2finch: "monofun f \ finite_chain Y \ finite_chain (\n. f (Y n))" - by (force simp add: finite_chain_def ch2ch_monofun max_in_chain_def) - -text \The same holds for continuous functions.\ - -lemma cont_finch2finch: "cont f \ finite_chain Y \ finite_chain (\n. f (Y n))" - by (rule cont2mono [THEN monofun_finch2finch]) - -text \All monotone functions with chain-finite domain are continuous.\ - -lemma chfindom_monofun2cont: "monofun f \ cont f" - for f :: "'a::chfin \ 'b::cpo" - apply (erule contI2) - apply (frule chfin2finch) - apply (clarsimp simp add: finite_chain_def) - apply (subgoal_tac "max_in_chain i (\i. f (Y i))") - apply (simp add: maxinch_is_thelub ch2ch_monofun) - apply (force simp add: max_in_chain_def) - done - -text \All strict functions with flat domain are continuous.\ - -lemma flatdom_strict2mono: "f \ = \ \ monofun f" - for f :: "'a::flat \ 'b::pcpo" - apply (rule monofunI) - apply (drule ax_flat) - apply auto - done - -lemma flatdom_strict2cont: "f \ = \ \ cont f" - for f :: "'a::flat \ 'b::pcpo" - by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) - -text \All functions with discrete domain are continuous.\ - -lemma cont_discrete_cpo [simp, cont2cont]: "cont f" - for f :: "'a::discrete_cpo \ 'b::cpo" - apply (rule contI) - apply (drule discrete_chain_const, clarify) - apply simp - done - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/ConvexPD.thy Wed Dec 11 13:44:35 2024 +0100 @@ -466,6 +466,7 @@ by (rule finite_range_imp_finite_fixes) qed + subsection \Convex powerdomain is bifinite\ lemma approx_chain_convex_map: @@ -481,6 +482,7 @@ by (fast intro!: approx_chain_convex_map) qed + subsection \Join\ definition diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Cpo.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/HOLCF/Cpo.thy Wed Dec 11 13:44:35 2024 +0100 @@ -0,0 +1,1438 @@ +(* Title: HOL/HOLCF/Cpo.thy + Author: Franz Regensburger + Author: Tobias Nipkow + Author: Brian Huffman + +Foundations of HOLCF: complete partial orders etc. +*) + +theory Cpo + imports Main +begin + +section \Partial orders\ + +declare [[typedef_overloaded]] + + +subsection \Type class for partial orders\ + +class below = + fixes below :: "'a \ 'a \ bool" +begin + +notation (ASCII) + below (infix \<<\ 50) + +notation + below (infix \\\ 50) + +abbreviation not_below :: "'a \ 'a \ bool" (infix \\\ 50) + where "not_below x y \ \ below x y" + +notation (ASCII) + not_below (infix \~<<\ 50) + +lemma below_eq_trans: "a \ b \ b = c \ a \ c" + by (rule subst) + +lemma eq_below_trans: "a = b \ b \ c \ a \ c" + by (rule ssubst) + +end + +class po = below + + assumes below_refl [iff]: "x \ x" + assumes below_trans: "x \ y \ y \ z \ x \ z" + assumes below_antisym: "x \ y \ y \ x \ x = y" +begin + +lemma eq_imp_below: "x = y \ x \ y" + by simp + +lemma box_below: "a \ b \ c \ a \ b \ d \ c \ d" + by (rule below_trans [OF below_trans]) + +lemma po_eq_conv: "x = y \ x \ y \ y \ x" + by (fast intro!: below_antisym) + +lemma rev_below_trans: "y \ z \ x \ y \ x \ z" + by (rule below_trans) + +lemma not_below2not_eq: "x \ y \ x \ y" + by auto + +end + +lemmas HOLCF_trans_rules [trans] = + below_trans + below_antisym + below_eq_trans + eq_below_trans + +context po +begin + +subsection \Upper bounds\ + +definition is_ub :: "'a set \ 'a \ bool" (infix \<|\ 55) + where "S <| x \ (\y\S. y \ x)" + +lemma is_ubI: "(\x. x \ S \ x \ u) \ S <| u" + by (simp add: is_ub_def) + +lemma is_ubD: "\S <| u; x \ S\ \ x \ u" + by (simp add: is_ub_def) + +lemma ub_imageI: "(\x. x \ S \ f x \ u) \ (\x. f x) ` S <| u" + unfolding is_ub_def by fast + +lemma ub_imageD: "\f ` S <| u; x \ S\ \ f x \ u" + unfolding is_ub_def by fast + +lemma ub_rangeI: "(\i. S i \ x) \ range S <| x" + unfolding is_ub_def by fast + +lemma ub_rangeD: "range S <| x \ S i \ x" + unfolding is_ub_def by fast + +lemma is_ub_empty [simp]: "{} <| u" + unfolding is_ub_def by fast + +lemma is_ub_insert [simp]: "(insert x A) <| y = (x \ y \ A <| y)" + unfolding is_ub_def by fast + +lemma is_ub_upward: "\S <| x; x \ y\ \ S <| y" + unfolding is_ub_def by (fast intro: below_trans) + + +subsection \Least upper bounds\ + +definition is_lub :: "'a set \ 'a \ bool" (infix \<<|\ 55) + where "S <<| x \ S <| x \ (\u. S <| u \ x \ u)" + +definition lub :: "'a set \ 'a" + where "lub S = (THE x. S <<| x)" + +end + +syntax (ASCII) + "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(\indent=3 notation=\binder LUB\\LUB _:_./ _)\ [0,0, 10] 10) + +syntax + "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0,0, 10] 10) + +syntax_consts + "_BLub" \ lub + +translations + "LUB x:A. t" \ "CONST lub ((\x. t) ` A)" + +context po +begin + +abbreviation Lub (binder \\\ 10) + where "\n. t n \ lub (range t)" + +notation (ASCII) + Lub (binder \LUB \ 10) + +text \access to some definition as inference rule\ + +lemma is_lubD1: "S <<| x \ S <| x" + unfolding is_lub_def by fast + +lemma is_lubD2: "\S <<| x; S <| u\ \ x \ u" + unfolding is_lub_def by fast + +lemma is_lubI: "\S <| x; \u. S <| u \ x \ u\ \ S <<| x" + unfolding is_lub_def by fast + +lemma is_lub_below_iff: "S <<| x \ x \ u \ S <| u" + unfolding is_lub_def is_ub_def by (metis below_trans) + +text \lubs are unique\ + +lemma is_lub_unique: "S <<| x \ S <<| y \ x = y" + unfolding is_lub_def is_ub_def by (blast intro: below_antisym) + +text \technical lemmas about \<^term>\lub\ and \<^term>\is_lub\\ + +lemma is_lub_lub: "M <<| x \ M <<| lub M" + unfolding lub_def by (rule theI [OF _ is_lub_unique]) + +lemma lub_eqI: "M <<| l \ lub M = l" + by (rule is_lub_unique [OF is_lub_lub]) + +lemma is_lub_singleton [simp]: "{x} <<| x" + by (simp add: is_lub_def) + +lemma lub_singleton [simp]: "lub {x} = x" + by (rule is_lub_singleton [THEN lub_eqI]) + +lemma is_lub_bin: "x \ y \ {x, y} <<| y" + by (simp add: is_lub_def) + +lemma lub_bin: "x \ y \ lub {x, y} = y" + by (rule is_lub_bin [THEN lub_eqI]) + +lemma is_lub_maximal: "S <| x \ x \ S \ S <<| x" + by (erule is_lubI, erule (1) is_ubD) + +lemma lub_maximal: "S <| x \ x \ S \ lub S = x" + by (rule is_lub_maximal [THEN lub_eqI]) + + +subsection \Countable chains\ + +definition chain :: "(nat \ 'a) \ bool" + where \ \Here we use countable chains and I prefer to code them as functions!\ + "chain Y = (\i. Y i \ Y (Suc i))" + +lemma chainI: "(\i. Y i \ Y (Suc i)) \ chain Y" + unfolding chain_def by fast + +lemma chainE: "chain Y \ Y i \ Y (Suc i)" + unfolding chain_def by fast + +text \chains are monotone functions\ + +lemma chain_mono_less: "chain Y \ i < j \ Y i \ Y j" + by (erule less_Suc_induct, erule chainE, erule below_trans) + +lemma chain_mono: "chain Y \ i \ j \ Y i \ Y j" + by (cases "i = j") (simp_all add: chain_mono_less) + +lemma chain_shift: "chain Y \ chain (\i. Y (i + j))" + by (rule chainI, simp, erule chainE) + +text \technical lemmas about (least) upper bounds of chains\ + +lemma is_lub_rangeD1: "range S <<| x \ S i \ x" + by (rule is_lubD1 [THEN ub_rangeD]) + +lemma is_ub_range_shift: "chain S \ range (\i. S (i + j)) <| x = range S <| x" + apply (rule iffI) + apply (rule ub_rangeI) + apply (rule_tac y="S (i + j)" in below_trans) + apply (erule chain_mono) + apply (rule le_add1) + apply (erule ub_rangeD) + apply (rule ub_rangeI) + apply (erule ub_rangeD) + done + +lemma is_lub_range_shift: "chain S \ range (\i. S (i + j)) <<| x = range S <<| x" + by (simp add: is_lub_def is_ub_range_shift) + +text \the lub of a constant chain is the constant\ + +lemma chain_const [simp]: "chain (\i. c)" + by (simp add: chainI) + +lemma is_lub_const: "range (\x. c) <<| c" +by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) + +lemma lub_const [simp]: "(\i. c) = c" + by (rule is_lub_const [THEN lub_eqI]) + + +subsection \Finite chains\ + +definition max_in_chain :: "nat \ (nat \ 'a) \ bool" + where \ \finite chains, needed for monotony of continuous functions\ + "max_in_chain i C \ (\j. i \ j \ C i = C j)" + +definition finite_chain :: "(nat \ 'a) \ bool" + where "finite_chain C = (chain C \ (\i. max_in_chain i C))" + +text \results about finite chains\ + +lemma max_in_chainI: "(\j. i \ j \ Y i = Y j) \ max_in_chain i Y" + unfolding max_in_chain_def by fast + +lemma max_in_chainD: "max_in_chain i Y \ i \ j \ Y i = Y j" + unfolding max_in_chain_def by fast + +lemma finite_chainI: "chain C \ max_in_chain i C \ finite_chain C" + unfolding finite_chain_def by fast + +lemma finite_chainE: "\finite_chain C; \i. \chain C; max_in_chain i C\ \ R\ \ R" + unfolding finite_chain_def by fast + +lemma lub_finch1: "chain C \ max_in_chain i C \ range C <<| C i" + apply (rule is_lubI) + apply (rule ub_rangeI, rename_tac j) + apply (rule_tac x=i and y=j in linorder_le_cases) + apply (drule (1) max_in_chainD, simp) + apply (erule (1) chain_mono) + apply (erule ub_rangeD) + done + +lemma lub_finch2: "finite_chain C \ range C <<| C (LEAST i. max_in_chain i C)" + apply (erule finite_chainE) + apply (erule LeastI2 [where Q="\i. range C <<| C i"]) + apply (erule (1) lub_finch1) + done + +lemma finch_imp_finite_range: "finite_chain Y \ finite (range Y)" + apply (erule finite_chainE) + apply (rule_tac B="Y ` {..i}" in finite_subset) + apply (rule subsetI) + apply (erule rangeE, rename_tac j) + apply (rule_tac x=i and y=j in linorder_le_cases) + apply (subgoal_tac "Y j = Y i", simp) + apply (simp add: max_in_chain_def) + apply simp + apply simp + done + +lemma finite_range_has_max: + fixes f :: "nat \ 'a" + and r :: "'a \ 'a \ bool" + assumes mono: "\i j. i \ j \ r (f i) (f j)" + assumes finite_range: "finite (range f)" + shows "\k. \i. r (f i) (f k)" +proof (intro exI allI) + fix i :: nat + let ?j = "LEAST k. f k = f i" + let ?k = "Max ((\x. LEAST k. f k = x) ` range f)" + have "?j \ ?k" + proof (rule Max_ge) + show "finite ((\x. LEAST k. f k = x) ` range f)" + using finite_range by (rule finite_imageI) + show "?j \ (\x. LEAST k. f k = x) ` range f" + by (intro imageI rangeI) + qed + hence "r (f ?j) (f ?k)" + by (rule mono) + also have "f ?j = f i" + by (rule LeastI, rule refl) + finally show "r (f i) (f ?k)" . +qed + +lemma finite_range_imp_finch: "chain Y \ finite (range Y) \ finite_chain Y" + apply (subgoal_tac "\k. \i. Y i \ Y k") + apply (erule exE) + apply (rule finite_chainI, assumption) + apply (rule max_in_chainI) + apply (rule below_antisym) + apply (erule (1) chain_mono) + apply (erule spec) + apply (rule finite_range_has_max) + apply (erule (1) chain_mono) + apply assumption + done + +lemma bin_chain: "x \ y \ chain (\i. if i=0 then x else y)" + by (rule chainI) simp + +lemma bin_chainmax: "x \ y \ max_in_chain (Suc 0) (\i. if i=0 then x else y)" + by (simp add: max_in_chain_def) + +lemma is_lub_bin_chain: "x \ y \ range (\i::nat. if i=0 then x else y) <<| y" + apply (frule bin_chain) + apply (drule bin_chainmax) + apply (drule (1) lub_finch1) + apply simp + done + +text \the maximal element in a chain is its lub\ + +lemma lub_chain_maxelem: "Y i = c \ \i. Y i \ c \ lub (range Y) = c" + by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI) + +end + + +section \Classes cpo and pcpo\ + +subsection \Complete partial orders\ + +text \The class cpo of chain complete partial orders\ + +class cpo = po + + assumes cpo: "chain S \ \x. range S <<| x" +begin + +text \in cpo's everthing equal to THE lub has lub properties for every chain\ + +lemma cpo_lubI: "chain S \ range S <<| (\i. S i)" + by (fast dest: cpo elim: is_lub_lub) + +lemma thelubE: "\chain S; (\i. S i) = l\ \ range S <<| l" + by (blast dest: cpo intro: is_lub_lub) + +text \Properties of the lub\ + +lemma is_ub_thelub: "chain S \ S x \ (\i. S i)" + by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1]) + +lemma is_lub_thelub: "\chain S; range S <| x\ \ (\i. S i) \ x" + by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2]) + +lemma lub_below_iff: "chain S \ (\i. S i) \ x \ (\i. S i \ x)" + by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def) + +lemma lub_below: "\chain S; \i. S i \ x\ \ (\i. S i) \ x" + by (simp add: lub_below_iff) + +lemma below_lub: "\chain S; x \ S i\ \ x \ (\i. S i)" + by (erule below_trans, erule is_ub_thelub) + +lemma lub_range_mono: "\range X \ range Y; chain Y; chain X\ \ (\i. X i) \ (\i. Y i)" + apply (erule lub_below) + apply (subgoal_tac "\j. X i = Y j") + apply clarsimp + apply (erule is_ub_thelub) + apply auto + done + +lemma lub_range_shift: "chain Y \ (\i. Y (i + j)) = (\i. Y i)" + apply (rule below_antisym) + apply (rule lub_range_mono) + apply fast + apply assumption + apply (erule chain_shift) + apply (rule lub_below) + apply assumption + apply (rule_tac i="i" in below_lub) + apply (erule chain_shift) + apply (erule chain_mono) + apply (rule le_add1) + done + +lemma maxinch_is_thelub: "chain Y \ max_in_chain i Y = ((\i. Y i) = Y i)" + apply (rule iffI) + apply (fast intro!: lub_eqI lub_finch1) + apply (unfold max_in_chain_def) + apply (safe intro!: below_antisym) + apply (fast elim!: chain_mono) + apply (drule sym) + apply (force elim!: is_ub_thelub) + done + +text \the \\\ relation between two chains is preserved by their lubs\ + +lemma lub_mono: "\chain X; chain Y; \i. X i \ Y i\ \ (\i. X i) \ (\i. Y i)" + by (fast elim: lub_below below_lub) + +text \the = relation between two chains is preserved by their lubs\ + +lemma lub_eq: "(\i. X i = Y i) \ (\i. X i) = (\i. Y i)" + by simp + +lemma ch2ch_lub: + assumes 1: "\j. chain (\i. Y i j)" + assumes 2: "\i. chain (\j. Y i j)" + shows "chain (\i. \j. Y i j)" + apply (rule chainI) + apply (rule lub_mono [OF 2 2]) + apply (rule chainE [OF 1]) + done + +lemma diag_lub: + assumes 1: "\j. chain (\i. Y i j)" + assumes 2: "\i. chain (\j. Y i j)" + shows "(\i. \j. Y i j) = (\i. Y i i)" +proof (rule below_antisym) + have 3: "chain (\i. Y i i)" + apply (rule chainI) + apply (rule below_trans) + apply (rule chainE [OF 1]) + apply (rule chainE [OF 2]) + done + have 4: "chain (\i. \j. Y i j)" + by (rule ch2ch_lub [OF 1 2]) + show "(\i. \j. Y i j) \ (\i. Y i i)" + apply (rule lub_below [OF 4]) + apply (rule lub_below [OF 2]) + apply (rule below_lub [OF 3]) + apply (rule below_trans) + apply (rule chain_mono [OF 1 max.cobounded1]) + apply (rule chain_mono [OF 2 max.cobounded2]) + done + show "(\i. Y i i) \ (\i. \j. Y i j)" + apply (rule lub_mono [OF 3 4]) + apply (rule is_ub_thelub [OF 2]) + done +qed + +lemma ex_lub: + assumes 1: "\j. chain (\i. Y i j)" + assumes 2: "\i. chain (\j. Y i j)" + shows "(\i. \j. Y i j) = (\j. \i. Y i j)" + by (simp add: diag_lub 1 2) + +end + + +subsection \Pointed cpos\ + +text \The class pcpo of pointed cpos\ + +class pcpo = cpo + + assumes least: "\x. \y. x \ y" +begin + +definition bottom :: "'a" (\\\) + where "bottom = (THE x. \y. x \ y)" + +lemma minimal [iff]: "\ \ x" + unfolding bottom_def + apply (rule the1I2) + apply (rule ex_ex1I) + apply (rule least) + apply (blast intro: below_antisym) + apply simp + done + +end + +text \Old "UU" syntax:\ +abbreviation (input) "UU \ bottom" + +text \Simproc to rewrite \<^term>\\ = x\ to \<^term>\x = \\.\ +setup \Reorient_Proc.add (fn \<^Const_>\bottom _\ => true | _ => false)\ +simproc_setup reorient_bottom ("\ = x") = \K Reorient_Proc.proc\ + +text \useful lemmas about \<^term>\\\\ + +lemma below_bottom_iff [simp]: "x \ \ \ x = \" + by (simp add: po_eq_conv) + +lemma eq_bottom_iff: "x = \ \ x \ \" + by simp + +lemma bottomI: "x \ \ \ x = \" + by (subst eq_bottom_iff) + +lemma lub_eq_bottom_iff: "chain Y \ (\i. Y i) = \ \ (\i. Y i = \)" + by (simp only: eq_bottom_iff lub_below_iff) + + +subsection \Chain-finite and flat cpos\ + +text \further useful classes for HOLCF domains\ + +class chfin = po + + assumes chfin: "chain Y \ \n. max_in_chain n Y" +begin + +subclass cpo + apply standard + apply (frule chfin) + apply (blast intro: lub_finch1) + done + +lemma chfin2finch: "chain Y \ finite_chain Y" + by (simp add: chfin finite_chain_def) + +end + +class flat = pcpo + + assumes ax_flat: "x \ y \ x = \ \ x = y" +begin + +subclass chfin +proof + fix Y + assume *: "chain Y" + show "\n. max_in_chain n Y" + apply (unfold max_in_chain_def) + apply (cases "\i. Y i = \") + apply simp + apply simp + apply (erule exE) + apply (rule_tac x="i" in exI) + apply clarify + using * apply (blast dest: chain_mono ax_flat) + done +qed + +lemma flat_below_iff: "x \ y \ x = \ \ x = y" + by (safe dest!: ax_flat) + +lemma flat_eq: "a \ \ \ a \ b = (a = b)" + by (safe dest!: ax_flat) + +end + + +subsection \Discrete cpos\ + +class discrete_cpo = below + + assumes discrete_cpo [simp]: "x \ y \ x = y" +begin + +subclass po + by standard simp_all + +text \In a discrete cpo, every chain is constant\ + +lemma discrete_chain_const: + assumes S: "chain S" + shows "\x. S = (\i. x)" +proof (intro exI ext) + fix i :: nat + from S le0 have "S 0 \ S i" by (rule chain_mono) + then have "S 0 = S i" by simp + then show "S i = S 0" by (rule sym) +qed + +subclass chfin +proof + fix S :: "nat \ 'a" + assume S: "chain S" + then have "\x. S = (\i. x)" + by (rule discrete_chain_const) + then have "max_in_chain 0 S" + by (auto simp: max_in_chain_def) + then show "\i. max_in_chain i S" .. +qed + +end + + +section \Continuity and monotonicity\ + +subsection \Definitions\ + +definition monofun :: "('a::po \ 'b::po) \ bool" \ \monotonicity\ + where "monofun f \ (\x y. x \ y \ f x \ f y)" + +definition cont :: "('a::cpo \ 'b::cpo) \ bool" + where "cont f = (\Y. chain Y \ range (\i. f (Y i)) <<| f (\i. Y i))" + +lemma contI: "(\Y. chain Y \ range (\i. f (Y i)) <<| f (\i. Y i)) \ cont f" + by (simp add: cont_def) + +lemma contE: "cont f \ chain Y \ range (\i. f (Y i)) <<| f (\i. Y i)" + by (simp add: cont_def) + +lemma monofunI: "(\x y. x \ y \ f x \ f y) \ monofun f" + by (simp add: monofun_def) + +lemma monofunE: "monofun f \ x \ y \ f x \ f y" + by (simp add: monofun_def) + + +subsection \Equivalence of alternate definition\ + +text \monotone functions map chains to chains\ + +lemma ch2ch_monofun: "monofun f \ chain Y \ chain (\i. f (Y i))" + apply (rule chainI) + apply (erule monofunE) + apply (erule chainE) + done + +text \monotone functions map upper bound to upper bounds\ + +lemma ub2ub_monofun: "monofun f \ range Y <| u \ range (\i. f (Y i)) <| f u" + apply (rule ub_rangeI) + apply (erule monofunE) + apply (erule ub_rangeD) + done + +text \a lemma about binary chains\ + +lemma binchain_cont: "cont f \ x \ y \ range (\i::nat. f (if i = 0 then x else y)) <<| f y" + apply (subgoal_tac "f (\i::nat. if i = 0 then x else y) = f y") + apply (erule subst) + apply (erule contE) + apply (erule bin_chain) + apply (rule_tac f=f in arg_cong) + apply (erule is_lub_bin_chain [THEN lub_eqI]) + done + +text \continuity implies monotonicity\ + +lemma cont2mono: "cont f \ monofun f" + apply (rule monofunI) + apply (drule (1) binchain_cont) + apply (drule_tac i=0 in is_lub_rangeD1) + apply simp + done + +lemmas cont2monofunE = cont2mono [THEN monofunE] + +lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun] + +text \continuity implies preservation of lubs\ + +lemma cont2contlubE: "cont f \ chain Y \ f (\i. Y i) = (\i. f (Y i))" + apply (rule lub_eqI [symmetric]) + apply (erule (1) contE) + done + +lemma contI2: + fixes f :: "'a::cpo \ 'b::cpo" + assumes mono: "monofun f" + assumes below: "\Y. \chain Y; chain (\i. f (Y i))\ \ f (\i. Y i) \ (\i. f (Y i))" + shows "cont f" +proof (rule contI) + fix Y :: "nat \ 'a" + assume Y: "chain Y" + with mono have fY: "chain (\i. f (Y i))" + by (rule ch2ch_monofun) + have "(\i. f (Y i)) = f (\i. Y i)" + apply (rule below_antisym) + apply (rule lub_below [OF fY]) + apply (rule monofunE [OF mono]) + apply (rule is_ub_thelub [OF Y]) + apply (rule below [OF Y fY]) + done + with fY show "range (\i. f (Y i)) <<| f (\i. Y i)" + by (rule thelubE) +qed + + +subsection \Collection of continuity rules\ + +named_theorems cont2cont "continuity intro rule" + + +subsection \Continuity of basic functions\ + +text \The identity function is continuous\ + +lemma cont_id [simp, cont2cont]: "cont (\x. x)" + apply (rule contI) + apply (erule cpo_lubI) + done + +text \constant functions are continuous\ + +lemma cont_const [simp, cont2cont]: "cont (\x. c)" + using is_lub_const by (rule contI) + +text \application of functions is continuous\ + +lemma cont_apply: + fixes f :: "'a::cpo \ 'b::cpo \ 'c::cpo" and t :: "'a \ 'b" + assumes 1: "cont (\x. t x)" + assumes 2: "\x. cont (\y. f x y)" + assumes 3: "\y. cont (\x. f x y)" + shows "cont (\x. (f x) (t x))" +proof (rule contI2 [OF monofunI]) + fix x y :: "'a" + assume "x \ y" + then show "f x (t x) \ f y (t y)" + by (auto intro: cont2monofunE [OF 1] + cont2monofunE [OF 2] + cont2monofunE [OF 3] + below_trans) +next + fix Y :: "nat \ 'a" + assume "chain Y" + then show "f (\i. Y i) (t (\i. Y i)) \ (\i. f (Y i) (t (Y i)))" + by (simp only: cont2contlubE [OF 1] ch2ch_cont [OF 1] + cont2contlubE [OF 2] ch2ch_cont [OF 2] + cont2contlubE [OF 3] ch2ch_cont [OF 3] + diag_lub below_refl) +qed + +lemma cont_compose: "cont c \ cont (\x. f x) \ cont (\x. c (f x))" + by (rule cont_apply [OF _ _ cont_const]) + +text \Least upper bounds preserve continuity\ + +lemma cont2cont_lub [simp]: + assumes chain: "\x. chain (\i. F i x)" + and cont: "\i. cont (\x. F i x)" + shows "cont (\x. \i. F i x)" + apply (rule contI2) + apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain) + apply (simp add: cont2contlubE [OF cont]) + apply (simp add: diag_lub ch2ch_cont [OF cont] chain) + done + +text \if-then-else is continuous\ + +lemma cont_if [simp, cont2cont]: "cont f \ cont g \ cont (\x. if b then f x else g x)" + by (induct b) simp_all + + +subsection \Finite chains and flat pcpos\ + +text \Monotone functions map finite chains to finite chains.\ + +lemma monofun_finch2finch: "monofun f \ finite_chain Y \ finite_chain (\n. f (Y n))" + by (force simp add: finite_chain_def ch2ch_monofun max_in_chain_def) + +text \The same holds for continuous functions.\ + +lemma cont_finch2finch: "cont f \ finite_chain Y \ finite_chain (\n. f (Y n))" + by (rule cont2mono [THEN monofun_finch2finch]) + +text \All monotone functions with chain-finite domain are continuous.\ + +lemma chfindom_monofun2cont: "monofun f \ cont f" + for f :: "'a::chfin \ 'b::cpo" + apply (erule contI2) + apply (frule chfin2finch) + apply (clarsimp simp add: finite_chain_def) + apply (subgoal_tac "max_in_chain i (\i. f (Y i))") + apply (simp add: maxinch_is_thelub ch2ch_monofun) + apply (force simp add: max_in_chain_def) + done + +text \All strict functions with flat domain are continuous.\ + +lemma flatdom_strict2mono: "f \ = \ \ monofun f" + for f :: "'a::flat \ 'b::pcpo" + apply (rule monofunI) + apply (drule ax_flat) + apply auto + done + +lemma flatdom_strict2cont: "f \ = \ \ cont f" + for f :: "'a::flat \ 'b::pcpo" + by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) + +text \All functions with discrete domain are continuous.\ + +lemma cont_discrete_cpo [simp, cont2cont]: "cont f" + for f :: "'a::discrete_cpo \ 'b::cpo" + apply (rule contI) + apply (drule discrete_chain_const, clarify) + apply simp + done + + +section \Admissibility and compactness\ + +default_sort cpo + + +subsection \Definitions\ + +definition adm :: "('a::cpo \ bool) \ bool" + where "adm P \ (\Y. chain Y \ (\i. P (Y i)) \ P (\i. Y i))" + +lemma admI: "(\Y. \chain Y; \i. P (Y i)\ \ P (\i. Y i)) \ adm P" + unfolding adm_def by fast + +lemma admD: "adm P \ chain Y \ (\i. P (Y i)) \ P (\i. Y i)" + unfolding adm_def by fast + +lemma admD2: "adm (\x. \ P x) \ chain Y \ P (\i. Y i) \ \i. P (Y i)" + unfolding adm_def by fast + +lemma triv_admI: "\x. P x \ adm P" + by (rule admI) (erule spec) + + +subsection \Admissibility on chain-finite types\ + +text \For chain-finite (easy) types every formula is admissible.\ + +lemma adm_chfin [simp]: "adm P" + for P :: "'a::chfin \ bool" + by (rule admI, frule chfin, auto simp add: maxinch_is_thelub) + + +subsection \Admissibility of special formulae and propagation\ + +lemma adm_const [simp]: "adm (\x. t)" + by (rule admI, simp) + +lemma adm_conj [simp]: "adm (\x. P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)" + by (fast intro: admI elim: admD) + +lemma adm_all [simp]: "(\y. adm (\x. P x y)) \ adm (\x. \y. P x y)" + by (fast intro: admI elim: admD) + +lemma adm_ball [simp]: "(\y. y \ A \ adm (\x. P x y)) \ adm (\x. \y\A. P x y)" + by (fast intro: admI elim: admD) + +text \Admissibility for disjunction is hard to prove. It requires 2 lemmas.\ + +lemma adm_disj_lemma1: + assumes adm: "adm P" + assumes chain: "chain Y" + assumes P: "\i. \j\i. P (Y j)" + shows "P (\i. Y i)" +proof - + define f where "f i = (LEAST j. i \ j \ P (Y j))" for i + have chain': "chain (\i. Y (f i))" + unfolding f_def + apply (rule chainI) + apply (rule chain_mono [OF chain]) + apply (rule Least_le) + apply (rule LeastI2_ex) + apply (simp_all add: P) + done + have f1: "\i. i \ f i" and f2: "\i. P (Y (f i))" + using LeastI_ex [OF P [rule_format]] by (simp_all add: f_def) + have lub_eq: "(\i. Y i) = (\i. Y (f i))" + apply (rule below_antisym) + apply (rule lub_mono [OF chain chain']) + apply (rule chain_mono [OF chain f1]) + apply (rule lub_range_mono [OF _ chain chain']) + apply clarsimp + done + show "P (\i. Y i)" + unfolding lub_eq using adm chain' f2 by (rule admD) +qed + +lemma adm_disj_lemma2: "\n::nat. P n \ Q n \ (\i. \j\i. P j) \ (\i. \j\i. Q j)" + apply (erule contrapos_pp) + apply (clarsimp, rename_tac a b) + apply (rule_tac x="max a b" in exI) + apply simp + done + +lemma adm_disj [simp]: "adm (\x. P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)" + apply (rule admI) + apply (erule adm_disj_lemma2 [THEN disjE]) + apply (erule (2) adm_disj_lemma1 [THEN disjI1]) + apply (erule (2) adm_disj_lemma1 [THEN disjI2]) + done + +lemma adm_imp [simp]: "adm (\x. \ P x) \ adm (\x. Q x) \ adm (\x. P x \ Q x)" + by (subst imp_conv_disj) (rule adm_disj) + +lemma adm_iff [simp]: "adm (\x. P x \ Q x) \ adm (\x. Q x \ P x) \ adm (\x. P x \ Q x)" + by (subst iff_conv_conj_imp) (rule adm_conj) + +text \admissibility and continuity\ + +lemma adm_below [simp]: "cont (\x. u x) \ cont (\x. v x) \ adm (\x. u x \ v x)" + by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont) + +lemma adm_eq [simp]: "cont (\x. u x) \ cont (\x. v x) \ adm (\x. u x = v x)" + by (simp add: po_eq_conv) + +lemma adm_subst: "cont (\x. t x) \ adm P \ adm (\x. P (t x))" + by (simp add: adm_def cont2contlubE ch2ch_cont) + +lemma adm_not_below [simp]: "cont (\x. t x) \ adm (\x. t x \ u)" + by (rule admI) (simp add: cont2contlubE ch2ch_cont lub_below_iff) + + +subsection \Compactness\ + +definition compact :: "'a::cpo \ bool" + where "compact k = adm (\x. k \ x)" + +lemma compactI: "adm (\x. k \ x) \ compact k" + unfolding compact_def . + +lemma compactD: "compact k \ adm (\x. k \ x)" + unfolding compact_def . + +lemma compactI2: "(\Y. \chain Y; x \ (\i. Y i)\ \ \i. x \ Y i) \ compact x" + unfolding compact_def adm_def by fast + +lemma compactD2: "compact x \ chain Y \ x \ (\i. Y i) \ \i. x \ Y i" + unfolding compact_def adm_def by fast + +lemma compact_below_lub_iff: "compact x \ chain Y \ x \ (\i. Y i) \ (\i. x \ Y i)" + by (fast intro: compactD2 elim: below_lub) + +lemma compact_chfin [simp]: "compact x" + for x :: "'a::chfin" + by (rule compactI [OF adm_chfin]) + +lemma compact_imp_max_in_chain: "chain Y \ compact (\i. Y i) \ \i. max_in_chain i Y" + apply (drule (1) compactD2, simp) + apply (erule exE, rule_tac x=i in exI) + apply (rule max_in_chainI) + apply (rule below_antisym) + apply (erule (1) chain_mono) + apply (erule (1) below_trans [OF is_ub_thelub]) + done + +text \admissibility and compactness\ + +lemma adm_compact_not_below [simp]: + "compact k \ cont (\x. t x) \ adm (\x. k \ t x)" + unfolding compact_def by (rule adm_subst) + +lemma adm_neq_compact [simp]: "compact k \ cont (\x. t x) \ adm (\x. t x \ k)" + by (simp add: po_eq_conv) + +lemma adm_compact_neq [simp]: "compact k \ cont (\x. t x) \ adm (\x. k \ t x)" + by (simp add: po_eq_conv) + +lemma compact_bottom [simp, intro]: "compact \" + by (rule compactI) simp + +text \Any upward-closed predicate is admissible.\ + +lemma adm_upward: + assumes P: "\x y. \P x; x \ y\ \ P y" + shows "adm P" + by (rule admI, drule spec, erule P, erule is_ub_thelub) + +lemmas adm_lemmas = + adm_const adm_conj adm_all adm_ball adm_disj adm_imp adm_iff + adm_below adm_eq adm_not_below + adm_compact_not_below adm_compact_neq adm_neq_compact + + +section \Class instances for the full function space\ + +subsection \Full function space is a partial order\ + +instantiation "fun" :: (type, below) below +begin + +definition below_fun_def: "(\) \ (\f g. \x. f x \ g x)" + +instance .. +end + +instance "fun" :: (type, po) po +proof + fix f :: "'a \ 'b" + show "f \ f" + by (simp add: below_fun_def) +next + fix f g :: "'a \ 'b" + assume "f \ g" and "g \ f" then show "f = g" + by (simp add: below_fun_def fun_eq_iff below_antisym) +next + fix f g h :: "'a \ 'b" + assume "f \ g" and "g \ h" then show "f \ h" + unfolding below_fun_def by (fast elim: below_trans) +qed + +lemma fun_below_iff: "f \ g \ (\x. f x \ g x)" + by (simp add: below_fun_def) + +lemma fun_belowI: "(\x. f x \ g x) \ f \ g" + by (simp add: below_fun_def) + +lemma fun_belowD: "f \ g \ f x \ g x" + by (simp add: below_fun_def) + + +subsection \Full function space is chain complete\ + +text \Properties of chains of functions.\ + +lemma fun_chain_iff: "chain S \ (\x. chain (\i. S i x))" + by (auto simp: chain_def fun_below_iff) + +lemma ch2ch_fun: "chain S \ chain (\i. S i x)" + by (simp add: chain_def below_fun_def) + +lemma ch2ch_lambda: "(\x. chain (\i. S i x)) \ chain S" + by (simp add: chain_def below_fun_def) + +text \Type \<^typ>\'a::type \ 'b::cpo\ is chain complete\ + +lemma is_lub_lambda: "(\x. range (\i. Y i x) <<| f x) \ range Y <<| f" + by (simp add: is_lub_def is_ub_def below_fun_def) + +lemma is_lub_fun: "chain S \ range S <<| (\x. \i. S i x)" + for S :: "nat \ 'a::type \ 'b::cpo" + apply (rule is_lub_lambda) + apply (rule cpo_lubI) + apply (erule ch2ch_fun) + done + +lemma lub_fun: "chain S \ (\i. S i) = (\x. \i. S i x)" + for S :: "nat \ 'a::type \ 'b::cpo" + by (rule is_lub_fun [THEN lub_eqI]) + +instance "fun" :: (type, cpo) cpo + by intro_classes (rule exI, erule is_lub_fun) + +instance "fun" :: (type, discrete_cpo) discrete_cpo +proof + fix f g :: "'a \ 'b" + show "f \ g \ f = g" + by (simp add: fun_below_iff fun_eq_iff) +qed + + +subsection \Full function space is pointed\ + +lemma minimal_fun: "(\x. \) \ f" + by (simp add: below_fun_def) + +instance "fun" :: (type, pcpo) pcpo + by standard (fast intro: minimal_fun) + +lemma inst_fun_pcpo: "\ = (\x. \)" + by (rule minimal_fun [THEN bottomI, symmetric]) + +lemma app_strict [simp]: "\ x = \" + by (simp add: inst_fun_pcpo) + +lemma lambda_strict: "(\x. \) = \" + by (rule bottomI, rule minimal_fun) + + +subsection \Propagation of monotonicity and continuity\ + +text \The lub of a chain of monotone functions is monotone.\ + +lemma adm_monofun: "adm monofun" + by (rule admI) (simp add: lub_fun fun_chain_iff monofun_def lub_mono) + +text \The lub of a chain of continuous functions is continuous.\ + +lemma adm_cont: "adm cont" + by (rule admI) (simp add: lub_fun fun_chain_iff) + +text \Function application preserves monotonicity and continuity.\ + +lemma mono2mono_fun: "monofun f \ monofun (\x. f x y)" + by (simp add: monofun_def fun_below_iff) + +lemma cont2cont_fun: "cont f \ cont (\x. f x y)" + apply (rule contI2) + apply (erule cont2mono [THEN mono2mono_fun]) + apply (simp add: cont2contlubE lub_fun ch2ch_cont) + done + +lemma cont_fun: "cont (\f. f x)" + using cont_id by (rule cont2cont_fun) + +text \ + Lambda abstraction preserves monotonicity and continuity. + (Note \(\x. \y. f x y) = f\.) +\ + +lemma mono2mono_lambda: "(\y. monofun (\x. f x y)) \ monofun f" + by (simp add: monofun_def fun_below_iff) + +lemma cont2cont_lambda [simp]: + assumes f: "\y. cont (\x. f x y)" + shows "cont f" + by (rule contI, rule is_lub_lambda, rule contE [OF f]) + +text \What D.A.Schmidt calls continuity of abstraction; never used here\ + +lemma contlub_lambda: "(\x. chain (\i. S i x)) \ (\x. \i. S i x) = (\i. (\x. S i x))" + for S :: "nat \ 'a::type \ 'b::cpo" + by (simp add: lub_fun ch2ch_lambda) + + +section \The cpo of cartesian products\ + +subsection \Unit type is a pcpo\ + +instantiation unit :: discrete_cpo +begin + +definition below_unit_def [simp]: "x \ (y::unit) \ True" + +instance + by standard simp + +end + +instance unit :: pcpo + by standard simp + + +subsection \Product type is a partial order\ + +instantiation prod :: (below, below) below +begin + +definition below_prod_def: "(\) \ \p1 p2. (fst p1 \ fst p2 \ snd p1 \ snd p2)" + +instance .. + +end + +instance prod :: (po, po) po +proof + fix x :: "'a \ 'b" + show "x \ x" + by (simp add: below_prod_def) +next + fix x y :: "'a \ 'b" + assume "x \ y" "y \ x" + then show "x = y" + unfolding below_prod_def prod_eq_iff + by (fast intro: below_antisym) +next + fix x y z :: "'a \ 'b" + assume "x \ y" "y \ z" + then show "x \ z" + unfolding below_prod_def + by (fast intro: below_trans) +qed + + +subsection \Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\ + +lemma prod_belowI: "fst p \ fst q \ snd p \ snd q \ p \ q" + by (simp add: below_prod_def) + +lemma Pair_below_iff [simp]: "(a, b) \ (c, d) \ a \ c \ b \ d" + by (simp add: below_prod_def) + +text \Pair \(_,_)\ is monotone in both arguments\ + +lemma monofun_pair1: "monofun (\x. (x, y))" + by (simp add: monofun_def) + +lemma monofun_pair2: "monofun (\y. (x, y))" + by (simp add: monofun_def) + +lemma monofun_pair: "x1 \ x2 \ y1 \ y2 \ (x1, y1) \ (x2, y2)" + by simp + +lemma ch2ch_Pair [simp]: "chain X \ chain Y \ chain (\i. (X i, Y i))" + by (rule chainI, simp add: chainE) + +text \\<^term>\fst\ and \<^term>\snd\ are monotone\ + +lemma fst_monofun: "x \ y \ fst x \ fst y" + by (simp add: below_prod_def) + +lemma snd_monofun: "x \ y \ snd x \ snd y" + by (simp add: below_prod_def) + +lemma monofun_fst: "monofun fst" + by (simp add: monofun_def below_prod_def) + +lemma monofun_snd: "monofun snd" + by (simp add: monofun_def below_prod_def) + +lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst] + +lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd] + +lemma prod_chain_cases: + assumes chain: "chain Y" + obtains A B + where "chain A" and "chain B" and "Y = (\i. (A i, B i))" +proof + from chain show "chain (\i. fst (Y i))" + by (rule ch2ch_fst) + from chain show "chain (\i. snd (Y i))" + by (rule ch2ch_snd) + show "Y = (\i. (fst (Y i), snd (Y i)))" + by simp +qed + + +subsection \Product type is a cpo\ + +lemma is_lub_Pair: "range A <<| x \ range B <<| y \ range (\i. (A i, B i)) <<| (x, y)" + by (simp add: is_lub_def is_ub_def below_prod_def) + +lemma lub_Pair: "chain A \ chain B \ (\i. (A i, B i)) = (\i. A i, \i. B i)" + for A :: "nat \ 'a::cpo" and B :: "nat \ 'b::cpo" + by (fast intro: lub_eqI is_lub_Pair elim: thelubE) + +lemma is_lub_prod: + fixes S :: "nat \ ('a::cpo \ 'b::cpo)" + assumes "chain S" + shows "range S <<| (\i. fst (S i), \i. snd (S i))" + using assms by (auto elim: prod_chain_cases simp: is_lub_Pair cpo_lubI) + +lemma lub_prod: "chain S \ (\i. S i) = (\i. fst (S i), \i. snd (S i))" + for S :: "nat \ 'a::cpo \ 'b::cpo" + by (rule is_lub_prod [THEN lub_eqI]) + +instance prod :: (cpo, cpo) cpo +proof + fix S :: "nat \ ('a \ 'b)" + assume "chain S" + then have "range S <<| (\i. fst (S i), \i. snd (S i))" + by (rule is_lub_prod) + then show "\x. range S <<| x" .. +qed + +instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo +proof + fix x y :: "'a \ 'b" + show "x \ y \ x = y" + by (simp add: below_prod_def prod_eq_iff) +qed + + +subsection \Product type is pointed\ + +lemma minimal_prod: "(\, \) \ p" + by (simp add: below_prod_def) + +instance prod :: (pcpo, pcpo) pcpo + by intro_classes (fast intro: minimal_prod) + +lemma inst_prod_pcpo: "\ = (\, \)" + by (rule minimal_prod [THEN bottomI, symmetric]) + +lemma Pair_bottom_iff [simp]: "(x, y) = \ \ x = \ \ y = \" + by (simp add: inst_prod_pcpo) + +lemma fst_strict [simp]: "fst \ = \" + unfolding inst_prod_pcpo by (rule fst_conv) + +lemma snd_strict [simp]: "snd \ = \" + unfolding inst_prod_pcpo by (rule snd_conv) + +lemma Pair_strict [simp]: "(\, \) = \" + by simp + +lemma split_strict [simp]: "case_prod f \ = f \ \" + by (simp add: split_def) + + +subsection \Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\ + +lemma cont_pair1: "cont (\x. (x, y))" + apply (rule contI) + apply (rule is_lub_Pair) + apply (erule cpo_lubI) + apply (rule is_lub_const) + done + +lemma cont_pair2: "cont (\y. (x, y))" + apply (rule contI) + apply (rule is_lub_Pair) + apply (rule is_lub_const) + apply (erule cpo_lubI) + done + +lemma cont_fst: "cont fst" + apply (rule contI) + apply (simp add: lub_prod) + apply (erule cpo_lubI [OF ch2ch_fst]) + done + +lemma cont_snd: "cont snd" + apply (rule contI) + apply (simp add: lub_prod) + apply (erule cpo_lubI [OF ch2ch_snd]) + done + +lemma cont2cont_Pair [simp, cont2cont]: + assumes f: "cont (\x. f x)" + assumes g: "cont (\x. g x)" + shows "cont (\x. (f x, g x))" + apply (rule cont_apply [OF f cont_pair1]) + apply (rule cont_apply [OF g cont_pair2]) + apply (rule cont_const) + done + +lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst] + +lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd] + +lemma cont2cont_case_prod: + assumes f1: "\a b. cont (\x. f x a b)" + assumes f2: "\x b. cont (\a. f x a b)" + assumes f3: "\x a. cont (\b. f x a b)" + assumes g: "cont (\x. g x)" + shows "cont (\x. case g x of (a, b) \ f x a b)" + unfolding split_def + apply (rule cont_apply [OF g]) + apply (rule cont_apply [OF cont_fst f2]) + apply (rule cont_apply [OF cont_snd f3]) + apply (rule cont_const) + apply (rule f1) + done + +lemma prod_contI: + assumes f1: "\y. cont (\x. f (x, y))" + assumes f2: "\x. cont (\y. f (x, y))" + shows "cont f" +proof - + have "cont (\(x, y). f (x, y))" + by (intro cont2cont_case_prod f1 f2 cont2cont) + then show "cont f" + by (simp only: case_prod_eta) +qed + +lemma prod_cont_iff: "cont f \ (\y. cont (\x. f (x, y))) \ (\x. cont (\y. f (x, y)))" + apply safe + apply (erule cont_compose [OF _ cont_pair1]) + apply (erule cont_compose [OF _ cont_pair2]) + apply (simp only: prod_contI) + done + +lemma cont2cont_case_prod' [simp, cont2cont]: + assumes f: "cont (\p. f (fst p) (fst (snd p)) (snd (snd p)))" + assumes g: "cont (\x. g x)" + shows "cont (\x. case_prod (f x) (g x))" + using assms by (simp add: cont2cont_case_prod prod_cont_iff) + +text \The simple version (due to Joachim Breitner) is needed if + either element type of the pair is not a cpo.\ + +lemma cont2cont_split_simple [simp, cont2cont]: + assumes "\a b. cont (\x. f x a b)" + shows "cont (\x. case p of (a, b) \ f x a b)" + using assms by (cases p) auto + +text \Admissibility of predicates on product types.\ + +lemma adm_case_prod [simp]: + assumes "adm (\x. P x (fst (f x)) (snd (f x)))" + shows "adm (\x. case f x of (a, b) \ P x a b)" + unfolding case_prod_beta using assms . + + +subsection \Compactness and chain-finiteness\ + +lemma fst_below_iff: "fst x \ y \ x \ (y, snd x)" + for x :: "'a \ 'b" + by (simp add: below_prod_def) + +lemma snd_below_iff: "snd x \ y \ x \ (fst x, y)" + for x :: "'a \ 'b" + by (simp add: below_prod_def) + +lemma compact_fst: "compact x \ compact (fst x)" + by (rule compactI) (simp add: fst_below_iff) + +lemma compact_snd: "compact x \ compact (snd x)" + by (rule compactI) (simp add: snd_below_iff) + +lemma compact_Pair: "compact x \ compact y \ compact (x, y)" + by (rule compactI) (simp add: below_prod_def) + +lemma compact_Pair_iff [simp]: "compact (x, y) \ compact x \ compact y" + apply (safe intro!: compact_Pair) + apply (drule compact_fst, simp) + apply (drule compact_snd, simp) + done + +instance prod :: (chfin, chfin) chfin + apply intro_classes + apply (erule compact_imp_max_in_chain) + apply (case_tac "\i. Y i", simp) + done + + +section \Discrete cpo types\ + +datatype 'a discr = Discr "'a :: type" + +subsection \Discrete cpo class instance\ + +instantiation discr :: (type) discrete_cpo +begin + +definition "((\) :: 'a discr \ 'a discr \ bool) = (=)" + +instance + by standard (simp add: below_discr_def) + +end + + +subsection \\emph{undiscr}\ + +definition undiscr :: "('a::type)discr \ 'a" + where "undiscr x = (case x of Discr y \ y)" + +lemma undiscr_Discr [simp]: "undiscr (Discr x) = x" + by (simp add: undiscr_def) + +lemma Discr_undiscr [simp]: "Discr (undiscr y) = y" + by (induct y) simp + +end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Cpodef.thy --- a/src/HOL/HOLCF/Cpodef.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Cpodef.thy Wed Dec 11 13:44:35 2024 +0100 @@ -5,7 +5,7 @@ section \Subtypes of pcpos\ theory Cpodef - imports Adm + imports Cpo keywords "pcpodef" "cpodef" :: thy_goal_defn begin @@ -16,7 +16,7 @@ if the ordering is defined in the standard way. \ -setup \Sign.add_const_constraint (\<^const_name>\Porder.below\, NONE)\ +setup \Sign.add_const_constraint (\<^const_name>\below\, NONE)\ theorem typedef_po: fixes Abs :: "'a::po \ 'b::type" @@ -30,7 +30,7 @@ apply (erule (1) below_antisym) done -setup \Sign.add_const_constraint (\<^const_name>\Porder.below\, SOME \<^typ>\'a::below \ 'a::below \ bool\)\ +setup \Sign.add_const_constraint (\<^const_name>\below\, SOME \<^typ>\'a::below \ 'a::below \ bool\)\ subsection \Proving a subtype is finite\ diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Deflation.thy --- a/src/HOL/HOLCF/Deflation.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Deflation.thy Wed Dec 11 13:44:35 2024 +0100 @@ -313,6 +313,7 @@ end + subsection \Uniqueness of ep-pairs\ lemma ep_pair_unique_e_lemma: diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Discrete_Cpo.thy --- a/src/HOL/HOLCF/Discrete_Cpo.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,37 +0,0 @@ -(* Title: HOL/HOLCF/Discrete_Cpo.thy - Author: Tobias Nipkow -*) - -section \Discrete cpo types\ - -theory Discrete_Cpo - imports Cont -begin - -datatype 'a discr = Discr "'a :: type" - -subsection \Discrete cpo class instance\ - -instantiation discr :: (type) discrete_cpo -begin - -definition "((\) :: 'a discr \ 'a discr \ bool) = (=)" - -instance - by standard (simp add: below_discr_def) - -end - - -subsection \\emph{undiscr}\ - -definition undiscr :: "('a::type)discr \ 'a" - where "undiscr x = (case x of Discr y \ y)" - -lemma undiscr_Discr [simp]: "undiscr (Discr x) = x" - by (simp add: undiscr_def) - -lemma Discr_undiscr [simp]: "Discr (undiscr y) = y" - by (induct y) simp - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Domain.thy --- a/src/HOL/HOLCF/Domain.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Domain.thy Wed Dec 11 13:44:35 2024 +0100 @@ -5,17 +5,377 @@ section \Domain package\ theory Domain -imports Representable Domain_Aux +imports Representable Map_Functions Fixrec keywords "lazy" "unsafe" and "domaindef" "domain" :: thy_defn and "domain_isomorphism" :: thy_decl begin -default_sort "domain" +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 \ 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 \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\ +simproc_setup cont ("cont f") = \K ContProc.cont_proc\ + +ML_file \Tools/Domain/domain_constructors.ML\ +ML_file \Tools/Domain/domain_induction.ML\ + subsection \Representations of types\ +default_sort "domain" + lemma emb_prj: "emb\((prj\x)::'a) = cast\DEFL('a)\x" by (simp add: cast_DEFL) @@ -60,6 +420,7 @@ unfolding abs_def rep_def by (simp add: emb_prj_emb DEFL) + subsection \Deflations as sets\ definition defl_set :: "'a::bifinite defl \ 'a set" @@ -79,6 +440,7 @@ apply (auto simp add: cast.belowI cast.belowD) done + subsection \Proving a subtype is representable\ text \Temporarily relax type constraints.\ @@ -153,6 +515,7 @@ ML_file \Tools/domaindef.ML\ + subsection \Isomorphic deflations\ definition isodefl :: "('a \ 'a) \ udom defl \ bool" @@ -315,6 +678,7 @@ using isodefl_sfun [OF assms] unfolding isodefl_def by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map) + subsection \Setting up the domain package\ named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)" diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Domain_Aux.thy --- a/src/HOL/HOLCF/Domain_Aux.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,366 +0,0 @@ -(* 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 \ 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 \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\ -simproc_setup cont ("cont f") = \K ContProc.cont_proc\ - -ML_file \Tools/Domain/domain_constructors.ML\ -ML_file \Tools/Domain/domain_induction.ML\ - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/FOCUS/Stream_adm.thy --- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy Wed Dec 11 13:44:35 2024 +0100 @@ -30,8 +30,8 @@ section "admissibility" lemma infinite_chain_adm_lemma: - "\Porder.chain Y; \i. P (Y i); - \Y. \Porder.chain Y; \i. P (Y i); \ finite_chain Y\ \ P (\i. Y i)\ + "\chain Y; \i. P (Y i); + \Y. \chain Y; \i. P (Y i); \ finite_chain Y\ \ P (\i. Y i)\ \ P (\i. Y i)" apply (case_tac "finite_chain Y") prefer 2 apply fast @@ -43,7 +43,7 @@ done lemma increasing_chain_adm_lemma: - "\Porder.chain Y; \i. P (Y i); \Y. \Porder.chain Y; \i. P (Y i); + "\chain Y; \i. P (Y i); \Y. \chain Y; \i. P (Y i); \i. \j>i. Y i \ Y j \ Y i \ Y j\ \ P (\i. Y i)\ \ P (\i. Y i)" apply (erule infinite_chain_adm_lemma) @@ -55,9 +55,9 @@ done lemma flatstream_adm_lemma: - assumes 1: "Porder.chain Y" + assumes 1: "chain Y" assumes 2: "\i. P (Y i)" - assumes 3: "(\Y. [| Porder.chain Y; \i. P (Y i); \k. \j. enat k < #((Y j)::'a::flat stream)|] + assumes 3: "(\Y. [| chain Y; \i. P (Y i); \k. \j. enat k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))" shows "P(LUB i. Y i)" apply (rule increasing_chain_adm_lemma [OF 1 2]) @@ -78,7 +78,7 @@ done (* should be without reference to stream length? *) -lemma flatstream_admI: "[|(\Y. [| Porder.chain Y; \i. P (Y i); +lemma flatstream_admI: "[|(\Y. [| chain Y; \i. P (Y i); \k. \j. enat k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P" apply (unfold adm_def) apply (intro strip) @@ -210,13 +210,13 @@ done lemma adm_set: -"{\i. Y i |Y. Porder.chain Y \ (\i. Y i \ P)} \ P \ adm (\x. x\P)" +"{\i. Y i |Y. chain Y \ (\i. Y i \ P)} \ P \ adm (\x. x\P)" apply (unfold adm_def) apply (fast) done -lemma def_gfp_admI: "P \ gfp F \ {\i. Y i |Y. Porder.chain Y \ (\i. Y i \ P)} \ - F {\i. Y i |Y. Porder.chain Y \ (\i. Y i \ P)} \ adm (\x. x\P)" +lemma def_gfp_admI: "P \ gfp F \ {\i. Y i |Y. chain Y \ (\i. Y i \ P)} \ + F {\i. Y i |Y. chain Y \ (\i. Y i \ P)} \ adm (\x. x\P)" apply (simp) apply (rule adm_set) apply (erule gfp_upperbound) diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Fix.thy --- a/src/HOL/HOLCF/Fix.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,247 +0,0 @@ -(* Title: HOL/HOLCF/Fix.thy - Author: Franz Regensburger - Author: Brian Huffman -*) - -section \Fixed point operator and admissibility\ - -theory Fix - imports Cfun -begin - -default_sort pcpo - - -subsection \Iteration\ - -primrec iterate :: "nat \ ('a::cpo \ 'a) \ ('a \ 'a)" - where - "iterate 0 = (\ F x. x)" - | "iterate (Suc n) = (\ F x. F\(iterate n\F\x))" - -text \Derive inductive properties of iterate from primitive recursion\ - -lemma iterate_0 [simp]: "iterate 0\F\x = x" - by simp - -lemma iterate_Suc [simp]: "iterate (Suc n)\F\x = F\(iterate n\F\x)" - by simp - -declare iterate.simps [simp del] - -lemma iterate_Suc2: "iterate (Suc n)\F\x = iterate n\F\(F\x)" - by (induct n) simp_all - -lemma iterate_iterate: "iterate m\F\(iterate n\F\x) = iterate (m + n)\F\x" - by (induct m) simp_all - -text \The sequence of function iterations is a chain.\ - -lemma chain_iterate [simp]: "chain (\i. iterate i\F\\)" - by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal) - - -subsection \Least fixed point operator\ - -definition "fix" :: "('a \ 'a) \ 'a" - where "fix = (\ F. \i. iterate i\F\\)" - -text \Binder syntax for \<^term>\fix\\ - -abbreviation fix_syn :: "('a \ 'a) \ 'a" (binder \\ \ 10) - where "fix_syn (\x. f x) \ fix\(\ x. f x)" - -notation (ASCII) - fix_syn (binder \FIX \ 10) - -text \Properties of \<^term>\fix\\ - -text \direct connection between \<^term>\fix\ and iteration\ - -lemma fix_def2: "fix\F = (\i. iterate i\F\\)" - by (simp add: fix_def) - -lemma iterate_below_fix: "iterate n\f\\ \ fix\f" - unfolding fix_def2 - using chain_iterate by (rule is_ub_thelub) - -text \ - Kleene's fixed point theorems for continuous functions in pointed - omega cpo's -\ - -lemma fix_eq: "fix\F = F\(fix\F)" - apply (simp add: fix_def2) - apply (subst lub_range_shift [of _ 1, symmetric]) - apply (rule chain_iterate) - apply (subst contlub_cfun_arg) - apply (rule chain_iterate) - apply simp - done - -lemma fix_least_below: "F\x \ x \ fix\F \ x" - apply (simp add: fix_def2) - apply (rule lub_below) - apply (rule chain_iterate) - apply (induct_tac i) - apply simp - apply simp - apply (erule rev_below_trans) - apply (erule monofun_cfun_arg) - done - -lemma fix_least: "F\x = x \ fix\F \ x" - by (rule fix_least_below) simp - -lemma fix_eqI: - assumes fixed: "F\x = x" - and least: "\z. F\z = z \ x \ z" - shows "fix\F = x" - apply (rule below_antisym) - apply (rule fix_least [OF fixed]) - apply (rule least [OF fix_eq [symmetric]]) - done - -lemma fix_eq2: "f \ fix\F \ f = F\f" - by (simp add: fix_eq [symmetric]) - -lemma fix_eq3: "f \ fix\F \ f\x = F\f\x" - by (erule fix_eq2 [THEN cfun_fun_cong]) - -lemma fix_eq4: "f = fix\F \ f = F\f" - by (erule ssubst) (rule fix_eq) - -lemma fix_eq5: "f = fix\F \ f\x = F\f\x" - by (erule fix_eq4 [THEN cfun_fun_cong]) - -text \strictness of \<^term>\fix\\ - -lemma fix_bottom_iff: "fix\F = \ \ F\\ = \" - apply (rule iffI) - apply (erule subst) - apply (rule fix_eq [symmetric]) - apply (erule fix_least [THEN bottomI]) - done - -lemma fix_strict: "F\\ = \ \ fix\F = \" - by (simp add: fix_bottom_iff) - -lemma fix_defined: "F\\ \ \ \ fix\F \ \" - by (simp add: fix_bottom_iff) - -text \\<^term>\fix\ applied to identity and constant functions\ - -lemma fix_id: "(\ x. x) = \" - by (simp add: fix_strict) - -lemma fix_const: "(\ x. c) = c" - by (subst fix_eq) simp - - -subsection \Fixed point induction\ - -lemma fix_ind: "adm P \ P \ \ (\x. P x \ P (F\x)) \ P (fix\F)" - unfolding fix_def2 - apply (erule admD) - apply (rule chain_iterate) - apply (rule nat_induct, simp_all) - done - -lemma cont_fix_ind: "cont F \ adm P \ P \ \ (\x. P x \ P (F x)) \ P (fix\(Abs_cfun F))" - by (simp add: fix_ind) - -lemma def_fix_ind: "\f \ fix\F; adm P; P \; \x. P x \ P (F\x)\ \ P f" - by (simp add: fix_ind) - -lemma fix_ind2: - assumes adm: "adm P" - assumes 0: "P \" and 1: "P (F\\)" - assumes step: "\x. \P x; P (F\x)\ \ P (F\(F\x))" - shows "P (fix\F)" - unfolding fix_def2 - apply (rule admD [OF adm chain_iterate]) - apply (rule nat_less_induct) - apply (case_tac n) - apply (simp add: 0) - apply (case_tac nat) - apply (simp add: 1) - apply (frule_tac x=nat in spec) - apply (simp add: step) - done - -lemma parallel_fix_ind: - assumes adm: "adm (\x. P (fst x) (snd x))" - assumes base: "P \ \" - assumes step: "\x y. P x y \ P (F\x) (G\y)" - shows "P (fix\F) (fix\G)" -proof - - from adm have adm': "adm (case_prod P)" - unfolding split_def . - have "P (iterate i\F\\) (iterate i\G\\)" for i - by (induct i) (simp add: base, simp add: step) - then have "\i. case_prod P (iterate i\F\\, iterate i\G\\)" - by simp - then have "case_prod P (\i. (iterate i\F\\, iterate i\G\\))" - by - (rule admD [OF adm'], simp, assumption) - then have "case_prod P (\i. iterate i\F\\, \i. iterate i\G\\)" - by (simp add: lub_Pair) - then have "P (\i. iterate i\F\\) (\i. iterate i\G\\)" - by simp - then show "P (fix\F) (fix\G)" - by (simp add: fix_def2) -qed - -lemma cont_parallel_fix_ind: - assumes "cont F" and "cont G" - assumes "adm (\x. P (fst x) (snd x))" - assumes "P \ \" - assumes "\x y. P x y \ P (F x) (G y)" - shows "P (fix\(Abs_cfun F)) (fix\(Abs_cfun G))" - by (rule parallel_fix_ind) (simp_all add: assms) - - -subsection \Fixed-points on product types\ - -text \ - Bekic's Theorem: Simultaneous fixed points over pairs - can be written in terms of separate fixed points. -\ - -lemma fix_cprod: - "fix\(F::'a \ 'b \ 'a \ 'b) = - (\ x. fst (F\(x, \ y. snd (F\(x, y)))), - \ y. snd (F\(\ x. fst (F\(x, \ y. snd (F\(x, y)))), y)))" - (is "fix\F = (?x, ?y)") -proof (rule fix_eqI) - have *: "fst (F\(?x, ?y)) = ?x" - by (rule trans [symmetric, OF fix_eq], simp) - have "snd (F\(?x, ?y)) = ?y" - by (rule trans [symmetric, OF fix_eq], simp) - with * show "F\(?x, ?y) = (?x, ?y)" - by (simp add: prod_eq_iff) -next - fix z - assume F_z: "F\z = z" - obtain x y where z: "z = (x, y)" by (rule prod.exhaust) - from F_z z have F_x: "fst (F\(x, y)) = x" by simp - from F_z z have F_y: "snd (F\(x, y)) = y" by simp - let ?y1 = "\ y. snd (F\(x, y))" - have "?y1 \ y" - by (rule fix_least) (simp add: F_y) - then have "fst (F\(x, ?y1)) \ fst (F\(x, y))" - by (simp add: fst_monofun monofun_cfun) - with F_x have "fst (F\(x, ?y1)) \ x" - by simp - then have *: "?x \ x" - by (simp add: fix_least_below) - then have "snd (F\(?x, y)) \ snd (F\(x, y))" - by (simp add: snd_monofun monofun_cfun) - with F_y have "snd (F\(?x, y)) \ y" - by simp - then have "?y \ y" - by (simp add: fix_least_below) - with z * show "(?x, ?y) \ z" - by simp -qed - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Fixrec.thy --- a/src/HOL/HOLCF/Fixrec.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Fixrec.thy Wed Dec 11 13:44:35 2024 +0100 @@ -1,14 +1,253 @@ (* Title: HOL/HOLCF/Fixrec.thy + Author: Franz Regensburger Author: Amber Telfer and Brian Huffman *) -section "Package for defining recursive functions in HOLCF" - theory Fixrec -imports Cprod Sprod Ssum Up One Tr Fix +imports Cprod Sprod Ssum Up One Tr Cfun keywords "fixrec" :: thy_defn begin +section \Fixed point operator and admissibility\ + +default_sort pcpo + + +subsection \Iteration\ + +primrec iterate :: "nat \ ('a::cpo \ 'a) \ ('a \ 'a)" + where + "iterate 0 = (\ F x. x)" + | "iterate (Suc n) = (\ F x. F\(iterate n\F\x))" + +text \Derive inductive properties of iterate from primitive recursion\ + +lemma iterate_0 [simp]: "iterate 0\F\x = x" + by simp + +lemma iterate_Suc [simp]: "iterate (Suc n)\F\x = F\(iterate n\F\x)" + by simp + +declare iterate.simps [simp del] + +lemma iterate_Suc2: "iterate (Suc n)\F\x = iterate n\F\(F\x)" + by (induct n) simp_all + +lemma iterate_iterate: "iterate m\F\(iterate n\F\x) = iterate (m + n)\F\x" + by (induct m) simp_all + +text \The sequence of function iterations is a chain.\ + +lemma chain_iterate [simp]: "chain (\i. iterate i\F\\)" + by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal) + + +subsection \Least fixed point operator\ + +definition "fix" :: "('a \ 'a) \ 'a" + where "fix = (\ F. \i. iterate i\F\\)" + +text \Binder syntax for \<^term>\fix\\ + +abbreviation fix_syn :: "('a \ 'a) \ 'a" (binder \\ \ 10) + where "fix_syn (\x. f x) \ fix\(\ x. f x)" + +notation (ASCII) + fix_syn (binder \FIX \ 10) + +text \Properties of \<^term>\fix\\ + +text \direct connection between \<^term>\fix\ and iteration\ + +lemma fix_def2: "fix\F = (\i. iterate i\F\\)" + by (simp add: fix_def) + +lemma iterate_below_fix: "iterate n\f\\ \ fix\f" + unfolding fix_def2 + using chain_iterate by (rule is_ub_thelub) + +text \ + Kleene's fixed point theorems for continuous functions in pointed + omega cpo's +\ + +lemma fix_eq: "fix\F = F\(fix\F)" + apply (simp add: fix_def2) + apply (subst lub_range_shift [of _ 1, symmetric]) + apply (rule chain_iterate) + apply (subst contlub_cfun_arg) + apply (rule chain_iterate) + apply simp + done + +lemma fix_least_below: "F\x \ x \ fix\F \ x" + apply (simp add: fix_def2) + apply (rule lub_below) + apply (rule chain_iterate) + apply (induct_tac i) + apply simp + apply simp + apply (erule rev_below_trans) + apply (erule monofun_cfun_arg) + done + +lemma fix_least: "F\x = x \ fix\F \ x" + by (rule fix_least_below) simp + +lemma fix_eqI: + assumes fixed: "F\x = x" + and least: "\z. F\z = z \ x \ z" + shows "fix\F = x" + apply (rule below_antisym) + apply (rule fix_least [OF fixed]) + apply (rule least [OF fix_eq [symmetric]]) + done + +lemma fix_eq2: "f \ fix\F \ f = F\f" + by (simp add: fix_eq [symmetric]) + +lemma fix_eq3: "f \ fix\F \ f\x = F\f\x" + by (erule fix_eq2 [THEN cfun_fun_cong]) + +lemma fix_eq4: "f = fix\F \ f = F\f" + by (erule ssubst) (rule fix_eq) + +lemma fix_eq5: "f = fix\F \ f\x = F\f\x" + by (erule fix_eq4 [THEN cfun_fun_cong]) + +text \strictness of \<^term>\fix\\ + +lemma fix_bottom_iff: "fix\F = \ \ F\\ = \" + apply (rule iffI) + apply (erule subst) + apply (rule fix_eq [symmetric]) + apply (erule fix_least [THEN bottomI]) + done + +lemma fix_strict: "F\\ = \ \ fix\F = \" + by (simp add: fix_bottom_iff) + +lemma fix_defined: "F\\ \ \ \ fix\F \ \" + by (simp add: fix_bottom_iff) + +text \\<^term>\fix\ applied to identity and constant functions\ + +lemma fix_id: "(\ x. x) = \" + by (simp add: fix_strict) + +lemma fix_const: "(\ x. c) = c" + by (subst fix_eq) simp + + +subsection \Fixed point induction\ + +lemma fix_ind: "adm P \ P \ \ (\x. P x \ P (F\x)) \ P (fix\F)" + unfolding fix_def2 + apply (erule admD) + apply (rule chain_iterate) + apply (rule nat_induct, simp_all) + done + +lemma cont_fix_ind: "cont F \ adm P \ P \ \ (\x. P x \ P (F x)) \ P (fix\(Abs_cfun F))" + by (simp add: fix_ind) + +lemma def_fix_ind: "\f \ fix\F; adm P; P \; \x. P x \ P (F\x)\ \ P f" + by (simp add: fix_ind) + +lemma fix_ind2: + assumes adm: "adm P" + assumes 0: "P \" and 1: "P (F\\)" + assumes step: "\x. \P x; P (F\x)\ \ P (F\(F\x))" + shows "P (fix\F)" + unfolding fix_def2 + apply (rule admD [OF adm chain_iterate]) + apply (rule nat_less_induct) + apply (case_tac n) + apply (simp add: 0) + apply (case_tac nat) + apply (simp add: 1) + apply (frule_tac x=nat in spec) + apply (simp add: step) + done + +lemma parallel_fix_ind: + assumes adm: "adm (\x. P (fst x) (snd x))" + assumes base: "P \ \" + assumes step: "\x y. P x y \ P (F\x) (G\y)" + shows "P (fix\F) (fix\G)" +proof - + from adm have adm': "adm (case_prod P)" + unfolding split_def . + have "P (iterate i\F\\) (iterate i\G\\)" for i + by (induct i) (simp add: base, simp add: step) + then have "\i. case_prod P (iterate i\F\\, iterate i\G\\)" + by simp + then have "case_prod P (\i. (iterate i\F\\, iterate i\G\\))" + by - (rule admD [OF adm'], simp, assumption) + then have "case_prod P (\i. iterate i\F\\, \i. iterate i\G\\)" + by (simp add: lub_Pair) + then have "P (\i. iterate i\F\\) (\i. iterate i\G\\)" + by simp + then show "P (fix\F) (fix\G)" + by (simp add: fix_def2) +qed + +lemma cont_parallel_fix_ind: + assumes "cont F" and "cont G" + assumes "adm (\x. P (fst x) (snd x))" + assumes "P \ \" + assumes "\x y. P x y \ P (F x) (G y)" + shows "P (fix\(Abs_cfun F)) (fix\(Abs_cfun G))" + by (rule parallel_fix_ind) (simp_all add: assms) + + +subsection \Fixed-points on product types\ + +text \ + Bekic's Theorem: Simultaneous fixed points over pairs + can be written in terms of separate fixed points. +\ + +lemma fix_cprod: + "fix\(F::'a \ 'b \ 'a \ 'b) = + (\ x. fst (F\(x, \ y. snd (F\(x, y)))), + \ y. snd (F\(\ x. fst (F\(x, \ y. snd (F\(x, y)))), y)))" + (is "fix\F = (?x, ?y)") +proof (rule fix_eqI) + have *: "fst (F\(?x, ?y)) = ?x" + by (rule trans [symmetric, OF fix_eq], simp) + have "snd (F\(?x, ?y)) = ?y" + by (rule trans [symmetric, OF fix_eq], simp) + with * show "F\(?x, ?y) = (?x, ?y)" + by (simp add: prod_eq_iff) +next + fix z + assume F_z: "F\z = z" + obtain x y where z: "z = (x, y)" by (rule prod.exhaust) + from F_z z have F_x: "fst (F\(x, y)) = x" by simp + from F_z z have F_y: "snd (F\(x, y)) = y" by simp + let ?y1 = "\ y. snd (F\(x, y))" + have "?y1 \ y" + by (rule fix_least) (simp add: F_y) + then have "fst (F\(x, ?y1)) \ fst (F\(x, y))" + by (simp add: fst_monofun monofun_cfun) + with F_x have "fst (F\(x, ?y1)) \ x" + by simp + then have *: "?x \ x" + by (simp add: fix_least_below) + then have "snd (F\(?x, y)) \ snd (F\(x, y))" + by (simp add: snd_monofun monofun_cfun) + with F_y have "snd (F\(?x, y)) \ y" + by simp + then have "?y \ y" + by (simp add: fix_least_below) + with z * show "(?x, ?y) \ z" + by simp +qed + + +section "Package for defining recursive functions in HOLCF" + subsection \Pattern-match monad\ default_sort cpo @@ -46,6 +285,7 @@ "succeed\x \ fail" "fail \ succeed\x" by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject) + subsubsection \Run operator\ definition @@ -66,6 +306,7 @@ unfolding run_def succeed_def by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse) + subsubsection \Monad plus operator\ definition @@ -96,6 +337,7 @@ lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" by (cases x, simp_all) + subsection \Match functions for built-in types\ default_sort pcpo @@ -192,6 +434,7 @@ "match_FF\\\k = \" by (simp_all add: match_FF_def) + subsection \Mutual recursion\ text \ diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Fun_Cpo.thy --- a/src/HOL/HOLCF/Fun_Cpo.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,150 +0,0 @@ -(* Title: HOL/HOLCF/Fun_Cpo.thy - Author: Franz Regensburger - Author: Brian Huffman -*) - -section \Class instances for the full function space\ - -theory Fun_Cpo - imports Adm -begin - -subsection \Full function space is a partial order\ - -instantiation "fun" :: (type, below) below -begin - -definition below_fun_def: "(\) \ (\f g. \x. f x \ g x)" - -instance .. -end - -instance "fun" :: (type, po) po -proof - fix f :: "'a \ 'b" - show "f \ f" - by (simp add: below_fun_def) -next - fix f g :: "'a \ 'b" - assume "f \ g" and "g \ f" then show "f = g" - by (simp add: below_fun_def fun_eq_iff below_antisym) -next - fix f g h :: "'a \ 'b" - assume "f \ g" and "g \ h" then show "f \ h" - unfolding below_fun_def by (fast elim: below_trans) -qed - -lemma fun_below_iff: "f \ g \ (\x. f x \ g x)" - by (simp add: below_fun_def) - -lemma fun_belowI: "(\x. f x \ g x) \ f \ g" - by (simp add: below_fun_def) - -lemma fun_belowD: "f \ g \ f x \ g x" - by (simp add: below_fun_def) - - -subsection \Full function space is chain complete\ - -text \Properties of chains of functions.\ - -lemma fun_chain_iff: "chain S \ (\x. chain (\i. S i x))" - by (auto simp: chain_def fun_below_iff) - -lemma ch2ch_fun: "chain S \ chain (\i. S i x)" - by (simp add: chain_def below_fun_def) - -lemma ch2ch_lambda: "(\x. chain (\i. S i x)) \ chain S" - by (simp add: chain_def below_fun_def) - -text \Type \<^typ>\'a::type \ 'b::cpo\ is chain complete\ - -lemma is_lub_lambda: "(\x. range (\i. Y i x) <<| f x) \ range Y <<| f" - by (simp add: is_lub_def is_ub_def below_fun_def) - -lemma is_lub_fun: "chain S \ range S <<| (\x. \i. S i x)" - for S :: "nat \ 'a::type \ 'b::cpo" - apply (rule is_lub_lambda) - apply (rule cpo_lubI) - apply (erule ch2ch_fun) - done - -lemma lub_fun: "chain S \ (\i. S i) = (\x. \i. S i x)" - for S :: "nat \ 'a::type \ 'b::cpo" - by (rule is_lub_fun [THEN lub_eqI]) - -instance "fun" :: (type, cpo) cpo - by intro_classes (rule exI, erule is_lub_fun) - -instance "fun" :: (type, discrete_cpo) discrete_cpo -proof - fix f g :: "'a \ 'b" - show "f \ g \ f = g" - by (simp add: fun_below_iff fun_eq_iff) -qed - - -subsection \Full function space is pointed\ - -lemma minimal_fun: "(\x. \) \ f" - by (simp add: below_fun_def) - -instance "fun" :: (type, pcpo) pcpo - by standard (fast intro: minimal_fun) - -lemma inst_fun_pcpo: "\ = (\x. \)" - by (rule minimal_fun [THEN bottomI, symmetric]) - -lemma app_strict [simp]: "\ x = \" - by (simp add: inst_fun_pcpo) - -lemma lambda_strict: "(\x. \) = \" - by (rule bottomI, rule minimal_fun) - - -subsection \Propagation of monotonicity and continuity\ - -text \The lub of a chain of monotone functions is monotone.\ - -lemma adm_monofun: "adm monofun" - by (rule admI) (simp add: lub_fun fun_chain_iff monofun_def lub_mono) - -text \The lub of a chain of continuous functions is continuous.\ - -lemma adm_cont: "adm cont" - by (rule admI) (simp add: lub_fun fun_chain_iff) - -text \Function application preserves monotonicity and continuity.\ - -lemma mono2mono_fun: "monofun f \ monofun (\x. f x y)" - by (simp add: monofun_def fun_below_iff) - -lemma cont2cont_fun: "cont f \ cont (\x. f x y)" - apply (rule contI2) - apply (erule cont2mono [THEN mono2mono_fun]) - apply (simp add: cont2contlubE lub_fun ch2ch_cont) - done - -lemma cont_fun: "cont (\f. f x)" - using cont_id by (rule cont2cont_fun) - -text \ - Lambda abstraction preserves monotonicity and continuity. - (Note \(\x. \y. f x y) = f\.) -\ - -lemma mono2mono_lambda: "(\y. monofun (\x. f x y)) \ monofun f" - by (simp add: monofun_def fun_below_iff) - -lemma cont2cont_lambda [simp]: - assumes f: "\y. cont (\x. f x y)" - shows "cont f" - by (rule contI, rule is_lub_lambda, rule contE [OF f]) - -text \What D.A.Schmidt calls continuity of abstraction; never used here\ - -lemma contlub_lambda: "(\x. chain (\i. S i x)) \ (\x. \i. S i x) = (\i. (\x. S i x))" - for S :: "nat \ 'a::type \ 'b::cpo" - by (simp add: lub_fun ch2ch_lambda) - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Lift.thy --- a/src/HOL/HOLCF/Lift.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Lift.thy Wed Dec 11 13:44:35 2024 +0100 @@ -5,7 +5,7 @@ section \Lifting types of class type to flat pcpo's\ theory Lift -imports Discrete_Cpo Up +imports Up begin default_sort type @@ -19,6 +19,7 @@ Def :: "'a \ 'a lift" where "Def x = Abs_lift (up\(Discr x))" + subsection \Lift as a datatype\ lemma lift_induct: "\P \; \x. P (Def x)\ \ P y" @@ -70,6 +71,7 @@ by (induct x) auto qed + subsection \Continuity of \<^const>\case_lift\\ lemma case_lift_eq: "case_lift \ f x = fup\(\ y. f (undiscr y))\(Rep_lift x)" @@ -82,6 +84,7 @@ "\\y. cont (\x. f x y); cont g\ \ cont (\x. case_lift \ (f x) (g x))" unfolding case_lift_eq by (simp add: cont_Rep_lift) + subsection \Further operations\ definition diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/LowerPD.thy Wed Dec 11 13:44:35 2024 +0100 @@ -459,6 +459,7 @@ by (rule finite_range_imp_finite_fixes) qed + subsection \Lower powerdomain is bifinite\ lemma approx_chain_lower_map: @@ -474,6 +475,7 @@ by (fast intro!: approx_chain_lower_map) qed + subsection \Join\ definition diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Pcpo.thy --- a/src/HOL/HOLCF/Pcpo.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,256 +0,0 @@ -(* Title: HOL/HOLCF/Pcpo.thy - Author: Franz Regensburger -*) - -section \Classes cpo and pcpo\ - -theory Pcpo - imports Porder -begin - -subsection \Complete partial orders\ - -text \The class cpo of chain complete partial orders\ - -class cpo = po + - assumes cpo: "chain S \ \x. range S <<| x" -begin - -text \in cpo's everthing equal to THE lub has lub properties for every chain\ - -lemma cpo_lubI: "chain S \ range S <<| (\i. S i)" - by (fast dest: cpo elim: is_lub_lub) - -lemma thelubE: "\chain S; (\i. S i) = l\ \ range S <<| l" - by (blast dest: cpo intro: is_lub_lub) - -text \Properties of the lub\ - -lemma is_ub_thelub: "chain S \ S x \ (\i. S i)" - by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1]) - -lemma is_lub_thelub: "\chain S; range S <| x\ \ (\i. S i) \ x" - by (blast dest: cpo intro: is_lub_lub [THEN is_lubD2]) - -lemma lub_below_iff: "chain S \ (\i. S i) \ x \ (\i. S i \ x)" - by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def) - -lemma lub_below: "\chain S; \i. S i \ x\ \ (\i. S i) \ x" - by (simp add: lub_below_iff) - -lemma below_lub: "\chain S; x \ S i\ \ x \ (\i. S i)" - by (erule below_trans, erule is_ub_thelub) - -lemma lub_range_mono: "\range X \ range Y; chain Y; chain X\ \ (\i. X i) \ (\i. Y i)" - apply (erule lub_below) - apply (subgoal_tac "\j. X i = Y j") - apply clarsimp - apply (erule is_ub_thelub) - apply auto - done - -lemma lub_range_shift: "chain Y \ (\i. Y (i + j)) = (\i. Y i)" - apply (rule below_antisym) - apply (rule lub_range_mono) - apply fast - apply assumption - apply (erule chain_shift) - apply (rule lub_below) - apply assumption - apply (rule_tac i="i" in below_lub) - apply (erule chain_shift) - apply (erule chain_mono) - apply (rule le_add1) - done - -lemma maxinch_is_thelub: "chain Y \ max_in_chain i Y = ((\i. Y i) = Y i)" - apply (rule iffI) - apply (fast intro!: lub_eqI lub_finch1) - apply (unfold max_in_chain_def) - apply (safe intro!: below_antisym) - apply (fast elim!: chain_mono) - apply (drule sym) - apply (force elim!: is_ub_thelub) - done - -text \the \\\ relation between two chains is preserved by their lubs\ - -lemma lub_mono: "\chain X; chain Y; \i. X i \ Y i\ \ (\i. X i) \ (\i. Y i)" - by (fast elim: lub_below below_lub) - -text \the = relation between two chains is preserved by their lubs\ - -lemma lub_eq: "(\i. X i = Y i) \ (\i. X i) = (\i. Y i)" - by simp - -lemma ch2ch_lub: - assumes 1: "\j. chain (\i. Y i j)" - assumes 2: "\i. chain (\j. Y i j)" - shows "chain (\i. \j. Y i j)" - apply (rule chainI) - apply (rule lub_mono [OF 2 2]) - apply (rule chainE [OF 1]) - done - -lemma diag_lub: - assumes 1: "\j. chain (\i. Y i j)" - assumes 2: "\i. chain (\j. Y i j)" - shows "(\i. \j. Y i j) = (\i. Y i i)" -proof (rule below_antisym) - have 3: "chain (\i. Y i i)" - apply (rule chainI) - apply (rule below_trans) - apply (rule chainE [OF 1]) - apply (rule chainE [OF 2]) - done - have 4: "chain (\i. \j. Y i j)" - by (rule ch2ch_lub [OF 1 2]) - show "(\i. \j. Y i j) \ (\i. Y i i)" - apply (rule lub_below [OF 4]) - apply (rule lub_below [OF 2]) - apply (rule below_lub [OF 3]) - apply (rule below_trans) - apply (rule chain_mono [OF 1 max.cobounded1]) - apply (rule chain_mono [OF 2 max.cobounded2]) - done - show "(\i. Y i i) \ (\i. \j. Y i j)" - apply (rule lub_mono [OF 3 4]) - apply (rule is_ub_thelub [OF 2]) - done -qed - -lemma ex_lub: - assumes 1: "\j. chain (\i. Y i j)" - assumes 2: "\i. chain (\j. Y i j)" - shows "(\i. \j. Y i j) = (\j. \i. Y i j)" - by (simp add: diag_lub 1 2) - -end - - -subsection \Pointed cpos\ - -text \The class pcpo of pointed cpos\ - -class pcpo = cpo + - assumes least: "\x. \y. x \ y" -begin - -definition bottom :: "'a" (\\\) - where "bottom = (THE x. \y. x \ y)" - -lemma minimal [iff]: "\ \ x" - unfolding bottom_def - apply (rule the1I2) - apply (rule ex_ex1I) - apply (rule least) - apply (blast intro: below_antisym) - apply simp - done - -end - -text \Old "UU" syntax:\ -abbreviation (input) "UU \ bottom" - -text \Simproc to rewrite \<^term>\\ = x\ to \<^term>\x = \\.\ -setup \Reorient_Proc.add (fn \<^Const_>\bottom _\ => true | _ => false)\ -simproc_setup reorient_bottom ("\ = x") = \K Reorient_Proc.proc\ - -text \useful lemmas about \<^term>\\\\ - -lemma below_bottom_iff [simp]: "x \ \ \ x = \" - by (simp add: po_eq_conv) - -lemma eq_bottom_iff: "x = \ \ x \ \" - by simp - -lemma bottomI: "x \ \ \ x = \" - by (subst eq_bottom_iff) - -lemma lub_eq_bottom_iff: "chain Y \ (\i. Y i) = \ \ (\i. Y i = \)" - by (simp only: eq_bottom_iff lub_below_iff) - - -subsection \Chain-finite and flat cpos\ - -text \further useful classes for HOLCF domains\ - -class chfin = po + - assumes chfin: "chain Y \ \n. max_in_chain n Y" -begin - -subclass cpo - apply standard - apply (frule chfin) - apply (blast intro: lub_finch1) - done - -lemma chfin2finch: "chain Y \ finite_chain Y" - by (simp add: chfin finite_chain_def) - -end - -class flat = pcpo + - assumes ax_flat: "x \ y \ x = \ \ x = y" -begin - -subclass chfin -proof - fix Y - assume *: "chain Y" - show "\n. max_in_chain n Y" - apply (unfold max_in_chain_def) - apply (cases "\i. Y i = \") - apply simp - apply simp - apply (erule exE) - apply (rule_tac x="i" in exI) - apply clarify - using * apply (blast dest: chain_mono ax_flat) - done -qed - -lemma flat_below_iff: "x \ y \ x = \ \ x = y" - by (safe dest!: ax_flat) - -lemma flat_eq: "a \ \ \ a \ b = (a = b)" - by (safe dest!: ax_flat) - -end - -subsection \Discrete cpos\ - -class discrete_cpo = below + - assumes discrete_cpo [simp]: "x \ y \ x = y" -begin - -subclass po - by standard simp_all - -text \In a discrete cpo, every chain is constant\ - -lemma discrete_chain_const: - assumes S: "chain S" - shows "\x. S = (\i. x)" -proof (intro exI ext) - fix i :: nat - from S le0 have "S 0 \ S i" by (rule chain_mono) - then have "S 0 = S i" by simp - then show "S i = S 0" by (rule sym) -qed - -subclass chfin -proof - fix S :: "nat \ 'a" - assume S: "chain S" - then have "\x. S = (\i. x)" - by (rule discrete_chain_const) - then have "max_in_chain 0 S" - by (auto simp: max_in_chain_def) - then show "\i. max_in_chain i S" .. -qed - -end - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Porder.thy --- a/src/HOL/HOLCF/Porder.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,343 +0,0 @@ -(* Title: HOL/HOLCF/Porder.thy - Author: Franz Regensburger and Brian Huffman -*) - -section \Partial orders\ - -theory Porder - imports Main -begin - -declare [[typedef_overloaded]] - - -subsection \Type class for partial orders\ - -class below = - fixes below :: "'a \ 'a \ bool" -begin - -notation (ASCII) - below (infix \<<\ 50) - -notation - below (infix \\\ 50) - -abbreviation not_below :: "'a \ 'a \ bool" (infix \\\ 50) - where "not_below x y \ \ below x y" - -notation (ASCII) - not_below (infix \~<<\ 50) - -lemma below_eq_trans: "a \ b \ b = c \ a \ c" - by (rule subst) - -lemma eq_below_trans: "a = b \ b \ c \ a \ c" - by (rule ssubst) - -end - -class po = below + - assumes below_refl [iff]: "x \ x" - assumes below_trans: "x \ y \ y \ z \ x \ z" - assumes below_antisym: "x \ y \ y \ x \ x = y" -begin - -lemma eq_imp_below: "x = y \ x \ y" - by simp - -lemma box_below: "a \ b \ c \ a \ b \ d \ c \ d" - by (rule below_trans [OF below_trans]) - -lemma po_eq_conv: "x = y \ x \ y \ y \ x" - by (fast intro!: below_antisym) - -lemma rev_below_trans: "y \ z \ x \ y \ x \ z" - by (rule below_trans) - -lemma not_below2not_eq: "x \ y \ x \ y" - by auto - -end - -lemmas HOLCF_trans_rules [trans] = - below_trans - below_antisym - below_eq_trans - eq_below_trans - -context po -begin - -subsection \Upper bounds\ - -definition is_ub :: "'a set \ 'a \ bool" (infix \<|\ 55) - where "S <| x \ (\y\S. y \ x)" - -lemma is_ubI: "(\x. x \ S \ x \ u) \ S <| u" - by (simp add: is_ub_def) - -lemma is_ubD: "\S <| u; x \ S\ \ x \ u" - by (simp add: is_ub_def) - -lemma ub_imageI: "(\x. x \ S \ f x \ u) \ (\x. f x) ` S <| u" - unfolding is_ub_def by fast - -lemma ub_imageD: "\f ` S <| u; x \ S\ \ f x \ u" - unfolding is_ub_def by fast - -lemma ub_rangeI: "(\i. S i \ x) \ range S <| x" - unfolding is_ub_def by fast - -lemma ub_rangeD: "range S <| x \ S i \ x" - unfolding is_ub_def by fast - -lemma is_ub_empty [simp]: "{} <| u" - unfolding is_ub_def by fast - -lemma is_ub_insert [simp]: "(insert x A) <| y = (x \ y \ A <| y)" - unfolding is_ub_def by fast - -lemma is_ub_upward: "\S <| x; x \ y\ \ S <| y" - unfolding is_ub_def by (fast intro: below_trans) - - -subsection \Least upper bounds\ - -definition is_lub :: "'a set \ 'a \ bool" (infix \<<|\ 55) - where "S <<| x \ S <| x \ (\u. S <| u \ x \ u)" - -definition lub :: "'a set \ 'a" - where "lub S = (THE x. S <<| x)" - -end - -syntax (ASCII) - "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(\indent=3 notation=\binder LUB\\LUB _:_./ _)\ [0,0, 10] 10) - -syntax - "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0,0, 10] 10) - -syntax_consts - "_BLub" \ lub - -translations - "LUB x:A. t" \ "CONST lub ((\x. t) ` A)" - -context po -begin - -abbreviation Lub (binder \\\ 10) - where "\n. t n \ lub (range t)" - -notation (ASCII) - Lub (binder \LUB \ 10) - -text \access to some definition as inference rule\ - -lemma is_lubD1: "S <<| x \ S <| x" - unfolding is_lub_def by fast - -lemma is_lubD2: "\S <<| x; S <| u\ \ x \ u" - unfolding is_lub_def by fast - -lemma is_lubI: "\S <| x; \u. S <| u \ x \ u\ \ S <<| x" - unfolding is_lub_def by fast - -lemma is_lub_below_iff: "S <<| x \ x \ u \ S <| u" - unfolding is_lub_def is_ub_def by (metis below_trans) - -text \lubs are unique\ - -lemma is_lub_unique: "S <<| x \ S <<| y \ x = y" - unfolding is_lub_def is_ub_def by (blast intro: below_antisym) - -text \technical lemmas about \<^term>\lub\ and \<^term>\is_lub\\ - -lemma is_lub_lub: "M <<| x \ M <<| lub M" - unfolding lub_def by (rule theI [OF _ is_lub_unique]) - -lemma lub_eqI: "M <<| l \ lub M = l" - by (rule is_lub_unique [OF is_lub_lub]) - -lemma is_lub_singleton [simp]: "{x} <<| x" - by (simp add: is_lub_def) - -lemma lub_singleton [simp]: "lub {x} = x" - by (rule is_lub_singleton [THEN lub_eqI]) - -lemma is_lub_bin: "x \ y \ {x, y} <<| y" - by (simp add: is_lub_def) - -lemma lub_bin: "x \ y \ lub {x, y} = y" - by (rule is_lub_bin [THEN lub_eqI]) - -lemma is_lub_maximal: "S <| x \ x \ S \ S <<| x" - by (erule is_lubI, erule (1) is_ubD) - -lemma lub_maximal: "S <| x \ x \ S \ lub S = x" - by (rule is_lub_maximal [THEN lub_eqI]) - - -subsection \Countable chains\ - -definition chain :: "(nat \ 'a) \ bool" - where \ \Here we use countable chains and I prefer to code them as functions!\ - "chain Y = (\i. Y i \ Y (Suc i))" - -lemma chainI: "(\i. Y i \ Y (Suc i)) \ chain Y" - unfolding chain_def by fast - -lemma chainE: "chain Y \ Y i \ Y (Suc i)" - unfolding chain_def by fast - -text \chains are monotone functions\ - -lemma chain_mono_less: "chain Y \ i < j \ Y i \ Y j" - by (erule less_Suc_induct, erule chainE, erule below_trans) - -lemma chain_mono: "chain Y \ i \ j \ Y i \ Y j" - by (cases "i = j") (simp_all add: chain_mono_less) - -lemma chain_shift: "chain Y \ chain (\i. Y (i + j))" - by (rule chainI, simp, erule chainE) - -text \technical lemmas about (least) upper bounds of chains\ - -lemma is_lub_rangeD1: "range S <<| x \ S i \ x" - by (rule is_lubD1 [THEN ub_rangeD]) - -lemma is_ub_range_shift: "chain S \ range (\i. S (i + j)) <| x = range S <| x" - apply (rule iffI) - apply (rule ub_rangeI) - apply (rule_tac y="S (i + j)" in below_trans) - apply (erule chain_mono) - apply (rule le_add1) - apply (erule ub_rangeD) - apply (rule ub_rangeI) - apply (erule ub_rangeD) - done - -lemma is_lub_range_shift: "chain S \ range (\i. S (i + j)) <<| x = range S <<| x" - by (simp add: is_lub_def is_ub_range_shift) - -text \the lub of a constant chain is the constant\ - -lemma chain_const [simp]: "chain (\i. c)" - by (simp add: chainI) - -lemma is_lub_const: "range (\x. c) <<| c" -by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) - -lemma lub_const [simp]: "(\i. c) = c" - by (rule is_lub_const [THEN lub_eqI]) - - -subsection \Finite chains\ - -definition max_in_chain :: "nat \ (nat \ 'a) \ bool" - where \ \finite chains, needed for monotony of continuous functions\ - "max_in_chain i C \ (\j. i \ j \ C i = C j)" - -definition finite_chain :: "(nat \ 'a) \ bool" - where "finite_chain C = (chain C \ (\i. max_in_chain i C))" - -text \results about finite chains\ - -lemma max_in_chainI: "(\j. i \ j \ Y i = Y j) \ max_in_chain i Y" - unfolding max_in_chain_def by fast - -lemma max_in_chainD: "max_in_chain i Y \ i \ j \ Y i = Y j" - unfolding max_in_chain_def by fast - -lemma finite_chainI: "chain C \ max_in_chain i C \ finite_chain C" - unfolding finite_chain_def by fast - -lemma finite_chainE: "\finite_chain C; \i. \chain C; max_in_chain i C\ \ R\ \ R" - unfolding finite_chain_def by fast - -lemma lub_finch1: "chain C \ max_in_chain i C \ range C <<| C i" - apply (rule is_lubI) - apply (rule ub_rangeI, rename_tac j) - apply (rule_tac x=i and y=j in linorder_le_cases) - apply (drule (1) max_in_chainD, simp) - apply (erule (1) chain_mono) - apply (erule ub_rangeD) - done - -lemma lub_finch2: "finite_chain C \ range C <<| C (LEAST i. max_in_chain i C)" - apply (erule finite_chainE) - apply (erule LeastI2 [where Q="\i. range C <<| C i"]) - apply (erule (1) lub_finch1) - done - -lemma finch_imp_finite_range: "finite_chain Y \ finite (range Y)" - apply (erule finite_chainE) - apply (rule_tac B="Y ` {..i}" in finite_subset) - apply (rule subsetI) - apply (erule rangeE, rename_tac j) - apply (rule_tac x=i and y=j in linorder_le_cases) - apply (subgoal_tac "Y j = Y i", simp) - apply (simp add: max_in_chain_def) - apply simp - apply simp - done - -lemma finite_range_has_max: - fixes f :: "nat \ 'a" - and r :: "'a \ 'a \ bool" - assumes mono: "\i j. i \ j \ r (f i) (f j)" - assumes finite_range: "finite (range f)" - shows "\k. \i. r (f i) (f k)" -proof (intro exI allI) - fix i :: nat - let ?j = "LEAST k. f k = f i" - let ?k = "Max ((\x. LEAST k. f k = x) ` range f)" - have "?j \ ?k" - proof (rule Max_ge) - show "finite ((\x. LEAST k. f k = x) ` range f)" - using finite_range by (rule finite_imageI) - show "?j \ (\x. LEAST k. f k = x) ` range f" - by (intro imageI rangeI) - qed - hence "r (f ?j) (f ?k)" - by (rule mono) - also have "f ?j = f i" - by (rule LeastI, rule refl) - finally show "r (f i) (f ?k)" . -qed - -lemma finite_range_imp_finch: "chain Y \ finite (range Y) \ finite_chain Y" - apply (subgoal_tac "\k. \i. Y i \ Y k") - apply (erule exE) - apply (rule finite_chainI, assumption) - apply (rule max_in_chainI) - apply (rule below_antisym) - apply (erule (1) chain_mono) - apply (erule spec) - apply (rule finite_range_has_max) - apply (erule (1) chain_mono) - apply assumption - done - -lemma bin_chain: "x \ y \ chain (\i. if i=0 then x else y)" - by (rule chainI) simp - -lemma bin_chainmax: "x \ y \ max_in_chain (Suc 0) (\i. if i=0 then x else y)" - by (simp add: max_in_chain_def) - -lemma is_lub_bin_chain: "x \ y \ range (\i::nat. if i=0 then x else y) <<| y" - apply (frule bin_chain) - apply (drule bin_chainmax) - apply (drule (1) lub_finch1) - apply simp - done - -text \the maximal element in a chain is its lub\ - -lemma lub_chain_maxelem: "Y i = c \ \i. Y i \ c \ lub (range Y) = c" - by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI) - -end - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Powerdomains.thy --- a/src/HOL/HOLCF/Powerdomains.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Powerdomains.thy Wed Dec 11 13:44:35 2024 +0100 @@ -31,6 +31,7 @@ unfolding convex_emb_def convex_prj_def by (simp add: ep_pair_udom approx_chain_convex_map) + subsection \Deflation combinators\ definition upper_defl :: "udom defl \ udom defl" @@ -57,6 +58,7 @@ using ep_pair_convex finite_deflation_convex_map unfolding convex_defl_def by (rule cast_defl_fun1) + subsection \Domain class instances\ instantiation upper_pd :: ("domain") "domain" @@ -167,6 +169,7 @@ lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\DEFL('a)" by (rule defl_convex_pd_def) + subsection \Isomorphic deflations\ lemma isodefl_upper: @@ -193,6 +196,7 @@ apply (simp add: convex_map_map) done + subsection \Domain package setup for powerdomains\ lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Product_Cpo.thy --- a/src/HOL/HOLCF/Product_Cpo.thy Wed Dec 11 13:44:16 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,304 +0,0 @@ -(* Title: HOL/HOLCF/Product_Cpo.thy - Author: Franz Regensburger -*) - -section \The cpo of cartesian products\ - -theory Product_Cpo - imports Adm -begin - -default_sort cpo - - -subsection \Unit type is a pcpo\ - -instantiation unit :: discrete_cpo -begin - -definition below_unit_def [simp]: "x \ (y::unit) \ True" - -instance - by standard simp - -end - -instance unit :: pcpo - by standard simp - - -subsection \Product type is a partial order\ - -instantiation prod :: (below, below) below -begin - -definition below_prod_def: "(\) \ \p1 p2. (fst p1 \ fst p2 \ snd p1 \ snd p2)" - -instance .. - -end - -instance prod :: (po, po) po -proof - fix x :: "'a \ 'b" - show "x \ x" - by (simp add: below_prod_def) -next - fix x y :: "'a \ 'b" - assume "x \ y" "y \ x" - then show "x = y" - unfolding below_prod_def prod_eq_iff - by (fast intro: below_antisym) -next - fix x y z :: "'a \ 'b" - assume "x \ y" "y \ z" - then show "x \ z" - unfolding below_prod_def - by (fast intro: below_trans) -qed - - -subsection \Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\ - -lemma prod_belowI: "fst p \ fst q \ snd p \ snd q \ p \ q" - by (simp add: below_prod_def) - -lemma Pair_below_iff [simp]: "(a, b) \ (c, d) \ a \ c \ b \ d" - by (simp add: below_prod_def) - -text \Pair \(_,_)\ is monotone in both arguments\ - -lemma monofun_pair1: "monofun (\x. (x, y))" - by (simp add: monofun_def) - -lemma monofun_pair2: "monofun (\y. (x, y))" - by (simp add: monofun_def) - -lemma monofun_pair: "x1 \ x2 \ y1 \ y2 \ (x1, y1) \ (x2, y2)" - by simp - -lemma ch2ch_Pair [simp]: "chain X \ chain Y \ chain (\i. (X i, Y i))" - by (rule chainI, simp add: chainE) - -text \\<^term>\fst\ and \<^term>\snd\ are monotone\ - -lemma fst_monofun: "x \ y \ fst x \ fst y" - by (simp add: below_prod_def) - -lemma snd_monofun: "x \ y \ snd x \ snd y" - by (simp add: below_prod_def) - -lemma monofun_fst: "monofun fst" - by (simp add: monofun_def below_prod_def) - -lemma monofun_snd: "monofun snd" - by (simp add: monofun_def below_prod_def) - -lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst] - -lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd] - -lemma prod_chain_cases: - assumes chain: "chain Y" - obtains A B - where "chain A" and "chain B" and "Y = (\i. (A i, B i))" -proof - from chain show "chain (\i. fst (Y i))" - by (rule ch2ch_fst) - from chain show "chain (\i. snd (Y i))" - by (rule ch2ch_snd) - show "Y = (\i. (fst (Y i), snd (Y i)))" - by simp -qed - - -subsection \Product type is a cpo\ - -lemma is_lub_Pair: "range A <<| x \ range B <<| y \ range (\i. (A i, B i)) <<| (x, y)" - by (simp add: is_lub_def is_ub_def below_prod_def) - -lemma lub_Pair: "chain A \ chain B \ (\i. (A i, B i)) = (\i. A i, \i. B i)" - for A :: "nat \ 'a::cpo" and B :: "nat \ 'b::cpo" - by (fast intro: lub_eqI is_lub_Pair elim: thelubE) - -lemma is_lub_prod: - fixes S :: "nat \ ('a::cpo \ 'b::cpo)" - assumes "chain S" - shows "range S <<| (\i. fst (S i), \i. snd (S i))" - using assms by (auto elim: prod_chain_cases simp: is_lub_Pair cpo_lubI) - -lemma lub_prod: "chain S \ (\i. S i) = (\i. fst (S i), \i. snd (S i))" - for S :: "nat \ 'a::cpo \ 'b::cpo" - by (rule is_lub_prod [THEN lub_eqI]) - -instance prod :: (cpo, cpo) cpo -proof - fix S :: "nat \ ('a \ 'b)" - assume "chain S" - then have "range S <<| (\i. fst (S i), \i. snd (S i))" - by (rule is_lub_prod) - then show "\x. range S <<| x" .. -qed - -instance prod :: (discrete_cpo, discrete_cpo) discrete_cpo -proof - fix x y :: "'a \ 'b" - show "x \ y \ x = y" - by (simp add: below_prod_def prod_eq_iff) -qed - - -subsection \Product type is pointed\ - -lemma minimal_prod: "(\, \) \ p" - by (simp add: below_prod_def) - -instance prod :: (pcpo, pcpo) pcpo - by intro_classes (fast intro: minimal_prod) - -lemma inst_prod_pcpo: "\ = (\, \)" - by (rule minimal_prod [THEN bottomI, symmetric]) - -lemma Pair_bottom_iff [simp]: "(x, y) = \ \ x = \ \ y = \" - by (simp add: inst_prod_pcpo) - -lemma fst_strict [simp]: "fst \ = \" - unfolding inst_prod_pcpo by (rule fst_conv) - -lemma snd_strict [simp]: "snd \ = \" - unfolding inst_prod_pcpo by (rule snd_conv) - -lemma Pair_strict [simp]: "(\, \) = \" - by simp - -lemma split_strict [simp]: "case_prod f \ = f \ \" - by (simp add: split_def) - - -subsection \Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\ - -lemma cont_pair1: "cont (\x. (x, y))" - apply (rule contI) - apply (rule is_lub_Pair) - apply (erule cpo_lubI) - apply (rule is_lub_const) - done - -lemma cont_pair2: "cont (\y. (x, y))" - apply (rule contI) - apply (rule is_lub_Pair) - apply (rule is_lub_const) - apply (erule cpo_lubI) - done - -lemma cont_fst: "cont fst" - apply (rule contI) - apply (simp add: lub_prod) - apply (erule cpo_lubI [OF ch2ch_fst]) - done - -lemma cont_snd: "cont snd" - apply (rule contI) - apply (simp add: lub_prod) - apply (erule cpo_lubI [OF ch2ch_snd]) - done - -lemma cont2cont_Pair [simp, cont2cont]: - assumes f: "cont (\x. f x)" - assumes g: "cont (\x. g x)" - shows "cont (\x. (f x, g x))" - apply (rule cont_apply [OF f cont_pair1]) - apply (rule cont_apply [OF g cont_pair2]) - apply (rule cont_const) - done - -lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst] - -lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd] - -lemma cont2cont_case_prod: - assumes f1: "\a b. cont (\x. f x a b)" - assumes f2: "\x b. cont (\a. f x a b)" - assumes f3: "\x a. cont (\b. f x a b)" - assumes g: "cont (\x. g x)" - shows "cont (\x. case g x of (a, b) \ f x a b)" - unfolding split_def - apply (rule cont_apply [OF g]) - apply (rule cont_apply [OF cont_fst f2]) - apply (rule cont_apply [OF cont_snd f3]) - apply (rule cont_const) - apply (rule f1) - done - -lemma prod_contI: - assumes f1: "\y. cont (\x. f (x, y))" - assumes f2: "\x. cont (\y. f (x, y))" - shows "cont f" -proof - - have "cont (\(x, y). f (x, y))" - by (intro cont2cont_case_prod f1 f2 cont2cont) - then show "cont f" - by (simp only: case_prod_eta) -qed - -lemma prod_cont_iff: "cont f \ (\y. cont (\x. f (x, y))) \ (\x. cont (\y. f (x, y)))" - apply safe - apply (erule cont_compose [OF _ cont_pair1]) - apply (erule cont_compose [OF _ cont_pair2]) - apply (simp only: prod_contI) - done - -lemma cont2cont_case_prod' [simp, cont2cont]: - assumes f: "cont (\p. f (fst p) (fst (snd p)) (snd (snd p)))" - assumes g: "cont (\x. g x)" - shows "cont (\x. case_prod (f x) (g x))" - using assms by (simp add: cont2cont_case_prod prod_cont_iff) - -text \The simple version (due to Joachim Breitner) is needed if - either element type of the pair is not a cpo.\ - -lemma cont2cont_split_simple [simp, cont2cont]: - assumes "\a b. cont (\x. f x a b)" - shows "cont (\x. case p of (a, b) \ f x a b)" - using assms by (cases p) auto - -text \Admissibility of predicates on product types.\ - -lemma adm_case_prod [simp]: - assumes "adm (\x. P x (fst (f x)) (snd (f x)))" - shows "adm (\x. case f x of (a, b) \ P x a b)" - unfolding case_prod_beta using assms . - - -subsection \Compactness and chain-finiteness\ - -lemma fst_below_iff: "fst x \ y \ x \ (y, snd x)" - for x :: "'a \ 'b" - by (simp add: below_prod_def) - -lemma snd_below_iff: "snd x \ y \ x \ (fst x, y)" - for x :: "'a \ 'b" - by (simp add: below_prod_def) - -lemma compact_fst: "compact x \ compact (fst x)" - by (rule compactI) (simp add: fst_below_iff) - -lemma compact_snd: "compact x \ compact (snd x)" - by (rule compactI) (simp add: snd_below_iff) - -lemma compact_Pair: "compact x \ compact y \ compact (x, y)" - by (rule compactI) (simp add: below_prod_def) - -lemma compact_Pair_iff [simp]: "compact (x, y) \ compact x \ compact y" - apply (safe intro!: compact_Pair) - apply (drule compact_fst, simp) - apply (drule compact_snd, simp) - done - -instance prod :: (chfin, chfin) chfin - apply intro_classes - apply (erule compact_imp_max_in_chain) - apply (case_tac "\i. Y i", simp) - done - -end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Representable.thy --- a/src/HOL/HOLCF/Representable.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Representable.thy Wed Dec 11 13:44:35 2024 +0100 @@ -10,6 +10,7 @@ default_sort cpo + subsection \Class of representable domains\ text \ @@ -88,6 +89,7 @@ lemmas emb_strict = domain.e_strict lemmas prj_strict = domain.p_strict + subsection \Domains are bifinite\ lemma approx_chain_ep_cast: @@ -126,6 +128,7 @@ instance predomain \ profinite by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl]) + subsection \Universal domain ep-pairs\ definition "u_emb = udom_emb (\i. u_map\(udom_approx i))" @@ -163,6 +166,7 @@ unfolding sfun_emb_def sfun_prj_def by (simp add: ep_pair_udom approx_chain_sfun_map) + subsection \Type combinators\ definition u_defl :: "udom defl \ udom defl" @@ -223,6 +227,7 @@ by (rule cast_eq_imp_eq) (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl) + subsection \Class instance proofs\ subsubsection \Universal domain\ @@ -267,6 +272,7 @@ end + subsubsection \Lifted cpo\ instantiation u :: (predomain) "domain" @@ -304,6 +310,7 @@ lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\LIFTDEFL('a)" by (rule defl_u_def) + subsubsection \Strict function space\ instantiation sfun :: ("domain", "domain") "domain" @@ -342,6 +349,7 @@ "DEFL('a::domain \! 'b::domain) = sfun_defl\DEFL('a)\DEFL('b)" by (rule defl_sfun_def) + subsubsection \Continuous function space\ instantiation cfun :: (predomain, "domain") "domain" @@ -382,6 +390,7 @@ "DEFL('a::predomain \ 'b::domain) = DEFL('a u \! 'b)" by (rule defl_cfun_def) + subsubsection \Strict product\ instantiation sprod :: ("domain", "domain") "domain" @@ -420,6 +429,7 @@ "DEFL('a::domain \ 'b::domain) = sprod_defl\DEFL('a)\DEFL('b)" by (rule defl_sprod_def) + subsubsection \Cartesian product\ definition prod_liftdefl :: "udom u defl \ udom u defl \ udom u defl" @@ -508,6 +518,7 @@ prod_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" by (rule liftdefl_prod_def) + subsubsection \Unit type\ instantiation unit :: "domain" @@ -541,6 +552,7 @@ end + subsubsection \Discrete cpo\ instantiation discr :: (countable) predomain @@ -586,6 +598,7 @@ end + subsubsection \Strict sum\ instantiation ssum :: ("domain", "domain") "domain" @@ -624,6 +637,7 @@ "DEFL('a::domain \ 'b::domain) = ssum_defl\DEFL('a)\DEFL('b)" by (rule defl_ssum_def) + subsubsection \Lifted HOL type\ instantiation lift :: (countable) "domain" diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/Universal.thy --- a/src/HOL/HOLCF/Universal.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/Universal.thy Wed Dec 11 13:44:35 2024 +0100 @@ -8,7 +8,8 @@ imports Bifinite Completion "HOL-Library.Nat_Bijection" begin -no_notation binomial (infix \choose\ 64) +unbundle no binomial_syntax + subsection \Basis for universal domain\ @@ -79,6 +80,7 @@ apply (simp add: 2 node_gt1 node_gt2) done + subsubsection \Basis ordering\ inductive @@ -105,6 +107,7 @@ apply (erule (1) ubasis_le_trans) done + subsubsection \Generic take function\ function @@ -275,6 +278,7 @@ approx_chain approx for approx :: "nat \ 'a::bifinite \ 'a" begin + subsubsection \Choosing a maximal element from a finite set\ lemma finite_has_maximal: @@ -389,6 +393,7 @@ apply (simp add: choose_pos.simps) done + subsubsection \Compact basis take function\ primrec @@ -443,6 +448,7 @@ apply (rule inj_onI, simp add: Rep_compact_basis_inject) done + subsubsection \Rank of basis elements\ definition @@ -522,6 +528,7 @@ lemma rank_lt_Un_rank_eq: "rank_lt x \ rank_eq x = rank_le x" unfolding rank_lt_def rank_eq_def rank_le_def by auto + subsubsection \Sequencing basis elements\ definition @@ -571,6 +578,7 @@ lemma inj_place: "inj place" by (rule inj_onI, erule place_eqD) + subsubsection \Embedding and projection on basis elements\ definition @@ -831,6 +839,7 @@ by (rule bifinite_approx_chain.ideal_completion) qed + subsubsection \EP-pair from any bifinite domain into \emph{udom}\ context bifinite_approx_chain begin @@ -879,6 +888,7 @@ lemmas ep_pair_udom = bifinite_approx_chain.ep_pair_udom [unfolded bifinite_approx_chain_def] + subsection \Chain of approx functions for type \emph{udom}\ definition @@ -973,6 +983,6 @@ hide_const (open) node -notation binomial (infixl \choose\ 65) +unbundle binomial_syntax end diff -r 1c2a68bb0ff1 -r ecd675295620 src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Wed Dec 11 13:44:16 2024 +0100 +++ b/src/HOL/HOLCF/UpperPD.thy Wed Dec 11 13:44:35 2024 +0100 @@ -452,6 +452,7 @@ by (rule finite_range_imp_finite_fixes) qed + subsection \Upper powerdomain is bifinite\ lemma approx_chain_upper_map: @@ -467,6 +468,7 @@ by (fast intro!: approx_chain_upper_map) qed + subsection \Join\ definition diff -r 1c2a68bb0ff1 -r ecd675295620 src/Pure/Admin/component_cvc5.scala --- a/src/Pure/Admin/component_cvc5.scala Wed Dec 11 13:44:16 2024 +0100 +++ b/src/Pure/Admin/component_cvc5.scala Wed Dec 11 13:44:35 2024 +0100 @@ -19,17 +19,17 @@ val platforms: List[Download_Platform] = List( - Download_Platform("arm64-darwin", "cvc5-macOS-arm64-static-2024-03-20-ef2bc3f.zip"), - Download_Platform("arm64-linux", "cvc5-Linux-arm64-static-2024-03-20-ef2bc3f.zip"), - Download_Platform("x86_64-darwin", "cvc5-macOS-static-2024-03-20-ef2bc3f.zip"), - Download_Platform("x86_64-linux", "cvc5-Linux-static-2024-03-20-ef2bc3f.zip"), - Download_Platform("x86_64-windows", "cvc5-Win64-static-2024-03-20-ef2bc3f.zip")) + Download_Platform("arm64-darwin", "cvc5-macOS-arm64-static.zip"), + Download_Platform("arm64-linux", "cvc5-Linux-arm64-static.zip"), + Download_Platform("x86_64-darwin", "cvc5-macOS-x86_64-static.zip"), + Download_Platform("x86_64-linux", "cvc5-Linux-x86_64-static.zip"), + Download_Platform("x86_64-windows", "cvc5-Win64-x86_64-static.zip")) /* build cvc5 */ val default_url = "https://github.com/cvc5/cvc5/releases/download" - val default_version = "latest" + val default_version = "1.2.0" def build_cvc5( base_url: String = default_url, @@ -48,7 +48,7 @@ for (platform <- platforms) { Isabelle_System.with_tmp_dir("download") { download_dir => - val download = base_url + "/" + version + "/" + platform.download_name + val download = base_url + "/cvc5-" + version + "/" + platform.download_name val archive_name = Url.get_base_name(platform.download_name) getOrElse @@ -86,11 +86,9 @@ /* README */ File.write(component_dir.README, - """This distribution of cvc5 was assembled from official downloads -from """ + base_url + """ for macOS, Linux, -and Windows, with ARM64 support on macOS and Linux. - -The change id is ef2bc3f735df (3 weeks after cvc5-1.1.2). + """This distribution of cvc5 was assembled from official downloads from +""" + base_url + """ --- the static.zip variants +for macOS, Linux, and Windows, with ARM64 support on macOS and Linux. The downloaded files were renamed and made executable. diff -r 1c2a68bb0ff1 -r ecd675295620 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Dec 11 13:44:16 2024 +0100 +++ b/src/Pure/ROOT.ML Wed Dec 11 13:44:35 2024 +0100 @@ -373,4 +373,3 @@ ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML"; - diff -r 1c2a68bb0ff1 -r ecd675295620 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Dec 11 13:44:16 2024 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Dec 11 13:44:35 2024 +0100 @@ -877,8 +877,8 @@ (case asts of [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] => let - val (c', _) = decode_const ctxt (c, map #pos (Term_Position.decode p)); - val d = if intern then Lexicon.mark_const c' else c; + val (c', reports) = decode_const ctxt (c, map #pos (Term_Position.decode p)); + val d = if intern then (Context_Position.reports ctxt reports; Lexicon.mark_const c') else c; in Ast.constrain (Ast.Constant d) T end | _ => raise Ast.AST ("const_ast_tr", asts)); diff -r 1c2a68bb0ff1 -r ecd675295620 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Wed Dec 11 13:44:16 2024 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Dec 11 13:44:35 2024 +0100 @@ -365,12 +365,14 @@ def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] = { // coordinates wrt. inner painter component val painter = text_area.getPainter + val buffer = text_area.getBuffer if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) { val offset = text_area.xyToOffset(x, y, false) if (offset >= 0) { - val range = point_range(text_area.getBuffer, offset) + val range = point_range(buffer, offset) gfx_range(text_area)(range) match { - case Some(g) if g.x <= x && x < g.x + g.length => Some(range) + case Some(g) if g.x <= x && x < g.x + g.length => + range.try_restrict(buffer_range(buffer)) case _ => None } }