11 types ubasis = nat |
11 types ubasis = nat |
12 |
12 |
13 definition |
13 definition |
14 node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis" |
14 node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis" |
15 where |
15 where |
16 "node i x A = Suc (prod2nat (i, prod2nat (x, set2nat A)))" |
16 "node i a S = Suc (prod2nat (i, prod2nat (a, set2nat S)))" |
17 |
17 |
18 lemma node_not_0 [simp]: "node i x A \<noteq> 0" |
18 lemma node_not_0 [simp]: "node i a S \<noteq> 0" |
19 unfolding node_def by simp |
19 unfolding node_def by simp |
20 |
20 |
21 lemma node_gt_0 [simp]: "0 < node i x A" |
21 lemma node_gt_0 [simp]: "0 < node i a S" |
22 unfolding node_def by simp |
22 unfolding node_def by simp |
23 |
23 |
24 lemma node_inject [simp]: |
24 lemma node_inject [simp]: |
25 "\<lbrakk>finite A; finite B\<rbrakk> |
25 "\<lbrakk>finite S; finite T\<rbrakk> |
26 \<Longrightarrow> node i x A = node j y B \<longleftrightarrow> i = j \<and> x = y \<and> A = B" |
26 \<Longrightarrow> node i a S = node j b T \<longleftrightarrow> i = j \<and> a = b \<and> S = T" |
27 unfolding node_def by simp |
27 unfolding node_def by simp |
28 |
28 |
29 lemma node_gt0: "i < node i x A" |
29 lemma node_gt0: "i < node i a S" |
30 unfolding node_def less_Suc_eq_le |
30 unfolding node_def less_Suc_eq_le |
31 by (rule le_prod2nat_1) |
31 by (rule le_prod2nat_1) |
32 |
32 |
33 lemma node_gt1: "x < node i x A" |
33 lemma node_gt1: "a < node i a S" |
34 unfolding node_def less_Suc_eq_le |
34 unfolding node_def less_Suc_eq_le |
35 by (rule order_trans [OF le_prod2nat_1 le_prod2nat_2]) |
35 by (rule order_trans [OF le_prod2nat_1 le_prod2nat_2]) |
36 |
36 |
37 lemma nat_less_power2: "n < 2^n" |
37 lemma nat_less_power2: "n < 2^n" |
38 by (induct n) simp_all |
38 by (induct n) simp_all |
39 |
39 |
40 lemma node_gt2: "\<lbrakk>finite A; y \<in> A\<rbrakk> \<Longrightarrow> y < node i x A" |
40 lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> b < node i a S" |
41 unfolding node_def less_Suc_eq_le set2nat_def |
41 unfolding node_def less_Suc_eq_le set2nat_def |
42 apply (rule order_trans [OF _ le_prod2nat_2]) |
42 apply (rule order_trans [OF _ le_prod2nat_2]) |
43 apply (rule order_trans [OF _ le_prod2nat_2]) |
43 apply (rule order_trans [OF _ le_prod2nat_2]) |
44 apply (rule order_trans [where y="setsum (op ^ 2) {y}"]) |
44 apply (rule order_trans [where y="setsum (op ^ 2) {b}"]) |
45 apply (simp add: nat_less_power2 [THEN order_less_imp_le]) |
45 apply (simp add: nat_less_power2 [THEN order_less_imp_le]) |
46 apply (erule setsum_mono2, simp, simp) |
46 apply (erule setsum_mono2, simp, simp) |
47 done |
47 done |
48 |
48 |
49 lemma eq_prod2nat_pairI: |
49 lemma eq_prod2nat_pairI: |
50 "\<lbrakk>fst (nat2prod x) = a; snd (nat2prod x) = b\<rbrakk> \<Longrightarrow> x = prod2nat (a, b)" |
50 "\<lbrakk>fst (nat2prod x) = a; snd (nat2prod x) = b\<rbrakk> \<Longrightarrow> x = prod2nat (a, b)" |
51 by (erule subst, erule subst, simp) |
51 by (erule subst, erule subst, simp) |
52 |
52 |
53 lemma node_cases: |
53 lemma node_cases: |
54 assumes 1: "x = 0 \<Longrightarrow> P" |
54 assumes 1: "x = 0 \<Longrightarrow> P" |
55 assumes 2: "\<And>i y A. \<lbrakk>finite A; x = node i y A\<rbrakk> \<Longrightarrow> P" |
55 assumes 2: "\<And>i a S. \<lbrakk>finite S; x = node i a S\<rbrakk> \<Longrightarrow> P" |
56 shows "P" |
56 shows "P" |
57 apply (cases x) |
57 apply (cases x) |
58 apply (erule 1) |
58 apply (erule 1) |
59 apply (rule 2) |
59 apply (rule 2) |
60 apply (rule finite_nat2set) |
60 apply (rule finite_nat2set) |
577 apply (rule finite_rank_eq) |
583 apply (rule finite_rank_eq) |
578 apply (rule rank_lt_Int_rank_eq) |
584 apply (rule rank_lt_Int_rank_eq) |
579 apply (simp add: rank_lt_Un_rank_eq) |
585 apply (simp add: rank_lt_Un_rank_eq) |
580 done |
586 done |
581 |
587 |
582 lemma reorder_ge: "card (rank_lt x) \<le> reorder x" |
588 lemma place_ge: "card (rank_lt x) \<le> place x" |
583 unfolding reorder_def by simp |
589 unfolding place_def by simp |
584 |
590 |
585 lemma reorder_rank_mono: |
591 lemma place_rank_mono: |
586 fixes x y :: "'a compact_basis" |
592 fixes x y :: "'a compact_basis" |
587 shows "rank x < rank y \<Longrightarrow> reorder x < reorder y" |
593 shows "rank x < rank y \<Longrightarrow> place x < place y" |
588 apply (rule less_le_trans [OF reorder_bounded]) |
594 apply (rule less_le_trans [OF place_bounded]) |
589 apply (rule order_trans [OF _ reorder_ge]) |
595 apply (rule order_trans [OF _ place_ge]) |
590 apply (rule card_mono) |
596 apply (rule card_mono) |
591 apply (rule finite_rank_lt) |
597 apply (rule finite_rank_lt) |
592 apply (simp add: rank_le_def rank_lt_def subset_eq) |
598 apply (simp add: rank_le_def rank_lt_def subset_eq) |
593 done |
599 done |
594 |
600 |
595 lemma reorder_eqD: "reorder x = reorder y \<Longrightarrow> x = y" |
601 lemma place_eqD: "place x = place y \<Longrightarrow> x = y" |
596 apply (rule linorder_cases [where x="rank x" and y="rank y"]) |
602 apply (rule linorder_cases [where x="rank x" and y="rank y"]) |
597 apply (drule reorder_rank_mono, simp) |
603 apply (drule place_rank_mono, simp) |
598 apply (simp add: reorder_def) |
604 apply (simp add: place_def) |
599 apply (rule inj_on_choose_pos [where A="rank_eq x", THEN inj_onD]) |
605 apply (rule inj_on_choose_pos [where A="rank_eq x", THEN inj_onD]) |
600 apply (rule finite_rank_eq) |
606 apply (rule finite_rank_eq) |
601 apply (simp cong: rank_lt_cong rank_eq_cong) |
607 apply (simp cong: rank_lt_cong rank_eq_cong) |
602 apply (simp add: rank_eq_def) |
608 apply (simp add: rank_eq_def) |
603 apply (simp add: rank_eq_def) |
609 apply (simp add: rank_eq_def) |
604 apply (drule reorder_rank_mono, simp) |
610 apply (drule place_rank_mono, simp) |
605 done |
611 done |
606 |
612 |
607 lemma inj_reorder: "inj reorder" |
613 lemma inj_place: "inj place" |
608 by (rule inj_onI, erule reorder_eqD) |
614 by (rule inj_onI, erule place_eqD) |
609 |
615 |
610 subsubsection {* Embedding and projection on basis elements *} |
616 subsubsection {* Embedding and projection on basis elements *} |
611 |
617 |
612 function |
618 definition |
613 basis_emb :: "'a compact_basis \<Rightarrow> ubasis" |
619 sub :: "'a compact_basis \<Rightarrow> 'a compact_basis" |
614 where |
620 where |
615 "basis_emb x = (if x = compact_bot then 0 else |
621 "sub x = (case rank x of 0 \<Rightarrow> compact_bot | Suc k \<Rightarrow> cb_take k x)" |
616 node |
622 |
617 (reorder x) |
623 lemma rank_sub_less: "x \<noteq> compact_bot \<Longrightarrow> rank (sub x) < rank x" |
618 (case rank x of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> basis_emb (cb_take k x)) |
624 unfolding sub_def |
619 (basis_emb ` {y. reorder y < reorder x \<and> x \<sqsubseteq> y}))" |
625 apply (cases "rank x", simp) |
620 by auto |
|
621 |
|
622 termination basis_emb |
|
623 apply (relation "measure reorder", simp) |
|
624 apply simp |
|
625 apply (rule reorder_rank_mono) |
|
626 apply (simp add: less_Suc_eq_le) |
626 apply (simp add: less_Suc_eq_le) |
627 apply (rule rank_leI) |
627 apply (rule rank_leI) |
628 apply (rule cb_take_idem) |
628 apply (rule cb_take_idem) |
|
629 done |
|
630 |
|
631 lemma place_sub_less: "x \<noteq> compact_bot \<Longrightarrow> place (sub x) < place x" |
|
632 apply (rule place_rank_mono) |
|
633 apply (erule rank_sub_less) |
|
634 done |
|
635 |
|
636 lemma sub_below: "sub x \<sqsubseteq> x" |
|
637 unfolding sub_def by (cases "rank x", simp_all add: cb_take_less) |
|
638 |
|
639 lemma rank_less_imp_below_sub: "\<lbrakk>x \<sqsubseteq> y; rank x < rank y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> sub y" |
|
640 unfolding sub_def |
|
641 apply (cases "rank y", simp) |
|
642 apply (simp add: less_Suc_eq_le) |
|
643 apply (subgoal_tac "cb_take nat x \<sqsubseteq> cb_take nat y") |
|
644 apply (simp add: rank_leD) |
|
645 apply (erule cb_take_mono) |
|
646 done |
|
647 |
|
648 function |
|
649 basis_emb :: "'a compact_basis \<Rightarrow> ubasis" |
|
650 where |
|
651 "basis_emb x = (if x = compact_bot then 0 else |
|
652 node (place x) (basis_emb (sub x)) |
|
653 (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}))" |
|
654 by auto |
|
655 |
|
656 termination basis_emb |
|
657 apply (relation "measure place", simp) |
|
658 apply (simp add: place_sub_less) |
629 apply simp |
659 apply simp |
630 done |
660 done |
631 |
661 |
632 declare basis_emb.simps [simp del] |
662 declare basis_emb.simps [simp del] |
633 |
663 |
634 lemma basis_emb_compact_bot [simp]: "basis_emb compact_bot = 0" |
664 lemma basis_emb_compact_bot [simp]: "basis_emb compact_bot = 0" |
635 by (simp add: basis_emb.simps) |
665 by (simp add: basis_emb.simps) |
636 |
666 |
637 lemma fin1: "finite {y. reorder y < reorder x \<and> x \<sqsubseteq> y}" |
667 lemma fin1: "finite {y. place y < place x \<and> x \<sqsubseteq> y}" |
638 apply (subst Collect_conj_eq) |
668 apply (subst Collect_conj_eq) |
639 apply (rule finite_Int) |
669 apply (rule finite_Int) |
640 apply (rule disjI1) |
670 apply (rule disjI1) |
641 apply (subgoal_tac "finite (reorder -` {n. n < reorder x})", simp) |
671 apply (subgoal_tac "finite (place -` {n. n < place x})", simp) |
642 apply (rule finite_vimageI [OF _ inj_reorder]) |
672 apply (rule finite_vimageI [OF _ inj_place]) |
643 apply (simp add: lessThan_def [symmetric]) |
673 apply (simp add: lessThan_def [symmetric]) |
644 done |
674 done |
645 |
675 |
646 lemma fin2: "finite (basis_emb ` {y. reorder y < reorder x \<and> x \<sqsubseteq> y})" |
676 lemma fin2: "finite (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y})" |
647 by (rule finite_imageI [OF fin1]) |
677 by (rule finite_imageI [OF fin1]) |
648 |
678 |
649 lemma basis_emb_mono [OF refl]: |
679 lemma rank_place_mono: |
650 "\<lbrakk>n = max (reorder x) (reorder y); x \<sqsubseteq> y\<rbrakk> |
680 "\<lbrakk>place x < place y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> rank x < rank y" |
651 \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)" |
681 apply (rule linorder_cases, assumption) |
652 proof (induct n arbitrary: x y rule: less_induct) |
682 apply (simp add: place_def cong: rank_lt_cong rank_eq_cong) |
|
683 apply (drule choose_pos_lessD) |
|
684 apply (rule finite_rank_eq) |
|
685 apply (simp add: rank_eq_def) |
|
686 apply (simp add: rank_eq_def) |
|
687 apply simp |
|
688 apply (drule place_rank_mono, simp) |
|
689 done |
|
690 |
|
691 lemma basis_emb_mono: |
|
692 "x \<sqsubseteq> y \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)" |
|
693 proof (induct n \<equiv> "max (place x) (place y)" arbitrary: x y rule: less_induct) |
653 case (less n) |
694 case (less n) |
654 assume IH: |
695 hence IH: |
655 "\<And>(m::nat) (x::'a compact_basis) y. |
696 "\<And>(a::'a compact_basis) b. |
656 \<lbrakk>m < n; m = max (reorder x) (reorder y); x \<sqsubseteq> y\<rbrakk> |
697 \<lbrakk>max (place a) (place b) < max (place x) (place y); a \<sqsubseteq> b\<rbrakk> |
657 \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)" |
698 \<Longrightarrow> ubasis_le (basis_emb a) (basis_emb b)" |
658 assume n: "n = max (reorder x) (reorder y)" |
699 by simp |
659 assume less: "x \<sqsubseteq> y" |
700 show ?case proof (rule linorder_cases) |
660 show ?case |
701 assume "place x < place y" |
661 proof (cases) |
702 then have "rank x < rank y" |
662 assume "x = compact_bot" |
703 using `x \<sqsubseteq> y` by (rule rank_place_mono) |
663 thus ?case by (simp add: ubasis_le_minimal) |
704 with `place x < place y` show ?case |
|
705 apply (case_tac "y = compact_bot", simp) |
|
706 apply (simp add: basis_emb.simps [of y]) |
|
707 apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) |
|
708 apply (rule IH) |
|
709 apply (simp add: less_max_iff_disj) |
|
710 apply (erule place_sub_less) |
|
711 apply (erule rank_less_imp_below_sub [OF `x \<sqsubseteq> y`]) |
|
712 done |
664 next |
713 next |
665 assume x_neq [simp]: "x \<noteq> compact_bot" |
714 assume "place x = place y" |
666 with less have y_neq [simp]: "y \<noteq> compact_bot" |
715 hence "x = y" by (rule place_eqD) |
667 apply clarify |
716 thus ?case by (simp add: ubasis_le_refl) |
668 apply (drule antisym_less [OF compact_bot_minimal]) |
717 next |
669 apply simp |
718 assume "place x > place y" |
|
719 with `x \<sqsubseteq> y` show ?case |
|
720 apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal) |
|
721 apply (simp add: basis_emb.simps [of x]) |
|
722 apply (rule ubasis_le_upper [OF fin2], simp) |
|
723 apply (rule IH) |
|
724 apply (simp add: less_max_iff_disj) |
|
725 apply (erule place_sub_less) |
|
726 apply (erule rev_trans_less) |
|
727 apply (rule sub_below) |
670 done |
728 done |
671 show ?case |
|
672 proof (rule linorder_cases) |
|
673 assume 1: "reorder x < reorder y" |
|
674 show ?case |
|
675 proof (rule linorder_cases) |
|
676 assume "rank x < rank y" |
|
677 with 1 show ?case |
|
678 apply (case_tac "rank y", simp) |
|
679 apply (subst basis_emb.simps [where x=y]) |
|
680 apply simp |
|
681 apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) |
|
682 apply (rule IH [OF _ refl, unfolded n]) |
|
683 apply (simp add: less_max_iff_disj) |
|
684 apply (rule reorder_rank_mono) |
|
685 apply (simp add: less_Suc_eq_le) |
|
686 apply (rule rank_leI) |
|
687 apply (rule cb_take_idem) |
|
688 apply (simp add: less_Suc_eq_le) |
|
689 apply (subgoal_tac "cb_take nat x \<sqsubseteq> cb_take nat y") |
|
690 apply (simp add: rank_leD) |
|
691 apply (rule cb_take_mono [OF less]) |
|
692 done |
|
693 next |
|
694 assume "rank x = rank y" |
|
695 with 1 show ?case |
|
696 apply (simp add: reorder_def) |
|
697 apply (simp cong: rank_lt_cong rank_eq_cong) |
|
698 apply (drule choose_pos_lessD) |
|
699 apply (rule finite_rank_eq) |
|
700 apply (simp add: rank_eq_def) |
|
701 apply (simp add: rank_eq_def) |
|
702 apply (simp add: less) |
|
703 done |
|
704 next |
|
705 assume "rank x > rank y" |
|
706 hence "reorder x > reorder y" |
|
707 by (rule reorder_rank_mono) |
|
708 with 1 show ?case by simp |
|
709 qed |
|
710 next |
|
711 assume "reorder x = reorder y" |
|
712 hence "x = y" by (rule reorder_eqD) |
|
713 thus ?case by (simp add: ubasis_le_refl) |
|
714 next |
|
715 assume "reorder x > reorder y" |
|
716 with less show ?case |
|
717 apply (simp add: basis_emb.simps [where x=x]) |
|
718 apply (rule ubasis_le_upper [OF fin2], simp) |
|
719 apply (cases "rank x") |
|
720 apply (simp add: ubasis_le_minimal) |
|
721 apply simp |
|
722 apply (rule IH [OF _ refl, unfolded n]) |
|
723 apply (simp add: less_max_iff_disj) |
|
724 apply (rule reorder_rank_mono) |
|
725 apply (simp add: less_Suc_eq_le) |
|
726 apply (rule rank_leI) |
|
727 apply (rule cb_take_idem) |
|
728 apply (erule rev_trans_less) |
|
729 apply (rule cb_take_less) |
|
730 done |
|
731 qed |
|
732 qed |
729 qed |
733 qed |
730 qed |
734 |
731 |
735 lemma inj_basis_emb: "inj basis_emb" |
732 lemma inj_basis_emb: "inj basis_emb" |
736 apply (rule inj_onI) |
733 apply (rule inj_onI) |
738 apply (case_tac [!] "y = compact_bot") |
735 apply (case_tac [!] "y = compact_bot") |
739 apply simp |
736 apply simp |
740 apply (simp add: basis_emb.simps) |
737 apply (simp add: basis_emb.simps) |
741 apply (simp add: basis_emb.simps) |
738 apply (simp add: basis_emb.simps) |
742 apply (simp add: basis_emb.simps) |
739 apply (simp add: basis_emb.simps) |
743 apply (simp add: fin2 inj_eq [OF inj_reorder]) |
740 apply (simp add: fin2 inj_eq [OF inj_place]) |
744 done |
741 done |
745 |
742 |
746 definition |
743 definition |
747 basis_prj :: "nat \<Rightarrow> 'a compact_basis" |
744 basis_prj :: "ubasis \<Rightarrow> 'a compact_basis" |
748 where |
745 where |
749 "basis_prj x = inv basis_emb |
746 "basis_prj x = inv basis_emb |
750 (ubasis_until (\<lambda>x. x \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)) x)" |
747 (ubasis_until (\<lambda>x. x \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> ubasis)) x)" |
751 |
748 |
752 lemma basis_prj_basis_emb: "\<And>x. basis_prj (basis_emb x) = x" |
749 lemma basis_prj_basis_emb: "\<And>x. basis_prj (basis_emb x) = x" |
753 unfolding basis_prj_def |
750 unfolding basis_prj_def |
754 apply (subst ubasis_until_same) |
751 apply (subst ubasis_until_same) |
755 apply (rule rangeI) |
752 apply (rule rangeI) |
756 apply (rule inv_f_f) |
753 apply (rule inv_f_f) |
757 apply (rule inj_basis_emb) |
754 apply (rule inj_basis_emb) |
758 done |
755 done |
759 |
756 |
760 lemma basis_prj_node: |
757 lemma basis_prj_node: |
761 "\<lbrakk>finite A; node i x A \<notin> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)\<rbrakk> |
758 "\<lbrakk>finite S; node i a S \<notin> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)\<rbrakk> |
762 \<Longrightarrow> basis_prj (node i x A) = (basis_prj x :: 'a compact_basis)" |
759 \<Longrightarrow> basis_prj (node i a S) = (basis_prj a :: 'a compact_basis)" |
763 unfolding basis_prj_def by simp |
760 unfolding basis_prj_def by simp |
764 |
761 |
765 lemma basis_prj_0: "basis_prj 0 = compact_bot" |
762 lemma basis_prj_0: "basis_prj 0 = compact_bot" |
766 apply (subst basis_emb_compact_bot [symmetric]) |
763 apply (subst basis_emb_compact_bot [symmetric]) |
767 apply (rule basis_prj_basis_emb) |
764 apply (rule basis_prj_basis_emb) |
768 done |
765 done |
769 |
766 |
770 lemma basis_prj_mono: "ubasis_le x y \<Longrightarrow> basis_prj x \<sqsubseteq> basis_prj y" |
767 lemma node_eq_basis_emb_iff: |
771 apply (erule ubasis_le.induct) |
768 "finite S \<Longrightarrow> node i a S = basis_emb x \<longleftrightarrow> |
772 apply (rule refl_less) |
769 x \<noteq> compact_bot \<and> i = place x \<and> a = basis_emb (sub x) \<and> |
773 apply (erule (1) trans_less) |
770 S = basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}" |
774 apply (case_tac "node i x A \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") |
771 apply (cases "x = compact_bot", simp) |
775 apply (erule rangeE, rename_tac a) |
772 apply (simp add: basis_emb.simps [of x]) |
776 apply (case_tac "a = compact_bot", simp) |
773 apply (simp add: fin2) |
777 apply (simp add: basis_prj_basis_emb) |
774 done |
778 apply (simp add: basis_emb.simps) |
775 |
779 apply (clarsimp simp add: fin2) |
776 lemma basis_prj_mono: "ubasis_le a b \<Longrightarrow> basis_prj a \<sqsubseteq> basis_prj b" |
780 apply (case_tac "rank a", simp) |
777 proof (induct a b rule: ubasis_le.induct) |
781 apply (simp add: basis_prj_0) |
778 case (ubasis_le_refl a) show ?case by (rule refl_less) |
782 apply (simp add: basis_prj_basis_emb) |
779 next |
783 apply (rule cb_take_less) |
780 case (ubasis_le_trans a b c) thus ?case by - (rule trans_less) |
784 apply (simp add: basis_prj_node) |
781 next |
785 apply (case_tac "node i x A \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") |
782 case (ubasis_le_lower S a i) thus ?case |
786 apply (erule rangeE, rename_tac a) |
783 apply (case_tac "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") |
787 apply (case_tac "a = compact_bot", simp) |
784 apply (erule rangeE, rename_tac x) |
788 apply (simp add: basis_prj_basis_emb) |
785 apply (simp add: basis_prj_basis_emb) |
789 apply (simp add: basis_emb.simps) |
786 apply (simp add: node_eq_basis_emb_iff) |
790 apply (clarsimp simp add: fin2) |
787 apply (simp add: basis_prj_basis_emb) |
791 apply (case_tac "rank a", simp add: basis_prj_basis_emb) |
788 apply (rule sub_below) |
792 apply (simp add: basis_prj_basis_emb) |
789 apply (simp add: basis_prj_node) |
793 apply (simp add: basis_prj_node) |
790 done |
794 done |
791 next |
|
792 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)") |
|
794 apply (erule rangeE, rename_tac x) |
|
795 apply (simp add: basis_prj_basis_emb) |
|
796 apply (clarsimp simp add: node_eq_basis_emb_iff) |
|
797 apply (simp add: basis_prj_basis_emb) |
|
798 apply (simp add: basis_prj_node) |
|
799 done |
|
800 qed |
795 |
801 |
796 lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x" |
802 lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x" |
797 unfolding basis_prj_def |
803 unfolding basis_prj_def |
798 apply (subst f_inv_f [where f=basis_emb]) |
804 apply (subst f_inv_f [where f=basis_emb]) |
799 apply (rule ubasis_until) |
805 apply (rule ubasis_until) |