author  Peter Lammich 
Mon, 28 Oct 2019 18:50:40 +0000  
changeset 70961  70fb697be418 
parent 69593  3dda49e08b9d 
permissions  rwrr 
62858  1 
(* Title: HOL/Library/Complete_Partial_Order2.thy 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

2 
Author: Andreas Lochbihler, ETH Zurich 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

3 
*) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

4 

62837  5 
section \<open>Formalisation of chaincomplete partial orders, continuity and admissibility\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

6 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

7 
theory Complete_Partial_Order2 imports 
65366  8 
Main Lattice_Syntax 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

9 
begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

10 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

11 
lemma chain_transfer [transfer_rule]: 
63343  12 
includes lifting_syntax 
67399  13 
shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

14 
unfolding chain_def[abs_def] by transfer_prover 
68980
5717fbc55521
added spaces because otherwise nonatomic arguments look awful: BIGf x > BIG f x
nipkow
parents:
67399
diff
changeset

15 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

16 
lemma linorder_chain [simp, intro!]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

17 
fixes Y :: "_ :: linorder set" 
67399  18 
shows "Complete_Partial_Order.chain (\<le>) Y" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

19 
by(auto intro: chainI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

20 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

21 
lemma fun_lub_apply: "\<And>Sup. fun_lub Sup Y x = Sup ((\<lambda>f. f x) ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

22 
by(simp add: fun_lub_def image_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

23 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

24 
lemma fun_lub_empty [simp]: "fun_lub lub {} = (\<lambda>_. lub {})" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

25 
by(rule ext)(simp add: fun_lub_apply) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

26 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

27 
lemma chain_fun_ordD: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

28 
assumes "Complete_Partial_Order.chain (fun_ord le) Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

29 
shows "Complete_Partial_Order.chain le ((\<lambda>f. f x) ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

30 
by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

31 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

32 
lemma chain_Diff: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

33 
"Complete_Partial_Order.chain ord A 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

34 
\<Longrightarrow> Complete_Partial_Order.chain ord (A  B)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

35 
by(erule chain_subset) blast 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

36 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

37 
lemma chain_rel_prodD1: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

38 
"Complete_Partial_Order.chain (rel_prod orda ordb) Y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

39 
\<Longrightarrow> Complete_Partial_Order.chain orda (fst ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

40 
by(auto 4 3 simp add: chain_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

41 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

42 
lemma chain_rel_prodD2: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

43 
"Complete_Partial_Order.chain (rel_prod orda ordb) Y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

44 
\<Longrightarrow> Complete_Partial_Order.chain ordb (snd ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

45 
by(auto 4 3 simp add: chain_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

46 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

47 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

48 
context ccpo begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

49 

67399  50 
lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord (\<le>)) (mk_less (fun_ord (\<le>)))" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

51 
by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

52 
intro: order.trans antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

53 

67399  54 
lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain (\<le>) Y \<Longrightarrow> Sup Y \<le> x \<longleftrightarrow> (\<forall>y\<in>Y. y \<le> x)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

55 
by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

56 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

57 
lemma Sup_minus_bot: 
67399  58 
assumes chain: "Complete_Partial_Order.chain (\<le>) A" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

59 
shows "\<Squnion>(A  {\<Squnion>{}}) = \<Squnion>A" 
63649  60 
(is "?lhs = ?rhs") 
61 
proof (rule antisym) 

62 
show "?lhs \<le> ?rhs" 

63 
by (blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain]) 

64 
show "?rhs \<le> ?lhs" 

65 
proof (rule ccpo_Sup_least [OF chain]) 

66 
show "x \<in> A \<Longrightarrow> x \<le> ?lhs" for x 

67 
by (cases "x = \<Squnion>{}") 

68 
(blast intro: ccpo_Sup_least chain_empty ccpo_Sup_upper[OF chain_Diff[OF chain]])+ 

69 
qed 

70 
qed 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

71 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

72 
lemma mono_lub: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

73 
fixes le_b (infix "\<sqsubseteq>" 60) 
67399  74 
assumes chain: "Complete_Partial_Order.chain (fun_ord (\<le>)) Y" 
75 
and mono: "\<And>f. f \<in> Y \<Longrightarrow> monotone le_b (\<le>) f" 

76 
shows "monotone (\<sqsubseteq>) (\<le>) (fun_lub Sup Y)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

77 
proof(rule monotoneI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

78 
fix x y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

79 
assume "x \<sqsubseteq> y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

80 

67399  81 
have chain'': "\<And>x. Complete_Partial_Order.chain (\<le>) ((\<lambda>f. f x) ` Y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

82 
using chain by(rule chain_imageI)(simp add: fun_ord_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

83 
then show "fun_lub Sup Y x \<le> fun_lub Sup Y y" unfolding fun_lub_apply 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

84 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

85 
fix x' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

86 
assume "x' \<in> (\<lambda>f. f x) ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

87 
then obtain f where "f \<in> Y" "x' = f x" by blast 
62837  88 
note \<open>x' = f x\<close> also 
89 
from \<open>f \<in> Y\<close> \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" by(blast dest: mono monotoneD) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

90 
also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain'' 
62837  91 
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Y\<close>) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

92 
finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

93 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

94 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

95 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

96 
context 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

97 
fixes le_b (infix "\<sqsubseteq>" 60) and Y f 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

98 
assumes chain: "Complete_Partial_Order.chain le_b Y" 
67399  99 
and mono1: "\<And>y. y \<in> Y \<Longrightarrow> monotone le_b (\<le>) (\<lambda>x. f x y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

100 
and mono2: "\<And>x a b. \<lbrakk> x \<in> Y; a \<sqsubseteq> b; a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> f x a \<le> f x b" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

101 
begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

102 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

103 
lemma Sup_mono: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

104 
assumes le: "x \<sqsubseteq> y" and x: "x \<in> Y" and y: "y \<in> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

105 
shows "\<Squnion>(f x ` Y) \<le> \<Squnion>(f y ` Y)" (is "_ \<le> ?rhs") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

106 
proof(rule ccpo_Sup_least) 
67399  107 
from chain show chain': "Complete_Partial_Order.chain (\<le>) (f x ` Y)" when "x \<in> Y" for x 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

108 
by(rule chain_imageI) (insert that, auto dest: mono2) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

109 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

110 
fix x' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

111 
assume "x' \<in> f x ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

112 
then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2) 
62837  113 
also from mono1[OF \<open>y' \<in> Y\<close>] le have "\<dots> \<le> f y y'" by(rule monotoneD) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

114 
also have "\<dots> \<le> ?rhs" using chain'[OF y] 
62837  115 
by (auto intro!: ccpo_Sup_upper simp add: \<open>y' \<in> Y\<close>) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

116 
finally show "x' \<le> ?rhs" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

117 
qed(rule x) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

118 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

119 
lemma diag_Sup: "\<Squnion>((\<lambda>x. \<Squnion>(f x ` Y)) ` Y) = \<Squnion>((\<lambda>x. f x x) ` Y)" (is "?lhs = ?rhs") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

120 
proof(rule antisym) 
67399  121 
have chain1: "Complete_Partial_Order.chain (\<le>) ((\<lambda>x. \<Squnion>(f x ` Y)) ` Y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

122 
using chain by(rule chain_imageI)(rule Sup_mono) 
67399  123 
have chain2: "\<And>y'. y' \<in> Y \<Longrightarrow> Complete_Partial_Order.chain (\<le>) (f y' ` Y)" using chain 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

124 
by(rule chain_imageI)(auto dest: mono2) 
67399  125 
have chain3: "Complete_Partial_Order.chain (\<le>) ((\<lambda>x. f x x) ` Y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

126 
using chain by(rule chain_imageI)(auto intro: monotoneD[OF mono1] mono2 order.trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

127 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

128 
show "?lhs \<le> ?rhs" using chain1 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

129 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

130 
fix x' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

131 
assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

132 
then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2) 
62837  133 
also have "\<dots> \<le> ?rhs" using chain2[OF \<open>y' \<in> Y\<close>] 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

134 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

135 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

136 
assume "x \<in> f y' ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

137 
then obtain y where "y \<in> Y" and x: "x = f y' y" by blast 
63040  138 
define y'' where "y'' = (if y \<sqsubseteq> y' then y' else y)" 
62837  139 
from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD) 
140 
hence "f y' y \<le> f y'' y''" using \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

141 
by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1]) 
62837  142 
also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def) 
143 
from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: \<open>y'' \<in> Y\<close>) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

144 
finally show "x \<le> ?rhs" by(simp add: x) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

145 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

146 
finally show "x' \<le> ?rhs" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

147 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

148 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

149 
show "?rhs \<le> ?lhs" using chain3 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

150 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

151 
fix y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

152 
assume "y \<in> (\<lambda>x. f x x) ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

153 
then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2) 
62837  154 
also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)" 
155 
by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>) 

