src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
author wenzelm
Fri Nov 13 19:57:46 2009 +0100 (2009-11-13)
changeset 33669 ae9a2ea9a989
parent 33643 b275f26a638b
child 33726 0878aecbf119
permissions -rw-r--r--
inductive: eliminated obsolete kind;
wenzelm@33265
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
wenzelm@33265
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@33250
     3
wenzelm@33265
     4
Preprocessing functions to predicates.
bulwahn@33250
     5
*)
bulwahn@33250
     6
bulwahn@33250
     7
signature PREDICATE_COMPILE_FUN =
bulwahn@33250
     8
sig
bulwahn@33630
     9
  val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
bulwahn@33250
    10
  val rewrite_intro : theory -> thm -> thm list
bulwahn@33250
    11
  val pred_of_function : theory -> string -> string option
bulwahn@33250
    12
end;
bulwahn@33250
    13
bulwahn@33250
    14
structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
bulwahn@33250
    15
struct
bulwahn@33250
    16
bulwahn@33250
    17
fun is_funtype (Type ("fun", [_, _])) = true
bulwahn@33250
    18
  | is_funtype _ = false;
bulwahn@33250
    19
bulwahn@33250
    20
fun is_Type (Type _) = true
bulwahn@33250
    21
  | is_Type _ = false
bulwahn@33250
    22
bulwahn@33250
    23
(* returns true if t is an application of an datatype constructor *)
bulwahn@33250
    24
(* which then consequently would be splitted *)
bulwahn@33250
    25
(* else false *)
bulwahn@33250
    26
(*
bulwahn@33250
    27
fun is_constructor thy t =
bulwahn@33250
    28
  if (is_Type (fastype_of t)) then
bulwahn@33250
    29
    (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
bulwahn@33250
    30
      NONE => false
bulwahn@33250
    31
    | SOME info => (let
bulwahn@33250
    32
      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
bulwahn@33250
    33
      val (c, _) = strip_comb t
bulwahn@33250
    34
      in (case c of
bulwahn@33250
    35
        Const (name, _) => name mem_string constr_consts
bulwahn@33250
    36
        | _ => false) end))
bulwahn@33250
    37
  else false
bulwahn@33250
    38
*)
bulwahn@33250
    39
bulwahn@33250
    40
(* must be exported in code.ML *)
bulwahn@33250
    41
fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
bulwahn@33250
    42
bulwahn@33250
    43
(* Table from constant name (string) to term of inductive predicate *)
wenzelm@33522
    44
structure Pred_Compile_Preproc = Theory_Data
bulwahn@33250
    45
(
bulwahn@33250
    46
  type T = string Symtab.table;
bulwahn@33250
    47
  val empty = Symtab.empty;
bulwahn@33250
    48
  val extend = I;
wenzelm@33522
    49
  fun merge data : T = Symtab.merge (op =) data;   (* FIXME handle Symtab.DUP ?? *)
bulwahn@33250
    50
)
bulwahn@33250
    51
bulwahn@33250
    52
fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
bulwahn@33250
    53
bulwahn@33250
    54
fun defined thy = Symtab.defined (Pred_Compile_Preproc.get thy) 
bulwahn@33250
    55
bulwahn@33250
    56
bulwahn@33250
    57
fun transform_ho_typ (T as Type ("fun", _)) =
bulwahn@33250
    58
  let
bulwahn@33250
    59
    val (Ts, T') = strip_type T
bulwahn@33250
    60
  in if T' = @{typ "bool"} then T else (Ts @ [T']) ---> HOLogic.boolT end
bulwahn@33250
    61
| transform_ho_typ t = t
bulwahn@33250
    62
bulwahn@33250
    63
fun transform_ho_arg arg = 
bulwahn@33250
    64
  case (fastype_of arg) of
bulwahn@33250
    65
    (T as Type ("fun", _)) =>
