src/HOL/Tools/function_package/fundef_datatype.ML
author krauss
Tue Nov 07 11:53:55 2006 +0100 (2006-11-07)
changeset 21211 5370cfbf3070
parent 21051 c49467a9c1e1
child 21240 8e75fb38522c
permissions -rw-r--r--
Preparations for making "lexicographic_order" part of "fun"
krauss@19564
     1
(*  Title:      HOL/Tools/function_package/fundef_datatype.ML
krauss@19564
     2
    ID:         $Id$
krauss@19564
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@19564
     4
wenzelm@20344
     5
A package for general recursive function definitions.
krauss@19564
     6
A tactic to prove completeness of datatype patterns.
krauss@19564
     7
*)
krauss@19564
     8
wenzelm@20344
     9
signature FUNDEF_DATATYPE =
krauss@19564
    10
sig
krauss@19564
    11
    val pat_complete_tac: int -> tactic
krauss@19564
    12
krauss@20523
    13
    val pat_completeness : method
krauss@19564
    14
    val setup : theory -> theory
krauss@19564
    15
end
krauss@19564
    16
krauss@19564
    17
structure FundefDatatype : FUNDEF_DATATYPE =
krauss@19564
    18
struct
krauss@19564
    19
krauss@21051
    20
open FundefLib
krauss@21051
    21
open FundefCommon
krauss@19770
    22
krauss@19564
    23
fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
krauss@19564
    24
fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
krauss@19564
    25
krauss@19564
    26
fun inst_free var inst thm =
krauss@19564
    27
    forall_elim inst (forall_intr var thm)
krauss@19564
    28
krauss@19564
    29
krauss@19564
    30
fun inst_case_thm thy x P thm =
krauss@19564
    31
    let
wenzelm@20344
    32
        val [Pv, xv] = term_vars (prop_of thm)
krauss@19564
    33
    in
wenzelm@20344
    34
        cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
krauss@19564
    35
    end
krauss@19564
    36
krauss@19564
    37
krauss@19564
    38
fun invent_vars constr i =
krauss@19564
    39
    let
wenzelm@20344
    40
        val Ts = binder_types (fastype_of constr)
wenzelm@20344
    41
        val j = i + length Ts
wenzelm@20344
    42
        val is = i upto (j - 1)
wenzelm@20344
    43
        val avs = map2 mk_argvar is Ts
wenzelm@20344
    44
        val pvs = map2 mk_patvar is Ts
krauss@19564
    45
    in
wenzelm@20344
    46
        (avs, pvs, j)
krauss@19564
    47
    end
krauss@19564
    48
krauss@19564
    49
krauss@19564
    50
fun filter_pats thy cons pvars [] = []
krauss@19564
    51
  | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
wenzelm@20344
    52
  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
krauss@19564
    53
    case pat of
wenzelm@20344
    54
        Free _ => let val inst = list_comb (cons, pvars)
wenzelm@20344
    55
                 in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
wenzelm@20344
    56
                    :: (filter_pats thy cons pvars pts) end
krauss@19564
    57
      | _ => if fst (strip_comb pat) = cons
wenzelm@20344
    58
             then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
wenzelm@20344
    59
             else filter_pats thy cons pvars pts
krauss@19564
    60
krauss@19564
    61
krauss@19564
    62
fun inst_constrs_of thy (T as Type (name, _)) =
wenzelm@20344
    63
        map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
wenzelm@20344
    64
            (the (DatatypePackage.get_datatype_constrs thy name))
krauss@19564
    65
  | inst_constrs_of thy _ = raise Match
krauss@19564
    66
krauss@19564
    67
krauss@19564
    68
fun transform_pat thy avars c_assum ([] , thm) = raise Match
krauss@19564
    69
  | transform_pat thy avars c_assum (pat :: pats, thm) =
krauss@19564
    70
    let
wenzelm@20344
    71
        val (_, subps) = strip_comb pat
wenzelm@20344
    72
        val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
wenzelm@20344
    73
        val a_eqs = map assume eqs
wenzelm@20344
    74
        val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
krauss@19564
    75
    in
wenzelm@20344
    76
        (subps @ pats, fold_rev implies_intr eqs
wenzelm@20344
    77
                                (implies_elim thm c_eq_pat))
krauss@19564
    78
    end
krauss@19564
    79
krauss@19564
    80
krauss@19564
    81
exception COMPLETENESS
krauss@19564
    82
krauss@19564
    83
fun constr_case thy P idx (v :: vs) pats cons =
krauss@19564
    84
    let
wenzelm@20344
    85
        val (avars, pvars, newidx) = invent_vars cons idx
wenzelm@20344
    86
        val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
wenzelm@20344
    87
        val c_assum = assume c_hyp
wenzelm@20344
    88
        val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
krauss@19564
    89
    in
wenzelm@20344
    90
        o_alg thy P newidx (avars @ vs) newpats
wenzelm@20344
    91
              |> implies_intr c_hyp
wenzelm@20344
    92
              |> fold_rev (forall_intr o cterm_of thy) avars
krauss@19564
    93
    end
krauss@19564
    94
  | constr_case _ _ _ _ _ _ = raise Match
krauss@19564
    95
and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
krauss@19564
    96
  | o_alg thy P idx (v :: vs) [] = raise COMPLETENESS
krauss@19564
    97
  | o_alg thy P idx (v :: vs) pts =
krauss@19564
    98
    if forall (is_Free o hd o fst) pts (* Var case *)
