equal
deleted
inserted
replaced
134 assumes take_take: "take n (take n a) = take n a" |
134 assumes take_take: "take n (take n a) = take n a" |
135 assumes take_mono: "a \<preceq> b \<Longrightarrow> take n a \<preceq> take n b" |
135 assumes take_mono: "a \<preceq> b \<Longrightarrow> take n a \<preceq> take n b" |
136 assumes take_chain: "take n a \<preceq> take (Suc n) a" |
136 assumes take_chain: "take n a \<preceq> take (Suc n) a" |
137 assumes finite_range_take: "finite (range (take n))" |
137 assumes finite_range_take: "finite (range (take n))" |
138 assumes take_covers: "\<exists>n. take n a = a" |
138 assumes take_covers: "\<exists>n. take n a = a" |
|
139 begin |
|
140 |
|
141 lemma take_chain_less: "m < n \<Longrightarrow> take m a \<preceq> take n a" |
|
142 by (erule less_Suc_induct, rule take_chain, erule (1) r_trans) |
|
143 |
|
144 lemma take_chain_le: "m \<le> n \<Longrightarrow> take m a \<preceq> take n a" |
|
145 by (cases "m = n", simp add: r_refl, simp add: take_chain_less) |
|
146 |
|
147 end |
139 |
148 |
140 locale ideal_completion = basis_take + |
149 locale ideal_completion = basis_take + |
141 fixes principal :: "'a::type \<Rightarrow> 'b::cpo" |
150 fixes principal :: "'a::type \<Rightarrow> 'b::cpo" |
142 fixes rep :: "'b::cpo \<Rightarrow> 'a::type set" |
151 fixes rep :: "'b::cpo \<Rightarrow> 'a::type set" |
143 assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)" |
152 assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)" |