author | blanchet |
Thu, 24 Mar 2011 17:49:27 +0100 | |
changeset 42103 | 6066a35f6678 |
parent 41144 | 509e51b7509a |
permissions | -rw-r--r-- |
33027 | 1 |
(* Title: HOL/Metis_Examples/set.thy |
23449 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
41144 | 3 |
Author: Jasmin Blanchette, TU Muenchen |
23449 | 4 |
|
41144 | 5 |
Testing Metis. |
23449 | 6 |
*) |
7 |
||
33027 | 8 |
theory set |
9 |
imports Main |
|
23449 | 10 |
begin |
11 |
||
42103
6066a35f6678
Metis examples use the new Skolemizer to test it
blanchet
parents:
41144
diff
changeset
|
12 |
declare [[metis_new_skolemizer]] |
6066a35f6678
Metis examples use the new Skolemizer to test it
blanchet
parents:
41144
diff
changeset
|
13 |
|
23449 | 14 |
lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & |
15 |
(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
|
16 |
(Q(X,y) | ~Q(y,Z) | S(X,X))" |
23519 | 17 |
by metis |
23449 | 18 |
|
19 |
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" |
|
20 |
by metis |
|
21 |
||
36925 | 22 |
sledgehammer_params [isar_proof, isar_shrink_factor = 1] |
23449 | 23 |
|
24 |
(*multiple versions of this example*) |
|
25 |
lemma (*equal_union: *) |
|
36566 | 26 |
"(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
|
27 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
28 |
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
|
29 |
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
|
30 |
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
|
31 |
{ 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
|
32 |
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
|
33 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
34 |
{ 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
|
35 |
{ 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
|
36 |
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
|
37 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
38 |
{ 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
|
39 |
{ 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
|
40 |
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
|
41 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
42 |
{ 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
|
43 |
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
|
44 |
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
|
45 |
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
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
50 |
{ 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
|
51 |
{ 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
|
52 |
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
|
53 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
54 |
{ 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
|
55 |
{ 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
|
56 |
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
|
57 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
58 |
{ 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
|
59 |
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
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
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
|
64 |
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
|
65 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
66 |
{ 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
|
67 |
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
|
68 |
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 | 69 |
qed |
70 |
||
36925 | 71 |
sledgehammer_params [isar_proof, isar_shrink_factor = 2] |
23449 | 72 |
|
73 |
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
|
74 |
"(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
|
75 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
76 |
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
|
77 |
{ 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
|
78 |
{ 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
|
79 |
{ 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
|
80 |
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
|
81 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
82 |
{ 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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
87 |
{ 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
|
88 |
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
|
89 |
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
|
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> 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
|
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_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 "\<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
|
95 |
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
|
96 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
97 |
{ 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
|
98 |
{ 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
|
99 |
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
|
100 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
101 |
{ 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
|
102 |
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
|
103 |
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
|
104 |
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
|
105 |
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 | 106 |
qed |
107 |
||
36925 | 108 |
sledgehammer_params [isar_proof, isar_shrink_factor = 3] |
23449 | 109 |
|
110 |
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
|
111 |
"(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
|
112 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
113 |
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
|
114 |
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
|
115 |
{ 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
|
116 |
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
|
117 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
118 |
{ 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
|
119 |
{ 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
|
120 |
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
|
121 |
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
|
122 |
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 | 123 |
qed |
124 |
||
36925 | 125 |
sledgehammer_params [isar_proof, isar_shrink_factor = 4] |
23449 | 126 |
|
127 |
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
|
128 |
"(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
|
129 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
130 |
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
|
131 |
{ 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
|
132 |
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
|
133 |
moreover |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
134 |
{ 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
|
135 |
{ 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
|
136 |
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
|
137 |
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
|
138 |
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
|
139 |
qed |
23449 | 140 |
|
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 |
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
|
142 |
|
23449 | 143 |
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
|
144 |
"(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 | 145 |
by (metis Un_least Un_upper1 Un_upper2 set_eq_subset) |
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 "(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
|
148 |
by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym) |
23449 | 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" |
23449 | 151 |
by metis |
152 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
153 |
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
|
154 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
155 |
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
|
156 |
thus "\<exists>!y\<Colon>'b. g (f y) = y" by metis |
23449 | 157 |
qed |
158 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
159 |
lemma (* singleton_example_2: *) |
23449 | 160 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
161 |
by (metis Set.subsetI Union_upper insertCI set_eq_subset) |
|
162 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
163 |
lemma (* singleton_example_2: *) |
23449 | 164 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
32685 | 165 |
by (metis Set.subsetI Union_upper insert_iff set_eq_subset) |
23449 | 166 |
|
167 |
lemma singleton_example_2: |
|
168 |
"\<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
|
169 |
proof - |
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
170 |
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
|
171 |
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
|
172 |
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
|
173 |
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
|
174 |
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
|
175 |
thus "\<exists>z. S \<subseteq> {z}" by metis |
23449 | 176 |
qed |
177 |
||
178 |
text {* |
|
179 |
From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages |
|
180 |
293-314. |
|
181 |
*} |
|
182 |
||
37325
c2a44bc874f9
redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents:
36925
diff
changeset
|
183 |
(* 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
|
184 |
(2) We must rename set variables to avoid type clashes. *) |
23449 | 185 |
lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))" |
186 |
"D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B" |
|
187 |
"P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)" |
|
188 |
"a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B" |
|
189 |
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A" |
|
190 |
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A" |
|
191 |
"\<exists>A. a \<notin> A" |
|
36566 | 192 |
"(\<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
|
193 |
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
|
194 |
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
|
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 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
|
197 |
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
|
198 |
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
|
199 |
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
|
200 |
by (metis pair_in_Id_conv) |
23449 | 201 |
|
202 |
end |