function package: more standard names for structures and files
authorkrauss
Fri Oct 23 16:22:10 2009 +0200 (2009-10-23)
changeset 33099b8cdd3d73022
parent 33098 3e9ae9032273
child 33100 acc2bd3934ba
function package: more standard names for structures and files
src/HOL/FunDef.thy
src/HOL/IsaMakefile
src/HOL/Tools/Function/auto_term.ML
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/decompose.ML
src/HOL/Tools/Function/descent.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/fundef.ML
src/HOL/Tools/Function/fundef_common.ML
src/HOL/Tools/Function/fundef_core.ML
src/HOL/Tools/Function/fundef_lib.ML
src/HOL/Tools/Function/induction_scheme.ML
src/HOL/Tools/Function/inductive_wrap.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/pat_completeness.ML
src/HOL/Tools/Function/pattern_split.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/scnp_solve.ML
src/HOL/Tools/Function/termination.ML
     1.1 --- a/src/HOL/FunDef.thy	Fri Oct 23 15:33:19 2009 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Fri Oct 23 16:22:10 2009 +0200
     1.3 @@ -9,15 +9,15 @@
     1.4  uses
     1.5    "Tools/prop_logic.ML"
     1.6    "Tools/sat_solver.ML"
     1.7 -  ("Tools/Function/fundef_lib.ML")
     1.8 -  ("Tools/Function/fundef_common.ML")
     1.9 +  ("Tools/Function/function_lib.ML")
    1.10 +  ("Tools/Function/function_common.ML")
    1.11    ("Tools/Function/inductive_wrap.ML")
    1.12    ("Tools/Function/context_tree.ML")
    1.13 -  ("Tools/Function/fundef_core.ML")
    1.14 +  ("Tools/Function/function_core.ML")
    1.15    ("Tools/Function/sum_tree.ML")
    1.16    ("Tools/Function/mutual.ML")
    1.17    ("Tools/Function/pattern_split.ML")
    1.18 -  ("Tools/Function/fundef.ML")
    1.19 +  ("Tools/Function/function.ML")
    1.20    ("Tools/Function/auto_term.ML")
    1.21    ("Tools/Function/measure_functions.ML")
    1.22    ("Tools/Function/lexicographic_order.ML")
    1.23 @@ -104,25 +104,25 @@
    1.24    "wf R \<Longrightarrow> wfP (in_rel R)"
    1.25    by (simp add: wfP_def)
    1.26  
    1.27 -use "Tools/Function/fundef_lib.ML"
    1.28 -use "Tools/Function/fundef_common.ML"
    1.29 +use "Tools/Function/function_lib.ML"
    1.30 +use "Tools/Function/function_common.ML"
    1.31  use "Tools/Function/inductive_wrap.ML"
    1.32  use "Tools/Function/context_tree.ML"
    1.33 -use "Tools/Function/fundef_core.ML"
    1.34 +use "Tools/Function/function_core.ML"
    1.35  use "Tools/Function/sum_tree.ML"
    1.36  use "Tools/Function/mutual.ML"
    1.37  use "Tools/Function/pattern_split.ML"
    1.38  use "Tools/Function/auto_term.ML"
    1.39 -use "Tools/Function/fundef.ML"
    1.40 +use "Tools/Function/function.ML"
    1.41  use "Tools/Function/pat_completeness.ML"
    1.42  use "Tools/Function/fun.ML"
    1.43  use "Tools/Function/induction_scheme.ML"
    1.44  
    1.45  setup {* 
    1.46 -  Fundef.setup
    1.47 +  Function.setup
    1.48    #> Pat_Completeness.setup
    1.49    #> Function_Fun.setup
    1.50 -  #> InductionScheme.setup
    1.51 +  #> Induction_Scheme.setup
    1.52  *}
    1.53  
    1.54  subsection {* Measure Functions *}
    1.55 @@ -142,7 +142,7 @@
    1.56  by (rule is_measure_trivial)
    1.57  
    1.58  use "Tools/Function/lexicographic_order.ML"
    1.59 -setup LexicographicOrder.setup 
    1.60 +setup Lexicographic_Order.setup 
    1.61  
    1.62  
    1.63  subsection {* Congruence Rules *}
    1.64 @@ -320,7 +320,7 @@
    1.65  
    1.66  ML_val -- "setup inactive"
    1.67  {*
    1.68 -  Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp 
    1.69 +  Context.theory_map (Function_Common.set_termination_prover (ScnpReconstruct.decomp_scnp 
    1.70    [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
    1.71  *}
    1.72  
     2.1 --- a/src/HOL/IsaMakefile	Fri Oct 23 15:33:19 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Oct 23 16:22:10 2009 +0200
     2.3 @@ -160,10 +160,10 @@
     2.4    Tools/Function/context_tree.ML \
     2.5    Tools/Function/decompose.ML \
     2.6    Tools/Function/descent.ML \
     2.7 -  Tools/Function/fundef_common.ML \
     2.8 -  Tools/Function/fundef_core.ML \
     2.9 -  Tools/Function/fundef_lib.ML \
    2.10 -  Tools/Function/fundef.ML \
    2.11 +  Tools/Function/function_common.ML \
    2.12 +  Tools/Function/function_core.ML \
    2.13 +  Tools/Function/function_lib.ML \
    2.14 +  Tools/Function/function.ML \
    2.15    Tools/Function/fun.ML \
    2.16    Tools/Function/induction_scheme.ML \
    2.17    Tools/Function/inductive_wrap.ML \
     3.1 --- a/src/HOL/Tools/Function/auto_term.ML	Fri Oct 23 15:33:19 2009 +0200
     3.2 +++ b/src/HOL/Tools/Function/auto_term.ML	Fri Oct 23 16:22:10 2009 +0200
     3.3 @@ -5,13 +5,13 @@
     3.4  Method "relation" to commence a termination proof using a user-specified relation.
     3.5  *)
     3.6  
     3.7 -signature FUNDEF_RELATION =
     3.8 +signature FUNCTION_RELATION =
     3.9  sig
    3.10    val relation_tac: Proof.context -> term -> int -> tactic
    3.11    val setup: theory -> theory
    3.12  end
    3.13  
    3.14 -structure FundefRelation : FUNDEF_RELATION =
    3.15 +structure Function_Relation : FUNCTION_RELATION =
    3.16  struct
    3.17  
    3.18  fun inst_thm ctxt rel st =
    3.19 @@ -25,7 +25,7 @@
    3.20      end
    3.21  
    3.22  fun relation_tac ctxt rel i = 
    3.23 -    TRY (FundefCommon.apply_termination_rule ctxt i)
    3.24 +    TRY (Function_Common.apply_termination_rule ctxt i)
    3.25      THEN PRIMITIVE (inst_thm ctxt rel)
    3.26  
    3.27  val setup =
     4.1 --- a/src/HOL/Tools/Function/context_tree.ML	Fri Oct 23 15:33:19 2009 +0200
     4.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Fri Oct 23 16:22:10 2009 +0200
     4.3 @@ -5,15 +5,15 @@
     4.4  Builds and traverses trees of nested contexts along a term.
     4.5  *)
     4.6  
     4.7 -signature FUNDEF_CTXTREE =
     4.8 +signature FUNCTION_CTXTREE =
     4.9  sig
    4.10      type ctxt = (string * typ) list * thm list (* poor man's contexts: fixes + assumes *)
    4.11      type ctx_tree
    4.12  
    4.13      (* FIXME: This interface is a mess and needs to be cleaned up! *)
    4.14 -    val get_fundef_congs : Proof.context -> thm list
    4.15 -    val add_fundef_cong : thm -> Context.generic -> Context.generic
    4.16 -    val map_fundef_congs : (thm list -> thm list) -> Context.generic -> Context.generic
    4.17 +    val get_function_congs : Proof.context -> thm list
    4.18 +    val add_function_cong : thm -> Context.generic -> Context.generic
    4.19 +    val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
    4.20  
    4.21      val cong_add: attribute
    4.22      val cong_del: attribute
    4.23 @@ -36,15 +36,15 @@
    4.24      val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> ctx_tree -> thm * (thm * thm) list
    4.25  end
    4.26  
    4.27 -structure FundefCtxTree : FUNDEF_CTXTREE =
    4.28 +structure Function_Ctx_Tree : FUNCTION_CTXTREE =
    4.29  struct
    4.30  
    4.31  type ctxt = (string * typ) list * thm list
    4.32  
    4.33 -open FundefCommon
    4.34 -open FundefLib
    4.35 +open Function_Common
    4.36 +open Function_Lib
    4.37  
    4.38 -structure FundefCongs = GenericDataFun
    4.39 +structure FunctionCongs = GenericDataFun
    4.40  (
    4.41    type T = thm list
    4.42    val empty = []
    4.43 @@ -52,14 +52,14 @@
    4.44    fun merge _ = Thm.merge_thms
    4.45  );
    4.46  
    4.47 -val get_fundef_congs = FundefCongs.get o Context.Proof
    4.48 -val map_fundef_congs = FundefCongs.map
    4.49 -val add_fundef_cong = FundefCongs.map o Thm.add_thm
    4.50 +val get_function_congs = FunctionCongs.get o Context.Proof
    4.51 +val map_function_congs = FunctionCongs.map
    4.52 +val add_function_cong = FunctionCongs.map o Thm.add_thm
    4.53  
    4.54  (* congruence rules *)
    4.55  
    4.56 -val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq);
    4.57 -val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq);
    4.58 +val cong_add = Thm.declaration_attribute (map_function_congs o Thm.add_thm o safe_mk_meta_eq);
    4.59 +val cong_del = Thm.declaration_attribute (map_function_congs o Thm.del_thm o safe_mk_meta_eq);
    4.60  
    4.61  
    4.62  type depgraph = int IntGraph.T
    4.63 @@ -128,7 +128,7 @@
    4.64  
    4.65  fun mk_tree fvar h ctxt t =
    4.66      let 
    4.67 -      val congs = get_fundef_congs ctxt
    4.68 +      val congs = get_function_congs ctxt
    4.69        val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs) (* FIXME: Save in theory *)
    4.70  
    4.71        fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
     5.1 --- a/src/HOL/Tools/Function/decompose.ML	Fri Oct 23 15:33:19 2009 +0200
     5.2 +++ b/src/HOL/Tools/Function/decompose.ML	Fri Oct 23 16:22:10 2009 +0200
     5.3 @@ -33,8 +33,8 @@
     5.4                                        Const (@{const_name Set.empty}, fastype_of c1))
     5.5                         |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
     5.6  
     5.7 -            val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of
     5.8 -                          FundefLib.Solved thm => SOME thm
     5.9 +            val chain = case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
    5.10 +                          Function_Lib.Solved thm => SOME thm
    5.11                          | _ => NONE
    5.12            in
    5.13              Termination.note_chain c1 c2 chain D
    5.14 @@ -62,7 +62,7 @@
    5.15     let
    5.16       val is = map (fn c => find_index (curry op aconv c) cs') cs
    5.17     in
    5.18 -     CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i
    5.19 +     CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv is))) i
    5.20     end)
    5.21  
    5.22  
     6.1 --- a/src/HOL/Tools/Function/descent.ML	Fri Oct 23 15:33:19 2009 +0200
     6.2 +++ b/src/HOL/Tools/Function/descent.ML	Fri Oct 23 16:22:10 2009 +0200
     6.3 @@ -35,7 +35,7 @@
     6.4                 (measures_of p) (measures_of q) D
     6.5        end
     6.6    in
     6.7 -    cont (FundefCommon.PROFILE "deriving descents" (fold derive cs) D) i
     6.8 +    cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i
     6.9    end)
    6.10  
    6.11  val derive_diag = gen_descent true
     7.1 --- a/src/HOL/Tools/Function/fun.ML	Fri Oct 23 15:33:19 2009 +0200
     7.2 +++ b/src/HOL/Tools/Function/fun.ML	Fri Oct 23 16:22:10 2009 +0200
     7.3 @@ -7,10 +7,10 @@
     7.4  
     7.5  signature FUNCTION_FUN =
     7.6  sig
     7.7 -    val add_fun : FundefCommon.fundef_config ->
     7.8 +    val add_fun : Function_Common.function_config ->
     7.9        (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
    7.10        bool -> local_theory -> Proof.context
    7.11 -    val add_fun_cmd : FundefCommon.fundef_config ->
    7.12 +    val add_fun_cmd : Function_Common.function_config ->
    7.13        (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
    7.14        bool -> local_theory -> Proof.context
    7.15  
    7.16 @@ -20,8 +20,8 @@
    7.17  structure Function_Fun : FUNCTION_FUN =
    7.18  struct
    7.19  
    7.20 -open FundefLib
    7.21 -open FundefCommon
    7.22 +open Function_Lib
    7.23 +open Function_Common
    7.24  
    7.25  
    7.26  fun check_pats ctxt geq =
    7.27 @@ -62,7 +62,7 @@
    7.28         SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
    7.29  
    7.30  fun termination_by method int =
    7.31 -    Fundef.termination_proof NONE
    7.32 +    Function.termination_proof NONE
    7.33      #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
    7.34  
    7.35  fun mk_catchall fixes arity_of =
    7.36 @@ -104,7 +104,7 @@
    7.37      end
    7.38  
    7.39  
    7.40 -fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec =
    7.41 +fun sequential_preproc (config as FunctionConfig {sequential, ...}) ctxt fixes spec =
    7.42        if sequential then
    7.43          let
    7.44            val (bnds, eqss) = split_list spec
    7.45 @@ -118,7 +118,7 @@
    7.46            val compleqs = add_catchall ctxt fixes feqs   (* Completion *)
    7.47  
    7.48            val spliteqs = warn_if_redundant ctxt feqs
    7.49 -                           (FundefSplit.split_all_equations ctxt compleqs)
    7.50 +                           (Function_Split.split_all_equations ctxt compleqs)
    7.51  
    7.52            fun restore_spec thms =
    7.53                bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
    7.54 @@ -141,13 +141,13 @@
    7.55            (flat spliteqs, restore_spec, sort, case_names)
    7.56          end
    7.57        else
    7.58 -        FundefCommon.empty_preproc check_defs config ctxt fixes spec
    7.59 +        Function_Common.empty_preproc check_defs config ctxt fixes spec
    7.60  
    7.61  val setup =
    7.62 -  Context.theory_map (FundefCommon.set_preproc sequential_preproc)
    7.63 +  Context.theory_map (Function_Common.set_preproc sequential_preproc)
    7.64  
    7.65  
    7.66 -val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
    7.67 +val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
    7.68                                  domintros=false, tailrec=false }
    7.69  
    7.70  fun gen_fun add config fixes statements int lthy =
    7.71 @@ -158,11 +158,11 @@
    7.72        |> by_pat_completeness_auto int
    7.73        |> LocalTheory.restore
    7.74        |> LocalTheory.set_group group
    7.75 -      |> termination_by (FundefCommon.get_termination_prover lthy) int
    7.76 +      |> termination_by (Function_Common.get_termination_prover lthy) int
    7.77    end;
    7.78  
    7.79 -val add_fun = gen_fun Fundef.add_fundef
    7.80 -val add_fun_cmd = gen_fun Fundef.add_fundef_cmd
    7.81 +val add_fun = gen_fun Function.add_function
    7.82 +val add_fun_cmd = gen_fun Function.add_function_cmd
    7.83  
    7.84  
    7.85  
    7.86 @@ -170,7 +170,7 @@
    7.87  
    7.88  val _ =
    7.89    OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
    7.90 -  (fundef_parser fun_config
    7.91 +  (function_parser fun_config
    7.92       >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
    7.93  
    7.94  end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/Function/function.ML	Fri Oct 23 16:22:10 2009 +0200
     8.3 @@ -0,0 +1,226 @@
     8.4 +(*  Title:      HOL/Tools/Function/fundef.ML
     8.5 +    Author:     Alexander Krauss, TU Muenchen
     8.6 +
     8.7 +A package for general recursive function definitions.
     8.8 +Isar commands.
     8.9 +*)
    8.10 +
    8.11 +signature FUNCTION =
    8.12 +sig
    8.13 +    val add_function :  (binding * typ option * mixfix) list
    8.14 +                       -> (Attrib.binding * term) list
    8.15 +                       -> Function_Common.function_config
    8.16 +                       -> local_theory
    8.17 +                       -> Proof.state
    8.18 +    val add_function_cmd :  (binding * string option * mixfix) list
    8.19 +                      -> (Attrib.binding * string) list
    8.20 +                      -> Function_Common.function_config
    8.21 +                      -> local_theory
    8.22 +                      -> Proof.state
    8.23 +
    8.24 +    val termination_proof : term option -> local_theory -> Proof.state
    8.25 +    val termination_proof_cmd : string option -> local_theory -> Proof.state
    8.26 +    val termination : term option -> local_theory -> Proof.state
    8.27 +    val termination_cmd : string option -> local_theory -> Proof.state
    8.28 +
    8.29 +    val setup : theory -> theory
    8.30 +    val get_congs : Proof.context -> thm list
    8.31 +end
    8.32 +
    8.33 +
    8.34 +structure Function : FUNCTION =
    8.35 +struct
    8.36 +
    8.37 +open Function_Lib
    8.38 +open Function_Common
    8.39 +
    8.40 +val simp_attribs = map (Attrib.internal o K)
    8.41 +    [Simplifier.simp_add,
    8.42 +     Code.add_default_eqn_attribute,
    8.43 +     Nitpick_Simps.add,
    8.44 +     Quickcheck_RecFun_Simps.add]
    8.45 +
    8.46 +val psimp_attribs = map (Attrib.internal o K)
    8.47 +    [Simplifier.simp_add,
    8.48 +     Nitpick_Psimps.add]
    8.49 +
    8.50 +fun note_theorem ((name, atts), ths) =
    8.51 +  LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
    8.52 +
    8.53 +fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
    8.54 +
    8.55 +fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
    8.56 +    let
    8.57 +      val spec = post simps
    8.58 +                   |> map (apfst (apsnd (fn ats => moreatts @ ats)))
    8.59 +                   |> map (apfst (apfst extra_qualify))
    8.60 +
    8.61 +      val (saved_spec_simps, lthy) =
    8.62 +        fold_map (LocalTheory.note Thm.generatedK) spec lthy
    8.63 +
    8.64 +      val saved_simps = maps snd saved_spec_simps
    8.65 +      val simps_by_f = sort saved_simps
    8.66 +
    8.67 +      fun add_for_f fname simps =
    8.68 +        note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
    8.69 +    in
    8.70 +      (saved_simps,
    8.71 +       fold2 add_for_f fnames simps_by_f lthy)
    8.72 +    end
    8.73 +
    8.74 +fun gen_add_function is_external prep default_constraint fixspec eqns config lthy =
    8.75 +    let
    8.76 +      val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
    8.77 +      val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
    8.78 +      val fixes = map (apfst (apfst Binding.name_of)) fixes0;
    8.79 +      val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
    8.80 +      val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
    8.81 +
    8.82 +      val defname = mk_defname fixes
    8.83 +
    8.84 +      val ((goalstate, cont), lthy) =
    8.85 +          Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
    8.86 +
    8.87 +      fun afterqed [[proof]] lthy =
    8.88 +        let
    8.89 +          val FunctionResult {fs, R, psimps, trsimps,  simple_pinducts, termination,
    8.90 +                            domintros, cases, ...} =
    8.91 +          cont (Thm.close_derivation proof)
    8.92 +
    8.93 +          val fnames = map (fst o fst) fixes
    8.94 +          val qualify = Long_Name.qualify defname
    8.95 +          val addsmps = add_simps fnames post sort_cont
    8.96 +
    8.97 +          val (((psimps', pinducts'), (_, [termination'])), lthy) =
    8.98 +            lthy
    8.99 +            |> addsmps (Binding.qualify false "partial") "psimps"
   8.100 +                 psimp_attribs psimps
   8.101 +            ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
   8.102 +            ||>> note_theorem ((qualify "pinduct",
   8.103 +                   [Attrib.internal (K (RuleCases.case_names cnames)),
   8.104 +                    Attrib.internal (K (RuleCases.consumes 1)),
   8.105 +                    Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
   8.106 +            ||>> note_theorem ((qualify "termination", []), [termination])
   8.107 +            ||> (snd o note_theorem ((qualify "cases",
   8.108 +                   [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
   8.109 +            ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
   8.110 +
   8.111 +          val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
   8.112 +                                      pinducts=snd pinducts', termination=termination',
   8.113 +                                      fs=fs, R=R, defname=defname }
   8.114 +          val _ =
   8.115 +            if not is_external then ()
   8.116 +            else Specification.print_consts lthy (K false) (map fst fixes)
   8.117 +        in
   8.118 +          lthy
   8.119 +          |> LocalTheory.declaration (add_function_data o morph_function_data cdata)
   8.120 +        end
   8.121 +    in
   8.122 +      lthy
   8.123 +        |> is_external ? LocalTheory.set_group (serial_string ())
   8.124 +        |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
   8.125 +        |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
   8.126 +    end
   8.127 +
   8.128 +val add_function = gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
   8.129 +val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
   8.130 +
   8.131 +fun gen_termination_proof prep_term raw_term_opt lthy =
   8.132 +    let
   8.133 +      val term_opt = Option.map (prep_term lthy) raw_term_opt
   8.134 +      val data = the (case term_opt of
   8.135 +                        SOME t => (import_function_data t lthy
   8.136 +                          handle Option.Option =>
   8.137 +                            error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
   8.138 +                      | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))
   8.139 +
   8.140 +        val FunctionCtxData { termination, R, add_simps, case_names, psimps,
   8.141 +                            pinducts, defname, ...} = data
   8.142 +        val domT = domain_type (fastype_of R)
   8.143 +        val goal = HOLogic.mk_Trueprop
   8.144 +                     (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
   8.145 +        fun afterqed [[totality]] lthy =
   8.146 +          let
   8.147 +            val totality = Thm.close_derivation totality
   8.148 +            val remove_domain_condition =
   8.149 +              full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
   8.150 +            val tsimps = map remove_domain_condition psimps
   8.151 +            val tinduct = map remove_domain_condition pinducts
   8.152 +            val qualify = Long_Name.qualify defname;
   8.153 +          in
   8.154 +            lthy
   8.155 +            |> add_simps I "simps" simp_attribs tsimps |> snd
   8.156 +            |> note_theorem
   8.157 +               ((qualify "induct",
   8.158 +                 [Attrib.internal (K (RuleCases.case_names case_names))]),
   8.159 +                tinduct) |> snd
   8.160 +          end
   8.161 +    in
   8.162 +      lthy
   8.163 +      |> ProofContext.note_thmss ""
   8.164 +         [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
   8.165 +      |> ProofContext.note_thmss ""
   8.166 +         [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
   8.167 +      |> ProofContext.note_thmss ""
   8.168 +         [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
   8.169 +           [([Goal.norm_result termination], [])])] |> snd
   8.170 +      |> Proof.theorem_i NONE afterqed [[(goal, [])]]
   8.171 +    end
   8.172 +
   8.173 +val termination_proof = gen_termination_proof Syntax.check_term;
   8.174 +val termination_proof_cmd = gen_termination_proof Syntax.read_term;
   8.175 +
   8.176 +fun termination term_opt lthy =
   8.177 +  lthy
   8.178 +  |> LocalTheory.set_group (serial_string ())
   8.179 +  |> termination_proof term_opt;
   8.180 +
   8.181 +fun termination_cmd term_opt lthy =
   8.182 +  lthy
   8.183 +  |> LocalTheory.set_group (serial_string ())
   8.184 +  |> termination_proof_cmd term_opt;
   8.185 +
   8.186 +
   8.187 +(* Datatype hook to declare datatype congs as "function_congs" *)
   8.188 +
   8.189 +
   8.190 +fun add_case_cong n thy =
   8.191 +    Context.theory_map (Function_Ctx_Tree.map_function_congs (Thm.add_thm
   8.192 +                          (Datatype.the_info thy n
   8.193 +                           |> #case_cong
   8.194 +                           |> safe_mk_meta_eq)))
   8.195 +                       thy
   8.196 +
   8.197 +val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
   8.198 +
   8.199 +
   8.200 +(* setup *)
   8.201 +
   8.202 +val setup =
   8.203 +  Attrib.setup @{binding fundef_cong}
   8.204 +    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
   8.205 +    "declaration of congruence rule for function definitions"
   8.206 +  #> setup_case_cong
   8.207 +  #> Function_Relation.setup
   8.208 +  #> Function_Common.Termination_Simps.setup
   8.209 +
   8.210 +val get_congs = Function_Ctx_Tree.get_function_congs
   8.211 +
   8.212 +
   8.213 +(* outer syntax *)
   8.214 +
   8.215 +local structure P = OuterParse and K = OuterKeyword in
   8.216 +
   8.217 +val _ =
   8.218 +  OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
   8.219 +  (function_parser default_config
   8.220 +     >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config));
   8.221 +
   8.222 +val _ =
   8.223 +  OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
   8.224 +  (Scan.option P.term >> termination_cmd);
   8.225 +
   8.226 +end;
   8.227 +
   8.228 +
   8.229 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/Function/function_common.ML	Fri Oct 23 16:22:10 2009 +0200
     9.3 @@ -0,0 +1,343 @@
     9.4 +(*  Title:      HOL/Tools/Function/fundef_common.ML
     9.5 +    Author:     Alexander Krauss, TU Muenchen
     9.6 +
     9.7 +A package for general recursive function definitions. 
     9.8 +Common definitions and other infrastructure.
     9.9 +*)
    9.10 +
    9.11 +structure Function_Common =
    9.12 +struct
    9.13 +
    9.14 +local open Function_Lib in
    9.15 +
    9.16 +(* Profiling *)
    9.17 +val profile = Unsynchronized.ref false;
    9.18 +
    9.19 +fun PROFILE msg = if !profile then timeap_msg msg else I
    9.20 +
    9.21 +
    9.22 +val acc_const_name = @{const_name accp}
    9.23 +fun mk_acc domT R =
    9.24 +    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
    9.25 +
    9.26 +val function_name = suffix "C"
    9.27 +val graph_name = suffix "_graph"
    9.28 +val rel_name = suffix "_rel"
    9.29 +val dom_name = suffix "_dom"
    9.30 +
    9.31 +(* Termination rules *)
    9.32 +
    9.33 +structure TerminationRule = GenericDataFun
    9.34 +(
    9.35 +  type T = thm list
    9.36 +  val empty = []
    9.37 +  val extend = I
    9.38 +  fun merge _ = Thm.merge_thms
    9.39 +);
    9.40 +
    9.41 +val get_termination_rules = TerminationRule.get
    9.42 +val store_termination_rule = TerminationRule.map o cons
    9.43 +val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
    9.44 +
    9.45 +
    9.46 +(* Function definition result data *)
    9.47 +
    9.48 +datatype function_result =
    9.49 +  FunctionResult of
    9.50 +     {
    9.51 +      fs: term list,
    9.52 +      G: term,
    9.53 +      R: term,
    9.54 +
    9.55 +      psimps : thm list, 
    9.56 +      trsimps : thm list option, 
    9.57 +
    9.58 +      simple_pinducts : thm list, 
    9.59 +      cases : thm,
    9.60 +      termination : thm,
    9.61 +      domintros : thm list option
    9.62 +     }
    9.63 +
    9.64 +
    9.65 +datatype function_context_data =
    9.66 +  FunctionCtxData of
    9.67 +     {
    9.68 +      defname : string,
    9.69 +
    9.70 +      (* contains no logical entities: invariant under morphisms *)
    9.71 +      add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list 
    9.72 +                  -> local_theory -> thm list * local_theory,
    9.73 +      case_names : string list,
    9.74 +
    9.75 +      fs : term list,
    9.76 +      R : term,
    9.77 +      
    9.78 +      psimps: thm list,
    9.79 +      pinducts: thm list,
    9.80 +      termination: thm
    9.81 +     }
    9.82 +
    9.83 +fun morph_function_data (FunctionCtxData {add_simps, case_names, fs, R, 
    9.84 +                                      psimps, pinducts, termination, defname}) phi =
    9.85 +    let
    9.86 +      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    9.87 +      val name = Binding.name_of o Morphism.binding phi o Binding.name
    9.88 +    in
    9.89 +      FunctionCtxData { add_simps = add_simps, case_names = case_names,
    9.90 +                      fs = map term fs, R = term R, psimps = fact psimps, 
    9.91 +                      pinducts = fact pinducts, termination = thm termination,
    9.92 +                      defname = name defname }
    9.93 +    end
    9.94 +
    9.95 +structure FunctionData = GenericDataFun
    9.96 +(
    9.97 +  type T = (term * function_context_data) Item_Net.T;
    9.98 +  val empty = Item_Net.init
    9.99 +    (op aconv o pairself fst : (term * function_context_data) * (term * function_context_data) -> bool)
   9.100 +    fst;
   9.101 +  val copy = I;
   9.102 +  val extend = I;
   9.103 +  fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
   9.104 +);
   9.105 +
   9.106 +val get_function = FunctionData.get o Context.Proof;
   9.107 +
   9.108 +
   9.109 +(* Generally useful?? *)
   9.110 +fun lift_morphism thy f = 
   9.111 +    let 
   9.112 +      val term = Drule.term_rule thy f
   9.113 +    in
   9.114 +      Morphism.thm_morphism f $> Morphism.term_morphism term 
   9.115 +       $> Morphism.typ_morphism (Logic.type_map term)
   9.116 +    end
   9.117 +
   9.118 +fun import_function_data t ctxt =
   9.119 +    let
   9.120 +      val thy = ProofContext.theory_of ctxt
   9.121 +      val ct = cterm_of thy t
   9.122 +      val inst_morph = lift_morphism thy o Thm.instantiate 
   9.123 +
   9.124 +      fun match (trm, data) = 
   9.125 +          SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
   9.126 +          handle Pattern.MATCH => NONE
   9.127 +    in 
   9.128 +      get_first match (Item_Net.retrieve (get_function ctxt) t)
   9.129 +    end
   9.130 +
   9.131 +fun import_last_function ctxt =
   9.132 +    case Item_Net.content (get_function ctxt) of
   9.133 +      [] => NONE
   9.134 +    | (t, data) :: _ =>
   9.135 +      let 
   9.136 +        val ([t'], ctxt') = Variable.import_terms true [t] ctxt
   9.137 +      in
   9.138 +        import_function_data t' ctxt'
   9.139 +      end
   9.140 +
   9.141 +val all_function_data = Item_Net.content o get_function
   9.142 +
   9.143 +fun add_function_data (data as FunctionCtxData {fs, termination, ...}) =
   9.144 +    FunctionData.map (fold (fn f => Item_Net.insert (f, data)) fs)
   9.145 +    #> store_termination_rule termination
   9.146 +
   9.147 +
   9.148 +(* Simp rules for termination proofs *)
   9.149 +
   9.150 +structure Termination_Simps = Named_Thms
   9.151 +(
   9.152 +  val name = "termination_simp" 
   9.153 +  val description = "Simplification rule for termination proofs"
   9.154 +);
   9.155 +
   9.156 +
   9.157 +(* Default Termination Prover *)
   9.158 +
   9.159 +structure TerminationProver = GenericDataFun
   9.160 +(
   9.161 +  type T = Proof.context -> Proof.method
   9.162 +  val empty = (fn _ => error "Termination prover not configured")
   9.163 +  val extend = I
   9.164 +  fun merge _ (a,b) = b (* FIXME *)
   9.165 +);
   9.166 +
   9.167 +val set_termination_prover = TerminationProver.put
   9.168 +val get_termination_prover = TerminationProver.get o Context.Proof
   9.169 +
   9.170 +
   9.171 +(* Configuration management *)
   9.172 +datatype function_opt 
   9.173 +  = Sequential
   9.174 +  | Default of string
   9.175 +  | DomIntros
   9.176 +  | Tailrec
   9.177 +
   9.178 +datatype function_config
   9.179 +  = FunctionConfig of
   9.180 +   {
   9.181 +    sequential: bool,
   9.182 +    default: string,
   9.183 +    domintros: bool,
   9.184 +    tailrec: bool
   9.185 +   }
   9.186 +
   9.187 +fun apply_opt Sequential (FunctionConfig {sequential, default, domintros,tailrec}) = 
   9.188 +    FunctionConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
   9.189 +  | apply_opt (Default d) (FunctionConfig {sequential, default, domintros,tailrec}) = 
   9.190 +    FunctionConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
   9.191 +  | apply_opt DomIntros (FunctionConfig {sequential, default, domintros,tailrec}) =
   9.192 +    FunctionConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
   9.193 +  | apply_opt Tailrec (FunctionConfig {sequential, default, domintros,tailrec}) =
   9.194 +    FunctionConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
   9.195 +
   9.196 +val default_config =
   9.197 +  FunctionConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
   9.198 +                 domintros=false, tailrec=false }
   9.199 +
   9.200 +
   9.201 +(* Analyzing function equations *)
   9.202 +
   9.203 +fun split_def ctxt geq =
   9.204 +    let
   9.205 +      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
   9.206 +      val qs = Term.strip_qnt_vars "all" geq
   9.207 +      val imp = Term.strip_qnt_body "all" geq
   9.208 +      val (gs, eq) = Logic.strip_horn imp
   9.209 +
   9.210 +      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
   9.211 +          handle TERM _ => error (input_error "Not an equation")
   9.212 +
   9.213 +      val (head, args) = strip_comb f_args
   9.214 +
   9.215 +      val fname = fst (dest_Free head)
   9.216 +          handle TERM _ => error (input_error "Head symbol must not be a bound variable")
   9.217 +    in
   9.218 +      (fname, qs, gs, args, rhs)
   9.219 +    end
   9.220 +
   9.221 +(* Check for all sorts of errors in the input *)
   9.222 +fun check_defs ctxt fixes eqs =
   9.223 +    let
   9.224 +      val fnames = map (fst o fst) fixes
   9.225 +                                
   9.226 +      fun check geq = 
   9.227 +          let
   9.228 +            fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
   9.229 +                                  
   9.230 +            val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
   9.231 +                                 
   9.232 +            val _ = fname mem fnames 
   9.233 +                    orelse input_error 
   9.234 +                             ("Head symbol of left hand side must be " 
   9.235 +                              ^ plural "" "one out of " fnames ^ commas_quote fnames)
   9.236 +                                            
   9.237 +            val _ = length args > 0 orelse input_error "Function has no arguments:"
   9.238 +
   9.239 +            fun add_bvs t is = add_loose_bnos (t, 0, is)
   9.240 +            val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
   9.241 +                        |> map (fst o nth (rev qs))
   9.242 +                      
   9.243 +            val _ = null rvs orelse input_error 
   9.244 +                        ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
   9.245 +                         ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
   9.246 +                                    
   9.247 +            val _ = forall (not o Term.exists_subterm 
   9.248 +                             (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
   9.249 +                    orelse input_error "Defined function may not occur in premises or arguments"
   9.250 +
   9.251 +            val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
   9.252 +            val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
   9.253 +            val _ = null funvars
   9.254 +                    orelse (warning (cat_lines 
   9.255 +                    ["Bound variable" ^ plural " " "s " funvars 
   9.256 +                     ^ commas_quote (map fst funvars) ^  
   9.257 +                     " occur" ^ plural "s" "" funvars ^ " in function position.",  
   9.258 +                     "Misspelled constructor???"]); true)
   9.259 +          in
   9.260 +            (fname, length args)
   9.261 +          end
   9.262 +
   9.263 +      val _ = AList.group (op =) (map check eqs)
   9.264 +        |> map (fn (fname, ars) =>
   9.265 +             length (distinct (op =) ars) = 1
   9.266 +             orelse error ("Function " ^ quote fname ^
   9.267 +                           " has different numbers of arguments in different equations"))
   9.268 +
   9.269 +      fun check_sorts ((fname, fT), _) =
   9.270 +          Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
   9.271 +          orelse error (cat_lines 
   9.272 +          ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
   9.273 +           setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
   9.274 +
   9.275 +      val _ = map check_sorts fixes
   9.276 +    in
   9.277 +      ()
   9.278 +    end
   9.279 +
   9.280 +(* Preprocessors *)
   9.281 +
   9.282 +type fixes = ((string * typ) * mixfix) list
   9.283 +type 'a spec = (Attrib.binding * 'a list) list
   9.284 +type preproc = function_config -> Proof.context -> fixes -> term spec 
   9.285 +               -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
   9.286 +
   9.287 +val fname_of = fst o dest_Free o fst o strip_comb o fst 
   9.288 + o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
   9.289 +
   9.290 +fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
   9.291 +  | mk_case_names _ n 0 = []
   9.292 +  | mk_case_names _ n 1 = [n]
   9.293 +  | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
   9.294 +
   9.295 +fun empty_preproc check _ ctxt fixes spec =
   9.296 +    let 
   9.297 +      val (bnds, tss) = split_list spec
   9.298 +      val ts = flat tss
   9.299 +      val _ = check ctxt fixes ts
   9.300 +      val fnames = map (fst o fst) fixes
   9.301 +      val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
   9.302 +
   9.303 +      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
   9.304 +                                   (indices ~~ xs)
   9.305 +                        |> map (map snd)
   9.306 +
   9.307 +      (* using theorem names for case name currently disabled *)
   9.308 +      val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
   9.309 +    in
   9.310 +      (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
   9.311 +    end
   9.312 +
   9.313 +structure Preprocessor = GenericDataFun
   9.314 +(
   9.315 +  type T = preproc
   9.316 +  val empty : T = empty_preproc check_defs
   9.317 +  val extend = I
   9.318 +  fun merge _ (a, _) = a
   9.319 +);
   9.320 +
   9.321 +val get_preproc = Preprocessor.get o Context.Proof
   9.322 +val set_preproc = Preprocessor.map o K
   9.323 +
   9.324 +
   9.325 +
   9.326 +local 
   9.327 +  structure P = OuterParse and K = OuterKeyword
   9.328 +
   9.329 +  val option_parser = 
   9.330 +      P.group "option" ((P.reserved "sequential" >> K Sequential)
   9.331 +                    || ((P.reserved "default" |-- P.term) >> Default)
   9.332 +                    || (P.reserved "domintros" >> K DomIntros)
   9.333 +                    || (P.reserved "tailrec" >> K Tailrec))
   9.334 +
   9.335 +  fun config_parser default = 
   9.336 +      (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
   9.337 +        >> (fn opts => fold apply_opt opts default)
   9.338 +in
   9.339 +  fun function_parser default_cfg = 
   9.340 +      config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
   9.341 +end
   9.342 +
   9.343 +
   9.344 +end
   9.345 +end
   9.346 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/Function/function_core.ML	Fri Oct 23 16:22:10 2009 +0200
    10.3 @@ -0,0 +1,956 @@
    10.4 +(*  Title:      HOL/Tools/Function/function_core.ML
    10.5 +    Author:     Alexander Krauss, TU Muenchen
    10.6 +
    10.7 +A package for general recursive function definitions:
    10.8 +Main functionality.
    10.9 +*)
   10.10 +
   10.11 +signature FUNCTION_CORE =
   10.12 +sig
   10.13 +    val trace: bool Unsynchronized.ref
   10.14 +
   10.15 +    val prepare_function : Function_Common.function_config
   10.16 +                         -> string (* defname *)
   10.17 +                         -> ((bstring * typ) * mixfix) list (* defined symbol *)
   10.18 +                         -> ((bstring * typ) list * term list * term * term) list (* specification *)
   10.19 +                         -> local_theory
   10.20 +
   10.21 +                         -> (term   (* f *)
   10.22 +                             * thm  (* goalstate *)
   10.23 +                             * (thm -> Function_Common.function_result) (* continuation *)
   10.24 +                            ) * local_theory
   10.25 +
   10.26 +end
   10.27 +
   10.28 +structure Function_Core : FUNCTION_CORE =
   10.29 +struct
   10.30 +
   10.31 +val trace = Unsynchronized.ref false;
   10.32 +fun trace_msg msg = if ! trace then tracing (msg ()) else ();
   10.33 +
   10.34 +val boolT = HOLogic.boolT
   10.35 +val mk_eq = HOLogic.mk_eq
   10.36 +
   10.37 +open Function_Lib
   10.38 +open Function_Common
   10.39 +
   10.40 +datatype globals =
   10.41 +   Globals of {
   10.42 +         fvar: term,
   10.43 +         domT: typ,
   10.44 +         ranT: typ,
   10.45 +         h: term,
   10.46 +         y: term,
   10.47 +         x: term,
   10.48 +         z: term,
   10.49 +         a: term,
   10.50 +         P: term,
   10.51 +         D: term,
   10.52 +         Pbool:term
   10.53 +}
   10.54 +
   10.55 +
   10.56 +datatype rec_call_info =
   10.57 +  RCInfo of
   10.58 +  {
   10.59 +   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
   10.60 +   CCas: thm list,
   10.61 +   rcarg: term,                 (* The recursive argument *)
   10.62 +
   10.63 +   llRI: thm,
   10.64 +   h_assum: term
   10.65 +  }
   10.66 +
   10.67 +
   10.68 +datatype clause_context =
   10.69 +  ClauseContext of
   10.70 +  {
   10.71 +    ctxt : Proof.context,
   10.72 +
   10.73 +    qs : term list,
   10.74 +    gs : term list,
   10.75 +    lhs: term,
   10.76 +    rhs: term,
   10.77 +
   10.78 +    cqs: cterm list,
   10.79 +    ags: thm list,
   10.80 +    case_hyp : thm
   10.81 +  }
   10.82 +
   10.83 +
   10.84 +fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
   10.85 +    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
   10.86 +                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
   10.87 +
   10.88 +
   10.89 +datatype clause_info =
   10.90 +  ClauseInfo of
   10.91 +     {
   10.92 +      no: int,
   10.93 +      qglr : ((string * typ) list * term list * term * term),
   10.94 +      cdata : clause_context,
   10.95 +
   10.96 +      tree: Function_Ctx_Tree.ctx_tree,
   10.97 +      lGI: thm,
   10.98 +      RCs: rec_call_info list
   10.99 +     }
  10.100 +
  10.101 +
  10.102 +(* Theory dependencies. *)
  10.103 +val Pair_inject = @{thm Product_Type.Pair_inject};
  10.104 +
  10.105 +val acc_induct_rule = @{thm accp_induct_rule};
  10.106 +
  10.107 +val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
  10.108 +val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
  10.109 +val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
  10.110 +
  10.111 +val acc_downward = @{thm accp_downward};
  10.112 +val accI = @{thm accp.accI};
  10.113 +val case_split = @{thm HOL.case_split};
  10.114 +val fundef_default_value = @{thm FunDef.fundef_default_value};
  10.115 +val not_acc_down = @{thm not_accp_down};
  10.116 +
  10.117 +
  10.118 +
  10.119 +fun find_calls tree =
  10.120 +    let
  10.121 +      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
  10.122 +        | add_Ri _ _ _ _ = raise Match
  10.123 +    in
  10.124 +      rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
  10.125 +    end
  10.126 +
  10.127 +
  10.128 +(** building proof obligations *)
  10.129 +
  10.130 +fun mk_compat_proof_obligations domT ranT fvar f glrs =
  10.131 +    let
  10.132 +      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
  10.133 +          let
  10.134 +            val shift = incr_boundvars (length qs')
  10.135 +          in
  10.136 +            Logic.mk_implies
  10.137 +              (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
  10.138 +                HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
  10.139 +              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
  10.140 +              |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
  10.141 +              |> curry abstract_over fvar
  10.142 +              |> curry subst_bound f
  10.143 +          end
  10.144 +    in
  10.145 +      map mk_impl (unordered_pairs glrs)
  10.146 +    end
  10.147 +
  10.148 +
  10.149 +fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
  10.150 +    let
  10.151 +        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
  10.152 +            HOLogic.mk_Trueprop Pbool
  10.153 +                     |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
  10.154 +                     |> fold_rev (curry Logic.mk_implies) gs
  10.155 +                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  10.156 +    in
  10.157 +        HOLogic.mk_Trueprop Pbool
  10.158 +                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
  10.159 +                 |> mk_forall_rename ("x", x)
  10.160 +                 |> mk_forall_rename ("P", Pbool)
  10.161 +    end
  10.162 +
  10.163 +(** making a context with it's own local bindings **)
  10.164 +
  10.165 +fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
  10.166 +    let
  10.167 +      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
  10.168 +                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
  10.169 +
  10.170 +      val thy = ProofContext.theory_of ctxt'
  10.171 +
  10.172 +      fun inst t = subst_bounds (rev qs, t)
  10.173 +      val gs = map inst pre_gs
  10.174 +      val lhs = inst pre_lhs
  10.175 +      val rhs = inst pre_rhs
  10.176 +
  10.177 +      val cqs = map (cterm_of thy) qs
  10.178 +      val ags = map (assume o cterm_of thy) gs
  10.179 +
  10.180 +      val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
  10.181 +    in
  10.182 +      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
  10.183 +                      cqs = cqs, ags = ags, case_hyp = case_hyp }
  10.184 +    end
  10.185 +
  10.186 +
  10.187 +(* lowlevel term function. FIXME: remove *)
  10.188 +fun abstract_over_list vs body =
  10.189 +  let
  10.190 +    fun abs lev v tm =
  10.191 +      if v aconv tm then Bound lev
  10.192 +      else
  10.193 +        (case tm of
  10.194 +          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
  10.195 +        | t $ u => abs lev v t $ abs lev v u
  10.196 +        | t => t);
  10.197 +  in
  10.198 +    fold_index (fn (i, v) => fn t => abs i v t) vs body
  10.199 +  end
  10.200 +
  10.201 +
  10.202 +
  10.203 +fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
  10.204 +    let
  10.205 +        val Globals {h, fvar, x, ...} = globals
  10.206 +
  10.207 +        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
  10.208 +        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
  10.209 +
  10.210 +        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
  10.211 +        val lGI = GIntro_thm
  10.212 +                    |> forall_elim (cert f)
  10.213 +                    |> fold forall_elim cqs
  10.214 +                    |> fold Thm.elim_implies ags
  10.215 +
  10.216 +        fun mk_call_info (rcfix, rcassm, rcarg) RI =
  10.217 +            let
  10.218 +                val llRI = RI
  10.219 +                             |> fold forall_elim cqs
  10.220 +                             |> fold (forall_elim o cert o Free) rcfix
  10.221 +                             |> fold Thm.elim_implies ags
  10.222 +                             |> fold Thm.elim_implies rcassm
  10.223 +
  10.224 +                val h_assum =
  10.225 +                    HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
  10.226 +                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  10.227 +                              |> fold_rev (Logic.all o Free) rcfix
  10.228 +                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
  10.229 +                              |> abstract_over_list (rev qs)
  10.230 +            in
  10.231 +                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
  10.232 +            end
  10.233 +
  10.234 +        val RC_infos = map2 mk_call_info RCs RIntro_thms
  10.235 +    in
  10.236 +        ClauseInfo
  10.237 +            {
  10.238 +             no=no,
  10.239 +             cdata=cdata,
  10.240 +             qglr=qglr,
  10.241 +
  10.242 +             lGI=lGI,
  10.243 +             RCs=RC_infos,
  10.244 +             tree=tree
  10.245 +            }
  10.246 +    end
  10.247 +
  10.248 +
  10.249 +
  10.250 +
  10.251 +
  10.252 +
  10.253 +
  10.254 +(* replace this by a table later*)
  10.255 +fun store_compat_thms 0 thms = []
  10.256 +  | store_compat_thms n thms =
  10.257 +    let
  10.258 +        val (thms1, thms2) = chop n thms
  10.259 +    in
  10.260 +        (thms1 :: store_compat_thms (n - 1) thms2)
  10.261 +    end
  10.262 +
  10.263 +(* expects i <= j *)
  10.264 +fun lookup_compat_thm i j cts =
  10.265 +    nth (nth cts (i - 1)) (j - i)
  10.266 +
  10.267 +(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
  10.268 +(* if j < i, then turn around *)
  10.269 +fun get_compat_thm thy cts i j ctxi ctxj =
  10.270 +    let
  10.271 +      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
  10.272 +      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
  10.273 +
  10.274 +      val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
  10.275 +    in if j < i then
  10.276 +         let
  10.277 +           val compat = lookup_compat_thm j i cts
  10.278 +         in
  10.279 +           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
  10.280 +                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
  10.281 +                |> fold Thm.elim_implies agsj
  10.282 +                |> fold Thm.elim_implies agsi
  10.283 +                |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
  10.284 +         end
  10.285 +       else
  10.286 +         let
  10.287 +           val compat = lookup_compat_thm i j cts
  10.288 +         in
  10.289 +               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
  10.290 +                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
  10.291 +                 |> fold Thm.elim_implies agsi
  10.292 +                 |> fold Thm.elim_implies agsj
  10.293 +                 |> Thm.elim_implies (assume lhsi_eq_lhsj)
  10.294 +                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
  10.295 +         end
  10.296 +    end
  10.297 +
  10.298 +
  10.299 +
  10.300 +
  10.301 +(* Generates the replacement lemma in fully quantified form. *)
  10.302 +fun mk_replacement_lemma thy h ih_elim clause =
  10.303 +    let
  10.304 +        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
  10.305 +        local open Conv in
  10.306 +        val ih_conv = arg1_conv o arg_conv o arg_conv
  10.307 +        end
  10.308 +
  10.309 +        val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
  10.310 +
  10.311 +        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
  10.312 +        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
  10.313 +
  10.314 +        val (eql, _) = Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
  10.315 +
  10.316 +        val replace_lemma = (eql RS meta_eq_to_obj_eq)
  10.317 +                                |> implies_intr (cprop_of case_hyp)
  10.318 +                                |> fold_rev (implies_intr o cprop_of) h_assums
  10.319 +                                |> fold_rev (implies_intr o cprop_of) ags
  10.320 +                                |> fold_rev forall_intr cqs
  10.321 +                                |> Thm.close_derivation
  10.322 +    in
  10.323 +      replace_lemma
  10.324 +    end
  10.325 +
  10.326 +
  10.327 +fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
  10.328 +    let
  10.329 +        val Globals {h, y, x, fvar, ...} = globals
  10.330 +        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
  10.331 +        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
  10.332 +
  10.333 +        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
  10.334 +            = mk_clause_context x ctxti cdescj
  10.335 +
  10.336 +        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
  10.337 +        val compat = get_compat_thm thy compat_store i j cctxi cctxj
  10.338 +        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
  10.339 +
  10.340 +        val RLj_import =
  10.341 +            RLj |> fold forall_elim cqsj'
  10.342 +                |> fold Thm.elim_implies agsj'
  10.343 +                |> fold Thm.elim_implies Ghsj'
  10.344 +
  10.345 +        val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
  10.346 +        val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
  10.347 +    in
  10.348 +        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
  10.349 +        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
  10.350 +        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
  10.351 +        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
  10.352 +        |> fold_rev (implies_intr o cprop_of) Ghsj'
  10.353 +        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
  10.354 +        |> implies_intr (cprop_of y_eq_rhsj'h)
  10.355 +        |> implies_intr (cprop_of lhsi_eq_lhsj')
  10.356 +        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
  10.357 +    end
  10.358 +
  10.359 +
  10.360 +
  10.361 +fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
  10.362 +    let
  10.363 +        val Globals {x, y, ranT, fvar, ...} = globals
  10.364 +        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
  10.365 +        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
  10.366 +
  10.367 +        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
  10.368 +
  10.369 +        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
  10.370 +                                                            |> fold_rev (implies_intr o cprop_of) CCas
  10.371 +                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  10.372 +
  10.373 +        val existence = fold (curry op COMP o prep_RC) RCs lGI
  10.374 +
  10.375 +        val P = cterm_of thy (mk_eq (y, rhsC))
  10.376 +        val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
  10.377 +
  10.378 +        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
  10.379 +
  10.380 +        val uniqueness = G_cases
  10.381 +                           |> forall_elim (cterm_of thy lhs)
  10.382 +                           |> forall_elim (cterm_of thy y)
  10.383 +                           |> forall_elim P
  10.384 +                           |> Thm.elim_implies G_lhs_y
  10.385 +                           |> fold Thm.elim_implies unique_clauses
  10.386 +                           |> implies_intr (cprop_of G_lhs_y)
  10.387 +                           |> forall_intr (cterm_of thy y)
  10.388 +
  10.389 +        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
  10.390 +
  10.391 +        val exactly_one =
  10.392 +            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
  10.393 +                 |> curry (op COMP) existence
  10.394 +                 |> curry (op COMP) uniqueness
  10.395 +                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
  10.396 +                 |> implies_intr (cprop_of case_hyp)
  10.397 +                 |> fold_rev (implies_intr o cprop_of) ags
  10.398 +                 |> fold_rev forall_intr cqs
  10.399 +
  10.400 +        val function_value =
  10.401 +            existence
  10.402 +              |> implies_intr ihyp
  10.403 +              |> implies_intr (cprop_of case_hyp)
  10.404 +              |> forall_intr (cterm_of thy x)
  10.405 +              |> forall_elim (cterm_of thy lhs)
  10.406 +              |> curry (op RS) refl
  10.407 +    in
  10.408 +        (exactly_one, function_value)
  10.409 +    end
  10.410 +
  10.411 +
  10.412 +
  10.413 +
  10.414 +fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
  10.415 +    let
  10.416 +        val Globals {h, domT, ranT, x, ...} = globals
  10.417 +        val thy = ProofContext.theory_of ctxt
  10.418 +
  10.419 +        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
  10.420 +        val ihyp = Term.all domT $ Abs ("z", domT,
  10.421 +                                   Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
  10.422 +                                     HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
  10.423 +                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
  10.424 +                       |> cterm_of thy
  10.425 +
  10.426 +        val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
  10.427 +        val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
  10.428 +        val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
  10.429 +                        |> instantiate' [] [NONE, SOME (cterm_of thy h)]
  10.430 +
  10.431 +        val _ = trace_msg (K "Proving Replacement lemmas...")
  10.432 +        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
  10.433 +
  10.434 +        val _ = trace_msg (K "Proving cases for unique existence...")
  10.435 +        val (ex1s, values) =
  10.436 +            split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
  10.437 +
  10.438 +        val _ = trace_msg (K "Proving: Graph is a function")
  10.439 +        val graph_is_function = complete
  10.440 +                                  |> Thm.forall_elim_vars 0
  10.441 +                                  |> fold (curry op COMP) ex1s
  10.442 +                                  |> implies_intr (ihyp)
  10.443 +                                  |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
  10.444 +                                  |> forall_intr (cterm_of thy x)
  10.445 +                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
  10.446 +                                  |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
  10.447 +
  10.448 +        val goalstate =  Conjunction.intr graph_is_function complete
  10.449 +                          |> Thm.close_derivation
  10.450 +                          |> Goal.protect
  10.451 +                          |> fold_rev (implies_intr o cprop_of) compat
  10.452 +                          |> implies_intr (cprop_of complete)
  10.453 +    in
  10.454 +      (goalstate, values)
  10.455 +    end
  10.456 +
  10.457 +
  10.458 +fun define_graph Gname fvar domT ranT clauses RCss lthy =
  10.459 +    let
  10.460 +      val GT = domT --> ranT --> boolT
  10.461 +      val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
  10.462 +
  10.463 +      fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
  10.464 +          let
  10.465 +            fun mk_h_assm (rcfix, rcassm, rcarg) =
  10.466 +                HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
  10.467 +                          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  10.468 +                          |> fold_rev (Logic.all o Free) rcfix
  10.469 +          in
  10.470 +            HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
  10.471 +                      |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
  10.472 +                      |> fold_rev (curry Logic.mk_implies) gs
  10.473 +                      |> fold_rev Logic.all (fvar :: qs)
  10.474 +          end
  10.475 +
  10.476 +      val G_intros = map2 mk_GIntro clauses RCss
  10.477 +
  10.478 +      val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
  10.479 +          Function_Inductive_Wrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
  10.480 +    in
  10.481 +      ((G, GIntro_thms, G_elim, G_induct), lthy)
  10.482 +    end
  10.483 +
  10.484 +
  10.485 +
  10.486 +fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
  10.487 +    let
  10.488 +      val f_def =
  10.489 +          Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
  10.490 +                                Abs ("y", ranT, G $ Bound 1 $ Bound 0))
  10.491 +              |> Syntax.check_term lthy
  10.492 +
  10.493 +      val ((f, (_, f_defthm)), lthy) =
  10.494 +        LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
  10.495 +    in
  10.496 +      ((f, f_defthm), lthy)
  10.497 +    end
  10.498 +
  10.499 +
  10.500 +fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
  10.501 +    let
  10.502 +
  10.503 +      val RT = domT --> domT --> boolT
  10.504 +      val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
  10.505 +
  10.506 +      fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
  10.507 +          HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
  10.508 +                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  10.509 +                    |> fold_rev (curry Logic.mk_implies) gs
  10.510 +                    |> fold_rev (Logic.all o Free) rcfix
  10.511 +                    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  10.512 +                    (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
  10.513 +
  10.514 +      val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
  10.515 +
  10.516 +      val (RIntro_thmss, (R, R_elim, _, lthy)) =
  10.517 +          fold_burrow Function_Inductive_Wrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
  10.518 +    in
  10.519 +      ((R, RIntro_thmss, R_elim), lthy)
  10.520 +    end
  10.521 +
  10.522 +
  10.523 +fun fix_globals domT ranT fvar ctxt =
  10.524 +    let
  10.525 +      val ([h, y, x, z, a, D, P, Pbool],ctxt') =
  10.526 +          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
  10.527 +    in
  10.528 +      (Globals {h = Free (h, domT --> ranT),
  10.529 +                y = Free (y, ranT),
  10.530 +                x = Free (x, domT),
  10.531 +                z = Free (z, domT),
  10.532 +                a = Free (a, domT),
  10.533 +                D = Free (D, domT --> boolT),
  10.534 +                P = Free (P, domT --> boolT),
  10.535 +                Pbool = Free (Pbool, boolT),
  10.536 +                fvar = fvar,
  10.537 +                domT = domT,
  10.538 +                ranT = ranT
  10.539 +               },
  10.540 +       ctxt')
  10.541 +    end
  10.542 +
  10.543 +
  10.544 +
  10.545 +fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
  10.546 +    let
  10.547 +      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
  10.548 +    in
  10.549 +      (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
  10.550 +    end
  10.551 +
  10.552 +
  10.553 +
  10.554 +(**********************************************************
  10.555 + *                   PROVING THE RULES
  10.556 + **********************************************************)
  10.557 +
  10.558 +fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
  10.559 +    let
  10.560 +      val Globals {domT, z, ...} = globals
  10.561 +
  10.562 +      fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
  10.563 +          let
  10.564 +            val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
  10.565 +            val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
  10.566 +          in
  10.567 +            ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
  10.568 +              |> (fn it => it COMP graph_is_function)
  10.569 +              |> implies_intr z_smaller
  10.570 +              |> forall_intr (cterm_of thy z)
  10.571 +              |> (fn it => it COMP valthm)
  10.572 +              |> implies_intr lhs_acc
  10.573 +              |> asm_simplify (HOL_basic_ss addsimps [f_iff])
  10.574 +              |> fold_rev (implies_intr o cprop_of) ags
  10.575 +              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  10.576 +          end
  10.577 +    in
  10.578 +      map2 mk_psimp clauses valthms
  10.579 +    end
  10.580 +
  10.581 +
  10.582 +(** Induction rule **)
  10.583 +
  10.584 +
  10.585 +val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
  10.586 +
  10.587 +
  10.588 +fun mk_partial_induct_rule thy globals R complete_thm clauses =
  10.589 +    let
  10.590 +      val Globals {domT, x, z, a, P, D, ...} = globals
  10.591 +      val acc_R = mk_acc domT R
  10.592 +
  10.593 +      val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
  10.594 +      val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
  10.595 +
  10.596 +      val D_subset = cterm_of thy (Logic.all x
  10.597 +        (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
  10.598 +
  10.599 +      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
  10.600 +                    Logic.all x
  10.601 +                    (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
  10.602 +                                                    Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
  10.603 +                                                                      HOLogic.mk_Trueprop (D $ z)))))
  10.604 +                    |> cterm_of thy
  10.605 +
  10.606 +
  10.607 +  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
  10.608 +      val ihyp = Term.all domT $ Abs ("z", domT,
  10.609 +               Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
  10.610 +                 HOLogic.mk_Trueprop (P $ Bound 0)))
  10.611 +           |> cterm_of thy
  10.612 +
  10.613 +      val aihyp = assume ihyp
  10.614 +
  10.615 +  fun prove_case clause =
  10.616 +      let
  10.617 +    val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
  10.618 +                    qglr = (oqs, _, _, _), ...} = clause
  10.619 +
  10.620 +    val case_hyp_conv = K (case_hyp RS eq_reflection)
  10.621 +    local open Conv in
  10.622 +    val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
  10.623 +    val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
  10.624 +    end
  10.625 +
  10.626 +    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
  10.627 +        sih |> forall_elim (cterm_of thy rcarg)
  10.628 +            |> Thm.elim_implies llRI
  10.629 +            |> fold_rev (implies_intr o cprop_of) CCas
  10.630 +            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  10.631 +
  10.632 +    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
  10.633 +
  10.634 +    val step = HOLogic.mk_Trueprop (P $ lhs)
  10.635 +            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
  10.636 +            |> fold_rev (curry Logic.mk_implies) gs
  10.637 +            |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
  10.638 +            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  10.639 +            |> cterm_of thy
  10.640 +
  10.641 +    val P_lhs = assume step
  10.642 +           |> fold forall_elim cqs
  10.643 +           |> Thm.elim_implies lhs_D
  10.644 +           |> fold Thm.elim_implies ags
  10.645 +           |> fold Thm.elim_implies P_recs
  10.646 +
  10.647 +    val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
  10.648 +           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
  10.649 +           |> symmetric (* P lhs == P x *)
  10.650 +           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
  10.651 +           |> implies_intr (cprop_of case_hyp)
  10.652 +           |> fold_rev (implies_intr o cprop_of) ags
  10.653 +           |> fold_rev forall_intr cqs
  10.654 +      in
  10.655 +        (res, step)
  10.656 +      end
  10.657 +
  10.658 +  val (cases, steps) = split_list (map prove_case clauses)
  10.659 +
  10.660 +  val istep = complete_thm
  10.661 +                |> Thm.forall_elim_vars 0
  10.662 +                |> fold (curry op COMP) cases (*  P x  *)
  10.663 +                |> implies_intr ihyp
  10.664 +                |> implies_intr (cprop_of x_D)
  10.665 +                |> forall_intr (cterm_of thy x)
  10.666 +
  10.667 +  val subset_induct_rule =
  10.668 +      acc_subset_induct
  10.669 +        |> (curry op COMP) (assume D_subset)
  10.670 +        |> (curry op COMP) (assume D_dcl)
  10.671 +        |> (curry op COMP) (assume a_D)
  10.672 +        |> (curry op COMP) istep
  10.673 +        |> fold_rev implies_intr steps
  10.674 +        |> implies_intr a_D
  10.675 +        |> implies_intr D_dcl
  10.676 +        |> implies_intr D_subset
  10.677 +
  10.678 +  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
  10.679 +
  10.680 +  val simple_induct_rule =
  10.681 +      subset_induct_rule
  10.682 +        |> forall_intr (cterm_of thy D)
  10.683 +        |> forall_elim (cterm_of thy acc_R)
  10.684 +        |> assume_tac 1 |> Seq.hd
  10.685 +        |> (curry op COMP) (acc_downward
  10.686 +                              |> (instantiate' [SOME (ctyp_of thy domT)]
  10.687 +                                               (map (SOME o cterm_of thy) [R, x, z]))
  10.688 +                              |> forall_intr (cterm_of thy z)
  10.689 +                              |> forall_intr (cterm_of thy x))
  10.690 +        |> forall_intr (cterm_of thy a)
  10.691 +        |> forall_intr (cterm_of thy P)
  10.692 +    in
  10.693 +      simple_induct_rule
  10.694 +    end
  10.695 +
  10.696 +
  10.697 +
  10.698 +(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
  10.699 +fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
  10.700 +    let
  10.701 +      val thy = ProofContext.theory_of ctxt
  10.702 +      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
  10.703 +                      qglr = (oqs, _, _, _), ...} = clause
  10.704 +      val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
  10.705 +                          |> fold_rev (curry Logic.mk_implies) gs
  10.706 +                          |> cterm_of thy
  10.707 +    in
  10.708 +      Goal.init goal
  10.709 +      |> (SINGLE (resolve_tac [accI] 1)) |> the
  10.710 +      |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
  10.711 +      |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
  10.712 +      |> Goal.conclude
  10.713 +      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  10.714 +    end
  10.715 +
  10.716 +
  10.717 +
  10.718 +(** Termination rule **)
  10.719 +
  10.720 +val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
  10.721 +val wf_in_rel = @{thm FunDef.wf_in_rel};
  10.722 +val in_rel_def = @{thm FunDef.in_rel_def};
  10.723 +
  10.724 +fun mk_nest_term_case thy globals R' ihyp clause =
  10.725 +    let
  10.726 +      val Globals {x, z, ...} = globals
  10.727 +      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
  10.728 +                      qglr=(oqs, _, _, _), ...} = clause
  10.729 +
  10.730 +      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
  10.731 +
  10.732 +      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
  10.733 +          let
  10.734 +            val used = map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) (u @ sub)
  10.735 +
  10.736 +            val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
  10.737 +                      |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
  10.738 +                      |> Function_Ctx_Tree.export_term (fixes, assumes)
  10.739 +                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
  10.740 +                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  10.741 +                      |> cterm_of thy
  10.742 +
  10.743 +            val thm = assume hyp
  10.744 +                      |> fold forall_elim cqs
  10.745 +                      |> fold Thm.elim_implies ags
  10.746 +                      |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
  10.747 +                      |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
  10.748 +
  10.749 +            val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
  10.750 +
  10.751 +            val acc = thm COMP ih_case
  10.752 +            val z_acc_local = acc
  10.753 +            |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
  10.754 +
  10.755 +            val ethm = z_acc_local
  10.756 +                         |> Function_Ctx_Tree.export_thm thy (fixes,
  10.757 +                                                          z_eq_arg :: case_hyp :: ags @ assumes)
  10.758 +                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  10.759 +
  10.760 +            val sub' = sub @ [(([],[]), acc)]
  10.761 +          in
  10.762 +            (sub', (hyp :: hyps, ethm :: thms))
  10.763 +          end
  10.764 +        | step _ _ _ _ = raise Match
  10.765 +    in
  10.766 +      Function_Ctx_Tree.traverse_tree step tree
  10.767 +    end
  10.768 +
  10.769 +
  10.770 +fun mk_nest_term_rule thy globals R R_cases clauses =
  10.771 +    let
  10.772 +      val Globals { domT, x, z, ... } = globals
  10.773 +      val acc_R = mk_acc domT R
  10.774 +
  10.775 +      val R' = Free ("R", fastype_of R)
  10.776 +
  10.777 +      val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
  10.778 +      val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
  10.779 +
  10.780 +      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
  10.781 +
  10.782 +      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
  10.783 +      val ihyp = Term.all domT $ Abs ("z", domT,
  10.784 +                                 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
  10.785 +                                   HOLogic.mk_Trueprop (acc_R $ Bound 0)))
  10.786 +                     |> cterm_of thy
  10.787 +
  10.788 +      val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
  10.789 +
  10.790 +      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
  10.791 +
  10.792 +      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
  10.793 +    in
  10.794 +      R_cases
  10.795 +        |> forall_elim (cterm_of thy z)
  10.796 +        |> forall_elim (cterm_of thy x)
  10.797 +        |> forall_elim (cterm_of thy (acc_R $ z))
  10.798 +        |> curry op COMP (assume R_z_x)
  10.799 +        |> fold_rev (curry op COMP) cases
  10.800 +        |> implies_intr R_z_x
  10.801 +        |> forall_intr (cterm_of thy z)
  10.802 +        |> (fn it => it COMP accI)
  10.803 +        |> implies_intr ihyp
  10.804 +        |> forall_intr (cterm_of thy x)
  10.805 +        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
  10.806 +        |> curry op RS (assume wfR')
  10.807 +        |> forall_intr_vars
  10.808 +        |> (fn it => it COMP allI)
  10.809 +        |> fold implies_intr hyps
  10.810 +        |> implies_intr wfR'
  10.811 +        |> forall_intr (cterm_of thy R')
  10.812 +        |> forall_elim (cterm_of thy (inrel_R))
  10.813 +        |> curry op RS wf_in_rel
  10.814 +        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
  10.815 +        |> forall_intr (cterm_of thy Rrel)
  10.816 +    end
  10.817 +
  10.818 +
  10.819 +
  10.820 +(* Tail recursion (probably very fragile)
  10.821 + *
  10.822 + * FIXME:
  10.823 + * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
  10.824 + * - Must we really replace the fvar by f here?
  10.825 + * - Splitting is not configured automatically: Problems with case?
  10.826 + *)
  10.827 +fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
  10.828 +    let
  10.829 +      val Globals {domT, ranT, fvar, ...} = globals
  10.830 +
  10.831 +      val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
  10.832 +
  10.833 +      val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
  10.834 +          Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
  10.835 +                     (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
  10.836 +                     (fn {prems=[a], ...} =>
  10.837 +                         ((rtac (G_induct OF [a]))
  10.838 +                            THEN_ALL_NEW (rtac accI)
  10.839 +                            THEN_ALL_NEW (etac R_cases)
  10.840 +                            THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
  10.841 +
  10.842 +      val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
  10.843 +
  10.844 +      fun mk_trsimp clause psimp =
  10.845 +          let
  10.846 +            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
  10.847 +            val thy = ProofContext.theory_of ctxt
  10.848 +            val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
  10.849 +
  10.850 +            val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
  10.851 +            val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
  10.852 +            fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
  10.853 +          in
  10.854 +            Goal.prove ctxt [] [] trsimp
  10.855 +                       (fn _ =>
  10.856 +                           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
  10.857 +                                THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
  10.858 +                                THEN (simp_default_tac (simpset_of ctxt) 1)
  10.859 +                                THEN (etac not_acc_down 1)
  10.860 +                                THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
  10.861 +              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  10.862 +          end
  10.863 +    in
  10.864 +      map2 mk_trsimp clauses psimps
  10.865 +    end
  10.866 +
  10.867 +
  10.868 +fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
  10.869 +    let
  10.870 +      val FunctionConfig {domintros, tailrec, default=default_str, ...} = config
  10.871 +
  10.872 +      val fvar = Free (fname, fT)
  10.873 +      val domT = domain_type fT
  10.874 +      val ranT = range_type fT
  10.875 +
  10.876 +      val default = Syntax.parse_term lthy default_str
  10.877 +        |> TypeInfer.constrain fT |> Syntax.check_term lthy
  10.878 +
  10.879 +      val (globals, ctxt') = fix_globals domT ranT fvar lthy
  10.880 +
  10.881 +      val Globals { x, h, ... } = globals
  10.882 +
  10.883 +      val clauses = map (mk_clause_context x ctxt') abstract_qglrs
  10.884 +
  10.885 +      val n = length abstract_qglrs
  10.886 +
  10.887 +      fun build_tree (ClauseContext { ctxt, rhs, ...}) =
  10.888 +            Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
  10.889 +
  10.890 +      val trees = map build_tree clauses
  10.891 +      val RCss = map find_calls trees
  10.892 +
  10.893 +      val ((G, GIntro_thms, G_elim, G_induct), lthy) =
  10.894 +          PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
  10.895 +
  10.896 +      val ((f, f_defthm), lthy) =
  10.897 +          PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
  10.898 +
  10.899 +      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
  10.900 +      val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
  10.901 +
  10.902 +      val ((R, RIntro_thmss, R_elim), lthy) =
  10.903 +          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
  10.904 +
  10.905 +      val (_, lthy) =
  10.906 +          LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
  10.907 +
  10.908 +      val newthy = ProofContext.theory_of lthy
  10.909 +      val clauses = map (transfer_clause_ctx newthy) clauses
  10.910 +
  10.911 +      val cert = cterm_of (ProofContext.theory_of lthy)
  10.912 +
  10.913 +      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
  10.914 +
  10.915 +      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
  10.916 +      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
  10.917 +
  10.918 +      val compat_store = store_compat_thms n compat
  10.919 +
  10.920 +      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm
  10.921 +
  10.922 +      val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
  10.923 +
  10.924 +      fun mk_partial_rules provedgoal =
  10.925 +          let
  10.926 +            val newthy = theory_of_thm provedgoal (*FIXME*)
  10.927 +
  10.928 +            val (graph_is_function, complete_thm) =
  10.929 +                provedgoal
  10.930 +                  |> Conjunction.elim
  10.931 +                  |> apfst (Thm.forall_elim_vars 0)
  10.932 +
  10.933 +            val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
  10.934 +
  10.935 +            val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
  10.936 +
  10.937 +            val simple_pinduct = PROFILE "Proving partial induction rule"
  10.938 +                                                           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
  10.939 +
  10.940 +
  10.941 +            val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
  10.942 +
  10.943 +            val dom_intros = if domintros
  10.944 +                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
  10.945 +                             else NONE
  10.946 +            val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
  10.947 +
  10.948 +          in
  10.949 +            FunctionResult {fs=[f], G=G, R=R, cases=complete_thm,
  10.950 +                          psimps=psimps, simple_pinducts=[simple_pinduct],
  10.951 +                          termination=total_intro, trsimps=trsimps,
  10.952 +                          domintros=dom_intros}
  10.953 +          end
  10.954 +    in
  10.955 +      ((f, goalstate, mk_partial_rules), lthy)
  10.956 +    end
  10.957 +
  10.958 +
  10.959 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Fri Oct 23 16:22:10 2009 +0200
    11.3 @@ -0,0 +1,180 @@
    11.4 +(*  Title:      HOL/Tools/Function/fundef_lib.ML
    11.5 +    Author:     Alexander Krauss, TU Muenchen
    11.6 +
    11.7 +A package for general recursive function definitions. 
    11.8 +Some fairly general functions that should probably go somewhere else... 
    11.9 +*)
   11.10 +
   11.11 +structure Function_Lib =
   11.12 +struct
   11.13 +
   11.14 +fun map_option f NONE = NONE 
   11.15 +  | map_option f (SOME x) = SOME (f x);
   11.16 +
   11.17 +fun fold_option f NONE y = y
   11.18 +  | fold_option f (SOME x) y = f x y;
   11.19 +
   11.20 +fun fold_map_option f NONE y = (NONE, y)
   11.21 +  | fold_map_option f (SOME x) y = apfst SOME (f x y);
   11.22 +
   11.23 +(* Ex: "The variable" ^ plural " is" "s are" vs *)
   11.24 +fun plural sg pl [x] = sg
   11.25 +  | plural sg pl _ = pl
   11.26 +
   11.27 +(* lambda-abstracts over an arbitrarily nested tuple
   11.28 +  ==> hologic.ML? *)
   11.29 +fun tupled_lambda vars t =
   11.30 +    case vars of
   11.31 +      (Free v) => lambda (Free v) t
   11.32 +    | (Var v) => lambda (Var v) t
   11.33 +    | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
   11.34 +      (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
   11.35 +    | _ => raise Match
   11.36 +                 
   11.37 +                 
   11.38 +fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
   11.39 +    let
   11.40 +      val (n, body) = Term.dest_abs a
   11.41 +    in
   11.42 +      (Free (n, T), body)
   11.43 +    end
   11.44 +  | dest_all _ = raise Match
   11.45 +                         
   11.46 +
   11.47 +(* Removes all quantifiers from a term, replacing bound variables by frees. *)
   11.48 +fun dest_all_all (t as (Const ("all",_) $ _)) = 
   11.49 +    let
   11.50 +      val (v,b) = dest_all t
   11.51 +      val (vs, b') = dest_all_all b
   11.52 +    in
   11.53 +      (v :: vs, b')
   11.54 +    end
   11.55 +  | dest_all_all t = ([],t)
   11.56 +                     
   11.57 +
   11.58 +(* FIXME: similar to Variable.focus *)
   11.59 +fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
   11.60 +    let
   11.61 +      val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
   11.62 +      val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
   11.63 +
   11.64 +      val (n'', body) = Term.dest_abs (n', T, b) 
   11.65 +      val _ = (n' = n'') orelse error "dest_all_ctx"
   11.66 +      (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
   11.67 +
   11.68 +      val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
   11.69 +    in
   11.70 +      (ctx'', (n', T) :: vs, bd)
   11.71 +    end
   11.72 +  | dest_all_all_ctx ctx t = 
   11.73 +    (ctx, [], t)
   11.74 +
   11.75 +
   11.76 +fun map3 _ [] [] [] = []
   11.77 +  | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
   11.78 +  | map3 _ _ _ _ = raise Library.UnequalLengths;
   11.79 +
   11.80 +fun map4 _ [] [] [] [] = []
   11.81 +  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
   11.82 +  | map4 _ _ _ _ _ = raise Library.UnequalLengths;
   11.83 +
   11.84 +fun map6 _ [] [] [] [] [] [] = []
   11.85 +  | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws
   11.86 +  | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths;
   11.87 +
   11.88 +fun map7 _ [] [] [] [] [] [] [] = []
   11.89 +  | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
   11.90 +  | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
   11.91 +
   11.92 +
   11.93 +
   11.94 +(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
   11.95 +(* ==> library *)
   11.96 +fun unordered_pairs [] = []
   11.97 +  | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
   11.98 +
   11.99 +
  11.100 +(* Replaces Frees by name. Works with loose Bounds. *)
  11.101 +fun replace_frees assoc =
  11.102 +    map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
  11.103 +                 | t => t)
  11.104 +
  11.105 +
  11.106 +fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
  11.107 +  | rename_bound n _ = raise Match
  11.108 +
  11.109 +fun mk_forall_rename (n, v) =
  11.110 +    rename_bound n o Logic.all v 
  11.111 +
  11.112 +fun forall_intr_rename (n, cv) thm =
  11.113 +    let
  11.114 +      val allthm = forall_intr cv thm
  11.115 +      val (_ $ abs) = prop_of allthm
  11.116 +    in
  11.117 +      Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
  11.118 +    end
  11.119 +
  11.120 +
  11.121 +(* Returns the frees in a term in canonical order, excluding the fixes from the context *)
  11.122 +fun frees_in_term ctxt t =
  11.123 +    Term.add_frees t []
  11.124 +    |> filter_out (Variable.is_fixed ctxt o fst)
  11.125 +    |> rev
  11.126 +
  11.127 +
  11.128 +datatype proof_attempt = Solved of thm | Stuck of thm | Fail
  11.129 +
  11.130 +fun try_proof cgoal tac = 
  11.131 +    case SINGLE tac (Goal.init cgoal) of
  11.132 +      NONE => Fail
  11.133 +    | SOME st =>
  11.134 +        if Thm.no_prems st
  11.135 +        then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
  11.136 +        else Stuck st
  11.137 +
  11.138 +
  11.139 +fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = 
  11.140 +    if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
  11.141 +  | dest_binop_list _ t = [ t ]
  11.142 +
  11.143 +
  11.144 +(* separate two parts in a +-expression:
  11.145 +   "a + b + c + d + e" --> "(a + b + d) + (c + e)"
  11.146 +
  11.147 +   Here, + can be any binary operation that is AC.
  11.148 +
  11.149 +   cn - The name of the binop-constructor (e.g. @{const_name Un})
  11.150 +   ac - the AC rewrite rules for cn
  11.151 +   is - the list of indices of the expressions that should become the first part
  11.152 +        (e.g. [0,1,3] in the above example)
  11.153 +*)
  11.154 +
  11.155 +fun regroup_conv neu cn ac is ct =
  11.156 + let
  11.157 +   val mk = HOLogic.mk_binop cn
  11.158 +   val t = term_of ct
  11.159 +   val xs = dest_binop_list cn t
  11.160 +   val js = subtract (op =) is (0 upto (length xs) - 1)
  11.161 +   val ty = fastype_of t
  11.162 +   val thy = theory_of_cterm ct
  11.163 + in
  11.164 +   Goal.prove_internal []
  11.165 +     (cterm_of thy
  11.166 +       (Logic.mk_equals (t,
  11.167 +          if is = []
  11.168 +          then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
  11.169 +          else if js = []
  11.170 +            then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
  11.171 +            else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
  11.172 +     (K (rewrite_goals_tac ac
  11.173 +         THEN rtac Drule.reflexive_thm 1))
  11.174 + end
  11.175 +
  11.176 +(* instance for unions *)
  11.177 +fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
  11.178 +  (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
  11.179 +                                     @{thms Un_empty_right} @
  11.180 +                                     @{thms Un_empty_left})) t
  11.181 +
  11.182 +
  11.183 +end
    12.1 --- a/src/HOL/Tools/Function/fundef.ML	Fri Oct 23 15:33:19 2009 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,226 +0,0 @@
    12.4 -(*  Title:      HOL/Tools/Function/fundef.ML
    12.5 -    Author:     Alexander Krauss, TU Muenchen
    12.6 -
    12.7 -A package for general recursive function definitions.
    12.8 -Isar commands.
    12.9 -*)
   12.10 -
   12.11 -signature FUNDEF =
   12.12 -sig
   12.13 -    val add_fundef :  (binding * typ option * mixfix) list
   12.14 -                       -> (Attrib.binding * term) list
   12.15 -                       -> FundefCommon.fundef_config
   12.16 -                       -> local_theory
   12.17 -                       -> Proof.state
   12.18 -    val add_fundef_cmd :  (binding * string option * mixfix) list
   12.19 -                      -> (Attrib.binding * string) list
   12.20 -                      -> FundefCommon.fundef_config
   12.21 -                      -> local_theory
   12.22 -                      -> Proof.state
   12.23 -
   12.24 -    val termination_proof : term option -> local_theory -> Proof.state
   12.25 -    val termination_proof_cmd : string option -> local_theory -> Proof.state
   12.26 -    val termination : term option -> local_theory -> Proof.state
   12.27 -    val termination_cmd : string option -> local_theory -> Proof.state
   12.28 -
   12.29 -    val setup : theory -> theory
   12.30 -    val get_congs : Proof.context -> thm list
   12.31 -end
   12.32 -
   12.33 -
   12.34 -structure Fundef : FUNDEF =
   12.35 -struct
   12.36 -
   12.37 -open FundefLib
   12.38 -open FundefCommon
   12.39 -
   12.40 -val simp_attribs = map (Attrib.internal o K)
   12.41 -    [Simplifier.simp_add,
   12.42 -     Code.add_default_eqn_attribute,
   12.43 -     Nitpick_Simps.add,
   12.44 -     Quickcheck_RecFun_Simps.add]
   12.45 -
   12.46 -val psimp_attribs = map (Attrib.internal o K)
   12.47 -    [Simplifier.simp_add,
   12.48 -     Nitpick_Psimps.add]
   12.49 -
   12.50 -fun note_theorem ((name, atts), ths) =
   12.51 -  LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
   12.52 -
   12.53 -fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
   12.54 -
   12.55 -fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
   12.56 -    let
   12.57 -      val spec = post simps
   12.58 -                   |> map (apfst (apsnd (fn ats => moreatts @ ats)))
   12.59 -                   |> map (apfst (apfst extra_qualify))
   12.60 -
   12.61 -      val (saved_spec_simps, lthy) =
   12.62 -        fold_map (LocalTheory.note Thm.generatedK) spec lthy
   12.63 -
   12.64 -      val saved_simps = maps snd saved_spec_simps
   12.65 -      val simps_by_f = sort saved_simps
   12.66 -
   12.67 -      fun add_for_f fname simps =
   12.68 -        note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
   12.69 -    in
   12.70 -      (saved_simps,
   12.71 -       fold2 add_for_f fnames simps_by_f lthy)
   12.72 -    end
   12.73 -
   12.74 -fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy =
   12.75 -    let
   12.76 -      val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
   12.77 -      val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
   12.78 -      val fixes = map (apfst (apfst Binding.name_of)) fixes0;
   12.79 -      val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
   12.80 -      val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec
   12.81 -
   12.82 -      val defname = mk_defname fixes
   12.83 -
   12.84 -      val ((goalstate, cont), lthy) =
   12.85 -          FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy
   12.86 -
   12.87 -      fun afterqed [[proof]] lthy =
   12.88 -        let
   12.89 -          val FundefResult {fs, R, psimps, trsimps,  simple_pinducts, termination,
   12.90 -                            domintros, cases, ...} =
   12.91 -          cont (Thm.close_derivation proof)
   12.92 -
   12.93 -          val fnames = map (fst o fst) fixes
   12.94 -          val qualify = Long_Name.qualify defname
   12.95 -          val addsmps = add_simps fnames post sort_cont
   12.96 -
   12.97 -          val (((psimps', pinducts'), (_, [termination'])), lthy) =
   12.98 -            lthy
   12.99 -            |> addsmps (Binding.qualify false "partial") "psimps"
  12.100 -                 psimp_attribs psimps
  12.101 -            ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
  12.102 -            ||>> note_theorem ((qualify "pinduct",
  12.103 -                   [Attrib.internal (K (RuleCases.case_names cnames)),
  12.104 -                    Attrib.internal (K (RuleCases.consumes 1)),
  12.105 -                    Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
  12.106 -            ||>> note_theorem ((qualify "termination", []), [termination])
  12.107 -            ||> (snd o note_theorem ((qualify "cases",
  12.108 -                   [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
  12.109 -            ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
  12.110 -
  12.111 -          val cdata = FundefCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
  12.112 -                                      pinducts=snd pinducts', termination=termination',
  12.113 -                                      fs=fs, R=R, defname=defname }
  12.114 -          val _ =
  12.115 -            if not is_external then ()
  12.116 -            else Specification.print_consts lthy (K false) (map fst fixes)
  12.117 -        in
  12.118 -          lthy
  12.119 -          |> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
  12.120 -        end
  12.121 -    in
  12.122 -      lthy
  12.123 -        |> is_external ? LocalTheory.set_group (serial_string ())
  12.124 -        |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
  12.125 -        |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
  12.126 -    end
  12.127 -
  12.128 -val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
  12.129 -val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type"
  12.130 -
  12.131 -fun gen_termination_proof prep_term raw_term_opt lthy =
  12.132 -    let
  12.133 -      val term_opt = Option.map (prep_term lthy) raw_term_opt
  12.134 -      val data = the (case term_opt of
  12.135 -                        SOME t => (import_fundef_data t lthy
  12.136 -                          handle Option.Option =>
  12.137 -                            error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
  12.138 -                      | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function"))
  12.139 -
  12.140 -        val FundefCtxData { termination, R, add_simps, case_names, psimps,
  12.141 -                            pinducts, defname, ...} = data
  12.142 -        val domT = domain_type (fastype_of R)
  12.143 -        val goal = HOLogic.mk_Trueprop
  12.144 -                     (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
  12.145 -        fun afterqed [[totality]] lthy =
  12.146 -          let
  12.147 -            val totality = Thm.close_derivation totality
  12.148 -            val remove_domain_condition =
  12.149 -              full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
  12.150 -            val tsimps = map remove_domain_condition psimps
  12.151 -            val tinduct = map remove_domain_condition pinducts
  12.152 -            val qualify = Long_Name.qualify defname;
  12.153 -          in
  12.154 -            lthy
  12.155 -            |> add_simps I "simps" simp_attribs tsimps |> snd
  12.156 -            |> note_theorem
  12.157 -               ((qualify "induct",
  12.158 -                 [Attrib.internal (K (RuleCases.case_names case_names))]),
  12.159 -                tinduct) |> snd
  12.160 -          end
  12.161 -    in
  12.162 -      lthy
  12.163 -      |> ProofContext.note_thmss ""
  12.164 -         [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
  12.165 -      |> ProofContext.note_thmss ""
  12.166 -         [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
  12.167 -      |> ProofContext.note_thmss ""
  12.168 -         [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
  12.169 -           [([Goal.norm_result termination], [])])] |> snd
  12.170 -      |> Proof.theorem_i NONE afterqed [[(goal, [])]]
  12.171 -    end
  12.172 -
  12.173 -val termination_proof = gen_termination_proof Syntax.check_term;
  12.174 -val termination_proof_cmd = gen_termination_proof Syntax.read_term;
  12.175 -
  12.176 -fun termination term_opt lthy =
  12.177 -  lthy
  12.178 -  |> LocalTheory.set_group (serial_string ())
  12.179 -  |> termination_proof term_opt;
  12.180 -
  12.181 -fun termination_cmd term_opt lthy =
  12.182 -  lthy
  12.183 -  |> LocalTheory.set_group (serial_string ())
  12.184 -  |> termination_proof_cmd term_opt;
  12.185 -
  12.186 -
  12.187 -(* Datatype hook to declare datatype congs as "fundef_congs" *)
  12.188 -
  12.189 -
  12.190 -fun add_case_cong n thy =
  12.191 -    Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm
  12.192 -                          (Datatype.the_info thy n
  12.193 -                           |> #case_cong
  12.194 -                           |> safe_mk_meta_eq)))
  12.195 -                       thy
  12.196 -
  12.197 -val setup_case_cong = Datatype.interpretation (K (fold add_case_cong))
  12.198 -
  12.199 -
  12.200 -(* setup *)
  12.201 -
  12.202 -val setup =
  12.203 -  Attrib.setup @{binding fundef_cong}
  12.204 -    (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del)
  12.205 -    "declaration of congruence rule for function definitions"
  12.206 -  #> setup_case_cong
  12.207 -  #> FundefRelation.setup
  12.208 -  #> FundefCommon.Termination_Simps.setup
  12.209 -
  12.210 -val get_congs = FundefCtxTree.get_fundef_congs
  12.211 -
  12.212 -
  12.213 -(* outer syntax *)
  12.214 -
  12.215 -local structure P = OuterParse and K = OuterKeyword in
  12.216 -
  12.217 -val _ =
  12.218 -  OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
  12.219 -  (fundef_parser default_config
  12.220 -     >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config));
  12.221 -
  12.222 -val _ =
  12.223 -  OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
  12.224 -  (Scan.option P.term >> termination_cmd);
  12.225 -
  12.226 -end;
  12.227 -
  12.228 -
  12.229 -end
    13.1 --- a/src/HOL/Tools/Function/fundef_common.ML	Fri Oct 23 15:33:19 2009 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,343 +0,0 @@
    13.4 -(*  Title:      HOL/Tools/Function/fundef_common.ML
    13.5 -    Author:     Alexander Krauss, TU Muenchen
    13.6 -
    13.7 -A package for general recursive function definitions. 
    13.8 -Common definitions and other infrastructure.
    13.9 -*)
   13.10 -
   13.11 -structure FundefCommon =
   13.12 -struct
   13.13 -
   13.14 -local open FundefLib in
   13.15 -
   13.16 -(* Profiling *)
   13.17 -val profile = Unsynchronized.ref false;
   13.18 -
   13.19 -fun PROFILE msg = if !profile then timeap_msg msg else I
   13.20 -
   13.21 -
   13.22 -val acc_const_name = @{const_name accp}
   13.23 -fun mk_acc domT R =
   13.24 -    Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
   13.25 -
   13.26 -val function_name = suffix "C"
   13.27 -val graph_name = suffix "_graph"
   13.28 -val rel_name = suffix "_rel"
   13.29 -val dom_name = suffix "_dom"
   13.30 -
   13.31 -(* Termination rules *)
   13.32 -
   13.33 -structure TerminationRule = GenericDataFun
   13.34 -(
   13.35 -  type T = thm list
   13.36 -  val empty = []
   13.37 -  val extend = I
   13.38 -  fun merge _ = Thm.merge_thms
   13.39 -);
   13.40 -
   13.41 -val get_termination_rules = TerminationRule.get
   13.42 -val store_termination_rule = TerminationRule.map o cons
   13.43 -val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof
   13.44 -
   13.45 -
   13.46 -(* Function definition result data *)
   13.47 -
   13.48 -datatype fundef_result =
   13.49 -  FundefResult of
   13.50 -     {
   13.51 -      fs: term list,
   13.52 -      G: term,
   13.53 -      R: term,
   13.54 -
   13.55 -      psimps : thm list, 
   13.56 -      trsimps : thm list option, 
   13.57 -
   13.58 -      simple_pinducts : thm list, 
   13.59 -      cases : thm,
   13.60 -      termination : thm,
   13.61 -      domintros : thm list option
   13.62 -     }
   13.63 -
   13.64 -
   13.65 -datatype fundef_context_data =
   13.66 -  FundefCtxData of
   13.67 -     {
   13.68 -      defname : string,
   13.69 -
   13.70 -      (* contains no logical entities: invariant under morphisms *)
   13.71 -      add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list 
   13.72 -                  -> local_theory -> thm list * local_theory,
   13.73 -      case_names : string list,
   13.74 -
   13.75 -      fs : term list,
   13.76 -      R : term,
   13.77 -      
   13.78 -      psimps: thm list,
   13.79 -      pinducts: thm list,
   13.80 -      termination: thm
   13.81 -     }
   13.82 -
   13.83 -fun morph_fundef_data (FundefCtxData {add_simps, case_names, fs, R, 
   13.84 -                                      psimps, pinducts, termination, defname}) phi =
   13.85 -    let
   13.86 -      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
   13.87 -      val name = Binding.name_of o Morphism.binding phi o Binding.name
   13.88 -    in
   13.89 -      FundefCtxData { add_simps = add_simps, case_names = case_names,
   13.90 -                      fs = map term fs, R = term R, psimps = fact psimps, 
   13.91 -                      pinducts = fact pinducts, termination = thm termination,
   13.92 -                      defname = name defname }
   13.93 -    end
   13.94 -
   13.95 -structure FundefData = GenericDataFun
   13.96 -(
   13.97 -  type T = (term * fundef_context_data) Item_Net.T;
   13.98 -  val empty = Item_Net.init
   13.99 -    (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
  13.100 -    fst;
  13.101 -  val copy = I;
  13.102 -  val extend = I;
  13.103 -  fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
  13.104 -);
  13.105 -
  13.106 -val get_fundef = FundefData.get o Context.Proof;
  13.107 -
  13.108 -
  13.109 -(* Generally useful?? *)
  13.110 -fun lift_morphism thy f = 
  13.111 -    let 
  13.112 -      val term = Drule.term_rule thy f
  13.113 -    in
  13.114 -      Morphism.thm_morphism f $> Morphism.term_morphism term 
  13.115 -       $> Morphism.typ_morphism (Logic.type_map term)
  13.116 -    end
  13.117 -
  13.118 -fun import_fundef_data t ctxt =
  13.119 -    let
  13.120 -      val thy = ProofContext.theory_of ctxt
  13.121 -      val ct = cterm_of thy t
  13.122 -      val inst_morph = lift_morphism thy o Thm.instantiate 
  13.123 -
  13.124 -      fun match (trm, data) = 
  13.125 -          SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
  13.126 -          handle Pattern.MATCH => NONE
  13.127 -    in 
  13.128 -      get_first match (Item_Net.retrieve (get_fundef ctxt) t)
  13.129 -    end
  13.130 -
  13.131 -fun import_last_fundef ctxt =
  13.132 -    case Item_Net.content (get_fundef ctxt) of
  13.133 -      [] => NONE
  13.134 -    | (t, data) :: _ =>
  13.135 -      let 
  13.136 -        val ([t'], ctxt') = Variable.import_terms true [t] ctxt
  13.137 -      in
  13.138 -        import_fundef_data t' ctxt'
  13.139 -      end
  13.140 -
  13.141 -val all_fundef_data = Item_Net.content o get_fundef
  13.142 -
  13.143 -fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
  13.144 -    FundefData.map (fold (fn f => Item_Net.insert (f, data)) fs)
  13.145 -    #> store_termination_rule termination
  13.146 -
  13.147 -
  13.148 -(* Simp rules for termination proofs *)
  13.149 -
  13.150 -structure Termination_Simps = Named_Thms
  13.151 -(
  13.152 -  val name = "termination_simp" 
  13.153 -  val description = "Simplification rule for termination proofs"
  13.154 -);
  13.155 -
  13.156 -
  13.157 -(* Default Termination Prover *)
  13.158 -
  13.159 -structure TerminationProver = GenericDataFun
  13.160 -(
  13.161 -  type T = Proof.context -> Proof.method
  13.162 -  val empty = (fn _ => error "Termination prover not configured")
  13.163 -  val extend = I
  13.164 -  fun merge _ (a,b) = b (* FIXME *)
  13.165 -);
  13.166 -
  13.167 -val set_termination_prover = TerminationProver.put
  13.168 -val get_termination_prover = TerminationProver.get o Context.Proof
  13.169 -
  13.170 -
  13.171 -(* Configuration management *)
  13.172 -datatype fundef_opt 
  13.173 -  = Sequential
  13.174 -  | Default of string
  13.175 -  | DomIntros
  13.176 -  | Tailrec
  13.177 -
  13.178 -datatype fundef_config
  13.179 -  = FundefConfig of
  13.180 -   {
  13.181 -    sequential: bool,
  13.182 -    default: string,
  13.183 -    domintros: bool,
  13.184 -    tailrec: bool
  13.185 -   }
  13.186 -
  13.187 -fun apply_opt Sequential (FundefConfig {sequential, default, domintros,tailrec}) = 
  13.188 -    FundefConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec}
  13.189 -  | apply_opt (Default d) (FundefConfig {sequential, default, domintros,tailrec}) = 
  13.190 -    FundefConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec}
  13.191 -  | apply_opt DomIntros (FundefConfig {sequential, default, domintros,tailrec}) =
  13.192 -    FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec}
  13.193 -  | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) =
  13.194 -    FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
  13.195 -
  13.196 -val default_config =
  13.197 -  FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), 
  13.198 -                 domintros=false, tailrec=false }
  13.199 -
  13.200 -
  13.201 -(* Analyzing function equations *)
  13.202 -
  13.203 -fun split_def ctxt geq =
  13.204 -    let
  13.205 -      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
  13.206 -      val qs = Term.strip_qnt_vars "all" geq
  13.207 -      val imp = Term.strip_qnt_body "all" geq
  13.208 -      val (gs, eq) = Logic.strip_horn imp
  13.209 -
  13.210 -      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
  13.211 -          handle TERM _ => error (input_error "Not an equation")
  13.212 -
  13.213 -      val (head, args) = strip_comb f_args
  13.214 -
  13.215 -      val fname = fst (dest_Free head)
  13.216 -          handle TERM _ => error (input_error "Head symbol must not be a bound variable")
  13.217 -    in
  13.218 -      (fname, qs, gs, args, rhs)
  13.219 -    end
  13.220 -
  13.221 -(* Check for all sorts of errors in the input *)
  13.222 -fun check_defs ctxt fixes eqs =
  13.223 -    let
  13.224 -      val fnames = map (fst o fst) fixes
  13.225 -                                
  13.226 -      fun check geq = 
  13.227 -          let
  13.228 -            fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq])
  13.229 -                                  
  13.230 -            val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
  13.231 -                                 
  13.232 -            val _ = fname mem fnames 
  13.233 -                    orelse input_error 
  13.234 -                             ("Head symbol of left hand side must be " 
  13.235 -                              ^ plural "" "one out of " fnames ^ commas_quote fnames)
  13.236 -                                            
  13.237 -            val _ = length args > 0 orelse input_error "Function has no arguments:"
  13.238 -
  13.239 -            fun add_bvs t is = add_loose_bnos (t, 0, is)
  13.240 -            val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
  13.241 -                        |> map (fst o nth (rev qs))
  13.242 -                      
  13.243 -            val _ = null rvs orelse input_error 
  13.244 -                        ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
  13.245 -                         ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
  13.246 -                                    
  13.247 -            val _ = forall (not o Term.exists_subterm 
  13.248 -                             (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args)
  13.249 -                    orelse input_error "Defined function may not occur in premises or arguments"
  13.250 -
  13.251 -            val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args
  13.252 -            val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs
  13.253 -            val _ = null funvars
  13.254 -                    orelse (warning (cat_lines 
  13.255 -                    ["Bound variable" ^ plural " " "s " funvars 
  13.256 -                     ^ commas_quote (map fst funvars) ^  
  13.257 -                     " occur" ^ plural "s" "" funvars ^ " in function position.",  
  13.258 -                     "Misspelled constructor???"]); true)
  13.259 -          in
  13.260 -            (fname, length args)
  13.261 -          end
  13.262 -
  13.263 -      val _ = AList.group (op =) (map check eqs)
  13.264 -        |> map (fn (fname, ars) =>
  13.265 -             length (distinct (op =) ars) = 1
  13.266 -             orelse error ("Function " ^ quote fname ^
  13.267 -                           " has different numbers of arguments in different equations"))
  13.268 -
  13.269 -      fun check_sorts ((fname, fT), _) =
  13.270 -          Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
  13.271 -          orelse error (cat_lines 
  13.272 -          ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
  13.273 -           setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
  13.274 -
  13.275 -      val _ = map check_sorts fixes
  13.276 -    in
  13.277 -      ()
  13.278 -    end
  13.279 -
  13.280 -(* Preprocessors *)
  13.281 -
  13.282 -type fixes = ((string * typ) * mixfix) list
  13.283 -type 'a spec = (Attrib.binding * 'a list) list
  13.284 -type preproc = fundef_config -> Proof.context -> fixes -> term spec 
  13.285 -               -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
  13.286 -
  13.287 -val fname_of = fst o dest_Free o fst o strip_comb o fst 
  13.288 - o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all
  13.289 -
  13.290 -fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k
  13.291 -  | mk_case_names _ n 0 = []
  13.292 -  | mk_case_names _ n 1 = [n]
  13.293 -  | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
  13.294 -
  13.295 -fun empty_preproc check _ ctxt fixes spec =
  13.296 -    let 
  13.297 -      val (bnds, tss) = split_list spec
  13.298 -      val ts = flat tss
  13.299 -      val _ = check ctxt fixes ts
  13.300 -      val fnames = map (fst o fst) fixes
  13.301 -      val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts
  13.302 -
  13.303 -      fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) 
  13.304 -                                   (indices ~~ xs)
  13.305 -                        |> map (map snd)
  13.306 -
  13.307 -      (* using theorem names for case name currently disabled *)
  13.308 -      val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
  13.309 -    in
  13.310 -      (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
  13.311 -    end
  13.312 -
  13.313 -structure Preprocessor = GenericDataFun
  13.314 -(
  13.315 -  type T = preproc
  13.316 -  val empty : T = empty_preproc check_defs
  13.317 -  val extend = I
  13.318 -  fun merge _ (a, _) = a
  13.319 -);
  13.320 -
  13.321 -val get_preproc = Preprocessor.get o Context.Proof
  13.322 -val set_preproc = Preprocessor.map o K
  13.323 -
  13.324 -
  13.325 -
  13.326 -local 
  13.327 -  structure P = OuterParse and K = OuterKeyword
  13.328 -
  13.329 -  val option_parser = 
  13.330 -      P.group "option" ((P.reserved "sequential" >> K Sequential)
  13.331 -                    || ((P.reserved "default" |-- P.term) >> Default)
  13.332 -                    || (P.reserved "domintros" >> K DomIntros)
  13.333 -                    || (P.reserved "tailrec" >> K Tailrec))
  13.334 -
  13.335 -  fun config_parser default = 
  13.336 -      (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
  13.337 -        >> (fn opts => fold apply_opt opts default)
  13.338 -in
  13.339 -  fun fundef_parser default_cfg = 
  13.340 -      config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
  13.341 -end
  13.342 -
  13.343 -
  13.344 -end
  13.345 -end
  13.346 -
    14.1 --- a/src/HOL/Tools/Function/fundef_core.ML	Fri Oct 23 15:33:19 2009 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,956 +0,0 @@
    14.4 -(*  Title:      HOL/Tools/Function/fundef_core.ML
    14.5 -    Author:     Alexander Krauss, TU Muenchen
    14.6 -
    14.7 -A package for general recursive function definitions:
    14.8 -Main functionality.
    14.9 -*)
   14.10 -
   14.11 -signature FUNDEF_CORE =
   14.12 -sig
   14.13 -    val trace: bool Unsynchronized.ref
   14.14 -
   14.15 -    val prepare_fundef : FundefCommon.fundef_config
   14.16 -                         -> string (* defname *)
   14.17 -                         -> ((bstring * typ) * mixfix) list (* defined symbol *)
   14.18 -                         -> ((bstring * typ) list * term list * term * term) list (* specification *)
   14.19 -                         -> local_theory
   14.20 -
   14.21 -                         -> (term   (* f *)
   14.22 -                             * thm  (* goalstate *)
   14.23 -                             * (thm -> FundefCommon.fundef_result) (* continuation *)
   14.24 -                            ) * local_theory
   14.25 -
   14.26 -end
   14.27 -
   14.28 -structure FundefCore : FUNDEF_CORE =
   14.29 -struct
   14.30 -
   14.31 -val trace = Unsynchronized.ref false;
   14.32 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
   14.33 -
   14.34 -val boolT = HOLogic.boolT
   14.35 -val mk_eq = HOLogic.mk_eq
   14.36 -
   14.37 -open FundefLib
   14.38 -open FundefCommon
   14.39 -
   14.40 -datatype globals =
   14.41 -   Globals of {
   14.42 -         fvar: term,
   14.43 -         domT: typ,
   14.44 -         ranT: typ,
   14.45 -         h: term,
   14.46 -         y: term,
   14.47 -         x: term,
   14.48 -         z: term,
   14.49 -         a: term,
   14.50 -         P: term,
   14.51 -         D: term,
   14.52 -         Pbool:term
   14.53 -}
   14.54 -
   14.55 -
   14.56 -datatype rec_call_info =
   14.57 -  RCInfo of
   14.58 -  {
   14.59 -   RIvs: (string * typ) list,  (* Call context: fixes and assumes *)
   14.60 -   CCas: thm list,
   14.61 -   rcarg: term,                 (* The recursive argument *)
   14.62 -
   14.63 -   llRI: thm,
   14.64 -   h_assum: term
   14.65 -  }
   14.66 -
   14.67 -
   14.68 -datatype clause_context =
   14.69 -  ClauseContext of
   14.70 -  {
   14.71 -    ctxt : Proof.context,
   14.72 -
   14.73 -    qs : term list,
   14.74 -    gs : term list,
   14.75 -    lhs: term,
   14.76 -    rhs: term,
   14.77 -
   14.78 -    cqs: cterm list,
   14.79 -    ags: thm list,
   14.80 -    case_hyp : thm
   14.81 -  }
   14.82 -
   14.83 -
   14.84 -fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
   14.85 -    ClauseContext { ctxt = ProofContext.transfer thy ctxt,
   14.86 -                    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
   14.87 -
   14.88 -
   14.89 -datatype clause_info =
   14.90 -  ClauseInfo of
   14.91 -     {
   14.92 -      no: int,
   14.93 -      qglr : ((string * typ) list * term list * term * term),
   14.94 -      cdata : clause_context,
   14.95 -
   14.96 -      tree: FundefCtxTree.ctx_tree,
   14.97 -      lGI: thm,
   14.98 -      RCs: rec_call_info list
   14.99 -     }
  14.100 -
  14.101 -
  14.102 -(* Theory dependencies. *)
  14.103 -val Pair_inject = @{thm Product_Type.Pair_inject};
  14.104 -
  14.105 -val acc_induct_rule = @{thm accp_induct_rule};
  14.106 -
  14.107 -val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
  14.108 -val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness};
  14.109 -val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff};
  14.110 -
  14.111 -val acc_downward = @{thm accp_downward};
  14.112 -val accI = @{thm accp.accI};
  14.113 -val case_split = @{thm HOL.case_split};
  14.114 -val fundef_default_value = @{thm FunDef.fundef_default_value};
  14.115 -val not_acc_down = @{thm not_accp_down};
  14.116 -
  14.117 -
  14.118 -
  14.119 -fun find_calls tree =
  14.120 -    let
  14.121 -      fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
  14.122 -        | add_Ri _ _ _ _ = raise Match
  14.123 -    in
  14.124 -      rev (FundefCtxTree.traverse_tree add_Ri tree [])
  14.125 -    end
  14.126 -
  14.127 -
  14.128 -(** building proof obligations *)
  14.129 -
  14.130 -fun mk_compat_proof_obligations domT ranT fvar f glrs =
  14.131 -    let
  14.132 -      fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
  14.133 -          let
  14.134 -            val shift = incr_boundvars (length qs')
  14.135 -          in
  14.136 -            Logic.mk_implies
  14.137 -              (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),
  14.138 -                HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))
  14.139 -              |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
  14.140 -              |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')
  14.141 -              |> curry abstract_over fvar
  14.142 -              |> curry subst_bound f
  14.143 -          end
  14.144 -    in
  14.145 -      map mk_impl (unordered_pairs glrs)
  14.146 -    end
  14.147 -
  14.148 -
  14.149 -fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
  14.150 -    let
  14.151 -        fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
  14.152 -            HOLogic.mk_Trueprop Pbool
  14.153 -                     |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))
  14.154 -                     |> fold_rev (curry Logic.mk_implies) gs
  14.155 -                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  14.156 -    in
  14.157 -        HOLogic.mk_Trueprop Pbool
  14.158 -                 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
  14.159 -                 |> mk_forall_rename ("x", x)
  14.160 -                 |> mk_forall_rename ("P", Pbool)
  14.161 -    end
  14.162 -
  14.163 -(** making a context with it's own local bindings **)
  14.164 -
  14.165 -fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
  14.166 -    let
  14.167 -      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
  14.168 -                                           |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
  14.169 -
  14.170 -      val thy = ProofContext.theory_of ctxt'
  14.171 -
  14.172 -      fun inst t = subst_bounds (rev qs, t)
  14.173 -      val gs = map inst pre_gs
  14.174 -      val lhs = inst pre_lhs
  14.175 -      val rhs = inst pre_rhs
  14.176 -
  14.177 -      val cqs = map (cterm_of thy) qs
  14.178 -      val ags = map (assume o cterm_of thy) gs
  14.179 -
  14.180 -      val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
  14.181 -    in
  14.182 -      ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
  14.183 -                      cqs = cqs, ags = ags, case_hyp = case_hyp }
  14.184 -    end
  14.185 -
  14.186 -
  14.187 -(* lowlevel term function. FIXME: remove *)
  14.188 -fun abstract_over_list vs body =
  14.189 -  let
  14.190 -    fun abs lev v tm =
  14.191 -      if v aconv tm then Bound lev
  14.192 -      else
  14.193 -        (case tm of
  14.194 -          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
  14.195 -        | t $ u => abs lev v t $ abs lev v u
  14.196 -        | t => t);
  14.197 -  in
  14.198 -    fold_index (fn (i, v) => fn t => abs i v t) vs body
  14.199 -  end
  14.200 -
  14.201 -
  14.202 -
  14.203 -fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
  14.204 -    let
  14.205 -        val Globals {h, fvar, x, ...} = globals
  14.206 -
  14.207 -        val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
  14.208 -        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
  14.209 -
  14.210 -        (* Instantiate the GIntro thm with "f" and import into the clause context. *)
  14.211 -        val lGI = GIntro_thm
  14.212 -                    |> forall_elim (cert f)
  14.213 -                    |> fold forall_elim cqs
  14.214 -                    |> fold Thm.elim_implies ags
  14.215 -
  14.216 -        fun mk_call_info (rcfix, rcassm, rcarg) RI =
  14.217 -            let
  14.218 -                val llRI = RI
  14.219 -                             |> fold forall_elim cqs
  14.220 -                             |> fold (forall_elim o cert o Free) rcfix
  14.221 -                             |> fold Thm.elim_implies ags
  14.222 -                             |> fold Thm.elim_implies rcassm
  14.223 -
  14.224 -                val h_assum =
  14.225 -                    HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
  14.226 -                              |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  14.227 -                              |> fold_rev (Logic.all o Free) rcfix
  14.228 -                              |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
  14.229 -                              |> abstract_over_list (rev qs)
  14.230 -            in
  14.231 -                RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
  14.232 -            end
  14.233 -
  14.234 -        val RC_infos = map2 mk_call_info RCs RIntro_thms
  14.235 -    in
  14.236 -        ClauseInfo
  14.237 -            {
  14.238 -             no=no,
  14.239 -             cdata=cdata,
  14.240 -             qglr=qglr,
  14.241 -
  14.242 -             lGI=lGI,
  14.243 -             RCs=RC_infos,
  14.244 -             tree=tree
  14.245 -            }
  14.246 -    end
  14.247 -
  14.248 -
  14.249 -
  14.250 -
  14.251 -
  14.252 -
  14.253 -
  14.254 -(* replace this by a table later*)
  14.255 -fun store_compat_thms 0 thms = []
  14.256 -  | store_compat_thms n thms =
  14.257 -    let
  14.258 -        val (thms1, thms2) = chop n thms
  14.259 -    in
  14.260 -        (thms1 :: store_compat_thms (n - 1) thms2)
  14.261 -    end
  14.262 -
  14.263 -(* expects i <= j *)
  14.264 -fun lookup_compat_thm i j cts =
  14.265 -    nth (nth cts (i - 1)) (j - i)
  14.266 -
  14.267 -(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
  14.268 -(* if j < i, then turn around *)
  14.269 -fun get_compat_thm thy cts i j ctxi ctxj =
  14.270 -    let
  14.271 -      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
  14.272 -      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
  14.273 -
  14.274 -      val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))
  14.275 -    in if j < i then
  14.276 -         let
  14.277 -           val compat = lookup_compat_thm j i cts
  14.278 -         in
  14.279 -           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
  14.280 -                |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
  14.281 -                |> fold Thm.elim_implies agsj
  14.282 -                |> fold Thm.elim_implies agsi
  14.283 -                |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
  14.284 -         end
  14.285 -       else
  14.286 -         let
  14.287 -           val compat = lookup_compat_thm i j cts
  14.288 -         in
  14.289 -               compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
  14.290 -                 |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
  14.291 -                 |> fold Thm.elim_implies agsi
  14.292 -                 |> fold Thm.elim_implies agsj
  14.293 -                 |> Thm.elim_implies (assume lhsi_eq_lhsj)
  14.294 -                 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
  14.295 -         end
  14.296 -    end
  14.297 -
  14.298 -
  14.299 -
  14.300 -
  14.301 -(* Generates the replacement lemma in fully quantified form. *)
  14.302 -fun mk_replacement_lemma thy h ih_elim clause =
  14.303 -    let
  14.304 -        val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
  14.305 -        local open Conv in
  14.306 -        val ih_conv = arg1_conv o arg_conv o arg_conv
  14.307 -        end
  14.308 -
  14.309 -        val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
  14.310 -
  14.311 -        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
  14.312 -        val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
  14.313 -
  14.314 -        val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
  14.315 -
  14.316 -        val replace_lemma = (eql RS meta_eq_to_obj_eq)
  14.317 -                                |> implies_intr (cprop_of case_hyp)
  14.318 -                                |> fold_rev (implies_intr o cprop_of) h_assums
  14.319 -                                |> fold_rev (implies_intr o cprop_of) ags
  14.320 -                                |> fold_rev forall_intr cqs
  14.321 -                                |> Thm.close_derivation
  14.322 -    in
  14.323 -      replace_lemma
  14.324 -    end
  14.325 -
  14.326 -
  14.327 -fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
  14.328 -    let
  14.329 -        val Globals {h, y, x, fvar, ...} = globals
  14.330 -        val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
  14.331 -        val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
  14.332 -
  14.333 -        val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
  14.334 -            = mk_clause_context x ctxti cdescj
  14.335 -
  14.336 -        val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
  14.337 -        val compat = get_compat_thm thy compat_store i j cctxi cctxj
  14.338 -        val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
  14.339 -
  14.340 -        val RLj_import =
  14.341 -            RLj |> fold forall_elim cqsj'
  14.342 -                |> fold Thm.elim_implies agsj'
  14.343 -                |> fold Thm.elim_implies Ghsj'
  14.344 -
  14.345 -        val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
  14.346 -        val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
  14.347 -    in
  14.348 -        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
  14.349 -        |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
  14.350 -        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
  14.351 -        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
  14.352 -        |> fold_rev (implies_intr o cprop_of) Ghsj'
  14.353 -        |> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
  14.354 -        |> implies_intr (cprop_of y_eq_rhsj'h)
  14.355 -        |> implies_intr (cprop_of lhsi_eq_lhsj')
  14.356 -        |> fold_rev forall_intr (cterm_of thy h :: cqsj')
  14.357 -    end
  14.358 -
  14.359 -
  14.360 -
  14.361 -fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
  14.362 -    let
  14.363 -        val Globals {x, y, ranT, fvar, ...} = globals
  14.364 -        val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
  14.365 -        val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
  14.366 -
  14.367 -        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
  14.368 -
  14.369 -        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
  14.370 -                                                            |> fold_rev (implies_intr o cprop_of) CCas
  14.371 -                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  14.372 -
  14.373 -        val existence = fold (curry op COMP o prep_RC) RCs lGI
  14.374 -
  14.375 -        val P = cterm_of thy (mk_eq (y, rhsC))
  14.376 -        val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
  14.377 -
  14.378 -        val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
  14.379 -
  14.380 -        val uniqueness = G_cases
  14.381 -                           |> forall_elim (cterm_of thy lhs)
  14.382 -                           |> forall_elim (cterm_of thy y)
  14.383 -                           |> forall_elim P
  14.384 -                           |> Thm.elim_implies G_lhs_y
  14.385 -                           |> fold Thm.elim_implies unique_clauses
  14.386 -                           |> implies_intr (cprop_of G_lhs_y)
  14.387 -                           |> forall_intr (cterm_of thy y)
  14.388 -
  14.389 -        val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
  14.390 -
  14.391 -        val exactly_one =
  14.392 -            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
  14.393 -                 |> curry (op COMP) existence
  14.394 -                 |> curry (op COMP) uniqueness
  14.395 -                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
  14.396 -                 |> implies_intr (cprop_of case_hyp)
  14.397 -                 |> fold_rev (implies_intr o cprop_of) ags
  14.398 -                 |> fold_rev forall_intr cqs
  14.399 -
  14.400 -        val function_value =
  14.401 -            existence
  14.402 -              |> implies_intr ihyp
  14.403 -              |> implies_intr (cprop_of case_hyp)
  14.404 -              |> forall_intr (cterm_of thy x)
  14.405 -              |> forall_elim (cterm_of thy lhs)
  14.406 -              |> curry (op RS) refl
  14.407 -    in
  14.408 -        (exactly_one, function_value)
  14.409 -    end
  14.410 -
  14.411 -
  14.412 -
  14.413 -
  14.414 -fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
  14.415 -    let
  14.416 -        val Globals {h, domT, ranT, x, ...} = globals
  14.417 -        val thy = ProofContext.theory_of ctxt
  14.418 -
  14.419 -        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
  14.420 -        val ihyp = Term.all domT $ Abs ("z", domT,
  14.421 -                                   Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
  14.422 -                                     HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
  14.423 -                                                             Abs ("y", ranT, G $ Bound 1 $ Bound 0))))
  14.424 -                       |> cterm_of thy
  14.425 -
  14.426 -        val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
  14.427 -        val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
  14.428 -        val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
  14.429 -                        |> instantiate' [] [NONE, SOME (cterm_of thy h)]
  14.430 -
  14.431 -        val _ = trace_msg (K "Proving Replacement lemmas...")
  14.432 -        val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
  14.433 -
  14.434 -        val _ = trace_msg (K "Proving cases for unique existence...")
  14.435 -        val (ex1s, values) =
  14.436 -            split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
  14.437 -
  14.438 -        val _ = trace_msg (K "Proving: Graph is a function")
  14.439 -        val graph_is_function = complete
  14.440 -                                  |> Thm.forall_elim_vars 0
  14.441 -                                  |> fold (curry op COMP) ex1s
  14.442 -                                  |> implies_intr (ihyp)
  14.443 -                                  |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
  14.444 -                                  |> forall_intr (cterm_of thy x)
  14.445 -                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
  14.446 -                                  |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
  14.447 -
  14.448 -        val goalstate =  Conjunction.intr graph_is_function complete
  14.449 -                          |> Thm.close_derivation
  14.450 -                          |> Goal.protect
  14.451 -                          |> fold_rev (implies_intr o cprop_of) compat
  14.452 -                          |> implies_intr (cprop_of complete)
  14.453 -    in
  14.454 -      (goalstate, values)
  14.455 -    end
  14.456 -
  14.457 -
  14.458 -fun define_graph Gname fvar domT ranT clauses RCss lthy =
  14.459 -    let
  14.460 -      val GT = domT --> ranT --> boolT
  14.461 -      val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
  14.462 -
  14.463 -      fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
  14.464 -          let
  14.465 -            fun mk_h_assm (rcfix, rcassm, rcarg) =
  14.466 -                HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
  14.467 -                          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  14.468 -                          |> fold_rev (Logic.all o Free) rcfix
  14.469 -          in
  14.470 -            HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
  14.471 -                      |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
  14.472 -                      |> fold_rev (curry Logic.mk_implies) gs
  14.473 -                      |> fold_rev Logic.all (fvar :: qs)
  14.474 -          end
  14.475 -
  14.476 -      val G_intros = map2 mk_GIntro clauses RCss
  14.477 -
  14.478 -      val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
  14.479 -          FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
  14.480 -    in
  14.481 -      ((G, GIntro_thms, G_elim, G_induct), lthy)
  14.482 -    end
  14.483 -
  14.484 -
  14.485 -
  14.486 -fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
  14.487 -    let
  14.488 -      val f_def =
  14.489 -          Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
  14.490 -                                Abs ("y", ranT, G $ Bound 1 $ Bound 0))
  14.491 -              |> Syntax.check_term lthy
  14.492 -
  14.493 -      val ((f, (_, f_defthm)), lthy) =
  14.494 -        LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
  14.495 -    in
  14.496 -      ((f, f_defthm), lthy)
  14.497 -    end
  14.498 -
  14.499 -
  14.500 -fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
  14.501 -    let
  14.502 -
  14.503 -      val RT = domT --> domT --> boolT
  14.504 -      val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
  14.505 -
  14.506 -      fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
  14.507 -          HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
  14.508 -                    |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
  14.509 -                    |> fold_rev (curry Logic.mk_implies) gs
  14.510 -                    |> fold_rev (Logic.all o Free) rcfix
  14.511 -                    |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  14.512 -                    (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
  14.513 -
  14.514 -      val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
  14.515 -
  14.516 -      val (RIntro_thmss, (R, R_elim, _, lthy)) =
  14.517 -          fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
  14.518 -    in
  14.519 -      ((R, RIntro_thmss, R_elim), lthy)
  14.520 -    end
  14.521 -
  14.522 -
  14.523 -fun fix_globals domT ranT fvar ctxt =
  14.524 -    let
  14.525 -      val ([h, y, x, z, a, D, P, Pbool],ctxt') =
  14.526 -          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
  14.527 -    in
  14.528 -      (Globals {h = Free (h, domT --> ranT),
  14.529 -                y = Free (y, ranT),
  14.530 -                x = Free (x, domT),
  14.531 -                z = Free (z, domT),
  14.532 -                a = Free (a, domT),
  14.533 -                D = Free (D, domT --> boolT),
  14.534 -                P = Free (P, domT --> boolT),
  14.535 -                Pbool = Free (Pbool, boolT),
  14.536 -                fvar = fvar,
  14.537 -                domT = domT,
  14.538 -                ranT = ranT
  14.539 -               },
  14.540 -       ctxt')
  14.541 -    end
  14.542 -
  14.543 -
  14.544 -
  14.545 -fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
  14.546 -    let
  14.547 -      fun inst_term t = subst_bound(f, abstract_over (fvar, t))
  14.548 -    in
  14.549 -      (rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
  14.550 -    end
  14.551 -
  14.552 -
  14.553 -
  14.554 -(**********************************************************
  14.555 - *                   PROVING THE RULES
  14.556 - **********************************************************)
  14.557 -
  14.558 -fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
  14.559 -    let
  14.560 -      val Globals {domT, z, ...} = globals
  14.561 -
  14.562 -      fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
  14.563 -          let
  14.564 -            val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
  14.565 -            val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *)
  14.566 -          in
  14.567 -            ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
  14.568 -              |> (fn it => it COMP graph_is_function)
  14.569 -              |> implies_intr z_smaller
  14.570 -              |> forall_intr (cterm_of thy z)
  14.571 -              |> (fn it => it COMP valthm)
  14.572 -              |> implies_intr lhs_acc
  14.573 -              |> asm_simplify (HOL_basic_ss addsimps [f_iff])
  14.574 -              |> fold_rev (implies_intr o cprop_of) ags
  14.575 -              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  14.576 -          end
  14.577 -    in
  14.578 -      map2 mk_psimp clauses valthms
  14.579 -    end
  14.580 -
  14.581 -
  14.582 -(** Induction rule **)
  14.583 -
  14.584 -
  14.585 -val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
  14.586 -
  14.587 -
  14.588 -fun mk_partial_induct_rule thy globals R complete_thm clauses =
  14.589 -    let
  14.590 -      val Globals {domT, x, z, a, P, D, ...} = globals
  14.591 -      val acc_R = mk_acc domT R
  14.592 -
  14.593 -      val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x)))
  14.594 -      val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a))
  14.595 -
  14.596 -      val D_subset = cterm_of thy (Logic.all x
  14.597 -        (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x))))
  14.598 -
  14.599 -      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
  14.600 -                    Logic.all x
  14.601 -                    (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x),
  14.602 -                                                    Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x),
  14.603 -                                                                      HOLogic.mk_Trueprop (D $ z)))))
  14.604 -                    |> cterm_of thy
  14.605 -
  14.606 -
  14.607 -  (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
  14.608 -      val ihyp = Term.all domT $ Abs ("z", domT,
  14.609 -               Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
  14.610 -                 HOLogic.mk_Trueprop (P $ Bound 0)))
  14.611 -           |> cterm_of thy
  14.612 -
  14.613 -      val aihyp = assume ihyp
  14.614 -
  14.615 -  fun prove_case clause =
  14.616 -      let
  14.617 -    val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
  14.618 -                    qglr = (oqs, _, _, _), ...} = clause
  14.619 -
  14.620 -    val case_hyp_conv = K (case_hyp RS eq_reflection)
  14.621 -    local open Conv in
  14.622 -    val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
  14.623 -    val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
  14.624 -    end
  14.625 -
  14.626 -    fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
  14.627 -        sih |> forall_elim (cterm_of thy rcarg)
  14.628 -            |> Thm.elim_implies llRI
  14.629 -            |> fold_rev (implies_intr o cprop_of) CCas
  14.630 -            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
  14.631 -
  14.632 -    val P_recs = map mk_Prec RCs   (*  [P rec1, P rec2, ... ]  *)
  14.633 -
  14.634 -    val step = HOLogic.mk_Trueprop (P $ lhs)
  14.635 -            |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
  14.636 -            |> fold_rev (curry Logic.mk_implies) gs
  14.637 -            |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs))
  14.638 -            |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  14.639 -            |> cterm_of thy
  14.640 -
  14.641 -    val P_lhs = assume step
  14.642 -           |> fold forall_elim cqs
  14.643 -           |> Thm.elim_implies lhs_D
  14.644 -           |> fold Thm.elim_implies ags
  14.645 -           |> fold Thm.elim_implies P_recs
  14.646 -
  14.647 -    val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
  14.648 -           |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
  14.649 -           |> symmetric (* P lhs == P x *)
  14.650 -           |> (fn eql => equal_elim eql P_lhs) (* "P x" *)
  14.651 -           |> implies_intr (cprop_of case_hyp)
  14.652 -           |> fold_rev (implies_intr o cprop_of) ags
  14.653 -           |> fold_rev forall_intr cqs
  14.654 -      in
  14.655 -        (res, step)
  14.656 -      end
  14.657 -
  14.658 -  val (cases, steps) = split_list (map prove_case clauses)
  14.659 -
  14.660 -  val istep = complete_thm
  14.661 -                |> Thm.forall_elim_vars 0
  14.662 -                |> fold (curry op COMP) cases (*  P x  *)
  14.663 -                |> implies_intr ihyp
  14.664 -                |> implies_intr (cprop_of x_D)
  14.665 -                |> forall_intr (cterm_of thy x)
  14.666 -
  14.667 -  val subset_induct_rule =
  14.668 -      acc_subset_induct
  14.669 -        |> (curry op COMP) (assume D_subset)
  14.670 -        |> (curry op COMP) (assume D_dcl)
  14.671 -        |> (curry op COMP) (assume a_D)
  14.672 -        |> (curry op COMP) istep
  14.673 -        |> fold_rev implies_intr steps
  14.674 -        |> implies_intr a_D
  14.675 -        |> implies_intr D_dcl
  14.676 -        |> implies_intr D_subset
  14.677 -
  14.678 -  val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
  14.679 -
  14.680 -  val simple_induct_rule =
  14.681 -      subset_induct_rule
  14.682 -        |> forall_intr (cterm_of thy D)
  14.683 -        |> forall_elim (cterm_of thy acc_R)
  14.684 -        |> assume_tac 1 |> Seq.hd
  14.685 -        |> (curry op COMP) (acc_downward
  14.686 -                              |> (instantiate' [SOME (ctyp_of thy domT)]
  14.687 -                                               (map (SOME o cterm_of thy) [R, x, z]))
  14.688 -                              |> forall_intr (cterm_of thy z)
  14.689 -                              |> forall_intr (cterm_of thy x))
  14.690 -        |> forall_intr (cterm_of thy a)
  14.691 -        |> forall_intr (cterm_of thy P)
  14.692 -    in
  14.693 -      simple_induct_rule
  14.694 -    end
  14.695 -
  14.696 -
  14.697 -
  14.698 -(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
  14.699 -fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
  14.700 -    let
  14.701 -      val thy = ProofContext.theory_of ctxt
  14.702 -      val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
  14.703 -                      qglr = (oqs, _, _, _), ...} = clause
  14.704 -      val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
  14.705 -                          |> fold_rev (curry Logic.mk_implies) gs
  14.706 -                          |> cterm_of thy
  14.707 -    in
  14.708 -      Goal.init goal
  14.709 -      |> (SINGLE (resolve_tac [accI] 1)) |> the
  14.710 -      |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
  14.711 -      |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
  14.712 -      |> Goal.conclude
  14.713 -      |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  14.714 -    end
  14.715 -
  14.716 -
  14.717 -
  14.718 -(** Termination rule **)
  14.719 -
  14.720 -val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule};
  14.721 -val wf_in_rel = @{thm FunDef.wf_in_rel};
  14.722 -val in_rel_def = @{thm FunDef.in_rel_def};
  14.723 -
  14.724 -fun mk_nest_term_case thy globals R' ihyp clause =
  14.725 -    let
  14.726 -      val Globals {x, z, ...} = globals
  14.727 -      val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
  14.728 -                      qglr=(oqs, _, _, _), ...} = clause
  14.729 -
  14.730 -      val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
  14.731 -
  14.732 -      fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
  14.733 -          let
  14.734 -            val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub)
  14.735 -
  14.736 -            val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
  14.737 -                      |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
  14.738 -                      |> FundefCtxTree.export_term (fixes, assumes)
  14.739 -                      |> fold_rev (curry Logic.mk_implies o prop_of) ags
  14.740 -                      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
  14.741 -                      |> cterm_of thy
  14.742 -
  14.743 -            val thm = assume hyp
  14.744 -                      |> fold forall_elim cqs
  14.745 -                      |> fold Thm.elim_implies ags
  14.746 -                      |> FundefCtxTree.import_thm thy (fixes, assumes)
  14.747 -                      |> fold Thm.elim_implies used (*  "(arg, lhs) : R'"  *)
  14.748 -
  14.749 -            val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
  14.750 -
  14.751 -            val acc = thm COMP ih_case
  14.752 -            val z_acc_local = acc
  14.753 -            |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
  14.754 -
  14.755 -            val ethm = z_acc_local
  14.756 -                         |> FundefCtxTree.export_thm thy (fixes,
  14.757 -                                                          z_eq_arg :: case_hyp :: ags @ assumes)
  14.758 -                         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  14.759 -
  14.760 -            val sub' = sub @ [(([],[]), acc)]
  14.761 -          in
  14.762 -            (sub', (hyp :: hyps, ethm :: thms))
  14.763 -          end
  14.764 -        | step _ _ _ _ = raise Match
  14.765 -    in
  14.766 -      FundefCtxTree.traverse_tree step tree
  14.767 -    end
  14.768 -
  14.769 -
  14.770 -fun mk_nest_term_rule thy globals R R_cases clauses =
  14.771 -    let
  14.772 -      val Globals { domT, x, z, ... } = globals
  14.773 -      val acc_R = mk_acc domT R
  14.774 -
  14.775 -      val R' = Free ("R", fastype_of R)
  14.776 -
  14.777 -      val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
  14.778 -      val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
  14.779 -
  14.780 -      val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
  14.781 -
  14.782 -      (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
  14.783 -      val ihyp = Term.all domT $ Abs ("z", domT,
  14.784 -                                 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
  14.785 -                                   HOLogic.mk_Trueprop (acc_R $ Bound 0)))
  14.786 -                     |> cterm_of thy
  14.787 -
  14.788 -      val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
  14.789 -
  14.790 -      val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
  14.791 -
  14.792 -      val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
  14.793 -    in
  14.794 -      R_cases
  14.795 -        |> forall_elim (cterm_of thy z)
  14.796 -        |> forall_elim (cterm_of thy x)
  14.797 -        |> forall_elim (cterm_of thy (acc_R $ z))
  14.798 -        |> curry op COMP (assume R_z_x)
  14.799 -        |> fold_rev (curry op COMP) cases
  14.800 -        |> implies_intr R_z_x
  14.801 -        |> forall_intr (cterm_of thy z)
  14.802 -        |> (fn it => it COMP accI)
  14.803 -        |> implies_intr ihyp
  14.804 -        |> forall_intr (cterm_of thy x)
  14.805 -        |> (fn it => Drule.compose_single(it,2,wf_induct_rule))
  14.806 -        |> curry op RS (assume wfR')
  14.807 -        |> forall_intr_vars
  14.808 -        |> (fn it => it COMP allI)
  14.809 -        |> fold implies_intr hyps
  14.810 -        |> implies_intr wfR'
  14.811 -        |> forall_intr (cterm_of thy R')
  14.812 -        |> forall_elim (cterm_of thy (inrel_R))
  14.813 -        |> curry op RS wf_in_rel
  14.814 -        |> full_simplify (HOL_basic_ss addsimps [in_rel_def])
  14.815 -        |> forall_intr (cterm_of thy Rrel)
  14.816 -    end
  14.817 -
  14.818 -
  14.819 -
  14.820 -(* Tail recursion (probably very fragile)
  14.821 - *
  14.822 - * FIXME:
  14.823 - * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
  14.824 - * - Must we really replace the fvar by f here?
  14.825 - * - Splitting is not configured automatically: Problems with case?
  14.826 - *)
  14.827 -fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
  14.828 -    let
  14.829 -      val Globals {domT, ranT, fvar, ...} = globals
  14.830 -
  14.831 -      val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
  14.832 -
  14.833 -      val graph_implies_dom = (* "G ?x ?y ==> dom ?x"  *)
  14.834 -          Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
  14.835 -                     (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
  14.836 -                     (fn {prems=[a], ...} =>
  14.837 -                         ((rtac (G_induct OF [a]))
  14.838 -                            THEN_ALL_NEW (rtac accI)
  14.839 -                            THEN_ALL_NEW (etac R_cases)
  14.840 -                            THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
  14.841 -
  14.842 -      val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
  14.843 -
  14.844 -      fun mk_trsimp clause psimp =
  14.845 -          let
  14.846 -            val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
  14.847 -            val thy = ProofContext.theory_of ctxt
  14.848 -            val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
  14.849 -
  14.850 -            val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
  14.851 -            val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
  14.852 -            fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def])
  14.853 -          in
  14.854 -            Goal.prove ctxt [] [] trsimp
  14.855 -                       (fn _ =>
  14.856 -                           rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
  14.857 -                                THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
  14.858 -                                THEN (simp_default_tac (simpset_of ctxt) 1)
  14.859 -                                THEN (etac not_acc_down 1)
  14.860 -                                THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
  14.861 -              |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
  14.862 -          end
  14.863 -    in
  14.864 -      map2 mk_trsimp clauses psimps
  14.865 -    end
  14.866 -
  14.867 -
  14.868 -fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy =
  14.869 -    let
  14.870 -      val FundefConfig {domintros, tailrec, default=default_str, ...} = config
  14.871 -
  14.872 -      val fvar = Free (fname, fT)
  14.873 -      val domT = domain_type fT
  14.874 -      val ranT = range_type fT
  14.875 -
  14.876 -      val default = Syntax.parse_term lthy default_str
  14.877 -        |> TypeInfer.constrain fT |> Syntax.check_term lthy
  14.878 -
  14.879 -      val (globals, ctxt') = fix_globals domT ranT fvar lthy
  14.880 -
  14.881 -      val Globals { x, h, ... } = globals
  14.882 -
  14.883 -      val clauses = map (mk_clause_context x ctxt') abstract_qglrs
  14.884 -
  14.885 -      val n = length abstract_qglrs
  14.886 -
  14.887 -      fun build_tree (ClauseContext { ctxt, rhs, ...}) =
  14.888 -            FundefCtxTree.mk_tree (fname, fT) h ctxt rhs
  14.889 -
  14.890 -      val trees = map build_tree clauses
  14.891 -      val RCss = map find_calls trees
  14.892 -
  14.893 -      val ((G, GIntro_thms, G_elim, G_induct), lthy) =
  14.894 -          PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
  14.895 -
  14.896 -      val ((f, f_defthm), lthy) =
  14.897 -          PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
  14.898 -
  14.899 -      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
  14.900 -      val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
  14.901 -
  14.902 -      val ((R, RIntro_thmss, R_elim), lthy) =
  14.903 -          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
  14.904 -
  14.905 -      val (_, lthy) =
  14.906 -          LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
  14.907 -
  14.908 -      val newthy = ProofContext.theory_of lthy
  14.909 -      val clauses = map (transfer_clause_ctx newthy) clauses
  14.910 -
  14.911 -      val cert = cterm_of (ProofContext.theory_of lthy)
  14.912 -
  14.913 -      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
  14.914 -
  14.915 -      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
  14.916 -      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
  14.917 -
  14.918 -      val compat_store = store_compat_thms n compat
  14.919 -
  14.920 -      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm
  14.921 -
  14.922 -      val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
  14.923 -
  14.924 -      fun mk_partial_rules provedgoal =
  14.925 -          let
  14.926 -            val newthy = theory_of_thm provedgoal (*FIXME*)
  14.927 -
  14.928 -            val (graph_is_function, complete_thm) =
  14.929 -                provedgoal
  14.930 -                  |> Conjunction.elim
  14.931 -                  |> apfst (Thm.forall_elim_vars 0)
  14.932 -
  14.933 -            val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
  14.934 -
  14.935 -            val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
  14.936 -
  14.937 -            val simple_pinduct = PROFILE "Proving partial induction rule"
  14.938 -                                                           (mk_partial_induct_rule newthy globals R complete_thm) xclauses
  14.939 -
  14.940 -
  14.941 -            val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
  14.942 -
  14.943 -            val dom_intros = if domintros
  14.944 -                             then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro lthy globals R R_elim)) xclauses)
  14.945 -                             else NONE
  14.946 -            val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
  14.947 -
  14.948 -          in
  14.949 -            FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
  14.950 -                          psimps=psimps, simple_pinducts=[simple_pinduct],
  14.951 -                          termination=total_intro, trsimps=trsimps,
  14.952 -                          domintros=dom_intros}
  14.953 -          end
  14.954 -    in
  14.955 -      ((f, goalstate, mk_partial_rules), lthy)
  14.956 -    end
  14.957 -
  14.958 -
  14.959 -end
    15.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Fri Oct 23 15:33:19 2009 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,179 +0,0 @@
    15.4 -(*  Title:      HOL/Tools/Function/fundef_lib.ML
    15.5 -    Author:     Alexander Krauss, TU Muenchen
    15.6 -
    15.7 -A package for general recursive function definitions. 
    15.8 -Some fairly general functions that should probably go somewhere else... 
    15.9 -*)
   15.10 -
   15.11 -structure FundefLib = struct
   15.12 -
   15.13 -fun map_option f NONE = NONE 
   15.14 -  | map_option f (SOME x) = SOME (f x);
   15.15 -
   15.16 -fun fold_option f NONE y = y
   15.17 -  | fold_option f (SOME x) y = f x y;
   15.18 -
   15.19 -fun fold_map_option f NONE y = (NONE, y)
   15.20 -  | fold_map_option f (SOME x) y = apfst SOME (f x y);
   15.21 -
   15.22 -(* Ex: "The variable" ^ plural " is" "s are" vs *)
   15.23 -fun plural sg pl [x] = sg
   15.24 -  | plural sg pl _ = pl
   15.25 -
   15.26 -(* lambda-abstracts over an arbitrarily nested tuple
   15.27 -  ==> hologic.ML? *)
   15.28 -fun tupled_lambda vars t =
   15.29 -    case vars of
   15.30 -      (Free v) => lambda (Free v) t
   15.31 -    | (Var v) => lambda (Var v) t
   15.32 -    | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>  
   15.33 -      (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
   15.34 -    | _ => raise Match
   15.35 -                 
   15.36 -                 
   15.37 -fun dest_all (Const ("all", _) $ Abs (a as (_,T,_))) =
   15.38 -    let
   15.39 -      val (n, body) = Term.dest_abs a
   15.40 -    in
   15.41 -      (Free (n, T), body)
   15.42 -    end
   15.43 -  | dest_all _ = raise Match
   15.44 -                         
   15.45 -
   15.46 -(* Removes all quantifiers from a term, replacing bound variables by frees. *)
   15.47 -fun dest_all_all (t as (Const ("all",_) $ _)) = 
   15.48 -    let
   15.49 -      val (v,b) = dest_all t
   15.50 -      val (vs, b') = dest_all_all b
   15.51 -    in
   15.52 -      (v :: vs, b')
   15.53 -    end
   15.54 -  | dest_all_all t = ([],t)
   15.55 -                     
   15.56 -
   15.57 -(* FIXME: similar to Variable.focus *)
   15.58 -fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
   15.59 -    let
   15.60 -      val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
   15.61 -      val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
   15.62 -
   15.63 -      val (n'', body) = Term.dest_abs (n', T, b) 
   15.64 -      val _ = (n' = n'') orelse error "dest_all_ctx"
   15.65 -      (* Note: We assume that n' does not occur in the body. Otherwise it would be fixed. *)
   15.66 -
   15.67 -      val (ctx'', vs, bd) = dest_all_all_ctx ctx' body
   15.68 -    in
   15.69 -      (ctx'', (n', T) :: vs, bd)
   15.70 -    end
   15.71 -  | dest_all_all_ctx ctx t = 
   15.72 -    (ctx, [], t)
   15.73 -
   15.74 -
   15.75 -fun map3 _ [] [] [] = []
   15.76 -  | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
   15.77 -  | map3 _ _ _ _ = raise Library.UnequalLengths;
   15.78 -
   15.79 -fun map4 _ [] [] [] [] = []
   15.80 -  | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
   15.81 -  | map4 _ _ _ _ _ = raise Library.UnequalLengths;
   15.82 -
   15.83 -fun map6 _ [] [] [] [] [] [] = []
   15.84 -  | map6 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) = f x y z u v w :: map6 f xs ys zs us vs ws
   15.85 -  | map6 _ _ _ _ _ _ _ = raise Library.UnequalLengths;
   15.86 -
   15.87 -fun map7 _ [] [] [] [] [] [] [] = []
   15.88 -  | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
   15.89 -  | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
   15.90 -
   15.91 -
   15.92 -
   15.93 -(* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
   15.94 -(* ==> library *)
   15.95 -fun unordered_pairs [] = []
   15.96 -  | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
   15.97 -
   15.98 -
   15.99 -(* Replaces Frees by name. Works with loose Bounds. *)
  15.100 -fun replace_frees assoc =
  15.101 -    map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
  15.102 -                 | t => t)
  15.103 -
  15.104 -
  15.105 -fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
  15.106 -  | rename_bound n _ = raise Match
  15.107 -
  15.108 -fun mk_forall_rename (n, v) =
  15.109 -    rename_bound n o Logic.all v 
  15.110 -
  15.111 -fun forall_intr_rename (n, cv) thm =
  15.112 -    let
  15.113 -      val allthm = forall_intr cv thm
  15.114 -      val (_ $ abs) = prop_of allthm
  15.115 -    in
  15.116 -      Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
  15.117 -    end
  15.118 -
  15.119 -
  15.120 -(* Returns the frees in a term in canonical order, excluding the fixes from the context *)
  15.121 -fun frees_in_term ctxt t =
  15.122 -    Term.add_frees t []
  15.123 -    |> filter_out (Variable.is_fixed ctxt o fst)
  15.124 -    |> rev
  15.125 -
  15.126 -
  15.127 -datatype proof_attempt = Solved of thm | Stuck of thm | Fail
  15.128 -
  15.129 -fun try_proof cgoal tac = 
  15.130 -    case SINGLE tac (Goal.init cgoal) of
  15.131 -      NONE => Fail
  15.132 -    | SOME st =>
  15.133 -        if Thm.no_prems st
  15.134 -        then Solved (Goal.finish (Syntax.init_pretty_global (Thm.theory_of_cterm cgoal)) st)
  15.135 -        else Stuck st
  15.136 -
  15.137 -
  15.138 -fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = 
  15.139 -    if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
  15.140 -  | dest_binop_list _ t = [ t ]
  15.141 -
  15.142 -
  15.143 -(* separate two parts in a +-expression:
  15.144 -   "a + b + c + d + e" --> "(a + b + d) + (c + e)"
  15.145 -
  15.146 -   Here, + can be any binary operation that is AC.
  15.147 -
  15.148 -   cn - The name of the binop-constructor (e.g. @{const_name Un})
  15.149 -   ac - the AC rewrite rules for cn
  15.150 -   is - the list of indices of the expressions that should become the first part
  15.151 -        (e.g. [0,1,3] in the above example)
  15.152 -*)
  15.153 -
  15.154 -fun regroup_conv neu cn ac is ct =
  15.155 - let
  15.156 -   val mk = HOLogic.mk_binop cn
  15.157 -   val t = term_of ct
  15.158 -   val xs = dest_binop_list cn t
  15.159 -   val js = subtract (op =) is (0 upto (length xs) - 1)
  15.160 -   val ty = fastype_of t
  15.161 -   val thy = theory_of_cterm ct
  15.162 - in
  15.163 -   Goal.prove_internal []
  15.164 -     (cterm_of thy
  15.165 -       (Logic.mk_equals (t,
  15.166 -          if is = []
  15.167 -          then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
  15.168 -          else if js = []
  15.169 -            then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
  15.170 -            else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
  15.171 -     (K (rewrite_goals_tac ac
  15.172 -         THEN rtac Drule.reflexive_thm 1))
  15.173 - end
  15.174 -
  15.175 -(* instance for unions *)
  15.176 -fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Lattices.sup}
  15.177 -  (map (fn t => t RS eq_reflection) (@{thms Un_ac} @
  15.178 -                                     @{thms Un_empty_right} @
  15.179 -                                     @{thms Un_empty_left})) t
  15.180 -
  15.181 -
  15.182 -end
    16.1 --- a/src/HOL/Tools/Function/induction_scheme.ML	Fri Oct 23 15:33:19 2009 +0200
    16.2 +++ b/src/HOL/Tools/Function/induction_scheme.ML	Fri Oct 23 16:22:10 2009 +0200
    16.3 @@ -13,10 +13,10 @@
    16.4  end
    16.5  
    16.6  
    16.7 -structure InductionScheme : INDUCTION_SCHEME =
    16.8 +structure Induction_Scheme : INDUCTION_SCHEME =
    16.9  struct
   16.10  
   16.11 -open FundefLib
   16.12 +open Function_Lib
   16.13  
   16.14  
   16.15  type rec_call_info = int * (string * typ) list * term list * term list
    17.1 --- a/src/HOL/Tools/Function/inductive_wrap.ML	Fri Oct 23 15:33:19 2009 +0200
    17.2 +++ b/src/HOL/Tools/Function/inductive_wrap.ML	Fri Oct 23 16:22:10 2009 +0200
    17.3 @@ -6,17 +6,17 @@
    17.4  the introduction and elimination rules.
    17.5  *)
    17.6  
    17.7 -signature FUNDEF_INDUCTIVE_WRAP =
    17.8 +signature FUNCTION_INDUCTIVE_WRAP =
    17.9  sig
   17.10    val inductive_def :  term list 
   17.11                         -> ((bstring * typ) * mixfix) * local_theory
   17.12                         -> thm list * (term * thm * thm * local_theory)
   17.13  end
   17.14  
   17.15 -structure FundefInductiveWrap: FUNDEF_INDUCTIVE_WRAP =
   17.16 +structure Function_Inductive_Wrap: FUNCTION_INDUCTIVE_WRAP =
   17.17  struct
   17.18  
   17.19 -open FundefLib
   17.20 +open Function_Lib
   17.21  
   17.22  fun requantify ctxt lfix orig_def thm =
   17.23      let
    18.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Oct 23 15:33:19 2009 +0200
    18.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Oct 23 16:22:10 2009 +0200
    18.3 @@ -13,10 +13,10 @@
    18.4    val setup: theory -> theory
    18.5  end
    18.6  
    18.7 -structure LexicographicOrder : LEXICOGRAPHIC_ORDER =
    18.8 +structure Lexicographic_Order : LEXICOGRAPHIC_ORDER =
    18.9  struct
   18.10  
   18.11 -open FundefLib
   18.12 +open Function_Lib
   18.13  
   18.14  (** General stuff **)
   18.15  
   18.16 @@ -58,7 +58,7 @@
   18.17  
   18.18  fun dest_term (t : term) =
   18.19      let
   18.20 -      val (vars, prop) = FundefLib.dest_all_all t
   18.21 +      val (vars, prop) = Function_Lib.dest_all_all t
   18.22        val (prems, concl) = Logic.strip_horn prop
   18.23        val (lhs, rhs) = concl
   18.24                           |> HOLogic.dest_Trueprop
   18.25 @@ -215,9 +215,9 @@
   18.26      end
   18.27  
   18.28  fun lexicographic_order_tac ctxt =
   18.29 -  TRY (FundefCommon.apply_termination_rule ctxt 1)
   18.30 +  TRY (Function_Common.apply_termination_rule ctxt 1)
   18.31    THEN lex_order_tac ctxt
   18.32 -    (auto_tac (clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
   18.33 +    (auto_tac (clasimpset_of ctxt addsimps2 Function_Common.Termination_Simps.get ctxt))
   18.34  
   18.35  val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
   18.36  
   18.37 @@ -225,7 +225,7 @@
   18.38    Method.setup @{binding lexicographic_order}
   18.39      (Method.sections clasimp_modifiers >> (K lexicographic_order))
   18.40      "termination prover for lexicographic orderings"
   18.41 -  #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
   18.42 +  #> Context.theory_map (Function_Common.set_termination_prover lexicographic_order)
   18.43  
   18.44  end;
   18.45  
    19.1 --- a/src/HOL/Tools/Function/mutual.ML	Fri Oct 23 15:33:19 2009 +0200
    19.2 +++ b/src/HOL/Tools/Function/mutual.ML	Fri Oct 23 16:22:10 2009 +0200
    19.3 @@ -5,29 +5,26 @@
    19.4  Tools for mutual recursive definitions.
    19.5  *)
    19.6  
    19.7 -signature FUNDEF_MUTUAL =
    19.8 +signature FUNCTION_MUTUAL =
    19.9  sig
   19.10  
   19.11 -  val prepare_fundef_mutual : FundefCommon.fundef_config
   19.12 +  val prepare_function_mutual : Function_Common.function_config
   19.13                                -> string (* defname *)
   19.14                                -> ((string * typ) * mixfix) list
   19.15                                -> term list
   19.16                                -> local_theory
   19.17                                -> ((thm (* goalstate *)
   19.18 -                                   * (thm -> FundefCommon.fundef_result) (* proof continuation *)
   19.19 +                                   * (thm -> Function_Common.function_result) (* proof continuation *)
   19.20                                    ) * local_theory)
   19.21  
   19.22  end
   19.23  
   19.24  
   19.25 -structure FundefMutual: FUNDEF_MUTUAL =
   19.26 +structure Function_Mutual: FUNCTION_MUTUAL =
   19.27  struct
   19.28  
   19.29 -open FundefLib
   19.30 -open FundefCommon
   19.31 -
   19.32 -
   19.33 -
   19.34 +open Function_Lib
   19.35 +open Function_Common
   19.36  
   19.37  type qgar = string * (string * typ) list * term list * term list * term
   19.38  
   19.39 @@ -268,7 +265,7 @@
   19.40  fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
   19.41      let
   19.42        val result = inner_cont proof
   19.43 -      val FundefResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
   19.44 +      val FunctionResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
   19.45                          termination,domintros} = result
   19.46                                                                                                                 
   19.47        val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
   19.48 @@ -288,20 +285,20 @@
   19.49        val mtermination = full_simplify rew_ss termination
   19.50        val mdomintros = map_option (map (full_simplify rew_ss)) domintros
   19.51      in
   19.52 -      FundefResult { fs=fs, G=G, R=R,
   19.53 +      FunctionResult { fs=fs, G=G, R=R,
   19.54                       psimps=mpsimps, simple_pinducts=minducts,
   19.55                       cases=cases, termination=mtermination,
   19.56                       domintros=mdomintros,
   19.57                       trsimps=mtrsimps}
   19.58      end
   19.59        
   19.60 -fun prepare_fundef_mutual config defname fixes eqss lthy =
   19.61 +fun prepare_function_mutual config defname fixes eqss lthy =
   19.62      let
   19.63        val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
   19.64        val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
   19.65            
   19.66        val ((fsum, goalstate, cont), lthy') =
   19.67 -          FundefCore.prepare_fundef config defname [((n, T), NoSyn)] qglrs lthy
   19.68 +          Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy
   19.69            
   19.70        val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
   19.71  
    20.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Fri Oct 23 15:33:19 2009 +0200
    20.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Fri Oct 23 16:22:10 2009 +0200
    20.3 @@ -17,8 +17,8 @@
    20.4  structure Pat_Completeness : PAT_COMPLETENESS =
    20.5  struct
    20.6  
    20.7 -open FundefLib
    20.8 -open FundefCommon
    20.9 +open Function_Lib
   20.10 +open Function_Common
   20.11  
   20.12  
   20.13  fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
    21.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Fri Oct 23 15:33:19 2009 +0200
    21.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Fri Oct 23 16:22:10 2009 +0200
    21.3 @@ -8,7 +8,7 @@
    21.4  
    21.5  *)
    21.6  
    21.7 -signature FUNDEF_SPLIT =
    21.8 +signature FUNCTION_SPLIT =
    21.9  sig
   21.10    val split_some_equations :
   21.11        Proof.context -> (bool * term) list -> term list list
   21.12 @@ -17,10 +17,10 @@
   21.13        Proof.context -> term list -> term list list
   21.14  end
   21.15  
   21.16 -structure FundefSplit : FUNDEF_SPLIT =
   21.17 +structure Function_Split : FUNCTION_SPLIT =
   21.18  struct
   21.19  
   21.20 -open FundefLib
   21.21 +open Function_Lib
   21.22  
   21.23  (* We use proof context for the variable management *)
   21.24  (* FIXME: no __ *)
    22.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Oct 23 15:33:19 2009 +0200
    22.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Oct 23 16:22:10 2009 +0200
    22.3 @@ -38,8 +38,8 @@
    22.4  structure ScnpReconstruct : SCNP_RECONSTRUCT =
    22.5  struct
    22.6  
    22.7 -val PROFILE = FundefCommon.PROFILE
    22.8 -fun TRACE x = if ! FundefCommon.profile then tracing x else ()
    22.9 +val PROFILE = Function_Common.PROFILE
   22.10 +fun TRACE x = if ! Function_Common.profile then tracing x else ()
   22.11  
   22.12  open ScnpSolve
   22.13  
   22.14 @@ -64,7 +64,7 @@
   22.15     reduction_pair : thm
   22.16    }
   22.17  
   22.18 -structure MultisetSetup = TheoryDataFun
   22.19 +structure Multiset_Setup = TheoryDataFun
   22.20  (
   22.21    type T = multiset_setup option
   22.22    val empty = NONE
   22.23 @@ -73,10 +73,10 @@
   22.24    fun merge _ (v1, v2) = if is_some v2 then v2 else v1
   22.25  )
   22.26  
   22.27 -val multiset_setup = MultisetSetup.put o SOME
   22.28 +val multiset_setup = Multiset_Setup.put o SOME
   22.29  
   22.30  fun undef x = error "undef"
   22.31 -fun get_multiset_setup thy = MultisetSetup.get thy
   22.32 +fun get_multiset_setup thy = Multiset_Setup.get thy
   22.33    |> the_default (Multiset
   22.34  { msetT = undef, mk_mset=undef,
   22.35    mset_regroup_conv=undef, mset_member_tac = undef,
   22.36 @@ -287,7 +287,7 @@
   22.37          |> cterm_of thy
   22.38      in
   22.39        PROFILE "Proof Reconstruction"
   22.40 -        (CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv sl))) 1
   22.41 +        (CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1
   22.42           THEN (rtac @{thm reduction_pair_lemma} 1)
   22.43           THEN (rtac @{thm rp_inv_image_rp} 1)
   22.44           THEN (rtac (order_rpair ms_rp label) 1)
   22.45 @@ -350,7 +350,7 @@
   22.46  
   22.47  fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
   22.48    let
   22.49 -    val ms_configured = is_some (MultisetSetup.get (ProofContext.theory_of ctxt))
   22.50 +    val ms_configured = is_some (Multiset_Setup.get (ProofContext.theory_of ctxt))
   22.51      val orders' = if ms_configured then orders
   22.52                    else filter_out (curry op = MS) orders
   22.53      val gp = gen_probl D cs
   22.54 @@ -395,7 +395,7 @@
   22.55    end
   22.56  
   22.57  fun gen_sizechange_tac orders autom_tac ctxt err_cont =
   22.58 -  TRY (FundefCommon.apply_termination_rule ctxt 1)
   22.59 +  TRY (Function_Common.apply_termination_rule ctxt 1)
   22.60    THEN TRY (Termination.wf_union_tac ctxt)
   22.61    THEN
   22.62     (rtac @{thm wf_empty} 1
   22.63 @@ -406,7 +406,7 @@
   22.64  
   22.65  fun decomp_scnp orders ctxt =
   22.66    let
   22.67 -    val extra_simps = FundefCommon.Termination_Simps.get ctxt
   22.68 +    val extra_simps = Function_Common.Termination_Simps.get ctxt
   22.69      val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
   22.70    in
   22.71      SIMPLE_METHOD
    23.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Fri Oct 23 15:33:19 2009 +0200
    23.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Fri Oct 23 16:22:10 2009 +0200
    23.3 @@ -73,7 +73,7 @@
    23.4  (* SAT solving *)
    23.5  val solver = Unsynchronized.ref "auto";
    23.6  fun sat_solver x =
    23.7 -  FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
    23.8 +  Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
    23.9  
   23.10  (* "Virtual constructors" for various propositional variables *)
   23.11  fun var_constrs (gp as GP (arities, gl)) =
    24.1 --- a/src/HOL/Tools/Function/termination.ML	Fri Oct 23 15:33:19 2009 +0200
    24.2 +++ b/src/HOL/Tools/Function/termination.ML	Fri Oct 23 16:22:10 2009 +0200
    24.3 @@ -48,7 +48,7 @@
    24.4  structure Termination : TERMINATION =
    24.5  struct
    24.6  
    24.7 -open FundefLib
    24.8 +open Function_Lib
    24.9  
   24.10  val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
   24.11  structure Term2tab = Table(type key = term * term val ord = term2_ord);
   24.12 @@ -145,7 +145,7 @@
   24.13  
   24.14  fun mk_sum_skel rel =
   24.15    let
   24.16 -    val cs = FundefLib.dest_binop_list @{const_name Lattices.sup} rel
   24.17 +    val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
   24.18      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   24.19        let
   24.20          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
   24.21 @@ -233,7 +233,7 @@
   24.22  fun CALLS tac i st =
   24.23    if Thm.no_prems st then all_tac st
   24.24    else case Thm.term_of (Thm.cprem_of st i) of
   24.25 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   24.26 +    (_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   24.27    |_ => no_tac st
   24.28  
   24.29  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
   24.30 @@ -251,7 +251,7 @@
   24.31  local
   24.32  fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
   24.33      let
   24.34 -      val (vars, prop) = FundefLib.dest_all_all t
   24.35 +      val (vars, prop) = Function_Lib.dest_all_all t
   24.36        val (prems, concl) = Logic.strip_horn prop
   24.37        val (lhs, rhs) = concl
   24.38                           |> HOLogic.dest_Trueprop