# HG changeset patch # User wenzelm # Date 1514844444 -3600 # Node ID 0d25e02759b744d1a146deb49c41582cf3038e89 # Parent 3869b2400e221def1f553f367b7d894294126369 misc tuning and modernization; diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Adm.thy --- a/src/HOL/HOLCF/Adm.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Adm.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,53 +5,51 @@ section \Admissibility and compactness\ theory Adm -imports Cont + 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))" +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 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 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 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) + 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::'a::chfin \ bool)" -by (rule admI, frule chfin, auto simp add: maxinch_is_thelub) +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) + 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_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_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) +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.\ @@ -68,14 +66,14 @@ apply (rule chain_mono [OF chain]) apply (rule Least_le) apply (rule LeastI2_ex) - apply (simp_all add: P) + 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_mono [OF chain chain']) + apply (rule chain_mono [OF chain f1]) apply (rule lub_range_mono [OF _ chain chain']) apply clarsimp done @@ -83,107 +81,95 @@ 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_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_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_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) +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_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_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_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) + 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)" +definition compact :: "'a::cpo \ bool" + where "compact k = adm (\x. k \ x)" lemma compactI: "adm (\x. k \ x) \ compact k" -unfolding compact_def . + unfolding compact_def . lemma compactD: "compact k \ adm (\x. k \ x)" -unfolding compact_def . + 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 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 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_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::'a::chfin)" -by (rule compactI [OF adm_chfin]) +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 +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) + "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_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 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) + 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) + 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 diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Bifinite.thy --- a/src/HOL/HOLCF/Bifinite.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Bifinite.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,7 +5,7 @@ section \Profinite and bifinite cpos\ theory Bifinite -imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable" + imports Map_Functions Cprod Sprod Sfun Up "HOL-Library.Countable" begin default_sort cpo diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Cfun.thy Mon Jan 01 23:07:24 2018 +0100 @@ -6,17 +6,18 @@ section \The type of continuous functions\ theory Cfun -imports Cpodef Fun_Cpo Product_Cpo + imports Cpodef Fun_Cpo Product_Cpo begin default_sort cpo + subsection \Definition of continuous function type\ -definition "cfun = {f::'a => 'b. cont f}" +definition "cfun = {f::'a \ 'b. cont f}" -cpodef ('a, 'b) cfun ("(_ \/ _)" [1, 0] 0) = "cfun :: ('a => 'b) set" - unfolding cfun_def by (auto intro: cont_const adm_cont) +cpodef ('a, 'b) cfun ("(_ \/ _)" [1, 0] 0) = "cfun :: ('a \ 'b) set" + by (auto simp: cfun_def intro: cont_const adm_cont) type_notation (ASCII) cfun (infixr "->" 0) @@ -78,18 +79,19 @@ text \Dummy patterns for continuous abstraction\ translations - "\ _. t" => "CONST Abs_cfun (\ _. t)" + "\ _. t" \ "CONST Abs_cfun (\_. t)" + subsection \Continuous function space is pointed\ lemma bottom_cfun: "\ \ cfun" -by (simp add: cfun_def inst_fun_pcpo) + by (simp add: cfun_def inst_fun_pcpo) instance cfun :: (cpo, discrete_cpo) discrete_cpo -by intro_classes (simp add: below_cfun_def Rep_cfun_inject) + by intro_classes (simp add: below_cfun_def Rep_cfun_inject) instance cfun :: (cpo, pcpo) pcpo -by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun]) + by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun]) lemmas Rep_cfun_strict = typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun] @@ -100,30 +102,32 @@ text \function application is strict in its first argument\ lemma Rep_cfun_strict1 [simp]: "\\x = \" -by (simp add: Rep_cfun_strict) + by (simp add: Rep_cfun_strict) lemma LAM_strict [simp]: "(\ x. \) = \" -by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict) + by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict) text \for compatibility with old HOLCF-Version\ lemma inst_cfun_pcpo: "\ = (\ x. \)" -by simp + by simp + subsection \Basic properties of continuous functions\ text \Beta-equality for continuous functions\ lemma Abs_cfun_inverse2: "cont f \ Rep_cfun (Abs_cfun f) = f" -by (simp add: Abs_cfun_inverse cfun_def) + by (simp add: Abs_cfun_inverse cfun_def) lemma beta_cfun: "cont f \ (\ x. f x)\u = f u" -by (simp add: Abs_cfun_inverse2) + by (simp add: Abs_cfun_inverse2) -text \Beta-reduction simproc\ + +subsubsection \Beta-reduction simproc\ text \ Given the term @{term "(\ x. f x)\y"}, the procedure tries to - construct the theorem @{term "(\ x. f x)\y == f y"}. If this + construct the theorem @{term "(\ x. f x)\y \ f y"}. If this theorem cannot be completely solved by the cont2cont rules, then the procedure returns the ordinary conditional \beta_cfun\ rule. @@ -140,12 +144,10 @@ simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \ fn phi => fn ctxt => fn ct => let - val dest = Thm.dest_comb; - val f = (snd o dest o snd o dest) ct; + val f = #2 (Thm.dest_comb (#2 (Thm.dest_comb ct))); val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f); - val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] - (mk_meta_eq @{thm Abs_cfun_inverse2}); - val rules = Named_Theorems.get ctxt @{named_theorems cont2cont}; + val tr = Thm.instantiate' [SOME T, SOME U] [SOME f] (mk_meta_eq @{thm Abs_cfun_inverse2}); + val rules = Named_Theorems.get ctxt \<^named_theorems>\cont2cont\; val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules))); in SOME (perhaps (SINGLE (tac 1)) tr) end \ @@ -153,44 +155,43 @@ text \Eta-equality for continuous functions\ lemma eta_cfun: "(\ x. f\x) = f" -by (rule Rep_cfun_inverse) + by (rule Rep_cfun_inverse) text \Extensionality for continuous functions\ lemma cfun_eq_iff: "f = g \ (\x. f\x = g\x)" -by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff) + by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff) lemma cfun_eqI: "(\x. f\x = g\x) \ f = g" -by (simp add: cfun_eq_iff) + by (simp add: cfun_eq_iff) text \Extensionality wrt. ordering for continuous functions\ -lemma cfun_below_iff: "f \ g \ (\x. f\x \ g\x)" -by (simp add: below_cfun_def fun_below_iff) +lemma cfun_below_iff: "f \ g \ (\x. f\x \ g\x)" + by (simp add: below_cfun_def fun_below_iff) lemma cfun_belowI: "(\x. f\x \ g\x) \ f \ g" -by (simp add: cfun_below_iff) + by (simp add: cfun_below_iff) text \Congruence for continuous function application\ -lemma cfun_cong: "\f = g; x = y\ \ f\x = g\y" -by simp +lemma cfun_cong: "f = g \ x = y \ f\x = g\y" + by simp lemma cfun_fun_cong: "f = g \ f\x = g\x" -by simp + by simp lemma cfun_arg_cong: "x = y \ f\x = f\y" -by simp + by simp + subsection \Continuity of application\ lemma cont_Rep_cfun1: "cont (\f. f\x)" -by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun]) + by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun]) lemma cont_Rep_cfun2: "cont (\x. f\x)" -apply (cut_tac x=f in Rep_cfun) -apply (simp add: cfun_def) -done + using Rep_cfun [where x = f] by (simp add: cfun_def) lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono] @@ -200,66 +201,66 @@ text \contlub, cont properties of @{term Rep_cfun} in each argument\ lemma contlub_cfun_arg: "chain Y \ f\(\i. Y i) = (\i. f\(Y i))" -by (rule cont_Rep_cfun2 [THEN cont2contlubE]) + by (rule cont_Rep_cfun2 [THEN cont2contlubE]) lemma contlub_cfun_fun: "chain F \ (\i. F i)\x = (\i. F i\x)" -by (rule cont_Rep_cfun1 [THEN cont2contlubE]) + by (rule cont_Rep_cfun1 [THEN cont2contlubE]) text \monotonicity of application\ lemma monofun_cfun_fun: "f \ g \ f\x \ g\x" -by (simp add: cfun_below_iff) + by (simp add: cfun_below_iff) lemma monofun_cfun_arg: "x \ y \ f\x \ f\y" -by (rule monofun_Rep_cfun2 [THEN monofunE]) + by (rule monofun_Rep_cfun2 [THEN monofunE]) -lemma monofun_cfun: "\f \ g; x \ y\ \ f\x \ g\y" -by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg]) +lemma monofun_cfun: "f \ g \ x \ y \ f\x \ g\y" + by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg]) -text \ch2ch - rules for the type @{typ "'a -> 'b"}\ +text \ch2ch - rules for the type @{typ "'a \ 'b"}\ lemma chain_monofun: "chain Y \ chain (\i. f\(Y i))" -by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun]) + by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun]) lemma ch2ch_Rep_cfunR: "chain Y \ chain (\i. f\(Y i))" -by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun]) + by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun]) lemma ch2ch_Rep_cfunL: "chain F \ chain (\i. (F i)\x)" -by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun]) + by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun]) -lemma ch2ch_Rep_cfun [simp]: - "\chain F; chain Y\ \ chain (\i. (F i)\(Y i))" -by (simp add: chain_def monofun_cfun) +lemma ch2ch_Rep_cfun [simp]: "chain F \ chain Y \ chain (\i. (F i)\(Y i))" + by (simp add: chain_def monofun_cfun) lemma ch2ch_LAM [simp]: - "\\x. chain (\i. S i x); \i. cont (\x. S i x)\ \ chain (\i. \ x. S i x)" -by (simp add: chain_def cfun_below_iff) + "(\x. chain (\i. S i x)) \ (\i. cont (\x. S i x)) \ chain (\i. \ x. S i x)" + by (simp add: chain_def cfun_below_iff) text \contlub, cont properties of @{term Rep_cfun} in both arguments\ -lemma lub_APP: - "\chain F; chain Y\ \ (\i. F i\(Y i)) = (\i. F i)\(\i. Y i)" -by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub) +lemma lub_APP: "chain F \ chain Y \ (\i. F i\(Y i)) = (\i. F i)\(\i. Y i)" + by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub) lemma lub_LAM: - "\\x. chain (\i. F i x); \i. cont (\x. F i x)\ - \ (\i. \ x. F i x) = (\ x. \i. F i x)" -by (simp add: lub_cfun lub_fun ch2ch_lambda) + assumes "\x. chain (\i. F i x)" + and "\i. cont (\x. F i x)" + shows "(\i. \ x. F i x) = (\ x. \i. F i x)" + using assms by (simp add: lub_cfun lub_fun ch2ch_lambda) lemmas lub_distribs = lub_APP lub_LAM text \strictness\ lemma strictI: "f\x = \ \ f\\ = \" -apply (rule bottomI) -apply (erule subst) -apply (rule minimal [THEN monofun_cfun_arg]) -done + apply (rule bottomI) + apply (erule subst) + apply (rule minimal [THEN monofun_cfun_arg]) + done -text \type @{typ "'a -> 'b"} is chain complete\ +text \type @{typ "'a \ 'b"} is chain complete\ lemma lub_cfun: "chain F \ (\i. F i) = (\ x. \i. F i\x)" -by (simp add: lub_cfun lub_fun ch2ch_lambda) + by (simp add: lub_cfun lub_fun ch2ch_lambda) + subsection \Continuity simplification procedure\ @@ -270,10 +271,10 @@ assumes t: "cont (\x. t x)" shows "cont (\x. (f x)\(t x))" proof - - have 1: "\y. cont (\x. (f x)\y)" - using cont_Rep_cfun1 f by (rule cont_compose) - show "cont (\x. (f x)\(t x))" - using t cont_Rep_cfun2 1 by (rule cont_apply) + from cont_Rep_cfun1 f have "cont (\x. (f x)\y)" for y + by (rule cont_compose) + with t cont_Rep_cfun2 show "cont (\x. (f x)\(t x))" + by (rule cont_apply) qed text \ @@ -281,21 +282,21 @@ These lemmas are needed in theories that use types like @{typ "'a \ 'b \ 'c"}. \ -lemma cont_APP_app [simp]: "\cont f; cont g\ \ cont (\x. ((f x)\(g x)) s)" -by (rule cont2cont_APP [THEN cont2cont_fun]) +lemma cont_APP_app [simp]: "cont f \ cont g \ cont (\x. ((f x)\(g x)) s)" + by (rule cont2cont_APP [THEN cont2cont_fun]) -lemma cont_APP_app_app [simp]: "\cont f; cont g\ \ cont (\x. ((f x)\(g x)) s t)" -by (rule cont_APP_app [THEN cont2cont_fun]) +lemma cont_APP_app_app [simp]: "cont f \ cont g \ cont (\x. ((f x)\(g x)) s t)" + by (rule cont_APP_app [THEN cont2cont_fun]) -text \cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"}\ +text \cont2mono Lemma for @{term "\x. LAM y. c1(x)(y)"}\ lemma cont2mono_LAM: "\\x. cont (\y. f x y); \y. monofun (\x. f x y)\ \ monofun (\x. \ y. f x y)" - unfolding monofun_def cfun_below_iff by simp + by (simp add: monofun_def cfun_below_iff) -text \cont2cont Lemma for @{term "%x. LAM y. f x y"}\ +text \cont2cont Lemma for @{term "\x. LAM y. f x y"}\ text \ Not suitable as a cont2cont rule, because on nested lambdas @@ -307,9 +308,10 @@ assumes f2: "\y. cont (\x. f x y)" shows "cont (\x. \ y. f x y)" proof (rule cont_Abs_cfun) - fix x - from f1 show "f x \ cfun" by (simp add: cfun_def) - from f2 show "cont f" by (rule cont2cont_lambda) + from f1 show "f x \ cfun" for x + by (simp add: cfun_def) + from f2 show "cont f" + by (rule cont2cont_lambda) qed text \ @@ -321,176 +323,173 @@ fixes f :: "'a::cpo \ 'b::cpo \ 'c::cpo" assumes f: "cont (\p. f (fst p) (snd p))" shows "cont (\x. \ y. f x y)" -using assms by (simp add: cont2cont_LAM prod_cont_iff) + using assms by (simp add: cont2cont_LAM prod_cont_iff) lemma cont2cont_LAM_discrete [simp, cont2cont]: "(\y::'a::discrete_cpo. cont (\x. f x y)) \ cont (\x. \ y. f x y)" -by (simp add: cont2cont_LAM) + by (simp add: cont2cont_LAM) + subsection \Miscellaneous\ text \Monotonicity of @{term Abs_cfun}\ -lemma monofun_LAM: - "\cont f; cont g; \x. f x \ g x\ \ (\ x. f x) \ (\ x. g x)" -by (simp add: cfun_below_iff) +lemma monofun_LAM: "cont f \ cont g \ (\x. f x \ g x) \ (\ x. f x) \ (\ x. g x)" + by (simp add: cfun_below_iff) text \some lemmata for functions with flat/chfin domain/range types\ -lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin) - ==> !s. ? n. (LUB i. Y i)\s = Y n\s" -apply (rule allI) -apply (subst contlub_cfun_fun) -apply assumption -apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL) -done +lemma chfin_Rep_cfunR: "chain Y \ \s. \n. (LUB i. Y i)\s = Y n\s" + for Y :: "nat \ 'a::cpo \ 'b::chfin" + apply (rule allI) + apply (subst contlub_cfun_fun) + apply assumption + apply (fast intro!: lub_eqI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL) + done lemma adm_chfindom: "adm (\(u::'a::cpo \ 'b::chfin). P(u\s))" -by (rule adm_subst, simp, rule adm_chfin) + by (rule adm_subst, simp, rule adm_chfin) + subsection \Continuous injection-retraction pairs\ text \Continuous retractions are strict.\ -lemma retraction_strict: - "\x. f\(g\x) = x \ f\\ = \" -apply (rule bottomI) -apply (drule_tac x="\" in spec) -apply (erule subst) -apply (rule monofun_cfun_arg) -apply (rule minimal) -done +lemma retraction_strict: "\x. f\(g\x) = x \ f\\ = \" + apply (rule bottomI) + apply (drule_tac x="\" in spec) + apply (erule subst) + apply (rule monofun_cfun_arg) + apply (rule minimal) + done -lemma injection_eq: - "\x. f\(g\x) = x \ (g\x = g\y) = (x = y)" -apply (rule iffI) -apply (drule_tac f=f in cfun_arg_cong) -apply simp -apply simp -done +lemma injection_eq: "\x. f\(g\x) = x \ (g\x = g\y) = (x = y)" + apply (rule iffI) + apply (drule_tac f=f in cfun_arg_cong) + apply simp + apply simp + done -lemma injection_below: - "\x. f\(g\x) = x \ (g\x \ g\y) = (x \ y)" -apply (rule iffI) -apply (drule_tac f=f in monofun_cfun_arg) -apply simp -apply (erule monofun_cfun_arg) -done +lemma injection_below: "\x. f\(g\x) = x \ (g\x \ g\y) = (x \ y)" + apply (rule iffI) + apply (drule_tac f=f in monofun_cfun_arg) + apply simp + apply (erule monofun_cfun_arg) + done -lemma injection_defined_rev: - "\\x. f\(g\x) = x; g\z = \\ \ z = \" -apply (drule_tac f=f in cfun_arg_cong) -apply (simp add: retraction_strict) -done +lemma injection_defined_rev: "\x. f\(g\x) = x \ g\z = \ \ z = \" + apply (drule_tac f=f in cfun_arg_cong) + apply (simp add: retraction_strict) + done -lemma injection_defined: - "\\x. f\(g\x) = x; z \ \\ \ g\z \ \" -by (erule contrapos_nn, rule injection_defined_rev) +lemma injection_defined: "\x. f\(g\x) = x \ z \ \ \ g\z \ \" + by (erule contrapos_nn, rule injection_defined_rev) + text \a result about functions with flat codomain\ -lemma flat_eqI: "\(x::'a::flat) \ y; x \ \\ \ x = y" -by (drule ax_flat, simp) +lemma flat_eqI: "x \ y \ x \ \ \ x = y" + for x y :: "'a::flat" + by (drule ax_flat) simp -lemma flat_codom: - "f\x = (c::'b::flat) \ f\\ = \ \ (\z. f\z = c)" -apply (case_tac "f\x = \") -apply (rule disjI1) -apply (rule bottomI) -apply (erule_tac t="\" in subst) -apply (rule minimal [THEN monofun_cfun_arg]) -apply clarify -apply (rule_tac a = "f\\" in refl [THEN box_equals]) -apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI]) -apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI]) -done +lemma flat_codom: "f\x = c \ f\\ = \ \ (\z. f\z = c)" + for c :: "'b::flat" + apply (case_tac "f\x = \") + apply (rule disjI1) + apply (rule bottomI) + apply (erule_tac t="\" in subst) + apply (rule minimal [THEN monofun_cfun_arg]) + apply clarify + apply (rule_tac a = "f\\" in refl [THEN box_equals]) + apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI]) + apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI]) + done + subsection \Identity and composition\ -definition - ID :: "'a \ 'a" where - "ID = (\ x. x)" +definition ID :: "'a \ 'a" + where "ID = (\ x. x)" -definition - cfcomp :: "('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" where - oo_def: "cfcomp = (\ f g x. f\(g\x))" +definition cfcomp :: "('b \ 'c) \ ('a \ 'b) \ 'a \ 'c" + where oo_def: "cfcomp = (\ f g x. f\(g\x))" -abbreviation - cfcomp_syn :: "['b \ 'c, 'a \ 'b] \ 'a \ 'c" (infixr "oo" 100) where - "f oo g == cfcomp\f\g" +abbreviation cfcomp_syn :: "['b \ 'c, 'a \ 'b] \ 'a \ 'c" (infixr "oo" 100) + where "f oo g == cfcomp\f\g" lemma ID1 [simp]: "ID\x = x" -by (simp add: ID_def) + by (simp add: ID_def) lemma cfcomp1: "(f oo g) = (\ x. f\(g\x))" -by (simp add: oo_def) + by (simp add: oo_def) lemma cfcomp2 [simp]: "(f oo g)\x = f\(g\x)" -by (simp add: cfcomp1) + by (simp add: cfcomp1) lemma cfcomp_LAM: "cont g \ f oo (\ x. g x) = (\ x. f\(g x))" -by (simp add: cfcomp1) + by (simp add: cfcomp1) lemma cfcomp_strict [simp]: "\ oo f = \" -by (simp add: cfun_eq_iff) + by (simp add: cfun_eq_iff) text \ - Show that interpretation of (pcpo,\_->_\) is a category. - The class of objects is interpretation of syntactical class pcpo. - The class of arrows between objects @{typ 'a} and @{typ 'b} is interpret. of @{typ "'a -> 'b"}. - The identity arrow is interpretation of @{term ID}. - The composition of f and g is interpretation of \oo\. + Show that interpretation of (pcpo, \_\_\) is a category. + \<^item> The class of objects is interpretation of syntactical class pcpo. + \<^item> The class of arrows between objects @{typ 'a} and @{typ 'b} is interpret. of @{typ "'a \ 'b"}. + \<^item> The identity arrow is interpretation of @{term ID}. + \<^item> The composition of f and g is interpretation of \oo\. \ lemma ID2 [simp]: "f oo ID = f" -by (rule cfun_eqI, simp) + by (rule cfun_eqI, simp) lemma ID3 [simp]: "ID oo f = f" -by (rule cfun_eqI, simp) + by (rule cfun_eqI) simp lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h" -by (rule cfun_eqI, simp) + by (rule cfun_eqI) simp + subsection \Strictified functions\ default_sort pcpo -definition - seq :: "'a \ 'b \ 'b" where - "seq = (\ x. if x = \ then \ else ID)" +definition seq :: "'a \ 'b \ 'b" + where "seq = (\ x. if x = \ then \ else ID)" lemma cont2cont_if_bottom [cont2cont, simp]: - assumes f: "cont (\x. f x)" and g: "cont (\x. g x)" + assumes f: "cont (\x. f x)" + and g: "cont (\x. g x)" shows "cont (\x. if f x = \ then \ else g x)" proof (rule cont_apply [OF f]) - show "\x. cont (\y. if y = \ then \ else g x)" + show "cont (\y. if y = \ then \ else g x)" for x unfolding cont_def is_lub_def is_ub_def ball_simps by (simp add: lub_eq_bottom_iff) - show "\y. cont (\x. if y = \ then \ else g x)" + show "cont (\x. if y = \ then \ else g x)" for y by (simp add: g) qed lemma seq_conv_if: "seq\x = (if x = \ then \ else ID)" -unfolding seq_def by simp + by (simp add: seq_def) lemma seq_simps [simp]: "seq\\ = \" "seq\x\\ = \" "x \ \ \ seq\x = ID" -by (simp_all add: seq_conv_if) + by (simp_all add: seq_conv_if) -definition - strictify :: "('a \ 'b) \ 'a \ 'b" where - "strictify = (\ f x. seq\x\(f\x))" +definition strictify :: "('a \ 'b) \ 'a \ 'b" + where "strictify = (\ f x. seq\x\(f\x))" lemma strictify_conv_if: "strictify\f\x = (if x = \ then \ else f\x)" -unfolding strictify_def by simp + by (simp add: strictify_def) lemma strictify1 [simp]: "strictify\f\\ = \" -by (simp add: strictify_conv_if) + by (simp add: strictify_conv_if) lemma strictify2 [simp]: "x \ \ \ strictify\f\x = f\x" -by (simp add: strictify_conv_if) + by (simp add: strictify_conv_if) + subsection \Continuity of let-bindings\ @@ -499,19 +498,18 @@ assumes g1: "\y. cont (\x. g x y)" assumes g2: "\x. cont (\y. g x y)" shows "cont (\x. let y = f x in g x y)" -unfolding Let_def using f g2 g1 by (rule cont_apply) + unfolding Let_def using f g2 g1 by (rule cont_apply) lemma cont2cont_Let' [simp, cont2cont]: assumes f: "cont (\x. f x)" assumes g: "cont (\p. g (fst p) (snd p))" shows "cont (\x. let y = f x in g x y)" -using f + using f proof (rule cont2cont_Let) - fix x show "cont (\y. g x y)" - using g by (simp add: prod_cont_iff) -next - fix y show "cont (\x. g x y)" - using g by (simp add: prod_cont_iff) + from g show "cont (\y. g x y)" for x + by (simp add: prod_cont_iff) + from g show "cont (\x. g x y)" for y + by (simp add: prod_cont_iff) qed text \The simple version (suggested by Joachim Breitner) is needed if @@ -520,6 +518,6 @@ lemma cont2cont_Let_simple [simp, cont2cont]: assumes "\y. cont (\x. g x y)" shows "cont (\x. let y = t in g x y)" -unfolding Let_def using assms . + unfolding Let_def using assms . end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Cont.thy --- a/src/HOL/HOLCF/Cont.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Cont.thy Mon Jan 01 23:07:24 2018 +0100 @@ -6,7 +6,7 @@ section \Continuity and monotonicity\ theory Cont -imports Pcpo + imports Pcpo begin text \ @@ -18,71 +18,62 @@ subsection \Definitions\ -definition - monofun :: "('a \ 'b) \ bool" \ "monotonicity" where - "monofun f = (\x y. x \ y \ f x \ f y)" +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))" +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 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 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 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) +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 +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 +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 +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 + 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] @@ -90,17 +81,15 @@ 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 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))" + 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" @@ -109,15 +98,16 @@ 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 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" @@ -128,9 +118,9 @@ text \The identity function is continuous\ lemma cont_id [simp, cont2cont]: "cont (\x. x)" -apply (rule contI) -apply (erule cpo_lubI) -done + apply (rule contI) + apply (erule cpo_lubI) + done text \constant functions are continuous\ @@ -146,87 +136,88 @@ 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" + 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) + cont2monofunE [OF 2] + cont2monofunE [OF 3] + below_trans) next - fix Y :: "nat \ 'a" assume "chain Y" + 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) + 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]) +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)" + 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 + 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 +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))" -apply (unfold finite_chain_def) -apply (simp add: ch2ch_monofun) -apply (force simp add: max_in_chain_def) -done +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]) +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::'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 +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::'a::flat \ 'b::pcpo)" -apply (rule monofunI) -apply (drule ax_flat) -apply auto -done +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::'a::flat \ 'b::pcpo)" -by (rule flatdom_strict2mono [THEN chfindom_monofun2cont]) +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::'a::discrete_cpo \ 'b::cpo)" -apply (rule contI) -apply (drule discrete_chain_const, clarify) -apply (simp add: is_lub_const) -done +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 add: is_lub_const) + done end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Cpodef.thy --- a/src/HOL/HOLCF/Cpodef.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Cpodef.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,8 +5,8 @@ section \Subtypes of pcpos\ theory Cpodef -imports Adm -keywords "pcpodef" "cpodef" :: thy_goal + imports Adm + keywords "pcpodef" "cpodef" :: thy_goal begin subsection \Proving a subtype is a partial order\ @@ -16,22 +16,22 @@ 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>\Porder.below\, NONE)\ theorem typedef_po: fixes Abs :: "'a::po \ 'b::type" assumes type: "type_definition Rep Abs A" and below: "op \ \ \x y. Rep x \ Rep y" shows "OFCLASS('b, po_class)" - apply (intro_classes, unfold below) - apply (rule below_refl) - apply (erule (1) below_trans) - apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) - apply (erule (1) below_antisym) -done + apply (intro_classes, unfold below) + apply (rule below_refl) + apply (erule (1) below_trans) + apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) + 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>\Porder.below\, SOME \<^typ>\'a::below \ 'a::below \ bool\)\ + subsection \Proving a subtype is finite\ @@ -41,29 +41,32 @@ shows "finite A \ finite (UNIV :: 'b set)" proof - assume "finite A" - hence "finite (Abs ` A)" by (rule finite_imageI) - thus "finite (UNIV :: 'b set)" + then have "finite (Abs ` A)" + by (rule finite_imageI) + then show "finite (UNIV :: 'b set)" by (simp only: type_definition.Abs_image [OF type]) qed + subsection \Proving a subtype is chain-finite\ lemma ch2ch_Rep: assumes below: "op \ \ \x y. Rep x \ Rep y" shows "chain S \ chain (\i. Rep (S i))" -unfolding chain_def below . + unfolding chain_def below . theorem typedef_chfin: fixes Abs :: "'a::chfin \ 'b::po" assumes type: "type_definition Rep Abs A" and below: "op \ \ \x y. Rep x \ Rep y" shows "OFCLASS('b, chfin_class)" - apply intro_classes - apply (drule ch2ch_Rep [OF below]) - apply (drule chfin) - apply (unfold max_in_chain_def) - apply (simp add: type_definition.Rep_inject [OF type]) -done + apply intro_classes + apply (drule ch2ch_Rep [OF below]) + apply (drule chfin) + apply (unfold max_in_chain_def) + apply (simp add: type_definition.Rep_inject [OF type]) + done + subsection \Proving a subtype is complete\ @@ -78,7 +81,7 @@ lemma typedef_is_lubI: assumes below: "op \ \ \x y. Rep x \ Rep y" shows "range (\i. Rep (S i)) <<| Rep x \ range S <<| x" -unfolding is_lub_def is_ub_def below by simp + by (simp add: is_lub_def is_ub_def below) lemma Abs_inverse_lub_Rep: fixes Abs :: "'a::cpo \ 'b::po" @@ -86,24 +89,26 @@ and below: "op \ \ \x y. Rep x \ Rep y" and adm: "adm (\x. x \ A)" shows "chain S \ Rep (Abs (\i. Rep (S i))) = (\i. Rep (S i))" - apply (rule type_definition.Abs_inverse [OF type]) - apply (erule admD [OF adm ch2ch_Rep [OF below]]) - apply (rule type_definition.Rep [OF type]) -done + apply (rule type_definition.Abs_inverse [OF type]) + apply (erule admD [OF adm ch2ch_Rep [OF below]]) + apply (rule type_definition.Rep [OF type]) + done theorem typedef_is_lub: fixes Abs :: "'a::cpo \ 'b::po" assumes type: "type_definition Rep Abs A" and below: "op \ \ \x y. Rep x \ Rep y" and adm: "adm (\x. x \ A)" - shows "chain S \ range S <<| Abs (\i. Rep (S i))" + assumes S: "chain S" + shows "range S <<| Abs (\i. Rep (S i))" proof - - assume S: "chain S" - hence "chain (\i. Rep (S i))" by (rule ch2ch_Rep [OF below]) - hence "range (\i. Rep (S i)) <<| (\i. Rep (S i))" by (rule cpo_lubI) - hence "range (\i. Rep (S i)) <<| Rep (Abs (\i. Rep (S i)))" + from S have "chain (\i. Rep (S i))" + by (rule ch2ch_Rep [OF below]) + then have "range (\i. Rep (S i)) <<| (\i. Rep (S i))" + by (rule cpo_lubI) + then have "range (\i. Rep (S i)) <<| Rep (Abs (\i. Rep (S i)))" by (simp only: Abs_inverse_lub_Rep [OF type below adm S]) - thus "range S <<| Abs (\i. Rep (S i))" + then show "range S <<| Abs (\i. Rep (S i))" by (rule typedef_is_lubI [OF below]) qed @@ -116,12 +121,14 @@ and adm: "adm (\x. x \ A)" shows "OFCLASS('b, cpo_class)" proof - fix S::"nat \ 'b" assume "chain S" - hence "range S <<| Abs (\i. Rep (S i))" + fix S :: "nat \ 'b" + assume "chain S" + then have "range S <<| Abs (\i. Rep (S i))" by (rule typedef_is_lub [OF type below adm]) - thus "\x. range S <<| x" .. + then show "\x. range S <<| x" .. qed + subsubsection \Continuity of \emph{Rep} and \emph{Abs}\ text \For any sub-cpo, the @{term Rep} function is continuous.\ @@ -132,13 +139,13 @@ and below: "op \ \ \x y. Rep x \ Rep y" and adm: "adm (\x. x \ A)" shows "cont (\x. f x) \ cont (\x. Rep (f x))" - apply (erule cont_apply [OF _ _ cont_const]) - apply (rule contI) - apply (simp only: typedef_lub [OF type below adm]) - apply (simp only: Abs_inverse_lub_Rep [OF type below adm]) - apply (rule cpo_lubI) - apply (erule ch2ch_Rep [OF below]) -done + apply (erule cont_apply [OF _ _ cont_const]) + apply (rule contI) + apply (simp only: typedef_lub [OF type below adm]) + apply (simp only: Abs_inverse_lub_Rep [OF type below adm]) + apply (rule cpo_lubI) + apply (erule ch2ch_Rep [OF below]) + done text \ For a sub-cpo, we can make the @{term Abs} function continuous @@ -154,8 +161,9 @@ and adm: "adm (\x. x \ A)" (* not used *) and f_in_A: "\x. f x \ A" shows "cont f \ cont (\x. Abs (f x))" -unfolding cont_def is_lub_def is_ub_def ball_simps below -by (simp add: type_definition.Abs_inverse [OF type f_in_A]) + unfolding cont_def is_lub_def is_ub_def ball_simps below + by (simp add: type_definition.Abs_inverse [OF type f_in_A]) + subsection \Proving subtype elements are compact\ @@ -170,9 +178,10 @@ by (rule typedef_cont_Rep [OF type below adm cont_id]) assume "adm (\x. Rep k \ x)" with cont_Rep have "adm (\x. Rep k \ Rep x)" by (rule adm_subst) - thus "adm (\x. k \ x)" by (unfold below) + then show "adm (\x. k \ x)" by (unfold below) qed + subsection \Proving a subtype is pointed\ text \ @@ -187,12 +196,12 @@ and z_in_A: "z \ A" and z_least: "\x. x \ A \ z \ x" shows "OFCLASS('b, pcpo_class)" - apply (intro_classes) - apply (rule_tac x="Abs z" in exI, rule allI) - apply (unfold below) - apply (subst type_definition.Abs_inverse [OF type z_in_A]) - apply (rule z_least [OF type_definition.Rep [OF type]]) -done + apply (intro_classes) + apply (rule_tac x="Abs z" in exI, rule allI) + apply (unfold below) + apply (subst type_definition.Abs_inverse [OF type z_in_A]) + apply (rule z_least [OF type_definition.Rep [OF type]]) + done text \ As a special case, a subtype of a pcpo has a least element @@ -205,7 +214,8 @@ and below: "op \ \ \x y. Rep x \ Rep y" and bottom_in_A: "\ \ A" shows "OFCLASS('b, pcpo_class)" -by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal) + by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal) + subsubsection \Strictness of \emph{Rep} and \emph{Abs}\ @@ -219,36 +229,37 @@ and below: "op \ \ \x y. Rep x \ Rep y" and bottom_in_A: "\ \ A" shows "Abs \ = \" - apply (rule bottomI, unfold below) - apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A]) -done + apply (rule bottomI, unfold below) + apply (simp add: type_definition.Abs_inverse [OF type bottom_in_A]) + done theorem typedef_Rep_strict: assumes type: "type_definition Rep Abs A" and below: "op \ \ \x y. Rep x \ Rep y" and bottom_in_A: "\ \ A" shows "Rep \ = \" - apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst]) - apply (rule type_definition.Abs_inverse [OF type bottom_in_A]) -done + apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst]) + apply (rule type_definition.Abs_inverse [OF type bottom_in_A]) + done theorem typedef_Abs_bottom_iff: assumes type: "type_definition Rep Abs A" and below: "op \ \ \x y. Rep x \ Rep y" and bottom_in_A: "\ \ A" shows "x \ A \ (Abs x = \) = (x = \)" - apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst]) - apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A) -done + apply (rule typedef_Abs_strict [OF type below bottom_in_A, THEN subst]) + apply (simp add: type_definition.Abs_inject [OF type] bottom_in_A) + done theorem typedef_Rep_bottom_iff: assumes type: "type_definition Rep Abs A" and below: "op \ \ \x y. Rep x \ Rep y" and bottom_in_A: "\ \ A" shows "(Rep x = \) = (x = \)" - apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst]) - apply (simp add: type_definition.Rep_inject [OF type]) -done + apply (rule typedef_Rep_strict [OF type below bottom_in_A, THEN subst]) + apply (simp add: type_definition.Rep_inject [OF type]) + done + subsection \Proving a subtype is flat\ @@ -258,12 +269,13 @@ and below: "op \ \ \x y. Rep x \ Rep y" and bottom_in_A: "\ \ A" shows "OFCLASS('b, flat_class)" - apply (intro_classes) - apply (unfold below) - apply (simp add: type_definition.Rep_inject [OF type, symmetric]) - apply (simp add: typedef_Rep_strict [OF type below bottom_in_A]) - apply (simp add: ax_flat) -done + apply (intro_classes) + apply (unfold below) + apply (simp add: type_definition.Rep_inject [OF type, symmetric]) + apply (simp add: typedef_Rep_strict [OF type below bottom_in_A]) + apply (simp add: ax_flat) + done + subsection \HOLCF type definition package\ diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Cprod.thy --- a/src/HOL/HOLCF/Cprod.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Cprod.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,46 +5,45 @@ section \The cpo of cartesian products\ theory Cprod -imports Cfun + imports Cfun begin default_sort cpo + subsection \Continuous case function for unit type\ -definition - unit_when :: "'a \ unit \ 'a" where - "unit_when = (\ a _. a)" +definition unit_when :: "'a \ unit \ 'a" + where "unit_when = (\ a _. a)" translations - "\(). t" == "CONST unit_when\t" + "\(). t" \ "CONST unit_when\t" lemma unit_when [simp]: "unit_when\a\u = a" -by (simp add: unit_when_def) + by (simp add: unit_when_def) + subsection \Continuous version of split function\ -definition - csplit :: "('a \ 'b \ 'c) \ ('a * 'b) \ 'c" where - "csplit = (\ f p. f\(fst p)\(snd p))" +definition csplit :: "('a \ 'b \ 'c) \ ('a \ 'b) \ 'c" + where "csplit = (\ f p. f\(fst p)\(snd p))" translations - "\(CONST Pair x y). t" == "CONST csplit\(\ x y. t)" + "\(CONST Pair x y). t" \ "CONST csplit\(\ x y. t)" -abbreviation - cfst :: "'a \ 'b \ 'a" where - "cfst \ Abs_cfun fst" +abbreviation cfst :: "'a \ 'b \ 'a" + where "cfst \ Abs_cfun fst" -abbreviation - csnd :: "'a \ 'b \ 'b" where - "csnd \ Abs_cfun snd" +abbreviation csnd :: "'a \ 'b \ 'b" + where "csnd \ Abs_cfun snd" + subsection \Convert all lemmas to the continuous versions\ lemma csplit1 [simp]: "csplit\f\\ = f\\\\" -by (simp add: csplit_def) + by (simp add: csplit_def) lemma csplit_Pair [simp]: "csplit\f\(x, y) = f\x\y" -by (simp add: csplit_def) + by (simp add: csplit_def) end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Deflation.thy --- a/src/HOL/HOLCF/Deflation.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Deflation.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,11 +5,12 @@ section \Continuous deflations and ep-pairs\ theory Deflation -imports Cfun + imports Cfun begin default_sort cpo + subsection \Continuous deflations\ locale deflation = @@ -19,15 +20,15 @@ begin lemma below_ID: "d \ ID" -by (rule cfun_belowI, simp add: below) + by (rule cfun_belowI) (simp add: below) text \The set of fixed points is the same as the range.\ lemma fixes_eq_range: "{x. d\x = x} = range (\x. d\x)" -by (auto simp add: eq_sym_conv idem) + by (auto simp add: eq_sym_conv idem) lemma range_eq_fixes: "range (\x. d\x) = {x. d\x = x}" -by (auto simp add: eq_sym_conv idem) + by (auto simp add: eq_sym_conv idem) text \ The pointwise ordering on deflation functions coincides with @@ -35,20 +36,22 @@ \ lemma belowI: - assumes f: "\x. d\x = x \ f\x = x" shows "d \ f" + assumes f: "\x. d\x = x \ f\x = x" + shows "d \ f" proof (rule cfun_belowI) fix x - from below have "f\(d\x) \ f\x" by (rule monofun_cfun_arg) - also from idem have "f\(d\x) = d\x" by (rule f) + from below have "f\(d\x) \ f\x" + by (rule monofun_cfun_arg) + also from idem have "f\(d\x) = d\x" + by (rule f) finally show "d\x \ f\x" . qed lemma belowD: "\f \ d; f\x = x\ \ d\x = x" proof (rule below_antisym) from below show "d\x \ x" . -next assume "f \ d" - hence "f\x \ d\x" by (rule monofun_cfun_fun) + then have "f\x \ d\x" by (rule monofun_cfun_fun) also assume "f\x = x" finally show "x \ d\x" . qed @@ -56,23 +59,22 @@ end lemma deflation_strict: "deflation d \ d\\ = \" -by (rule deflation.below [THEN bottomI]) + by (rule deflation.below [THEN bottomI]) lemma adm_deflation: "adm (\d. deflation d)" -by (simp add: deflation_def) + by (simp add: deflation_def) lemma deflation_ID: "deflation ID" -by (simp add: deflation.intro) + by (simp add: deflation.intro) lemma deflation_bottom: "deflation \" -by (simp add: deflation.intro) + by (simp add: deflation.intro) -lemma deflation_below_iff: - "\deflation p; deflation q\ \ p \ q \ (\x. p\x = x \ q\x = x)" - apply safe - apply (simp add: deflation.belowD) - apply (simp add: deflation.belowI) -done +lemma deflation_below_iff: "deflation p \ deflation q \ p \ q \ (\x. p\x = x \ q\x = x)" + apply safe + apply (simp add: deflation.belowD) + apply (simp add: deflation.belowI) + done text \ The composition of two deflations is equal to @@ -88,26 +90,26 @@ from g.below show "f\(g\x) \ f\x" by (rule monofun_cfun_arg) next interpret f: deflation f by fact - assume "f \ g" hence "f\x \ g\x" by (rule monofun_cfun_fun) - hence "f\(f\x) \ f\(g\x)" by (rule monofun_cfun_arg) + assume "f \ g" + then have "f\x \ g\x" by (rule monofun_cfun_fun) + then have "f\(f\x) \ f\(g\x)" by (rule monofun_cfun_arg) also have "f\(f\x) = f\x" by (rule f.idem) finally show "f\x \ f\(g\x)" . qed -lemma deflation_below_comp2: - "\deflation f; deflation g; f \ g\ \ g\(f\x) = f\x" -by (simp only: deflation.belowD deflation.idem) +lemma deflation_below_comp2: "deflation f \ deflation g \ f \ g \ g\(f\x) = f\x" + by (simp only: deflation.belowD deflation.idem) subsection \Deflations with finite range\ lemma finite_range_imp_finite_fixes: - "finite (range f) \ finite {x. f x = x}" + assumes "finite (range f)" + shows "finite {x. f x = x}" proof - have "{x. f x = x} \ range f" by (clarify, erule subst, rule rangeI) - moreover assume "finite (range f)" - ultimately show "finite {x. f x = x}" + from this assms show "finite {x. f x = x}" by (rule finite_subset) qed @@ -116,10 +118,10 @@ begin lemma finite_range: "finite (range (\x. d\x))" -by (simp add: range_eq_fixes finite_fixes) + by (simp add: range_eq_fixes finite_fixes) lemma finite_image: "finite ((\x. d\x) ` A)" -by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range]) + by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range]) lemma compact: "compact (d\x)" proof (rule compactI2) @@ -127,41 +129,36 @@ assume Y: "chain Y" have "finite_chain (\i. d\(Y i))" proof (rule finite_range_imp_finch) - show "chain (\i. d\(Y i))" - using Y by simp - have "range (\i. d\(Y i)) \ range (\x. d\x)" - by clarsimp - thus "finite (range (\i. d\(Y i)))" + from Y show "chain (\i. d\(Y i))" by simp + have "range (\i. d\(Y i)) \ range (\x. d\x)" by auto + then show "finite (range (\i. d\(Y i)))" using finite_range by (rule finite_subset) qed - hence "\j. (\i. d\(Y i)) = d\(Y j)" + then have "\j. (\i. d\(Y i)) = d\(Y j)" by (simp add: finite_chain_def maxinch_is_thelub Y) then obtain j where j: "(\i. d\(Y i)) = d\(Y j)" .. assume "d\x \ (\i. Y i)" - hence "d\(d\x) \ d\(\i. Y i)" + then have "d\(d\x) \ d\(\i. Y i)" by (rule monofun_cfun_arg) - hence "d\x \ (\i. d\(Y i))" + then have "d\x \ (\i. d\(Y i))" by (simp add: contlub_cfun_arg Y idem) - hence "d\x \ d\(Y j)" - using j by simp - hence "d\x \ Y j" + with j have "d\x \ d\(Y j)" by simp + then have "d\x \ Y j" using below by (rule below_trans) - thus "\j. d\x \ Y j" .. + then show "\j. d\x \ Y j" .. qed end -lemma finite_deflation_intro: - "deflation d \ finite {x. d\x = x} \ finite_deflation d" -by (intro finite_deflation.intro finite_deflation_axioms.intro) +lemma finite_deflation_intro: "deflation d \ finite {x. d\x = x} \ finite_deflation d" + by (intro finite_deflation.intro finite_deflation_axioms.intro) -lemma finite_deflation_imp_deflation: - "finite_deflation d \ deflation d" -unfolding finite_deflation_def by simp +lemma finite_deflation_imp_deflation: "finite_deflation d \ deflation d" + by (simp add: finite_deflation_def) lemma finite_deflation_bottom: "finite_deflation \" -by standard simp_all + by standard simp_all subsection \Continuous embedding-projection pairs\ @@ -175,22 +172,21 @@ lemma e_below_iff [simp]: "e\x \ e\y \ x \ y" proof assume "e\x \ e\y" - hence "p\(e\x) \ p\(e\y)" by (rule monofun_cfun_arg) - thus "x \ y" by simp + then have "p\(e\x) \ p\(e\y)" by (rule monofun_cfun_arg) + then show "x \ y" by simp next assume "x \ y" - thus "e\x \ e\y" by (rule monofun_cfun_arg) + then show "e\x \ e\y" by (rule monofun_cfun_arg) qed lemma e_eq_iff [simp]: "e\x = e\y \ x = y" -unfolding po_eq_conv e_below_iff .. + unfolding po_eq_conv e_below_iff .. -lemma p_eq_iff: - "\e\(p\x) = x; e\(p\y) = y\ \ p\x = p\y \ x = y" -by (safe, erule subst, erule subst, simp) +lemma p_eq_iff: "e\(p\x) = x \ e\(p\y) = y \ p\x = p\y \ x = y" + by (safe, erule subst, erule subst, simp) -lemma p_inverse: "(\x. y = e\x) = (e\(p\y) = y)" -by (auto, rule exI, erule sym) +lemma p_inverse: "(\x. y = e\x) \ e\(p\y) = y" + by (auto, rule exI, erule sym) lemma e_below_iff_below_p: "e\x \ y \ x \ p\y" proof @@ -206,28 +202,29 @@ lemma compact_e_rev: "compact (e\x) \ compact x" proof - assume "compact (e\x)" - hence "adm (\y. e\x \ y)" by (rule compactD) - hence "adm (\y. e\x \ e\y)" by (rule adm_subst [OF cont_Rep_cfun2]) - hence "adm (\y. x \ y)" by simp - thus "compact x" by (rule compactI) + then have "adm (\y. e\x \ y)" by (rule compactD) + then have "adm (\y. e\x \ e\y)" by (rule adm_subst [OF cont_Rep_cfun2]) + then have "adm (\y. x \ y)" by simp + then show "compact x" by (rule compactI) qed -lemma compact_e: "compact x \ compact (e\x)" +lemma compact_e: + assumes "compact x" + shows "compact (e\x)" proof - - assume "compact x" - hence "adm (\y. x \ y)" by (rule compactD) - hence "adm (\y. x \ p\y)" by (rule adm_subst [OF cont_Rep_cfun2]) - hence "adm (\y. e\x \ y)" by (simp add: e_below_iff_below_p) - thus "compact (e\x)" by (rule compactI) + from assms have "adm (\y. x \ y)" by (rule compactD) + then have "adm (\y. x \ p\y)" by (rule adm_subst [OF cont_Rep_cfun2]) + then have "adm (\y. e\x \ y)" by (simp add: e_below_iff_below_p) + then show "compact (e\x)" by (rule compactI) qed lemma compact_e_iff: "compact (e\x) \ compact x" -by (rule iffI [OF compact_e_rev compact_e]) + by (rule iffI [OF compact_e_rev compact_e]) text \Deflations from ep-pairs\ lemma deflation_e_p: "deflation (e oo p)" -by (simp add: deflation.intro e_p_below) + by (simp add: deflation.intro e_p_below) lemma deflation_e_d_p: assumes "deflation d" @@ -253,9 +250,9 @@ by (simp add: e_below_iff_below_p below) have "finite ((\x. e\x) ` (\x. d\x) ` range (\x. p\x))" by (simp add: finite_image) - hence "finite (range (\x. (e oo d oo p)\x))" + then have "finite (range (\x. (e oo d oo p)\x))" by (simp add: image_image) - thus "finite {x. (e oo d oo p)\x = x}" + then show "finite {x. (e oo d oo p)\x = x}" by (rule finite_range_imp_finite_fixes) qed @@ -265,32 +262,27 @@ shows "deflation (p oo d oo e)" proof - interpret d: deflation d by fact - { - fix x + have p_d_e_below: "(p oo d oo e)\x \ x" for x + proof - have "d\(e\x) \ e\x" by (rule d.below) - hence "p\(d\(e\x)) \ p\(e\x)" + then have "p\(d\(e\x)) \ p\(e\x)" by (rule monofun_cfun_arg) - hence "(p oo d oo e)\x \ x" - by simp - } - note p_d_e_below = this + then show ?thesis by simp + qed show ?thesis proof - fix x - show "(p oo d oo e)\x \ x" + show "(p oo d oo e)\x \ x" for x by (rule p_d_e_below) - next - fix x - show "(p oo d oo e)\((p oo d oo e)\x) = (p oo d oo e)\x" + show "(p oo d oo e)\((p oo d oo e)\x) = (p oo d oo e)\x" for x proof (rule below_antisym) show "(p oo d oo e)\((p oo d oo e)\x) \ (p oo d oo e)\x" by (rule p_d_e_below) have "p\(d\(d\(d\(e\x)))) \ p\(d\(e\(p\(d\(e\x)))))" by (intro monofun_cfun_arg d) - hence "p\(d\(e\x)) \ p\(d\(e\(p\(d\(e\x)))))" + then have "p\(d\(e\x)) \ p\(d\(e\(p\(d\(e\x)))))" by (simp only: d.idem) - thus "(p oo d oo e)\x \ (p oo d oo e)\((p oo d oo e)\x)" + then show "(p oo d oo e)\x \ (p oo d oo e)\((p oo d oo e)\x)" by simp qed qed @@ -305,16 +297,16 @@ show ?thesis proof (rule finite_deflation_intro) have "deflation d" .. - thus "deflation (p oo d oo e)" + then show "deflation (p oo d oo e)" using d by (rule deflation_p_d_e) next have "finite ((\x. d\x) ` range (\x. e\x))" by (rule d.finite_image) - hence "finite ((\x. p\x) ` (\x. d\x) ` range (\x. e\x))" + then have "finite ((\x. p\x) ` (\x. d\x) ` range (\x. e\x))" by (rule finite_imageI) - hence "finite (range (\x. (p oo d oo e)\x))" + then have "finite (range (\x. (p oo d oo e)\x))" by (simp add: image_image) - thus "finite {x. (p oo d oo e)\x = x}" + then show "finite {x. (p oo d oo e)\x = x}" by (rule finite_range_imp_finite_fixes) qed qed @@ -324,41 +316,42 @@ subsection \Uniqueness of ep-pairs\ lemma ep_pair_unique_e_lemma: - assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p" + assumes 1: "ep_pair e1 p" + and 2: "ep_pair e2 p" shows "e1 \ e2" proof (rule cfun_belowI) fix x have "e1\(p\(e2\x)) \ e2\x" by (rule ep_pair.e_p_below [OF 1]) - thus "e1\x \ e2\x" + then show "e1\x \ e2\x" by (simp only: ep_pair.e_inverse [OF 2]) qed -lemma ep_pair_unique_e: - "\ep_pair e1 p; ep_pair e2 p\ \ e1 = e2" -by (fast intro: below_antisym elim: ep_pair_unique_e_lemma) +lemma ep_pair_unique_e: "ep_pair e1 p \ ep_pair e2 p \ e1 = e2" + by (fast intro: below_antisym elim: ep_pair_unique_e_lemma) lemma ep_pair_unique_p_lemma: - assumes 1: "ep_pair e p1" and 2: "ep_pair e p2" + assumes 1: "ep_pair e p1" + and 2: "ep_pair e p2" shows "p1 \ p2" proof (rule cfun_belowI) fix x have "e\(p1\x) \ x" by (rule ep_pair.e_p_below [OF 1]) - hence "p2\(e\(p1\x)) \ p2\x" + then have "p2\(e\(p1\x)) \ p2\x" by (rule monofun_cfun_arg) - thus "p1\x \ p2\x" + then show "p1\x \ p2\x" by (simp only: ep_pair.e_inverse [OF 2]) qed -lemma ep_pair_unique_p: - "\ep_pair e p1; ep_pair e p2\ \ p1 = p2" -by (fast intro: below_antisym elim: ep_pair_unique_p_lemma) +lemma ep_pair_unique_p: "ep_pair e p1 \ ep_pair e p2 \ p1 = p2" + by (fast intro: below_antisym elim: ep_pair_unique_p_lemma) + subsection \Composing ep-pairs\ lemma ep_pair_ID_ID: "ep_pair ID ID" -by standard simp_all + by standard simp_all lemma ep_pair_comp: assumes "ep_pair e1 p1" and "ep_pair e2 p2" @@ -371,7 +364,7 @@ by simp have "e1\(p1\(p2\y)) \ p2\y" by (rule ep1.e_p_below) - hence "e2\(e1\(p1\(p2\y))) \ e2\(p2\y)" + then have "e2\(e1\(p1\(p2\y))) \ e2\(p2\y)" by (rule monofun_cfun_arg) also have "e2\(p2\y) \ y" by (rule ep2.e_p_below) @@ -387,19 +380,19 @@ lemma e_strict [simp]: "e\\ = \" proof - have "\ \ p\\" by (rule minimal) - hence "e\\ \ e\(p\\)" by (rule monofun_cfun_arg) + then have "e\\ \ e\(p\\)" by (rule monofun_cfun_arg) also have "e\(p\\) \ \" by (rule e_p_below) finally show "e\\ = \" by simp qed lemma e_bottom_iff [simp]: "e\x = \ \ x = \" -by (rule e_eq_iff [where y="\", unfolded e_strict]) + by (rule e_eq_iff [where y="\", unfolded e_strict]) lemma e_defined: "x \ \ \ e\x \ \" -by simp + by simp lemma p_strict [simp]: "p\\ = \" -by (rule e_inverse [where x="\", unfolded e_strict]) + by (rule e_inverse [where x="\", unfolded e_strict]) lemmas stricts = e_strict p_strict diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Discrete.thy --- a/src/HOL/HOLCF/Discrete.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Discrete.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,7 +5,7 @@ section \Discrete cpo types\ theory Discrete -imports Cont + imports Cont begin datatype 'a discr = Discr "'a :: type" @@ -15,24 +15,23 @@ instantiation discr :: (type) discrete_cpo begin -definition - "(op \ :: 'a discr \ 'a discr \ bool) = (op =)" +definition "(op \ :: 'a discr \ 'a discr \ bool) = (op =)" 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)" +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) + by (simp add: undiscr_def) lemma Discr_undiscr [simp]: "Discr (undiscr y) = y" -by (induct y) simp + by (induct y) simp end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Fix.thy --- a/src/HOL/HOLCF/Fix.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Fix.thy Mon Jan 01 23:07:24 2018 +0100 @@ -6,51 +6,50 @@ section \Fixed point operator and admissibility\ theory Fix -imports Cfun + imports Cfun begin default_sort pcpo + subsection \Iteration\ -primrec iterate :: "nat \ ('a::cpo \ 'a) \ ('a \ 'a)" where +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 + by simp lemma iterate_Suc [simp]: "iterate (Suc n)\F\x = F\(iterate n\F\x)" -by simp + 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 + 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 +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) + 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\\)" +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)" +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) @@ -60,7 +59,7 @@ text \direct connection between @{term fix} and iteration\ lemma fix_def2: "fix\F = (\i. iterate i\F\\)" -unfolding fix_def by simp + by (simp add: fix_def) lemma iterate_below_fix: "iterate n\f\\ \ fix\f" unfolding fix_def2 @@ -72,105 +71,103 @@ \ 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 + 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 + 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) + by (rule fix_least_below) simp lemma fix_eqI: - assumes fixed: "F\x = x" and least: "\z. F\z = z \ x \ z" + 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 + 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]) + 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]) + by (erule fix_eq2 [THEN cfun_fun_cong]) lemma fix_eq4: "f = fix\F \ f = F\f" -apply (erule ssubst) -apply (rule fix_eq) -done + 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]) + 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_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) + by (simp add: fix_bottom_iff) lemma fix_defined: "F\\ \ \ \ fix\F \ \" -by (simp add: fix_bottom_iff) + 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) + by (simp add: fix_strict) lemma fix_const: "(\ x. c) = c" -by (subst fix_eq, simp) + 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 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 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 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 + 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))" @@ -180,17 +177,17 @@ proof - from adm have adm': "adm (case_prod P)" unfolding split_def . - have "\i. P (iterate i\F\\) (iterate i\G\\)" - by (induct_tac i, simp add: base, simp add: step) - hence "\i. case_prod P (iterate i\F\\, iterate i\G\\)" + 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 - hence "case_prod P (\i. (iterate i\F\\, iterate i\G\\))" + then have "case_prod P (\i. (iterate i\F\\, iterate i\G\\))" by - (rule admD [OF adm'], simp, assumption) - hence "case_prod P (\i. iterate i\F\\, \i. iterate i\G\\)" + then have "case_prod P (\i. iterate i\F\\, \i. iterate i\G\\)" by (simp add: lub_Pair) - hence "P (\i. iterate i\F\\) (\i. iterate i\G\\)" + then have "P (\i. iterate i\F\\) (\i. iterate i\G\\)" by simp - thus "P (fix\F) (fix\G)" + then show "P (fix\F) (fix\G)" by (simp add: fix_def2) qed @@ -200,7 +197,8 @@ 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) + by (rule parallel_fix_ind) (simp_all add: assms) + subsection \Fixed-points on product types\ @@ -215,27 +213,35 @@ \ y. snd (F\(\ x. fst (F\(x, \ y. snd (F\(x, y)))), y)))" (is "fix\F = (?x, ?y)") proof (rule fix_eqI) - have 1: "fst (F\(?x, ?y)) = ?x" + have *: "fst (F\(?x, ?y)) = ?x" by (rule trans [symmetric, OF fix_eq], simp) - have 2: "snd (F\(?x, ?y)) = ?y" + have "snd (F\(?x, ?y)) = ?y" by (rule trans [symmetric, OF fix_eq], simp) - from 1 2 show "F\(?x, ?y) = (?x, ?y)" by (simp add: prod_eq_iff) + 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) + 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) - hence "fst (F\(x, ?y1)) \ fst (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) - hence "fst (F\(x, ?y1)) \ x" using F_x by simp - hence 1: "?x \ x" by (simp add: fix_least_below) - hence "snd (F\(?x, y)) \ snd (F\(x, y))" + 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) - hence "snd (F\(?x, y)) \ y" using F_y by simp - hence 2: "?y \ y" by (simp add: fix_least_below) - show "(?x, ?y) \ z" using z 1 2 by simp + 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 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Fun_Cpo.thy --- a/src/HOL/HOLCF/Fun_Cpo.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Fun_Cpo.thy Mon Jan 01 23:07:24 2018 +0100 @@ -6,7 +6,7 @@ section \Class instances for the full function space\ theory Fun_Cpo -imports Adm + imports Adm begin subsection \Full function space is a partial order\ @@ -14,8 +14,7 @@ instantiation "fun" :: (type, below) below begin -definition - below_fun_def: "(op \) \ (\f g. \x. f x \ g x)" +definition below_fun_def: "(op \) \ (\f g. \x. f x \ g x)" instance .. end @@ -27,127 +26,125 @@ by (simp add: below_fun_def) next fix f g :: "'a \ 'b" - assume "f \ g" and "g \ f" thus "f = g" + 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" thus "f \ h" + 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) + by (simp add: below_fun_def) lemma fun_belowI: "(\x. f x \ g x) \ f \ g" -by (simp add: below_fun_def) + by (simp add: below_fun_def) lemma fun_belowD: "f \ g \ f x \ g x" -by (simp add: below_fun_def) + 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))" -unfolding chain_def fun_below_iff by auto + 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) + 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\ + by (simp add: chain_def below_fun_def) -lemma is_lub_lambda: - "(\x. range (\i. Y i x) <<| f x) \ range Y <<| f" -unfolding is_lub_def is_ub_def below_fun_def by simp +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::nat \ 'a::type \ 'b::cpo) - \ range S <<| (\x. \i. S i x)" -apply (rule is_lub_lambda) -apply (rule cpo_lubI) -apply (erule ch2ch_fun) -done +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::nat \ 'a::type \ 'b::cpo) - \ (\i. S i) = (\x. \i. S i x)" -by (rule is_lub_fun [THEN lub_eqI]) +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) + 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" - unfolding fun_below_iff fun_eq_iff - by simp + 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) + by (simp add: below_fun_def) instance "fun" :: (type, pcpo) pcpo -by standard (fast intro: minimal_fun) + by standard (fast intro: minimal_fun) lemma inst_fun_pcpo: "\ = (\x. \)" -by (rule minimal_fun [THEN bottomI, symmetric]) + by (rule minimal_fun [THEN bottomI, symmetric]) lemma app_strict [simp]: "\ x = \" -by (simp add: inst_fun_pcpo) + by (simp add: inst_fun_pcpo) lemma lambda_strict: "(\x. \) = \" -by (rule bottomI, rule minimal_fun) + 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) + 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) + 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) + 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 + 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) + using cont_id by (rule cont2cont_fun) text \ Lambda abstraction preserves monotonicity and continuity. (Note \(\x. \y. f x y) = f\.) \ -lemma mono2mono_lambda: - assumes f: "\y. monofun (\x. f x y)" shows "monofun f" -using f by (simp add: monofun_def fun_below_iff) +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]) + 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::'a::type. chain (\i. S i x::'b::cpo)) - \ (\x. \i. S i x) = (\i. (\x. S i x))" -by (simp add: lub_fun ch2ch_lambda) +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 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Map_Functions.thy --- a/src/HOL/HOLCF/Map_Functions.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Map_Functions.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,28 +5,24 @@ section \Map functions for various types\ theory Map_Functions -imports Deflation Sprod Ssum Sfun Up + imports Deflation Sprod Ssum Sfun Up begin subsection \Map operator for continuous function space\ default_sort cpo -definition - cfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \ 'c) \ ('b \ 'd)" -where - "cfun_map = (\ a b f x. b\(f\(a\x)))" +definition cfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \ 'c) \ ('b \ 'd)" + where "cfun_map = (\ a b f x. b\(f\(a\x)))" lemma cfun_map_beta [simp]: "cfun_map\a\b\f\x = b\(f\(a\x))" -unfolding cfun_map_def by simp + by (simp add: cfun_map_def) lemma cfun_map_ID: "cfun_map\ID\ID = ID" -unfolding cfun_eq_iff by simp + by (simp add: cfun_eq_iff) -lemma cfun_map_map: - "cfun_map\f1\g1\(cfun_map\f2\g2\p) = - cfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\p" -by (rule cfun_eqI) simp +lemma cfun_map_map: "cfun_map\f1\g1\(cfun_map\f2\g2\p) = cfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\p" + by (rule cfun_eqI) simp lemma ep_pair_cfun_map: assumes "ep_pair e1 p1" and "ep_pair e2 p2" @@ -34,9 +30,9 @@ proof interpret e1p1: ep_pair e1 p1 by fact interpret e2p2: ep_pair e2 p2 by fact - fix f show "cfun_map\e1\p2\(cfun_map\p1\e2\f) = f" + show "cfun_map\e1\p2\(cfun_map\p1\e2\f) = f" for f by (simp add: cfun_eq_iff) - fix g show "cfun_map\p1\e2\(cfun_map\e1\p2\g) \ g" + show "cfun_map\p1\e2\(cfun_map\e1\p2\g) \ g" for g apply (rule cfun_belowI, simp) apply (rule below_trans [OF e2p2.e_p_below]) apply (rule monofun_cfun_arg) @@ -79,13 +75,13 @@ proof (rule inj_onI, rule cfun_eqI, clarsimp) fix x f g assume "range (\x. (a\x, b\(f\(a\x)))) = range (\x. (a\x, b\(g\(a\x))))" - hence "range (\x. (a\x, b\(f\(a\x)))) \ range (\x. (a\x, b\(g\(a\x))))" + then have "range (\x. (a\x, b\(f\(a\x)))) \ range (\x. (a\x, b\(g\(a\x))))" by (rule equalityD1) - hence "(a\x, b\(f\(a\x))) \ range (\x. (a\x, b\(g\(a\x))))" + then have "(a\x, b\(f\(a\x))) \ range (\x. (a\x, b\(g\(a\x))))" by (simp add: subset_eq) then obtain y where "(a\x, b\(f\(a\x))) = (a\y, b\(g\(a\y)))" by (rule rangeE) - thus "b\(f\(a\x)) = b\(g\(a\x))" + then show "b\(f\(a\x)) = b\(g\(a\x))" by clarsimp qed qed @@ -97,41 +93,39 @@ interpret d1: finite_deflation d1 by fact interpret d2: finite_deflation d2 by fact have "deflation d1" and "deflation d2" by fact+ - thus "deflation (cfun_map\d1\d2)" by (rule deflation_cfun_map) + then show "deflation (cfun_map\d1\d2)" + by (rule deflation_cfun_map) have "finite (range (\f. cfun_map\d1\d2\f))" using d1.finite_range d2.finite_range by (rule finite_range_cfun_map) - thus "finite {f. cfun_map\d1\d2\f = f}" + then show "finite {f. cfun_map\d1\d2\f = f}" by (rule finite_range_imp_finite_fixes) qed text \Finite deflations are compact elements of the function space\ lemma finite_deflation_imp_compact: "finite_deflation d \ compact d" -apply (frule finite_deflation_imp_deflation) -apply (subgoal_tac "compact (cfun_map\d\d\d)") -apply (simp add: cfun_map_def deflation.idem eta_cfun) -apply (rule finite_deflation.compact) -apply (simp only: finite_deflation_cfun_map) -done + apply (frule finite_deflation_imp_deflation) + apply (subgoal_tac "compact (cfun_map\d\d\d)") + apply (simp add: cfun_map_def deflation.idem eta_cfun) + apply (rule finite_deflation.compact) + apply (simp only: finite_deflation_cfun_map) + done + subsection \Map operator for product type\ -definition - prod_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" -where - "prod_map = (\ f g p. (f\(fst p), g\(snd p)))" +definition prod_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" + where "prod_map = (\ f g p. (f\(fst p), g\(snd p)))" lemma prod_map_Pair [simp]: "prod_map\f\g\(x, y) = (f\x, g\y)" -unfolding prod_map_def by simp + by (simp add: prod_map_def) lemma prod_map_ID: "prod_map\ID\ID = ID" -unfolding cfun_eq_iff by auto + by (auto simp: cfun_eq_iff) -lemma prod_map_map: - "prod_map\f1\g1\(prod_map\f2\g2\p) = - prod_map\(\ x. f1\(f2\x))\(\ x. g1\(g2\x))\p" -by (induct p) simp +lemma prod_map_map: "prod_map\f1\g1\(prod_map\f2\g2\p) = prod_map\(\ x. f1\(f2\x))\(\ x. g1\(g2\x))\p" + by (induct p) simp lemma ep_pair_prod_map: assumes "ep_pair e1 p1" and "ep_pair e2 p2" @@ -139,9 +133,9 @@ proof interpret e1p1: ep_pair e1 p1 by fact interpret e2p2: ep_pair e2 p2 by fact - fix x show "prod_map\p1\p2\(prod_map\e1\e2\x) = x" + show "prod_map\p1\p2\(prod_map\e1\e2\x) = x" for x by (induct x) simp - fix y show "prod_map\e1\e2\(prod_map\p1\p2\y) \ y" + show "prod_map\e1\e2\(prod_map\p1\p2\y) \ y" for y by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below) qed @@ -165,91 +159,90 @@ interpret d1: finite_deflation d1 by fact interpret d2: finite_deflation d2 by fact have "deflation d1" and "deflation d2" by fact+ - thus "deflation (prod_map\d1\d2)" by (rule deflation_prod_map) + then show "deflation (prod_map\d1\d2)" by (rule deflation_prod_map) have "{p. prod_map\d1\d2\p = p} \ {x. d1\x = x} \ {y. d2\y = y}" - by clarsimp - thus "finite {p. prod_map\d1\d2\p = p}" + by auto + then show "finite {p. prod_map\d1\d2\p = p}" by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) qed + subsection \Map function for lifted cpo\ -definition - u_map :: "('a \ 'b) \ 'a u \ 'b u" -where - "u_map = (\ f. fup\(up oo f))" +definition u_map :: "('a \ 'b) \ 'a u \ 'b u" + where "u_map = (\ f. fup\(up oo f))" lemma u_map_strict [simp]: "u_map\f\\ = \" -unfolding u_map_def by simp + by (simp add: u_map_def) lemma u_map_up [simp]: "u_map\f\(up\x) = up\(f\x)" -unfolding u_map_def by simp + by (simp add: u_map_def) lemma u_map_ID: "u_map\ID = ID" -unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun) + by (simp add: u_map_def cfun_eq_iff eta_cfun) lemma u_map_map: "u_map\f\(u_map\g\p) = u_map\(\ x. f\(g\x))\p" -by (induct p) simp_all + by (induct p) simp_all lemma u_map_oo: "u_map\(f oo g) = u_map\f oo u_map\g" -by (simp add: cfcomp1 u_map_map eta_cfun) + by (simp add: cfcomp1 u_map_map eta_cfun) lemma ep_pair_u_map: "ep_pair e p \ ep_pair (u_map\e) (u_map\p)" -apply standard -apply (case_tac x, simp, simp add: ep_pair.e_inverse) -apply (case_tac y, simp, simp add: ep_pair.e_p_below) -done + apply standard + subgoal for x by (cases x, simp, simp add: ep_pair.e_inverse) + subgoal for y by (cases y, simp, simp add: ep_pair.e_p_below) + done lemma deflation_u_map: "deflation d \ deflation (u_map\d)" -apply standard -apply (case_tac x, simp, simp add: deflation.idem) -apply (case_tac x, simp, simp add: deflation.below) -done + apply standard + subgoal for x by (cases x, simp, simp add: deflation.idem) + subgoal for x by (cases x, simp, simp add: deflation.below) + done lemma finite_deflation_u_map: - assumes "finite_deflation d" shows "finite_deflation (u_map\d)" + assumes "finite_deflation d" + shows "finite_deflation (u_map\d)" proof (rule finite_deflation_intro) interpret d: finite_deflation d by fact have "deflation d" by fact - thus "deflation (u_map\d)" by (rule deflation_u_map) + then show "deflation (u_map\d)" + by (rule deflation_u_map) have "{x. u_map\d\x = x} \ insert \ ((\x. up\x) ` {x. d\x = x})" by (rule subsetI, case_tac x, simp_all) - thus "finite {x. u_map\d\x = x}" - by (rule finite_subset, simp add: d.finite_fixes) + then show "finite {x. u_map\d\x = x}" + by (rule finite_subset) (simp add: d.finite_fixes) qed + subsection \Map function for strict products\ default_sort pcpo -definition - sprod_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" -where - "sprod_map = (\ f g. ssplit\(\ x y. (:f\x, g\y:)))" +definition sprod_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" + where "sprod_map = (\ f g. ssplit\(\ x y. (:f\x, g\y:)))" lemma sprod_map_strict [simp]: "sprod_map\a\b\\ = \" -unfolding sprod_map_def by simp + by (simp add: sprod_map_def) -lemma sprod_map_spair [simp]: - "x \ \ \ y \ \ \ sprod_map\f\g\(:x, y:) = (:f\x, g\y:)" -by (simp add: sprod_map_def) +lemma sprod_map_spair [simp]: "x \ \ \ y \ \ \ sprod_map\f\g\(:x, y:) = (:f\x, g\y:)" + by (simp add: sprod_map_def) -lemma sprod_map_spair': - "f\\ = \ \ g\\ = \ \ sprod_map\f\g\(:x, y:) = (:f\x, g\y:)" -by (cases "x = \ \ y = \") auto +lemma sprod_map_spair': "f\\ = \ \ g\\ = \ \ sprod_map\f\g\(:x, y:) = (:f\x, g\y:)" + by (cases "x = \ \ y = \") auto lemma sprod_map_ID: "sprod_map\ID\ID = ID" -unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun) + by (simp add: sprod_map_def cfun_eq_iff eta_cfun) lemma sprod_map_map: "\f1\\ = \; g1\\ = \\ \ sprod_map\f1\g1\(sprod_map\f2\g2\p) = sprod_map\(\ x. f1\(f2\x))\(\ x. g1\(g2\x))\p" -apply (induct p, simp) -apply (case_tac "f2\x = \", simp) -apply (case_tac "g2\y = \", simp) -apply simp -done + apply (induct p) + apply simp + apply (case_tac "f2\x = \", simp) + apply (case_tac "g2\y = \", simp) + apply simp + done lemma ep_pair_sprod_map: assumes "ep_pair e1 p1" and "ep_pair e2 p2" @@ -257,10 +250,11 @@ proof interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact - fix x show "sprod_map\p1\p2\(sprod_map\e1\e2\x) = x" + show "sprod_map\p1\p2\(sprod_map\e1\e2\x) = x" for x by (induct x) simp_all - fix y show "sprod_map\e1\e2\(sprod_map\p1\p2\y) \ y" - apply (induct y, simp) + show "sprod_map\e1\e2\(sprod_map\p1\p2\y) \ y" for y + apply (induct y) + apply simp apply (case_tac "p1\x = \", simp, case_tac "p2\y = \", simp) apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below) done @@ -291,47 +285,48 @@ interpret d1: finite_deflation d1 by fact interpret d2: finite_deflation d2 by fact have "deflation d1" and "deflation d2" by fact+ - thus "deflation (sprod_map\d1\d2)" by (rule deflation_sprod_map) - have "{x. sprod_map\d1\d2\x = x} \ insert \ - ((\(x, y). (:x, y:)) ` ({x. d1\x = x} \ {y. d2\y = y}))" + then show "deflation (sprod_map\d1\d2)" + by (rule deflation_sprod_map) + have "{x. sprod_map\d1\d2\x = x} \ + insert \ ((\(x, y). (:x, y:)) ` ({x. d1\x = x} \ {y. d2\y = y}))" by (rule subsetI, case_tac x, auto simp add: spair_eq_iff) - thus "finite {x. sprod_map\d1\d2\x = x}" - by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) + then show "finite {x. sprod_map\d1\d2\x = x}" + by (rule finite_subset) (simp add: d1.finite_fixes d2.finite_fixes) qed + subsection \Map function for strict sums\ -definition - ssum_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" -where - "ssum_map = (\ f g. sscase\(sinl oo f)\(sinr oo g))" +definition ssum_map :: "('a \ 'b) \ ('c \ 'd) \ 'a \ 'c \ 'b \ 'd" + where "ssum_map = (\ f g. sscase\(sinl oo f)\(sinr oo g))" lemma ssum_map_strict [simp]: "ssum_map\f\g\\ = \" -unfolding ssum_map_def by simp + by (simp add: ssum_map_def) lemma ssum_map_sinl [simp]: "x \ \ \ ssum_map\f\g\(sinl\x) = sinl\(f\x)" -unfolding ssum_map_def by simp + by (simp add: ssum_map_def) lemma ssum_map_sinr [simp]: "x \ \ \ ssum_map\f\g\(sinr\x) = sinr\(g\x)" -unfolding ssum_map_def by simp + by (simp add: ssum_map_def) lemma ssum_map_sinl': "f\\ = \ \ ssum_map\f\g\(sinl\x) = sinl\(f\x)" -by (cases "x = \") simp_all + by (cases "x = \") simp_all lemma ssum_map_sinr': "g\\ = \ \ ssum_map\f\g\(sinr\x) = sinr\(g\x)" -by (cases "x = \") simp_all + by (cases "x = \") simp_all lemma ssum_map_ID: "ssum_map\ID\ID = ID" -unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun) + by (simp add: ssum_map_def cfun_eq_iff eta_cfun) lemma ssum_map_map: "\f1\\ = \; g1\\ = \\ \ ssum_map\f1\g1\(ssum_map\f2\g2\p) = ssum_map\(\ x. f1\(f2\x))\(\ x. g1\(g2\x))\p" -apply (induct p, simp) -apply (case_tac "f2\x = \", simp, simp) -apply (case_tac "g2\y = \", simp, simp) -done + apply (induct p) + apply simp + apply (case_tac "f2\x = \", simp, simp) + apply (case_tac "g2\y = \", simp, simp) + done lemma ep_pair_ssum_map: assumes "ep_pair e1 p1" and "ep_pair e2 p2" @@ -339,11 +334,12 @@ proof interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact - fix x show "ssum_map\p1\p2\(ssum_map\e1\e2\x) = x" + show "ssum_map\p1\p2\(ssum_map\e1\e2\x) = x" for x by (induct x) simp_all - fix y show "ssum_map\e1\e2\(ssum_map\p1\p2\y) \ y" - apply (induct y, simp) - apply (case_tac "p1\x = \", simp, simp add: e1p1.e_p_below) + show "ssum_map\e1\e2\(ssum_map\p1\p2\y) \ y" for y + apply (induct y) + apply simp + apply (case_tac "p1\x = \", simp, simp add: e1p1.e_p_below) apply (case_tac "p2\y = \", simp, simp add: e2p2.e_p_below) done qed @@ -374,32 +370,30 @@ interpret d1: finite_deflation d1 by fact interpret d2: finite_deflation d2 by fact have "deflation d1" and "deflation d2" by fact+ - thus "deflation (ssum_map\d1\d2)" by (rule deflation_ssum_map) + then show "deflation (ssum_map\d1\d2)" + by (rule deflation_ssum_map) have "{x. ssum_map\d1\d2\x = x} \ (\x. sinl\x) ` {x. d1\x = x} \ (\x. sinr\x) ` {x. d2\x = x} \ {\}" by (rule subsetI, case_tac x, simp_all) - thus "finite {x. ssum_map\d1\d2\x = x}" + then show "finite {x. ssum_map\d1\d2\x = x}" by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) qed + subsection \Map operator for strict function space\ -definition - sfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \! 'c) \ ('b \! 'd)" -where - "sfun_map = (\ a b. sfun_abs oo cfun_map\a\b oo sfun_rep)" +definition sfun_map :: "('b \ 'a) \ ('c \ 'd) \ ('a \! 'c) \ ('b \! 'd)" + where "sfun_map = (\ a b. sfun_abs oo cfun_map\a\b oo sfun_rep)" lemma sfun_map_ID: "sfun_map\ID\ID = ID" - unfolding sfun_map_def - by (simp add: cfun_map_ID cfun_eq_iff) + by (simp add: sfun_map_def cfun_map_ID cfun_eq_iff) lemma sfun_map_map: - assumes "f2\\ = \" and "g2\\ = \" shows - "sfun_map\f1\g1\(sfun_map\f2\g2\p) = + assumes "f2\\ = \" and "g2\\ = \" + shows "sfun_map\f1\g1\(sfun_map\f2\g2\p) = sfun_map\(\ x. f2\(f1\x))\(\ x. g1\(g2\x))\p" -unfolding sfun_map_def -by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map) + by (simp add: sfun_map_def cfun_eq_iff strictify_cancel assms cfun_map_map) lemma ep_pair_sfun_map: assumes 1: "ep_pair e1 p1" @@ -410,13 +404,13 @@ unfolding pcpo_ep_pair_def by fact interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact - fix f show "sfun_map\e1\p2\(sfun_map\p1\e2\f) = f" + show "sfun_map\e1\p2\(sfun_map\p1\e2\f) = f" for f unfolding sfun_map_def apply (simp add: sfun_eq_iff strictify_cancel) apply (rule ep_pair.e_inverse) apply (rule ep_pair_cfun_map [OF 1 2]) done - fix g show "sfun_map\p1\e2\(sfun_map\e1\p2\g) \ g" + show "sfun_map\p1\e2\(sfun_map\e1\p2\g) \ g" for g unfolding sfun_map_def apply (simp add: sfun_below_iff strictify_cancel) apply (rule ep_pair.e_p_below) @@ -428,40 +422,39 @@ assumes 1: "deflation d1" assumes 2: "deflation d2" shows "deflation (sfun_map\d1\d2)" -apply (simp add: sfun_map_def) -apply (rule deflation.intro) -apply simp -apply (subst strictify_cancel) -apply (simp add: cfun_map_def deflation_strict 1 2) -apply (simp add: cfun_map_def deflation.idem 1 2) -apply (simp add: sfun_below_iff) -apply (subst strictify_cancel) -apply (simp add: cfun_map_def deflation_strict 1 2) -apply (rule deflation.below) -apply (rule deflation_cfun_map [OF 1 2]) -done + apply (simp add: sfun_map_def) + apply (rule deflation.intro) + apply simp + apply (subst strictify_cancel) + apply (simp add: cfun_map_def deflation_strict 1 2) + apply (simp add: cfun_map_def deflation.idem 1 2) + apply (simp add: sfun_below_iff) + apply (subst strictify_cancel) + apply (simp add: cfun_map_def deflation_strict 1 2) + apply (rule deflation.below) + apply (rule deflation_cfun_map [OF 1 2]) + done lemma finite_deflation_sfun_map: - assumes 1: "finite_deflation d1" - assumes 2: "finite_deflation d2" + assumes "finite_deflation d1" + and "finite_deflation d2" shows "finite_deflation (sfun_map\d1\d2)" proof (intro finite_deflation_intro) interpret d1: finite_deflation d1 by fact interpret d2: finite_deflation d2 by fact have "deflation d1" and "deflation d2" by fact+ - thus "deflation (sfun_map\d1\d2)" by (rule deflation_sfun_map) - from 1 2 have "finite_deflation (cfun_map\d1\d2)" + then show "deflation (sfun_map\d1\d2)" + by (rule deflation_sfun_map) + from assms have "finite_deflation (cfun_map\d1\d2)" by (rule finite_deflation_cfun_map) then have "finite {f. cfun_map\d1\d2\f = f}" by (rule finite_deflation.finite_fixes) moreover have "inj (\f. sfun_rep\f)" - by (rule inj_onI, simp add: sfun_eq_iff) + by (rule inj_onI) (simp add: sfun_eq_iff) ultimately have "finite ((\f. sfun_rep\f) -` {f. cfun_map\d1\d2\f = f})" by (rule finite_vimageI) - then show "finite {f. sfun_map\d1\d2\f = f}" - unfolding sfun_map_def sfun_eq_iff - by (simp add: strictify_cancel - deflation_strict \deflation d1\ \deflation d2\) + with \deflation d1\ \deflation d2\ show "finite {f. sfun_map\d1\d2\f = f}" + by (simp add: sfun_map_def sfun_eq_iff strictify_cancel deflation_strict) qed end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/One.thy --- a/src/HOL/HOLCF/One.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/One.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,69 +5,67 @@ section \The unit domain\ theory One -imports Lift + imports Lift begin -type_synonym - one = "unit lift" +type_synonym one = "unit lift" translations - (type) "one" <= (type) "unit lift" + (type) "one" \ (type) "unit lift" definition ONE :: "one" - where "ONE == Def ()" + where "ONE \ Def ()" text \Exhaustion and Elimination for type @{typ one}\ lemma Exh_one: "t = \ \ t = ONE" -unfolding ONE_def by (induct t) simp_all + by (induct t) (simp_all add: ONE_def) lemma oneE [case_names bottom ONE]: "\p = \ \ Q; p = ONE \ Q\ \ Q" -unfolding ONE_def by (induct p) simp_all + by (induct p) (simp_all add: ONE_def) -lemma one_induct [case_names bottom ONE]: "\P \; P ONE\ \ P x" -by (cases x rule: oneE) simp_all +lemma one_induct [case_names bottom ONE]: "P \ \ P ONE \ P x" + by (cases x rule: oneE) simp_all lemma dist_below_one [simp]: "ONE \ \" -unfolding ONE_def by simp + by (simp add: ONE_def) lemma below_ONE [simp]: "x \ ONE" -by (induct x rule: one_induct) simp_all + by (induct x rule: one_induct) simp_all lemma ONE_below_iff [simp]: "ONE \ x \ x = ONE" -by (induct x rule: one_induct) simp_all + by (induct x rule: one_induct) simp_all lemma ONE_defined [simp]: "ONE \ \" -unfolding ONE_def by simp + by (simp add: ONE_def) lemma one_neq_iffs [simp]: "x \ ONE \ x = \" "ONE \ x \ x = \" "x \ \ \ x = ONE" "\ \ x \ x = ONE" -by (induct x rule: one_induct) simp_all + by (induct x rule: one_induct) simp_all lemma compact_ONE: "compact ONE" -by (rule compact_chfin) + by (rule compact_chfin) text \Case analysis function for type @{typ one}\ -definition - one_case :: "'a::pcpo \ one \ 'a" where - "one_case = (\ a x. seq\x\a)" +definition one_case :: "'a::pcpo \ one \ 'a" + where "one_case = (\ a x. seq\x\a)" translations - "case x of XCONST ONE \ t" == "CONST one_case\t\x" - "case x of XCONST ONE :: 'a \ t" => "CONST one_case\t\x" - "\ (XCONST ONE). t" == "CONST one_case\t" + "case x of XCONST ONE \ t" \ "CONST one_case\t\x" + "case x of XCONST ONE :: 'a \ t" \ "CONST one_case\t\x" + "\ (XCONST ONE). t" \ "CONST one_case\t" lemma one_case1 [simp]: "(case \ of ONE \ t) = \" -by (simp add: one_case_def) + by (simp add: one_case_def) lemma one_case2 [simp]: "(case ONE of ONE \ t) = t" -by (simp add: one_case_def) + by (simp add: one_case_def) lemma one_case3 [simp]: "(case x of ONE \ ONE) = x" -by (induct x rule: one_induct) simp_all + by (induct x rule: one_induct) simp_all end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Pcpo.thy --- a/src/HOL/HOLCF/Pcpo.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Pcpo.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,7 +5,7 @@ section \Classes cpo and pcpo\ theory Pcpo -imports Porder + imports Porder begin subsection \Complete partial orders\ @@ -29,8 +29,7 @@ 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" +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)" @@ -42,63 +41,56 @@ 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_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 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 +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) +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)" +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 + 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)" @@ -108,7 +100,7 @@ have 3: "chain (\i. Y i i)" apply (rule chainI) apply (rule below_trans) - apply (rule chainE [OF 1]) + apply (rule chainE [OF 1]) apply (rule chainE [OF 2]) done have 4: "chain (\i. \j. Y i j)" @@ -118,7 +110,7 @@ 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 1 max.cobounded1]) apply (rule chain_mono [OF 2 max.cobounded2]) done show "(\i. Y i i) \ (\i. \j. Y i j)" @@ -135,6 +127,7 @@ end + subsection \Pointed cpos\ text \The class pcpo of pointed cpos\ @@ -147,44 +140,39 @@ 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 + 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:\ syntax UU :: logic - -translations "UU" => "CONST bottom" +translations "UU" \ "CONST bottom" text \Simproc to rewrite @{term "\ = x"} to @{term "x = \"}.\ - -setup \ - Reorient_Proc.add - (fn Const(@{const_name bottom}, _) => true | _ => false) -\ - +setup \Reorient_Proc.add (fn Const(\<^const_name>\bottom\, _) => true | _ => false)\ simproc_setup reorient_bottom ("\ = x") = Reorient_Proc.proc text \useful lemmas about @{term \}\ -lemma below_bottom_iff [simp]: "(x \ \) = (x = \)" -by (simp add: po_eq_conv) +lemma below_bottom_iff [simp]: "x \ \ \ x = \" + by (simp add: po_eq_conv) -lemma eq_bottom_iff: "(x = \) = (x \ \)" -by simp +lemma eq_bottom_iff: "x = \ \ x \ \" + by simp lemma bottomI: "x \ \ \ x = \" -by (subst eq_bottom_iff) + 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) + by (simp only: eq_bottom_iff lub_below_iff) + subsection \Chain-finite and flat cpos\ @@ -195,10 +183,10 @@ begin subclass cpo -apply standard -apply (frule chfin) -apply (blast intro: lub_finch1) -done + 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) @@ -210,19 +198,18 @@ begin subclass chfin -apply standard -apply (unfold max_in_chain_def) -apply (case_tac "\i. Y i = \") -apply simp -apply simp -apply (erule exE) -apply (rule_tac x="i" in exI) -apply clarify -apply (blast dest: chain_mono ax_flat) -done + apply standard + apply (unfold max_in_chain_def) + apply (case_tac "\i. Y i = \") + apply simp + apply simp + apply (erule exE) + apply (rule_tac x="i" in exI) + apply clarify + apply (blast dest: chain_mono ax_flat) + done -lemma flat_below_iff: - shows "(x \ y) = (x = \ \ x = y)" +lemma flat_below_iff: "x \ y \ x = \ \ x = y" by (safe dest!: ax_flat) lemma flat_eq: "a \ \ \ a \ b = (a = b)" @@ -237,7 +224,7 @@ begin subclass po -proof qed simp_all + by standard simp_all text \In a discrete cpo, every chain is constant\ @@ -246,19 +233,20 @@ shows "\x. S = (\i. x)" proof (intro exI ext) fix i :: nat - have "S 0 \ S i" using S le0 by (rule chain_mono) - hence "S 0 = S i" by simp - thus "S i = S 0" by (rule sym) + 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" - hence "\x. S = (\i. x)" by (rule discrete_chain_const) - hence "max_in_chain 0 S" - unfolding max_in_chain_def by auto - thus "\i. max_in_chain i 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 diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Porder.thy --- a/src/HOL/HOLCF/Porder.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Porder.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,7 +5,7 @@ section \Partial orders\ theory Porder -imports Main + imports Main begin declare [[typedef_overloaded]] @@ -23,17 +23,16 @@ notation below (infix "\" 50) -abbreviation - not_below :: "'a \ 'a \ bool" (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" +lemma below_eq_trans: "a \ b \ b = c \ a \ c" by (rule subst) -lemma eq_below_trans: "\a = b; b \ c\ \ a \ c" +lemma eq_below_trans: "a = b \ b \ c \ a \ c" by (rule ssubst) end @@ -72,8 +71,8 @@ subsection \Upper bounds\ -definition is_ub :: "'a set \ 'a \ bool" (infix "<|" 55) where - "S <| x \ (\y\S. y \ x)" +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) @@ -102,13 +101,14 @@ 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 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)" +definition lub :: "'a set \ 'a" + where "lub S = (THE x. S <<| x)" end @@ -119,14 +119,13 @@ "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" ("(3\_\_./ _)" [0,0, 10] 10) translations - "LUB x:A. t" == "CONST lub ((%x. t) ` A)" + "LUB x:A. t" \ "CONST lub ((\x. t) ` A)" context po begin -abbreviation - Lub (binder "\" 10) where - "\n. t n == lub (range t)" +abbreviation Lub (binder "\" 10) + where "\n. t n \ lub (range t)" notation (ASCII) Lub (binder "LUB " 10) @@ -147,7 +146,7 @@ text \lubs are unique\ -lemma is_lub_unique: "\S <<| x; S <<| y\ \ x = y" +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}\ @@ -170,16 +169,17 @@ 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" +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" +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!\ +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" @@ -190,11 +190,11 @@ text \chains are monotone functions\ -lemma chain_mono_less: "\chain Y; i < j\ \ Y i \ Y j" +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, simp add: chain_mono_less) +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) @@ -204,20 +204,18 @@ 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_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" +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\ @@ -231,61 +229,60 @@ 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\ +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))" +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" +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" +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" +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_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 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 (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 - apply simp -done + done lemma finite_range_has_max: - fixes f :: "nat \ 'a" and r :: "'a \ 'a \ bool" + 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)" @@ -307,38 +304,35 @@ 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) +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 (erule spec) - apply (rule finite_range_has_max) - apply (erule (1) chain_mono) - apply assumption -done + apply assumption + done lemma bin_chain: "x \ y \ chain (\i. if i=0 then x else y)" - by (rule chainI, simp) + by (rule chainI) simp -lemma bin_chainmax: - "x \ y \ max_in_chain (Suc 0) (\i. if i=0 then x else y)" - unfolding max_in_chain_def by 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 +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" +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 diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Product_Cpo.thy --- a/src/HOL/HOLCF/Product_Cpo.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Product_Cpo.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,26 +5,26 @@ section \The cpo of cartesian products\ theory Product_Cpo -imports Adm + 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" +definition below_unit_def [simp]: "x \ (y::unit) \ True" -instance proof -qed simp +instance + by standard simp end instance unit :: pcpo -by intro_classes simp + by standard simp subsection \Product type is a partial order\ @@ -32,182 +32,185 @@ instantiation prod :: (below, below) below begin -definition - below_prod_def: "(op \) \ \p1 p2. (fst p1 \ fst p2 \ snd p1 \ snd p2)" +definition below_prod_def: "(op \) \ \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" - unfolding below_prod_def by simp + by (simp add: below_prod_def) next fix x y :: "'a \ 'b" - assume "x \ y" "y \ x" thus "x = y" + 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" thus "x \ z" + 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" -unfolding below_prod_def by simp +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" -unfolding below_prod_def by simp + 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) + by (simp add: monofun_def) lemma monofun_pair2: "monofun (\y. (x, y))" -by (simp add: monofun_def) + by (simp add: monofun_def) -lemma monofun_pair: - "\x1 \ x2; y1 \ y2\ \ (x1, y1) \ (x2, y2)" -by simp +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) +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" -unfolding below_prod_def by simp + by (simp add: below_prod_def) lemma snd_monofun: "x \ y \ snd x \ snd y" -unfolding below_prod_def by simp + by (simp add: below_prod_def) lemma monofun_fst: "monofun fst" -by (simp add: monofun_def below_prod_def) + by (simp add: monofun_def below_prod_def) lemma monofun_snd: "monofun snd" -by (simp add: monofun_def below_prod_def) + 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 Y" + assumes chain: "chain Y" obtains A B where "chain A" and "chain B" and "Y = (\i. (A i, B i))" proof - from \chain Y\ show "chain (\i. fst (Y i))" by (rule ch2ch_fst) - from \chain Y\ show "chain (\i. snd (Y i))" by (rule ch2ch_snd) - show "Y = (\i. (fst (Y i), snd (Y i)))" by simp + 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)" -unfolding is_lub_def is_ub_def ball_simps below_prod_def by simp +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::nat \ 'a::cpo); chain (B::nat \ 'b::cpo)\ - \ (\i. (A i, B i)) = (\i. A i, \i. B i)" -by (fast intro: lub_eqI is_lub_Pair elim: thelubE) +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 S: "chain S" + assumes "chain S" shows "range S <<| (\i. fst (S i), \i. snd (S i))" -using S by (auto elim: prod_chain_cases simp add: is_lub_Pair cpo_lubI) + using assms by (auto elim: prod_chain_cases simp: is_lub_Pair cpo_lubI) -lemma lub_prod: - "chain (S::nat \ 'a::cpo \ 'b::cpo) - \ (\i. S i) = (\i. fst (S i), \i. snd (S i))" -by (rule is_lub_prod [THEN lub_eqI]) +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" - hence "range S <<| (\i. fst (S i), \i. snd (S i))" + then have "range S <<| (\i. fst (S i), \i. snd (S i))" by (rule is_lub_prod) - thus "\x. range S <<| x" .. + 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" - unfolding below_prod_def prod_eq_iff - by simp + 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) + by (simp add: below_prod_def) instance prod :: (pcpo, pcpo) pcpo -by intro_classes (fast intro: minimal_prod) + by intro_classes (fast intro: minimal_prod) lemma inst_prod_pcpo: "\ = (\, \)" -by (rule minimal_prod [THEN bottomI, symmetric]) + by (rule minimal_prod [THEN bottomI, symmetric]) lemma Pair_bottom_iff [simp]: "(x, y) = \ \ x = \ \ y = \" -unfolding inst_prod_pcpo by simp + by (simp add: inst_prod_pcpo) lemma fst_strict [simp]: "fst \ = \" -unfolding inst_prod_pcpo by (rule fst_conv) + unfolding inst_prod_pcpo by (rule fst_conv) lemma snd_strict [simp]: "snd \ = \" -unfolding inst_prod_pcpo by (rule snd_conv) + unfolding inst_prod_pcpo by (rule snd_conv) lemma Pair_strict [simp]: "(\, \) = \" -by simp + by simp lemma split_strict [simp]: "case_prod f \ = f \ \" -unfolding split_def by simp + 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 + 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 + 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 + 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 + 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 + 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] @@ -219,13 +222,13 @@ 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 + 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))" @@ -234,66 +237,68 @@ proof - have "cont (\(x, y). f (x, y))" by (intro cont2cont_case_prod f1 f2 cont2cont) - thus "cont f" + 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 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) + 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 + 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 . + unfolding case_prod_beta using assms . + subsection \Compactness and chain-finiteness\ -lemma fst_below_iff: "fst (x::'a \ 'b) \ y \ x \ (y, snd x)" -unfolding below_prod_def by simp +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::'a \ 'b) \ y \ x \ (fst x, y)" -unfolding below_prod_def by simp +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) + by (rule compactI) (simp add: fst_below_iff) lemma compact_snd: "compact x \ compact (snd x)" -by (rule compactI, simp add: snd_below_iff) + 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: "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 + 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 + apply intro_classes + apply (erule compact_imp_max_in_chain) + apply (case_tac "\i. Y i", simp) + done end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Sfun.thy --- a/src/HOL/HOLCF/Sfun.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Sfun.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,30 +5,25 @@ section \The Strict Function Type\ theory Sfun -imports Cfun + imports Cfun begin -pcpodef ('a, 'b) sfun (infixr "\!" 0) - = "{f :: 'a \ 'b. f\\ = \}" -by simp_all +pcpodef ('a, 'b) sfun (infixr "\!" 0) = "{f :: 'a \ 'b. f\\ = \}" + by simp_all type_notation (ASCII) sfun (infixr "->!" 0) text \TODO: Define nice syntax for abstraction, application.\ -definition - sfun_abs :: "('a \ 'b) \ ('a \! 'b)" -where - "sfun_abs = (\ f. Abs_sfun (strictify\f))" +definition sfun_abs :: "('a \ 'b) \ ('a \! 'b)" + where "sfun_abs = (\ f. Abs_sfun (strictify\f))" -definition - sfun_rep :: "('a \! 'b) \ 'a \ 'b" -where - "sfun_rep = (\ f. Rep_sfun f)" +definition sfun_rep :: "('a \! 'b) \ 'a \ 'b" + where "sfun_rep = (\ f. Rep_sfun f)" lemma sfun_rep_beta: "sfun_rep\f = Rep_sfun f" - unfolding sfun_rep_def by (simp add: cont_Rep_sfun) + by (simp add: sfun_rep_def cont_Rep_sfun) lemma sfun_rep_strict1 [simp]: "sfun_rep\\ = \" unfolding sfun_rep_beta by (rule Rep_sfun_strict) @@ -54,9 +49,9 @@ done lemma sfun_eq_iff: "f = g \ sfun_rep\f = sfun_rep\g" -by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject) + by (simp add: sfun_rep_def cont_Rep_sfun Rep_sfun_inject) lemma sfun_below_iff: "f \ g \ sfun_rep\f \ sfun_rep\g" -by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def) + by (simp add: sfun_rep_def cont_Rep_sfun below_sfun_def) end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Sprod.thy --- a/src/HOL/HOLCF/Sprod.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Sprod.thy Mon Jan 01 23:07:24 2018 +0100 @@ -6,20 +6,21 @@ section \The type of strict products\ theory Sprod -imports Cfun + imports Cfun begin default_sort pcpo + subsection \Definition of strict product type\ definition "sprod = {p::'a \ 'b. p = \ \ (fst p \ \ \ snd p \ \)}" pcpodef ('a, 'b) sprod ("(_ \/ _)" [21,20] 20) = "sprod :: ('a \ 'b) set" - unfolding sprod_def by simp_all + by (simp_all add: sprod_def) instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin -by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) + by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) type_notation (ASCII) sprod (infixr "**" 20) @@ -27,39 +28,34 @@ subsection \Definitions of constants\ -definition - sfst :: "('a ** 'b) \ 'a" where - "sfst = (\ p. fst (Rep_sprod p))" +definition sfst :: "('a ** 'b) \ 'a" + where "sfst = (\ p. fst (Rep_sprod p))" -definition - ssnd :: "('a ** 'b) \ 'b" where - "ssnd = (\ p. snd (Rep_sprod p))" +definition ssnd :: "('a ** 'b) \ 'b" + where "ssnd = (\ p. snd (Rep_sprod p))" -definition - spair :: "'a \ 'b \ ('a ** 'b)" where - "spair = (\ a b. Abs_sprod (seq\b\a, seq\a\b))" +definition spair :: "'a \ 'b \ ('a ** 'b)" + where "spair = (\ a b. Abs_sprod (seq\b\a, seq\a\b))" -definition - ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" where - "ssplit = (\ f p. seq\p\(f\(sfst\p)\(ssnd\p)))" +definition ssplit :: "('a \ 'b \ 'c) \ ('a ** 'b) \ 'c" + where "ssplit = (\ f p. seq\p\(f\(sfst\p)\(ssnd\p)))" -syntax - "_stuple" :: "[logic, args] \ logic" ("(1'(:_,/ _:'))") +syntax "_stuple" :: "[logic, args] \ logic" ("(1'(:_,/ _:'))") +translations + "(:x, y, z:)" \ "(:x, (:y, z:):)" + "(:x, y:)" \ "CONST spair\x\y" translations - "(:x, y, z:)" == "(:x, (:y, z:):)" - "(:x, y:)" == "CONST spair\x\y" + "\(CONST spair\x\y). t" \ "CONST ssplit\(\ x y. t)" -translations - "\(CONST spair\x\y). t" == "CONST ssplit\(\ x y. t)" subsection \Case analysis\ lemma spair_sprod: "(seq\b\a, seq\a\b) \ sprod" -by (simp add: sprod_def seq_conv_if) + by (simp add: sprod_def seq_conv_if) lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\b\a, seq\a\b)" -by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod) + by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod) lemmas Rep_sprod_simps = Rep_sprod_inject [symmetric] below_sprod_def @@ -68,144 +64,139 @@ lemma sprodE [case_names bottom spair, cases type: sprod]: obtains "p = \" | x y where "p = (:x, y:)" and "x \ \" and "y \ \" -using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps) + using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps) lemma sprod_induct [case_names bottom spair, induct type: sprod]: "\P \; \x y. \x \ \; y \ \\ \ P (:x, y:)\ \ P x" -by (cases x, simp_all) + by (cases x) simp_all + subsection \Properties of \emph{spair}\ lemma spair_strict1 [simp]: "(:\, y:) = \" -by (simp add: Rep_sprod_simps) + by (simp add: Rep_sprod_simps) lemma spair_strict2 [simp]: "(:x, \:) = \" -by (simp add: Rep_sprod_simps) + by (simp add: Rep_sprod_simps) -lemma spair_bottom_iff [simp]: "((:x, y:) = \) = (x = \ \ y = \)" -by (simp add: Rep_sprod_simps seq_conv_if) +lemma spair_bottom_iff [simp]: "(:x, y:) = \ \ x = \ \ y = \" + by (simp add: Rep_sprod_simps seq_conv_if) -lemma spair_below_iff: - "((:a, b:) \ (:c, d:)) = (a = \ \ b = \ \ (a \ c \ b \ d))" -by (simp add: Rep_sprod_simps seq_conv_if) +lemma spair_below_iff: "(:a, b:) \ (:c, d:) \ a = \ \ b = \ \ (a \ c \ b \ d)" + by (simp add: Rep_sprod_simps seq_conv_if) -lemma spair_eq_iff: - "((:a, b:) = (:c, d:)) = - (a = c \ b = d \ (a = \ \ b = \) \ (c = \ \ d = \))" -by (simp add: Rep_sprod_simps seq_conv_if) +lemma spair_eq_iff: "(:a, b:) = (:c, d:) \ a = c \ b = d \ (a = \ \ b = \) \ (c = \ \ d = \)" + by (simp add: Rep_sprod_simps seq_conv_if) lemma spair_strict: "x = \ \ y = \ \ (:x, y:) = \" -by simp + by simp lemma spair_strict_rev: "(:x, y:) \ \ \ x \ \ \ y \ \" -by simp + by simp lemma spair_defined: "\x \ \; y \ \\ \ (:x, y:) \ \" -by simp + by simp lemma spair_defined_rev: "(:x, y:) = \ \ x = \ \ y = \" -by simp + by simp -lemma spair_below: - "\x \ \; y \ \\ \ (:x, y:) \ (:a, b:) = (x \ a \ y \ b)" -by (simp add: spair_below_iff) +lemma spair_below: "x \ \ \ y \ \ \ (:x, y:) \ (:a, b:) \ x \ a \ y \ b" + by (simp add: spair_below_iff) -lemma spair_eq: - "\x \ \; y \ \\ \ ((:x, y:) = (:a, b:)) = (x = a \ y = b)" -by (simp add: spair_eq_iff) +lemma spair_eq: "x \ \ \ y \ \ \ (:x, y:) = (:a, b:) \ x = a \ y = b" + by (simp add: spair_eq_iff) -lemma spair_inject: - "\x \ \; y \ \; (:x, y:) = (:a, b:)\ \ x = a \ y = b" -by (rule spair_eq [THEN iffD1]) +lemma spair_inject: "x \ \ \ y \ \ \ (:x, y:) = (:a, b:) \ x = a \ y = b" + by (rule spair_eq [THEN iffD1]) lemma inst_sprod_pcpo2: "\ = (:\, \:)" -by simp + by simp lemma sprodE2: "(\x y. p = (:x, y:) \ Q) \ Q" -by (cases p, simp only: inst_sprod_pcpo2, simp) + by (cases p) (simp only: inst_sprod_pcpo2, simp) + subsection \Properties of \emph{sfst} and \emph{ssnd}\ lemma sfst_strict [simp]: "sfst\\ = \" -by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict) + by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict) lemma ssnd_strict [simp]: "ssnd\\ = \" -by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict) + by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict) lemma sfst_spair [simp]: "y \ \ \ sfst\(:x, y:) = x" -by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair) + by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair) lemma ssnd_spair [simp]: "x \ \ \ ssnd\(:x, y:) = y" -by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair) + by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair) -lemma sfst_bottom_iff [simp]: "(sfst\p = \) = (p = \)" -by (cases p, simp_all) +lemma sfst_bottom_iff [simp]: "sfst\p = \ \ p = \" + by (cases p) simp_all -lemma ssnd_bottom_iff [simp]: "(ssnd\p = \) = (p = \)" -by (cases p, simp_all) +lemma ssnd_bottom_iff [simp]: "ssnd\p = \ \ p = \" + by (cases p) simp_all lemma sfst_defined: "p \ \ \ sfst\p \ \" -by simp + by simp lemma ssnd_defined: "p \ \ \ ssnd\p \ \" -by simp + by simp lemma spair_sfst_ssnd: "(:sfst\p, ssnd\p:) = p" -by (cases p, simp_all) + by (cases p) simp_all -lemma below_sprod: "(x \ y) = (sfst\x \ sfst\y \ ssnd\x \ ssnd\y)" -by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod) +lemma below_sprod: "x \ y \ sfst\x \ sfst\y \ ssnd\x \ ssnd\y" + by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod) -lemma eq_sprod: "(x = y) = (sfst\x = sfst\y \ ssnd\x = ssnd\y)" -by (auto simp add: po_eq_conv below_sprod) +lemma eq_sprod: "x = y \ sfst\x = sfst\y \ ssnd\x = ssnd\y" + by (auto simp add: po_eq_conv below_sprod) lemma sfst_below_iff: "sfst\x \ y \ x \ (:y, ssnd\x:)" -apply (cases "x = \", simp, cases "y = \", simp) -apply (simp add: below_sprod) -done + by (cases "x = \", simp, cases "y = \", simp, simp add: below_sprod) lemma ssnd_below_iff: "ssnd\x \ y \ x \ (:sfst\x, y:)" -apply (cases "x = \", simp, cases "y = \", simp) -apply (simp add: below_sprod) -done + by (cases "x = \", simp, cases "y = \", simp, simp add: below_sprod) + subsection \Compactness\ lemma compact_sfst: "compact x \ compact (sfst\x)" -by (rule compactI, simp add: sfst_below_iff) + by (rule compactI) (simp add: sfst_below_iff) lemma compact_ssnd: "compact x \ compact (ssnd\x)" -by (rule compactI, simp add: ssnd_below_iff) + by (rule compactI) (simp add: ssnd_below_iff) -lemma compact_spair: "\compact x; compact y\ \ compact (:x, y:)" -by (rule compact_sprod, simp add: Rep_sprod_spair seq_conv_if) +lemma compact_spair: "compact x \ compact y \ compact (:x, y:)" + by (rule compact_sprod) (simp add: Rep_sprod_spair seq_conv_if) -lemma compact_spair_iff: - "compact (:x, y:) = (x = \ \ y = \ \ (compact x \ compact y))" -apply (safe elim!: compact_spair) -apply (drule compact_sfst, simp) -apply (drule compact_ssnd, simp) -apply simp -apply simp -done +lemma compact_spair_iff: "compact (:x, y:) \ x = \ \ y = \ \ (compact x \ compact y)" + apply (safe elim!: compact_spair) + apply (drule compact_sfst, simp) + apply (drule compact_ssnd, simp) + apply simp + apply simp + done + subsection \Properties of \emph{ssplit}\ lemma ssplit1 [simp]: "ssplit\f\\ = \" -by (simp add: ssplit_def) + by (simp add: ssplit_def) -lemma ssplit2 [simp]: "\x \ \; y \ \\ \ ssplit\f\(:x, y:) = f\x\y" -by (simp add: ssplit_def) +lemma ssplit2 [simp]: "x \ \ \ y \ \ \ ssplit\f\(:x, y:) = f\x\y" + by (simp add: ssplit_def) lemma ssplit3 [simp]: "ssplit\spair\z = z" -by (cases z, simp_all) + by (cases z) simp_all + subsection \Strict product preserves flatness\ instance sprod :: (flat, flat) flat proof fix x y :: "'a \ 'b" - assume "x \ y" thus "x = \ \ x = y" + assume "x \ y" + then show "x = \ \ x = y" apply (induct x, simp) apply (induct y, simp) apply (simp add: spair_below_iff flat_below_iff) diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Ssum.thy --- a/src/HOL/HOLCF/Ssum.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Ssum.thy Mon Jan 01 23:07:24 2018 +0100 @@ -6,24 +6,24 @@ section \The type of strict sums\ theory Ssum -imports Tr + imports Tr begin default_sort pcpo + subsection \Definition of strict sum type\ -definition - "ssum = - {p :: tr \ ('a \ 'b). p = \ \ - (fst p = TT \ fst (snd p) \ \ \ snd (snd p) = \) \ - (fst p = FF \ fst (snd p) = \ \ snd (snd p) \ \)}" +definition "ssum = + {p :: tr \ ('a \ 'b). p = \ \ + (fst p = TT \ fst (snd p) \ \ \ snd (snd p) = \) \ + (fst p = FF \ fst (snd p) = \ \ snd (snd p) \ \)}" pcpodef ('a, 'b) ssum ("(_ \/ _)" [21, 20] 20) = "ssum :: (tr \ 'a \ 'b) set" - unfolding ssum_def by simp_all + by (simp_all add: ssum_def) instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin -by (rule typedef_chfin [OF type_definition_ssum below_ssum_def]) + by (rule typedef_chfin [OF type_definition_ssum below_ssum_def]) type_notation (ASCII) ssum (infixr "++" 10) @@ -31,108 +31,108 @@ subsection \Definitions of constructors\ -definition - sinl :: "'a \ ('a ++ 'b)" where - "sinl = (\ a. Abs_ssum (seq\a\TT, a, \))" +definition sinl :: "'a \ ('a ++ 'b)" + where "sinl = (\ a. Abs_ssum (seq\a\TT, a, \))" -definition - sinr :: "'b \ ('a ++ 'b)" where - "sinr = (\ b. Abs_ssum (seq\b\FF, \, b))" +definition sinr :: "'b \ ('a ++ 'b)" + where "sinr = (\ b. Abs_ssum (seq\b\FF, \, b))" lemma sinl_ssum: "(seq\a\TT, a, \) \ ssum" -by (simp add: ssum_def seq_conv_if) + by (simp add: ssum_def seq_conv_if) lemma sinr_ssum: "(seq\b\FF, \, b) \ ssum" -by (simp add: ssum_def seq_conv_if) + by (simp add: ssum_def seq_conv_if) lemma Rep_ssum_sinl: "Rep_ssum (sinl\a) = (seq\a\TT, a, \)" -by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum) + by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum) lemma Rep_ssum_sinr: "Rep_ssum (sinr\b) = (seq\b\FF, \, b)" -by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum) + by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum) lemmas Rep_ssum_simps = Rep_ssum_inject [symmetric] below_ssum_def prod_eq_iff below_prod_def Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr + subsection \Properties of \emph{sinl} and \emph{sinr}\ text \Ordering\ -lemma sinl_below [simp]: "(sinl\x \ sinl\y) = (x \ y)" -by (simp add: Rep_ssum_simps seq_conv_if) +lemma sinl_below [simp]: "sinl\x \ sinl\y \ x \ y" + by (simp add: Rep_ssum_simps seq_conv_if) -lemma sinr_below [simp]: "(sinr\x \ sinr\y) = (x \ y)" -by (simp add: Rep_ssum_simps seq_conv_if) +lemma sinr_below [simp]: "sinr\x \ sinr\y \ x \ y" + by (simp add: Rep_ssum_simps seq_conv_if) -lemma sinl_below_sinr [simp]: "(sinl\x \ sinr\y) = (x = \)" -by (simp add: Rep_ssum_simps seq_conv_if) +lemma sinl_below_sinr [simp]: "sinl\x \ sinr\y \ x = \" + by (simp add: Rep_ssum_simps seq_conv_if) -lemma sinr_below_sinl [simp]: "(sinr\x \ sinl\y) = (x = \)" -by (simp add: Rep_ssum_simps seq_conv_if) +lemma sinr_below_sinl [simp]: "sinr\x \ sinl\y \ x = \" + by (simp add: Rep_ssum_simps seq_conv_if) text \Equality\ -lemma sinl_eq [simp]: "(sinl\x = sinl\y) = (x = y)" -by (simp add: po_eq_conv) +lemma sinl_eq [simp]: "sinl\x = sinl\y \ x = y" + by (simp add: po_eq_conv) -lemma sinr_eq [simp]: "(sinr\x = sinr\y) = (x = y)" -by (simp add: po_eq_conv) +lemma sinr_eq [simp]: "sinr\x = sinr\y \ x = y" + by (simp add: po_eq_conv) -lemma sinl_eq_sinr [simp]: "(sinl\x = sinr\y) = (x = \ \ y = \)" -by (subst po_eq_conv, simp) +lemma sinl_eq_sinr [simp]: "sinl\x = sinr\y \ x = \ \ y = \" + by (subst po_eq_conv) simp -lemma sinr_eq_sinl [simp]: "(sinr\x = sinl\y) = (x = \ \ y = \)" -by (subst po_eq_conv, simp) +lemma sinr_eq_sinl [simp]: "sinr\x = sinl\y \ x = \ \ y = \" + by (subst po_eq_conv) simp lemma sinl_inject: "sinl\x = sinl\y \ x = y" -by (rule sinl_eq [THEN iffD1]) + by (rule sinl_eq [THEN iffD1]) lemma sinr_inject: "sinr\x = sinr\y \ x = y" -by (rule sinr_eq [THEN iffD1]) + by (rule sinr_eq [THEN iffD1]) text \Strictness\ lemma sinl_strict [simp]: "sinl\\ = \" -by (simp add: Rep_ssum_simps) + by (simp add: Rep_ssum_simps) lemma sinr_strict [simp]: "sinr\\ = \" -by (simp add: Rep_ssum_simps) + by (simp add: Rep_ssum_simps) -lemma sinl_bottom_iff [simp]: "(sinl\x = \) = (x = \)" -using sinl_eq [of "x" "\"] by simp +lemma sinl_bottom_iff [simp]: "sinl\x = \ \ x = \" + using sinl_eq [of "x" "\"] by simp -lemma sinr_bottom_iff [simp]: "(sinr\x = \) = (x = \)" -using sinr_eq [of "x" "\"] by simp +lemma sinr_bottom_iff [simp]: "sinr\x = \ \ x = \" + using sinr_eq [of "x" "\"] by simp lemma sinl_defined: "x \ \ \ sinl\x \ \" -by simp + by simp lemma sinr_defined: "x \ \ \ sinr\x \ \" -by simp + by simp text \Compactness\ lemma compact_sinl: "compact x \ compact (sinl\x)" -by (rule compact_ssum, simp add: Rep_ssum_sinl) + by (rule compact_ssum) (simp add: Rep_ssum_sinl) lemma compact_sinr: "compact x \ compact (sinr\x)" -by (rule compact_ssum, simp add: Rep_ssum_sinr) + by (rule compact_ssum) (simp add: Rep_ssum_sinr) lemma compact_sinlD: "compact (sinl\x) \ compact x" -unfolding compact_def -by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp) + unfolding compact_def + by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp) lemma compact_sinrD: "compact (sinr\x) \ compact x" -unfolding compact_def -by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp) + unfolding compact_def + by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp) lemma compact_sinl_iff [simp]: "compact (sinl\x) = compact x" -by (safe elim!: compact_sinl compact_sinlD) + by (safe elim!: compact_sinl compact_sinlD) lemma compact_sinr_iff [simp]: "compact (sinr\x) = compact x" -by (safe elim!: compact_sinr compact_sinrD) + by (safe elim!: compact_sinr compact_sinrD) + subsection \Case analysis\ @@ -140,61 +140,61 @@ obtains "p = \" | x where "p = sinl\x" and "x \ \" | y where "p = sinr\y" and "y \ \" -using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps) + using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps) lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]: "\P \; \x. x \ \ \ P (sinl\x); \y. y \ \ \ P (sinr\y)\ \ P x" -by (cases x, simp_all) + by (cases x) simp_all lemma ssumE2 [case_names sinl sinr]: "\\x. p = sinl\x \ Q; \y. p = sinr\y \ Q\ \ Q" -by (cases p, simp only: sinl_strict [symmetric], simp, simp) + by (cases p, simp only: sinl_strict [symmetric], simp, simp) lemma below_sinlD: "p \ sinl\x \ \y. p = sinl\y \ y \ x" -by (cases p, rule_tac x="\" in exI, simp_all) + by (cases p, rule_tac x="\" in exI, simp_all) lemma below_sinrD: "p \ sinr\x \ \y. p = sinr\y \ y \ x" -by (cases p, rule_tac x="\" in exI, simp_all) + by (cases p, rule_tac x="\" in exI, simp_all) + subsection \Case analysis combinator\ -definition - sscase :: "('a \ 'c) \ ('b \ 'c) \ ('a ++ 'b) \ 'c" where - "sscase = (\ f g s. (\(t, x, y). If t then f\x else g\y) (Rep_ssum s))" +definition sscase :: "('a \ 'c) \ ('b \ 'c) \ ('a ++ 'b) \ 'c" + where "sscase = (\ f g s. (\(t, x, y). If t then f\x else g\y) (Rep_ssum s))" translations - "case s of XCONST sinl\x \ t1 | XCONST sinr\y \ t2" == "CONST sscase\(\ x. t1)\(\ y. t2)\s" - "case s of (XCONST sinl :: 'a)\x \ t1 | XCONST sinr\y \ t2" => "CONST sscase\(\ x. t1)\(\ y. t2)\s" + "case s of XCONST sinl\x \ t1 | XCONST sinr\y \ t2" \ "CONST sscase\(\ x. t1)\(\ y. t2)\s" + "case s of (XCONST sinl :: 'a)\x \ t1 | XCONST sinr\y \ t2" \ "CONST sscase\(\ x. t1)\(\ y. t2)\s" translations - "\(XCONST sinl\x). t" == "CONST sscase\(\ x. t)\\" - "\(XCONST sinr\y). t" == "CONST sscase\\\(\ y. t)" + "\(XCONST sinl\x). t" \ "CONST sscase\(\ x. t)\\" + "\(XCONST sinr\y). t" \ "CONST sscase\\\(\ y. t)" -lemma beta_sscase: - "sscase\f\g\s = (\(t, x, y). If t then f\x else g\y) (Rep_ssum s)" -unfolding sscase_def by (simp add: cont_Rep_ssum) +lemma beta_sscase: "sscase\f\g\s = (\(t, x, y). If t then f\x else g\y) (Rep_ssum s)" + by (simp add: sscase_def cont_Rep_ssum) lemma sscase1 [simp]: "sscase\f\g\\ = \" -unfolding beta_sscase by (simp add: Rep_ssum_strict) + by (simp add: beta_sscase Rep_ssum_strict) lemma sscase2 [simp]: "x \ \ \ sscase\f\g\(sinl\x) = f\x" -unfolding beta_sscase by (simp add: Rep_ssum_sinl) + by (simp add: beta_sscase Rep_ssum_sinl) lemma sscase3 [simp]: "y \ \ \ sscase\f\g\(sinr\y) = g\y" -unfolding beta_sscase by (simp add: Rep_ssum_sinr) + by (simp add: beta_sscase Rep_ssum_sinr) lemma sscase4 [simp]: "sscase\sinl\sinr\z = z" -by (cases z, simp_all) + by (cases z) simp_all + subsection \Strict sum preserves flatness\ instance ssum :: (flat, flat) flat -apply (intro_classes, clarify) -apply (case_tac x, simp) -apply (case_tac y, simp_all add: flat_below_iff) -apply (case_tac y, simp_all add: flat_below_iff) -done + apply (intro_classes, clarify) + apply (case_tac x, simp) + apply (case_tac y, simp_all add: flat_below_iff) + apply (case_tac y, simp_all add: flat_below_iff) + done end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Tr.thy --- a/src/HOL/HOLCF/Tr.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Tr.thy Mon Jan 01 23:07:24 2018 +0100 @@ -5,107 +5,97 @@ section \The type of lifted booleans\ theory Tr -imports Lift + imports Lift begin subsection \Type definition and constructors\ -type_synonym - tr = "bool lift" +type_synonym tr = "bool lift" translations - (type) "tr" <= (type) "bool lift" + (type) "tr" \ (type) "bool lift" -definition - TT :: "tr" where - "TT = Def True" +definition TT :: "tr" + where "TT = Def True" -definition - FF :: "tr" where - "FF = Def False" +definition FF :: "tr" + where "FF = Def False" text \Exhaustion and Elimination for type @{typ tr}\ lemma Exh_tr: "t = \ \ t = TT \ t = FF" -unfolding FF_def TT_def by (induct t) auto + by (induct t) (auto simp: FF_def TT_def) lemma trE [case_names bottom TT FF, cases type: tr]: "\p = \ \ Q; p = TT \ Q; p = FF \ Q\ \ Q" -unfolding FF_def TT_def by (induct p) auto + by (induct p) (auto simp: FF_def TT_def) lemma tr_induct [case_names bottom TT FF, induct type: tr]: - "\P \; P TT; P FF\ \ P x" -by (cases x) simp_all + "P \ \ P TT \ P FF \ P x" + by (cases x) simp_all text \distinctness for type @{typ tr}\ lemma dist_below_tr [simp]: "TT \ \" "FF \ \" "TT \ FF" "FF \ TT" -unfolding TT_def FF_def by simp_all + by (simp_all add: TT_def FF_def) -lemma dist_eq_tr [simp]: - "TT \ \" "FF \ \" "TT \ FF" "\ \ TT" "\ \ FF" "FF \ TT" -unfolding TT_def FF_def by simp_all +lemma dist_eq_tr [simp]: "TT \ \" "FF \ \" "TT \ FF" "\ \ TT" "\ \ FF" "FF \ TT" + by (simp_all add: TT_def FF_def) lemma TT_below_iff [simp]: "TT \ x \ x = TT" -by (induct x) simp_all + by (induct x) simp_all lemma FF_below_iff [simp]: "FF \ x \ x = FF" -by (induct x) simp_all + by (induct x) simp_all lemma not_below_TT_iff [simp]: "x \ TT \ x = FF" -by (induct x) simp_all + by (induct x) simp_all lemma not_below_FF_iff [simp]: "x \ FF \ x = TT" -by (induct x) simp_all + by (induct x) simp_all subsection \Case analysis\ default_sort pcpo -definition tr_case :: "'a \ 'a \ tr \ 'a" where - "tr_case = (\ t e (Def b). if b then t else e)" +definition tr_case :: "'a \ 'a \ tr \ 'a" + where "tr_case = (\ t e (Def b). if b then t else e)" -abbreviation - cifte_syn :: "[tr, 'c, 'c] \ 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60) -where - "If b then e1 else e2 == tr_case\e1\e2\b" +abbreviation cifte_syn :: "[tr, 'c, 'c] \ 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60) + where "If b then e1 else e2 \ tr_case\e1\e2\b" translations - "\ (XCONST TT). t" == "CONST tr_case\t\\" - "\ (XCONST FF). t" == "CONST tr_case\\\t" + "\ (XCONST TT). t" \ "CONST tr_case\t\\" + "\ (XCONST FF). t" \ "CONST tr_case\\\t" lemma ifte_thms [simp]: "If \ then e1 else e2 = \" "If FF then e1 else e2 = e2" "If TT then e1 else e2 = e1" -by (simp_all add: tr_case_def TT_def FF_def) + by (simp_all add: tr_case_def TT_def FF_def) subsection \Boolean connectives\ -definition - trand :: "tr \ tr \ tr" where - andalso_def: "trand = (\ x y. If x then y else FF)" -abbreviation - andalso_syn :: "tr \ tr \ tr" ("_ andalso _" [36,35] 35) where - "x andalso y == trand\x\y" +definition trand :: "tr \ tr \ tr" + where andalso_def: "trand = (\ x y. If x then y else FF)" + +abbreviation andalso_syn :: "tr \ tr \ tr" ("_ andalso _" [36,35] 35) + where "x andalso y \ trand\x\y" + +definition tror :: "tr \ tr \ tr" + where orelse_def: "tror = (\ x y. If x then TT else y)" -definition - tror :: "tr \ tr \ tr" where - orelse_def: "tror = (\ x y. If x then TT else y)" -abbreviation - orelse_syn :: "tr \ tr \ tr" ("_ orelse _" [31,30] 30) where - "x orelse y == tror\x\y" +abbreviation orelse_syn :: "tr \ tr \ tr" ("_ orelse _" [31,30] 30) + where "x orelse y \ tror\x\y" -definition - neg :: "tr \ tr" where - "neg = flift2 Not" +definition neg :: "tr \ tr" + where "neg = flift2 Not" -definition - If2 :: "[tr, 'c, 'c] \ 'c" where - "If2 Q x y = (If Q then x else y)" +definition If2 :: "tr \ 'c \ 'c \ 'c" + where "If2 Q x y = (If Q then x else y)" text \tactic for tr-thms with case split\ @@ -119,10 +109,10 @@ "(\ andalso y) = \" "(y andalso TT) = y" "(y andalso y) = y" -apply (unfold andalso_def, simp_all) -apply (cases y, simp_all) -apply (cases y, simp_all) -done + apply (unfold andalso_def, simp_all) + apply (cases y, simp_all) + apply (cases y, simp_all) + done lemma orelse_thms [simp]: "(TT orelse y) = TT" @@ -130,25 +120,21 @@ "(\ orelse y) = \" "(y orelse FF) = y" "(y orelse y) = y" -apply (unfold orelse_def, simp_all) -apply (cases y, simp_all) -apply (cases y, simp_all) -done + apply (unfold orelse_def, simp_all) + apply (cases y, simp_all) + apply (cases y, simp_all) + done lemma neg_thms [simp]: "neg\TT = FF" "neg\FF = TT" "neg\\ = \" -by (simp_all add: neg_def TT_def FF_def) + by (simp_all add: neg_def TT_def FF_def) text \split-tac for If via If2 because the constant has to be a constant\ -lemma split_If2: - "P (If2 Q x y) = ((Q = \ \ P \) \ (Q = TT \ P x) \ (Q = FF \ P y))" -apply (unfold If2_def) -apply (cases Q) -apply (simp_all) -done +lemma split_If2: "P (If2 Q x y) \ ((Q = \ \ P \) \ (Q = TT \ P x) \ (Q = FF \ P y))" + by (cases Q) (simp_all add: If2_def) (* FIXME unused!? *) ML \ @@ -159,42 +145,34 @@ subsection "Rewriting of HOLCF operations to HOL functions" -lemma andalso_or: - "t \ \ \ ((t andalso s) = FF) = (t = FF \ s = FF)" -apply (cases t) -apply simp_all -done +lemma andalso_or: "t \ \ \ (t andalso s) = FF \ t = FF \ s = FF" + by (cases t) simp_all -lemma andalso_and: - "t \ \ \ ((t andalso s) \ FF) = (t \ FF \ s \ FF)" -apply (cases t) -apply simp_all -done +lemma andalso_and: "t \ \ \ ((t andalso s) \ FF) \ t \ FF \ s \ FF" + by (cases t) simp_all -lemma Def_bool1 [simp]: "(Def x \ FF) = x" -by (simp add: FF_def) +lemma Def_bool1 [simp]: "Def x \ FF \ x" + by (simp add: FF_def) -lemma Def_bool2 [simp]: "(Def x = FF) = (\ x)" -by (simp add: FF_def) +lemma Def_bool2 [simp]: "Def x = FF \ \ x" + by (simp add: FF_def) -lemma Def_bool3 [simp]: "(Def x = TT) = x" -by (simp add: TT_def) +lemma Def_bool3 [simp]: "Def x = TT \ x" + by (simp add: TT_def) -lemma Def_bool4 [simp]: "(Def x \ TT) = (\ x)" -by (simp add: TT_def) +lemma Def_bool4 [simp]: "Def x \ TT \ \ x" + by (simp add: TT_def) -lemma If_and_if: - "(If Def P then A else B) = (if P then A else B)" -apply (cases "Def P") -apply (auto simp add: TT_def[symmetric] FF_def[symmetric]) -done +lemma If_and_if: "(If Def P then A else B) = (if P then A else B)" + by (cases "Def P") (auto simp add: TT_def[symmetric] FF_def[symmetric]) + subsection \Compactness\ lemma compact_TT: "compact TT" -by (rule compact_chfin) + by (rule compact_chfin) lemma compact_FF: "compact FF" -by (rule compact_chfin) + by (rule compact_chfin) end diff -r 3869b2400e22 -r 0d25e02759b7 src/HOL/HOLCF/Up.thy --- a/src/HOL/HOLCF/Up.thy Mon Jan 01 21:17:28 2018 +0100 +++ b/src/HOL/HOLCF/Up.thy Mon Jan 01 23:07:24 2018 +0100 @@ -6,40 +6,47 @@ section \The type of lifted values\ theory Up -imports Cfun + imports Cfun begin default_sort cpo + subsection \Definition of new type for lifting\ datatype 'a u ("(_\<^sub>\)" [1000] 999) = Ibottom | Iup 'a -primrec Ifup :: "('a \ 'b::pcpo) \ 'a u \ 'b" where +primrec Ifup :: "('a \ 'b::pcpo) \ 'a u \ 'b" + where "Ifup f Ibottom = \" - | "Ifup f (Iup x) = f\x" + | "Ifup f (Iup x) = f\x" + subsection \Ordering on lifted cpo\ instantiation u :: (cpo) below begin -definition - below_up_def: - "(op \) \ (\x y. case x of Ibottom \ True | Iup a \ - (case y of Ibottom \ False | Iup b \ a \ b))" +definition below_up_def: + "(op \) \ + (\x y. + (case x of + Ibottom \ True + | Iup a \ (case y of Ibottom \ False | Iup b \ a \ b)))" instance .. + end lemma minimal_up [iff]: "Ibottom \ z" -by (simp add: below_up_def) + by (simp add: below_up_def) lemma not_Iup_below [iff]: "Iup x \ Ibottom" -by (simp add: below_up_def) + by (simp add: below_up_def) lemma Iup_below [iff]: "(Iup x \ Iup y) = (x \ y)" -by (simp add: below_up_def) + by (simp add: below_up_def) + subsection \Lifted cpo is a partial order\ @@ -47,28 +54,28 @@ proof fix x :: "'a u" show "x \ x" - unfolding below_up_def by (simp split: u.split) + by (simp add: below_up_def split: u.split) next fix x y :: "'a u" - assume "x \ y" "y \ x" thus "x = y" - unfolding below_up_def - by (auto split: u.split_asm intro: below_antisym) + assume "x \ y" "y \ x" + then show "x = y" + by (auto simp: below_up_def split: u.split_asm intro: below_antisym) next fix x y z :: "'a u" - assume "x \ y" "y \ z" thus "x \ z" - unfolding below_up_def - by (auto split: u.split_asm intro: below_trans) + assume "x \ y" "y \ z" + then show "x \ z" + by (auto simp: below_up_def split: u.split_asm intro: below_trans) qed + subsection \Lifted cpo is a cpo\ -lemma is_lub_Iup: - "range S <<| x \ range (\i. Iup (S i)) <<| Iup x" -unfolding is_lub_def is_ub_def ball_simps -by (auto simp add: below_up_def split: u.split) +lemma is_lub_Iup: "range S <<| x \ range (\i. Iup (S i)) <<| Iup x" + by (auto simp: is_lub_def is_ub_def ball_simps below_up_def split: u.split) lemma up_chain_lemma: - assumes Y: "chain Y" obtains "\i. Y i = Ibottom" + assumes Y: "chain Y" + obtains "\i. Y i = Ibottom" | A k where "\i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\i. A i)" proof (cases "\k. Y k \ Ibottom") case True @@ -78,20 +85,19 @@ proof fix i :: nat from Y le_add2 have "Y k \ Y (i + k)" by (rule chain_mono) - with k have "Y (i + k) \ Ibottom" by (cases "Y k", auto) - thus "Iup (A i) = Y (i + k)" + with k have "Y (i + k) \ Ibottom" by (cases "Y k") auto + then show "Iup (A i) = Y (i + k)" by (cases "Y (i + k)", simp_all add: A_def) qed from Y have chain_A: "chain A" - unfolding chain_def Iup_below [symmetric] - by (simp add: Iup_A) - hence "range A <<| (\i. A i)" + by (simp add: chain_def Iup_below [symmetric] Iup_A) + then have "range A <<| (\i. A i)" by (rule cpo_lubI) - hence "range (\i. Iup (A i)) <<| Iup (\i. A i)" + then have "range (\i. Iup (A i)) <<| Iup (\i. A i)" by (rule is_lub_Iup) - hence "range (\i. Y (i + k)) <<| Iup (\i. A i)" + then have "range (\i. Y (i + k)) <<| Iup (\i. A i)" by (simp only: Iup_A) - hence "range (\i. Y i) <<| Iup (\i. A i)" + then have "range (\i. Y i) <<| Iup (\i. A i)" by (simp only: is_lub_range_shift [OF Y]) with Iup_A chain_A show ?thesis .. next @@ -104,59 +110,62 @@ proof fix S :: "nat \ 'a u" assume S: "chain S" - thus "\x. range (\i. S i) <<| x" + then show "\x. range (\i. S i) <<| x" proof (rule up_chain_lemma) assume "\i. S i = Ibottom" - hence "range (\i. S i) <<| Ibottom" + then have "range (\i. S i) <<| Ibottom" by (simp add: is_lub_const) - thus ?thesis .. + then show ?thesis .. next fix A :: "nat \ 'a" assume "range S <<| Iup (\i. A i)" - thus ?thesis .. + then show ?thesis .. qed qed + subsection \Lifted cpo is pointed\ instance u :: (cpo) pcpo -by intro_classes fast + by intro_classes fast text \for compatibility with old HOLCF-Version\ lemma inst_up_pcpo: "\ = Ibottom" -by (rule minimal_up [THEN bottomI, symmetric]) + by (rule minimal_up [THEN bottomI, symmetric]) + subsection \Continuity of \emph{Iup} and \emph{Ifup}\ text \continuity for @{term Iup}\ lemma cont_Iup: "cont Iup" -apply (rule contI) -apply (rule is_lub_Iup) -apply (erule cpo_lubI) -done + apply (rule contI) + apply (rule is_lub_Iup) + apply (erule cpo_lubI) + done text \continuity for @{term Ifup}\ lemma cont_Ifup1: "cont (\f. Ifup f x)" -by (induct x, simp_all) + by (induct x) simp_all lemma monofun_Ifup2: "monofun (\x. Ifup f x)" -apply (rule monofunI) -apply (case_tac x, simp) -apply (case_tac y, simp) -apply (simp add: monofun_cfun_arg) -done + apply (rule monofunI) + apply (case_tac x, simp) + apply (case_tac y, simp) + apply (simp add: monofun_cfun_arg) + done lemma cont_Ifup2: "cont (\x. Ifup f x)" proof (rule contI2) - fix Y assume Y: "chain Y" and Y': "chain (\i. Ifup f (Y i))" + fix Y + assume Y: "chain Y" and Y': "chain (\i. Ifup f (Y i))" from Y show "Ifup f (\i. Y i) \ (\i. Ifup f (Y i))" proof (rule up_chain_lemma) fix A and k assume A: "\i. Iup (A i) = Y (i + k)" assume "chain A" and "range Y <<| Iup (\i. A i)" - hence "Ifup f (\i. Y i) = (\i. Ifup f (Iup (A i)))" + then have "Ifup f (\i. Y i) = (\i. Ifup f (Iup (A i)))" by (simp add: lub_eqI contlub_cfun_arg) also have "\ = (\i. Ifup f (Y (i + k)))" by (simp add: A) @@ -166,96 +175,86 @@ qed simp qed (rule monofun_Ifup2) + subsection \Continuous versions of constants\ -definition - up :: "'a \ 'a u" where - "up = (\ x. Iup x)" +definition up :: "'a \ 'a u" + where "up = (\ x. Iup x)" -definition - fup :: "('a \ 'b::pcpo) \ 'a u \ 'b" where - "fup = (\ f p. Ifup f p)" +definition fup :: "('a \ 'b::pcpo) \ 'a u \ 'b" + where "fup = (\ f p. Ifup f p)" translations - "case l of XCONST up\x \ t" == "CONST fup\(\ x. t)\l" - "case l of (XCONST up :: 'a)\x \ t" => "CONST fup\(\ x. t)\l" - "\(XCONST up\x). t" == "CONST fup\(\ x. t)" + "case l of XCONST up\x \ t" \ "CONST fup\(\ x. t)\l" + "case l of (XCONST up :: 'a)\x \ t" \ "CONST fup\(\ x. t)\l" + "\(XCONST up\x). t" \ "CONST fup\(\ x. t)" text \continuous versions of lemmas for @{typ "('a)u"}\ lemma Exh_Up: "z = \ \ (\x. z = up\x)" -apply (induct z) -apply (simp add: inst_up_pcpo) -apply (simp add: up_def cont_Iup) -done + by (induct z) (simp add: inst_up_pcpo, simp add: up_def cont_Iup) lemma up_eq [simp]: "(up\x = up\y) = (x = y)" -by (simp add: up_def cont_Iup) + by (simp add: up_def cont_Iup) lemma up_inject: "up\x = up\y \ x = y" -by simp + by simp lemma up_defined [simp]: "up\x \ \" -by (simp add: up_def cont_Iup inst_up_pcpo) + by (simp add: up_def cont_Iup inst_up_pcpo) lemma not_up_less_UU: "up\x \ \" -by simp (* FIXME: remove? *) + by simp (* FIXME: remove? *) lemma up_below [simp]: "up\x \ up\y \ x \ y" -by (simp add: up_def cont_Iup) + by (simp add: up_def cont_Iup) -lemma upE [case_names bottom up, cases type: u]: - "\p = \ \ Q; \x. p = up\x \ Q\ \ Q" -apply (cases p) -apply (simp add: inst_up_pcpo) -apply (simp add: up_def cont_Iup) -done +lemma upE [case_names bottom up, cases type: u]: "\p = \ \ Q; \x. p = up\x \ Q\ \ Q" + by (cases p) (simp add: inst_up_pcpo, simp add: up_def cont_Iup) -lemma up_induct [case_names bottom up, induct type: u]: - "\P \; \x. P (up\x)\ \ P x" -by (cases x, simp_all) +lemma up_induct [case_names bottom up, induct type: u]: "P \ \ (\x. P (up\x)) \ P x" + by (cases x) simp_all text \lifting preserves chain-finiteness\ lemma up_chain_cases: - assumes Y: "chain Y" obtains "\i. Y i = \" + assumes Y: "chain Y" + obtains "\i. Y i = \" | A k where "\i. up\(A i) = Y (i + k)" and "chain A" and "(\i. Y i) = up\(\i. A i)" -apply (rule up_chain_lemma [OF Y]) -apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI) -done + by (rule up_chain_lemma [OF Y]) (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI) lemma compact_up: "compact x \ compact (up\x)" -apply (rule compactI2) -apply (erule up_chain_cases) -apply simp -apply (drule (1) compactD2, simp) -apply (erule exE) -apply (drule_tac f="up" and x="x" in monofun_cfun_arg) -apply (simp, erule exI) -done + apply (rule compactI2) + apply (erule up_chain_cases) + apply simp + apply (drule (1) compactD2, simp) + apply (erule exE) + apply (drule_tac f="up" and x="x" in monofun_cfun_arg) + apply (simp, erule exI) + done lemma compact_upD: "compact (up\x) \ compact x" -unfolding compact_def -by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp) + unfolding compact_def + by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp) lemma compact_up_iff [simp]: "compact (up\x) = compact x" -by (safe elim!: compact_up compact_upD) + by (safe elim!: compact_up compact_upD) instance u :: (chfin) chfin -apply intro_classes -apply (erule compact_imp_max_in_chain) -apply (rule_tac p="\i. Y i" in upE, simp_all) -done + apply intro_classes + apply (erule compact_imp_max_in_chain) + apply (rule_tac p="\i. Y i" in upE, simp_all) + done text \properties of fup\ lemma fup1 [simp]: "fup\f\\ = \" -by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM) + by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM) lemma fup2 [simp]: "fup\f\(up\x) = f\x" -by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM) + by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM) lemma fup3 [simp]: "fup\up\x = x" -by (cases x, simp_all) + by (cases x) simp_all end