author | haftmann |
Tue, 13 Jul 2010 16:00:56 +0200 | |
changeset 37804 | 0145e59c1f6c |
parent 37325 | c2a44bc874f9 |
child 41144 | 509e51b7509a |
permissions | -rw-r--r-- |
33027 | 1 |
(* Title: HOL/Metis_Examples/set.thy |
23449 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
||
33027 | 4 |
Testing the metis method. |
23449 | 5 |
*) |
6 |
||
33027 | 7 |
theory set |
8 |
imports Main |
|
23449 | 9 |
begin |
10 |
||
11 |
lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & |
|
12 |
(S(x,y) | ~S(y,z) | Q(Z,Z)) & |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
23519
diff
changeset
|
13 |
(Q(X,y) | ~Q(y,Z) | S(X,X))" |
23519 | 14 |
by metis |
23449 | 15 |
|
16 |
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" |
|
17 |
by metis |
|
18 |
||
36925 | 19 |
sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
23449 | 20 |
|
21 |
(*multiple versions of this example*) |
|
22 |
lemma (*equal_union: *) |
|
36566 | 23 |
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
24 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
25 |
have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>1 \<union> x\<^isub>2" by (metis Un_commute Un_upper2) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
26 |
have F2a: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
27 |
have F2: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
28 |
{ assume "\<not> Z \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
29 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
30 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
31 |
{ assume AA1: "Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
32 |
{ assume "\<not> Y \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
33 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
34 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
35 |
{ assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
36 |
{ assume "\<not> Z \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
37 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
38 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
39 |
{ assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
40 |
hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
41 |
hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
42 |
hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
43 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
44 |
ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
45 |
ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
46 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
47 |
{ assume "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
48 |
{ assume "\<not> Y \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
49 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
50 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
51 |
{ assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
52 |
{ assume "\<not> Z \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
53 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
54 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
55 |
{ assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
56 |
hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
57 |
hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
58 |
hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
59 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
60 |
ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
61 |
ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by blast } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
62 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
63 |
{ assume "\<not> Y \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
64 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
65 |
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis |
23449 | 66 |
qed |
67 |
||
36925 | 68 |
sledgehammer_params [isar_proof, isar_shrink_factor = 2] |
23449 | 69 |
|
70 |
lemma (*equal_union: *) |
|
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
71 |
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
72 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
73 |
have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
74 |
{ assume AA1: "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
75 |
{ assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
76 |
{ assume "\<not> Z \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
77 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
78 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
79 |
{ assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
80 |
hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
81 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
82 |
ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1 Un_subset_iff) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
83 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
84 |
{ assume "\<not> Y \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
85 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
86 |
ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
87 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
88 |
{ assume "\<not> Z \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
89 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
90 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
91 |
{ assume "\<not> Y \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
92 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
93 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
94 |
{ assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
95 |
{ assume "\<not> Z \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
96 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
97 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
98 |
{ assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
99 |
hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
100 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
101 |
ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
102 |
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis |
23449 | 103 |
qed |
104 |
||
36925 | 105 |
sledgehammer_params [isar_proof, isar_shrink_factor = 3] |
23449 | 106 |
|
107 |
lemma (*equal_union: *) |
|
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
108 |
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
109 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
110 |
have F1a: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
111 |
have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
112 |
{ assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
113 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
114 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
115 |
{ assume AA1: "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
116 |
{ assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
117 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
118 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
119 |
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) |
23449 | 120 |
qed |
121 |
||
36925 | 122 |
sledgehammer_params [isar_proof, isar_shrink_factor = 4] |
23449 | 123 |
|
124 |
lemma (*equal_union: *) |
|
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
125 |
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
126 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
127 |
have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
128 |
{ assume "\<not> Y \<subseteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
129 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
130 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
131 |
{ assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
132 |
{ assume "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
133 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
134 |
hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) } |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
135 |
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
136 |
qed |
23449 | 137 |
|
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
138 |
sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
139 |
|
23449 | 140 |
lemma (*equal_union: *) |
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
141 |
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
23449 | 142 |
by (metis Un_least Un_upper1 Un_upper2 set_eq_subset) |
143 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
144 |
lemma "(X = Y \<inter> Z) = (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
145 |
by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym) |
23449 | 146 |
|
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
147 |
lemma fixedpoint: "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y" |
23449 | 148 |
by metis |
149 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
150 |
lemma (* fixedpoint: *) "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
151 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
152 |
assume "\<exists>!x\<Colon>'a. f (g x) = x" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
153 |
thus "\<exists>!y\<Colon>'b. g (f y) = y" by metis |
23449 | 154 |
qed |
155 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
156 |
lemma (* singleton_example_2: *) |
23449 | 157 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
158 |
by (metis Set.subsetI Union_upper insertCI set_eq_subset) |
|
159 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
160 |
lemma (* singleton_example_2: *) |
23449 | 161 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
32685 | 162 |
by (metis Set.subsetI Union_upper insert_iff set_eq_subset) |
23449 | 163 |
|
164 |
lemma singleton_example_2: |
|
165 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
|
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
166 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
167 |
assume "\<forall>x \<in> S. \<Union>S \<subseteq> x" |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
168 |
hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> \<Union>S \<and> x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis set_eq_subset) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
169 |
hence "\<forall>x\<^isub>1. x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis Union_upper) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
170 |
hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. \<Union>S \<in> x\<^isub>1 \<longrightarrow> S \<subseteq> x\<^isub>1" by (metis subsetI) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
171 |
hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. S \<subseteq> insert (\<Union>S) x\<^isub>1" by (metis insert_iff) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
172 |
thus "\<exists>z. S \<subseteq> {z}" by metis |
23449 | 173 |
qed |
174 |
||
175 |
text {* |
|
176 |
From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages |
|
177 |
293-314. |
|
178 |
*} |
|
179 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
180 |
(* Notes: (1) The numbering doesn't completely agree with the paper. |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
181 |
(2) We must rename set variables to avoid type clashes. *) |
23449 | 182 |
lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))" |
183 |
"D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B" |
|
184 |
"P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)" |
|
185 |
"a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B" |
|
186 |
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A" |
|
187 |
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A" |
|
188 |
"\<exists>A. a \<notin> A" |
|
36566 | 189 |
"(\<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" |
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
190 |
apply (metis all_not_in_conv) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
191 |
apply (metis all_not_in_conv) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
192 |
apply (metis mem_def) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
193 |
apply (metis less_int_def singleton_iff) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
194 |
apply (metis mem_def) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
195 |
apply (metis mem_def) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
196 |
apply (metis all_not_in_conv) |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
197 |
by (metis pair_in_Id_conv) |
23449 | 198 |
|
199 |
end |