23449
|
1 |
(* Title: HOL/MetisExamples/set.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
|
|
5 |
Testing the metis method
|
|
6 |
*)
|
|
7 |
|
|
8 |
theory set imports Main
|
|
9 |
|
|
10 |
begin
|
|
11 |
|
|
12 |
lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
|
|
13 |
(S(x,y) | ~S(y,z) | Q(Z,Z)) &
|
|
14 |
(Q(X,y) | ~Q(y,Z) | S(X,X))";
|
|
15 |
by metis;
|
|
16 |
|
|
17 |
(*??Single-step reconstruction fails due to "assume?"*)
|
|
18 |
|
|
19 |
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
|
|
20 |
by metis
|
|
21 |
|
|
22 |
ML{*ResReconstruct.modulus := 1*}
|
|
23 |
|
|
24 |
(*multiple versions of this example*)
|
|
25 |
lemma (*equal_union: *)
|
|
26 |
"(X = Y \<union> Z) =
|
|
27 |
(Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
|
|
28 |
proof (neg_clausify)
|
|
29 |
fix x
|
|
30 |
assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
|
|
31 |
assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
|
|
32 |
assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
|
|
33 |
assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
|
|
34 |
assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
|
|
35 |
assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
|
|
36 |
have 6: "sup Y Z = X \<or> Y \<subseteq> X"
|
|
37 |
by (metis 0 sup_set_eq)
|
|
38 |
have 7: "sup Y Z = X \<or> Z \<subseteq> X"
|
|
39 |
by (metis 1 sup_set_eq)
|
|
40 |
have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
|
|
41 |
by (metis 5 sup_set_eq)
|
|
42 |
have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
|
|
43 |
by (metis 2 sup_set_eq)
|
|
44 |
have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
|
|
45 |
by (metis 3 sup_set_eq)
|
|
46 |
have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
|
|
47 |
by (metis 4 sup_set_eq)
|
|
48 |
have 12: "Z \<subseteq> X"
|
|
49 |
by (metis Un_upper2 sup_set_eq 7)
|
|
50 |
have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
|
|
51 |
by (metis 8 Un_upper2 sup_set_eq)
|
|
52 |
have 14: "Y \<subseteq> X"
|
|
53 |
by (metis Un_upper1 sup_set_eq 6)
|
|
54 |
have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
|
|
55 |
by (metis 10 12)
|
|
56 |
have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
|
|
57 |
by (metis 9 12)
|
|
58 |
have 17: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
|
|
59 |
by (metis 11 12)
|
|
60 |
have 18: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x"
|
|
61 |
by (metis 17 14)
|
|
62 |
have 19: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
|
|
63 |
by (metis 15 14)
|
|
64 |
have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
|
|
65 |
by (metis 16 14)
|
|
66 |
have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
|
|
67 |
by (metis 13 Un_upper1 sup_set_eq)
|
|
68 |
have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
|
|
69 |
by (metis equalityI 21)
|
|
70 |
have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
|
|
71 |
by (metis 22 Un_least sup_set_eq)
|
|
72 |
have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
|
|
73 |
by (metis 23 12)
|
|
74 |
have 25: "sup Y Z = X"
|
|
75 |
by (metis 24 14)
|
|
76 |
have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
|
|
77 |
by (metis Un_least sup_set_eq 25)
|
|
78 |
have 27: "Y \<subseteq> x"
|
|
79 |
by (metis 20 25)
|
|
80 |
have 28: "Z \<subseteq> x"
|
|
81 |
by (metis 19 25)
|
|
82 |
have 29: "\<not> X \<subseteq> x"
|
|
83 |
by (metis 18 25)
|
|
84 |
have 30: "X \<subseteq> x \<or> \<not> Y \<subseteq> x"
|
|
85 |
by (metis 26 28)
|
|
86 |
have 31: "X \<subseteq> x"
|
|
87 |
by (metis 30 27)
|
|
88 |
show "False"
|
|
89 |
by (metis 31 29)
|
|
90 |
qed
|
|
91 |
|
|
92 |
|
|
93 |
ML{*ResReconstruct.modulus := 2*}
|
|
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"
|
|
105 |
assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
|
|
106 |
have 6: "sup Y Z = X \<or> Y \<subseteq> X"
|
|
107 |
by (metis 0 sup_set_eq)
|
|
108 |
have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
|
|
109 |
by (metis 2 sup_set_eq)
|
|
110 |
have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
|
|
111 |
by (metis 4 sup_set_eq)
|
|
112 |
have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
|
|
113 |
by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
|
|
114 |
have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
|
|
115 |
by (metis 3 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
|
|
116 |
have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
|
|
117 |
by (metis 8 Un_upper2 sup_set_eq 1 sup_set_eq)
|
|
118 |
have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
|
|
119 |
by (metis 10 Un_upper1 sup_set_eq 6)
|
|
120 |
have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
|
|
121 |
by (metis 9 Un_upper1 sup_set_eq)
|
|
122 |
have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
|
|
123 |
by (metis equalityI 13 Un_least sup_set_eq)
|
|
124 |
have 15: "sup Y Z = X"
|
|
125 |
by (metis 14 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 6)
|
|
126 |
have 16: "Y \<subseteq> x"
|
|
127 |
by (metis 7 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 6 15)
|
|
128 |
have 17: "\<not> X \<subseteq> x"
|
|
129 |
by (metis 11 Un_upper1 sup_set_eq 6 15)
|
|
130 |
have 18: "X \<subseteq> x"
|
|
131 |
by (metis Un_least sup_set_eq 15 12 15 16)
|
|
132 |
show "False"
|
|
133 |
by (metis 18 17)
|
|
134 |
qed
|
|
135 |
|
|
136 |
ML{*ResReconstruct.modulus := 3*}
|
|
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"
|
|
148 |
assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
|
|
149 |
have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
|
|
150 |
by (metis 3 sup_set_eq)
|
|
151 |
have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
|
|
152 |
by (metis 5 sup_set_eq Un_upper2 sup_set_eq)
|
|
153 |
have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
|
|
154 |
by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
|
|
155 |
have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
|
|
156 |
by (metis 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
|
|
157 |
have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
|
|
158 |
by (metis equalityI 7 Un_upper1 sup_set_eq)
|
|
159 |
have 11: "sup Y Z = X"
|
|
160 |
by (metis 10 Un_least sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
|
|
161 |
have 12: "Z \<subseteq> x"
|
|
162 |
by (metis 9 11)
|
|
163 |
have 13: "X \<subseteq> x"
|
|
164 |
by (metis Un_least sup_set_eq 11 12 8 Un_upper1 sup_set_eq 0 sup_set_eq 11)
|
|
165 |
show "False"
|
|
166 |
by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 11)
|
|
167 |
qed
|
|
168 |
|
|
169 |
(*Example included in TPHOLs paper*)
|
|
170 |
|
|
171 |
ML{*ResReconstruct.modulus := 4*}
|
|
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"
|
|
183 |
assume 5: "\<And>A. ((\<not> Y \<subseteq> A \<or> \<not> Z \<subseteq> A) \<or> X \<subseteq> A) \<or> X = Y \<union> Z"
|
|
184 |
have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
|
|
185 |
by (metis 4 sup_set_eq)
|
|
186 |
have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
|
|
187 |
by (metis 3 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq)
|
|
188 |
have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
|
|
189 |
by (metis 7 Un_upper1 sup_set_eq 0 sup_set_eq)
|
|
190 |
have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
|
|
191 |
by (metis equalityI 5 sup_set_eq Un_upper2 sup_set_eq Un_upper1 sup_set_eq Un_least sup_set_eq)
|
|
192 |
have 10: "Y \<subseteq> x"
|
|
193 |
by (metis 2 sup_set_eq Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
|
|
194 |
have 11: "X \<subseteq> x"
|
|
195 |
by (metis Un_least sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 8 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 10)
|
|
196 |
show "False"
|
|
197 |
by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
|
|
198 |
qed
|
|
199 |
|
|
200 |
ML {*ResAtp.problem_name := "set__equal_union"*}
|
|
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 |
|
|
208 |
ML {*ResAtp.problem_name := "set__equal_inter"*}
|
|
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 |
|
|
213 |
ML {*ResAtp.problem_name := "set__fixedpoint"*}
|
|
214 |
lemma fixedpoint:
|
|
215 |
"\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
|
|
216 |
by metis
|
|
217 |
|
|
218 |
lemma fixedpoint:
|
|
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"
|
|
223 |
assume 1: "\<And>mes_oip. mes_oip = x \<or> f (g mes_oip) \<noteq> mes_oip"
|
|
224 |
assume 2: "\<And>mes_oio. g (f (xa mes_oio)) = xa mes_oio \<or> g (f mes_oio) \<noteq> mes_oio"
|
|
225 |
assume 3: "\<And>mes_oio. g (f mes_oio) \<noteq> mes_oio \<or> xa mes_oio \<noteq> mes_oio"
|
|
226 |
have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
|
|
227 |
by (metis 3 2 1 2)
|
|
228 |
show "False"
|
|
229 |
by (metis 4 0)
|
|
230 |
qed
|
|
231 |
|
|
232 |
ML {*ResAtp.problem_name := "set__singleton_example"*}
|
|
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}"
|
|
240 |
by (metis UnE Un_absorb Un_absorb2 Un_eq_Union Union_insert insertI1 insert_Diff insert_Diff_single subset_def)
|
|
241 |
--{*found by Vampire*}
|
|
242 |
|
|
243 |
lemma singleton_example_2:
|
|
244 |
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
|
|
245 |
proof (neg_clausify)
|
|
246 |
assume 0: "\<And>mes_ojD. \<not> S \<subseteq> {mes_ojD}"
|
|
247 |
assume 1: "\<And>mes_ojE. mes_ojE \<notin> S \<or> \<Union>S \<subseteq> mes_ojE"
|
|
248 |
have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S"
|
|
249 |
by (metis equalityI 1)
|
|
250 |
have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3"
|
|
251 |
by (metis Set.subsetI 2 Union_upper Set.subsetI insertCI)
|
|
252 |
show "False"
|
|
253 |
by (metis 0 3)
|
|
254 |
qed
|
|
255 |
|
|
256 |
|
|
257 |
|
|
258 |
text {*
|
|
259 |
From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
|
|
260 |
293-314.
|
|
261 |
*}
|
|
262 |
|
|
263 |
ML {*ResAtp.problem_name := "set__Bledsoe_Fung"*}
|
|
264 |
(*Notes: 1, the numbering doesn't completely agree with the paper.
|
|
265 |
2, we must rename set variables to avoid type clashes.*)
|
|
266 |
lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
|
|
267 |
"D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
|
|
268 |
"P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
|
|
269 |
"a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B"
|
|
270 |
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
|
|
271 |
"P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
|
|
272 |
"\<exists>A. a \<notin> A"
|
|
273 |
"(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
|
|
274 |
apply (metis atMost_iff);
|
|
275 |
apply (metis emptyE)
|
|
276 |
apply (metis insert_iff singletonE)
|
|
277 |
apply (metis insertCI singletonE zless_le)
|
|
278 |
apply (metis insert_iff singletonE)
|
|
279 |
apply (metis insert_iff singletonE)
|
|
280 |
apply (metis DiffE)
|
|
281 |
apply (metis Suc_eq_add_numeral_1 nat_add_commute pair_in_Id_conv)
|
|
282 |
done
|
|
283 |
|
|
284 |
end
|
|
285 |
|