author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63649  e690d6f2185b 
child 65366  10ca63a18e56 
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 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

9 
"~~/src/HOL/Library/Lattice_Syntax" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

11 

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

12 
lemma chain_transfer [transfer_rule]: 
63343  13 
includes lifting_syntax 
14 
shows "((A ===> A ===> op =) ===> rel_set A ===> op =) 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

15 
unfolding chain_def[abs_def] by transfer_prover 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

16 

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

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

18 
fixes Y :: "_ :: linorder set" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

19 
shows "Complete_Partial_Order.chain op \<le> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

21 

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

22 
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

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

24 

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

25 
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

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

27 

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

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

29 
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

30 
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

31 
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

32 

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

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

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

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

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

37 

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

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

39 
"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

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

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

42 

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

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

44 
"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

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

46 
by(auto 4 3 simp add: chain_def) 
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 

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

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

50 

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

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

52 
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

53 
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

54 

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

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

56 
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

57 

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

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

59 
assumes chain: "Complete_Partial_Order.chain op \<le> A" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

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

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

66 
proof (rule ccpo_Sup_least [OF chain]) 

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

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

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

70 
qed 

71 
qed 

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

72 

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

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

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

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

76 
and mono: "\<And>f. f \<in> Y \<Longrightarrow> monotone le_b op \<le> f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

77 
shows "monotone op \<sqsubseteq> op \<le> (fun_lub Sup Y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

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

81 

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

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

83 
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

84 
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

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

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

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

88 
then obtain f where "f \<in> Y" "x' = f x" by blast 
62837  89 
note \<open>x' = f x\<close> also 
90 
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

91 
also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain'' 
62837  92 
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

93 
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

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

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

96 

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

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

98 
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

99 
assumes chain: "Complete_Partial_Order.chain le_b Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

101 
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

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

103 

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

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

105 
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

106 
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

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

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

109 
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

110 

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

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

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

113 
then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2) 
62837  114 
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

115 
also have "\<dots> \<le> ?rhs" using chain'[OF y] 
62837  116 
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

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

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

119 

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

120 
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

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

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

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

124 
have chain2: "\<And>y'. y' \<in> Y \<Longrightarrow> Complete_Partial_Order.chain op \<le> (f y' ` Y)" using chain 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

127 
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

128 

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

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

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

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

132 
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

133 
then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2) 
62837  134 
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

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

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

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

138 
then obtain y where "y \<in> Y" and x: "x = f y' y" by blast 
63040  139 
define y'' where "y'' = (if y \<sqsubseteq> y' then y' else y)" 
62837  140 
from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD) 
141 
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

142 
by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1]) 
62837  143 
also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def) 
144 
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

145 
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

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

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

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

149 

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

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

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

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

153 
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

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

157 
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

158 
finally show "y \<le> ?lhs" . 
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 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

161 

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

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

163 

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

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

165 
fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>_" [900] 900) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

166 
assumes ccpo: "class.ccpo Sup_b op \<sqsubseteq> lt_b" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

167 
assumes chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

168 
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

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

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

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

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

173 

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

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

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

176 
then obtain y where "y \<in> Y" and "x = f y" by blast note this(2) 
62837  177 
also have "y \<sqsubseteq> \<Or>Y" using ccpo chain \<open>y \<in> Y\<close> by(rule ccpo.ccpo_Sup_upper) 
178 
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

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

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

181 

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

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

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

184 
assumes Y: "Complete_Partial_Order.chain op \<sqsubseteq> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

185 
and Z: "Complete_Partial_Order.chain (fun_ord op \<le>) Z" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

186 
and mono: "\<And>f. f \<in> Z \<Longrightarrow> monotone op \<sqsubseteq> op \<le> f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

187 
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

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

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

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

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

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

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

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

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

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

197 
have chain2: "Complete_Partial_Order.chain op \<le> ((\<lambda>x. \<Squnion>(x ` Y)) ` Z)" using Z 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

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

201 
and "fun_ord op \<le> f g" 
62837  202 
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

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

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

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

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

209 
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

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

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

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

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

214 
using Z 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

