src/ZF/Tools/primrec_package.ML
author wenzelm
Fri, 19 Jan 2007 22:08:08 +0100
changeset 22101 6d13239d5f52
parent 20342 4392003fcbfa
child 24707 dfeb98f84e93
permissions -rw-r--r--
moved parts of OuterParse to SpecParse;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     1
(*  Title:      ZF/Tools/primrec_package.ML
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     2
    ID:         $Id$
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     3
    Author:     Stefan Berghofer and Norbert Voelker
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     4
    Copyright   1998  TU Muenchen
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     5
    ZF version by Lawrence C Paulson (Cambridge)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     6
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     7
Package for defining functions on datatypes by primitive recursion
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     8
*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
     9
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    10
signature PRIMREC_PACKAGE =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    11
sig
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    12
  val quiet_mode: bool ref
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
    13
  val add_primrec: ((bstring * string) * Attrib.src list) list -> theory -> theory * thm list
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18688
diff changeset
    14
  val add_primrec_i: ((bstring * term) * attribute list) list -> theory -> theory * thm list
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    15
end;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    16
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    17
structure PrimrecPackage : PRIMREC_PACKAGE =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    18
struct
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    19
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    20
(* messages *)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    21
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    22
val quiet_mode = ref false;
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    23
fun message s = if ! quiet_mode then () else writeln s;
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    24
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    25
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    26
exception RecError of string;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    27
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
    28
(*Remove outer Trueprop and equality sign*)
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
    29
val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop;
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    30
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    31
fun primrec_err s = error ("Primrec definition error:\n" ^ s);
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    32
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    33
fun primrec_eq_err sign s eq =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    34
  primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    35
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    36
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    37
(* preprocessing of equations *)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    38
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    39
(*rec_fn_opt records equations already noted for this function*)
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    40
fun process_eqn thy (eq, rec_fn_opt) =
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    41
  let
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    42
    val (lhs, rhs) =
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    43
        if null (term_vars eq) then
12203
571d9c288640 avoid handle _;
wenzelm
parents: 12188
diff changeset
    44
            dest_eqn eq handle TERM _ => raise RecError "not a proper equation"
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    45
        else raise RecError "illegal schematic variable(s)";
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    46
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    47
    val (recfun, args) = strip_comb lhs;
12203
571d9c288640 avoid handle _;
wenzelm
parents: 12188
diff changeset
    48
    val (fname, ftype) = dest_Const recfun handle TERM _ =>
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    49
      raise RecError "function is not declared as constant in theory";
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    50
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    51
    val (ls_frees, rest)  = take_prefix is_Free args;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    52
    val (middle, rs_frees) = take_suffix is_Free rest;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    53
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    54
    val (constr, cargs_frees) =
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    55
      if null middle then raise RecError "constructor missing"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    56
      else strip_comb (hd middle);
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    57
    val (cname, _) = dest_Const constr
12203
571d9c288640 avoid handle _;
wenzelm
parents: 12188
diff changeset
    58
      handle TERM _ => raise RecError "ill-formed constructor";
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17314
diff changeset
    59
    val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12876
diff changeset
    60
      handle Option =>
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    61
      raise RecError "cannot determine datatype associated with function"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    62
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    63
    val (ls, cargs, rs) = (map dest_Free ls_frees,
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    64
                           map dest_Free cargs_frees,
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    65
                           map dest_Free rs_frees)
12203
571d9c288640 avoid handle _;
wenzelm
parents: 12188
diff changeset
    66
      handle TERM _ => raise RecError "illegal argument in pattern";
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    67
    val lfrees = ls @ rs @ cargs;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    68
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    69
    (*Constructor, frees to left of pattern, pattern variables,
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    70
      frees to right of pattern, rhs of equation, full original equation. *)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    71
    val new_eqn = (cname, (rhs, cargs, eq))
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    72
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    73
  in
18973
f88976608aad has_duplicates;
wenzelm
parents: 18928
diff changeset
    74
    if has_duplicates (op =) lfrees then
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    75
      raise RecError "repeated variable name in pattern"
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    76
    else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    77
      raise RecError "extra variables on rhs"
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    78
    else if length middle > 1 then
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    79
      raise RecError "more than one non-variable in pattern"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    80
    else case rec_fn_opt of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12876
diff changeset
    81
        NONE => SOME (fname, ftype, ls, rs, con_info, [new_eqn])
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12876
diff changeset
    82
      | SOME (fname', _, ls', rs', con_info': constructor_info, eqns) =>
17314
04e21a27c0ad introduces some modern-style AList operations
haftmann
parents: 17224
diff changeset
    83
          if AList.defined (op =) eqns cname then
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    84
            raise RecError "constructor already occurred as pattern"
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    85
          else if (ls <> ls') orelse (rs <> rs') then
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    86
            raise RecError "non-recursive arguments are inconsistent"
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    87
          else if #big_rec_name con_info <> #big_rec_name con_info' then
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    88
             raise RecError ("Mixed datatypes for function " ^ fname)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    89
          else if fname <> fname' then
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    90
             raise RecError ("inconsistent functions for datatype " ^
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    91
                             #big_rec_name con_info)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12876
diff changeset
    92
          else SOME (fname, ftype, ls, rs, con_info, new_eqn::eqns)
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    93
  end
20342
wenzelm
parents: 20071
diff changeset
    94
  handle RecError s => primrec_eq_err thy s eq;
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    95
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    96
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    97
(*Instantiates a recursor equation with constructor arguments*)
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
    98
fun inst_recursor ((_ $ constr, rhs), cargs') =
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    99
    subst_atomic (#2 (strip_comb constr) ~~ map Free cargs') rhs;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   100
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   101
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   102
(*Convert a list of recursion equations into a recursor call*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   103
fun process_fun thy (fname, ftype, ls, rs, con_info: constructor_info, eqns) =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   104
  let
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   105
    val fconst = Const(fname, ftype)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   106
    val fabs = list_comb (fconst, map Free ls @ [Bound 0] @ map Free rs)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   107
    and {big_rec_name, constructors, rec_rewrites, ...} = con_info
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   108
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   109
    (*Replace X_rec(args,t) by fname(ls,t,rs) *)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   110
    fun use_fabs (_ $ t) = subst_bound (t, fabs)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   111
      | use_fabs t       = t
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   112
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   113
    val cnames         = map (#1 o dest_Const) constructors
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
   114
    and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   115
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   116
    fun absterm (Free(a,T), body) = absfree (a,T,body)
9179
44eabc57ed46 no longer depends upon a prior "open Ind_Syntax" from elsewhere
paulson
parents: 8819
diff changeset
   117
      | absterm (t,body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   118
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   119
    (*Translate rec equations into function arguments suitable for recursor.
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   120
      Missing cases are replaced by 0 and all cases are put into order.*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   121
    fun add_case ((cname, recursor_pair), cases) =
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   122
      let val (rhs, recursor_rhs, eq) =
17314
04e21a27c0ad introduces some modern-style AList operations
haftmann
parents: 17224
diff changeset
   123
            case AList.lookup (op =) eqns cname of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12876
diff changeset
   124
                NONE => (warning ("no equation for constructor " ^ cname ^
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   125
                                  "\nin definition of function " ^ fname);
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   126
                         (Const ("0", Ind_Syntax.iT),
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   127
                          #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12876
diff changeset
   128
              | SOME (rhs, cargs', eq) =>
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   129
                    (rhs, inst_recursor (recursor_pair, cargs'), eq)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   130
          val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   131
          val abs = foldr absterm rhs allowed_terms
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   132
      in
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   133
          if !Ind_Syntax.trace then
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   134
              writeln ("recursor_rhs = " ^
20342
wenzelm
parents: 20071
diff changeset
   135
                       Sign.string_of_term thy recursor_rhs ^
wenzelm
parents: 20071
diff changeset
   136
                       "\nabs = " ^ Sign.string_of_term thy abs)
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   137
          else();
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   138
          if Logic.occs (fconst, abs) then
20342
wenzelm
parents: 20071
diff changeset
   139
              primrec_eq_err thy
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   140
                   ("illegal recursive occurrences of " ^ fname)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   141
                   eq
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   142
          else abs :: cases
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   143
      end
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   144
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   145
    val recursor = head_of (#1 (hd recursor_pairs))
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   146
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   147
    (** make definition **)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   148
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   149
    (*the recursive argument*)
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 20046
diff changeset
   150
    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   151
                        Ind_Syntax.iT)
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   152
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   153
    val def_tm = Logic.mk_equals
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   154
                    (subst_bound (rec_arg, fabs),
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   155
                     list_comb (recursor,
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   156
                                foldr add_case [] (cnames ~~ recursor_pairs))
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   157
                     $ rec_arg)
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   158
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   159
  in
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   160
      if !Ind_Syntax.trace then
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   161
            writeln ("primrec def:\n" ^
20342
wenzelm
parents: 20071
diff changeset
   162
                     Sign.string_of_term thy def_tm)
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   163
      else();
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   164
      (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   165
       def_tm)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   166
  end;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   167
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   168
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   169
(* prepare functions needed for definitions *)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   170
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   171
fun add_primrec_i args thy =
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   172
  let
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   173
    val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 12876
diff changeset
   174
    val SOME (fname, ftype, ls, rs, con_info, eqns) =
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   175
      foldr (process_eqn thy) NONE eqn_terms;
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   176
    val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   177
18358
0a733e11021a re-oriented some result tuples in PureThy
haftmann
parents: 17985
diff changeset
   178
    val ([def_thm], thy1) = thy
12188
e4279b7fb8cc fix path prefix;
wenzelm
parents: 12183
diff changeset
   179
      |> Theory.add_path (Sign.base_name fname)
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   180
      |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   181
8438
b8389b4fca9c adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7904
diff changeset
   182
    val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   183
    val eqn_thms =
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   184
     (message ("Proving equations for primrec function " ^ fname);
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   185
      eqn_terms |> map (fn t =>
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 18973
diff changeset
   186
        Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t)
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 18973
diff changeset
   187
          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])));
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   188
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   189
    val (eqn_thms', thy2) =
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   190
      thy1
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   191
      |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   192
    val (_, thy3) =
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   193
      thy2
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18688
diff changeset
   194
      |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   195
      ||> Theory.parent_path;
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   196
  in (thy3, eqn_thms') end;
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   197
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   198
fun add_primrec args thy =
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   199
  add_primrec_i (map (fn ((name, s), srcs) =>
20342
wenzelm
parents: 20071
diff changeset
   200
    ((name, Sign.read_prop thy s), map (Attrib.attribute thy) srcs))
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   201
    args) thy;
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   202
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   203
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   204
(* outer syntax *)
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   205
17057
0934ac31985f OuterKeyword;
wenzelm
parents: 15705
diff changeset
   206
local structure P = OuterParse and K = OuterKeyword in
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   207
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 20342
diff changeset
   208
val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   209
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   210
val primrecP =
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   211
  OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   212
    (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   213
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   214
val _ = OuterSyntax.add_parsers [primrecP];
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   215
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   216
end;
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   217
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 9329
diff changeset
   218
end;
15705
b5edb9dcec9a *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
   219
b5edb9dcec9a *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
   220