# HG changeset patch
# User krauss
# Date 1163021094 -3600
# Node ID 617fdb08abe94bc7057de2b756fcbbb7ec4d1683
# Parent  d53f76357f41c0d71e2fb88adc51f5362fd32568
added profiling code, improved handling of proof terms, generation of domain
introduction rules becomes optional (global reference FundefCommon.domintros)

diff -r d53f76357f41 -r 617fdb08abe9 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Nov 08 22:24:54 2006 +0100
@@ -12,6 +12,11 @@
 (* Theory Dependencies *)
 val acc_const_name = "FunDef.accP"
 
+val domintros = ref true;
+val profile = ref false;
+
+fun PROFILE msg = if !profile then timeap_msg msg else I
+
 fun mk_acc domT R =
     Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
 
@@ -175,14 +180,26 @@
       domintros : thm list
      }
 
+datatype fundef_context_data =
+  FundefCtxData of
+     {
+      fixes : ((string * typ) * mixfix) list,
+      spec : ((string * Attrib.src list) * term list) list list,
+      mutual: mutual_info,
 
-type fundef_spec = ((string * typ) * mixfix) list *((string * Attrib.src list) * term list) list list
-type result_with_names = fundef_mresult * mutual_info * fundef_spec
+      f : term,
+      R : term,
+      
+      psimps: thm list,
+      pinducts: thm list,
+      termination: thm
+     }
+
 
 structure FundefData = GenericDataFun
 (struct
   val name = "HOL/function_def/data";
-  type T = string * result_with_names Symtab.table
+  type T = string * fundef_context_data Symtab.table
 
   val empty = ("", Symtab.empty);
   val copy = I;
@@ -206,10 +223,11 @@
 
 
 fun add_fundef_data name fundef_data =
-    FundefData.map (fn (_,tab) => (name, Symtab.update_new (name, fundef_data) tab))
+    FundefData.map (fn (last,tab) => (name, Symtab.update_new (name, fundef_data) tab))
 
 fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name
 
+fun set_last_fundef name = FundefData.map (apfst (K name))
 fun get_last_fundef thy = fst (FundefData.get thy)
 
 val map_fundef_congs = FundefCongs.map 
diff -r d53f76357f41 -r 617fdb08abe9 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 22:24:54 2006 +0100
@@ -50,31 +50,43 @@
 fun add_simps label moreatts mutual_info fixes psimps spec lthy =
     let
       val fnames = map (fst o fst) fixes
-      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps
+
+      val (saved_spec_psimps, lthy) = fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) lthy
+      val saved_psimps = flat (map snd (flat saved_spec_psimps))
+
+      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
 
       fun add_for_f fname psimps =
           LocalTheory.note ((NameSpace.append fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
     in
-      lthy
-        |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd
-        |> fold2 add_for_f fnames psimps_by_f
+      (saved_psimps,
+       fold2 add_for_f fnames psimps_by_f lthy)
     end
 
 
 fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
     let
-        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
-        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
-        val qualify = NameSpace.append defname;
+      val Prep {f, R, ...} = data
+      val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
+      val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
+      val qualify = NameSpace.append defname
+          
+      val (((psimps', pinducts'), (_, [termination'])), lthy) = 
+          lthy
+            |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
+            ||>> PROFILE "adding pinduct" (LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
+            ||>> PROFILE "adding termination" (LocalTheory.note ((qualify "termination", []), [termination]))
+            ||> (snd o PROFILE "adding cases" (LocalTheory.note ((qualify "cases", []), [cases])))
+            ||> (snd o PROFILE "adding domintros" (LocalTheory.note ((qualify "domintros", []), domintros)))
+
+      val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
+                                  pinducts=snd pinducts', termination=termination', f=f, R=R }
+
+      
     in
       lthy
-        |> add_simps "psimps" [] mutual_info fixes psimps spec
-        |> LocalTheory.note ((qualify "domintros", []), domintros) |> snd
-        |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd
-        |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd
-        |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd
-        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* save in target *)
-        |> Context.proof_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* also save in local context *)
+        |> LocalTheory.declaration (add_fundef_data defname cdata) (* save in target *)
+        |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
     end (* FIXME: Add cases for induct and cases thm *)
 
 
@@ -117,12 +129,14 @@
 
 fun total_termination_afterqed defname data [[totality]] lthy =
     let
-        val (FundefMResult {psimps, simple_pinducts, ... }, mutual_info, (fixes, stmts)) = data
+      val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
+
+      val totality = PROFILE "closing" Drule.close_derivation totality
 
-        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
+      val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
 
-        val tsimps = map remove_domain_condition psimps
-        val tinduct = map remove_domain_condition simple_pinducts
+      val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
+      val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
 
         (* FIXME: How to generate code from (possibly) local contexts
         val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
@@ -131,8 +145,8 @@
         val qualify = NameSpace.append defname;
     in
         lthy
-          |> add_simps "simps" [] mutual_info fixes tsimps stmts
-          |> LocalTheory.note ((qualify "induct", []), tinduct) |> snd
+          |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
+          |> PROFILE "adding tinduct" (LocalTheory.note ((qualify "induct", []), tinduct)) |> snd
     end
 
 
@@ -142,8 +156,8 @@
         val data = the (get_fundef_data name (Context.Proof lthy))
                    handle Option.Option => raise ERROR ("No such function definition: " ^ name)
 
-        val (res as FundefMResult {termination, ...}, _, _) = data
-        val goal = FundefTermination.mk_total_termination_goal data
+        val FundefCtxData {termination, f, R, ...} = data
+        val goal = FundefTermination.mk_total_termination_goal f R
     in
       lthy
         |> ProofContext.note_thmss_i [(("termination",
diff -r d53f76357f41 -r 617fdb08abe9 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Wed Nov 08 22:24:54 2006 +0100
@@ -477,6 +477,8 @@
       val fvar = Free (fname, fT)
       val domT = domain_type fT
       val ranT = range_type fT
+
+                 
                             
       val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
 
@@ -485,7 +487,7 @@
 
       val Globals { x, h, ... } = globals
 
-      val clauses = map (mk_clause_context x ctxt') abstract_qglrs 
+      val clauses = PROFILE "mk_clause_context" (map (mk_clause_context x ctxt')) abstract_qglrs 
 
       val n = length abstract_qglrs
 
@@ -494,34 +496,34 @@
       fun build_tree (ClauseContext { ctxt, rhs, ...}) = 
             FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
 
-      val trees = map build_tree clauses
-      val RCss = map find_calls trees
+      val trees = PROFILE "making trees" (map build_tree) clauses
+      val RCss = PROFILE "finding calls" (map find_calls) trees
 
-      val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy
-      val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default lthy
+      val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy
+      val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
 
-      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
-      val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
+      val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss
+      val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
 
       val ((R, RIntro_thmss, R_elim), lthy) = 
-          define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss lthy
+          PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss) lthy
 
       val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", domT --> boolT), mk_acc domT R)
-      val lthy = Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)] lthy
+      val lthy = PROFILE "abbrev" (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) lthy
 
       val newthy = ProofContext.theory_of lthy
       val clauses = map (transfer_clause_ctx newthy) clauses
 
       val cert = cterm_of (ProofContext.theory_of lthy)
 
-      val xclauses = map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms RIntro_thmss
+      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
 
-      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
-      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
+      val complete = PROFILE "mk_compl" (mk_completeness globals clauses) abstract_qglrs |> cert |> assume
+      val compat = PROFILE "mk_compat" (mk_compat_proof_obligations domT ranT fvar f) abstract_qglrs |> map (cert #> assume)
 
       val compat_store = store_compat_thms n compat
 
-      val (goal, goalI, ex1_iff, values) = prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim f_defthm
+      val (goal, goalI, ex1_iff, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
     in
         (Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f,
          lthy)
diff -r d53f76357f41 -r 617fdb08abe9 src/HOL/Tools/function_package/fundef_proof.ML
--- a/src/HOL/Tools/function_package/fundef_proof.ML	Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_proof.ML	Wed Nov 08 22:24:54 2006 +0100
@@ -43,11 +43,11 @@
 
 fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
     let
-  val Globals {domT, z, ...} = globals
-
-  val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
-  val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
-  val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
+      val Globals {domT, z, ...} = globals
+                                   
+      val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
+      val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
+      val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
     in
       ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
         |> (fn it => it COMP graph_is_function)
@@ -64,29 +64,29 @@
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
     let
-  val Globals {domT, x, z, a, P, D, ...} = globals
-        val acc_R = mk_acc domT R
-
-  val x_D = assume (cterm_of thy (Trueprop (D $ x)))
-  val a_D = cterm_of thy (Trueprop (D $ a))
-
-  val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
-
-  val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
-      mk_forall x
-          (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
-                  Logic.mk_implies (Trueprop (R $ z $ x),
-                  Trueprop (D $ z)))))
-          |> cterm_of thy
-
-
+      val Globals {domT, x, z, a, P, D, ...} = globals
+      val acc_R = mk_acc domT R
+                  
+      val x_D = assume (cterm_of thy (Trueprop (D $ x)))
+      val a_D = cterm_of thy (Trueprop (D $ a))
+                
+      val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
+                     
+      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
+                    mk_forall x
+                    (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
+                                                    Logic.mk_implies (Trueprop (R $ z $ x),
+                                                                      Trueprop (D $ z)))))
+                    |> cterm_of thy
+                    
+                    
   (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
-  val ihyp = all domT $ Abs ("z", domT, 
-           implies $ Trueprop (R $ Bound 0 $ x)
+      val ihyp = all domT $ Abs ("z", domT, 
+               implies $ Trueprop (R $ Bound 0 $ x)
              $ Trueprop (P $ Bound 0))
            |> cterm_of thy
 
-  val aihyp = assume ihyp
+      val aihyp = assume ihyp
 
   fun prove_case clause =
       let
@@ -188,6 +188,9 @@
     end
 
 
+fun maybe_mk_domain_intro thy =
+    if !FundefCommon.domintros then mk_domain_intro thy
+    else K (K (K (K refl)))
 
 
 fun mk_nest_term_case thy globals R' ihyp clause =
@@ -296,34 +299,22 @@
     let
       val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
                                                                             
-      val _ = Output.debug "Closing Derivation"
-              
-      val provedgoal = Drule.close_derivation provedgoal
+      val provedgoal = PROFILE "Closing Derivation" Drule.close_derivation provedgoal
                        
-      val _ = Output.debug "Getting function theorem"
-              
-      val graph_is_function = (provedgoal COMP conjunctionD1)
-                                |> forall_elim_vars 0
+      val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal
                               
-      val _ = Output.debug "Getting cases"
-              
-      val complete_thm = provedgoal COMP conjunctionD2
-                         
-      val _ = Output.debug "Making f_iff"
-              
-      val f_iff = (graph_is_function RS ex1_iff) 
+      val complete_thm = PROFILE "Getting cases" (curry op COMP provedgoal) conjunctionD2
+
+      val f_iff = PROFILE "Making f_iff" (curry op RS graph_is_function) ex1_iff
                   
-      val _ = Output.debug "Proving simplification rules"
-      val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
+      val psimps = PROFILE "Proving simplification rules" (map2 (mk_psimp thy globals R f_iff graph_is_function)) clauses values
                     
-      val _ = Output.debug "Proving partial induction rule"
-      val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
+      val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule" 
+                                             (mk_partial_induct_rule thy globals R complete_thm) clauses
                                              
-      val _ = Output.debug "Proving nested termination rule"
-      val total_intro = mk_nest_term_rule thy globals R R_cases clauses
+      val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule thy globals R R_cases) clauses
                         
-      val _ = Output.debug "Proving domain introduction rules"
-      val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
+      val dom_intros = PROFILE "Proving domain introduction rules" (map (maybe_mk_domain_intro thy globals R R_cases)) clauses
     in 
       FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
                     psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
diff -r d53f76357f41 -r 617fdb08abe9 src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Wed Nov 08 22:24:54 2006 +0100
@@ -337,10 +337,9 @@
       fun mk_mpsimp fqgar sum_psimp =
           in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
           
-      val mpsimps = map2 mk_mpsimp fqgars psimps
-                    
-      val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
-      val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
+      val mpsimps = PROFILE "making mpsimps" (map2 mk_mpsimp fqgars) psimps
+      val minducts = PROFILE "making mpinduct" (mutual_induct_rules thy simple_pinduct all_f_defs) m
+      val termination = PROFILE "making mtermination" (full_simplify (HOL_basic_ss addsimps all_f_defs)) total_intro
     in
       FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
                       psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
diff -r d53f76357f41 -r 617fdb08abe9 src/HOL/Tools/function_package/termination.ML
--- a/src/HOL/Tools/function_package/termination.ML	Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/termination.ML	Wed Nov 08 22:24:54 2006 +0100
@@ -9,8 +9,8 @@
 
 signature FUNDEF_TERMINATION =
 sig
-  val mk_total_termination_goal : FundefCommon.result_with_names -> term
-  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
+  val mk_total_termination_goal : term -> term -> term
+(*  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*)
 end
 
 structure FundefTermination : FUNDEF_TERMINATION =
@@ -21,7 +21,7 @@
 open FundefCommon
 open FundefAbbrev
      
-fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
+fun mk_total_termination_goal f R =
     let
       val domT = domain_type (fastype_of f)
       val x = Free ("x", domT)
@@ -29,6 +29,7 @@
       mk_forall x (Trueprop (mk_acc domT R $ x))
     end
     
+(*
 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
     let
       val domT = domain_type (fastype_of f)
@@ -55,7 +56,7 @@
     in
       (subs, dcl)
     end
-
+*)
 end