157 done |
157 done |
158 |
158 |
159 lemma ubasis_until_mono: |
159 lemma ubasis_until_mono: |
160 assumes "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> P b" |
160 assumes "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> P b" |
161 shows "ubasis_le a b \<Longrightarrow> ubasis_le (ubasis_until P a) (ubasis_until P b)" |
161 shows "ubasis_le a b \<Longrightarrow> ubasis_le (ubasis_until P a) (ubasis_until P b)" |
162 apply (induct set: ubasis_le) |
162 proof (induct set: ubasis_le) |
163 apply (rule ubasis_le_refl) |
163 case (ubasis_le_refl a) show ?case by (rule ubasis_le.ubasis_le_refl) |
164 apply (erule (1) ubasis_le_trans) |
164 next |
165 apply (simp add: ubasis_le_refl) |
165 case (ubasis_le_trans a b c) thus ?case by - (rule ubasis_le.ubasis_le_trans) |
166 apply (rule impI) |
166 next |
167 apply (rule ubasis_le_trans) |
167 case (ubasis_le_lower S a i) thus ?case |
168 apply (rule ubasis_until_less) |
168 apply (clarsimp simp add: ubasis_le_refl) |
169 apply (erule ubasis_le_lower) |
169 apply (rule ubasis_le_trans [OF ubasis_until_less]) |
170 apply simp |
170 apply (erule ubasis_le.ubasis_le_lower) |
171 apply (rule impI) |
171 done |
172 apply (subst ubasis_until_same) |
172 next |
173 apply (erule (3) prems) |
173 case (ubasis_le_upper S b a i) thus ?case |
174 apply (erule (2) ubasis_le_upper) |
174 apply clarsimp |
175 done |
175 apply (subst ubasis_until_same) |
|
176 apply (erule (3) prems) |
|
177 apply (erule (2) ubasis_le.ubasis_le_upper) |
|
178 done |
|
179 qed |
176 |
180 |
177 lemma finite_range_ubasis_until: |
181 lemma finite_range_ubasis_until: |
178 "finite {x. P x} \<Longrightarrow> finite (range (ubasis_until P))" |
182 "finite {x. P x} \<Longrightarrow> finite (range (ubasis_until P))" |
179 apply (rule finite_subset [where B="insert 0 {x. P x}"]) |
183 apply (rule finite_subset [where B="insert 0 {x. P x}"]) |
180 apply (clarsimp simp add: ubasis_until') |
184 apply (clarsimp simp add: ubasis_until') |
778 case (ubasis_le_refl a) show ?case by (rule refl_less) |
782 case (ubasis_le_refl a) show ?case by (rule refl_less) |
779 next |
783 next |
780 case (ubasis_le_trans a b c) thus ?case by - (rule trans_less) |
784 case (ubasis_le_trans a b c) thus ?case by - (rule trans_less) |
781 next |
785 next |
782 case (ubasis_le_lower S a i) thus ?case |
786 case (ubasis_le_lower S a i) thus ?case |
783 apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") |
787 apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") |
784 apply (erule rangeE, rename_tac x) |
788 apply (erule rangeE, rename_tac x) |
785 apply (simp add: basis_prj_basis_emb) |
789 apply (simp add: basis_prj_basis_emb) |
786 apply (simp add: node_eq_basis_emb_iff) |
790 apply (simp add: node_eq_basis_emb_iff) |
787 apply (simp add: basis_prj_basis_emb) |
791 apply (simp add: basis_prj_basis_emb) |
788 apply (rule sub_below) |
792 apply (rule sub_below) |
789 apply (simp add: basis_prj_node) |
793 apply (simp add: basis_prj_node) |
790 done |
794 done |
791 next |
795 next |
792 case (ubasis_le_upper S b a i) thus ?case |
796 case (ubasis_le_upper S b a i) thus ?case |
793 apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") |
797 apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") |
794 apply (erule rangeE, rename_tac x) |
798 apply (erule rangeE, rename_tac x) |
795 apply (simp add: basis_prj_basis_emb) |
799 apply (simp add: basis_prj_basis_emb) |
796 apply (clarsimp simp add: node_eq_basis_emb_iff) |
800 apply (clarsimp simp add: node_eq_basis_emb_iff) |
797 apply (simp add: basis_prj_basis_emb) |
801 apply (simp add: basis_prj_basis_emb) |
798 apply (simp add: basis_prj_node) |
802 apply (simp add: basis_prj_node) |