author paulson Fri Aug 06 13:35:26 2004 +0200 (2004-08-06) changeset 15116 af3bca62444b parent 15115 1c3be9eb4126 child 15117 b860e444c1db
modified resolution proof
```     1.1 --- a/src/HOL/ex/Classical.thy	Fri Aug 06 12:30:31 2004 +0200
1.2 +++ b/src/HOL/ex/Classical.thy	Fri Aug 06 13:35:26 2004 +0200
1.3 @@ -786,16 +786,14 @@
1.4  lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
1.5  proof (rule ccontr, skolemize, make_clauses)
1.6    fix f g
1.7 -  assume P: "\<And>U. P U"
1.8 -     and Q: "\<And>U. \<not> Q U"
1.9 -     and PQ: "\<And>U. \<not> P (f U) \<or> Q (g U)"
1.10 -  from PQ [of a]
1.11 +  assume P: "\<And>U. \<not> P U \<Longrightarrow> False"
1.12 +     and Q: "\<And>U. Q U \<Longrightarrow> False"
1.13 +     and PQ: "\<And>U.  \<lbrakk>P (f U); \<not> Q (g U)\<rbrakk> \<Longrightarrow> False"
1.14 +  have cl4: "\<And>U. \<not> Q (g U) \<Longrightarrow> False"
1.15 +    by (blast intro: P PQ)
1.16 +       --{*Temporary: to be replaced by resolution attributes*}
1.17    show False
1.18 -  proof
1.19 -    assume "\<not> P (f a)" thus False by (rule notE [OF _ P])
1.20 -  next
1.21 -    assume "Q (g a)" thus False by (rule notE [OF Q])
1.22 -  qed
1.23 +    by (blast intro: Q cl4)
1.24  qed
1.25
1.26  end
```