215 
have chain4: "Complete_Partial_Order.chain op \<le> ((\<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

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

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

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

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

220 
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

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

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

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

224 
then obtain f where "f \<in> Z" "x' = f x" by blast note this(2) 
62837  225 
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

226 
also have "f y \<le> ?rhs" using chain3 
62837  227 
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

228 
finally show "x' \<le> ?rhs" . 
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 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

231 

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

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

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

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

235 
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

236 
then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2) 
62837  237 
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

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

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

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

241 
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

242 
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3 
62837  243 
by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>) 
244 
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

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

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

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

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

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

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

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

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

253 
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

254 
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

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

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

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

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

259 
then obtain f where "f \<in> Z" "x' = f y" by blast note this(2) 
62837  260 
also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>] 
261 
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

262 
also have "\<dots> \<le> ?lhs" using chain2 
62837  263 
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

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

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

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

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

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

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

270 

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

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

272 
assumes fg: "fun_ord op \<le> f g" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

273 
and f: "monotone op \<le> op \<le> f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

274 
and g: "monotone op \<le> op \<le> g" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

275 
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

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

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

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

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

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

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

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

283 
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

284 
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

285 
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

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

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

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

289 

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

290 
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

291 

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

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

293 
assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

294 
and mono: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

295 
shows "monotone op \<sqsubseteq> op \<le> f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

297 
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

298 

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

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

300 
assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

301 
and mono2: "\<And>f. monotone op \<sqsubseteq> op \<le> f \<Longrightarrow> monotone op \<sqsubseteq> op \<le> (F f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

302 
shows "monotone op \<sqsubseteq> op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

305 
have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

306 
by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

307 
let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

