2772 |
2780 |
2773 subsection {* Hence we get just about the nice induction. *} |
2781 subsection {* Hence we get just about the nice induction. *} |
2774 |
2782 |
2775 lemma kuhn_induction: |
2783 lemma kuhn_induction: |
2776 assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" |
2784 assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" |
2777 "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)" |
2785 "\<forall>x. \<forall>j\<in>{1..n+1}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)" |
2778 "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})" |
2786 "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})" |
2779 shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) ` s = {0..n+1})})" proof- |
2787 shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) ` s = {0..n+1})})" |
2780 have *:"\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)" "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto |
2788 proof - |
2781 show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling) |
2789 have *: "\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)" |
2782 apply(rule *(1)[OF assms(4)]) apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*) |
2790 "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto |
2783 fix f assume as:"ksimplex p n f" "reduced lab n ` f = {0..n}" |
2791 show ?thesis |
2784 have *:"\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0" "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1" |
2792 apply (rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) |
|
2793 apply (rule, rule, rule *, rule reduced_labelling) |
|
2794 apply (rule *(1)[OF assms(4)]) |
|
2795 apply (rule set_eqI) |
|
2796 unfolding mem_Collect_eq |
|
2797 apply (rule, erule conjE) |
|
2798 defer |
|
2799 apply rule |
|
2800 proof - |
|
2801 fix f |
|
2802 assume as: "ksimplex p n f" "reduced lab n ` f = {0..n}" |
|
2803 have *: "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0" |
|
2804 "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1" |
2785 using assms(2-3) using as(1)[unfolded ksimplex_def] by auto |
2805 using assms(2-3) using as(1)[unfolded ksimplex_def] by auto |
2786 have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto |
2806 have allp: "\<forall>x\<in>f. x (n + 1) = p" |
2787 { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_nonzero) |
2807 using assms(2) using as(1)[unfolded ksimplex_def] by auto |
2788 defer using assms(3) using as(1)[unfolded ksimplex_def] by auto |
2808 { |
2789 hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto } |
2809 fix x |
2790 hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[symmetric] apply- apply(rule set_eqI) unfolding image_iff by auto |
2810 assume "x \<in> f" |
2791 moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] .. then guess a .. |
2811 hence "reduced lab (n + 1) x < n + 1" |
|
2812 apply - |
|
2813 apply (rule reduced_labelling_nonzero) |
|
2814 defer using assms(3) using as(1)[unfolded ksimplex_def] |
|
2815 apply auto |
|
2816 done |
|
2817 hence "reduced lab (n + 1) x = reduced lab n x" |
|
2818 apply - |
|
2819 apply (rule reduced_labelling_Suc) |
|
2820 using reduced_labelling(1) |
|
2821 apply auto |
|
2822 done |
|
2823 } |
|
2824 hence "reduced lab (n + 1) ` f = {0..n}" |
|
2825 unfolding as(2)[symmetric] |
|
2826 apply - |
|
2827 apply (rule set_eqI) |
|
2828 unfolding image_iff |
|
2829 apply auto |
|
2830 done |
|
2831 moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] .. |
|
2832 then guess a .. |
2792 ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and> |
2833 ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and> |
2793 a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex) |
2834 a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex) |
2794 apply(rule_tac x=s in exI,rule_tac x=a in exI) unfolding complete_face_top[OF *] using allp as(1) by auto |
2835 apply (rule_tac x = s in exI) |
2795 next fix f assume as:"\<exists>s a. ksimplex p (n + 1) s \<and> |
2836 apply (rule_tac x = a in exI) |
|
2837 unfolding complete_face_top[OF *] |
|
2838 using allp as(1) |
|
2839 apply auto |
|
2840 done |
|
2841 next |
|
2842 fix f |
|
2843 assume as: "\<exists>s a. ksimplex p (n + 1) s \<and> |
2796 a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex) |
2844 a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex) |
2797 then guess s .. then guess a apply-apply(erule exE,(erule conjE)+) . note sa=this |
2845 then guess s .. |
2798 { fix x assume "x\<in>f" hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" by auto |
2846 then guess a |
2799 hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto |
2847 apply - |
2800 hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) |
2848 apply (erule exE,(erule conjE)+) |
2801 using reduced_labelling(1) by auto } |
2849 done |
2802 thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[symmetric] apply-apply(rule set_eqI) unfolding image_iff by auto |
2850 note sa = this |
2803 have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0") |
2851 { |
2804 case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_zero) apply assumption |
2852 fix x |
2805 apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover |
2853 assume "x \<in> f" |
|
2854 hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" |
|
2855 by auto |
|
2856 hence "reduced lab (n + 1) x < n + 1" |
|
2857 using sa(4) by auto |
|
2858 hence "reduced lab (n + 1) x = reduced lab n x" |
|
2859 apply - |
|
2860 apply (rule reduced_labelling_Suc) |
|
2861 using reduced_labelling(1) |
|
2862 apply auto |
|
2863 done |
|
2864 } |
|
2865 thus part1: "reduced lab n ` f = {0..n}" |
|
2866 unfolding sa(4)[symmetric] |
|
2867 apply - |
|
2868 apply (rule set_eqI) |
|
2869 unfolding image_iff |
|
2870 apply auto |
|
2871 done |
|
2872 have *: "\<forall>x\<in>f. x (n + 1) = p" |
|
2873 proof (cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0") |
|
2874 case True |
|
2875 then guess j .. |
|
2876 hence "\<And>x. x \<in> f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" |
|
2877 apply - |
|
2878 apply (rule reduced_labelling_zero) |
|
2879 apply assumption |
|
2880 apply (rule assms(2)[rule_format]) |
|
2881 using sa(1)[unfolded ksimplex_def] |
|
2882 unfolding sa |
|
2883 apply auto |
|
2884 done |
|
2885 moreover |
2806 have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto |
2886 have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto |
2807 ultimately have False unfolding sa(4)[symmetric] unfolding image_iff by fastforce thus ?thesis by auto next |
2887 ultimately have False |
2808 case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastforce then guess j .. note j=this |
2888 unfolding sa(4)[symmetric] |
2809 thus ?thesis proof(cases "j = n+1") |
2889 unfolding image_iff |
2810 case False hence *:"j\<in>{1..n}" using j by auto |
2890 by fastforce |
2811 hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_nonzero) proof- fix x assume "x\<in>f" |
2891 thus ?thesis by auto |
2812 hence "lab x j = 1" apply-apply(rule assms(3)[rule_format,OF j(1)]) |
2892 next |
2813 using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \<noteq> 0" by auto qed |
2893 case False |
2814 moreover have "j\<in>{0..n}" using * by auto |
2894 hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" |
2815 ultimately have False unfolding part1[symmetric] using * unfolding image_iff by auto thus ?thesis by auto qed auto qed |
2895 using sa(5) by fastforce then guess j .. note j=this |
2816 thus "ksimplex p n f" using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto qed qed |
2896 thus ?thesis |
|
2897 proof (cases "j = n + 1") |
|
2898 case False hence *: "j \<in> {1..n}" |
|
2899 using j by auto |
|
2900 hence "\<And>x. x \<in> f \<Longrightarrow> reduced lab n x < j" |
|
2901 apply (rule reduced_labelling_nonzero) |
|
2902 proof - |
|
2903 fix x |
|
2904 assume "x \<in> f" |
|
2905 hence "lab x j = 1" |
|
2906 apply - |
|
2907 apply (rule assms(3)[rule_format,OF j(1)]) |
|
2908 using sa(1)[unfolded ksimplex_def] |
|
2909 using j |
|
2910 unfolding sa |
|
2911 apply auto |
|
2912 done |
|
2913 thus "lab x j \<noteq> 0" by auto |
|
2914 qed |
|
2915 moreover have "j \<in> {0..n}" using * by auto |
|
2916 ultimately have False |
|
2917 unfolding part1[symmetric] |
|
2918 using * unfolding image_iff |
|
2919 by auto |
|
2920 thus ?thesis by auto |
|
2921 qed auto |
|
2922 qed |
|
2923 thus "ksimplex p n f" |
|
2924 using as unfolding simplex_top_face[OF assms(1) *,symmetric] by auto |
|
2925 qed |
|
2926 qed |
2817 |
2927 |
2818 lemma kuhn_induction_Suc: |
2928 lemma kuhn_induction_Suc: |
2819 assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" |
2929 assumes "0 < p" "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" |
2820 "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)" |
2930 "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> (x j = p) \<longrightarrow> (lab x j = 1)" |
2821 "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})" |
2931 "odd (card {f. ksimplex p n f \<and> ((reduced lab n) ` f = {0..n})})" |
2822 shows "odd (card {s. ksimplex p (Suc n) s \<and>((reduced lab (Suc n)) ` s = {0..Suc n})})" |
2932 shows "odd (card {s. ksimplex p (Suc n) s \<and>((reduced lab (Suc n)) ` s = {0..Suc n})})" |
2823 using assms unfolding Suc_eq_plus1 by(rule kuhn_induction) |
2933 using assms unfolding Suc_eq_plus1 by(rule kuhn_induction) |
2824 |
2934 |
|
2935 |
2825 subsection {* And so we get the final combinatorial result. *} |
2936 subsection {* And so we get the final combinatorial result. *} |
2826 |
2937 |
2827 lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}" (is "?l = ?r") proof |
2938 lemma ksimplex_0: "ksimplex p 0 s \<longleftrightarrow> s = {(\<lambda>x. p)}" (is "?l = ?r") |
2828 assume l:?l guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a=this |
2939 proof |
2829 have "a = (\<lambda>x. p)" using ksimplexD(5)[OF l, rule_format, OF a(1)] by(rule,auto) thus ?r using a by auto next |
2940 assume l: ?l |
2830 assume r:?r show ?l unfolding r ksimplex_eq by auto qed |
2941 guess a using ksimplexD(3)[OF l, unfolded add_0] unfolding card_1_exists .. note a = this |
2831 |
2942 have "a = (\<lambda>x. p)" |
2832 lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0" apply(rule reduced_labelling_unique) by auto |
2943 using ksimplexD(5)[OF l, rule_format, OF a(1)] by rule auto |
|
2944 thus ?r using a by auto |
|
2945 next |
|
2946 assume r: ?r |
|
2947 show ?l unfolding r ksimplex_eq by auto |
|
2948 qed |
|
2949 |
|
2950 lemma reduce_labelling_zero[simp]: "reduced lab 0 x = 0" |
|
2951 by (rule reduced_labelling_unique) auto |
2833 |
2952 |
2834 lemma kuhn_combinatorial: |
2953 lemma kuhn_combinatorial: |
2835 assumes "0 < p" "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" |
2954 assumes "0 < p" "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = 0) \<longrightarrow> (lab x j = 0)" |
2836 "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = p) \<longrightarrow> (lab x j = 1)" |
2955 "\<forall>x j. (\<forall>j. x(j) \<le> p) \<and> 1 \<le> j \<and> j \<le> n \<and> (x j = p) \<longrightarrow> (lab x j = 1)" |
2837 shows " odd (card {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})})" using assms proof(induct n) |
2956 shows " odd (card {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})})" |
|
2957 using assms |
|
2958 proof (induct n) |
2838 let ?M = "\<lambda>n. {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})}" |
2959 let ?M = "\<lambda>n. {s. ksimplex p n s \<and> ((reduced lab n) ` s = {0..n})}" |
2839 { case 0 have *:"?M 0 = {{(\<lambda>x. p)}}" unfolding ksimplex_0 by auto show ?case unfolding * by auto } |
2960 { |
2840 case (Suc n) have "odd (card (?M n))" apply(rule Suc(1)[OF Suc(2)]) using Suc(3-) by auto |
2961 case 0 |
2841 thus ?case apply-apply(rule kuhn_induction_Suc) using Suc(2-) by auto qed |
2962 have *: "?M 0 = {{(\<lambda>x. p)}}" |
2842 |
2963 unfolding ksimplex_0 by auto |
2843 lemma kuhn_lemma: assumes "0 < (p::nat)" "0 < (n::nat)" |
2964 show ?case unfolding * by auto |
2844 "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (label x i = (0::nat)) \<or> (label x i = 1))" |
2965 next |
2845 "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = 0) \<longrightarrow> (label x i = 0))" |
2966 case (Suc n) |
2846 "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = p) \<longrightarrow> (label x i = 1))" |
2967 have "odd (card (?M n))" |
|
2968 apply (rule Suc(1)[OF Suc(2)]) |
|
2969 using Suc(3-) |
|
2970 apply auto |
|
2971 done |
|
2972 thus ?case |
|
2973 apply - |
|
2974 apply (rule kuhn_induction_Suc) |
|
2975 using Suc(2-) |
|
2976 apply auto |
|
2977 done |
|
2978 } |
|
2979 qed |
|
2980 |
|
2981 lemma kuhn_lemma: |
|
2982 assumes "0 < (p::nat)" "0 < (n::nat)" |
|
2983 "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (label x i = (0::nat)) \<or> (label x i = 1))" |
|
2984 "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = 0) \<longrightarrow> (label x i = 0))" |
|
2985 "\<forall>x. (\<forall>i\<in>{1..n}. x i \<le> p) \<longrightarrow> (\<forall>i\<in>{1..n}. (x i = p) \<longrightarrow> (label x i = 1))" |
2847 obtains q where "\<forall>i\<in>{1..n}. q i < p" |
2986 obtains q where "\<forall>i\<in>{1..n}. q i < p" |
2848 "\<forall>i\<in>{1..n}. \<exists>r s. (\<forall>j\<in>{1..n}. q(j) \<le> r(j) \<and> r(j) \<le> q(j) + 1) \<and> |
2987 "\<forall>i\<in>{1..n}. \<exists>r s. (\<forall>j\<in>{1..n}. q(j) \<le> r(j) \<and> r(j) \<le> q(j) + 1) \<and> |
2849 (\<forall>j\<in>{1..n}. q(j) \<le> s(j) \<and> s(j) \<le> q(j) + 1) \<and> |
2988 (\<forall>j\<in>{1..n}. q(j) \<le> s(j) \<and> s(j) \<le> q(j) + 1) \<and> |
2850 ~(label r i = label s i)" proof- |
2989 ~(label r i = label s i)" |
2851 let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}" have "n\<noteq>0" using assms by auto |
2990 proof - |
2852 have conjD:"\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q" by auto |
2991 let ?A = "{s. ksimplex p n s \<and> reduced label n ` s = {0..n}}" |
2853 have "odd (card ?A)" apply(rule kuhn_combinatorial[of p n label]) using assms by auto |
2992 have "n \<noteq> 0" using assms by auto |
2854 hence "card ?A \<noteq> 0" apply-apply(rule ccontr) by auto hence "?A \<noteq> {}" unfolding card_eq_0_iff by auto |
2993 have conjD:"\<And>P Q. P \<and> Q \<Longrightarrow> P" "\<And>P Q. P \<and> Q \<Longrightarrow> Q" |
2855 then obtain s where "s\<in>?A" by auto note s=conjD[OF this[unfolded mem_Collect_eq]] |
2994 by auto |
2856 guess a b apply(rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) . note ab=this |
2995 have "odd (card ?A)" |
2857 show ?thesis apply(rule that[of a]) proof(rule_tac[!] ballI) fix i assume "i\<in>{1..n}" |
2996 apply (rule kuhn_combinatorial[of p n label]) |
2858 hence "a i + 1 \<le> p" apply-apply(rule order_trans[of _ "b i"]) apply(subst ab(5)[THEN spec[where x=i]]) |
2997 using assms |
2859 using s(1)[unfolded ksimplex_def] defer apply- apply(erule conjE)+ apply(drule_tac bspec[OF _ ab(2)])+ by auto |
2998 apply auto |
|
2999 done |
|
3000 hence "card ?A \<noteq> 0" |
|
3001 apply - |
|
3002 apply (rule ccontr) |
|
3003 apply auto |
|
3004 done |
|
3005 hence "?A \<noteq> {}" unfolding card_eq_0_iff by auto |
|
3006 then obtain s where "s \<in> ?A" |
|
3007 by auto note s=conjD[OF this[unfolded mem_Collect_eq]] |
|
3008 guess a b by (rule ksimplex_extrema_strong[OF s(1) `n\<noteq>0`]) note ab = this |
|
3009 show ?thesis |
|
3010 apply (rule that[of a]) |
|
3011 apply (rule_tac[!] ballI) |
|
3012 proof - |
|
3013 fix i |
|
3014 assume "i\<in>{1..n}" |
|
3015 hence "a i + 1 \<le> p" |
|
3016 apply - |
|
3017 apply (rule order_trans[of _ "b i"]) |
|
3018 apply (subst ab(5)[THEN spec[where x=i]]) |
|
3019 using s(1)[unfolded ksimplex_def] |
|
3020 defer |
|
3021 apply - |
|
3022 apply (erule conjE)+ |
|
3023 apply (drule_tac bspec[OF _ ab(2)])+ |
|
3024 apply auto |
|
3025 done |
2860 thus "a i < p" by auto |
3026 thus "a i < p" by auto |
2861 case goal2 hence "i \<in> reduced label n ` s" using s by auto then guess u unfolding image_iff .. note u=this |
3027 next |
2862 from goal2 have "i - 1 \<in> reduced label n ` s" using s by auto then guess v unfolding image_iff .. note v=this |
3028 case goal2 |
2863 show ?case apply(rule_tac x=u in exI, rule_tac x=v in exI) apply(rule conjI) defer apply(rule conjI) defer 2 proof(rule_tac[1-2] ballI) |
3029 hence "i \<in> reduced label n ` s" using s by auto |
2864 show "label u i \<noteq> label v i" using reduced_labelling[of label n u] reduced_labelling[of label n v] |
3030 then guess u unfolding image_iff .. note u = this |
2865 unfolding u(2)[symmetric] v(2)[symmetric] using goal2 by auto |
3031 from goal2 have "i - 1 \<in> reduced label n ` s" |
2866 fix j assume j:"j\<in>{1..n}" show "a j \<le> u j \<and> u j \<le> a j + 1" "a j \<le> v j \<and> v j \<le> a j + 1" |
3032 using s by auto |
2867 using conjD[OF ab(4)[rule_format, OF u(1)]] and conjD[OF ab(4)[rule_format, OF v(1)]] apply- |
3033 then guess v unfolding image_iff .. note v = this |
2868 apply(drule_tac[!] kle_imp_pointwise)+ apply(erule_tac[!] x=j in allE)+ unfolding ab(5)[rule_format] using j |
3034 show ?case |
2869 by auto qed qed qed |
3035 apply (rule_tac x = u in exI) |
|
3036 apply (rule_tac x = v in exI) |
|
3037 apply (rule conjI) |
|
3038 defer |
|
3039 apply (rule conjI) |
|
3040 defer 2 |
|
3041 apply (rule_tac[1-2] ballI) |
|
3042 proof - |
|
3043 show "label u i \<noteq> label v i" |
|
3044 using reduced_labelling [of label n u] reduced_labelling [of label n v] |
|
3045 unfolding u(2)[symmetric] v(2)[symmetric] |
|
3046 using goal2 |
|
3047 apply auto |
|
3048 done |
|
3049 fix j |
|
3050 assume j: "j \<in> {1..n}" |
|
3051 show "a j \<le> u j \<and> u j \<le> a j + 1" "a j \<le> v j \<and> v j \<le> a j + 1" |
|
3052 using conjD[OF ab(4)[rule_format, OF u(1)]] |
|
3053 and conjD[OF ab(4)[rule_format, OF v(1)]] |
|
3054 apply - |
|
3055 apply (drule_tac[!] kle_imp_pointwise)+ |
|
3056 apply (erule_tac[!] x=j in allE)+ |
|
3057 unfolding ab(5)[rule_format] |
|
3058 using j |
|
3059 apply auto |
|
3060 done |
|
3061 qed |
|
3062 qed |
|
3063 qed |
2870 |
3064 |
2871 |
3065 |
2872 subsection {* The main result for the unit cube. *} |
3066 subsection {* The main result for the unit cube. *} |
2873 |
3067 |
2874 lemma kuhn_labelling_lemma': |
3068 lemma kuhn_labelling_lemma': |