156 
also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

157 
finally show "y \<le> ?lhs" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

158 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

159 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

160 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

161 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

162 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

163 
lemma Sup_image_mono_le: 
69038  164 
fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>") 
67399  165 
assumes ccpo: "class.ccpo Sup_b (\<sqsubseteq>) lt_b" 
166 
assumes chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

167 
and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

168 
shows "Sup (f ` Y) \<le> f (\<Or>Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

169 
proof(rule ccpo_Sup_least) 
67399  170 
show "Complete_Partial_Order.chain (\<le>) (f ` Y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

171 
using chain by(rule chain_imageI)(rule mono) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

172 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

173 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

174 
assume "x \<in> f ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

175 
then obtain y where "y \<in> Y" and "x = f y" by blast note this(2) 
62837  176 
also have "y \<sqsubseteq> \<Or>Y" using ccpo chain \<open>y \<in> Y\<close> by(rule ccpo.ccpo_Sup_upper) 
177 
hence "f y \<le> f (\<Or>Y)" using \<open>y \<in> Y\<close> by(rule mono) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

178 
finally show "x \<le> \<dots>" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

179 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

180 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

181 
lemma swap_Sup: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

182 
fixes le_b (infix "\<sqsubseteq>" 60) 
67399  183 
assumes Y: "Complete_Partial_Order.chain (\<sqsubseteq>) Y" 
184 
and Z: "Complete_Partial_Order.chain (fun_ord (\<le>)) Z" 

185 
and mono: "\<And>f. f \<in> Z \<Longrightarrow> monotone (\<sqsubseteq>) (\<le>) f" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

186 
shows "\<Squnion>((\<lambda>x. \<Squnion>(x ` Y)) ` Z) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

187 
(is "?lhs = ?rhs") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

188 
proof(cases "Y = {}") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

189 
case True 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

190 
then show ?thesis 
69546
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69164
diff
changeset

191 
by (simp add: image_constant_conv cong del: SUP_cong_simp) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

192 
next 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

193 
case False 
67399  194 
have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain (\<le>) (f ` Y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

195 
by(rule chain_imageI[OF Y])(rule monotoneD[OF mono]) 
67399  196 
have chain2: "Complete_Partial_Order.chain (\<le>) ((\<lambda>x. \<Squnion>(x ` Y)) ` Z)" using Z 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

197 
proof(rule chain_imageI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

198 
fix f g 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

199 
assume "f \<in> Z" "g \<in> Z" 
67399  200 
and "fun_ord (\<le>) f g" 
62837  201 
from chain1[OF \<open>f \<in> Z\<close>] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

202 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

203 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

204 
assume "x \<in> f ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

205 
then obtain y where "y \<in> Y" "x = f y" by blast note this(2) 
67399  206 
also have "\<dots> \<le> g y" using \<open>fun_ord (\<le>) f g\<close> by(simp add: fun_ord_def) 
62837  207 
also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF \<open>g \<in> Z\<close>] 
208 
by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

209 
finally show "x \<le> \<Squnion>(g ` Y)" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

210 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

211 
qed 
67399  212 
have chain3: "\<And>x. Complete_Partial_Order.chain (\<le>) ((\<lambda>f. f x) ` Z)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

213 
using Z by(rule chain_imageI)(simp add: fun_ord_def) 
67399  214 
have chain4: "Complete_Partial_Order.chain (\<le>) ((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

215 
using Y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

216 
proof(rule chain_imageI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

217 
fix f x y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

218 
assume "x \<sqsubseteq> y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

219 
show "\<Squnion>((\<lambda>f. f x) ` Z) \<le> \<Squnion>((\<lambda>f. f y) ` Z)" (is "_ \<le> ?rhs") using chain3 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

220 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

221 
fix x' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

222 
assume "x' \<in> (\<lambda>f. f x) ` Z" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

223 
then obtain f where "f \<in> Z" "x' = f x" by blast note this(2) 
62837  224 
also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono]) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

225 
also have "f y \<le> ?rhs" using chain3 
62837  226 
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

227 
finally show "x' \<le> ?rhs" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

228 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

229 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

230 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

231 
from chain2 have "?lhs \<le> ?rhs" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

232 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

233 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

234 
assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

235 
then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2) 
62837  236 
also have "\<dots> \<le> ?rhs" using chain1[OF \<open>f \<in> Z\<close>] 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

237 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

238 
fix x' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

239 
assume "x' \<in> f ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

240 
then obtain y where "y \<in> Y" "x' = f y" by blast note this(2) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

241 
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3 
62837  242 
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>) 
243 
also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

244 
finally show "x' \<le> ?rhs" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

245 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

246 
finally show "x \<le> ?rhs" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

247 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

248 
moreover 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

249 
have "?rhs \<le> ?lhs" using chain4 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

250 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

251 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

252 
assume "x \<in> (\<lambda>x. \<Squnion>((\<lambda>f. f x) ` Z)) ` Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

253 
then obtain y where "y \<in> Y" "x = \<Squnion>((\<lambda>f. f y) ` Z)" by blast note this(2) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

254 
also have "\<dots> \<le> ?lhs" using chain3 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

255 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

256 
fix x' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

257 
assume "x' \<in> (\<lambda>f. f y) ` Z" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

258 
then obtain f where "f \<in> Z" "x' = f y" by blast note this(2) 
62837  259 
also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>] 
260 
by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

261 
also have "\<dots> \<le> ?lhs" using chain2 
62837  262 
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

263 
finally show "x' \<le> ?lhs" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

264 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

265 
finally show "x \<le> ?lhs" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

266 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

267 
ultimately show "?lhs = ?rhs" by(rule antisym) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

268 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

269 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

270 
lemma fixp_mono: 
67399  271 
assumes fg: "fun_ord (\<le>) f g" 
272 
and f: "monotone (\<le>) (\<le>) f" 

273 
and g: "monotone (\<le>) (\<le>) g" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

274 
shows "ccpo_class.fixp f \<le> ccpo_class.fixp g" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

275 
unfolding fixp_def 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

276 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

277 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

278 
assume "x \<in> ccpo_class.iterates f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

279 
thus "x \<le> \<Squnion>ccpo_class.iterates g" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

280 
proof induction 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

281 
case (step x) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

282 
from f step.IH have "f x \<le> f (\<Squnion>ccpo_class.iterates g)" by(rule monotoneD) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

283 
also have "\<dots> \<le> g (\<Squnion>ccpo_class.iterates g)" using fg by(simp add: fun_ord_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

284 
also have "\<dots> = \<Squnion>ccpo_class.iterates g" by(fold fixp_def fixp_unfold[OF g]) simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

285 
finally show ?case . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

286 
qed(blast intro: ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

287 
qed(rule chain_iterates[OF f]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

288 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

289 
context fixes ordb :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

290 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

291 
lemma iterates_mono: 
67399  292 
assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord (\<le>)) F" 
293 
and mono: "\<And>f. monotone (\<sqsubseteq>) (\<le>) f \<Longrightarrow> monotone (\<sqsubseteq>) (\<le>) (F f)" 

294 
shows "monotone (\<sqsubseteq>) (\<le>) f" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

295 
using f 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

296 
by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mono_lub)+ 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

297 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

298 
lemma fixp_preserves_mono: 
67399  299 
assumes mono: "\<And>x. monotone (fun_ord (\<le>)) (\<le>) (\<lambda>f. F f x)" 
300 
and mono2: "\<And>f. monotone (\<sqsubseteq>) (\<le>) f \<Longrightarrow> monotone (\<sqsubseteq>) (\<le>) (F f)" 

301 
shows "monotone (\<sqsubseteq>) (\<le>) (ccpo.fixp (fun_lub Sup) (fun_ord (\<le>)) F)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

302 
(is "monotone _ _ ?fixp") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

303 
proof(rule monotoneI) 
67399  304 
have mono: "monotone (fun_ord (\<le>)) (fun_ord (\<le>)) F" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

305 
by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono]) 
67399  306 
let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord (\<le>)) F" 
307 
have chain: "\<And>x. Complete_Partial_Order.chain (\<le>) ((\<lambda>f. f x) ` ?iter)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