308 
have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` ?iter)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

309 
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

310 

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

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

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

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

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

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

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

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

319 
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

320 
also have "f x \<le> f y" 
62837  321 
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

322 
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain 
62837  323 
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

324 
finally show "x' \<le> \<dots>" . 
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 
qed 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

327 

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

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

329 

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

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

331 

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

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

333 
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

334 
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

335 
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

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

337 
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

338 
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

339 

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

341 

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

342 
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

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

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

345 
(\<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

346 

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

347 
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

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

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

350 
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

351 

62837  352 
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

353 

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

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

356 
(* 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

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

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

359 
REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems cont_intro}))) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

361 

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

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

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

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

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

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

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

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

369 
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

370 
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

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

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

373 
case Thm.term_of ct of 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

374 
t as Const (@{const_name ccpo.admissible}, _) $ _ $ _ $ _ => mk_thm t 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

375 
 t as Const (@{const_name mcont}, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

376 
 t as Const (@{const_name monotone}, _) $ _ $ _ $ _ => mk_thm t 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

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

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

382 

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

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

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

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

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

388 

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

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

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

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

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

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

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

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

396 

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

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

398 

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

399 
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

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

401 

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

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

403 
"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

404 
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

405 

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

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

407 
"\<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

408 
\<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

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

410 

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

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

412 
"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

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

414 

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

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

416 
"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

417 
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

418 

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

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

420 

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

421 
lemma transp_le [simp, cont_intro]: "transp op \<le>" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

423 

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

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

425 
by(rule monotoneI) simp 
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 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

428 

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

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

430 
"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

431 
by(rule preorder.transp_le) 
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 
context partial_function_definitions begin 
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 
declare const_mono [cont_intro, simp] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

436 

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

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

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

439 

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

440 
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

441 
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

442 

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

443 
declare ccpo[cont_intro, simp] 
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 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

446 

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

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

448 
"(\<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

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

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

451 

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

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

453 
"\<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

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

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

456 

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

457 
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

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

459 

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

460 
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

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

462 

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

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

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

465 
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

466 
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

467 

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

468 
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

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

470 

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

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

472 
"\<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

473 
\<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

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

475 

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

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

477 
"\<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

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

479 

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

480 
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

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

482 

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

483 
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

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

485 

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

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

487 
"\<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

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

489 

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

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

491 
"\<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

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

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

494 

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

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

496 
"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

497 
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

498 

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

499 
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

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

501 

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

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

503 
"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

504 
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

505 

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

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

507 
"\<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

508 
\<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

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

510 

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

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

512 
"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

513 
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

514 

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

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

516 
"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

517 
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

518 

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

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

520 

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

521 
lemma cont_const [simp, cont_intro]: "cont luba orda Sup op \<le> (\<lambda>x. c)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

523 

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

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

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

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

527 

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

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

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

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

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

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

533 
and mono2: "\<And>x. monotone ordb op \<le> (\<lambda>y. f x y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

535 
shows "cont luba orda Sup op \<le> (\<lambda>x. f x (t x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

538 
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

539 
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

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

541 
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

542 
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

543 
(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

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

545 

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

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

547 
"\<lbrakk> \<And>x. mcont lub' ord' Sup op \<le> (\<lambda>y. f x y); 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

548 
\<And>y. mcont lub ord Sup op \<le> (\<lambda>x. f x y); 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

549 
mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

550 
\<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f x (t x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

551 
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

552 

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

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

554 
"\<lbrakk>mcont lub' ord' Sup op \<le> (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

555 
\<Longrightarrow> mcont lub ord Sup op \<le> (\<lambda>x. f (t x))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

557 

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

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

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

560 
and lub :: "'b set \<Rightarrow> 'b" ("\<Or>_" [900] 900) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

562 

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

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

564 
assumes chainM: "Complete_Partial_Order.chain (fun_ord op \<le>) M" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

565 
and mcont [rule_format]: "\<forall>f\<in>M. mcont lub op \<sqsubseteq> Sup op \<le> f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

566 
shows "cont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

569 
assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

571 
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

572 
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

573 
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

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

575 

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

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

577 
"\<lbrakk> Complete_Partial_Order.chain (fun_ord op \<le>) M; 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

578 
\<forall>f\<in>M. mcont lub ord Sup op \<le> f \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

579 
\<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (fun_lub Sup M)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

580 
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

581 

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

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

583 
assumes f: "f \<in> ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

584 
and mono: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

585 
shows "mcont lub op \<sqsubseteq> Sup op \<le> f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

587 
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

588 

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

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

590 
assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. F f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

591 
and mcont: "\<And>f. mcont lub op \<sqsubseteq> Sup op \<le> f \<Longrightarrow> mcont lub op \<sqsubseteq> Sup op \<le> (F f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

592 
shows "mcont lub op \<sqsubseteq> Sup op \<le> (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) F)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

595 
proof(intro conjI monotoneI contI) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

596 
have mono: "monotone (fun_ord op \<le>) (fun_ord op \<le>) F" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

597 
by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono]) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

598 
let ?iter = "ccpo.iterates (fun_lub Sup) (fun_ord op \<le>) F" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

599 
have chain: "\<And>x. Complete_Partial_Order.chain op \<le> ((\<lambda>f. f x) ` ?iter)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

600 
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

601 

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

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

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

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

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

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

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

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

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

611 
then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2) 
62837  612 
also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" 
613 
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

614 
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain 
62837  615 
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

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

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

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

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

620 
assume chain: "Complete_Partial_Order.chain op \<sqsubseteq> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

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

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

625 
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

626 
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

627 
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

628 
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

629 
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

630 
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

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

632 
qed 
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 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

635 

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

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

637 
fixes F :: "'c \<Rightarrow> 'c" and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and f 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

638 
assumes mono: "\<And>x. monotone (fun_ord op \<le>) op \<le> (\<lambda>f. U (F (C f)) x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

639 
and eq: "f \<equiv> C (ccpo.fixp (fun_lub Sup) (fun_ord op \<le>) (\<lambda>f. U (F (C f))))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

642 

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

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

644 
assumes mono2: "\<And>f. monotone ord op \<le> (U f) \<Longrightarrow> monotone ord op \<le> (U (F f))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

645 
shows "monotone ord op \<le> (U f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

646 
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

647 

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

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

649 
assumes mcont: "\<And>f. mcont lubb ordb Sup op \<le> (U f) \<Longrightarrow> mcont lubb ordb Sup op \<le> (U (F f))" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

