equal
deleted
inserted
replaced
71 done |
71 done |
72 |
72 |
73 text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *} |
73 text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *} |
74 |
74 |
75 lemma lub_mono: |
75 lemma lub_mono: |
76 "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<forall>k. X k \<sqsubseteq> Y k\<rbrakk> |
76 "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> |
77 \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" |
77 \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)" |
78 apply (erule is_lub_thelub) |
78 apply (erule is_lub_thelub) |
79 apply (rule ub_rangeI) |
79 apply (rule ub_rangeI) |
80 apply (rule trans_less) |
80 apply (rule trans_less) |
81 apply (erule spec) |
81 apply (erule meta_spec) |
82 apply (erule is_ub_thelub) |
82 apply (erule is_ub_thelub) |
83 done |
83 done |
84 |
84 |
85 text {* the = relation between two chains is preserved by their lubs *} |
85 text {* the = relation between two chains is preserved by their lubs *} |
86 |
86 |
121 fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" |
121 fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" |
122 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
122 assumes 1: "\<And>j. chain (\<lambda>i. Y i j)" |
123 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
123 assumes 2: "\<And>i. chain (\<lambda>j. Y i j)" |
124 shows "chain (\<lambda>i. \<Squnion>j. Y i j)" |
124 shows "chain (\<lambda>i. \<Squnion>j. Y i j)" |
125 apply (rule chainI) |
125 apply (rule chainI) |
126 apply (rule lub_mono [rule_format, OF 2 2]) |
126 apply (rule lub_mono [OF 2 2]) |
127 apply (rule chainE [OF 1]) |
127 apply (rule chainE [OF 1]) |
128 done |
128 done |
129 |
129 |
130 lemma diag_lub: |
130 lemma diag_lub: |
131 fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" |
131 fixes Y :: "nat \<Rightarrow> nat \<Rightarrow> 'a::cpo" |
149 apply (rule trans_less) |
149 apply (rule trans_less) |
150 apply (rule chain_mono [OF 1 le_maxI1]) |
150 apply (rule chain_mono [OF 1 le_maxI1]) |
151 apply (rule chain_mono [OF 2 le_maxI2]) |
151 apply (rule chain_mono [OF 2 le_maxI2]) |
152 done |
152 done |
153 show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" |
153 show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)" |
154 apply (rule lub_mono [rule_format, OF 3 4]) |
154 apply (rule lub_mono [OF 3 4]) |
155 apply (rule is_ub_thelub [OF 2]) |
155 apply (rule is_ub_thelub [OF 2]) |
156 done |
156 done |
157 qed |
157 qed |
158 |
158 |
159 lemma ex_lub: |
159 lemma ex_lub: |