308 
by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

309 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

310 
fix x y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

311 
assume "x \<sqsubseteq> y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

312 
show "?fixp x \<le> ?fixp y" 
63170  313 
apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply) 
314 
using chain 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

315 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

316 
fix x' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

317 
assume "x' \<in> (\<lambda>f. f x) ` ?iter" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

318 
then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

319 
also have "f x \<le> f y" 
62837  320 
by(rule monotoneD[OF iterates_mono[OF \<open>f \<in> ?iter\<close> mono2]])(blast intro: \<open>x \<sqsubseteq> y\<close>)+ 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

321 
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain 
62837  322 
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

323 
finally show "x' \<le> \<dots>" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

324 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

325 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

326 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

327 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

328 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

329 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

330 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

331 
lemma monotone2monotone: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

332 
assumes 2: "\<And>x. monotone ordb ordc (\<lambda>y. f x y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

333 
and t: "monotone orda ordb (\<lambda>x. t x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

334 
and 1: "\<And>y. monotone orda ordc (\<lambda>x. f x y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

335 
and trans: "transp ordc" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

336 
shows "monotone orda ordc (\<lambda>x. f x (t x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

337 
by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

338 

62837  339 
subsection \<open>Continuity\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

340 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

341 
definition cont :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

342 
where 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

343 
"cont luba orda lubb ordb f \<longleftrightarrow> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

344 
(\<forall>Y. Complete_Partial_Order.chain orda Y \<longrightarrow> Y \<noteq> {} \<longrightarrow> f (luba Y) = lubb (f ` Y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

345 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

346 
definition mcont :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

347 
where 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

348 
"mcont luba orda lubb ordb f \<longleftrightarrow> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

349 
monotone orda ordb f \<and> cont luba orda lubb ordb f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

350 

62837  351 
subsubsection \<open>Theorem collection \<open>cont_intro\<close>\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

352 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

353 
named_theorems cont_intro "continuity and admissibility intro rules" 
62837  354 
ML \<open> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

355 
(* apply cont_intro rules as intro and try to solve 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

356 
the remaining of the emerging subgoals with simp *) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

357 
fun cont_intro_tac ctxt = 
69593  358 
REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>cont_intro\<close>))) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

359 
THEN_ALL_NEW (SOLVED' (simp_tac ctxt)) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

360 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

361 
fun cont_intro_simproc ctxt ct = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

362 
let 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

363 
fun mk_stmt t = t 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

364 
> HOLogic.mk_Trueprop 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

365 
> Thm.cterm_of ctxt 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

366 
> Goal.init 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

367 
fun mk_thm t = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

368 
case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

369 
SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI}) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

370 
 NONE => NONE 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

371 
in 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

372 
case Thm.term_of ct of 
69593  373 
t as Const (\<^const_name>\<open>ccpo.admissible\<close>, _) $ _ $ _ $ _ => mk_thm t 
374 
 t as Const (\<^const_name>\<open>mcont\<close>, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t 

375 
 t as Const (\<^const_name>\<open>monotone\<close>, _) $ _ $ _ $ _ => mk_thm t 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

376 
 _ => NONE 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

377 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

378 
handle THM _ => NONE 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

379 
 TYPE _ => NONE 
62837  380 
\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

381 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

382 
simproc_setup "cont_intro" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

383 
( "ccpo.admissible lub ord P" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

384 
 "mcont lub ord lub' ord' f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

385 
 "monotone ord ord' f" 
62837  386 
) = \<open>K cont_intro_simproc\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

387 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

388 
lemmas [cont_intro] = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

389 
call_mono 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

390 
let_mono 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

391 
if_mono 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

392 
option.const_mono 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

393 
tailrec.const_mono 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

394 
bind_mono 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

395 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

396 
declare if_mono[simp] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

397 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

398 
lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

399 
by(simp add: monotone_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

400 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

401 
lemma monotone_applyI: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

402 
"monotone orda ordb F \<Longrightarrow> monotone (fun_ord orda) ordb (\<lambda>f. F (f x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

403 
by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

404 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

405 
lemma monotone_if_fun [partial_function_mono]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

406 
"\<lbrakk> monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

407 
\<Longrightarrow> monotone (fun_ord orda) (fun_ord ordb) (\<lambda>f n. if c n then F f n else G f n)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

408 
by(simp add: monotone_def fun_ord_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

409 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

410 
lemma monotone_fun_apply_fun [partial_function_mono]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

411 
"monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\<lambda>f n. f t (g n))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

412 
by(rule monotoneI)(simp add: fun_ord_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

413 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

414 
lemma monotone_fun_ord_apply: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

415 
"monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

416 
by(auto simp add: monotone_def fun_ord_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

417 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

418 
context preorder begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

419 

70961
70fb697be418
Removed dup lemma that inhibited locale instantiations (dup fact error)
Peter Lammich
parents:
69593
diff
changeset

420 
declare transp_le[cont_intro] 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

421 

67399  422 
lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

423 
by(rule monotoneI) simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

424 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

425 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

426 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

427 
lemma transp_le [cont_intro, simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

428 
"class.preorder ord (mk_less ord) \<Longrightarrow> transp ord" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

429 
by(rule preorder.transp_le) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

430 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

431 
context partial_function_definitions begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

432 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

433 
declare const_mono [cont_intro, simp] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

434 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

435 
lemma transp_le [cont_intro, simp]: "transp leq" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

436 
by(rule transpI)(rule leq_trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

437 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

438 
lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

439 
by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

440 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

441 
declare ccpo[cont_intro, simp] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

442 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

443 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

444 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

445 
lemma contI [intro?]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

446 
"(\<And>Y. \<lbrakk> Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> \<Longrightarrow> f (luba Y) = lubb (f ` Y)) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

447 
\<Longrightarrow> cont luba orda lubb ordb f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

448 
unfolding cont_def by blast 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

449 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

450 
lemma contD: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

451 
"\<lbrakk> cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