650 
shows "mcont lubb ordb Sup op \<le> (U f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

651 
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

652 

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

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

654 

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

655 
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

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

657 
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

658 
lemmas fixp_preserves_mono3 = 
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 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

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

661 
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

662 

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

663 
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

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

665 
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

666 
lemmas fixp_preserves_mcont3 = 
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 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

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

669 
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

670 

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

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

672 

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

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

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

675 
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

676 
and bot: "\<And>x. \<not> x \<le> 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

677 
shows "monotone op \<le> ord (\<lambda>x. if x \<le> bound then bot else f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

678 
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

679 

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

680 
lemma (in ccpo) mcont_if_bot: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

681 
fixes bot and lub ("\<Or>_" [900] 900) and ord (infix "\<sqsubseteq>" 60) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

682 
assumes ccpo: "class.ccpo lub op \<sqsubseteq> lt" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

685 
and bot: "\<And>x. \<not> x \<le> bound \<Longrightarrow> bot \<sqsubseteq> f x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

688 
interpret c: ccpo lub "op \<sqsubseteq>" lt by(fact ccpo) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

689 
show "monotone op \<le> op \<sqsubseteq> ?g" by(rule monotone_if_bot)(simp_all add: mono bot) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

690 

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

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

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

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

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

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

696 
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

697 
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

698 
ultimately show ?thesis using True Y 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

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

702 
let ?Y = "Y \<inter> {x. \<not> x \<le> bound}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

703 
have chain': "Complete_Partial_Order.chain op \<le> ?Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

705 

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

706 
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

707 
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

708 
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

709 
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

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

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

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

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

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

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

716 
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

717 
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

718 
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

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

720 
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

721 
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

722 
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

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

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

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

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

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

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

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

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

731 
using chain by(auto intro!: chainI bot dest: chainD intro: mono) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

