equal
deleted
inserted
replaced
84 { assume "?C" |
84 { assume "?C" |
85 then have "clique (insert v R) E" using \<open>R <= ?M\<close> |
85 then have "clique (insert v R) E" using \<open>R <= ?M\<close> |
86 by(auto simp:clique_def insert_commute) |
86 by(auto simp:clique_def insert_commute) |
87 moreover have "card(insert v R) = m" |
87 moreover have "card(insert v R) = m" |
88 using \<open>?C\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>m\<noteq>0\<close> by simp |
88 using \<open>?C\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>m\<noteq>0\<close> by simp |
89 ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by blast |
89 ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by (metis insert_subset) |
90 } ultimately have "?EX V E m n" using CI by blast |
90 } ultimately have "?EX V E m n" using CI by blast |
91 } moreover |
91 } moreover |
92 { assume "r2 \<le> card ?N" |
92 { assume "r2 \<le> card ?N" |
93 moreover have "finite ?N" using \<open>finite V\<close> by auto |
93 moreover have "finite ?N" using \<open>finite V\<close> by auto |
94 ultimately have "?EX ?N E m (n - 1)" using \<open>?R m (n - 1) r2\<close> by blast |
94 ultimately have "?EX ?N E m (n - 1)" using \<open>?R m (n - 1) r2\<close> by blast |
104 { assume "?I" |
104 { assume "?I" |
105 then have "indep (insert v R) E" using \<open>R <= ?N\<close> |
105 then have "indep (insert v R) E" using \<open>R <= ?N\<close> |
106 by(auto simp:indep_def insert_commute) |
106 by(auto simp:indep_def insert_commute) |
107 moreover have "card(insert v R) = n" |
107 moreover have "card(insert v R) = n" |
108 using \<open>?I\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>n\<noteq>0\<close> by simp |
108 using \<open>?I\<close> \<open>finite R\<close> \<open>v ~: R\<close> \<open>n\<noteq>0\<close> by simp |
109 ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by blast |
109 ultimately have "?EX V E m n" using \<open>R <= V\<close> \<open>v : V\<close> by (metis insert_subset) |
110 } ultimately have "?EX V E m n" using CI by blast |
110 } ultimately have "?EX V E m n" using CI by blast |
111 } ultimately show "?EX V E m n" by blast |
111 } ultimately show "?EX V E m n" by blast |
112 qed |
112 qed |
113 ultimately have ?case by blast |
113 ultimately have ?case by blast |
114 } ultimately show ?case by blast |
114 } ultimately show ?case by blast |