452 
\<Longrightarrow> f (luba Y) = lubb (f ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

453 
unfolding cont_def by blast 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

454 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

455 
lemma cont_id [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord id" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

456 
by(rule contI) simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

457 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

458 
lemma cont_id' [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord (\<lambda>x. x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

459 
using cont_id[unfolded id_def] . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

460 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

461 
lemma cont_applyI [cont_intro]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

462 
assumes cont: "cont luba orda lubb ordb g" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

463 
shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. g (f x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

464 
by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

465 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

466 
lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

467 
by(simp add: cont_def fun_lub_apply) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

468 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

469 
lemma cont_if [cont_intro]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

470 
"\<lbrakk> cont luba orda lubb ordb f; cont luba orda lubb ordb g \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

471 
\<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

472 
by(cases c) simp_all 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

473 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

474 
lemma mcontI [intro?]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

475 
"\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

476 
by(simp add: mcont_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

477 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

478 
lemma mcont_mono: "mcont luba orda lubb ordb f \<Longrightarrow> monotone orda ordb f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

479 
by(simp add: mcont_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

480 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

481 
lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \<Longrightarrow> cont luba orda lubb ordb f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

482 
by(simp add: mcont_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

483 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

484 
lemma mcont_monoD: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

485 
"\<lbrakk> mcont luba orda lubb ordb f; orda x y \<rbrakk> \<Longrightarrow> ordb (f x) (f y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

486 
by(auto simp add: mcont_def dest: monotoneD) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

487 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

488 
lemma mcont_contD: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

489 
"\<lbrakk> mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

490 
\<Longrightarrow> f (luba Y) = lubb (f ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

491 
by(auto simp add: mcont_def dest: contD) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

492 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

493 
lemma mcont_call [cont_intro, simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

494 
"mcont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

495 
by(simp add: mcont_def call_mono call_cont) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

496 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

497 
lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\<lambda>x. x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

498 
by(simp add: mcont_def monotone_id') 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

499 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

500 
lemma mcont_applyI: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

501 
"mcont luba orda lubb ordb (\<lambda>x. F x) \<Longrightarrow> mcont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. F (f x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

502 
by(simp add: mcont_def monotone_applyI cont_applyI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

503 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

504 
lemma mcont_if [cont_intro, simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

505 
"\<lbrakk> mcont luba orda lubb ordb (\<lambda>x. f x); mcont luba orda lubb ordb (\<lambda>x. g x) \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

506 
\<Longrightarrow> mcont luba orda lubb ordb (\<lambda>x. if c then f x else g x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

507 
by(simp add: mcont_def cont_if) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

508 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

509 
lemma cont_fun_lub_apply: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

510 
"cont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. cont luba orda lubb ordb (\<lambda>y. f y x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

511 
by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

512 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

513 
lemma mcont_fun_lub_apply: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

514 
"mcont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. mcont luba orda lubb ordb (\<lambda>y. f y x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

515 
by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

516 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

517 
context ccpo begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

518 

67399  519 
lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)" 
69546
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69164
diff
changeset

520 
by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

521 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

522 
lemma mcont_const [cont_intro, simp]: 
67399  523 
"mcont luba orda Sup (\<le>) (\<lambda>x. c)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

524 
by(simp add: mcont_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

525 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

526 
lemma cont_apply: 
67399  527 
assumes 2: "\<And>x. cont lubb ordb Sup (\<le>) (\<lambda>y. f x y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

528 
and t: "cont luba orda lubb ordb (\<lambda>x. t x)" 
67399  529 
and 1: "\<And>y. cont luba orda Sup (\<le>) (\<lambda>x. f x y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

530 
and mono: "monotone orda ordb (\<lambda>x. t x)" 
67399  531 
and mono2: "\<And>x. monotone ordb (\<le>) (\<lambda>y. f x y)" 
532 
and mono1: "\<And>y. monotone orda (\<le>) (\<lambda>x. f x y)" 

533 
shows "cont luba orda Sup (\<le>) (\<lambda>x. f x (t x))" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

534 
proof 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

535 
fix Y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

536 
assume chain: "Complete_Partial_Order.chain orda Y" and "Y \<noteq> {}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

537 
moreover from chain have chain': "Complete_Partial_Order.chain ordb (t ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

538 
by(rule chain_imageI)(rule monotoneD[OF mono]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

539 
ultimately show "f (luba Y) (t (luba Y)) = \<Squnion>((\<lambda>x. f x (t x)) ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

540 
by(simp add: contD[OF 1] contD[OF t] contD[OF 2] image_image) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

541 
(rule diag_Sup[OF chain], auto intro: monotone2monotone[OF mono2 mono monotone_const transpI] monotoneD[OF mono1]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

542 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

543 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

544 
lemma mcont2mcont': 
67399  545 
"\<lbrakk> \<And>x. mcont lub' ord' Sup (\<le>) (\<lambda>y. f x y); 
546 
\<And>y. mcont lub ord Sup (\<le>) (\<lambda>x. f x y); 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

547 
mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk> 
67399  548 
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x (t x))" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

549 
unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

550 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

551 
lemma mcont2mcont: 
67399  552 
"\<lbrakk>mcont lub' ord' Sup (\<le>) (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 
553 
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f (t x))" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

554 
by(rule mcont2mcont'[OF _ mcont_const]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

555 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

556 
context 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

557 
fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 
69039  558 
and lub :: "'b set \<Rightarrow> 'b" ("\<Or>") 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

559 
begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

560 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

561 
lemma cont_fun_lub_Sup: 
67399  562 
assumes chainM: "Complete_Partial_Order.chain (fun_ord (\<le>)) M" 
563 
and mcont [rule_format]: "\<forall>f\<in>M. mcont lub (\<sqsubseteq>) Sup (\<le>) f" 

564 
shows "cont lub (\<sqsubseteq>) Sup (\<le>) (fun_lub Sup M)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

565 
proof(rule contI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

566 
fix Y 
67399  567 
assume chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

568 
and Y: "Y \<noteq> {}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

569 
from swap_Sup[OF chain chainM mcont[THEN mcont_mono]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

570 
show "fun_lub Sup M (\<Or>Y) = \<Squnion>(fun_lub Sup M ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

571 
by(simp add: mcont_contD[OF mcont chain Y] fun_lub_apply cong: image_cong) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

572 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

573 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

574 
lemma mcont_fun_lub_Sup: 
67399  575 
"\<lbrakk> Complete_Partial_Order.chain (fun_ord (\<le>)) M; 
576 
\<forall>f\<in>M. mcont lub ord Sup (\<le>) f \<rbrakk> 

577 
\<Longrightarrow> mcont lub (\<sqsubseteq>) Sup (\<le>) (fun_lub Sup M)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

578 
by(simp add: mcont_def cont_fun_lub_Sup mono_lub) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

579 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

580 
lemma iterates_mcont: 
67399  581 
assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord (\<le>)) F" 
582 
and mono: "\<And>f. mcont lub (\<sqsubseteq>) Sup (\<le>) f \<Longrightarrow> mcont lub (\<sqsubseteq>) Sup (\<le>) (F f)" 

583 
shows "mcont lub (\<sqsubseteq>) Sup (\<le>) f" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

584 
using f 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

585 
by(induction rule: ccpo.iterates.induct[OF ccpo_fun, consumes 1, case_names step Sup])(blast intro: mono mcont_fun_lub_Sup)+ 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

586 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

587 
lemma fixp_preserves_mcont: 
67399  588 
assumes mono: "\<And>x. monotone (fun_ord (\<le>)) (\<le>) (\<lambda>f. F f x)" 
589 
and mcont: "\<And>f. mcont lub (\<sqsubseteq>) Sup (\<le>) f \<Longrightarrow> mcont lub (\<sqsubseteq>) Sup (\<le>) (F f)" 

590 
shows "mcont lub (\<sqsubseteq>) Sup (\<le>) (ccpo.fixp (fun_lub Sup) (fun_ord (\<le>)) F)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

591 
(is "mcont _ _ _ _ ?fixp") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

592 
unfolding mcont_def 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

593 
proof(intro conjI monotoneI contI) 
67399  594 
have mono: "monotone (fun_ord (\<le>)) (fun_ord (\<le>)) F" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

595 
by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono]) 
67399  596 
let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord (\<le>)) F" 
597 
have chain: "\<And>x. Complete_Partial_Order.chain (\<le>) ((\<lambda>f. f x) ` ?iter)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

598 
by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

599 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

600 
{ 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

601 
fix x y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

602 
assume "x \<sqsubseteq> y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

603 
show "?fixp x \<le> ?fixp y" 
63170  604 
apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply) 
605 
using chain 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

606 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

607 
fix x' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

608 
assume "x' \<in> (\<lambda>f. f x) ` ?iter" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

609 
then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2) 
62837  610 
also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" 
611 
by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]]) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

612 
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain 
62837  613 
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

614 
finally show "x' \<le> \<dots>" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

615 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

616 
next 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

617 
fix Y 
67399  618 
assume chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

619 
and Y: "Y \<noteq> {}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

620 
{ fix f 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

621 
assume "f \<in> ?iter" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

622 
hence "f (\<Or>Y) = \<Squnion>(f ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

623 
using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) } 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

624 
moreover have "\<Squnion>((\<lambda>f. \<Squnion>(f ` Y)) ` ?iter) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` ?iter)) ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

625 
using chain ccpo.chain_iterates[OF ccpo_fun mono] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

626 
by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

627 
ultimately show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

628 
by(simp add: fun_lub_apply cong: image_cong) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

629 
} 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

630 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

631 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

632 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

633 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

634 
context 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

635 
fixes F :: "'c \<Rightarrow> 'c" and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and f 
67399  636 
assumes mono: "\<And>x. monotone (fun_ord (\<le>)) (\<le>) (\<lambda>f. U (F (C f)) x)" 
637 
and eq: "f \<equiv> C (ccpo.fixp (fun_lub Sup) (fun_ord (\<le>)) (\<lambda>f. U (F (C f))))" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

638 
and inverse: "\<And>f. U (C f) = f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

639 
begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

640 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

641 
lemma fixp_preserves_mono_uc: 
67399  642 
assumes mono2: "\<And>f. monotone ord (\<le>) (U f) \<Longrightarrow> monotone ord (\<le>) (U (F f))" 
643 
shows "monotone ord (\<le>) (U f)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

644 
using fixp_preserves_mono[OF mono mono2] by(subst eq)(simp add: inverse) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

645 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

646 
lemma fixp_preserves_mcont_uc: 
67399  647 
assumes mcont: "\<And>f. mcont lubb ordb Sup (\<le>) (U f) \<Longrightarrow> mcont lubb ordb Sup (\<le>) (U (F f))" 
648 
shows "mcont lubb ordb Sup (\<le>) (U f)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

649 
using fixp_preserves_mcont[OF mono mcont] by(subst eq)(simp add: inverse) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

650 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

651 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

652 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

653 
lemmas fixp_preserves_mono1 = fixp_preserves_mono_uc[of "\<lambda>x. x" _ "\<lambda>x. x", OF _ _ refl] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

654 
lemmas fixp_preserves_mono2 = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

655 
fixp_preserves_mono_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

656 
lemmas fixp_preserves_mono3 = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

657 
fixp_preserves_mono_uc[of "\<lambda>f. case_prod (case_prod f)" _ "\<lambda>f. curry (curry f)", unfolded case_prod_curry curry_case_prod, OF _ _ refl] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

658 
lemmas fixp_preserves_mono4 = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

659 
fixp_preserves_mono_uc[of "\<lambda>f. case_prod (case_prod (case_prod f))" _ "\<lambda>f. curry (curry (curry f))", unfolded case_prod_curry curry_case_prod, OF _ _ refl] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

660 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

661 
lemmas fixp_preserves_mcont1 = fixp_preserves_mcont_uc[of "\<lambda>x. x" _ "\<lambda>x. x", OF _ _ refl] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

662 
lemmas fixp_preserves_mcont2 = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

663 
fixp_preserves_mcont_uc[of "case_prod" _ "curry", unfolded case_prod_curry curry_case_prod, OF _ _ refl] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

664 
lemmas fixp_preserves_mcont3 = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

665 
fixp_preserves_mcont_uc[of "\<lambda>f. case_prod (case_prod f)" _ "\<lambda>f. curry (curry f)", unfolded case_prod_curry curry_case_prod, OF _ _ refl] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

666 
lemmas fixp_preserves_mcont4 = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

667 
fixp_preserves_mcont_uc[of "\<lambda>f. case_prod (case_prod (case_prod f))" _ "\<lambda>f. curry (curry (curry f))", unfolded case_prod_curry curry_case_prod, OF _ _ refl] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

668 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

669 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

670 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

671 
lemma (in preorder) monotone_if_bot: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

672 
fixes bot 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

673 
assumes mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> (x \<le> bound) \<rbrakk> \<Longrightarrow> ord (f x) (f y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

674 
and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> ord bot (f x)" "ord bot bot" 
67399  675 
shows "monotone (\<le>) ord (\<lambda>x. if x \<le> bound then bot else f x)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

676 
by(rule monotoneI)(auto intro: bot intro: mono order_trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

677 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

678 
lemma (in ccpo) mcont_if_bot: 
69039  679 
fixes bot and lub ("\<Or>") and ord (infix "\<sqsubseteq>" 60) 
67399  680 
assumes ccpo: "class.ccpo lub (\<sqsubseteq>) lt" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

681 
and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" 
67399  682 
and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

683 
and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> bot \<sqsubseteq> f x" 
67399  684 
shows "mcont Sup (\<le>) lub (\<sqsubseteq>) (\<lambda>x. if x \<le> bound then bot else f x)" (is "mcont _ _ _ _ ?g") 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

685 
proof(intro mcontI contI) 
67399  686 
interpret c: ccpo lub "(\<sqsubseteq>)" lt by(fact ccpo) 
687 
show "monotone (\<le>) (\<sqsubseteq>) ?g" by(rule monotone_if_bot)(simp_all add: mono bot) 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

688 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

689 
fix Y 
67399  690 
assume chain: "Complete_Partial_Order.chain (\<le>) Y" and Y: "Y \<noteq> {}" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

691 
show "?g (\<Squnion>Y) = \<Or>(?g ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

692 
proof(cases "Y \<subseteq> {x. x \<le> bound}") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

693 
case True 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

694 
hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

695 
moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

696 
ultimately show ?thesis using True Y 
69546
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69164
diff
changeset

697 
by (auto simp add: image_constant_conv cong del: c.SUP_cong_simp) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

698 
next 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

699 
case False 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

700 
let ?Y = "Y \<inter> {x. \<not> x \<le> bound}" 
67399  701 
have chain': "Complete_Partial_Order.chain (\<le>) ?Y" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

702 
using chain by(rule chain_subset) simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

703 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

704 
from False obtain y where ybound: "\<not> y \<le> bound" and y: "y \<in> Y" by blast 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

705 
hence "\<not> \<Squnion>Y \<le> bound" by (metis ccpo_Sup_upper chain order.trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

706 
hence "?g (\<Squnion>Y) = f (\<Squnion>Y)" by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

707 
also have "\<Squnion>Y \<le> \<Squnion>?Y" using chain 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

708 
proof(rule ccpo_Sup_least) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

709 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

710 
assume x: "x \<in> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

711 
show "x \<le> \<Squnion>?Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

712 
proof(cases "x \<le> bound") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

713 
case True 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

714 
with chainD[OF chain x y] have "x \<le> y" using ybound by(auto intro: order_trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

715 
thus ?thesis by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

716 
qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

717 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

718 
hence "\<Squnion>Y = \<Squnion>?Y" by(rule antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

719 
hence "f (\<Squnion>Y) = f (\<Squnion>?Y)" by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

720 
also have "f (\<Squnion>?Y) = \<Or>(f ` ?Y)" using chain' by(rule cont)(insert y ybound, auto) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

721 
also have "\<Or>(f ` ?Y) = \<Or>(?g ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

722 
proof(cases "Y \<inter> {x. x \<le> bound} = {}") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

723 
case True 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

724 
hence "f ` ?Y = ?g ` Y" by auto 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

725 
thus ?thesis by(rule arg_cong) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

726 
next 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

727 
case False 
67399  728 
have chain'': "Complete_Partial_Order.chain (\<sqsubseteq>) (insert bot (f ` ?Y))" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

729 
using chain by(auto intro!: chainI bot dest: chainD intro: mono) 
67399  730 
hence chain''': "Complete_Partial_Order.chain (\<sqsubseteq>) (f ` ?Y)" by(rule chain_subset) blast 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

731 
have "bot \<sqsubseteq> \<Or>(f ` ?Y)" using y ybound by(blast intro: c.order_trans[OF bot] c.ccpo_Sup_upper[OF chain''']) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

732 
hence "\<Or>(insert bot (f ` ?Y)) \<sqsubseteq> \<Or>(f ` ?Y)" using chain'' 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

733 
by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain''']) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

734 
with _ have "\<dots> = \<Or>(insert bot (f ` ?Y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

735 
by(rule c.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain'']) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

736 
also have "insert bot (f ` ?Y) = ?g ` Y" using False by auto 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

737 
finally show ?thesis . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

738 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

739 
finally show ?thesis . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

740 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

741 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

742 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

743 
context partial_function_definitions begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

744 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

745 
lemma mcont_const [cont_intro, simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

746 
"mcont luba orda lub leq (\<lambda>x. c)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

747 
by(rule ccpo.mcont_const)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

748 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

749 
lemmas [cont_intro, simp] = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

750 
ccpo.cont_const[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

751 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

752 
lemma mono2mono: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

753 
assumes "monotone ordb leq (\<lambda>y. f y)" "monotone orda ordb (\<lambda>x. t x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

754 
shows "monotone orda leq (\<lambda>x. f (t x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

755 
using assms by(rule monotone2monotone) simp_all 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

756 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

757 
lemmas mcont2mcont' = ccpo.mcont2mcont'[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

758 
lemmas mcont2mcont = ccpo.mcont2mcont[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

759 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

760 
lemmas fixp_preserves_mono1 = ccpo.fixp_preserves_mono1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

761 
lemmas fixp_preserves_mono2 = ccpo.fixp_preserves_mono2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

762 
lemmas fixp_preserves_mono3 = ccpo.fixp_preserves_mono3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

763 
lemmas fixp_preserves_mono4 = ccpo.fixp_preserves_mono4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

764 
lemmas fixp_preserves_mcont1 = ccpo.fixp_preserves_mcont1[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

765 
lemmas fixp_preserves_mcont2 = ccpo.fixp_preserves_mcont2[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

766 
lemmas fixp_preserves_mcont3 = ccpo.fixp_preserves_mcont3[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

767 
lemmas fixp_preserves_mcont4 = ccpo.fixp_preserves_mcont4[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

768 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

769 
lemma monotone_if_bot: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

770 
fixes bot 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

771 
assumes g: "\<And>x. g x = (if leq x bound then bot else f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

772 
and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

773 
and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)" "ord bot bot" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

774 
shows "monotone leq ord g" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

775 
unfolding g[abs_def] using preorder mono bot by(rule preorder.monotone_if_bot) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

776 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

777 
lemma mcont_if_bot: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

778 
fixes bot 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

779 
assumes ccpo: "class.ccpo lub' ord (mk_less ord)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

780 
and bot: "\<And>x. \<not> leq x bound \<Longrightarrow> ord bot (f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

781 
and g: "\<And>x. g x = (if leq x bound then bot else f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

782 
and mono: "\<And>x y. \<lbrakk> leq x y; \<not> leq x bound \<rbrakk> \<Longrightarrow> ord (f x) (f y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

783 
and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain leq Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> leq x bound \<rbrakk> \<Longrightarrow> f (lub Y) = lub' (f ` Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

784 
shows "mcont lub leq lub' ord g" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

785 
unfolding g[abs_def] using ccpo mono cont bot by(rule ccpo.mcont_if_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

786 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

787 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

788 

62837  789 
subsection \<open>Admissibility\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

790 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

791 
lemma admissible_subst: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

792 
assumes adm: "ccpo.admissible luba orda (\<lambda>x. P x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

793 
and mcont: "mcont lubb ordb luba orda f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

794 
shows "ccpo.admissible lubb ordb (\<lambda>x. P (f x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

795 
apply(rule ccpo.admissibleI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

796 
apply(frule (1) mcont_contD[OF mcont]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

797 
apply(auto intro: ccpo.admissibleD[OF adm] chain_imageI dest: mcont_monoD[OF mcont]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

798 
done 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

799 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

800 
lemmas [simp, cont_intro] = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

801 
admissible_all 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

802 
admissible_ball 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

803 
admissible_const 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

804 
admissible_conj 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

805 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

806 
lemma admissible_disj' [simp, cont_intro]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

807 
"\<lbrakk> class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

808 
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

809 
by(rule ccpo.admissible_disj) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

810 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

811 
lemma admissible_imp' [cont_intro]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

812 
"\<lbrakk> class.ccpo lub ord (mk_less ord); 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

813 
ccpo.admissible lub ord (\<lambda>x. \<not> P x); 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

814 
ccpo.admissible lub ord (\<lambda>x. Q x) \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

815 
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

816 
unfolding imp_conv_disj by(rule ccpo.admissible_disj) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

817 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

818 
lemma admissible_imp [cont_intro]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

819 
"(Q \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x)) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

820 
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. Q \<longrightarrow> P x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

821 
by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

822 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

823 
lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]: 
67399  824 
shows admissible_not_mem: "ccpo.admissible Union (\<subseteq>) (\<lambda>A. x \<notin> A)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

825 
by(rule ccpo.admissibleI) auto 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

826 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

827 
lemma admissible_eqI: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

828 
assumes f: "cont luba orda lub ord (\<lambda>x. f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

829 
and g: "cont luba orda lub ord (\<lambda>x. g x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

830 
shows "ccpo.admissible luba orda (\<lambda>x. f x = g x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

831 
apply(rule ccpo.admissibleI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

832 
apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

833 
done 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

834 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

835 
corollary admissible_eq_mcontI [cont_intro]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

836 
"\<lbrakk> mcont luba orda lub ord (\<lambda>x. f x); 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

837 
mcont luba orda lub ord (\<lambda>x. g x) \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

838 
\<Longrightarrow> ccpo.admissible luba orda (\<lambda>x. f x = g x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

839 
by(rule admissible_eqI)(auto simp add: mcont_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

840 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

841 
lemma admissible_iff [cont_intro, simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

842 
"\<lbrakk> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x); ccpo.admissible lub ord (\<lambda>x. Q x \<longrightarrow> P x) \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

843 
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longleftrightarrow> Q x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

844 
by(subst iff_conv_conj_imp)(rule admissible_conj) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

845 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

846 
context ccpo begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

847 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

848 
lemma admissible_leI: 
67399  849 
assumes f: "mcont luba orda Sup (\<le>) (\<lambda>x. f x)" 
850 
and g: "mcont luba orda Sup (\<le>) (\<lambda>x. g x)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

851 
shows "ccpo.admissible luba orda (\<lambda>x. f x \<le> g x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

852 
proof(rule ccpo.admissibleI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

853 
fix A 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

854 
assume chain: "Complete_Partial_Order.chain orda A" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

855 
and le: "\<forall>x\<in>A. f x \<le> g x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

856 
and False: "A \<noteq> {}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

857 
have "f (luba A) = \<Squnion>(f ` A)" by(simp add: mcont_contD[OF f] chain False) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

858 
also have "\<dots> \<le> \<Squnion>(g ` A)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

859 
proof(rule ccpo_Sup_least) 
67399  860 
from chain show "Complete_Partial_Order.chain (\<le>) (f ` A)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

861 
by(rule chain_imageI)(rule mcont_monoD[OF f]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

862 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

863 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

864 
assume "x \<in> f ` A" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

865 
then obtain y where "y \<in> A" "x = f y" by blast note this(2) 
62837  866 
also have "f y \<le> g y" using le \<open>y \<in> A\<close> by simp 
67399  867 
also have "Complete_Partial_Order.chain (\<le>) (g ` A)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

868 
using chain by(rule chain_imageI)(rule mcont_monoD[OF g]) 
62837  869 
hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> A\<close>) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

870 
finally show "x \<le> \<dots>" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

871 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

872 
also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

873 
finally show "f (luba A) \<le> g (luba A)" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

874 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

875 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

876 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

877 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

878 
lemma admissible_leI: 
69039  879 
fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>") 
67399  880 
assumes "class.ccpo lub (\<sqsubseteq>) (mk_less (\<sqsubseteq>))" 
881 
and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. f x)" 

882 
and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. g x)" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

883 
shows "ccpo.admissible luba orda (\<lambda>x. f x \<sqsubseteq> g x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

884 
using assms by(rule ccpo.admissible_leI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

885 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

886 
declare ccpo_class.admissible_leI[cont_intro] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

887 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

888 
context ccpo begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

889 

67399  890 
lemma admissible_not_below: "ccpo.admissible Sup (\<le>) (\<lambda>x. \<not> (\<le>) x y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

891 
by(rule ccpo.admissibleI)(simp add: ccpo_Sup_below_iff) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

892 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

893 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

894 

67399  895 
lemma (in preorder) preorder [cont_intro, simp]: "class.preorder (\<le>) (mk_less (\<le>))" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

896 
by(unfold_locales)(auto simp add: mk_less_def intro: order_trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

897 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

898 
context partial_function_definitions begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

899 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

900 
lemmas [cont_intro, simp] = 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

901 
admissible_leI[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

902 
ccpo.admissible_not_below[THEN admissible_subst, OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

903 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

904 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

905 

66244
4c999b5d78e2
qualify Complete_Partial_Order2.compact
Andreas Lochbihler
parents:
65366
diff
changeset

906 
setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

907 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

908 
inductive compact :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

909 
for lub ord x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

910 
where compact: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

911 
"\<lbrakk> ccpo.admissible lub ord (\<lambda>y. \<not> ord x y); 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

912 
ccpo.admissible lub ord (\<lambda>y. x \<noteq> y) \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

913 
\<Longrightarrow> compact lub ord x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

914 

66244
4c999b5d78e2
qualify Complete_Partial_Order2.compact
Andreas Lochbihler
parents:
65366
diff
changeset

915 
setup \<open>Sign.map_naming Name_Space.parent_path\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

916 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

917 
context ccpo begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

918 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

919 
lemma compactI: 
67399  920 
assumes "ccpo.admissible Sup (\<le>) (\<lambda>y. \<not> x \<le> y)" 
921 
shows "ccpo.compact Sup (\<le>) x" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

922 
using assms 
66244
4c999b5d78e2
qualify Complete_Partial_Order2.compact
Andreas Lochbihler
parents:
65366
diff
changeset

923 
proof(rule ccpo.compact.intros) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

924 
have neq: "(\<lambda>y. x \<noteq> y) = (\<lambda>y. \<not> x \<le> y \<or> \<not> y \<le> x)" by(auto) 
67399  925 
show "ccpo.admissible Sup (\<le>) (\<lambda>y. x \<noteq> y)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

926 
by(subst neq)(rule admissible_disj admissible_not_below assms)+ 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

927 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

928 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

929 
lemma compact_bot: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

930 
assumes "x = Sup {}" 
67399  931 
shows "ccpo.compact Sup (\<le>) x" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

932 
proof(rule compactI) 
67399  933 
show "ccpo.admissible Sup (\<le>) (\<lambda>y. \<not> x \<le> y)" using assms 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

934 
by(auto intro!: ccpo.admissibleI intro: ccpo_Sup_least chain_empty) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

935 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

936 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

937 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

938 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

939 
lemma admissible_compact_neq' [THEN admissible_subst, cont_intro, simp]: 
66244
4c999b5d78e2
qualify Complete_Partial_Order2.compact
Andreas Lochbihler
parents:
65366
diff
changeset

940 
shows admissible_compact_neq: "ccpo.compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. k \<noteq> x)" 
4c999b5d78e2
qualify Complete_Partial_Order2.compact
Andreas Lochbihler
parents:
65366
diff
changeset

941 
by(simp add: ccpo.compact.simps) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

942 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

943 
lemma admissible_neq_compact' [THEN admissible_subst, cont_intro, simp]: 
66244
4c999b5d78e2
qualify Complete_Partial_Order2.compact
Andreas Lochbihler
parents:
65366
diff
changeset

944 
shows admissible_neq_compact: "ccpo.compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. x \<noteq> k)" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

945 
by(subst eq_commute)(rule admissible_compact_neq) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

946 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

947 
context partial_function_definitions begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

948 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

949 
lemmas [cont_intro, simp] = ccpo.compact_bot[OF Partial_Function.ccpo[OF partial_function_definitions_axioms]] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

950 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

951 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

952 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

953 
context ccpo begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

954 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

955 
lemma fixp_strong_induct: 
67399  956 
assumes [cont_intro]: "ccpo.admissible Sup (\<le>) P" 
957 
and mono: "monotone (\<le>) (\<le>) f" 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

958 
and bot: "P (\<Squnion>{})" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

959 
and step: "\<And>x. \<lbrakk> x \<le> ccpo_class.fixp f; P x \<rbrakk> \<Longrightarrow> P (f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

960 
shows "P (ccpo_class.fixp f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

961 
proof(rule fixp_induct[where P="\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x", THEN conjunct2]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

962 
note [cont_intro] = admissible_leI 
67399  963 
show "ccpo.admissible Sup (\<le>) (\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x)" by simp 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

964 
next 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

965 
show "\<Squnion>{} \<le> ccpo_class.fixp f \<and> P (\<Squnion>{})" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

966 
by(auto simp add: bot intro: ccpo_Sup_least chain_empty) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

967 
next 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

968 
fix x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

969 
assume "x \<le> ccpo_class.fixp f \<and> P x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

970 
thus "f x \<le> ccpo_class.fixp f \<and> P (f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

971 
by(subst fixp_unfold[OF mono])(auto dest: monotoneD[OF mono] intro: step) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

972 
qed(rule mono) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

973 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

974 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

975 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

976 
context partial_function_definitions begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

977 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

978 
lemma fixp_strong_induct_uc: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

979 
fixes F :: "'c \<Rightarrow> 'c" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

980 
and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

981 
and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

982 
and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

983 
assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

984 
and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

985 
and inverse: "\<And>f. U (C f) = f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

986 
and adm: "ccpo.admissible lub_fun le_fun P" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

987 
and bot: "P (\<lambda>_. lub {})" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

988 
and step: "\<And>f'. \<lbrakk> P (U f'); le_fun (U f') (U f) \<rbrakk> \<Longrightarrow> P (U (F f'))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

989 
shows "P (U f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

990 
unfolding eq inverse 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

991 
apply (rule ccpo.fixp_strong_induct[OF ccpo adm]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

992 
apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

993 
apply (rule_tac f'5="C x" in step) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

994 
apply (simp_all add: inverse eq) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

995 
done 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

996 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

997 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

998 

69593  999 
subsection \<open>\<^term>\<open>(=)\<close> as order\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1000 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1001 
definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1002 
where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1003 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1004 
definition the_Sup :: "'a set \<Rightarrow> 'a" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1005 
where "the_Sup A = (THE a. a \<in> A)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1006 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1007 
lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1008 
by(simp add: lub_singleton_def the_Sup_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1009 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1010 
lemma (in ccpo) lub_singleton: "lub_singleton Sup" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1011 
by(simp add: lub_singleton_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1012 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1013 
lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1014 
by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1015 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1016 
lemma preorder_eq [cont_intro, simp]: 
67399  1017 
"class.preorder (=) (mk_less (=))" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1018 
by(unfold_locales)(simp_all add: mk_less_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1019 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1020 
lemma monotone_eqI [cont_intro]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1021 
assumes "class.preorder ord (mk_less ord)" 
67399  1022 
shows "monotone (=) ord f" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1023 
proof  
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1024 
interpret preorder ord "mk_less ord" by fact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1025 
show ?thesis by(simp add: monotone_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1026 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1027 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1028 
lemma cont_eqI [cont_intro]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1029 
fixes f :: "'a \<Rightarrow> 'b" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1030 
assumes "lub_singleton lub" 
67399  1031 
shows "cont the_Sup (=) lub ord f" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1032 
proof(rule contI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1033 
fix Y :: "'a set" 
67399  1034 
assume "Complete_Partial_Order.chain (=) Y" "Y \<noteq> {}" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1035 
then obtain a where "Y = {a}" by(auto simp add: chain_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1036 
thus "f (the_Sup Y) = lub (f ` Y)" using assms 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1037 
by(simp add: the_Sup_def lub_singleton_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1038 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1039 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1040 
lemma mcont_eqI [cont_intro, simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1041 
"\<lbrakk> class.preorder ord (mk_less ord); lub_singleton lub \<rbrakk> 
67399  1042 
\<Longrightarrow> mcont the_Sup (=) lub ord f" 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1043 
by(simp add: mcont_def cont_eqI monotone_eqI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1044 

62837  1045 
subsection \<open>ccpo for products\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1046 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1047 
definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1048 
where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1049 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1050 
lemma lub_singleton_prod_lub [cont_intro, simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1051 
"\<lbrakk> lub_singleton luba; lub_singleton lubb \<rbrakk> \<Longrightarrow> lub_singleton (prod_lub luba lubb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1052 
by(simp add: lub_singleton_def prod_lub_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1053 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1054 
lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1055 
by(simp add: prod_lub_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1056 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1057 
lemma preorder_rel_prodI [cont_intro, simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1058 
assumes "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1059 
and "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1060 
shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1061 
proof  
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1062 
interpret a: preorder orda "mk_less orda" by fact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1063 
interpret b: preorder ordb "mk_less ordb" by fact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1064 
show ?thesis by(unfold_locales)(auto simp add: mk_less_def intro: a.order_trans b.order_trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1065 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1066 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1067 
lemma order_rel_prodI: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1068 
assumes a: "class.order orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1069 
and b: "class.order ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1070 
shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1071 
(is "class.order ?ord ?ord'") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1072 
proof(intro class.order.intro class.order_axioms.intro) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1073 
interpret a: order orda "mk_less orda" by(fact a) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1074 
interpret b: order ordb "mk_less ordb" by(fact b) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1075 
show "class.preorder ?ord ?ord'" by(rule preorder_rel_prodI) unfold_locales 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1076 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1077 
fix x y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1078 
assume "?ord x y" "?ord y x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1079 
thus "x = y" by(cases x y rule: prod.exhaust[case_product prod.exhaust]) auto 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1080 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1081 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1082 
lemma monotone_rel_prodI: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1083 
assumes mono2: "\<And>a. monotone ordb ordc (\<lambda>b. f (a, b))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1084 
and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1085 
and a: "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1086 
and b: "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1087 
and c: "class.preorder ordc (mk_less ordc)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1088 
shows "monotone (rel_prod orda ordb) ordc f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1089 
proof  
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1090 
interpret a: preorder orda "mk_less orda" by(rule a) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1091 
interpret b: preorder ordb "mk_less ordb" by(rule b) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1092 
interpret c: preorder ordc "mk_less ordc" by(rule c) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1093 
show ?thesis using mono2 mono1 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1094 
by(auto 7 2 simp add: monotone_def intro: c.order_trans) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1095 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1096 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1097 
lemma monotone_rel_prodD1: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1098 
assumes mono: "monotone (rel_prod orda ordb) ordc f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1099 
and preorder: "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1100 
shows "monotone orda ordc (\<lambda>a. f (a, b))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1101 
proof  
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1102 
interpret preorder ordb "mk_less ordb" by(rule preorder) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1103 
show ?thesis using mono by(simp add: monotone_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1104 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1105 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1106 
lemma monotone_rel_prodD2: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1107 
assumes mono: "monotone (rel_prod orda ordb) ordc f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1108 
and preorder: "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1109 
shows "monotone ordb ordc (\<lambda>b. f (a, b))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1110 
proof  
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1111 
interpret preorder orda "mk_less orda" by(rule preorder) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1112 
show ?thesis using mono by(simp add: monotone_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1113 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1114 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1115 
lemma monotone_case_prodI: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1116 
"\<lbrakk> \<And>a. monotone ordb ordc (f a); \<And>b. monotone orda ordc (\<lambda>a. f a b); 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1117 
class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb); 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1118 
class.preorder ordc (mk_less ordc) \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1119 
\<Longrightarrow> monotone (rel_prod orda ordb) ordc (case_prod f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1120 
by(rule monotone_rel_prodI) simp_all 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1121 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1122 
lemma monotone_case_prodD1: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1123 
assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1124 
and preorder: "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1125 
shows "monotone orda ordc (\<lambda>a. f a b)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1126 
using monotone_rel_prodD1[OF assms] by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1127 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1128 
lemma monotone_case_prodD2: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1129 
assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1130 
and preorder: "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1131 
shows "monotone ordb ordc (f a)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1132 
using monotone_rel_prodD2[OF assms] by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1133 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1134 
context 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1135 
fixes orda ordb ordc 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1136 
assumes a: "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1137 
and b: "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1138 
and c: "class.preorder ordc (mk_less ordc)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1139 
begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1140 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1141 
lemma monotone_rel_prod_iff: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1142 
"monotone (rel_prod orda ordb) ordc f \<longleftrightarrow> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1143 
(\<forall>a. monotone ordb ordc (\<lambda>b. f (a, b))) \<and> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1144 
(\<forall>b. monotone orda ordc (\<lambda>a. f (a, b)))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1145 
using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1146 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1147 
lemma monotone_case_prod_iff [simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1148 
"monotone (rel_prod orda ordb) ordc (case_prod f) \<longleftrightarrow> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1149 
(\<forall>a. monotone ordb ordc (f a)) \<and> (\<forall>b. monotone orda ordc (\<lambda>a. f a b))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1150 
by(simp add: monotone_rel_prod_iff) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1151 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1152 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1153 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1154 
lemma monotone_case_prod_apply_iff: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1155 
"monotone orda ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1156 
by(simp add: monotone_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1157 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1158 
lemma monotone_case_prod_applyD: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1159 
"monotone orda ordb (\<lambda>x. (case_prod f x) y) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1160 
\<Longrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1161 
by(simp add: monotone_case_prod_apply_iff) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1162 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1163 
lemma monotone_case_prod_applyI: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1164 
"monotone orda ordb (case_prod (\<lambda>a b. f a b y)) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1165 
\<Longrightarrow> monotone orda ordb (\<lambda>x. (case_prod f x) y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1166 
by(simp add: monotone_case_prod_apply_iff) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1167 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1168 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1169 
lemma cont_case_prod_apply_iff: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1170 
"cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1171 
by(simp add: cont_def split_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1172 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1173 
lemma cont_case_prod_applyI: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1174 
"cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y)) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1175 
\<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1176 
by(simp add: cont_case_prod_apply_iff) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1177 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1178 
lemma cont_case_prod_applyD: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1179 
"cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1180 
\<Longrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1181 
by(simp add: cont_case_prod_apply_iff) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1182 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1183 
lemma mcont_case_prod_apply_iff [simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1184 
"mcont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1185 
mcont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1186 
by(simp add: mcont_def monotone_case_prod_apply_iff cont_case_prod_apply_iff) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1187 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1188 
lemma cont_prodD1: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1189 
assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1190 
and "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1191 
and luba: "lub_singleton luba" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1192 
shows "cont lubb ordb lubc ordc (\<lambda>y. f (x, y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1193 
proof(rule contI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1194 
interpret preorder orda "mk_less orda" by fact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1195 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1196 
fix Y :: "'b set" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1197 
let ?Y = "{x} \<times> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1198 
assume "Complete_Partial_Order.chain ordb Y" "Y \<noteq> {}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1199 
hence "Complete_Partial_Order.chain (rel_prod orda ordb) ?Y" "?Y \<noteq> {}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1200 
by(simp_all add: chain_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1201 
with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1202 
moreover have "f ` ?Y = (\<lambda>y. f (x, y)) ` Y" by auto 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1203 
ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba 
62837  1204 
by(simp add: prod_lub_def \<open>Y \<noteq> {}\<close> lub_singleton_def) 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1205 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1206 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1207 
lemma cont_prodD2: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1208 
assumes cont: "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1209 
and "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1210 
and lubb: "lub_singleton lubb" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1211 
shows "cont luba orda lubc ordc (\<lambda>x. f (x, y))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1212 
proof(rule contI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1213 
interpret preorder ordb "mk_less ordb" by fact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1214 

7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1215 
fix Y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1216 
assume Y: "Complete_Partial_Order.chain orda Y" "Y \<noteq> {}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1217 
let ?Y = "Y \<times> {y}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1218 
have "f (luba Y, y) = f (prod_lub luba lubb ?Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1219 
using lubb by(simp add: prod_lub_def Y lub_singleton_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas&# 