# HG changeset patch # User Andreas Lochbihler # Date 1458302060 -3600 # Node ID d3a5b127eb81a955078f781729f5c87b10dca80f # Parent 66568c9b82163a711c28d48c625ba240ae26e66c# Parent 7248d106c6078e39f4ad9f4982c8c601f9562e35 merged diff -r 66568c9b8216 -r d3a5b127eb81 CONTRIBUTORS --- a/CONTRIBUTORS Fri Mar 18 12:48:00 2016 +0100 +++ b/CONTRIBUTORS Fri Mar 18 12:54:20 2016 +0100 @@ -13,6 +13,9 @@ * March 2016: Florian Haftmann Abstract factorial rings with unique factorization. +* March 2016: Andreas Lochbihler + Reasoning support for monotonicity, continuity and + admissibility in chain-complete partial orders. Contributions to Isabelle2016 ----------------------------- diff -r 66568c9b8216 -r d3a5b127eb81 NEWS --- a/NEWS Fri Mar 18 12:48:00 2016 +0100 +++ b/NEWS Fri Mar 18 12:54:20 2016 +0100 @@ -113,6 +113,10 @@ * Added topological_monoid +* Library/Complete_Partial_Order2.thy provides reasoning support for +proofs about monotonicity and continuity in chain-complete partial +orders and about admissibility conditions for fixpoint inductions. + * Library/Polynomial.thy contains also derivation of polynomials but not gcd/lcm on polynomials over fields. This has been moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to @@ -1092,9 +1096,9 @@ performance. * Property values in etc/symbols may contain spaces, if written with the -replacement character "␣" (Unicode point 0x2324). For example: - - \ code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono +replacement character "?" (Unicode point 0x2324). For example: + + \ code: 0x0022c6 group: operator font: Deja?Vu?Sans?Mono * Java runtime environment for x86_64-windows allows to use larger heap space. diff -r 66568c9b8216 -r d3a5b127eb81 src/HOL/Library/Complete_Partial_Order2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Complete_Partial_Order2.thy Fri Mar 18 12:54:20 2016 +0100 @@ -0,0 +1,1708 @@ +(* Title: src/HOL/Library/Complete_Partial_Order2 + Author: Andreas Lochbihler, ETH Zurich +*) + +section {* Formalisation of chain-complete partial orders, continuity and admissibility *} + +theory Complete_Partial_Order2 imports + Main + "~~/src/HOL/Library/Lattice_Syntax" +begin + +context begin interpretation lifting_syntax . + +lemma chain_transfer [transfer_rule]: + "((A ===> A ===> op =) ===> rel_set A ===> op =) Complete_Partial_Order.chain Complete_Partial_Order.chain" +unfolding chain_def[abs_def] by transfer_prover + +end + +lemma linorder_chain [simp, intro!]: + fixes Y :: "_ :: linorder set" + shows "Complete_Partial_Order.chain op \ Y" +by(auto intro: chainI) + +lemma fun_lub_apply: "\Sup. fun_lub Sup Y x = Sup ((\f. f x) ` Y)" +by(simp add: fun_lub_def image_def) + +lemma fun_lub_empty [simp]: "fun_lub lub {} = (\_. lub {})" +by(rule ext)(simp add: fun_lub_apply) + +lemma chain_fun_ordD: + assumes "Complete_Partial_Order.chain (fun_ord le) Y" + shows "Complete_Partial_Order.chain le ((\f. f x) ` Y)" +by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def) + +lemma chain_Diff: + "Complete_Partial_Order.chain ord A + \ Complete_Partial_Order.chain ord (A - B)" +by(erule chain_subset) blast + +lemma chain_rel_prodD1: + "Complete_Partial_Order.chain (rel_prod orda ordb) Y + \ Complete_Partial_Order.chain orda (fst ` Y)" +by(auto 4 3 simp add: chain_def) + +lemma chain_rel_prodD2: + "Complete_Partial_Order.chain (rel_prod orda ordb) Y + \ Complete_Partial_Order.chain ordb (snd ` Y)" +by(auto 4 3 simp add: chain_def) + + +context ccpo begin + +lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord op \) (mk_less (fun_ord op \))" + by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply + intro: order.trans antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least) + +lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain op \ Y \ Sup Y \ x \ (\y\Y. y \ x)" +by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least) + +lemma Sup_minus_bot: + assumes chain: "Complete_Partial_Order.chain op \ A" + shows "\(A - {\{}}) = \A" +apply(rule antisym) + apply(blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain]) +apply(rule ccpo_Sup_least[OF chain]) +apply(case_tac "x = \{}") +by(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+ + +lemma mono_lub: + fixes le_b (infix "\" 60) + assumes chain: "Complete_Partial_Order.chain (fun_ord op \) Y" + and mono: "\f. f \ Y \ monotone le_b op \ f" + shows "monotone op \ op \ (fun_lub Sup Y)" +proof(rule monotoneI) + fix x y + assume "x \ y" + + have chain'': "\x. Complete_Partial_Order.chain op \ ((\f. f x) ` Y)" + using chain by(rule chain_imageI)(simp add: fun_ord_def) + then show "fun_lub Sup Y x \ fun_lub Sup Y y" unfolding fun_lub_apply + proof(rule ccpo_Sup_least) + fix x' + assume "x' \ (\f. f x) ` Y" + then obtain f where "f \ Y" "x' = f x" by blast + note `x' = f x` also + from `f \ Y` `x \ y` have "f x \ f y" by(blast dest: mono monotoneD) + also have "\ \ \((\f. f y) ` Y)" using chain'' + by(rule ccpo_Sup_upper)(simp add: `f \ Y`) + finally show "x' \ \((\f. f y) ` Y)" . + qed +qed + +context + fixes le_b (infix "\" 60) and Y f + assumes chain: "Complete_Partial_Order.chain le_b Y" + and mono1: "\y. y \ Y \ monotone le_b op \ (\x. f x y)" + and mono2: "\x a b. \ x \ Y; a \ b; a \ Y; b \ Y \ \ f x a \ f x b" +begin + +lemma Sup_mono: + assumes le: "x \ y" and x: "x \ Y" and y: "y \ Y" + shows "\(f x ` Y) \ \(f y ` Y)" (is "_ \ ?rhs") +proof(rule ccpo_Sup_least) + from chain show chain': "Complete_Partial_Order.chain op \ (f x ` Y)" when "x \ Y" for x + by(rule chain_imageI) (insert that, auto dest: mono2) + + fix x' + assume "x' \ f x ` Y" + then obtain y' where "y' \ Y" "x' = f x y'" by blast note this(2) + also from mono1[OF `y' \ Y`] le have "\ \ f y y'" by(rule monotoneD) + also have "\ \ ?rhs" using chain'[OF y] + by (auto intro!: ccpo_Sup_upper simp add: `y' \ Y`) + finally show "x' \ ?rhs" . +qed(rule x) + +lemma diag_Sup: "\((\x. \(f x ` Y)) ` Y) = \((\x. f x x) ` Y)" (is "?lhs = ?rhs") +proof(rule antisym) + have chain1: "Complete_Partial_Order.chain op \ ((\x. \(f x ` Y)) ` Y)" + using chain by(rule chain_imageI)(rule Sup_mono) + have chain2: "\y'. y' \ Y \ Complete_Partial_Order.chain op \ (f y' ` Y)" using chain + by(rule chain_imageI)(auto dest: mono2) + have chain3: "Complete_Partial_Order.chain op \ ((\x. f x x) ` Y)" + using chain by(rule chain_imageI)(auto intro: monotoneD[OF mono1] mono2 order.trans) + + show "?lhs \ ?rhs" using chain1 + proof(rule ccpo_Sup_least) + fix x' + assume "x' \ (\x. \(f x ` Y)) ` Y" + then obtain y' where "y' \ Y" "x' = \(f y' ` Y)" by blast note this(2) + also have "\ \ ?rhs" using chain2[OF `y' \ Y`] + proof(rule ccpo_Sup_least) + fix x + assume "x \ f y' ` Y" + then obtain y where "y \ Y" and x: "x = f y' y" by blast + def y'' \ "if y \ y' then y' else y" + from chain `y \ Y` `y' \ Y` have "y \ y' \ y' \ y" by(rule chainD) + hence "f y' y \ f y'' y''" using `y \ Y` `y' \ Y` + by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1]) + also from `y \ Y` `y' \ Y` have "y'' \ Y" by(simp add: y''_def) + from chain3 have "f y'' y'' \ ?rhs" by(rule ccpo_Sup_upper)(simp add: `y'' \ Y`) + finally show "x \ ?rhs" by(simp add: x) + qed + finally show "x' \ ?rhs" . + qed + + show "?rhs \ ?lhs" using chain3 + proof(rule ccpo_Sup_least) + fix y + assume "y \ (\x. f x x) ` Y" + then obtain x where "x \ Y" and "y = f x x" by blast note this(2) + also from chain2[OF `x \ Y`] have "\ \ \(f x ` Y)" + by(rule ccpo_Sup_upper)(simp add: `x \ Y`) + also have "\ \ ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: `x \ Y`) + finally show "y \ ?lhs" . + qed +qed + +end + +lemma Sup_image_mono_le: + fixes le_b (infix "\" 60) and Sup_b ("\_" [900] 900) + assumes ccpo: "class.ccpo Sup_b op \ lt_b" + assumes chain: "Complete_Partial_Order.chain op \ Y" + and mono: "\x y. \ x \ y; x \ Y \ \ f x \ f y" + shows "Sup (f ` Y) \ f (\Y)" +proof(rule ccpo_Sup_least) + show "Complete_Partial_Order.chain op \ (f ` Y)" + using chain by(rule chain_imageI)(rule mono) + + fix x + assume "x \ f ` Y" + then obtain y where "y \ Y" and "x = f y" by blast note this(2) + also have "y \ \Y" using ccpo chain `y \ Y` by(rule ccpo.ccpo_Sup_upper) + hence "f y \ f (\Y)" using `y \ Y` by(rule mono) + finally show "x \ \" . +qed + +lemma swap_Sup: + fixes le_b (infix "\" 60) + assumes Y: "Complete_Partial_Order.chain op \ Y" + and Z: "Complete_Partial_Order.chain (fun_ord op \) Z" + and mono: "\f. f \ Z \ monotone op \ op \ f" + shows "\((\x. \(x ` Y)) ` Z) = \((\x. \((\f. f x) ` Z)) ` Y)" + (is "?lhs = ?rhs") +proof(cases "Y = {}") + case True + then show ?thesis + by (simp add: image_constant_conv cong del: strong_SUP_cong) +next + case False + have chain1: "\f. f \ Z \ Complete_Partial_Order.chain op \ (f ` Y)" + by(rule chain_imageI[OF Y])(rule monotoneD[OF mono]) + have chain2: "Complete_Partial_Order.chain op \ ((\x. \(x ` Y)) ` Z)" using Z + proof(rule chain_imageI) + fix f g + assume "f \ Z" "g \ Z" + and "fun_ord op \ f g" + from chain1[OF `f \ Z`] show "\(f ` Y) \ \(g ` Y)" + proof(rule ccpo_Sup_least) + fix x + assume "x \ f ` Y" + then obtain y where "y \ Y" "x = f y" by blast note this(2) + also have "\ \ g y" using `fun_ord op \ f g` by(simp add: fun_ord_def) + also have "\ \ \(g ` Y)" using chain1[OF `g \ Z`] + by(rule ccpo_Sup_upper)(simp add: `y \ Y`) + finally show "x \ \(g ` Y)" . + qed + qed + have chain3: "\x. Complete_Partial_Order.chain op \ ((\f. f x) ` Z)" + using Z by(rule chain_imageI)(simp add: fun_ord_def) + have chain4: "Complete_Partial_Order.chain op \ ((\x. \((\f. f x) ` Z)) ` Y)" + using Y + proof(rule chain_imageI) + fix f x y + assume "x \ y" + show "\((\f. f x) ` Z) \ \((\f. f y) ` Z)" (is "_ \ ?rhs") using chain3 + proof(rule ccpo_Sup_least) + fix x' + assume "x' \ (\f. f x) ` Z" + then obtain f where "f \ Z" "x' = f x" by blast note this(2) + also have "f x \ f y" using `f \ Z` `x \ y` by(rule monotoneD[OF mono]) + also have "f y \ ?rhs" using chain3 + by(rule ccpo_Sup_upper)(simp add: `f \ Z`) + finally show "x' \ ?rhs" . + qed + qed + + from chain2 have "?lhs \ ?rhs" + proof(rule ccpo_Sup_least) + fix x + assume "x \ (\x. \(x ` Y)) ` Z" + then obtain f where "f \ Z" "x = \(f ` Y)" by blast note this(2) + also have "\ \ ?rhs" using chain1[OF `f \ Z`] + proof(rule ccpo_Sup_least) + fix x' + assume "x' \ f ` Y" + then obtain y where "y \ Y" "x' = f y" by blast note this(2) + also have "f y \ \((\f. f y) ` Z)" using chain3 + by(rule ccpo_Sup_upper)(simp add: `f \ Z`) + also have "\ \ ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: `y \ Y`) + finally show "x' \ ?rhs" . + qed + finally show "x \ ?rhs" . + qed + moreover + have "?rhs \ ?lhs" using chain4 + proof(rule ccpo_Sup_least) + fix x + assume "x \ (\x. \((\f. f x) ` Z)) ` Y" + then obtain y where "y \ Y" "x = \((\f. f y) ` Z)" by blast note this(2) + also have "\ \ ?lhs" using chain3 + proof(rule ccpo_Sup_least) + fix x' + assume "x' \ (\f. f y) ` Z" + then obtain f where "f \ Z" "x' = f y" by blast note this(2) + also have "f y \ \(f ` Y)" using chain1[OF `f \ Z`] + by(rule ccpo_Sup_upper)(simp add: `y \ Y`) + also have "\ \ ?lhs" using chain2 + by(rule ccpo_Sup_upper)(simp add: `f \ Z`) + finally show "x' \ ?lhs" . + qed + finally show "x \ ?lhs" . + qed + ultimately show "?lhs = ?rhs" by(rule antisym) +qed + +lemma fixp_mono: + assumes fg: "fun_ord op \ f g" + and f: "monotone op \ op \ f" + and g: "monotone op \ op \ g" + shows "ccpo_class.fixp f \ ccpo_class.fixp g" +unfolding fixp_def +proof(rule ccpo_Sup_least) + fix x + assume "x \ ccpo_class.iterates f" + thus "x \ \ccpo_class.iterates g" + proof induction + case (step x) + from f step.IH have "f x \ f (\ccpo_class.iterates g)" by(rule monotoneD) + also have "\ \ g (\ccpo_class.iterates g)" using fg by(simp add: fun_ord_def) + also have "\ = \ccpo_class.iterates g" by(fold fixp_def fixp_unfold[OF g]) simp + finally show ?case . + qed(blast intro: ccpo_Sup_least) +qed(rule chain_iterates[OF f]) + +context fixes ordb :: "'b \ 'b \ bool" (infix "\" 60) begin + +lemma iterates_mono: + assumes f: "f \ ccpo.iterates (fun_lub Sup) (fun_ord op \) F" + and mono: "\f. monotone op \ op \ f \ monotone op \ op \ (F f)" + shows "monotone op \ op \ f" +using f +by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mono_lub)+ + +lemma fixp_preserves_mono: + assumes mono: "\x. monotone (fun_ord op \) op \ (\f. F f x)" + and mono2: "\f. monotone op \ op \ f \ monotone op \ op \ (F f)" + shows "monotone op \ op \ (ccpo.fixp (fun_lub Sup) (fun_ord op \) F)" + (is "monotone _ _ ?fixp") +proof(rule monotoneI) + have mono: "monotone (fun_ord op \) (fun_ord op \) F" + by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono]) + let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \) F" + have chain: "\x. Complete_Partial_Order.chain op \ ((\f. f x) ` ?iter)" + by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def) + + fix x y + assume "x \ y" + show "?fixp x \ ?fixp y" + unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain + proof(rule ccpo_Sup_least) + fix x' + assume "x' \ (\f. f x) ` ?iter" + then obtain f where "f \ ?iter" "x' = f x" by blast note this(2) + also have "f x \ f y" + by(rule monotoneD[OF iterates_mono[OF `f \ ?iter` mono2]])(blast intro: `x \ y`)+ + also have "f y \ \((\f. f y) ` ?iter)" using chain + by(rule ccpo_Sup_upper)(simp add: `f \ ?iter`) + finally show "x' \ \" . + qed +qed + +end + +end + +lemma monotone2monotone: + assumes 2: "\x. monotone ordb ordc (\y. f x y)" + and t: "monotone orda ordb (\x. t x)" + and 1: "\y. monotone orda ordc (\x. f x y)" + and trans: "transp ordc" + shows "monotone orda ordc (\x. f x (t x))" +by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1]) + +subsection {* Continuity *} + +definition cont :: "('a set \ 'a) \ ('a \ 'a \ bool) \ ('b set \ 'b) \ ('b \ 'b \ bool) \ ('a \ 'b) \ bool" +where + "cont luba orda lubb ordb f \ + (\Y. Complete_Partial_Order.chain orda Y \ Y \ {} \ f (luba Y) = lubb (f ` Y))" + +definition mcont :: "('a set \ 'a) \ ('a \ 'a \ bool) \ ('b set \ 'b) \ ('b \ 'b \ bool) \ ('a \ 'b) \ bool" +where + "mcont luba orda lubb ordb f \ + monotone orda ordb f \ cont luba orda lubb ordb f" + +subsubsection {* Theorem collection @{text cont_intro} *} + +named_theorems cont_intro "continuity and admissibility intro rules" +ML {* +(* apply cont_intro rules as intro and try to solve + the remaining of the emerging subgoals with simp *) +fun cont_intro_tac ctxt = + REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems cont_intro}))) + THEN_ALL_NEW (SOLVED' (simp_tac ctxt)) + +fun cont_intro_simproc ctxt ct = + let + fun mk_stmt t = t + |> HOLogic.mk_Trueprop + |> Thm.cterm_of ctxt + |> Goal.init + fun mk_thm t = + case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of + SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI}) + | NONE => NONE + in + case Thm.term_of ct of + t as Const (@{const_name ccpo.admissible}, _) $ _ $ _ $ _ => mk_thm t + | t as Const (@{const_name mcont}, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t + | t as Const (@{const_name monotone}, _) $ _ $ _ $ _ => mk_thm t + | _ => NONE + end + handle THM _ => NONE + | TYPE _ => NONE +*} + +simproc_setup "cont_intro" + ( "ccpo.admissible lub ord P" + | "mcont lub ord lub' ord' f" + | "monotone ord ord' f" + ) = {* K cont_intro_simproc *} + +lemmas [cont_intro] = + call_mono + let_mono + if_mono + option.const_mono + tailrec.const_mono + bind_mono + +declare if_mono[simp] + +lemma monotone_id' [cont_intro]: "monotone ord ord (\x. x)" +by(simp add: monotone_def) + +lemma monotone_applyI: + "monotone orda ordb F \ monotone (fun_ord orda) ordb (\f. F (f x))" +by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD) + +lemma monotone_if_fun [partial_function_mono]: + "\ monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \ + \ monotone (fun_ord orda) (fun_ord ordb) (\f n. if c n then F f n else G f n)" +by(simp add: monotone_def fun_ord_def) + +lemma monotone_fun_apply_fun [partial_function_mono]: + "monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\f n. f t (g n))" +by(rule monotoneI)(simp add: fun_ord_def) + +lemma monotone_fun_ord_apply: + "monotone orda (fun_ord ordb) f \ (\x. monotone orda ordb (\y. f y x))" +by(auto simp add: monotone_def fun_ord_def) + +context preorder begin + +lemma transp_le [simp, cont_intro]: "transp op \" +by(rule transpI)(rule order_trans) + +lemma monotone_const [simp, cont_intro]: "monotone ord op \ (\_. c)" +by(rule monotoneI) simp + +end + +lemma transp_le [cont_intro, simp]: + "class.preorder ord (mk_less ord) \ transp ord" +by(rule preorder.transp_le) + +context partial_function_definitions begin + +declare const_mono [cont_intro, simp] + +lemma transp_le [cont_intro, simp]: "transp leq" +by(rule transpI)(rule leq_trans) + +lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)" +by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans) + +declare ccpo[cont_intro, simp] + +end + +lemma contI [intro?]: + "(\Y. \ Complete_Partial_Order.chain orda Y; Y \ {} \ \ f (luba Y) = lubb (f ` Y)) + \ cont luba orda lubb ordb f" +unfolding cont_def by blast + +lemma contD: + "\ cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \ {} \ + \ f (luba Y) = lubb (f ` Y)" +unfolding cont_def by blast + +lemma cont_id [simp, cont_intro]: "\Sup. cont Sup ord Sup ord id" +by(rule contI) simp + +lemma cont_id' [simp, cont_intro]: "\Sup. cont Sup ord Sup ord (\x. x)" +using cont_id[unfolded id_def] . + +lemma cont_applyI [cont_intro]: + assumes cont: "cont luba orda lubb ordb g" + shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\f. g (f x))" +by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont]) + +lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\f. f t)" +by(simp add: cont_def fun_lub_apply) + +lemma cont_if [cont_intro]: + "\ cont luba orda lubb ordb f; cont luba orda lubb ordb g \ + \ cont luba orda lubb ordb (\x. if c then f x else g x)" +by(cases c) simp_all + +lemma mcontI [intro?]: + "\ monotone orda ordb f; cont luba orda lubb ordb f \ \ mcont luba orda lubb ordb f" +by(simp add: mcont_def) + +lemma mcont_mono: "mcont luba orda lubb ordb f \ monotone orda ordb f" +by(simp add: mcont_def) + +lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \ cont luba orda lubb ordb f" +by(simp add: mcont_def) + +lemma mcont_monoD: + "\ mcont luba orda lubb ordb f; orda x y \ \ ordb (f x) (f y)" +by(auto simp add: mcont_def dest: monotoneD) + +lemma mcont_contD: + "\ mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \ {} \ + \ f (luba Y) = lubb (f ` Y)" +by(auto simp add: mcont_def dest: contD) + +lemma mcont_call [cont_intro, simp]: + "mcont (fun_lub lub) (fun_ord ord) lub ord (\f. f t)" +by(simp add: mcont_def call_mono call_cont) + +lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\x. x)" +by(simp add: mcont_def monotone_id') + +lemma mcont_applyI: + "mcont luba orda lubb ordb (\x. F x) \ mcont (fun_lub luba) (fun_ord orda) lubb ordb (\f. F (f x))" +by(simp add: mcont_def monotone_applyI cont_applyI) + +lemma mcont_if [cont_intro, simp]: + "\ mcont luba orda lubb ordb (\x. f x); mcont luba orda lubb ordb (\x. g x) \ + \ mcont luba orda lubb ordb (\x. if c then f x else g x)" +by(simp add: mcont_def cont_if) + +lemma cont_fun_lub_apply: + "cont luba orda (fun_lub lubb) (fun_ord ordb) f \ (\x. cont luba orda lubb ordb (\y. f y x))" +by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def) + +lemma mcont_fun_lub_apply: + "mcont luba orda (fun_lub lubb) (fun_ord ordb) f \ (\x. mcont luba orda lubb ordb (\y. f y x))" +by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def) + +context ccpo begin + +lemma cont_const [simp, cont_intro]: "cont luba orda Sup op \ (\x. c)" +by (rule contI) (simp add: image_constant_conv cong del: strong_SUP_cong) + +lemma mcont_const [cont_intro, simp]: + "mcont luba orda Sup op \ (\x. c)" +by(simp add: mcont_def) + +lemma cont_apply: + assumes 2: "\x. cont lubb ordb Sup op \ (\y. f x y)" + and t: "cont luba orda lubb ordb (\x. t x)" + and 1: "\y. cont luba orda Sup op \ (\x. f x y)" + and mono: "monotone orda ordb (\x. t x)" + and mono2: "\x. monotone ordb op \ (\y. f x y)" + and mono1: "\y. monotone orda op \ (\x. f x y)" + shows "cont luba orda Sup op \ (\x. f x (t x))" +proof + fix Y + assume chain: "Complete_Partial_Order.chain orda Y" and "Y \ {}" + moreover from chain have chain': "Complete_Partial_Order.chain ordb (t ` Y)" + by(rule chain_imageI)(rule monotoneD[OF mono]) + ultimately show "f (luba Y) (t (luba Y)) = \((\x. f x (t x)) ` Y)" + by(simp add: contD[OF 1] contD[OF t] contD[OF 2] image_image) + (rule diag_Sup[OF chain], auto intro: monotone2monotone[OF mono2 mono monotone_const transpI] monotoneD[OF mono1]) +qed + +lemma mcont2mcont': + "\ \x. mcont lub' ord' Sup op \ (\y. f x y); + \y. mcont lub ord Sup op \ (\x. f x y); + mcont lub ord lub' ord' (\y. t y) \ + \ mcont lub ord Sup op \ (\x. f x (t x))" +unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply) + +lemma mcont2mcont: + "\mcont lub' ord' Sup op \ (\x. f x); mcont lub ord lub' ord' (\x. t x)\ + \ mcont lub ord Sup op \ (\x. f (t x))" +by(rule mcont2mcont'[OF _ mcont_const]) + +context + fixes ord :: "'b \ 'b \ bool" (infix "\" 60) + and lub :: "'b set \ 'b" ("\_" [900] 900) +begin + +lemma cont_fun_lub_Sup: + assumes chainM: "Complete_Partial_Order.chain (fun_ord op \) M" + and mcont [rule_format]: "\f\M. mcont lub op \ Sup op \ f" + shows "cont lub op \ Sup op \ (fun_lub Sup M)" +proof(rule contI) + fix Y + assume chain: "Complete_Partial_Order.chain op \ Y" + and Y: "Y \ {}" + from swap_Sup[OF chain chainM mcont[THEN mcont_mono]] + show "fun_lub Sup M (\Y) = \(fun_lub Sup M ` Y)" + by(simp add: mcont_contD[OF mcont chain Y] fun_lub_apply cong: image_cong) +qed + +lemma mcont_fun_lub_Sup: + "\ Complete_Partial_Order.chain (fun_ord op \) M; + \f\M. mcont lub ord Sup op \ f \ + \ mcont lub op \ Sup op \ (fun_lub Sup M)" +by(simp add: mcont_def cont_fun_lub_Sup mono_lub) + +lemma iterates_mcont: + assumes f: "f \ ccpo.iterates (fun_lub Sup) (fun_ord op \) F" + and mono: "\f. mcont lub op \ Sup op \ f \ mcont lub op \ Sup op \ (F f)" + shows "mcont lub op \ Sup op \ f" +using f +by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mcont_fun_lub_Sup)+ + +lemma fixp_preserves_mcont: + assumes mono: "\x. monotone (fun_ord op \) op \ (\f. F f x)" + and mcont: "\f. mcont lub op \ Sup op \ f \ mcont lub op \ Sup op \ (F f)" + shows "mcont lub op \ Sup op \ (ccpo.fixp (fun_lub Sup) (fun_ord op \) F)" + (is "mcont _ _ _ _ ?fixp") +unfolding mcont_def +proof(intro conjI monotoneI contI) + have mono: "monotone (fun_ord op \) (fun_ord op \) F" + by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono]) + let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \) F" + have chain: "\x. Complete_Partial_Order.chain op \ ((\f. f x) ` ?iter)" + by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def) + + { + fix x y + assume "x \ y" + show "?fixp x \ ?fixp y" + unfolding ccpo.fixp_def[OF ccpo_fun] fun_lub_apply using chain + proof(rule ccpo_Sup_least) + fix x' + assume "x' \ (\f. f x) ` ?iter" + then obtain f where "f \ ?iter" "x' = f x" by blast note this(2) + also from _ `x \ y` have "f x \ f y" + by(rule mcont_monoD[OF iterates_mcont[OF `f \ ?iter` mcont]]) + also have "f y \ \((\f. f y) ` ?iter)" using chain + by(rule ccpo_Sup_upper)(simp add: `f \ ?iter`) + finally show "x' \ \" . + qed + next + fix Y + assume chain: "Complete_Partial_Order.chain op \ Y" + and Y: "Y \ {}" + { fix f + assume "f \ ?iter" + hence "f (\Y) = \(f ` Y)" + using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) } + moreover have "\((\f. \(f ` Y)) ` ?iter) = \((\x. \((\f. f x) ` ?iter)) ` Y)" + using chain ccpo.chain_iterates[OF ccpo_fun mono] + by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]]) + ultimately show "?fixp (\Y) = \(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun] + by(simp add: fun_lub_apply cong: image_cong) + } +qed + +end + +context + fixes F :: "'c \ 'c" and U :: "'c \ 'b \ 'a" and C :: "('b \ 'a) \ 'c" and f + assumes mono: "\x. monotone (fun_ord op \) op \ (\f. U (F (C f)) x)" + and eq: "f \ C (ccpo.fixp (fun_lub Sup) (fun_ord op \) (\f. U (F (C f))))" + and inverse: "\f. U (C f) = f" +begin + +lemma fixp_preserves_mono_uc: + assumes mono2: "\f. monotone ord op \ (U f) \ monotone ord op \ (U (F f))" + shows "monotone ord op \ (U f)" +using fixp_preserves_mono[OF mono mono2] by(subst eq)(simp add: inverse) + +lemma fixp_preserves_mcont_uc: + assumes mcont: "\f. mcont lubb ordb Sup op \ (U f) \ mcont lubb ordb Sup op \ (U (F f))" + shows "mcont lubb ordb Sup op \ (U f)" +using fixp_preserves_mcont[OF mono mcont] by(subst eq)(simp add: inverse) + +end + +lemmas fixp_preserves_mono1 = fixp_preserves_mono_uc[of "\x. x" _ "\x. x", OF _ _ refl] +lemmas fixp_preserves_mono2 = + fixp_preserves_mono_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl] +lemmas fixp_preserves_mono3 = + fixp_preserves_mono_uc[of "\f. case_prod (case_prod f)" _ "\f. curry (curry f)", unfolded case_prod_curry curry_case_prod, OF _ _ refl] +lemmas fixp_preserves_mono4 = + fixp_preserves_mono_uc[of "\f. case_prod (case_prod (case_prod f))" _ "\f. curry (curry (curry f))", unfolded case_prod_curry curry_case_prod, OF _ _ refl] + +lemmas fixp_preserves_mcont1 = fixp_preserves_mcont_uc[of "\x. x" _ "\x. x", OF _ _ refl] +lemmas fixp_preserves_mcont2 = + fixp_preserves_mcont_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl] +lemmas fixp_preserves_mcont3 = + fixp_preserves_mcont_uc[of "\f. case_prod (case_prod f)" _ "\f. curry (curry f)", unfolded case_prod_curry curry_case_prod, OF _ _ refl] +lemmas fixp_preserves_mcont4 = + fixp_preserves_mcont_uc[of "\f. case_prod (case_prod (case_prod f))" _ "\f. curry (curry (curry f))", unfolded case_prod_curry curry_case_prod, OF _ _ refl] + +end + +lemma (in preorder) monotone_if_bot: + fixes bot + assumes mono: "\x y. \ x \ y; \ (x \ bound) \ \ ord (f x) (f y)" + and bot: "\x. \ x \ bound \ ord bot (f x)" "ord bot bot" + shows "monotone op \ ord (\x. if x \ bound then bot else f x)" +by(rule monotoneI)(auto intro: bot intro: mono order_trans) + +lemma (in ccpo) mcont_if_bot: + fixes bot and lub ("\_" [900] 900) and ord (infix "\" 60) + assumes ccpo: "class.ccpo lub op \ lt" + and mono: "\x y. \ x \ y; \ x \ bound \ \ f x \ f y" + and cont: "\Y. \ Complete_Partial_Order.chain op \ Y; Y \ {}; \x. x \ Y \ \ x \ bound \ \ f (\Y) = \(f ` Y)" + and bot: "\x. \ x \ bound \ bot \ f x" + shows "mcont Sup op \ lub op \ (\x. if x \ bound then bot else f x)" (is "mcont _ _ _ _ ?g") +proof(intro mcontI contI) + interpret c: ccpo lub "op \" lt by(fact ccpo) + show "monotone op \ op \ ?g" by(rule monotone_if_bot)(simp_all add: mono bot) + + fix Y + assume chain: "Complete_Partial_Order.chain op \ Y" and Y: "Y \ {}" + show "?g (\Y) = \(?g ` Y)" + proof(cases "Y \ {x. x \ bound}") + case True + hence "\Y \ bound" using chain by(auto intro: ccpo_Sup_least) + moreover have "Y \ {x. \ x \ bound} = {}" using True by auto + ultimately show ?thesis using True Y + by (auto simp add: image_constant_conv cong del: c.strong_SUP_cong) + next + case False + let ?Y = "Y \ {x. \ x \ bound}" + have chain': "Complete_Partial_Order.chain op \ ?Y" + using chain by(rule chain_subset) simp + + from False obtain y where ybound: "\ y \ bound" and y: "y \ Y" by blast + hence "\ \Y \ bound" by (metis ccpo_Sup_upper chain order.trans) + hence "?g (\Y) = f (\Y)" by simp + also have "\Y \ \?Y" using chain + proof(rule ccpo_Sup_least) + fix x + assume x: "x \ Y" + show "x \ \?Y" + proof(cases "x \ bound") + case True + with chainD[OF chain x y] have "x \ y" using ybound by(auto intro: order_trans) + thus ?thesis by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound) + qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x) + qed + hence "\Y = \?Y" by(rule antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain]) + hence "f (\Y) = f (\?Y)" by simp + also have "f (\?Y) = \(f ` ?Y)" using chain' by(rule cont)(insert y ybound, auto) + also have "\(f ` ?Y) = \(?g ` Y)" + proof(cases "Y \ {x. x \ bound} = {}") + case True + hence "f ` ?Y = ?g ` Y" by auto + thus ?thesis by(rule arg_cong) + next + case False + have chain'': "Complete_Partial_Order.chain op \ (insert bot (f ` ?Y))" + using chain by(auto intro!: chainI bot dest: chainD intro: mono) + hence chain''': "Complete_Partial_Order.chain op \ (f ` ?Y)" by(rule chain_subset) blast + have "bot \ \(f ` ?Y)" using y ybound by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain''']) + hence "\(insert bot (f ` ?Y)) \ \(f ` ?Y)" using chain'' + by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain''']) + with _ have "\ = \(insert bot (f ` ?Y))" + by(rule c.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain'']) + also have "insert bot (f ` ?Y) = ?g ` Y" using False by auto + finally show ?thesis . + qed + finally show ?thesis . + qed +qed + +context partial_function_definitions begin + +lemma mcont_const [cont_intro, simp]: + "mcont luba orda lub leq (\x. c)" +by(rule ccpo.mcont_const)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms]) + +lemmas [cont_intro, simp] = + ccpo.cont_const[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] + +lemma mono2mono: + assumes "monotone ordb leq (\y. f y)" "monotone orda ordb (\x. t x)" + shows "monotone orda leq (\x. f (t x))" +using assms by(rule monotone2monotone) simp_all + +lemmas mcont2mcont' = ccpo.mcont2mcont'[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] +lemmas mcont2mcont = ccpo.mcont2mcont[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] + +lemmas fixp_preserves_mono1 = ccpo.fixp_preserves_mono1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] +lemmas fixp_preserves_mono2 = ccpo.fixp_preserves_mono2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] +lemmas fixp_preserves_mono3 = ccpo.fixp_preserves_mono3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] +lemmas fixp_preserves_mono4 = ccpo.fixp_preserves_mono4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] +lemmas fixp_preserves_mcont1 = ccpo.fixp_preserves_mcont1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] +lemmas fixp_preserves_mcont2 = ccpo.fixp_preserves_mcont2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] +lemmas fixp_preserves_mcont3 = ccpo.fixp_preserves_mcont3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] +lemmas fixp_preserves_mcont4 = ccpo.fixp_preserves_mcont4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] + +lemma monotone_if_bot: + fixes bot + assumes g: "\x. g x = (if leq x bound then bot else f x)" + and mono: "\x y. \ leq x y; \ leq x bound \ \ ord (f x) (f y)" + and bot: "\x. \ leq x bound \ ord bot (f x)" "ord bot bot" + shows "monotone leq ord g" +unfolding g[abs_def] using preorder mono bot by(rule preorder.monotone_if_bot) + +lemma mcont_if_bot: + fixes bot + assumes ccpo: "class.ccpo lub' ord (mk_less ord)" + and bot: "\x. \ leq x bound \ ord bot (f x)" + and g: "\x. g x = (if leq x bound then bot else f x)" + and mono: "\x y. \ leq x y; \ leq x bound \ \ ord (f x) (f y)" + and cont: "\Y. \ Complete_Partial_Order.chain leq Y; Y \ {}; \x. x \ Y \ \ leq x bound \ \ f (lub Y) = lub' (f ` Y)" + shows "mcont lub leq lub' ord g" +unfolding g[abs_def] using ccpo mono cont bot by(rule ccpo.mcont_if_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]) + +end + +subsection {* Admissibility *} + +lemma admissible_subst: + assumes adm: "ccpo.admissible luba orda (\x. P x)" + and mcont: "mcont lubb ordb luba orda f" + shows "ccpo.admissible lubb ordb (\x. P (f x))" +apply(rule ccpo.admissibleI) +apply(frule (1) mcont_contD[OF mcont]) +apply(auto intro: ccpo.admissibleD[OF adm] chain_imageI dest: mcont_monoD[OF mcont]) +done + +lemmas [simp, cont_intro] = + admissible_all + admissible_ball + admissible_const + admissible_conj + +lemma admissible_disj' [simp, cont_intro]: + "\ class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \ + \ ccpo.admissible lub ord (\x. P x \ Q x)" +by(rule ccpo.admissible_disj) + +lemma admissible_imp' [cont_intro]: + "\ class.ccpo lub ord (mk_less ord); + ccpo.admissible lub ord (\x. \ P x); + ccpo.admissible lub ord (\x. Q x) \ + \ ccpo.admissible lub ord (\x. P x \ Q x)" +unfolding imp_conv_disj by(rule ccpo.admissible_disj) + +lemma admissible_imp [cont_intro]: + "(Q \ ccpo.admissible lub ord (\x. P x)) + \ ccpo.admissible lub ord (\x. Q \ P x)" +by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD) + +lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]: + shows admissible_not_mem: "ccpo.admissible Union op \ (\A. x \ A)" +by(rule ccpo.admissibleI) auto + +lemma admissible_eqI: + assumes f: "cont luba orda lub ord (\x. f x)" + and g: "cont luba orda lub ord (\x. g x)" + shows "ccpo.admissible luba orda (\x. f x = g x)" +apply(rule ccpo.admissibleI) +apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong) +done + +corollary admissible_eq_mcontI [cont_intro]: + "\ mcont luba orda lub ord (\x. f x); + mcont luba orda lub ord (\x. g x) \ + \ ccpo.admissible luba orda (\x. f x = g x)" +by(rule admissible_eqI)(auto simp add: mcont_def) + +lemma admissible_iff [cont_intro, simp]: + "\ ccpo.admissible lub ord (\x. P x \ Q x); ccpo.admissible lub ord (\x. Q x \ P x) \ + \ ccpo.admissible lub ord (\x. P x \ Q x)" +by(subst iff_conv_conj_imp)(rule admissible_conj) + +context ccpo begin + +lemma admissible_leI: + assumes f: "mcont luba orda Sup op \ (\x. f x)" + and g: "mcont luba orda Sup op \ (\x. g x)" + shows "ccpo.admissible luba orda (\x. f x \ g x)" +proof(rule ccpo.admissibleI) + fix A + assume chain: "Complete_Partial_Order.chain orda A" + and le: "\x\A. f x \ g x" + and False: "A \ {}" + have "f (luba A) = \(f ` A)" by(simp add: mcont_contD[OF f] chain False) + also have "\ \ \(g ` A)" + proof(rule ccpo_Sup_least) + from chain show "Complete_Partial_Order.chain op \ (f ` A)" + by(rule chain_imageI)(rule mcont_monoD[OF f]) + + fix x + assume "x \ f ` A" + then obtain y where "y \ A" "x = f y" by blast note this(2) + also have "f y \ g y" using le `y \ A` by simp + also have "Complete_Partial_Order.chain op \ (g ` A)" + using chain by(rule chain_imageI)(rule mcont_monoD[OF g]) + hence "g y \ \(g ` A)" by(rule ccpo_Sup_upper)(simp add: `y \ A`) + finally show "x \ \" . + qed + also have "\ = g (luba A)" by(simp add: mcont_contD[OF g] chain False) + finally show "f (luba A) \ g (luba A)" . +qed + +end + +lemma admissible_leI: + fixes ord (infix "\" 60) and lub ("\_" [900] 900) + assumes "class.ccpo lub op \ (mk_less op \)" + and "mcont luba orda lub op \ (\x. f x)" + and "mcont luba orda lub op \ (\x. g x)" + shows "ccpo.admissible luba orda (\x. f x \ g x)" +using assms by(rule ccpo.admissible_leI) + +declare ccpo_class.admissible_leI[cont_intro] + +context ccpo begin + +lemma admissible_not_below: "ccpo.admissible Sup op \ (\x. \ op \ x y)" +by(rule ccpo.admissibleI)(simp add: ccpo_Sup_below_iff) + +end + +lemma (in preorder) preorder [cont_intro, simp]: "class.preorder op \ (mk_less op \)" +by(unfold_locales)(auto simp add: mk_less_def intro: order_trans) + +context partial_function_definitions begin + +lemmas [cont_intro, simp] = + admissible_leI[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] + ccpo.admissible_not_below[THEN admissible_subst, OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] + +end + + +inductive compact :: "('a set \ 'a) \ ('a \ 'a \ bool) \ 'a \ bool" + for lub ord x +where compact: + "\ ccpo.admissible lub ord (\y. \ ord x y); + ccpo.admissible lub ord (\y. x \ y) \ + \ compact lub ord x" + +hide_fact (open) compact + +context ccpo begin + +lemma compactI: + assumes "ccpo.admissible Sup op \ (\y. \ x \ y)" + shows "compact Sup op \ x" +using assms +proof(rule compact.intros) + have neq: "(\y. x \ y) = (\y. \ x \ y \ \ y \ x)" by(auto) + show "ccpo.admissible Sup op \ (\y. x \ y)" + by(subst neq)(rule admissible_disj admissible_not_below assms)+ +qed + +lemma compact_bot: + assumes "x = Sup {}" + shows "compact Sup op \ x" +proof(rule compactI) + show "ccpo.admissible Sup op \ (\y. \ x \ y)" using assms + by(auto intro!: ccpo.admissibleI intro: ccpo_Sup_least chain_empty) +qed + +end + +lemma admissible_compact_neq' [THEN admissible_subst, cont_intro, simp]: + shows admissible_compact_neq: "compact lub ord k \ ccpo.admissible lub ord (\x. k \ x)" +by(simp add: compact.simps) + +lemma admissible_neq_compact' [THEN admissible_subst, cont_intro, simp]: + shows admissible_neq_compact: "compact lub ord k \ ccpo.admissible lub ord (\x. x \ k)" +by(subst eq_commute)(rule admissible_compact_neq) + +context partial_function_definitions begin + +lemmas [cont_intro, simp] = ccpo.compact_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] + +end + +context ccpo begin + +lemma fixp_strong_induct: + assumes [cont_intro]: "ccpo.admissible Sup op \ P" + and mono: "monotone op \ op \ f" + and bot: "P (\{})" + and step: "\x. \ x \ ccpo_class.fixp f; P x \ \ P (f x)" + shows "P (ccpo_class.fixp f)" +proof(rule fixp_induct[where P="\x. x \ ccpo_class.fixp f \ P x", THEN conjunct2]) + note [cont_intro] = admissible_leI + show "ccpo.admissible Sup op \ (\x. x \ ccpo_class.fixp f \ P x)" by simp +next + show "\{} \ ccpo_class.fixp f \ P (\{})" + by(auto simp add: bot intro: ccpo_Sup_least chain_empty) +next + fix x + assume "x \ ccpo_class.fixp f \ P x" + thus "f x \ ccpo_class.fixp f \ P (f x)" + by(subst fixp_unfold[OF mono])(auto dest: monotoneD[OF mono] intro: step) +qed(rule mono) + +end + +context partial_function_definitions begin + +lemma fixp_strong_induct_uc: + fixes F :: "'c \ 'c" + and U :: "'c \ 'b \ 'a" + and C :: "('b \ 'a) \ 'c" + and P :: "('b \ 'a) \ bool" + assumes mono: "\x. mono_body (\f. U (F (C f)) x)" + and eq: "f \ C (fixp_fun (\f. U (F (C f))))" + and inverse: "\f. U (C f) = f" + and adm: "ccpo.admissible lub_fun le_fun P" + and bot: "P (\_. lub {})" + and step: "\f'. \ P (U f'); le_fun (U f') (U f) \ \ P (U (F f'))" + shows "P (U f)" +unfolding eq inverse +apply (rule ccpo.fixp_strong_induct[OF ccpo adm]) +apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2] +apply (rule_tac f'5="C x" in step) +apply (simp_all add: inverse eq) +done + +end + +subsection {* @{term "op ="} as order *} + +definition lub_singleton :: "('a set \ 'a) \ bool" +where "lub_singleton lub \ (\a. lub {a} = a)" + +definition the_Sup :: "'a set \ 'a" +where "the_Sup A = (THE a. a \ A)" + +lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup" +by(simp add: lub_singleton_def the_Sup_def) + +lemma (in ccpo) lub_singleton: "lub_singleton Sup" +by(simp add: lub_singleton_def) + +lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub" +by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms]) + +lemma preorder_eq [cont_intro, simp]: + "class.preorder op = (mk_less op =)" +by(unfold_locales)(simp_all add: mk_less_def) + +lemma monotone_eqI [cont_intro]: + assumes "class.preorder ord (mk_less ord)" + shows "monotone op = ord f" +proof - + interpret preorder ord "mk_less ord" by fact + show ?thesis by(simp add: monotone_def) +qed + +lemma cont_eqI [cont_intro]: + fixes f :: "'a \ 'b" + assumes "lub_singleton lub" + shows "cont the_Sup op = lub ord f" +proof(rule contI) + fix Y :: "'a set" + assume "Complete_Partial_Order.chain op = Y" "Y \ {}" + then obtain a where "Y = {a}" by(auto simp add: chain_def) + thus "f (the_Sup Y) = lub (f ` Y)" using assms + by(simp add: the_Sup_def lub_singleton_def) +qed + +lemma mcont_eqI [cont_intro, simp]: + "\ class.preorder ord (mk_less ord); lub_singleton lub \ + \ mcont the_Sup op = lub ord f" +by(simp add: mcont_def cont_eqI monotone_eqI) + +subsection {* ccpo for products *} + +definition prod_lub :: "('a set \ 'a) \ ('b set \ 'b) \ ('a \ 'b) set \ 'a \ 'b" +where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))" + +lemma lub_singleton_prod_lub [cont_intro, simp]: + "\ lub_singleton luba; lub_singleton lubb \ \ lub_singleton (prod_lub luba lubb)" +by(simp add: lub_singleton_def prod_lub_def) + +lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})" +by(simp add: prod_lub_def) + +lemma preorder_rel_prodI [cont_intro, simp]: + assumes "class.preorder orda (mk_less orda)" + and "class.preorder ordb (mk_less ordb)" + shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))" +proof - + interpret a: preorder orda "mk_less orda" by fact + interpret b: preorder ordb "mk_less ordb" by fact + show ?thesis by(unfold_locales)(auto simp add: mk_less_def intro: a.order_trans b.order_trans) +qed + +lemma order_rel_prodI: + assumes a: "class.order orda (mk_less orda)" + and b: "class.order ordb (mk_less ordb)" + shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))" + (is "class.order ?ord ?ord'") +proof(intro class.order.intro class.order_axioms.intro) + interpret a: order orda "mk_less orda" by(fact a) + interpret b: order ordb "mk_less ordb" by(fact b) + show "class.preorder ?ord ?ord'" by(rule preorder_rel_prodI) unfold_locales + + fix x y + assume "?ord x y" "?ord y x" + thus "x = y" by(cases x y rule: prod.exhaust[case_product prod.exhaust]) auto +qed + +lemma monotone_rel_prodI: + assumes mono2: "\a. monotone ordb ordc (\b. f (a, b))" + and mono1: "\b. monotone orda ordc (\a. f (a, b))" + and a: "class.preorder orda (mk_less orda)" + and b: "class.preorder ordb (mk_less ordb)" + and c: "class.preorder ordc (mk_less ordc)" + shows "monotone (rel_prod orda ordb) ordc f" +proof - + interpret a: preorder orda "mk_less orda" by(rule a) + interpret b: preorder ordb "mk_less ordb" by(rule b) + interpret c: preorder ordc "mk_less ordc" by(rule c) + show ?thesis using mono2 mono1 + by(auto 7 2 simp add: monotone_def intro: c.order_trans) +qed + +lemma monotone_rel_prodD1: + assumes mono: "monotone (rel_prod orda ordb) ordc f" + and preorder: "class.preorder ordb (mk_less ordb)" + shows "monotone orda ordc (\a. f (a, b))" +proof - + interpret preorder ordb "mk_less ordb" by(rule preorder) + show ?thesis using mono by(simp add: monotone_def) +qed + +lemma monotone_rel_prodD2: + assumes mono: "monotone (rel_prod orda ordb) ordc f" + and preorder: "class.preorder orda (mk_less orda)" + shows "monotone ordb ordc (\b. f (a, b))" +proof - + interpret preorder orda "mk_less orda" by(rule preorder) + show ?thesis using mono by(simp add: monotone_def) +qed + +lemma monotone_case_prodI: + "\ \a. monotone ordb ordc (f a); \b. monotone orda ordc (\a. f a b); + class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb); + class.preorder ordc (mk_less ordc) \ + \ monotone (rel_prod orda ordb) ordc (case_prod f)" +by(rule monotone_rel_prodI) simp_all + +lemma monotone_case_prodD1: + assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)" + and preorder: "class.preorder ordb (mk_less ordb)" + shows "monotone orda ordc (\a. f a b)" +using monotone_rel_prodD1[OF assms] by simp + +lemma monotone_case_prodD2: + assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)" + and preorder: "class.preorder orda (mk_less orda)" + shows "monotone ordb ordc (f a)" +using monotone_rel_prodD2[OF assms] by simp + +context + fixes orda ordb ordc + assumes a: "class.preorder orda (mk_less orda)" + and b: "class.preorder ordb (mk_less ordb)" + and c: "class.preorder ordc (mk_less ordc)" +begin + +lemma monotone_rel_prod_iff: + "monotone (rel_prod orda ordb) ordc f \ + (\a. monotone ordb ordc (\b. f (a, b))) \ + (\b. monotone orda ordc (\a. f (a, b)))" +using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2) + +lemma monotone_case_prod_iff [simp]: + "monotone (rel_prod orda ordb) ordc (case_prod f) \ + (\a. monotone ordb ordc (f a)) \ (\b. monotone orda ordc (\a. f a b))" +by(simp add: monotone_rel_prod_iff) + +end + +lemma monotone_case_prod_apply_iff: + "monotone orda ordb (\x. (case_prod f x) y) \ monotone orda ordb (case_prod (\a b. f a b y))" +by(simp add: monotone_def) + +lemma monotone_case_prod_applyD: + "monotone orda ordb (\x. (case_prod f x) y) + \ monotone orda ordb (case_prod (\a b. f a b y))" +by(simp add: monotone_case_prod_apply_iff) + +lemma monotone_case_prod_applyI: + "monotone orda ordb (case_prod (\a b. f a b y)) + \ monotone orda ordb (\x. (case_prod f x) y)" +by(simp add: monotone_case_prod_apply_iff) + + +lemma cont_case_prod_apply_iff: + "cont luba orda lubb ordb (\x. (case_prod f x) y) \ cont luba orda lubb ordb (case_prod (\a b. f a b y))" +by(simp add: cont_def split_def) + +lemma cont_case_prod_applyI: + "cont luba orda lubb ordb (case_prod (\a b. f a b y)) + \ cont luba orda lubb ordb (\x. (case_prod f x) y)" +by(simp add: cont_case_prod_apply_iff) + +lemma cont_case_prod_applyD: + "cont luba orda lubb ordb (\x. (case_prod f x) y) + \ cont luba orda lubb ordb (case_prod (\a b. f a b y))" +by(simp add: cont_case_prod_apply_iff) + +lemma mcont_case_prod_apply_iff [simp]: + "mcont luba orda lubb ordb (\x. (case_prod f x) y) \ + mcont luba orda lubb ordb (case_prod (\a b. f a b y))" +by(simp add: mcont_def monotone_case_prod_apply_iff cont_case_prod_apply_iff) + +lemma cont_prodD1: + assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f" + and "class.preorder orda (mk_less orda)" + and luba: "lub_singleton luba" + shows "cont lubb ordb lubc ordc (\y. f (x, y))" +proof(rule contI) + interpret preorder orda "mk_less orda" by fact + + fix Y :: "'b set" + let ?Y = "{x} \ Y" + assume "Complete_Partial_Order.chain ordb Y" "Y \ {}" + hence "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \ {}" + by(simp_all add: chain_def) + with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD) + moreover have "f ` ?Y = (\y. f (x, y)) ` Y" by auto + ultimately show "f (x, lubb Y) = lubc ((\y. f (x, y)) ` Y)" using luba + by(simp add: prod_lub_def `Y \ {}` lub_singleton_def) +qed + +lemma cont_prodD2: + assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f" + and "class.preorder ordb (mk_less ordb)" + and lubb: "lub_singleton lubb" + shows "cont luba orda lubc ordc (\x. f (x, y))" +proof(rule contI) + interpret preorder ordb "mk_less ordb" by fact + + fix Y + assume Y: "Complete_Partial_Order.chain orda Y" "Y \ {}" + let ?Y = "Y \ {y}" + have "f (luba Y, y) = f (prod_lub luba lubb ?Y)" + using lubb by(simp add: prod_lub_def Y lub_singleton_def) + also from Y have "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \ {}" + by(simp_all add: chain_def) + with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD) + also have "f ` ?Y = (\x. f (x, y)) ` Y" by auto + finally show "f (luba Y, y) = lubc \" . +qed + +lemma cont_case_prodD1: + assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)" + and "class.preorder orda (mk_less orda)" + and "lub_singleton luba" + shows "cont lubb ordb lubc ordc (f x)" +using cont_prodD1[OF assms] by simp + +lemma cont_case_prodD2: + assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)" + and "class.preorder ordb (mk_less ordb)" + and "lub_singleton lubb" + shows "cont luba orda lubc ordc (\x. f x y)" +using cont_prodD2[OF assms] by simp + +context ccpo begin + +lemma cont_prodI: + assumes mono: "monotone (rel_prod orda ordb) op \ f" + and cont1: "\x. cont lubb ordb Sup op \ (\y. f (x, y))" + and cont2: "\y. cont luba orda Sup op \ (\x. f (x, y))" + and "class.preorder orda (mk_less orda)" + and "class.preorder ordb (mk_less ordb)" + shows "cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \ f" +proof(rule contI) + interpret a: preorder orda "mk_less orda" by fact + interpret b: preorder ordb "mk_less ordb" by fact + + fix Y + assume chain: "Complete_Partial_Order.chain (rel_prod orda ordb) Y" + and "Y \ {}" + have "f (prod_lub luba lubb Y) = f (luba (fst ` Y), lubb (snd ` Y))" + by(simp add: prod_lub_def) + also from cont2 have "f (luba (fst ` Y), lubb (snd ` Y)) = \((\x. f (x, lubb (snd ` Y))) ` fst ` Y)" + by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] `Y \ {}`) + also from cont1 have "\x. f (x, lubb (snd ` Y)) = \((\y. f (x, y)) ` snd ` Y)" + by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] `Y \ {}`) + hence "\((\x. f (x, lubb (snd ` Y))) ` fst ` Y) = \((\x. \ x) ` fst ` Y)" by simp + also have "\ = \((\x. f (fst x, snd x)) ` Y)" + unfolding image_image split_def using chain + apply(rule diag_Sup) + using monotoneD[OF mono] + by(auto intro: monotoneI) + finally show "f (prod_lub luba lubb Y) = \(f ` Y)" by simp +qed + +lemma cont_case_prodI: + assumes "monotone (rel_prod orda ordb) op \ (case_prod f)" + and "\x. cont lubb ordb Sup op \ (\y. f x y)" + and "\y. cont luba orda Sup op \ (\x. f x y)" + and "class.preorder orda (mk_less orda)" + and "class.preorder ordb (mk_less ordb)" + shows "cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \ (case_prod f)" +by(rule cont_prodI)(simp_all add: assms) + +lemma cont_case_prod_iff: + "\ monotone (rel_prod orda ordb) op \ (case_prod f); + class.preorder orda (mk_less orda); lub_singleton luba; + class.preorder ordb (mk_less ordb); lub_singleton lubb \ + \ cont (prod_lub luba lubb) (rel_prod orda ordb) Sup op \ (case_prod f) \ + (\x. cont lubb ordb Sup op \ (\y. f x y)) \ (\y. cont luba orda Sup op \ (\x. f x y))" +by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI) + +end + +context partial_function_definitions begin + +lemma mono2mono2: + assumes f: "monotone (rel_prod ordb ordc) leq (\(x, y). f x y)" + and t: "monotone orda ordb (\x. t x)" + and t': "monotone orda ordc (\x. t' x)" + shows "monotone orda leq (\x. f (t x) (t' x))" +proof(rule monotoneI) + fix x y + assume "orda x y" + hence "rel_prod ordb ordc (t x, t' x) (t y, t' y)" + using t t' by(auto dest: monotoneD) + from monotoneD[OF f this] show "leq (f (t x) (t' x)) (f (t y) (t' y))" by simp +qed + +lemma cont_case_prodI [cont_intro]: + "\ monotone (rel_prod orda ordb) leq (case_prod f); + \x. cont lubb ordb lub leq (\y. f x y); + \y. cont luba orda lub leq (\x. f x y); + class.preorder orda (mk_less orda); + class.preorder ordb (mk_less ordb) \ + \ cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f)" +by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms]) + +lemma cont_case_prod_iff: + "\ monotone (rel_prod orda ordb) leq (case_prod f); + class.preorder orda (mk_less orda); lub_singleton luba; + class.preorder ordb (mk_less ordb); lub_singleton lubb \ + \ cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \ + (\x. cont lubb ordb lub leq (\y. f x y)) \ (\y. cont luba orda lub leq (\x. f x y))" +by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI) + +lemma mcont_case_prod_iff [simp]: + "\ class.preorder orda (mk_less orda); lub_singleton luba; + class.preorder ordb (mk_less ordb); lub_singleton lubb \ + \ mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \ + (\x. mcont lubb ordb lub leq (\y. f x y)) \ (\y. mcont luba orda lub leq (\x. f x y))" +unfolding mcont_def by(auto simp add: cont_case_prod_iff) + +end + +lemma mono2mono_case_prod [cont_intro]: + assumes "\x y. monotone orda ordb (\f. pair f x y)" + shows "monotone orda ordb (\f. case_prod (pair f) x)" +by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms]) + +subsection {* Complete lattices as ccpo *} + +context complete_lattice begin + +lemma complete_lattice_ccpo: "class.ccpo Sup op \ op <" +by(unfold_locales)(fast intro: Sup_upper Sup_least)+ + +lemma complete_lattice_ccpo': "class.ccpo Sup op \ (mk_less op \)" +by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least) + +lemma complete_lattice_partial_function_definitions: + "partial_function_definitions op \ Sup" +by(unfold_locales)(auto intro: Sup_least Sup_upper) + +lemma complete_lattice_partial_function_definitions_dual: + "partial_function_definitions op \ Inf" +by(unfold_locales)(auto intro: Inf_lower Inf_greatest) + +lemmas [cont_intro, simp] = + Partial_Function.ccpo[OF complete_lattice_partial_function_definitions] + Partial_Function.ccpo[OF complete_lattice_partial_function_definitions_dual] + +lemma mono2mono_inf: + assumes f: "monotone ord op \ (\x. f x)" + and g: "monotone ord op \ (\x. g x)" + shows "monotone ord op \ (\x. f x \ g x)" +by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI) + +lemma mcont_const [simp]: "mcont lub ord Sup op \ (\_. c)" +by(rule ccpo.mcont_const[OF complete_lattice_ccpo]) + +lemma mono2mono_sup: + assumes f: "monotone ord op \ (\x. f x)" + and g: "monotone ord op \ (\x. g x)" + shows "monotone ord op \ (\x. f x \ g x)" +by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g]) + +lemma Sup_image_sup: + assumes "Y \ {}" + shows "\(op \ x ` Y) = x \ \Y" +proof(rule Sup_eqI) + fix y + assume "y \ op \ x ` Y" + then obtain z where "y = x \ z" and "z \ Y" by blast + from `z \ Y` have "z \ \Y" by(rule Sup_upper) + with _ show "y \ x \ \Y" unfolding `y = x \ z` by(rule sup_mono) simp +next + fix y + assume upper: "\z. z \ op \ x ` Y \ z \ y" + show "x \ \Y \ y" unfolding Sup_insert[symmetric] + proof(rule Sup_least) + fix z + assume "z \ insert x Y" + from assms obtain z' where "z' \ Y" by blast + let ?z = "if z \ Y then x \ z else x \ z'" + have "z \ x \ ?z" using `z' \ Y` `z \ insert x Y` by auto + also have "\ \ y" by(rule upper)(auto split: if_split_asm intro: `z' \ Y`) + finally show "z \ y" . + qed +qed + +lemma mcont_sup1: "mcont Sup op \ Sup op \ (\y. x \ y)" +by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric]) + +lemma mcont_sup2: "mcont Sup op \ Sup op \ (\x. x \ y)" +by(subst sup_commute)(rule mcont_sup1) + +lemma mcont2mcont_sup [cont_intro, simp]: + "\ mcont lub ord Sup op \ (\x. f x); + mcont lub ord Sup op \ (\x. g x) \ + \ mcont lub ord Sup op \ (\x. f x \ g x)" +by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo]) + +end + +lemmas [cont_intro] = admissible_leI[OF complete_lattice_ccpo'] + +context complete_distrib_lattice begin + +lemma mcont_inf1: "mcont Sup op \ Sup op \ (\y. x \ y)" +by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def) + +lemma mcont_inf2: "mcont Sup op \ Sup op \ (\x. x \ y)" +by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def) + +lemma mcont2mcont_inf [cont_intro, simp]: + "\ mcont lub ord Sup op \ (\x. f x); + mcont lub ord Sup op \ (\x. g x) \ + \ mcont lub ord Sup op \ (\x. f x \ g x)" +by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo]) + +end + +interpretation lfp: partial_function_definitions "op \ :: _ :: complete_lattice \ _" Sup +by(rule complete_lattice_partial_function_definitions) + +declaration {* Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body} + @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE *} + +interpretation gfp: partial_function_definitions "op \ :: _ :: complete_lattice \ _" Inf +by(rule complete_lattice_partial_function_definitions_dual) + +declaration {* Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body} + @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE *} + +lemma insert_mono [partial_function_mono]: + "monotone (fun_ord op \) op \ A \ monotone (fun_ord op \) op \ (\y. insert x (A y))" +by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD) + +lemma mono2mono_insert [THEN lfp.mono2mono, cont_intro, simp]: + shows monotone_insert: "monotone op \ op \ (insert x)" +by(rule monotoneI) blast + +lemma mcont2mcont_insert[THEN lfp.mcont2mcont, cont_intro, simp]: + shows mcont_insert: "mcont Union op \ Union op \ (insert x)" +by(blast intro: mcontI contI monotone_insert) + +lemma mono2mono_image [THEN lfp.mono2mono, cont_intro, simp]: + shows monotone_image: "monotone op \ op \ (op ` f)" +by(rule monotoneI) blast + +lemma cont_image: "cont Union op \ Union op \ (op ` f)" +by(rule contI)(auto) + +lemma mcont2mcont_image [THEN lfp.mcont2mcont, cont_intro, simp]: + shows mcont_image: "mcont Union op \ Union op \ (op ` f)" +by(blast intro: mcontI monotone_image cont_image) + +context complete_lattice begin + +lemma monotone_Sup [cont_intro, simp]: + "monotone ord op \ f \ monotone ord op \ (\x. \f x)" +by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD) + +lemma cont_Sup: + assumes "cont lub ord Union op \ f" + shows "cont lub ord Sup op \ (\x. \f x)" +apply(rule contI) +apply(simp add: contD[OF assms]) +apply(blast intro: Sup_least Sup_upper order_trans antisym) +done + +lemma mcont_Sup: "mcont lub ord Union op \ f \ mcont lub ord Sup op \ (\x. \f x)" +unfolding mcont_def by(blast intro: monotone_Sup cont_Sup) + +lemma monotone_SUP: + "\ monotone ord op \ f; \y. monotone ord op \ (\x. g x y) \ \ monotone ord op \ (\x. \y\f x. g x y)" +by(rule monotoneI)(blast dest: monotoneD intro: Sup_upper order_trans intro!: Sup_least) + +lemma monotone_SUP2: + "(\y. y \ A \ monotone ord op \ (\x. g x y)) \ monotone ord op \ (\x. \y\A. g x y)" +by(rule monotoneI)(blast intro: Sup_upper order_trans dest: monotoneD intro!: Sup_least) + +lemma cont_SUP: + assumes f: "mcont lub ord Union op \ f" + and g: "\y. mcont lub ord Sup op \ (\x. g x y)" + shows "cont lub ord Sup op \ (\x. \y\f x. g x y)" +proof(rule contI) + fix Y + assume chain: "Complete_Partial_Order.chain ord Y" + and Y: "Y \ {}" + show "\(g (lub Y) ` f (lub Y)) = \((\x. \(g x ` f x)) ` Y)" (is "?lhs = ?rhs") + proof(rule antisym) + show "?lhs \ ?rhs" + proof(rule Sup_least) + fix x + assume "x \ g (lub Y) ` f (lub Y)" + with mcont_contD[OF f chain Y] mcont_contD[OF g chain Y] + obtain y z where "y \ Y" "z \ f y" + and x: "x = \((\x. g x z) ` Y)" by auto + show "x \ ?rhs" unfolding x + proof(rule Sup_least) + fix u + assume "u \ (\x. g x z) ` Y" + then obtain y' where "u = g y' z" "y' \ Y" by auto + from chain `y \ Y` `y' \ Y` have "ord y y' \ ord y' y" by(rule chainD) + thus "u \ ?rhs" + proof + note `u = g y' z` also + assume "ord y y'" + with f have "f y \ f y'" by(rule mcont_monoD) + with `z \ f y` + have "g y' z \ \(g y' ` f y')" by(auto intro: Sup_upper) + also have "\ \ ?rhs" using `y' \ Y` by(auto intro: Sup_upper) + finally show ?thesis . + next + note `u = g y' z` also + assume "ord y' y" + with g have "g y' z \ g y z" by(rule mcont_monoD) + also have "\ \ \(g y ` f y)" using `z \ f y` + by(auto intro: Sup_upper) + also have "\ \ ?rhs" using `y \ Y` by(auto intro: Sup_upper) + finally show ?thesis . + qed + qed + qed + next + show "?rhs \ ?lhs" + proof(rule Sup_least) + fix x + assume "x \ (\x. \(g x ` f x)) ` Y" + then obtain y where x: "x = \(g y ` f y)" and "y \ Y" by auto + show "x \ ?lhs" unfolding x + proof(rule Sup_least) + fix u + assume "u \ g y ` f y" + then obtain z where "u = g y z" "z \ f y" by auto + note `u = g y z` + also have "g y z \ \((\x. g x z) ` Y)" + using `y \ Y` by(auto intro: Sup_upper) + also have "\ = g (lub Y) z" by(simp add: mcont_contD[OF g chain Y]) + also have "\ \ ?lhs" using `z \ f y` `y \ Y` + by(auto intro: Sup_upper simp add: mcont_contD[OF f chain Y]) + finally show "u \ ?lhs" . + qed + qed + qed +qed + +lemma mcont_SUP [cont_intro, simp]: + "\ mcont lub ord Union op \ f; \y. mcont lub ord Sup op \ (\x. g x y) \ + \ mcont lub ord Sup op \ (\x. \y\f x. g x y)" +by(blast intro: mcontI cont_SUP[OF assms] monotone_SUP mcont_mono) + +end + +lemma admissible_Ball [cont_intro, simp]: + "\ \x. ccpo.admissible lub ord (\A. P A x); + mcont lub ord Union op \ f; + class.ccpo lub ord (mk_less ord) \ + \ ccpo.admissible lub ord (\A. \x\f A. P A x)" +unfolding Ball_def by simp + +lemma admissible_Bex'[THEN admissible_subst, cont_intro, simp]: + shows admissible_Bex: "ccpo.admissible Union op \ (\A. \x\A. P x)" +by(rule ccpo.admissibleI)(auto) + +subsection {* Parallel fixpoint induction *} + +context + fixes luba :: "'a set \ 'a" + and orda :: "'a \ 'a \ bool" + and lubb :: "'b set \ 'b" + and ordb :: "'b \ 'b \ bool" + assumes a: "class.ccpo luba orda (mk_less orda)" + and b: "class.ccpo lubb ordb (mk_less ordb)" +begin + +interpretation a: ccpo luba orda "mk_less orda" by(rule a) +interpretation b: ccpo lubb ordb "mk_less ordb" by(rule b) + +lemma ccpo_rel_prodI: + "class.ccpo (prod_lub luba lubb) (rel_prod orda ordb) (mk_less (rel_prod orda ordb))" + (is "class.ccpo ?lub ?ord ?ord'") +proof(intro class.ccpo.intro class.ccpo_axioms.intro) + show "class.order ?ord ?ord'" by(rule order_rel_prodI) intro_locales +qed(auto 4 4 simp add: prod_lub_def intro: a.ccpo_Sup_upper b.ccpo_Sup_upper a.ccpo_Sup_least b.ccpo_Sup_least rev_image_eqI dest: chain_rel_prodD1 chain_rel_prodD2) + +interpretation ab: ccpo "prod_lub luba lubb" "rel_prod orda ordb" "mk_less (rel_prod orda ordb)" +by(rule ccpo_rel_prodI) + +lemma monotone_map_prod [simp]: + "monotone (rel_prod orda ordb) (rel_prod ordc ordd) (map_prod f g) \ + monotone orda ordc f \ monotone ordb ordd g" +by(auto simp add: monotone_def) + +lemma parallel_fixp_induct: + assumes adm: "ccpo.admissible (prod_lub luba lubb) (rel_prod orda ordb) (\x. P (fst x) (snd x))" + and f: "monotone orda orda f" + and g: "monotone ordb ordb g" + and bot: "P (luba {}) (lubb {})" + and step: "\x y. P x y \ P (f x) (g y)" + shows "P (ccpo.fixp luba orda f) (ccpo.fixp lubb ordb g)" +proof - + let ?lub = "prod_lub luba lubb" + and ?ord = "rel_prod orda ordb" + and ?P = "\(x, y). P x y" + from adm have adm': "ccpo.admissible ?lub ?ord ?P" by(simp add: split_def) + hence "?P (ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g))" + by(rule ab.fixp_induct)(auto simp add: f g step bot) + also have "ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g) = + (ccpo.fixp luba orda f, ccpo.fixp lubb ordb g)" (is "?lhs = (?rhs1, ?rhs2)") + proof(rule ab.antisym) + have "ccpo.admissible ?lub ?ord (\xy. ?ord xy (?rhs1, ?rhs2))" + by(rule admissible_leI[OF ccpo_rel_prodI])(auto simp add: prod_lub_def chain_empty intro: a.ccpo_Sup_least b.ccpo_Sup_least) + thus "?ord ?lhs (?rhs1, ?rhs2)" + by(rule ab.fixp_induct)(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] simp add: b.fixp_unfold[OF g, symmetric] a.fixp_unfold[OF f, symmetric] f g intro: a.ccpo_Sup_least b.ccpo_Sup_least chain_empty) + next + have "ccpo.admissible luba orda (\x. orda x (fst ?lhs))" + by(rule admissible_leI[OF a])(auto intro: a.ccpo_Sup_least simp add: chain_empty) + hence "orda ?rhs1 (fst ?lhs)" using f + proof(rule a.fixp_induct) + fix x + assume "orda x (fst ?lhs)" + thus "orda (f x) (fst ?lhs)" + by(subst ab.fixp_unfold)(auto simp add: f g dest: monotoneD[OF f]) + qed(auto intro: a.ccpo_Sup_least chain_empty) + moreover + have "ccpo.admissible lubb ordb (\y. ordb y (snd ?lhs))" + by(rule admissible_leI[OF b])(auto intro: b.ccpo_Sup_least simp add: chain_empty) + hence "ordb ?rhs2 (snd ?lhs)" using g + proof(rule b.fixp_induct) + fix y + assume "ordb y (snd ?lhs)" + thus "ordb (g y) (snd ?lhs)" + by(subst ab.fixp_unfold)(auto simp add: f g dest: monotoneD[OF g]) + qed(auto intro: b.ccpo_Sup_least chain_empty) + ultimately show "?ord (?rhs1, ?rhs2) ?lhs" + by(simp add: rel_prod_conv split_beta) + qed + finally show ?thesis by simp +qed + +end + +lemma parallel_fixp_induct_uc: + assumes a: "partial_function_definitions orda luba" + and b: "partial_function_definitions ordb lubb" + and F: "\x. monotone (fun_ord orda) orda (\f. U1 (F (C1 f)) x)" + and G: "\y. monotone (fun_ord ordb) ordb (\g. U2 (G (C2 g)) y)" + and eq1: "f \ C1 (ccpo.fixp (fun_lub luba) (fun_ord orda) (\f. U1 (F (C1 f))))" + and eq2: "g \ C2 (ccpo.fixp (fun_lub lubb) (fun_ord ordb) (\g. U2 (G (C2 g))))" + and inverse: "\f. U1 (C1 f) = f" + and inverse2: "\g. U2 (C2 g) = g" + and adm: "ccpo.admissible (prod_lub (fun_lub luba) (fun_lub lubb)) (rel_prod (fun_ord orda) (fun_ord ordb)) (\x. P (fst x) (snd x))" + and bot: "P (\_. luba {}) (\_. lubb {})" + and step: "\f g. P (U1 f) (U2 g) \ P (U1 (F f)) (U2 (G g))" + shows "P (U1 f) (U2 g)" +apply(unfold eq1 eq2 inverse inverse2) +apply(rule parallel_fixp_induct[OF partial_function_definitions.ccpo[OF a] partial_function_definitions.ccpo[OF b] adm]) +using F apply(simp add: monotone_def fun_ord_def) +using G apply(simp add: monotone_def fun_ord_def) +apply(simp add: fun_lub_def bot) +apply(rule step, simp add: inverse inverse2) +done + +lemmas parallel_fixp_induct_1_1 = parallel_fixp_induct_uc[ + of _ _ _ _ "\x. x" _ "\x. x" "\x. x" _ "\x. x", + OF _ _ _ _ _ _ refl refl] + +lemmas parallel_fixp_induct_2_2 = parallel_fixp_induct_uc[ + of _ _ _ _ "case_prod" _ "curry" "case_prod" _ "curry", + where P="\f g. P (curry f) (curry g)", + unfolded case_prod_curry curry_case_prod curry_K, + OF _ _ _ _ _ _ refl refl] + for P + +lemma monotone_fst: "monotone (rel_prod orda ordb) orda fst" +by(auto intro: monotoneI) + +lemma mcont_fst: "mcont (prod_lub luba lubb) (rel_prod orda ordb) luba orda fst" +by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def) + +lemma mcont2mcont_fst [cont_intro, simp]: + "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t + \ mcont lub ord luba orda (\x. fst (t x))" +by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image) + +lemma monotone_snd: "monotone (rel_prod orda ordb) ordb snd" +by(auto intro: monotoneI) + +lemma mcont_snd: "mcont (prod_lub luba lubb) (rel_prod orda ordb) lubb ordb snd" +by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def) + +lemma mcont2mcont_snd [cont_intro, simp]: + "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t + \ mcont lub ord lubb ordb (\x. snd (t x))" +by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image) + +context partial_function_definitions begin +text \Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\ +lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst] +lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd] +end + +end diff -r 66568c9b8216 -r d3a5b127eb81 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Fri Mar 18 12:48:00 2016 +0100 +++ b/src/HOL/Library/Library.thy Fri Mar 18 12:54:20 2016 +0100 @@ -11,6 +11,7 @@ Code_Test ContNotDenum Convex + Complete_Partial_Order2 Countable Countable_Complete_Lattices Countable_Set_Type