Preparations for making "lexicographic_order" part of "fun"

--- a/src/HOL/FunDef.thy	Tue Nov 07 11:47:57 2006 +0100
+++ b/src/HOL/FunDef.thy	Tue Nov 07 11:53:55 2006 +0100
@@ -189,11 +189,6 @@
   "rproj (Inr x) = x"
   by (auto simp:rproj_def intro: the_equality rpg.intros elim: rpg.cases)
 
-
-
-lemma P_imp_P: "P \<Longrightarrow> P" .
-
-
 use "Tools/function_package/sum_tools.ML"
 use "Tools/function_package/fundef_common.ML"
 use "Tools/function_package/fundef_lib.ML"
@@ -205,16 +200,11 @@
 use "Tools/function_package/mutual.ML"
 use "Tools/function_package/pattern_split.ML"
 use "Tools/function_package/fundef_package.ML"
+use "Tools/function_package/auto_term.ML"
 
 setup FundefPackage.setup
-
-use "Tools/function_package/fundef_datatype.ML"
-setup FundefDatatype.setup
-
-use "Tools/function_package/auto_term.ML"
 setup FundefAutoTerm.setup
 
-
 lemmas [fundef_cong] = 
   let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
 

--- a/src/HOL/List.thy	Tue Nov 07 11:47:57 2006 +0100
+++ b/src/HOL/List.thy	Tue Nov 07 11:53:55 2006 +0100
@@ -2428,8 +2428,12 @@
 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
   by auto
 
+(* install the lexicographic_order method and the "fun" command *)
 use "Tools/function_package/lexicographic_order.ML"
-setup {* LexicographicOrder.setup *}
+use "Tools/function_package/fundef_datatype.ML"
+setup LexicographicOrder.setup
+setup FundefDatatype.setup
+
 
 subsubsection{*Lifting a Relation on List Elements to the Lists*}
 

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Nov 07 11:47:57 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Nov 07 11:53:55 2006 +0100
@@ -169,6 +169,9 @@
        SOME (Method.Source (Args.src (("simp_all", []), Position.none))))
          (* FIXME avoid dynamic scoping of method name! *)
 
+fun termination_by_lexicographic_order name =
+    FundefPackage.setup_termination_proof (SOME name)
+    #> Proof.global_terminal_proof (Method.Basic (K LexicographicOrder.lexicographic_order), NONE)
 
 val setup =
     Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")]
@@ -184,14 +187,19 @@
 val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
 val statements_ow = or_list1 statement_ow
 
+
+fun fun_cmd fixes statements lthy =
+    lthy
+      |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config
+      ||> by_pat_completeness_simp
+      (*|-> termination_by_lexicographic_order*) |> snd
+
+
 val funP =
   OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
   ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
      >> (fn ((target, fixes), statements) =>
-            Toplevel.print o
-            Toplevel.local_theory target
-              (FundefPackage.add_fundef fixes statements FundefCommon.fun_config
-               #> by_pat_completeness_simp)));
+            (Toplevel.local_theory target (fun_cmd fixes statements))));
 
 val _ = OuterSyntax.add_parsers [funP];
 end

--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 11:47:57 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 07 11:53:55 2006 +0100
@@ -13,13 +13,15 @@
                       -> ((bstring * Attrib.src list) * string list) list list
                       -> FundefCommon.fundef_config
                       -> local_theory
-                      -> Proof.state
+                      -> string * Proof.state
 
     val add_fundef_i:  (string * typ option * mixfix) list
                        -> ((bstring * Attrib.src list) * term list) list list
                        -> bool
                        -> local_theory
-                       -> Proof.state
+                       -> string * Proof.state
+
+    val setup_termination_proof : string option -> local_theory -> Proof.state
 
     val cong_add: attribute
     val cong_del: attribute
@@ -105,9 +107,9 @@
 
       val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
     in
-        lthy
-          |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
-          |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd
+      (name, lthy
+         |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
+         |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
     end
 
 
@@ -132,7 +134,7 @@
     end
 
 
-fun fundef_setup_termination_proof name_opt lthy =
+fun setup_termination_proof name_opt lthy =
     let
         val name = the_default (get_last_fundef (Context.Proof lthy)) name_opt
         val data = the (get_fundef_data name (Context.Proof lthy))
@@ -190,8 +192,8 @@
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal
   ((config_parser default_config -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
      >> (fn (((config, target), fixes), statements) =>
-            Toplevel.print o
-            Toplevel.local_theory_to_proof target (add_fundef fixes statements config)));
+            Toplevel.local_theory_to_proof target (add_fundef fixes statements config #> snd)
+            #> Toplevel.print));
 
 
 
@@ -200,7 +202,7 @@
   (P.opt_locale_target -- Scan.option P.name
     >> (fn (target, name) =>
            Toplevel.print o
-           Toplevel.local_theory_to_proof target (fundef_setup_termination_proof name)));
+           Toplevel.local_theory_to_proof target (setup_termination_proof name)));
 
 
 val _ = OuterSyntax.add_parsers [functionP];