# HG changeset patch
# User wenzelm
# Date 995658774 -7200
# Node ID 8a203ae6efe39ab4ad7d6bc26c9c9e6d9b150ae3
# Parent  2328d48eeba80c2de9463b41aea6cb9f58cd549b
added "The" (definite description operator) (by Larry);

diff -r 2328d48eeba8 -r 8a203ae6efe3 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jul 20 17:49:21 2001 +0200
+++ b/src/HOL/HOL.thy	Fri Jul 20 21:52:54 2001 +0200
@@ -38,6 +38,7 @@
   (* Binders *)
 
   Eps           :: "('a => bool) => 'a"
+  The           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"           (binder "ALL " 10)
   Ex            :: "('a => bool) => bool"           (binder "EX " 10)
   Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
@@ -97,6 +98,7 @@
 syntax
   ~=            :: "['a, 'a] => bool"                    (infixl 50)
   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
+  "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
 
   (* Let expressions *)
 
@@ -115,6 +117,7 @@
 translations
   "x ~= y"                == "~ (x = y)"
   "SOME x. P"             == "Eps (%x. P)"
+  "THE x. P"              == "The (%x. P)"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
@@ -171,6 +174,7 @@
   ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
 
   someI:        "P (x::'a) ==> P (SOME x. P x)"
+  the_eq_trivial: "(THE x. x = a) = (a::'a)"
 
   impI:         "(P ==> Q) ==> P-->Q"
   mp:           "[| P-->Q;  P |] ==> Q"
diff -r 2328d48eeba8 -r 8a203ae6efe3 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Fri Jul 20 17:49:21 2001 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Jul 20 21:52:54 2001 +0200
@@ -403,6 +403,61 @@
 qed "some_sym_eq_trivial";
 
 
+
+section "THE: definite description operator";
+
+val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> (THE x. P x) = a";
+by (rtac trans 1); 
+ by (rtac (thm "the_eq_trivial") 2);
+by (res_inst_tac [("f","The")] arg_cong 1); 
+by (rtac ext 1); 
+ by (rtac iffI 1); 
+by (etac premx 1); 
+by (etac ssubst 1 THEN rtac prema 1);
+qed "the_equality";
+
+val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> P (THE x. P x)";
+by (rtac (the_equality RS ssubst) 1);
+by (REPEAT (ares_tac [prema,premx] 1));
+qed "theI";
+
+Goal "(EX! x. P x) ==> P (THE x. P x)";
+by (etac ex1E 1);
+by (etac theI 1);
+by (etac allE 1);
+by (etac mp 1);
+by (atac 1);
+qed "theI'";
+
+(*Easier to apply than theI: only one occurrence of P*)
+val [prema,premx,premq] = Goal
+     "[| P a;  !!x. P x ==> x=a;  !!x. P x ==> Q x |] \
+\     ==> Q (THE x. P x)";
+by (rtac premq 1); 
+by (rtac theI 1); 
+by (REPEAT (ares_tac [prema,premx] 1));
+qed "theI2";
+
+Goal "[| EX!x. P x; P a |] ==> (THE x. P x) = a";
+by (rtac the_equality 1);
+by  (atac 1);
+by (etac ex1E 1);
+by (etac all_dupE 1);
+by (dtac mp 1);
+by  (atac 1);
+by (etac ssubst 1);
+by (etac allE 1);
+by (etac mp 1);
+by (atac 1);
+qed "the1_equality";
+
+Goal "(THE y. x=y) = x";
+by (rtac the_equality 1);
+by (rtac refl 1);
+by (etac sym 1);
+qed "the_sym_eq_trivial";
+
+
 section "Classical intro rules for disjunction and existential quantifiers";
 
 val prems = Goal "(~Q ==> P) ==> P|Q";