krauss@19564
    99
    then o_alg thy P idx vs (map (fn (pv :: pats, thm) =>
wenzelm@20344
   100
                               (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
krauss@19564
   101
    else (* Cons case *)
wenzelm@20344
   102
         let
wenzelm@20344
   103
             val T = fastype_of v
wenzelm@20344
   104
             val (tname, _) = dest_Type T
wenzelm@20344
   105
             val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname
wenzelm@20344
   106
             val constrs = inst_constrs_of thy T
wenzelm@20344
   107
             val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
wenzelm@20344
   108
         in
wenzelm@20344
   109
             inst_case_thm thy v P case_thm
wenzelm@20344
   110
                           |> fold (curry op COMP) c_cases
wenzelm@20344
   111
         end
krauss@19564
   112
  | o_alg _ _ _ _ _ = raise Match
krauss@19564
   113
wenzelm@20344
   114
krauss@19564
   115
fun prove_completeness thy x P qss pats =
krauss@19564
   116
    let
wenzelm@20344
   117
        fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)),
wenzelm@20344
   118
                                                HOLogic.mk_Trueprop P)
wenzelm@20344
   119
                                               |> fold_rev mk_forall qs
wenzelm@20344
   120
                                               |> cterm_of thy
krauss@19564
   121
wenzelm@20344
   122
        val hyps = map2 mk_assum qss pats
krauss@19564
   123
wenzelm@20344
   124
        fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
krauss@19564
   125
wenzelm@20344
   126
        val assums = map2 inst_hyps hyps qss
krauss@19564
   127
    in
wenzelm@20344
   128
        o_alg thy P 2 [x] (map2 (pair o single) pats assums)
wenzelm@20344
   129
              |> fold_rev implies_intr hyps
krauss@19564
   130
    end
krauss@19564
   131
krauss@19564
   132
krauss@19564
   133
krauss@19564
   134
fun pat_complete_tac i thm =
wenzelm@20344
   135
    let
krauss@19922
   136
      val thy = theory_of_thm thm
krauss@19922
   137
wenzelm@20344
   138
        val subgoal = nth (prems_of thm) (i - 1)   (* FIXME SUBGOAL tactical *)
krauss@19922
   139
krauss@19922
   140
        val ([P, x], subgf) = dest_all_all subgoal
krauss@19922
   141
wenzelm@20344
   142
        val assums = Logic.strip_imp_prems subgf
krauss@19564
   143
wenzelm@20344
   144
        fun pat_of assum =
wenzelm@20344
   145
            let
wenzelm@20344
   146
                val (qs, imp) = dest_all_all assum
wenzelm@20344
   147
            in
wenzelm@20344
   148
                case Logic.dest_implies imp of
wenzelm@20344
   149
                    (_ $ (_ $ _ $ pat), _) => (qs, pat)
wenzelm@20344
   150
                  | _ => raise COMPLETENESS
wenzelm@20344
   151
            end
krauss@19564
   152
wenzelm@20344
   153
        val (qss, pats) = split_list (map pat_of assums)
wenzelm@20344
   154
wenzelm@20344
   155
        val complete_thm = prove_completeness thy x P qss pats
krauss@19922
   156
                                              |> forall_intr (cterm_of thy x)
krauss@19922
   157
                                              |> forall_intr (cterm_of thy P)
krauss@19564
   158
    in
wenzelm@20344
   159
        Seq.single (Drule.compose_single(complete_thm, i, thm))
krauss@19564
   160
    end
krauss@19564
   161
    handle COMPLETENESS => Seq.empty
krauss@19564
   162
krauss@19564
   163
krauss@20523
   164
val pat_completeness = Method.SIMPLE_METHOD (pat_complete_tac 1)
krauss@20523
   165
krauss@20523
   166
val by_pat_completeness_simp =
krauss@20523
   167
    Proof.global_terminal_proof
krauss@20523
   168
      (Method.Basic (K pat_completeness),
krauss@20523
   169
       SOME (Method.Source (Args.src (("simp_all", []), Position.none))))
wenzelm@20999
   170
         (* FIXME avoid dynamic scoping of method name! *)
krauss@20523
   171
krauss@21211
   172
fun termination_by_lexicographic_order name =
krauss@21211
   173
    FundefPackage.setup_termination_proof (SOME name)
krauss@21211
   174
    #> Proof.global_terminal_proof (Method.Basic (K LexicographicOrder.lexicographic_order), NONE)
krauss@19564
   175
wenzelm@20344
   176
val setup =
krauss@20523
   177
    Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")]
krauss@20523
   178
krauss@20523
   179
krauss@20523
   180
krauss@20523
   181
krauss@20523
   182
local structure P = OuterParse and K = OuterKeyword in
krauss@20523
   183
krauss@20523
   184
krauss@20523
   185
fun or_list1 s = P.enum1 "|" s
krauss@20523
   186
val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
krauss@20523
   187
val statement_ow = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 (P.prop -- Scan.optional (otherwise >> K true) false))
krauss@20523
   188
val statements_ow = or_list1 statement_ow
krauss@19564
   189
krauss@21211
   190
krauss@21211
   191
fun fun_cmd fixes statements lthy =
krauss@21211
   192
    lthy
krauss@21211
   193
      |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config
krauss@21211
   194
      ||> by_pat_completeness_simp
krauss@21211
   195
      (*|-> termination_by_lexicographic_order*) |> snd
krauss@21211
   196
krauss@21211
   197
krauss@20523
   198
val funP =
krauss@20523
   199
  OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl
krauss@20523
   200
  ((P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
krauss@20523
   201
     >> (fn ((target, fixes), statements) =>
krauss@21211
   202
            (Toplevel.local_theory target (fun_cmd fixes statements))));
krauss@20523
   203
krauss@20523
   204
val _ = OuterSyntax.add_parsers [funP];
wenzelm@20344
   205
end
krauss@20523
   206
wenzelm@20875
   207
end