src/HOL/Tools/function_package/mutual.ML
author krauss
Tue, 07 Aug 2007 17:01:35 +0200
changeset 24171 25381ce95316
parent 24170 33f055a0f3a1
child 24977 9f98751c9628
permissions -rw-r--r--
Issue a warning, when "function" encounters variables occuring in function position, as in "f (g x) = ..." where g is a variable.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     1
(*  Title:      HOL/Tools/function_package/mutual.ML
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     2
    ID:         $Id$
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     3
    Author:     Alexander Krauss, TU Muenchen
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     4
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
     5
A package for general recursive function definitions.
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     6
Tools for mutual recursive definitions.
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     7
*)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     8
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
     9
signature FUNDEF_MUTUAL =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    10
sig
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
    11
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    12
  val prepare_fundef_mutual : FundefCommon.fundef_config
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    13
                              -> string (* defname *)
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    14
                              -> ((string * typ) * mixfix) list
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
    15
                              -> term list
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
    16
                              -> local_theory
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    17
                              -> ((thm (* goalstate *)
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    18
                                   * (thm -> FundefCommon.fundef_result) (* proof continuation *)
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    19
                                  ) * local_theory)
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    20
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    21
end
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    22
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    23
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
    24
structure FundefMutual: FUNDEF_MUTUAL =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    25
struct
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    26
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20949
diff changeset
    27
open FundefLib
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    28
open FundefCommon
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    29
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    30
(* Theory dependencies *)
22622
25693088396b Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents: 22620
diff changeset
    31
val sum_case_rules = thms "Sum_Type.sum_cases"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    32
val split_apply = thm "Product_Type.split"
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    33
val projl_inl = thm "Sum_Type.Projl_Inl"
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    34
val projr_inr = thm "Sum_Type.Projr_Inr"
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    35
23528
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    36
(* top-down access in balanced tree *)
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    37
fun access_top_down {left, right, init} len i =
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    38
    BalancedTree.access {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    39
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    40
(* Sum types *)
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    41
fun mk_sumT LT RT = Type ("+", [LT, RT])
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    42
fun mk_sumcase TL TR T l r = Const (@{const_name "Sum_Type.sum_case"}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    43
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    44
val App = curry op $
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    45
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    46
fun mk_inj ST n i = 
23528
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    47
    access_top_down 
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    48
    { init = (ST, I : term -> term),
23528
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    49
      left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, inj o App (Const (@{const_name "Inl"}, LT --> T)))),
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    50
      right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, inj o App (Const (@{const_name "Inr"}, RT --> T))))} n i 
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    51
    |> snd
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    52
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    53
fun mk_proj ST n i = 
23528
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    54
    access_top_down 
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    55
    { init = (ST, I : term -> term),
23528
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    56
      left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, App (Const (@{const_name "Projl"}, T --> LT)) o proj)),
55597852285a fixed an issue with mutual recursion
krauss
parents: 23494
diff changeset
    57
      right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, App (Const (@{const_name "Projr"}, T --> RT)) o proj))} n i
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    58
    |> snd
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    59
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    60
fun mk_sumcases T fs =
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    61
      BalancedTree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    62
                        (map (fn f => (f, domain_type (fastype_of f))) fs)
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    63
      |> fst
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    64
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    65
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    66
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    67
type qgar = string * (string * typ) list * term list * term list * term
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    68
23217
8eac3bda1063 name_of_fqgar: precise type;
wenzelm
parents: 23203
diff changeset
    69