732 
hence chain''': "Complete_Partial_Order.chain op \<sqsubseteq> (f ` ?Y)" by(rule chain_subset) blast 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

733 
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

734 
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

735 
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

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

737 
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

738 
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

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 
finally show ?thesis . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

743 
qed 
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 
context partial_function_definitions begin 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

746 

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

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

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

749 
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

750 

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

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

752 
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

753 

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

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

755 
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

756 
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

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

758 

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

759 
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

760 
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

761 

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

762 
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

763 
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

764 
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

765 
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

766 
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

767 
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

768 
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

769 
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

770 

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

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

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

773 
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

774 
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

775 
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

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

777 
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

778 

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

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

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

781 
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

782 
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

783 
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

784 
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

785 
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

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

787 
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

788 

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

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

790 

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

792 

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

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

794 
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

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

796 
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

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

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

799 
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

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

801 

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

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

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

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

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

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

807 

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

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

809 
"\<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

810 
\<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

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

812 

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

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

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

815 
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

816 
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

817 
\<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

818 
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

819 

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

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

821 
"(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

822 
\<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

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

824 

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

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

826 
shows admissible_not_mem: "ccpo.admissible Union op \<subseteq> (\<lambda>A. x \<notin> A)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

828 

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

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

830 
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

831 
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

832 
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

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

834 
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

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

836 

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

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

838 
"\<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

839 
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

840 
\<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

841 
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

842 

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

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

844 
"\<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

845 
\<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

846 
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

847 

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

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

849 

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

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

851 
assumes f: "mcont luba orda Sup op \<le> (\<lambda>x. f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

852 
and g: "mcont luba orda Sup op \<le> (\<lambda>x. g x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

853 
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

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

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

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

857 
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

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

859 
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

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

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

862 
from chain show "Complete_Partial_Order.chain op \<le> (f ` A)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

863 
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

864 

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

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

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

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

869 
also have "Complete_Partial_Order.chain op \<le> (g ` A)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

870 
using chain by(rule chain_imageI)(rule mcont_monoD[OF g]) 
62837  871 
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

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

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

874 
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

875 
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

876 
qed 
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 
end 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

879 

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

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

881 
fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>_" [900] 900) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

882 
assumes "class.ccpo lub op \<sqsubseteq> (mk_less op \<sqsubseteq>)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

883 
and "mcont luba orda lub op \<sqsubseteq> (\<lambda>x. f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

885 
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

886 
using assms by(rule ccpo.admissible_leI) 
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 
declare ccpo_class.admissible_leI[cont_intro] 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

889 

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

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

891 

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

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

893 
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

894 

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

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

896 

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

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

898 
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

899 

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

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

901 

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

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

903 
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

904 
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

905 

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

906 
end 
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 

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

909 
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

910 
for lub ord x 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

912 
"\<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

913 
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

914 
\<Longrightarrow> compact lub ord x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

915 

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

916 
hide_fact (open) compact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

917 

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

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

919 

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

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

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

922 
shows "compact Sup op \<le> x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

924 
proof(rule compact.intros) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

925 
have neq: "(\<lambda>y. x \<noteq> y) = (\<lambda>y. \<not> x \<le> y \<or> \<not> y \<le> x)" by(auto) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

926 
show "ccpo.admissible Sup op \<le> (\<lambda>y. x \<noteq> y)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

927 
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

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

929 

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

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

931 
assumes "x = Sup {}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

932 
shows "compact Sup op \<le> x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

934 
show "ccpo.admissible Sup op \<le> (\<lambda>y. \<not> x \<le> y)" using assms 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

935 
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

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

937 

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

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

939 

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

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

941 
shows admissible_compact_neq: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. k \<noteq> x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

942 
by(simp add: compact.simps) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

943 

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

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

945 
shows admissible_neq_compact: "compact lub ord k \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. x \<noteq> k)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

946 
by(subst eq_commute)(rule admissible_compact_neq) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

947 

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

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

949 

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

950 
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

951 

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

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

953 

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

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

955 

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

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

957 
assumes [cont_intro]: "ccpo.admissible Sup op \<le> P" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

958 
and mono: "monotone op \<le> op \<le> f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

959 
and bot: "P (\<Squnion>{})" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

960 
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

961 
shows "P (ccpo_class.fixp f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

962 
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

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

964 
show "ccpo.admissible Sup op \<le> (\<lambda>x. x \<le> ccpo_class.fixp f \<and> P x)" by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

966 
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

967 
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

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

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

970 
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

971 
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

972 
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

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

974 

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

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

976 

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

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

978 

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

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

980 
fixes F :: "'c \<Rightarrow> 'c" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

981 
and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

982 
and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

984 
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

985 
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

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

987 
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

988 
and bot: "P (\<lambda>_. lub {})" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

989 
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

990 
shows "P (U f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

992 
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

993 
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

994 
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

995 
apply (simp_all add: inverse eq) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

997 

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

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

999 

62837  1000 
subsection \<open>@{term "op ="} as order\<close> 
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1001 

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

1002 
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

1003 
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

1004 

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

1005 
definition the_Sup :: "'a set \<Rightarrow> 'a" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1006 
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

1007 

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

1008 
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

1009 
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

1010 

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

1011 
lemma (in ccpo) lub_singleton: "lub_singleton Sup" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

1013 

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

1014 
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

1015 
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

1016 

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

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

1018 
"class.preorder op = (mk_less op =)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1019 
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

1020 

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

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

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

1023 
shows "monotone op = ord f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

1025 
interpret preorder ord "mk_less ord" by fact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

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

1028 

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

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

1030 
fixes f :: "'a \<Rightarrow> 'b" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1031 
assumes "lub_singleton lub" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1032 
shows "cont the_Sup op = lub ord f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

1034 
fix Y :: "'a set" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

1036 
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

1037 
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

1038 
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

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

1040 

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

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

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

1043 
\<Longrightarrow> mcont the_Sup op = lub ord f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1044 
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

1045 

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

1047 

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

1048 
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

1049 
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

1050 

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

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

1052 
"\<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

1053 
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

1054 

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

1055 
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

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

1057 

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

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

1059 
assumes "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1060 
and "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1061 
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

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

1063 
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

1064 
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

1065 
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

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

1067 

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

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

1069 
assumes a: "class.order orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1070 
and b: "class.order ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1071 
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

1072 
(is "class.order ?ord ?ord'") 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1073 
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

1074 
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

1075 
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

1076 
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

1077 

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

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

1079 
assume "?ord x y" "?ord y x" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1080 
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

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

1082 

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

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

1084 
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

1085 
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

1086 
and a: "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1087 
and b: "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1088 
and c: "class.preorder ordc (mk_less ordc)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1089 
shows "monotone (rel_prod orda ordb) ordc f" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

1091 
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

1092 
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

1093 
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

1094 
show ?thesis using mono2 mono1 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1095 
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

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

1097 

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

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

1099 
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

1100 
and preorder: "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1101 
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

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

1103 
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

1104 
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

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

1106 

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

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

1108 
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

1109 
and preorder: "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1110 
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

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

1112 
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

1113 
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

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

1115 

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

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

1117 
"\<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

1118 
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

1119 
class.preorder ordc (mk_less ordc) \<rbrakk> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1120 
\<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

1121 
by(rule monotone_rel_prodI) simp_all 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1122 

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

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

1124 
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

1125 
and preorder: "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1126 
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

1127 
using monotone_rel_prodD1[OF assms] by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1128 

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

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

1130 
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

1131 
and preorder: "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1132 
shows "monotone ordb ordc (f a)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1133 
using monotone_rel_prodD2[OF assms] by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1134 

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

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

1136 
fixes orda ordb ordc 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1137 
assumes a: "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1138 
and b: "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1139 
and c: "class.preorder ordc (mk_less ordc)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

1141 

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

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

1143 
"monotone (rel_prod orda ordb) ordc f \<longleftrightarrow> 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1144 
(\<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

1145 
(\<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

1146 
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

1147 

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

1148 
lemma monotone_case_prod_iff [simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1149 
"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

1150 
(\<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

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

1152 

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

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

1154 

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

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

1156 
"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

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

1158 

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

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

1160 
"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

1161 
\<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

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

1163 

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

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

1165 
"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

1166 
\<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

1167 
by(simp add: monotone_case_prod_apply_iff) 
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 

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

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

1171 
"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

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

1173 

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

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

1175 
"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

1176 
\<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

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

1178 

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

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

1180 
"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

1181 
\<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

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

1183 

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

1184 
lemma mcont_case_prod_apply_iff [simp]: 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1185 
"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

1186 
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

1187 
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

1188 

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

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

1190 
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

1191 
and "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1192 
and luba: "lub_singleton luba" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1193 
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

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

1195 
interpret preorder orda "mk_less orda" by fact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1196 

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

1197 
fix Y :: "'b set" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1198 
let ?Y = "{x} \<times> Y" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1199 
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

1200 
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

1201 
by(simp_all add: chain_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1202 
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

1203 
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

1204 
ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba 
62837  1205 
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

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

1207 

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

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

1209 
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

1210 
and "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1211 
and lubb: "lub_singleton lubb" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1212 
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

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

1214 
interpret preorder ordb "mk_less ordb" by fact 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1215 

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

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

1217 
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

1218 
let ?Y = "Y \<times> {y}" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1219 
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

1220 
using lubb by(simp add: prod_lub_def Y lub_singleton_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1221 
also from Y have "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

1222 
by(simp_all add: chain_def) 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1223 
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

1224 
also have "f ` ?Y = (\<lambda>x. f (x, y)) ` Y" by auto 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1225 
finally show "f (luba Y, y) = lubc \<dots>" . 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

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

1227 

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

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

1229 
assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1230 
and "class.preorder orda (mk_less orda)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1231 
and "lub_singleton luba" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1232 
shows "cont lubb ordb lubc ordc (f x)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1233 
using cont_prodD1[OF assms] by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1234 

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

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

1236 
assumes "cont (prod_lub luba lubb) (rel_prod orda ordb) lubc ordc (case_prod f)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1237 
and "class.preorder ordb (mk_less ordb)" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1238 
and "lub_singleton lubb" 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1239 
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

1240 
using cont_prodD2[OF assms] by simp 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
diff
changeset

1241 

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

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

1243 

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

1244 
lemma cont_prodI: 