Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added lemma
authornipkow
Fri, 07 Sep 2007 17:56:03 +0200
changeset 24553 9b19da7b2b08
parent 24552 bb7fdd10de9a
child 24554 e9edafca311c
added lemma
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Fri Sep 07 15:35:25 2007 +0200
+++ b/src/HOL/HOL.thy	Fri Sep 07 17:56:03 2007 +0200
@@ -708,6 +708,10 @@
   shows "Q (THE x. P x)"
 by (iprover intro: assms theI)
 
+lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
+by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
+           elim:allE impE)
+
 lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
 apply (rule the_equality)
 apply  assumption
isabelle