bulwahn@33250
    66
      (case arg of
bulwahn@33250
    67
        Free (name, _) => Free (name, transform_ho_typ T)
bulwahn@33250
    68
      | _ => error "I am surprised")
bulwahn@33250
    69
| _ => arg
bulwahn@33250
    70
bulwahn@33250
    71
fun pred_type T =
bulwahn@33250
    72
  let
bulwahn@33250
    73
    val (Ts, T') = strip_type T
bulwahn@33250
    74
    val Ts' = map transform_ho_typ Ts
bulwahn@33250
    75
  in
bulwahn@33250
    76
    (Ts' @ [T']) ---> HOLogic.boolT
bulwahn@33250
    77
  end;
bulwahn@33250
    78
bulwahn@33250
    79
(* FIXME: create new predicate name -- does not avoid nameclashing *)
bulwahn@33250
    80
fun pred_of f =
bulwahn@33250
    81
  let
bulwahn@33250
    82
    val (name, T) = dest_Const f
bulwahn@33250
    83
  in
bulwahn@33250
    84
    if (body_type T = @{typ bool}) then
bulwahn@33250
    85
      (Free (Long_Name.base_name name ^ "P", T))
bulwahn@33250
    86
    else
bulwahn@33250
    87
      (Free (Long_Name.base_name name ^ "P", pred_type T))
bulwahn@33250
    88
  end
bulwahn@33250
    89
bulwahn@33250
    90
fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t
bulwahn@33250
    91
  | mk_param thy lookup_pred t =
bulwahn@33250
    92
  let
bulwahn@33250
    93
  val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t))
bulwahn@33250
    94
  in if Predicate_Compile_Aux.is_predT (fastype_of t) then
bulwahn@33250
    95
    t
bulwahn@33250
    96
  else
bulwahn@33250
    97
    let
bulwahn@33250
    98
      val (vs, body) = strip_abs t
bulwahn@33250
    99
      val names = Term.add_free_names body []
bulwahn@33250
   100
      val vs_names = Name.variant_list names (map fst vs)
bulwahn@33250
   101
      val vs' = map2 (curry Free) vs_names (map snd vs)
bulwahn@33250
   102
      val body' = subst_bounds (rev vs', body)
bulwahn@33250
   103
      val (f, args) = strip_comb body'
bulwahn@33250
   104
      val resname = Name.variant (vs_names @ names) "res"