fun name_of_fqgar ((f, _, _, _, _): qgar) = f
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    70
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    71
datatype mutual_part =
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    72
  MutualPart of 
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    73
   {
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    74
    i : int,
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    75
    i' : int,
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    76
    fvar : string * typ,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    77
    cargTs: typ list,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    78
    f_def: term,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    79
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    80
    f: term option,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    81
    f_defthm : thm option
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    82
   }
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    83
   
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    84
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    85
datatype mutual_info =
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    86
  Mutual of 
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    87
   { 
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    88
    n : int,
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    89
    n' : int,
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    90
    fsum_var : string * typ,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    91
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    92
    ST: typ,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    93
    RST: typ,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    94
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    95
    parts: mutual_part list,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    96
    fqgars: qgar list,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    97
    qglrs: ((string * typ) list * term list * term * term) list,
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    98
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    99
    fsum : term option
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   100
   }
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   101
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   102
fun mutual_induct_Pnames n =
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   103
    if n < 5 then fst (chop n ["P","Q","R","S"])
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   104
    else map (fn i => "P" ^ string_of_int i) (1 upto n)
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   105
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   106
fun get_part fname =
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   107
    the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   108
                     
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   109
(* FIXME *)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   110
fun mk_prod_abs e (t1, t2) =
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   111
    let
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   112
      val bTs = rev (map snd e)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   113
      val T1 = fastype_of1 (bTs, t1)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   114
      val T2 = fastype_of1 (bTs, t2)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   115
    in
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   116
      HOLogic.pair_const T1 T2 $ t1 $ t2
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   117
    end;
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   118
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   119
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   120
fun analyze_eqs ctxt defname fs eqs =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   121
    let
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   122
      val num = length fs
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   123
        val fnames = map fst fs
24170
33f055a0f3a1 more error handling
krauss
parents: 23819
diff changeset
   124
        val fqgars = map (split_def ctxt) eqs
23189
4574ab8f3b21 simplified interfaces, some restructuring
krauss
parents: 22733
diff changeset
   125
        val arities = mk_arities fqgars
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   126
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   127
        fun curried_types (fname, fT) =
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   128
            let
