equal
deleted
inserted
replaced
18 |
18 |
19 |
19 |
20 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" |
20 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" |
21 by metis |
21 by metis |
22 |
22 |
23 declare [[reconstruction_modulus = 1]] |
23 declare [[sledgehammer_full = true]] |
|
24 declare [[sledgehammer_modulus = 1]] |
24 |
25 |
25 (*multiple versions of this example*) |
26 (*multiple versions of this example*) |
26 lemma (*equal_union: *) |
27 lemma (*equal_union: *) |
27 "(X = Y \<union> Z) = |
28 "(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 (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" |
88 by (metis 30 27) |
89 by (metis 30 27) |
89 show "False" |
90 show "False" |
90 by (metis 31 29) |
91 by (metis 31 29) |
91 qed |
92 qed |
92 |
93 |
93 declare [[reconstruction_modulus = 2]] |
94 declare [[sledgehammer_modulus = 2]] |
94 |
95 |
95 lemma (*equal_union: *) |
96 lemma (*equal_union: *) |
96 "(X = Y \<union> Z) = |
97 "(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 (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 proof (neg_clausify) |
131 by (metis Un_least sup_set_eq 15 12 15 16) |
132 by (metis Un_least sup_set_eq 15 12 15 16) |
132 show "False" |
133 show "False" |
133 by (metis 18 17) |
134 by (metis 18 17) |
134 qed |
135 qed |
135 |
136 |
136 declare [[reconstruction_modulus = 3]] |
137 declare [[sledgehammer_modulus = 3]] |
137 |
138 |
138 lemma (*equal_union: *) |
139 lemma (*equal_union: *) |
139 "(X = Y \<union> Z) = |
140 "(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 (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 proof (neg_clausify) |
166 by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11) |
167 by (metis 13 4 sup_set_eq Un_upper2 sup_set_eq sup_set_eq Un_upper1 sup_set_eq sup_set_eq 11) |
167 qed |
168 qed |
168 |
169 |
169 (*Example included in TPHOLs paper*) |
170 (*Example included in TPHOLs paper*) |
170 |
171 |
171 declare [[reconstruction_modulus = 4]] |
172 declare [[sledgehammer_modulus = 4]] |
172 |
173 |
173 lemma (*equal_union: *) |
174 lemma (*equal_union: *) |
174 "(X = Y \<union> Z) = |
175 "(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 (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 proof (neg_clausify) |