src/ZF/Tools/primrec_package.ML
author wenzelm
Thu, 30 Nov 2000 20:04:16 +0100
changeset 10548 e8c774c12105
parent 9329 d2655dc8a4b4
child 12183 c10cea75dd56
permissions -rw-r--r--
'consumes' att;
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
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    12
  val add_primrec_i : (string * term) list -> theory -> theory * thm list
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    13
  val add_primrec   : (string * string) list -> theory -> theory * thm list
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    14
end;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    15
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    16
structure PrimrecPackage : PRIMREC_PACKAGE =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    17
struct
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    18
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    19
exception RecError of string;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    20
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
    21
(*Remove outer Trueprop and equality sign*)
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
    22
val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop;
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    23
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    24
fun primrec_err s = error ("Primrec definition error:\n" ^ s);
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    25
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    26
fun primrec_eq_err sign s eq =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    27
  primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    28
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    29
(* preprocessing of equations *)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    30
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    31
(*rec_fn_opt records equations already noted for this function*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    32
fun process_eqn thy (eq, rec_fn_opt) = 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    33
  let
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
    34
    val (lhs, rhs) = 
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
    35
	if null (term_vars eq) then
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
    36
	    dest_eqn eq handle _ => raise RecError "not a proper equation"
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
    37
	else raise RecError "illegal schematic variable(s)";
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    38
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    39
    val (recfun, args) = strip_comb lhs;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    40
    val (fname, ftype) = dest_Const recfun handle _ => 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    41
      raise RecError "function is not declared as constant in theory";
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    42
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    43
    val (ls_frees, rest)  = take_prefix is_Free args;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    44
    val (middle, rs_frees) = take_suffix is_Free rest;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    45
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    46
    val (constr, cargs_frees) = 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    47
      if null middle then raise RecError "constructor missing"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    48
      else strip_comb (hd middle);
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    49
    val (cname, _) = dest_Const constr
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    50
      handle _ => raise RecError "ill-formed constructor";
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    51
    val con_info = the (Symtab.lookup (ConstructorsData.get thy, cname))
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    52
      handle _ =>
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    53
      raise RecError "cannot determine datatype associated with function"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    54
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    55
    val (ls, cargs, rs) = (map dest_Free ls_frees, 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    56
			   map dest_Free cargs_frees, 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    57
			   map dest_Free rs_frees)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    58
      handle _ => raise RecError "illegal argument in pattern";
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    59
    val lfrees = ls @ rs @ cargs;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    60
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    61
    (*Constructor, frees to left of pattern, pattern variables,
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    62
      frees to right of pattern, rhs of equation, full original equation. *)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    63
    val new_eqn = (cname, (rhs, cargs, eq))
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    64
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    65
  in
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    66
    if not (null (duplicates lfrees)) then 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    67
      raise RecError "repeated variable name in pattern" 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    68
    else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    69
      raise RecError "extra variables on rhs"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    70
    else if length middle > 1 then 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    71
      raise RecError "more than one non-variable in pattern"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    72
    else case rec_fn_opt of
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    73
        None => Some (fname, ftype, ls, rs, con_info, [new_eqn])
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    74
      | Some (fname', _, ls', rs', con_info': constructor_info, eqns) => 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    75
	  if is_some (assoc (eqns, cname)) then
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    76
	    raise RecError "constructor already occurred as pattern"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    77
	  else if (ls <> ls') orelse (rs <> rs') then
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    78
	    raise RecError "non-recursive arguments are inconsistent"
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    79
	  else if #big_rec_name con_info <> #big_rec_name con_info' then
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    80
	     raise RecError ("Mixed datatypes for function " ^ fname)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    81
	  else if fname <> fname' then
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    82
	     raise RecError ("inconsistent functions for datatype " ^ 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    83
			     #big_rec_name con_info)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    84
	  else Some (fname, ftype, ls, rs, con_info, new_eqn::eqns)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    85
  end
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    86
  handle RecError s => primrec_eq_err (sign_of thy) s eq;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    87
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    88
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    89
(*Instantiates a recursor equation with constructor arguments*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    90
fun inst_recursor ((_ $ constr, rhs), cargs') = 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    91
    subst_atomic (#2 (strip_comb constr) ~~ map Free cargs') rhs;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    92
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    93
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    94
(*Convert a list of recursion equations into a recursor call*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    95
fun process_fun thy (fname, ftype, ls, rs, con_info: constructor_info, eqns) =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    96
  let
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    97
    val fconst = Const(fname, ftype)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    98
    val fabs = list_comb (fconst, map Free ls @ [Bound 0] @ map Free rs)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
    99
    and {big_rec_name, constructors, rec_rewrites, ...} = con_info
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   100
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   101
    (*Replace X_rec(args,t) by fname(ls,t,rs) *)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   102
    fun use_fabs (_ $ t) = subst_bound (t, fabs)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   103
      | use_fabs t       = t
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   104
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   105
    val cnames         = map (#1 o dest_Const) constructors
6141
a6922171b396 removal of the (thm list) argument of mk_cases
paulson
parents: 6092
diff changeset
   106
    and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   107
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   108
    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
   109
      | absterm (t,body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body))
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   110
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   111
    (*Translate rec equations into function arguments suitable for recursor.
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   112
      Missing cases are replaced by 0 and all cases are put into order.*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   113
    fun add_case ((cname, recursor_pair), cases) =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   114
      let val (rhs, recursor_rhs, eq) = 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   115
	    case assoc (eqns, cname) of
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   116
		None => (warning ("no equation for constructor " ^ cname ^
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   117
				  "\nin definition of function " ^ fname);
9179
44eabc57ed46 no longer depends upon a prior "open Ind_Syntax" from elsewhere
paulson
parents: 8819
diff changeset
   118
			 (Const ("0", Ind_Syntax.iT), 
44eabc57ed46 no longer depends upon a prior "open Ind_Syntax" from elsewhere
paulson
parents: 8819
diff changeset
   119
			  #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   120
	      | Some (rhs, cargs', eq) =>
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   121
		    (rhs, inst_recursor (recursor_pair, cargs'), eq)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   122
	  val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   123
	  val abs = foldr absterm (allowed_terms, rhs)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   124
      in 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   125
          if !Ind_Syntax.trace then
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   126
	      writeln ("recursor_rhs = " ^ 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   127
		       Sign.string_of_term (sign_of thy) recursor_rhs ^
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   128
		       "\nabs = " ^ Sign.string_of_term (sign_of thy) abs)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   129
          else();
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   130
	  if Logic.occs (fconst, abs) then 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   131
	      primrec_eq_err (sign_of thy) 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   132
	           ("illegal recursive occurrences of " ^ fname)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   133
		   eq
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   134
	  else abs :: cases
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   135
      end
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   136
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   137
    val recursor = head_of (#1 (hd recursor_pairs))
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   138
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   139
    (** make definition **)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   140
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   141
    (*the recursive argument*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   142
    val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
9179
44eabc57ed46 no longer depends upon a prior "open Ind_Syntax" from elsewhere
paulson
parents: 8819
diff changeset
   143
			Ind_Syntax.iT)
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   144
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   145
    val def_tm = Logic.mk_equals
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   146
	            (subst_bound (rec_arg, fabs),
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   147
		     list_comb (recursor,
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   148
				foldr add_case (cnames ~~ recursor_pairs, []))
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   149
		     $ rec_arg)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   150
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   151
  in
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   152
      if !Ind_Syntax.trace then
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   153
	    writeln ("primrec def:\n" ^ 
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   154
		     Sign.string_of_term (sign_of thy) def_tm)
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   155
      else();
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   156
      (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   157
       def_tm)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   158
  end;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   159
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   160
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   161
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   162
(* prepare functions needed for definitions *)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   163
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   164
(*Each equation is paired with an optional name, which is "_" (ML wildcard)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   165
  if omitted.*)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   166
fun add_primrec_i recursion_eqns thy =
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   167
  let
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   168
    val Some (fname, ftype, ls, rs, con_info, eqns) = 
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   169
	foldr (process_eqn thy) (map snd recursion_eqns, None);
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   170
    val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns) 
8438
b8389b4fca9c adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7904
diff changeset
   171
    val (thy', [def_thm]) = thy |> Theory.add_path (Sign.base_name (#1 def))
9329
d2655dc8a4b4 adapted PureThy.add_defs_i;
wenzelm
parents: 9179
diff changeset
   172
                   |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]
8438
b8389b4fca9c adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7904
diff changeset
   173
    val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   174
    val char_thms = 
6092
d9db67970c73 eliminated tthm type and Attribute structure;
wenzelm
parents: 6065
diff changeset
   175
	(if !Ind_Syntax.trace then	(* FIXME message / quiet_mode (!?) *)
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   176
	     writeln ("Proving equations for primrec function " ^ fname)
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   177
	 else ();
6092
d9db67970c73 eliminated tthm type and Attribute structure;
wenzelm
parents: 6065
diff changeset
   178
	 map (fn (_,t) =>
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   179
	      prove_goalw_cterm rewrites
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   180
		(Ind_Syntax.traceIt "next primrec equation = "
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   181
		 (cterm_of (sign_of thy') t))
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   182
	      (fn _ => [rtac refl 1]))
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6050
diff changeset
   183
	 recursion_eqns);
6092
d9db67970c73 eliminated tthm type and Attribute structure;
wenzelm
parents: 6065
diff changeset
   184
    val simps = char_thms;
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   185
    val thy'' = thy' 
8438
b8389b4fca9c adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7904
diff changeset
   186
      |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
b8389b4fca9c adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7904
diff changeset
   187
      |> (#1 o PureThy.add_thms (map (rpair [])
b8389b4fca9c adapted to new PureThy.add_thms etc.;
wenzelm
parents: 7904
diff changeset
   188
         (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps))))
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   189
      |> Theory.parent_path;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   190
  in
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   191
    (thy'', char_thms)
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   192
  end;
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   193
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   194
fun add_primrec eqns thy =
8819
d04923e183c7 use Sign.simple_read_term;
wenzelm
parents: 8438
diff changeset
   195
  add_primrec_i (map (apsnd (Sign.simple_read_term (sign_of thy) propT)) eqns) thy;
6050
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   196
b3eb3de3a288 new primrec package
paulson
parents:
diff changeset
   197
end;