Function package: Outside their domain functions now return "arbitrary".

--- a/src/HOL/FunDef.thy	Thu Sep 14 15:25:23 2006 +0200
+++ b/src/HOL/FunDef.thy	Thu Sep 14 15:27:08 2006 +0200
@@ -23,25 +23,42 @@
 ("Tools/function_package/auto_term.ML")
 begin
 
+
+definition
+  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
+  "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
+
+lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
+  by (simp add:theI' THE_default_def)
+
+lemma THE_default1_equality: 
+  "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
+  by (simp add:the1_equality THE_default_def)
+
+lemma THE_default_none:
+  "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
+by (simp add:THE_default_def)
+
+
 lemma fundef_ex1_existence:
-assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
 assumes ex1: "\<exists>!y. (x,y)\<in>G"
 shows "(x, f x)\<in>G"
-  by (simp only:f_def, rule theI', rule ex1)
+  by (simp only:f_def, rule THE_defaultI', rule ex1)
 
 lemma fundef_ex1_uniqueness:
-assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
 assumes ex1: "\<exists>!y. (x,y)\<in>G"
 assumes elm: "(x, h x)\<in>G"
 shows "h x = f x"
-  by (simp only:f_def, rule the1_equality[symmetric], rule ex1, rule elm)
+  by (simp only:f_def, rule THE_default1_equality[symmetric], rule ex1, rule elm)
 
 lemma fundef_ex1_iff:
-assumes f_def: "f \<equiv> \<lambda>x. THE y. (x,y)\<in>G"
+assumes f_def: "f \<equiv> \<lambda>x. THE_default d (\<lambda>y. (x,y)\<in>G)"
 assumes ex1: "\<exists>!y. (x,y)\<in>G"
 shows "((x, y)\<in>G) = (f x = y)"
-  apply (auto simp:ex1 f_def the1_equality)
-  by (rule theI', rule ex1)
+  apply (auto simp:ex1 f_def THE_default1_equality)
+  by (rule THE_defaultI', rule ex1)
 
 
 subsection {* Projections *}

--- a/src/HOL/Tools/function_package/fundef_prep.ML	Thu Sep 14 15:25:23 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Thu Sep 14 15:27:08 2006 +0200
@@ -422,7 +422,7 @@
 fun define_function fdefname (fname, mixfix) domT ranT G lthy =
     let
       val f_def = 
-          Abs ("x", domT, Const ("The", (ranT --> boolT) --> ranT) $
+          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ Const ("arbitrary", ranT) $
                                 Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))
           
       val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy

--- a/src/HOL/ex/Fundefs.thy	Thu Sep 14 15:25:23 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy	Thu Sep 14 15:27:08 2006 +0200
@@ -9,10 +9,8 @@
 imports Main
 begin
 
-
 section {* Very basic *}
 
-ML "trace_simp := false"
 
 fun fib :: "nat \<Rightarrow> nat"
 where
@@ -59,7 +57,6 @@
   "nz 0 = 0"
 | "nz (Suc x) = nz (nz x)"
 
-
 lemma nz_is_zero: -- {* A lemma we need to prove termination *}
   assumes trm: "x \<in> nz_dom"
   shows "nz x = 0"
@@ -123,7 +120,6 @@
 thm gcd2.simps
 thm gcd2.induct
 
-
 subsection {* Guards *}
 
 text {* We can reformulate the above example using guarded patterns *}