src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Mon Jan 22 16:53:33 2007 +0100
+++ b/src/HOL/FunDef.thy	Mon Jan 22 17:29:43 2007 +0100
@@ -13,13 +13,11 @@
 ("Tools/function_package/fundef_lib.ML")
 ("Tools/function_package/inductive_wrap.ML")
 ("Tools/function_package/context_tree.ML")
-("Tools/function_package/fundef_prep.ML")
-("Tools/function_package/fundef_proof.ML")
+("Tools/function_package/fundef_core.ML")
 ("Tools/function_package/termination.ML")
 ("Tools/function_package/mutual.ML")
 ("Tools/function_package/pattern_split.ML")
 ("Tools/function_package/fundef_package.ML")
-(*("Tools/function_package/fundef_datatype.ML")*)
 ("Tools/function_package/auto_term.ML")
 begin
 
@@ -71,6 +69,27 @@
   done
 
 
+lemma not_accP_down:
+  assumes na: "\<not> accP R x"
+  obtains z where "R z x" and "\<not>accP R z"
+proof -
+  assume a: "\<And>z. \<lbrakk>R z x; \<not> accP R z\<rbrakk> \<Longrightarrow> thesis"
+
+  show thesis
+  proof (cases "\<forall>z. R z x \<longrightarrow> accP R z")
+    case True
+    hence "\<And>z. R z x \<Longrightarrow> accP R z" by auto
+    hence "accP R x"
+      by (rule accPI)
+    with na show thesis ..
+  next
+    case False then obtain z where "R z x" and "\<not>accP R z"
+      by auto
+    with a show thesis .
+  qed
+qed
+
+
 lemma accP_subset:
   assumes sub: "\<And>x y. R1 x y \<Longrightarrow> R2 x y"
   shows "\<And>x. accP R2 x \<Longrightarrow> accP R1 x"
@@ -195,8 +214,7 @@
 use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/inductive_wrap.ML"
 use "Tools/function_package/context_tree.ML"
-use "Tools/function_package/fundef_prep.ML"
-use "Tools/function_package/fundef_proof.ML"
+use "Tools/function_package/fundef_core.ML"
 use "Tools/function_package/termination.ML"
 use "Tools/function_package/mutual.ML"
 use "Tools/function_package/pattern_split.ML"