equal
deleted
inserted
replaced
236 by (metis Set.subsetI Union_upper insertCI set_eq_subset) |
236 by (metis Set.subsetI Union_upper insertCI set_eq_subset) |
237 --{*found by SPASS*} |
237 --{*found by SPASS*} |
238 |
238 |
239 lemma (*singleton_example_2:*) |
239 lemma (*singleton_example_2:*) |
240 "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
240 "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
241 by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq) |
241 by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset) |
242 |
242 |
243 lemma singleton_example_2: |
243 lemma singleton_example_2: |
244 "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
244 "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
245 proof (neg_clausify) |
245 proof (neg_clausify) |
246 assume 0: "\<And>x. \<not> S \<subseteq> {x}" |
246 assume 0: "\<And>x. \<not> S \<subseteq> {x}" |
273 "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m" |
273 "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m" |
274 apply (metis atMost_iff) |
274 apply (metis atMost_iff) |
275 apply (metis emptyE) |
275 apply (metis emptyE) |
276 apply (metis insert_iff singletonE) |
276 apply (metis insert_iff singletonE) |
277 apply (metis insertCI singletonE zless_le) |
277 apply (metis insertCI singletonE zless_le) |
278 apply (metis insert_iff singletonE) |
278 apply (metis Collect_def Collect_mem_eq) |
279 apply (metis insert_iff singletonE) |
279 apply (metis Collect_def Collect_mem_eq) |
280 apply (metis DiffE) |
280 apply (metis DiffE) |
281 apply (metis pair_in_Id_conv) |
281 apply (metis pair_in_Id_conv) |
282 done |
282 done |
283 |
283 |
284 end |
284 end |