20654
d80502f0d701 1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents: 20534
diff changeset
   129
              val k = the_default 1 (Symtab.lookup arities fname)
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   130
              val (caTs, uaTs) = chop k (binder_types fT)
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   131
            in
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   132
                (caTs, uaTs ---> body_type fT)
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   133
            end
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   134
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   135
        val (caTss, resultTs) = split_list (map curried_types fs)
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   136
        val argTs = map (foldr1 HOLogic.mk_prodT) caTss
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   137
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   138
        val dresultTs = distinct (Type.eq_type Vartab.empty) resultTs
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   139
        val n' = length dresultTs
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   140
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   141
        val RST = BalancedTree.make (uncurry mk_sumT) dresultTs
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   142
        val ST = BalancedTree.make (uncurry mk_sumT) argTs
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   143
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   144
        val fsum_type = ST --> RST
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   145
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   146
        val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   147
        val fsum_var = (fsum_var_name, fsum_type)
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   148
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   149
        fun define (fvar as (n, T)) caTs resultT i =
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   150
            let
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   151
                val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   152
                val i' = find_index (fn Ta => Type.eq_type Vartab.empty (Ta, resultT)) dresultTs + 1 
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   153
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   154
                val f_exp = mk_proj RST n' i' (Free fsum_var $ mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   155
                val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   156
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   157
                val rew = (n, fold_rev lambda vars f_exp)
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   158
            in
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   159
                (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   160
            end
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   161
            
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   162
        val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   163
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   164
        fun convert_eqs (f, qs, gs, args, rhs) =
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   165
            let
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   166
              val MutualPart {i, i', ...} = get_part f parts
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   167
            in
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   168
              (qs, gs, mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   169
               mk_inj RST n' i' (replace_frees rews rhs)
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   170
                               |> Envir.beta_norm)
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   171
            end
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   172
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   173
        val qglrs = map convert_eqs fqgars
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   174
    in
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   175
        Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, 
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   176
                parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   177
    end
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   178
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   179
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   180
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   181
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   182
fun define_projections fixes mutual fsum lthy =
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   183
    let
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   184
      fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   185
          let
21436
5313a4cc3823 LocalTheory.notes/defs: proper kind;
wenzelm
parents: 21319
diff changeset
   186
            val ((f, (_, f_defthm)), lthy') =
5313a4cc3823 LocalTheory.notes/defs: proper kind;
wenzelm
parents: 21319
diff changeset
   187
              LocalTheory.def Thm.internalK ((fname, mixfix),
5313a4cc3823 LocalTheory.notes/defs: proper kind;
wenzelm
parents: 21319
diff changeset
   188
                                            ((fname ^ "_def", []), Term.subst_bound (fsum, f_def)))
5313a4cc3823 LocalTheory.notes/defs: proper kind;
wenzelm
parents: 21319
diff changeset
   189
                              lthy
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   190
          in
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   191
            (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   192
                         f=SOME f, f_defthm=SOME f_defthm },
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   193
             lthy')
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   194
          end
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   195
          
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   196
      val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   197
      val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   198
    in
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   199
      (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts',
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   200
                fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   201
       lthy')
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   202
    end
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   203
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   204
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   205
fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   206
                      
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   207
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   208
    let
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   209
      val thy = ProofContext.theory_of ctxt
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   210
                
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   211
      val oqnames = map fst pre_qs
20797
c1f0bc7e7d80 renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents: 20654
diff changeset
   212
      val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   213
                        |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   214
                        
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   215
      fun inst t = subst_bounds (rev qs, t)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   216
      val gs = map inst pre_gs
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   217
      val args = map inst pre_args
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   218
      val rhs = inst pre_rhs
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   219
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   220
      val cqs = map (cterm_of thy) qs
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   221
      val ags = map (assume o cterm_of thy) gs
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   222
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   223
      val import = fold forall_elim cqs
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   224
                   #> fold (flip implies_elim) ags
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   225
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   226
      val export = fold_rev (implies_intr o cprop_of) ags
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   227
                   #> fold_rev forall_intr_rename (oqnames ~~ cqs)
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   228
    in
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   229
      F ctxt (f, qs, gs, args, rhs) import export
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   230
    end
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   231
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   232
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq =
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   233
    let
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   234
      val (MutualPart {f=SOME f, f_defthm=SOME f_def, ...}) = get_part fname parts
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   235
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   236
      val psimp = import sum_psimp_eq
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   237
      val (simp, restore_cond) = case cprems_of psimp of
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   238
                                   [] => (psimp, I)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   239
                                 | [cond] => (implies_elim psimp (assume cond), implies_intr cond)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   240
                                 | _ => sys_error "Too many conditions"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   241
    in
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   242
      Goal.prove ctxt [] [] 
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   243
                 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
24171
25381ce95316 Issue a warning, when "function" encounters variables occuring in function position,
krauss
parents: 24170
diff changeset
   244
                 (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   245
                          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   246
                          THEN SIMPSET' (fn ss => simp_tac (ss addsimps [projl_inl, projr_inr])) 1)
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   247
        |> restore_cond 
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   248
        |> export
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   249
    end
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   250
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   251
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   252
(* FIXME HACK *)
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   253
fun mk_applied_form ctxt caTs thm =
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   254
    let
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   255
      val thy = ProofContext.theory_of ctxt
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   256
      val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   257
    in
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   258
      fold (fn x => fn thm => combination thm (reflexive x)) xs thm
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   259
           |> beta_reduce
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   260
           |> fold_rev forall_intr xs
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   261
           |> forall_elim_vars 0
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   262
    end
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   263
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   264
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   265
fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, RST, parts, ...}) =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   266
    let
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   267
      val cert = cterm_of (ProofContext.theory_of lthy)
20949
f030835fd9e4 Induction rules have schematic variables again.
krauss
parents: 20878
diff changeset
   268
      val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   269
                                       Free (Pname, cargTs ---> HOLogic.boolT))
20949
f030835fd9e4 Induction rules have schematic variables again.
krauss
parents: 20878
diff changeset
   270
                       (mutual_induct_Pnames (length parts))
f030835fd9e4 Induction rules have schematic variables again.
krauss
parents: 20878
diff changeset
   271
                       parts
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   272
                       
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   273
      fun mk_P (MutualPart {cargTs, ...}) P =
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   274
          let
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   275
            val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   276
            val atup = foldr1 HOLogic.mk_prod avars
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   277
          in
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   278
            tupled_lambda atup (list_comb (P, avars))
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   279
          end
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   280
          
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   281
      val Ps = map2 mk_P parts newPs
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   282
      val case_exp = mk_sumcases HOLogic.boolT Ps
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   283
                     
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   284
      val induct_inst =
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   285
          forall_elim (cert case_exp) induct
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   286
                      |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   287
                      |> full_simplify (HOL_basic_ss addsimps all_f_defs)
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   288
          
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   289
      fun project rule (MutualPart {cargTs, i, ...}) =
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   290
          let
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   291
            val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int j, T)) cargTs
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   292
            val inj = mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   293
          in
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   294
            rule
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   295
              |> forall_elim (cert inj)
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   296
              |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   297
              |> fold_rev (forall_intr o cert) (afs @ newPs)
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   298
          end
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   299
    in
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
   300
      map (project induct_inst) parts
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   301
    end
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   302
    
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   303
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   304
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   305
    let
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   306
      val result = inner_cont proof
22733
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents: 22623
diff changeset
   307
      val FundefResult {fs=[f], G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   308
                        termination,domintros} = result
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   309
                                                                                                               
22733
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents: 22623
diff changeset
   310
      val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents: 22623
diff changeset
   311
                                     (mk_applied_form lthy cargTs (symmetric f_def), f))
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents: 22623
diff changeset
   312
                                 parts
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents: 22623
diff changeset
   313
                             |> split_list
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   314
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   315
      val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   316
                           
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   317
      fun mk_mpsimp fqgar sum_psimp =
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   318
          in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   319
          