bulwahn@33250
   105
      val resvar = Free (resname, body_type (fastype_of body'))
bulwahn@33250
   106
      (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param"
bulwahn@33250
   107
      val pred_body = list_comb (P, args @ [resvar])
bulwahn@33250
   108
      *)
bulwahn@33250
   109
      val pred_body = HOLogic.mk_eq (body', resvar)
bulwahn@33250
   110
      val param = fold_rev lambda (vs' @ [resvar]) pred_body
bulwahn@33250
   111
    in param end
bulwahn@33250
   112
  end
bulwahn@33250
   113
(* creates the list of premises for every intro rule *)
bulwahn@33250
   114
(* theory -> term -> (string list, term list list) *)
bulwahn@33250
   115
bulwahn@33250
   116
fun dest_code_eqn eqn = let
bulwahn@33250
   117
  val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn))
bulwahn@33250
   118
  val (func, args) = strip_comb lhs
bulwahn@33250
   119
in ((func, args), rhs) end;
bulwahn@33250
   120
bulwahn@33250
   121
fun string_of_typ T = Syntax.string_of_typ_global @{theory} T
bulwahn@33250
   122
bulwahn@33250
   123
fun string_of_term t =
bulwahn@33250
   124
  case t of
bulwahn@33250
   125
    Const (c, T) => "Const (" ^ c ^ ", " ^ string_of_typ T ^ ")"
bulwahn@33250
   126
  | Free (c, T) => "Free (" ^ c ^ ", " ^ string_of_typ T ^ ")"
bulwahn@33250
   127
  | Var ((c, i), T) => "Var ((" ^ c ^ ", " ^ string_of_int i ^ "), " ^ string_of_typ T ^ ")"
bulwahn@33250
   128
  | Bound i => "Bound " ^ string_of_int i
bulwahn@33250
   129
  | Abs (x, T, t) => "Abs (" ^ x ^ ", " ^ string_of_typ T ^ ", " ^ string_of_term t ^ ")"
bulwahn@33250
   130
  | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")"
bulwahn@33250
   131
  
bulwahn@33250
   132
fun ind_package_get_nparams thy name =
bulwahn@33250
   133
  case try (Inductive.the_inductive (ProofContext.init thy)) name of
bulwahn@33250
   134
    SOME (_, result) => length (Inductive.params_of (#raw_induct result))
bulwahn@33250
   135
  | NONE => error ("No such predicate: " ^ quote name) 
bulwahn@33250
   136
bulwahn@33250
   137
(* TODO: does not work with higher order functions yet *)
bulwahn@33250
   138
fun mk_rewr_eq (func, pred) =
bulwahn@33250
   139
  let
bulwahn@33250
   140
    val (argTs, resT) = (strip_type (fastype_of func))
bulwahn@33250
   141
    val nctxt =
bulwahn@33250
   142
      Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
bulwahn@33250
   143
    val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
bulwahn@33250
   144
    val ([resname], nctxt'') = Name.variants ["r"] nctxt'
bulwahn@33250
   145
    val args = map Free (argnames ~~ argTs)
bulwahn@33250
   146
    val res = Free (resname, resT)
bulwahn@33250
   147
  in Logic.mk_equals
bulwahn@33250
   148
      (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
bulwahn@33250
   149
  end;
bulwahn@33250
   150
bulwahn@33250
   151
fun has_split_rule_cname @{const_name "nat_case"} = true
bulwahn@33250
   152
  | has_split_rule_cname @{const_name "list_case"} = true
bulwahn@33250
   153
  | has_split_rule_cname _ = false
bulwahn@33250
   154
  
bulwahn@33250
   155
fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true 
bulwahn@33250
   156
  | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true 
bulwahn@33250
   157
  | has_split_rule_term thy _ = false
bulwahn@33250
   158
bulwahn@33250
   159
fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
bulwahn@33250
   160
  | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
bulwahn@33250
   161
  | has_split_rule_term' thy c = has_split_rule_term thy c
bulwahn@33250
   162
  
bulwahn@33250
   163
fun prepare_split_thm ctxt split_thm =
bulwahn@33250
   164
    (split_thm RS @{thm iffD2})
bulwahn@33250
   165
    |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
bulwahn@33250
   166
      @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
bulwahn@33250
   167
bulwahn@33250
   168
fun find_split_thm thy (Const (name, typ)) =
bulwahn@33250
   169
  let
bulwahn@33250
   170
    fun split_name str =
bulwahn@33250
   171
      case first_field "." str
bulwahn@33250
   172
        of (SOME (field, rest)) => field :: split_name rest
bulwahn@33250
   173
         | NONE => [str]
bulwahn@33250
   174
    val splitted_name = split_name name
bulwahn@33250
   175
  in
bulwahn@33250
   176
    if length splitted_name > 0 andalso
bulwahn@33250
   177
       String.isSuffix "_case" (List.last splitted_name)
bulwahn@33250
   178
    then
bulwahn@33250
   179
      (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
bulwahn@33250
   180
      |> space_implode "."
bulwahn@33250
   181
      |> PureThy.get_thm thy
bulwahn@33250
   182
      |> SOME
bulwahn@33250
   183
      handle ERROR msg => NONE
bulwahn@33250
   184
    else NONE
bulwahn@33250
   185
  end
bulwahn@33250
   186
  | find_split_thm _ _ = NONE
bulwahn@33250
   187
bulwahn@33250
   188
fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
bulwahn@33250
   189
  | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
bulwahn@33250
   190
  | find_split_thm' thy c = find_split_thm thy c
bulwahn@33250
   191
bulwahn@33250
   192
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
bulwahn@33250
   193
bulwahn@33250
   194
fun folds_map f xs y =
bulwahn@33250
   195
  let
bulwahn@33250
   196
    fun folds_map' acc [] y = [(rev acc, y)]
bulwahn@33250
   197
      | folds_map' acc (x :: xs) y =
bulwahn@33250
   198
        maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y)
bulwahn@33250
   199
    in
bulwahn@33250
   200
      folds_map' [] xs y
bulwahn@33250
   201
    end;
bulwahn@33250
   202
bulwahn@33250
   203
fun mk_prems thy (lookup_pred, get_nparams) t (names, prems) =
bulwahn@33250
   204
  let
bulwahn@33250
   205
    fun mk_prems' (t as Const (name, T)) (names, prems) =
bulwahn@33250
   206
      if is_constr thy name orelse (is_none (try lookup_pred t)) then
bulwahn@33250
   207
        [(t, (names, prems))]
bulwahn@33250
   208
      else [(lookup_pred t, (names, prems))]
bulwahn@33250
   209
    | mk_prems' (t as Free (f, T)) (names, prems) = 
bulwahn@33250
   210
      [(lookup_pred t, (names, prems))]
bulwahn@33250
   211
    | mk_prems' (t as Abs _) (names, prems) =
bulwahn@33250
   212
      if Predicate_Compile_Aux.is_predT (fastype_of t) then
bulwahn@33250
   213
      [(t, (names, prems))] else error "mk_prems': Abs "
bulwahn@33250
   214
      (* mk_param *)
bulwahn@33250
   215
    | mk_prems' t (names, prems) =
bulwahn@33250
   216
      if Predicate_Compile_Aux.is_constrt thy t then
bulwahn@33250
   217
        [(t, (names, prems))]
bulwahn@33250
   218
      else
bulwahn@33250
   219
        if has_split_rule_term' thy (fst (strip_comb t)) then
bulwahn@33250
   220
          let
bulwahn@33250
   221
            val (f, args) = strip_comb t
bulwahn@33250
   222
            val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
bulwahn@33250
   223
            (* TODO: contextify things - this line is to unvarify the split_thm *)
bulwahn@33250
   224
            (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
bulwahn@33250
   225
            val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
bulwahn@33250
   226
            val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
bulwahn@33250
   227
            val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
bulwahn@33250
   228
            val (_, split_args) = strip_comb split_t
bulwahn@33250
   229
            val match = split_args ~~ args
bulwahn@33250
   230
            fun mk_prems_of_assm assm =
bulwahn@33250
   231
              let
bulwahn@33250
   232
                val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
bulwahn@33250
   233
                val var_names = Name.variant_list names (map fst vTs)
bulwahn@33250
   234
                val vars = map Free (var_names ~~ (map snd vTs))
bulwahn@33250
   235
                val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
bulwahn@33250
   236
                val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
bulwahn@33250
   237
              in
bulwahn@33250
   238
                mk_prems' inner_t (var_names @ names, prems' @ prems)
bulwahn@33250
   239
              end
bulwahn@33250
   240
          in
bulwahn@33250
   241
            maps mk_prems_of_assm assms
bulwahn@33250
   242
          end
bulwahn@33250
   243
        else
bulwahn@33250
   244
          let
bulwahn@33250
   245
            val (f, args) = strip_comb t
bulwahn@33250
   246
            (* TODO: special procedure for higher-order functions: split arguments in
bulwahn@33250
   247
              simple types and function types *)
bulwahn@33250
   248
            val resname = Name.variant names "res"
bulwahn@33250
   249
            val resvar = Free (resname, body_type (fastype_of t))
bulwahn@33250
   250
            val names' = resname :: names
bulwahn@33250
   251
            fun mk_prems'' (t as Const (c, _)) =
bulwahn@33250
   252
              if is_constr thy c orelse (is_none (try lookup_pred t)) then
bulwahn@33250
   253
                folds_map mk_prems' args (names', prems) |>
bulwahn@33250
   254
                map
bulwahn@33250
   255
                  (fn (argvs, (names'', prems')) =>
bulwahn@33250
   256
                  let
bulwahn@33250
   257
                    val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (resvar, list_comb (f, argvs)))
bulwahn@33250
   258
                  in (names'', prem :: prems') end)
bulwahn@33250
   259
              else
bulwahn@33250
   260
                let
bulwahn@33250
   261
                  val pred = lookup_pred t
bulwahn@33250
   262
                  val nparams = get_nparams pred
bulwahn@33250
   263
                  val (params, args) = chop nparams args
bulwahn@33250
   264
                  val params' = map (mk_param thy lookup_pred) params
bulwahn@33250
   265
                in
bulwahn@33250
   266
                  folds_map mk_prems' args (names', prems)
bulwahn@33250
   267
                  |> map (fn (argvs, (names'', prems')) =>
bulwahn@33250
   268
                    let
bulwahn@33250
   269
                      val prem = HOLogic.mk_Trueprop (list_comb (pred, params' @ argvs @ [resvar]))
bulwahn@33250
   270
                    in (names'', prem :: prems') end)
bulwahn@33250
   271
                end
bulwahn@33250
   272
            | mk_prems'' (t as Free (_, _)) =
bulwahn@33250
   273
                let
bulwahn@33250
   274
                  (* higher order argument call *)
bulwahn@33250
   275
                  val pred = lookup_pred t
bulwahn@33250
   276
                in
bulwahn@33250
   277
                  folds_map mk_prems' args (resname :: names, prems)
bulwahn@33250
   278
                  |> map (fn (argvs, (names', prems')) =>
bulwahn@33250
   279
                     let
bulwahn@33250
   280
                       val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar]))
bulwahn@33250
   281
                     in (names', prem :: prems') end)
bulwahn@33250
   282
                end
bulwahn@33250
   283
            | mk_prems'' t =
bulwahn@33250
   284
              error ("Invalid term: " ^ Syntax.string_of_term_global thy t)
bulwahn@33250
   285
          in
bulwahn@33250
   286
            map (pair resvar) (mk_prems'' f)
bulwahn@33250
   287
          end
bulwahn@33250
   288
  in
bulwahn@33250
   289
    mk_prems' t (names, prems)
bulwahn@33250
   290
  end;
bulwahn@33250
   291
bulwahn@33250
   292
(* assumption: mutual recursive predicates all have the same parameters. *)  
bulwahn@33250
   293
fun define_predicates specs thy =
bulwahn@33250
   294
  if forall (fn (const, _) => member (op =) (Symtab.keys (Pred_Compile_Preproc.get thy)) const) specs then
bulwahn@33250
   295
    ([], thy)
bulwahn@33250
   296
  else
bulwahn@33250
   297
  let
bulwahn@33250
   298
    val consts = map fst specs
bulwahn@33250
   299
    val eqns = maps snd specs
bulwahn@33250
   300
    (*val eqns = maps (Predicate_Compile_Preproc_Data.get_specification thy) consts*)
bulwahn@33250
   301
      (* create prednames *)
bulwahn@33250
   302
    val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
bulwahn@33250
   303
    val argss' = map (map transform_ho_arg) argss
bulwahn@33250
   304
    val pnames = map dest_Free (distinct (op =) (maps (filter (is_funtype o fastype_of)) argss'))
bulwahn@33250
   305
    val preds = map pred_of funs
bulwahn@33250
   306
    val prednames = map (fst o dest_Free) preds
bulwahn@33250
   307
    val funnames = map (fst o dest_Const) funs
bulwahn@33250
   308
    val fun_pred_names = (funnames ~~ prednames)  
bulwahn@33250
   309
      (* mapping from term (Free or Const) to term *)
bulwahn@33250
   310
    fun lookup_pred (Const (name, T)) =
bulwahn@33250
   311
      (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
bulwahn@33250
   312
          SOME c => Const (c, pred_type T)
bulwahn@33250
   313
        | NONE =>
bulwahn@33250
   314
          (case AList.lookup op = fun_pred_names name of
bulwahn@33250
   315
            SOME f => Free (f, pred_type T)
bulwahn@33250
   316
          | NONE => Const (name, T)))
bulwahn@33250
   317
      | lookup_pred (Free (name, T)) =
bulwahn@33250
   318
        if member op = (map fst pnames) name then
bulwahn@33250
   319
          Free (name, transform_ho_typ T)
bulwahn@33250
   320
        else
bulwahn@33250
   321
          Free (name, T)
bulwahn@33250
   322
      | lookup_pred t =
bulwahn@33250
   323
         error ("lookup function is not defined for " ^ Syntax.string_of_term_global thy t)
bulwahn@33250
   324
     
bulwahn@33250
   325
        (* mapping from term (predicate term, not function term!) to int *)
bulwahn@33250
   326
    fun get_nparams (Const (name, _)) =
bulwahn@33250
   327
      the_default 0 (try (ind_package_get_nparams thy) name)
bulwahn@33250
   328
    | get_nparams (Free (name, _)) =
bulwahn@33250
   329
        (if member op = prednames name then
bulwahn@33250
   330
          length pnames
bulwahn@33250
   331
        else 0)
bulwahn@33250
   332
    | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
bulwahn@33250
   333
  
bulwahn@33250
   334
    (* create intro rules *)
bulwahn@33250
   335
  
bulwahn@33250
   336
    fun mk_intros ((func, pred), (args, rhs)) =
bulwahn@33250
   337
      if (body_type (fastype_of func) = @{typ bool}) then
bulwahn@33250
   338
       (*TODO: preprocess predicate definition of rhs *)
bulwahn@33250
   339
        [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
bulwahn@33250
   340
      else
bulwahn@33250
   341
        let
bulwahn@33250
   342
          val names = Term.add_free_names rhs []
bulwahn@33250
   343
        in mk_prems thy (lookup_pred, get_nparams) rhs (names, [])
bulwahn@33250
   344
          |> map (fn (resultt, (names', prems)) =>
bulwahn@33250
   345
            Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
bulwahn@33250
   346
        end
bulwahn@33250
   347
    fun mk_rewr_thm (func, pred) = @{thm refl}
bulwahn@33250
   348
  in
bulwahn@33250
   349
    case try (maps mk_intros) ((funs ~~ preds) ~~ (argss' ~~ rhss)) of
bulwahn@33250
   350
      NONE => ([], thy) 
bulwahn@33250
   351
    | SOME intr_ts =>
bulwahn@33250
   352
        if is_some (try (map (cterm_of thy)) intr_ts) then
bulwahn@33250
   353
          let
bulwahn@33250
   354
            val (ind_result, thy') =
wenzelm@33278
   355
              thy
wenzelm@33278
   356
              |> Sign.map_naming Name_Space.conceal
wenzelm@33278
   357
              |> Inductive.add_inductive_global (serial ())
wenzelm@33669
   358
                {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
wenzelm@33669
   359
                  no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
wenzelm@33278
   360
                (map (fn (s, T) =>
wenzelm@33278
   361
                  ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
bulwahn@33250
   362
                pnames
bulwahn@33250
   363
                (map (fn x => (Attrib.empty_binding, x)) intr_ts)
wenzelm@33278
   364
                []
wenzelm@33278
   365
              ||> Sign.restore_naming thy
bulwahn@33250
   366
            val prednames = map (fst o dest_Const) (#preds ind_result)
bulwahn@33250
   367
            (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
bulwahn@33250
   368
            (* add constants to my table *)
bulwahn@33250
   369
            val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames
bulwahn@33250
   370
            val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy'
bulwahn@33250
   371
          in
bulwahn@33250
   372
            (specs, thy'')
bulwahn@33250
   373
          end
bulwahn@33250
   374
        else
bulwahn@33250
   375
          let
bulwahn@33250
   376
            val _ = tracing "Introduction rules of function_predicate are not welltyped"
bulwahn@33250
   377
          in ([], thy) end
bulwahn@33250
   378
  end
bulwahn@33250
   379
bulwahn@33250
   380
fun rewrite_intro thy intro =
bulwahn@33250
   381
  let
bulwahn@33250
   382
    fun lookup_pred (Const (name, T)) =
bulwahn@33250
   383
      (case (Symtab.lookup (Pred_Compile_Preproc.get thy) name) of
bulwahn@33250
   384
        SOME c => Const (c, pred_type T)
bulwahn@33250
   385
      | NONE => error ("Function " ^ name ^ " is not inductified"))
bulwahn@33250
   386
    | lookup_pred (Free (name, T)) = Free (name, T)
bulwahn@33250
   387
    | lookup_pred _ = error "lookup function is not defined!"
bulwahn@33250
   388
bulwahn@33250
   389
    fun get_nparams (Const (name, _)) =
bulwahn@33250
   390
      the_default 0 (try (ind_package_get_nparams thy) name)
bulwahn@33250
   391
    | get_nparams (Free _) = 0
bulwahn@33250
   392
    | get_nparams t = error ("No parameters for " ^ (Syntax.string_of_term_global thy t))
bulwahn@33250
   393
    
bulwahn@33250
   394
    val intro_t = (Logic.unvarify o prop_of) intro
bulwahn@33250
   395
    val (prems, concl) = Logic.strip_horn intro_t
bulwahn@33250
   396
    val frees = map fst (Term.add_frees intro_t [])
bulwahn@33250
   397
    fun rewrite prem names =
bulwahn@33250
   398
      let
bulwahn@33250
   399
        val t = (HOLogic.dest_Trueprop prem)
bulwahn@33250
   400
        val (lit, mk_lit) = case try HOLogic.dest_not t of
bulwahn@33250
   401
            SOME t => (t, HOLogic.mk_not)
bulwahn@33250
   402
          | NONE => (t, I)
bulwahn@33250
   403
        val (P, args) = (strip_comb lit) 
bulwahn@33250
   404
      in
bulwahn@33250
   405
        folds_map (
bulwahn@33250
   406
          fn t => if (is_funtype (fastype_of t)) then (fn x => [(t, x)])
bulwahn@33250
   407
            else mk_prems thy (lookup_pred, get_nparams) t) args (names, [])
bulwahn@33250
   408
        |> map (fn (resargs, (names', prems')) =>
bulwahn@33250
   409
          let
bulwahn@33250
   410
            val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
bulwahn@33250
   411
          in (prem'::prems', names') end)
bulwahn@33250
   412
      end
bulwahn@33250
   413
    val intro_ts' = folds_map rewrite prems frees
bulwahn@33250
   414
      |> maps (fn (prems', frees') =>
bulwahn@33250
   415
        rewrite concl frees'
bulwahn@33250
   416
        |> map (fn (concl'::conclprems, _) =>
bulwahn@33250
   417
          Logic.list_implies ((flat prems') @ conclprems, concl')))
bulwahn@33250
   418
  in
bulwahn@33630
   419
    map (Drule.standard o (Skip_Proof.make_thm thy)) intro_ts'
bulwahn@33630
   420
  end
bulwahn@33250
   421
bulwahn@33250
   422
end;