author | haftmann |
Mon, 21 Sep 2009 11:01:39 +0200 | |
changeset 32685 | 29e4e567b5f4 |
parent 32519 | e9644b497e1c |
child 32864 | a226f29d4bdc |
permissions | -rw-r--r-- |
23449 | 1 |
(* Title: HOL/MetisExamples/set.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
||
4 |
Testing the metis method |
|
5 |
*) |
|
6 |
||
7 |
theory set imports Main |
|
8 |
||
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 |
15 |
(*??But metis can't prove the single-step version...*) |
|
23449 | 16 |
|
23519 | 17 |
|
23449 | 18 |
|
19 |
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" |
|
20 |
by metis |
|
21 |
||
26333
68e5eee47a45
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
paulson
parents:
26312
diff
changeset
|
22 |
declare [[sledgehammer_modulus = 1]] |
23449 | 23 |
|
28486 | 24 |
|
23449 | 25 |
(*multiple versions of this example*) |
26 |
lemma (*equal_union: *) |
|
27 |
"(X = Y \<union> Z) = |
|
28 |
(Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
|
29 |
proof (neg_clausify) |
|
30 |
fix x |
|
31 |
assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z" |
|
32 |
assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z" |
|
33 |
assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
34 |
assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
35 |
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
36 |
assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z" |
23449 | 37 |
have 6: "sup Y Z = X \<or> Y \<subseteq> X" |
32685 | 38 |
by (metis 0) |
23449 | 39 |
have 7: "sup Y Z = X \<or> Z \<subseteq> X" |
32685 | 40 |
by (metis 1) |
23449 | 41 |
have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3" |
32685 | 42 |
by (metis 5) |
23449 | 43 |
have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X" |
32685 | 44 |
by (metis 2) |
23449 | 45 |
have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X" |
32685 | 46 |
by (metis 3) |
23449 | 47 |
have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X" |
32685 | 48 |
by (metis 4) |
23449 | 49 |
have 12: "Z \<subseteq> X" |
32685 | 50 |
by (metis Un_upper2 7) |
23449 | 51 |
have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z" |
32685 | 52 |
by (metis 8 Un_upper2) |
23449 | 53 |
have 14: "Y \<subseteq> X" |
32685 | 54 |
by (metis Un_upper1 6) |
23449 | 55 |
have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X" |
56 |
by (metis 10 12) |
|
57 |
have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X" |
|
58 |
by (metis 9 12) |
|
59 |
have 17: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X" |
|
60 |
by (metis 11 12) |
|
61 |
have 18: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x" |
|
62 |
by (metis 17 14) |
|
63 |
have 19: "Z \<subseteq> x \<or> sup Y Z \<noteq> X" |
|
64 |
by (metis 15 14) |
|
65 |
have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X" |
|
66 |
by (metis 16 14) |
|
67 |
have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z" |
|
32685 | 68 |
by (metis 13 Un_upper1) |
23449 | 69 |
have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X" |
70 |
by (metis equalityI 21) |
|
71 |
have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X" |
|
32685 | 72 |
by (metis 22 Un_least) |
23449 | 73 |
have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X" |
74 |
by (metis 23 12) |
|
75 |
have 25: "sup Y Z = X" |
|
76 |
by (metis 24 14) |
|
77 |
have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3" |
|
32685 | 78 |
by (metis Un_least 25) |
23449 | 79 |
have 27: "Y \<subseteq> x" |
80 |
by (metis 20 25) |
|
81 |
have 28: "Z \<subseteq> x" |
|
82 |
by (metis 19 25) |
|
83 |
have 29: "\<not> X \<subseteq> x" |
|
84 |
by (metis 18 25) |
|
85 |
have 30: "X \<subseteq> x \<or> \<not> Y \<subseteq> x" |
|
86 |
by (metis 26 28) |
|
87 |
have 31: "X \<subseteq> x" |
|
88 |
by (metis 30 27) |
|
89 |
show "False" |
|
90 |
by (metis 31 29) |
|
91 |
qed |
|
92 |
||
26333
68e5eee47a45
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
paulson
parents:
26312
diff
changeset
|
93 |
declare [[sledgehammer_modulus = 2]] |
23449 | 94 |
|
95 |
lemma (*equal_union: *) |
|
96 |
"(X = Y \<union> Z) = |
|
97 |
(Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
|
98 |
proof (neg_clausify) |
|
99 |
fix x |
|
100 |
assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z" |
|
101 |
assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z" |
|
102 |
assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
103 |
assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
104 |
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
105 |
assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z" |
23449 | 106 |
have 6: "sup Y Z = X \<or> Y \<subseteq> X" |
32685 | 107 |
by (metis 0) |
23449 | 108 |
have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X" |
32685 | 109 |
by (metis 2) |
23449 | 110 |
have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X" |
32685 | 111 |
by (metis 4) |
23449 | 112 |
have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z" |
32685 | 113 |
by (metis 5 Un_upper2) |
23449 | 114 |
have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X" |
32685 | 115 |
by (metis 3 Un_upper2) |
23449 | 116 |
have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X" |
32685 | 117 |
by (metis 8 Un_upper2) |
23449 | 118 |
have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X" |
32685 | 119 |
by (metis 10 Un_upper1) |
23449 | 120 |
have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z" |
32685 | 121 |
by (metis 9 Un_upper1) |
23449 | 122 |
have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X" |
32685 | 123 |
by (metis equalityI 13 Un_least) |
23449 | 124 |
have 15: "sup Y Z = X" |
32685 | 125 |
by (metis 14 1 6) |
23449 | 126 |
have 16: "Y \<subseteq> x" |
32685 | 127 |
by (metis 7 Un_upper2 Un_upper1 15) |
23449 | 128 |
have 17: "\<not> X \<subseteq> x" |
32685 | 129 |
by (metis 11 Un_upper1 15) |
23449 | 130 |
have 18: "X \<subseteq> x" |
32685 | 131 |
by (metis Un_least 15 12 15 16) |
23449 | 132 |
show "False" |
133 |
by (metis 18 17) |
|
134 |
qed |
|
135 |
||
26333
68e5eee47a45
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
paulson
parents:
26312
diff
changeset
|
136 |
declare [[sledgehammer_modulus = 3]] |
23449 | 137 |
|
138 |
lemma (*equal_union: *) |
|
139 |
"(X = Y \<union> Z) = |
|
140 |
(Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
|
141 |
proof (neg_clausify) |
|
142 |
fix x |
|
143 |
assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z" |
|
144 |
assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z" |
|
145 |
assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
146 |
assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
147 |
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
148 |
assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z" |
23449 | 149 |
have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X" |
32685 | 150 |
by (metis 3) |
23449 | 151 |
have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z" |
32685 | 152 |
by (metis 5 Un_upper2) |
23449 | 153 |
have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X" |
32685 | 154 |
by (metis 2 Un_upper2) |
23449 | 155 |
have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X" |
32685 | 156 |
by (metis 6 Un_upper2 Un_upper1) |
23449 | 157 |
have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X" |
32685 | 158 |
by (metis equalityI 7 Un_upper1) |
23449 | 159 |
have 11: "sup Y Z = X" |
32685 | 160 |
by (metis 10 Un_least 1 0) |
23449 | 161 |
have 12: "Z \<subseteq> x" |
162 |
by (metis 9 11) |
|
163 |
have 13: "X \<subseteq> x" |
|
32685 | 164 |
by (metis Un_least 11 12 8 Un_upper1 11) |
23449 | 165 |
show "False" |
32685 | 166 |
by (metis 13 4 Un_upper2 Un_upper1 11) |
23449 | 167 |
qed |
168 |
||
169 |
(*Example included in TPHOLs paper*) |
|
170 |
||
26333
68e5eee47a45
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
paulson
parents:
26312
diff
changeset
|
171 |
declare [[sledgehammer_modulus = 4]] |
23449 | 172 |
|
173 |
lemma (*equal_union: *) |
|
174 |
"(X = Y \<union> Z) = |
|
175 |
(Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
|
176 |
proof (neg_clausify) |
|
177 |
fix x |
|
178 |
assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z" |
|
179 |
assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z" |
|
180 |
assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
181 |
assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
182 |
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z" |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
183 |
assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z" |
23449 | 184 |
have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X" |
32685 | 185 |
by (metis 4) |
23449 | 186 |
have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X" |
32685 | 187 |
by (metis 3 Un_upper2) |
23449 | 188 |
have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X" |
32685 | 189 |
by (metis 7 Un_upper1) |
23449 | 190 |
have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X" |
32685 | 191 |
by (metis equalityI 5 Un_upper2 Un_upper1 Un_least) |
23449 | 192 |
have 10: "Y \<subseteq> x" |
32685 | 193 |
by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0) |
23449 | 194 |
have 11: "X \<subseteq> x" |
32685 | 195 |
by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10) |
23449 | 196 |
show "False" |
32685 | 197 |
by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0) |
23449 | 198 |
qed |
199 |
||
28592 | 200 |
ML {*AtpWrapper.problem_name := "set__equal_union"*} |
23449 | 201 |
lemma (*equal_union: *) |
202 |
"(X = Y \<union> Z) = |
|
203 |
(Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
|
204 |
(*One shot proof: hand-reduced. Metis can't do the full proof any more.*) |
|
205 |
by (metis Un_least Un_upper1 Un_upper2 set_eq_subset) |
|
206 |
||
207 |
||
28592 | 208 |
ML {*AtpWrapper.problem_name := "set__equal_inter"*} |
23449 | 209 |
lemma "(X = Y \<inter> Z) = |
210 |
(X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))" |
|
211 |
by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset) |
|
212 |
||
28592 | 213 |
ML {*AtpWrapper.problem_name := "set__fixedpoint"*} |
23449 | 214 |
lemma fixedpoint: |
215 |
"\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y" |
|
216 |
by metis |
|
217 |
||
26312 | 218 |
lemma (*fixedpoint:*) |
23449 | 219 |
"\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y" |
220 |
proof (neg_clausify) |
|
221 |
fix x xa |
|
222 |
assume 0: "f (g x) = x" |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
223 |
assume 1: "\<And>y. y = x \<or> f (g y) \<noteq> y" |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
224 |
assume 2: "\<And>x. g (f (xa x)) = xa x \<or> g (f x) \<noteq> x" |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
225 |
assume 3: "\<And>x. g (f x) \<noteq> x \<or> xa x \<noteq> x" |
23449 | 226 |
have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1" |
23519 | 227 |
by (metis 3 1 2) |
23449 | 228 |
show "False" |
229 |
by (metis 4 0) |
|
230 |
qed |
|
231 |
||
28592 | 232 |
ML {*AtpWrapper.problem_name := "set__singleton_example"*} |
23449 | 233 |
lemma (*singleton_example_2:*) |
234 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
|
235 |
by (metis Set.subsetI Union_upper insertCI set_eq_subset) |
|
236 |
--{*found by SPASS*} |
|
237 |
||
238 |
lemma (*singleton_example_2:*) |
|
239 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
|
32685 | 240 |
by (metis Set.subsetI Union_upper insert_iff set_eq_subset) |
23449 | 241 |
|
242 |
lemma singleton_example_2: |
|
243 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}" |
|
244 |
proof (neg_clausify) |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
245 |
assume 0: "\<And>x. \<not> S \<subseteq> {x}" |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24855
diff
changeset
|
246 |
assume 1: "\<And>x. x \<notin> S \<or> \<Union>S \<subseteq> x" |
23449 | 247 |
have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S" |
24855 | 248 |
by (metis set_eq_subset 1) |
23449 | 249 |
have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3" |
24855 | 250 |
by (metis insert_iff Set.subsetI Union_upper 2 Set.subsetI) |
23449 | 251 |
show "False" |
24855 | 252 |
by (metis 3 0) |
23449 | 253 |
qed |
254 |
||
255 |
||
256 |
||
257 |
text {* |
|
258 |
From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages |
|
259 |
293-314. |
|
260 |
*} |
|
261 |
||
28592 | 262 |
ML {*AtpWrapper.problem_name := "set__Bledsoe_Fung"*} |
23449 | 263 |
(*Notes: 1, the numbering doesn't completely agree with the paper. |
264 |
2, we must rename set variables to avoid type clashes.*) |
|
265 |
lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))" |
|
266 |
"D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B" |
|
267 |
"P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)" |
|
268 |
"a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B" |
|
269 |
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A" |
|
270 |
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A" |
|
271 |
"\<exists>A. a \<notin> A" |
|
272 |
"(\<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" |
|
24855 | 273 |
apply (metis atMost_iff) |
23449 | 274 |
apply (metis emptyE) |
275 |
apply (metis insert_iff singletonE) |
|
276 |
apply (metis insertCI singletonE zless_le) |
|
32519 | 277 |
apply (metis Collect_def Collect_mem_eq) |
278 |
apply (metis Collect_def Collect_mem_eq) |
|
23449 | 279 |
apply (metis DiffE) |
24855 | 280 |
apply (metis pair_in_Id_conv) |
23449 | 281 |
done |
282 |
||
283 |
end |