23189
4574ab8f3b21 simplified interfaces, some restructuring
krauss
parents: 22733
diff changeset
   320
      val rew_ss = HOL_basic_ss addsimps all_f_defs
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   321
      val mpsimps = map2 mk_mpsimp fqgars psimps
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   322
      val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   323
      val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
23189
4574ab8f3b21 simplified interfaces, some restructuring
krauss
parents: 22733
diff changeset
   324
      val mtermination = full_simplify rew_ss termination
4574ab8f3b21 simplified interfaces, some restructuring
krauss
parents: 22733
diff changeset
   325
      val mdomintros = map_option (map (full_simplify rew_ss)) domintros
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   326
    in
22733
0b14bb35be90 definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents: 22623
diff changeset
   327
      FundefResult { fs=fs, G=G, R=R,
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   328
                     psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   329
                     cases=cases, termination=mtermination,
23189
4574ab8f3b21 simplified interfaces, some restructuring
krauss
parents: 22733
diff changeset
   330
                     domintros=mdomintros,
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   331
                     trsimps=mtrsimps}
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   332
    end
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   333
      
23189
4574ab8f3b21 simplified interfaces, some restructuring
krauss
parents: 22733
diff changeset
   334
fun prepare_fundef_mutual config defname fixes eqss lthy =
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   335
    let
22323
b8c227d8ca91 beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on.
krauss
parents: 22244
diff changeset
   336
      val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   337
      val Mutual {fsum_var=(n, T), qglrs, ...} = mutual
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   338
          
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   339
      val ((fsum, goalstate, cont), lthy') =
23189
4574ab8f3b21 simplified interfaces, some restructuring
krauss
parents: 22733
diff changeset
   340
          FundefCore.prepare_fundef config defname [((n, T), NoSyn)] qglrs lthy
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   341
          
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   342
      val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   343
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   344
      val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual'
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   345
    in
23819
2040846d1bbe some interface cleanup
krauss
parents: 23528
diff changeset
   346
      ((goalstate, mutual_cont), lthy'')
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   347
    end
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   348
21237
b803f9870e97 untabified
krauss
parents: 21051
diff changeset
   349
    
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   350
end