modified resolution proof
authorpaulson
Fri Aug 06 13:35:26 2004 +0200 (2004-08-06)
changeset 15116af3bca62444b
parent 15115 1c3be9eb4126
child 15117 b860e444c1db
modified resolution proof
src/HOL/ex/Classical.thy
     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