src/HOL/Tools/Predicate_Compile/core_data.ML
author bulwahn
Thu Oct 21 19:13:10 2010 +0200 (2010-10-21)
changeset 40053 3fa49ea76cbb
parent 40052 ea46574ca815
child 40101 f7fc517e21c6
permissions -rw-r--r--
using a signature in core_data and moving some more functions to core_data
bulwahn@40053
     1
(*  Title:      HOL/Tools/Predicate_Compile/core_data.ML
bulwahn@40053
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@40052
     3
bulwahn@40053
     4
Data of the predicate compiler core
bulwahn@40053
     5
bulwahn@40053
     6
*)
bulwahn@40053
     7
signature CORE_DATA =
bulwahn@40053
     8
sig
bulwahn@40053
     9
  type mode = Predicate_Compile_Aux.mode
bulwahn@40053
    10
  type compilation = Predicate_Compile_Aux.compilation
bulwahn@40053
    11
  type compilation_funs = Predicate_Compile_Aux.compilation_funs
bulwahn@40053
    12
  
bulwahn@40053
    13
  datatype predfun_data = PredfunData of {
bulwahn@40053
    14
    definition : thm,
bulwahn@40053
    15
    intro : thm,
bulwahn@40053
    16
    elim : thm,
bulwahn@40053
    17
    neg_intro : thm option
bulwahn@40053
    18
  };
bulwahn@40053
    19
bulwahn@40053
    20
  datatype pred_data = PredData of {
bulwahn@40053
    21
    intros : (string option * thm) list,
bulwahn@40053
    22
    elim : thm option,
bulwahn@40053
    23
    preprocessed : bool,
bulwahn@40053
    24
    function_names : (compilation * (mode * string) list) list,
bulwahn@40053
    25
    predfun_data : (mode * predfun_data) list,
bulwahn@40053
    26
    needs_random : mode list
bulwahn@40053
    27
  };
bulwahn@40053
    28
bulwahn@40053
    29
  (* general operations *)
bulwahn@40053
    30
  val unify_consts : theory -> term list -> term list -> (term list * term list)
bulwahn@40053
    31
  val mk_casesrule : Proof.context -> term -> thm list -> term
bulwahn@40053
    32
  val preprocess_intro : theory -> thm -> thm
bulwahn@40053
    33
bulwahn@40053
    34
  structure PredData : THEORY_DATA
bulwahn@40053
    35
  
bulwahn@40053
    36
  (* queries *)
bulwahn@40053
    37
  val defined_functions : compilation -> Proof.context -> string -> bool
bulwahn@40053
    38
  val is_registered : Proof.context -> string -> bool
bulwahn@40053
    39
  val function_name_of : compilation -> Proof.context -> string -> mode -> string
bulwahn@40053
    40
  val the_elim_of : Proof.context -> string -> thm
bulwahn@40053
    41
  val has_elim : Proof.context -> string -> bool
bulwahn@40053
    42
  
bulwahn@40053
    43
  val needs_random : Proof.context -> string -> mode -> bool
bulwahn@40053
    44
  
bulwahn@40053
    45
  val predfun_intro_of : Proof.context -> string -> mode -> thm
bulwahn@40053
    46
  val predfun_neg_intro_of : Proof.context -> string -> mode -> thm option
bulwahn@40053
    47
  val predfun_elim_of : Proof.context -> string -> mode -> thm
bulwahn@40053
    48
  val predfun_definition_of : Proof.context -> string -> mode -> thm
bulwahn@40053
    49
  
bulwahn@40053
    50
  val all_preds_of : Proof.context -> string list
bulwahn@40053
    51
  val modes_of: compilation -> Proof.context -> string -> mode list
bulwahn@40053
    52
  val all_modes_of : compilation -> Proof.context -> (string * mode list) list
bulwahn@40053
    53
  val all_random_modes_of : Proof.context -> (string * mode list) list
bulwahn@40053
    54
  val intros_of : Proof.context -> string -> thm list
bulwahn@40053
    55
  val names_of : Proof.context -> string -> string option list
bulwahn@40053
    56
bulwahn@40053
    57
  val intros_graph_of : Proof.context -> thm list Graph.T
bulwahn@40053
    58
  
bulwahn@40053
    59
  (* updaters *)
bulwahn@40053
    60
  
bulwahn@40053
    61
  val register_predicate : (string * thm list * thm) -> theory -> theory
bulwahn@40053
    62
  val register_intros : string * thm list -> theory -> theory
bulwahn@40053
    63
bulwahn@40053
    64
  (* FIXME: naming of function is strange *)
bulwahn@40053
    65
  val defined_function_of : compilation -> string -> theory -> theory
bulwahn@40053
    66
  val add_intro : string option * thm -> theory -> theory
bulwahn@40053
    67
  val set_elim : thm -> theory -> theory
bulwahn@40053
    68
  val set_function_name : compilation -> string -> mode -> string -> theory -> theory
bulwahn@40053
    69
  val add_predfun_data : string -> mode -> thm * ((thm * thm) * thm option) -> theory -> theory
bulwahn@40053
    70
  val set_needs_random : string -> mode list -> theory -> theory
bulwahn@40053
    71
  (* sophisticated updaters *)
bulwahn@40053
    72
  val extend_intro_graph : string list -> theory -> theory
bulwahn@40053
    73
  val preprocess_intros : string -> theory -> theory
bulwahn@40053
    74
  
bulwahn@40053
    75
  (* alternative function definitions *)
bulwahn@40053
    76
  val register_alternative_function : string -> mode -> string -> theory -> theory
bulwahn@40053
    77
  val alternative_compilation_of_global : theory -> string -> mode ->
bulwahn@40053
    78
    (compilation_funs -> typ -> term) option
bulwahn@40053
    79
  val alternative_compilation_of : Proof.context -> string -> mode ->
bulwahn@40053
    80
    (compilation_funs -> typ -> term) option
bulwahn@40053
    81
  val functional_compilation : string -> mode -> compilation_funs -> typ -> term
bulwahn@40053
    82
  val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory
bulwahn@40053
    83
  val force_modes_and_compilations : string ->
bulwahn@40053
    84
    (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
bulwahn@40053
    85
bulwahn@40053
    86
end;
bulwahn@40053
    87
bulwahn@40053
    88
structure Core_Data : CORE_DATA =
bulwahn@40052
    89
struct
bulwahn@40052
    90
bulwahn@40052
    91
open Predicate_Compile_Aux;
bulwahn@40052
    92
bulwahn@40053
    93
(* FIXME: should be moved to Predicate_Compile_Aux *)
bulwahn@40053
    94
val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
bulwahn@40053
    95
bulwahn@40053
    96
bulwahn@40052
    97
(* book-keeping *)
bulwahn@40052
    98
bulwahn@40052
    99
datatype predfun_data = PredfunData of {
bulwahn@40052
   100
  definition : thm,
bulwahn@40052
   101
  intro : thm,
bulwahn@40052
   102
  elim : thm,
bulwahn@40052
   103
  neg_intro : thm option
bulwahn@40052
   104
};
bulwahn@40052
   105
bulwahn@40052
   106
fun rep_predfun_data (PredfunData data) = data;
bulwahn@40052
   107
bulwahn@40052
   108
fun mk_predfun_data (definition, ((intro, elim), neg_intro)) =
bulwahn@40052
   109
  PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
bulwahn@40052
   110
bulwahn@40052
   111
datatype pred_data = PredData of {
bulwahn@40052
   112
  intros : (string option * thm) list,
bulwahn@40052
   113
  elim : thm option,
bulwahn@40052
   114
  preprocessed : bool,
bulwahn@40052
   115
  function_names : (compilation * (mode * string) list) list,
bulwahn@40052
   116
  predfun_data : (mode * predfun_data) list,
bulwahn@40052
   117
  needs_random : mode list
bulwahn@40052
   118
};
bulwahn@40052
   119
bulwahn@40052
   120
fun rep_pred_data (PredData data) = data;
bulwahn@40052
   121
bulwahn@40052
   122
fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
bulwahn@40052
   123
  PredData {intros = intros, elim = elim, preprocessed = preprocessed,
bulwahn@40052
   124
    function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
bulwahn@40052
   125
bulwahn@40052
   126
fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
bulwahn@40052
   127
  mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
bulwahn@40052
   128
bulwahn@40052
   129
fun eq_option eq (NONE, NONE) = true
bulwahn@40052
   130
  | eq_option eq (SOME x, SOME y) = eq (x, y)
bulwahn@40052
   131
  | eq_option eq _ = false
bulwahn@40052
   132
bulwahn@40052
   133
fun eq_pred_data (PredData d1, PredData d2) = 
bulwahn@40052
   134
  eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso
bulwahn@40052
   135
  eq_option Thm.eq_thm (#elim d1, #elim d2)
bulwahn@40052
   136
bulwahn@40052
   137
structure PredData = Theory_Data
bulwahn@40052
   138
(
bulwahn@40052
   139
  type T = pred_data Graph.T;
bulwahn@40052
   140
  val empty = Graph.empty;
bulwahn@40052
   141
  val extend = I;
bulwahn@40052
   142
  val merge = Graph.merge eq_pred_data;
bulwahn@40052
   143
);
bulwahn@40052
   144
bulwahn@40052
   145
(* queries *)
bulwahn@40052
   146
bulwahn@40052
   147
fun lookup_pred_data ctxt name =
bulwahn@40052
   148
  Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)
bulwahn@40052
   149
bulwahn@40052
   150
fun the_pred_data ctxt name = case lookup_pred_data ctxt name
bulwahn@40052
   151
 of NONE => error ("No such predicate " ^ quote name)  
bulwahn@40052
   152
  | SOME data => data;
bulwahn@40052
   153
bulwahn@40052
   154
val is_registered = is_some oo lookup_pred_data
bulwahn@40052
   155
bulwahn@40052
   156
val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
bulwahn@40052
   157
bulwahn@40052
   158
val intros_of = map snd o #intros oo the_pred_data
bulwahn@40052
   159
bulwahn@40052
   160
val names_of = map fst o #intros oo the_pred_data
bulwahn@40052
   161
bulwahn@40052
   162
fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
bulwahn@40052
   163
 of NONE => error ("No elimination rule for predicate " ^ quote name)
bulwahn@40052
   164
  | SOME thm => thm
bulwahn@40052
   165
  
bulwahn@40052
   166
val has_elim = is_some o #elim oo the_pred_data
bulwahn@40052
   167
bulwahn@40052
   168
fun function_names_of compilation ctxt name =
bulwahn@40052
   169
  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
bulwahn@40052
   170
    NONE => error ("No " ^ string_of_compilation compilation
bulwahn@40052
   171
      ^ " functions defined for predicate " ^ quote name)
bulwahn@40052
   172
  | SOME fun_names => fun_names
bulwahn@40052
   173
bulwahn@40052
   174
fun function_name_of compilation ctxt name mode =
bulwahn@40052
   175
  case AList.lookup eq_mode
bulwahn@40052
   176
    (function_names_of compilation ctxt name) mode of
bulwahn@40052
   177
    NONE => error ("No " ^ string_of_compilation compilation
bulwahn@40052
   178
      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
bulwahn@40052
   179
  | SOME function_name => function_name
bulwahn@40052
   180
bulwahn@40052
   181
fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
bulwahn@40052
   182
bulwahn@40052
   183
fun all_modes_of compilation ctxt =
bulwahn@40052
   184
  map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
bulwahn@40052
   185
    (all_preds_of ctxt)
bulwahn@40052
   186
bulwahn@40052
   187
val all_random_modes_of = all_modes_of Random
bulwahn@40052
   188
bulwahn@40052
   189
fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
bulwahn@40052
   190
    NONE => false
bulwahn@40052
   191
  | SOME data => AList.defined (op =) (#function_names data) compilation
bulwahn@40052
   192
bulwahn@40052
   193
fun needs_random ctxt s m =
bulwahn@40052
   194
  member (op =) (#needs_random (the_pred_data ctxt s)) m
bulwahn@40052
   195
bulwahn@40052
   196
fun lookup_predfun_data ctxt name mode =
bulwahn@40052
   197
  Option.map rep_predfun_data
bulwahn@40052
   198
    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
bulwahn@40052
   199
bulwahn@40052
   200
fun the_predfun_data ctxt name mode =
bulwahn@40052
   201
  case lookup_predfun_data ctxt name mode of
bulwahn@40052
   202
    NONE => error ("No function defined for mode " ^ string_of_mode mode ^
bulwahn@40052
   203
      " of predicate " ^ name)
bulwahn@40052
   204
  | SOME data => data;
bulwahn@40052
   205
bulwahn@40052
   206
val predfun_definition_of = #definition ooo the_predfun_data
bulwahn@40052
   207
bulwahn@40052
   208
val predfun_intro_of = #intro ooo the_predfun_data
bulwahn@40052
   209
bulwahn@40052
   210
val predfun_elim_of = #elim ooo the_predfun_data
bulwahn@40052
   211
bulwahn@40052
   212
val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
bulwahn@40052
   213
bulwahn@40052
   214
val intros_graph_of =
bulwahn@40052
   215
  Graph.map (K (map snd o #intros o rep_pred_data)) o PredData.get o ProofContext.theory_of
bulwahn@40052
   216
bulwahn@40053
   217
(** preprocessing rules **)
bulwahn@40053
   218
bulwahn@40053
   219
fun Trueprop_conv cv ct =
bulwahn@40053
   220
  case Thm.term_of ct of
bulwahn@40053
   221
    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
bulwahn@40053
   222
  | _ => raise Fail "Trueprop_conv"
bulwahn@40053
   223
bulwahn@40053
   224
fun preprocess_equality thy rule =
bulwahn@40053
   225
  Conv.fconv_rule
bulwahn@40053
   226
    (imp_prems_conv
bulwahn@40053
   227
      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
bulwahn@40053
   228
    (Thm.transfer thy rule)
bulwahn@40053
   229
bulwahn@40053
   230
fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
bulwahn@40053
   231
bulwahn@40053
   232
(* importing introduction rules *)
bulwahn@40053
   233
bulwahn@40053
   234
fun unify_consts thy cs intr_ts =
bulwahn@40053
   235
  (let
bulwahn@40053
   236
     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
bulwahn@40053
   237
     fun varify (t, (i, ts)) =
bulwahn@40053
   238
       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
bulwahn@40053
   239
       in (maxidx_of_term t', t'::ts) end;
bulwahn@40053
   240
     val (i, cs') = List.foldr varify (~1, []) cs;
bulwahn@40053
   241
     val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
bulwahn@40053
   242
     val rec_consts = fold add_term_consts_2 cs' [];
bulwahn@40053
   243
     val intr_consts = fold add_term_consts_2 intr_ts' [];
bulwahn@40053
   244
     fun unify (cname, cT) =
bulwahn@40053
   245
       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
bulwahn@40053
   246
       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
bulwahn@40053
   247
     val (env, _) = fold unify rec_consts (Vartab.empty, i');
bulwahn@40053
   248
     val subst = map_types (Envir.norm_type env)
bulwahn@40053
   249
   in (map subst cs', map subst intr_ts')
bulwahn@40053
   250
   end) handle Type.TUNIFY =>
bulwahn@40053
   251
     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
bulwahn@40053
   252
bulwahn@40053
   253
fun import_intros inp_pred [] ctxt =
bulwahn@40053
   254
  let
bulwahn@40053
   255
    val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
bulwahn@40053
   256
    val T = fastype_of outp_pred
bulwahn@40053
   257
    val paramTs = ho_argsT_of_typ (binder_types T)
bulwahn@40053
   258
    val (param_names, ctxt'') = Variable.variant_fixes
bulwahn@40053
   259
      (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
bulwahn@40053
   260
    val params = map2 (curry Free) param_names paramTs
bulwahn@40053
   261
  in
bulwahn@40053
   262
    (((outp_pred, params), []), ctxt')
bulwahn@40053
   263
  end
bulwahn@40053
   264
  | import_intros inp_pred (th :: ths) ctxt =
bulwahn@40053
   265
    let
bulwahn@40053
   266
      val ((_, [th']), ctxt') = Variable.import true [th] ctxt
bulwahn@40053
   267
      val thy = ProofContext.theory_of ctxt'
bulwahn@40053
   268
      val (pred, args) = strip_intro_concl th'
bulwahn@40053
   269
      val T = fastype_of pred
bulwahn@40053
   270
      val ho_args = ho_args_of_typ T args
bulwahn@40053
   271
      fun subst_of (pred', pred) =
bulwahn@40053
   272
        let
bulwahn@40053
   273
          val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
bulwahn@40053
   274
            handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
bulwahn@40053
   275
            ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
bulwahn@40053
   276
            ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
bulwahn@40053
   277
            ^ " in " ^ Display.string_of_thm ctxt th)
bulwahn@40053
   278
        in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
bulwahn@40053
   279
      fun instantiate_typ th =
bulwahn@40053
   280
        let
bulwahn@40053
   281
          val (pred', _) = strip_intro_concl th
bulwahn@40053
   282
          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
bulwahn@40053
   283
            raise Fail "Trying to instantiate another predicate" else ()
bulwahn@40053
   284
        in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
bulwahn@40053
   285
      fun instantiate_ho_args th =
bulwahn@40053
   286
        let
bulwahn@40053
   287
          val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
bulwahn@40053
   288
          val ho_args' = map dest_Var (ho_args_of_typ T args')
bulwahn@40053
   289
        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
bulwahn@40053
   290
      val outp_pred =
bulwahn@40053
   291
        Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
bulwahn@40053
   292
      val ((_, ths'), ctxt1) =
bulwahn@40053
   293
        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
bulwahn@40053
   294
    in
bulwahn@40053
   295
      (((outp_pred, ho_args), th' :: ths'), ctxt1)
bulwahn@40053
   296
    end
bulwahn@40053
   297
bulwahn@40053
   298
(* generation of case rules from user-given introduction rules *)
bulwahn@40053
   299
bulwahn@40053
   300
fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
bulwahn@40053
   301
    let
bulwahn@40053
   302
      val (t1, st') = mk_args2 T1 st
bulwahn@40053
   303
      val (t2, st'') = mk_args2 T2 st'
bulwahn@40053
   304
    in
bulwahn@40053
   305
      (HOLogic.mk_prod (t1, t2), st'')
bulwahn@40053
   306
    end
bulwahn@40053
   307
  (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) = 
bulwahn@40053
   308
    let
bulwahn@40053
   309
      val (S, U) = strip_type T
bulwahn@40053
   310
    in
bulwahn@40053
   311
      if U = HOLogic.boolT then
bulwahn@40053
   312
        (hd params, (tl params, ctxt))
bulwahn@40053
   313
      else
bulwahn@40053
   314
        let
bulwahn@40053
   315
          val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
bulwahn@40053
   316
        in
bulwahn@40053
   317
          (Free (x, T), (params, ctxt'))
bulwahn@40053
   318
        end
bulwahn@40053
   319
    end*)
bulwahn@40053
   320
  | mk_args2 T (params, ctxt) =
bulwahn@40053
   321
    let
bulwahn@40053
   322
      val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
bulwahn@40053
   323
    in
bulwahn@40053
   324
      (Free (x, T), (params, ctxt'))
bulwahn@40053
   325
    end
bulwahn@40053
   326
bulwahn@40053
   327
fun mk_casesrule ctxt pred introrules =
bulwahn@40053
   328
  let
bulwahn@40053
   329
    (* TODO: can be simplified if parameters are not treated specially ? *)
bulwahn@40053
   330
    val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
bulwahn@40053
   331
    (* TODO: distinct required ? -- test case with more than one parameter! *)
bulwahn@40053
   332
    val params = distinct (op aconv) params
bulwahn@40053
   333
    val intros = map prop_of intros_th
bulwahn@40053
   334
    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
bulwahn@40053
   335
    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
bulwahn@40053
   336
    val argsT = binder_types (fastype_of pred)
bulwahn@40053
   337
    (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)
bulwahn@40053
   338
    val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
bulwahn@40053
   339
    fun mk_case intro =
bulwahn@40053
   340
      let
bulwahn@40053
   341
        val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
bulwahn@40053
   342
        val prems = Logic.strip_imp_prems intro
bulwahn@40053
   343
        val eqprems =
bulwahn@40053
   344
          map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
bulwahn@40053
   345
        val frees = map Free (fold Term.add_frees (args @ prems) [])
bulwahn@40053
   346
      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
bulwahn@40053
   347
    val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
bulwahn@40053
   348
    val cases = map mk_case intros
bulwahn@40053
   349
  in Logic.list_implies (assm :: cases, prop) end;
bulwahn@40053
   350
bulwahn@40053
   351
fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =
bulwahn@40053
   352
  let
bulwahn@40053
   353
    val thy = ProofContext.theory_of ctxt
bulwahn@40053
   354
    val nargs = length (binder_types (fastype_of pred))
bulwahn@40053
   355
    fun PEEK f dependent_tactic st = dependent_tactic (f st) st
bulwahn@40053
   356
    fun meta_eq_of th = th RS @{thm eq_reflection}
bulwahn@40053
   357
    val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
bulwahn@40053
   358
    fun instantiate i n {context = ctxt, params = p, prems = prems,
bulwahn@40053
   359
      asms = a, concl = cl, schematics = s}  =
bulwahn@40053
   360
      let
bulwahn@40053
   361
        fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
bulwahn@40053
   362
        fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
bulwahn@40053
   363
          |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
bulwahn@40053
   364
        val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
bulwahn@40053
   365
        val case_th = MetaSimplifier.simplify true
bulwahn@40053
   366
          (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
bulwahn@40053
   367
        val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
bulwahn@40053
   368
        val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
bulwahn@40053
   369
        val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
bulwahn@40053
   370
          OF (replicate nargs @{thm refl})
bulwahn@40053
   371
        val thesis =
bulwahn@40053
   372
          Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'
bulwahn@40053
   373
            OF prems'
bulwahn@40053
   374
      in
bulwahn@40053
   375
        (rtac thesis 1)
bulwahn@40053
   376
      end
bulwahn@40053
   377
    val tac =
bulwahn@40053
   378
      etac pre_cases_rule 1
bulwahn@40053
   379
      THEN
bulwahn@40053
   380
      (PEEK nprems_of
bulwahn@40053
   381
        (fn n =>
bulwahn@40053
   382
          ALLGOALS (fn i =>
bulwahn@40053
   383
            MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i
bulwahn@40053
   384
            THEN (SUBPROOF (instantiate i n) ctxt i))))
bulwahn@40053
   385
  in
bulwahn@40053
   386
    Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
bulwahn@40053
   387
  end
bulwahn@40053
   388
bulwahn@40053
   389
(* updaters *)
bulwahn@40053
   390
bulwahn@40053
   391
(* fetching introduction rules or registering introduction rules *)
bulwahn@40053
   392
bulwahn@40053
   393
val no_compilation = ([], ([], []))
bulwahn@40053
   394
bulwahn@40053
   395
fun fetch_pred_data ctxt name =
bulwahn@40053
   396
  case try (Inductive.the_inductive ctxt) name of
bulwahn@40053
   397
    SOME (info as (_, result)) => 
bulwahn@40053
   398
      let
bulwahn@40053
   399
        fun is_intro_of intro =
bulwahn@40053
   400
          let
bulwahn@40053
   401
            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
bulwahn@40053
   402
          in (fst (dest_Const const) = name) end;
bulwahn@40053
   403
        val thy = ProofContext.theory_of ctxt
bulwahn@40053
   404
        val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
bulwahn@40053
   405
        val index = find_index (fn s => s = name) (#names (fst info))
bulwahn@40053
   406
        val pre_elim = nth (#elims result) index
bulwahn@40053
   407
        val pred = nth (#preds result) index
bulwahn@40053
   408
        val elim_t = mk_casesrule ctxt pred intros
bulwahn@40053
   409
        val nparams = length (Inductive.params_of (#raw_induct result))
bulwahn@40053
   410
        val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
bulwahn@40053
   411
      in
bulwahn@40053
   412
        mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
bulwahn@40053
   413
      end
bulwahn@40053
   414
  | NONE => error ("No such predicate: " ^ quote name)
bulwahn@40053
   415
bulwahn@40053
   416
fun add_predfun_data name mode data =
bulwahn@40053
   417
  let
bulwahn@40053
   418
    val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
bulwahn@40053
   419
  in PredData.map (Graph.map_node name (map_pred_data add)) end
bulwahn@40053
   420
bulwahn@40053
   421
fun is_inductive_predicate ctxt name =
bulwahn@40053
   422
  is_some (try (Inductive.the_inductive ctxt) name)
bulwahn@40053
   423
bulwahn@40053
   424
fun depending_preds_of ctxt (key, value) =
bulwahn@40053
   425
  let
bulwahn@40053
   426
    val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value)
bulwahn@40053
   427
  in
bulwahn@40053
   428
    fold Term.add_const_names intros []
bulwahn@40053
   429
      |> (fn cs =>
bulwahn@40053
   430
        if member (op =) cs @{const_name "HOL.eq"} then
bulwahn@40053
   431
          insert (op =) @{const_name Predicate.eq} cs
bulwahn@40053
   432
        else cs)
bulwahn@40053
   433
      |> filter (fn c => (not (c = key)) andalso
bulwahn@40053
   434
        (is_inductive_predicate ctxt c orelse is_registered ctxt c))
bulwahn@40053
   435
  end;
bulwahn@40053
   436
bulwahn@40053
   437
fun add_intro (opt_case_name, thm) thy =
bulwahn@40053
   438
  let
bulwahn@40053
   439
    val (name, T) = dest_Const (fst (strip_intro_concl thm))
bulwahn@40053
   440
    fun cons_intro gr =
bulwahn@40053
   441
     case try (Graph.get_node gr) name of
bulwahn@40053
   442
       SOME pred_data => Graph.map_node name (map_pred_data
bulwahn@40053
   443
         (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
bulwahn@40053
   444
     | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
bulwahn@40053
   445
  in PredData.map cons_intro thy end
bulwahn@40053
   446
bulwahn@40053
   447
fun set_elim thm =
bulwahn@40053
   448
  let
bulwahn@40053
   449
    val (name, _) = dest_Const (fst 
bulwahn@40053
   450
      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
bulwahn@40053
   451
  in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
bulwahn@40053
   452
bulwahn@40053
   453
fun register_predicate (constname, intros, elim) thy =
bulwahn@40053
   454
  let
bulwahn@40053
   455
    val named_intros = map (pair NONE) intros
bulwahn@40053
   456
  in
bulwahn@40053
   457
    if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
bulwahn@40053
   458
      PredData.map
bulwahn@40053
   459
        (Graph.new_node (constname,
bulwahn@40053
   460
          mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
bulwahn@40053
   461
    else thy
bulwahn@40053
   462
  end
bulwahn@40053
   463
bulwahn@40053
   464
fun register_intros (constname, pre_intros) thy =
bulwahn@40053
   465
  let
bulwahn@40053
   466
    val T = Sign.the_const_type thy constname
bulwahn@40053
   467
    fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))
bulwahn@40053
   468
    val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then
bulwahn@40053
   469
      error ("register_intros: Introduction rules of different constants are used\n" ^
bulwahn@40053
   470
        "expected rules for " ^ constname ^ ", but received rules for " ^
bulwahn@40053
   471
          commas (map constname_of_intro pre_intros))
bulwahn@40053
   472
      else ()
bulwahn@40053
   473
    val pred = Const (constname, T)
bulwahn@40053
   474
    val pre_elim = 
bulwahn@40053
   475
      (Drule.export_without_context o Skip_Proof.make_thm thy)
bulwahn@40053
   476
      (mk_casesrule (ProofContext.init_global thy) pred pre_intros)
bulwahn@40053
   477
  in register_predicate (constname, pre_intros, pre_elim) thy end
bulwahn@40053
   478
bulwahn@40053
   479
fun defined_function_of compilation pred =
bulwahn@40053
   480
  let
bulwahn@40053
   481
    val set = (apsnd o apfst) (cons (compilation, []))
bulwahn@40053
   482
  in
bulwahn@40053
   483
    PredData.map (Graph.map_node pred (map_pred_data set))
bulwahn@40053
   484
  end
bulwahn@40053
   485
bulwahn@40053
   486
fun set_function_name compilation pred mode name =
bulwahn@40053
   487
  let
bulwahn@40053
   488
    val set = (apsnd o apfst)
bulwahn@40053
   489
      (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
bulwahn@40053
   490
  in
bulwahn@40053
   491
    PredData.map (Graph.map_node pred (map_pred_data set))
bulwahn@40053
   492
  end
bulwahn@40053
   493
bulwahn@40053
   494
fun set_needs_random name modes =
bulwahn@40053
   495
  let
bulwahn@40053
   496
    val set = (apsnd o apsnd o apsnd) (K modes)
bulwahn@40053
   497
  in
bulwahn@40053
   498
    PredData.map (Graph.map_node name (map_pred_data set))
bulwahn@40053
   499
  end  
bulwahn@40053
   500
bulwahn@40053
   501
fun extend' value_of edges_of key (G, visited) =
bulwahn@40053
   502
  let
bulwahn@40053
   503
    val (G', v) = case try (Graph.get_node G) key of
bulwahn@40053
   504
        SOME v => (G, v)
bulwahn@40053
   505
      | NONE => (Graph.new_node (key, value_of key) G, value_of key)
bulwahn@40053
   506
    val (G'', visited') = fold (extend' value_of edges_of)
bulwahn@40053
   507
      (subtract (op =) visited (edges_of (key, v)))
bulwahn@40053
   508
      (G', key :: visited)
bulwahn@40053
   509
  in
bulwahn@40053
   510
    (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
bulwahn@40053
   511
  end;
bulwahn@40053
   512
bulwahn@40053
   513
fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) 
bulwahn@40053
   514
bulwahn@40053
   515
fun extend_intro_graph names thy =
bulwahn@40053
   516
  let
bulwahn@40053
   517
    val ctxt = ProofContext.init_global thy
bulwahn@40053
   518
  in
bulwahn@40053
   519
    PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names) thy
bulwahn@40053
   520
  end
bulwahn@40053
   521
bulwahn@40053
   522
fun preprocess_intros name thy =
bulwahn@40053
   523
  PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
bulwahn@40053
   524
    if preprocessed then (rules, preprocessed)
bulwahn@40053
   525
    else
bulwahn@40053
   526
      let
bulwahn@40053
   527
        val (named_intros, SOME elim) = rules
bulwahn@40053
   528
        val named_intros' = map (apsnd (preprocess_intro thy)) named_intros
bulwahn@40053
   529
        val pred = Const (name, Sign.the_const_type thy name)
bulwahn@40053
   530
        val ctxt = ProofContext.init_global thy
bulwahn@40053
   531
        val elim_t = mk_casesrule ctxt pred (map snd named_intros')
bulwahn@40053
   532
        val nparams = (case try (Inductive.the_inductive ctxt) name of
bulwahn@40053
   533
            SOME (_, result) => length (Inductive.params_of (#raw_induct result))
bulwahn@40053
   534
          | NONE => 0)
bulwahn@40053
   535
        val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
bulwahn@40053
   536
      in
bulwahn@40053
   537
        ((named_intros', SOME elim'), true)
bulwahn@40053
   538
      end))))
bulwahn@40053
   539
    thy  
bulwahn@40053
   540
bulwahn@40052
   541
(* registration of alternative function names *)
bulwahn@40052
   542
bulwahn@40052
   543
structure Alt_Compilations_Data = Theory_Data
bulwahn@40052
   544
(
bulwahn@40052
   545
  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
bulwahn@40052
   546
  val empty = Symtab.empty;
bulwahn@40052
   547
  val extend = I;
bulwahn@40052
   548
  fun merge data : T = Symtab.merge (K true) data;
bulwahn@40052
   549
);
bulwahn@40052
   550
bulwahn@40052
   551
fun alternative_compilation_of_global thy pred_name mode =
bulwahn@40052
   552
  AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
bulwahn@40052
   553
bulwahn@40052
   554
fun alternative_compilation_of ctxt pred_name mode =
bulwahn@40052
   555
  AList.lookup eq_mode
bulwahn@40052
   556
    (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode
bulwahn@40052
   557
bulwahn@40052
   558
fun force_modes_and_compilations pred_name compilations =
bulwahn@40052
   559
  let
bulwahn@40052
   560
    (* thm refl is a dummy thm *)
bulwahn@40052
   561
    val modes = map fst compilations
bulwahn@40052
   562
    val (needs_random, non_random_modes) = pairself (map fst)
bulwahn@40052
   563
      (List.partition (fn (m, (fun_name, random)) => random) compilations)
bulwahn@40052
   564
    val non_random_dummys = map (rpair "dummy") non_random_modes
bulwahn@40052
   565
    val all_dummys = map (rpair "dummy") modes
bulwahn@40052
   566
    val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
bulwahn@40052
   567
      @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
bulwahn@40052
   568
    val alt_compilations = map (apsnd fst) compilations
bulwahn@40052
   569
  in
bulwahn@40052
   570
    PredData.map (Graph.new_node
bulwahn@40052
   571
      (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
bulwahn@40052
   572
    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
bulwahn@40052
   573
  end
bulwahn@40052
   574
bulwahn@40052
   575
fun functional_compilation fun_name mode compfuns T =
bulwahn@40052
   576
  let
bulwahn@40052
   577
    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
bulwahn@40052
   578
      mode (binder_types T)
bulwahn@40052
   579
    val bs = map (pair "x") inpTs
bulwahn@40052
   580
    val bounds = map Bound (rev (0 upto (length bs) - 1))
bulwahn@40052
   581
    val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
bulwahn@40052
   582
  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
bulwahn@40052
   583
bulwahn@40052
   584
fun register_alternative_function pred_name mode fun_name =
bulwahn@40052
   585
  Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
bulwahn@40052
   586
    (pred_name, (mode, functional_compilation fun_name mode)))
bulwahn@40052
   587
bulwahn@40052
   588
fun force_modes_and_functions pred_name fun_names =
bulwahn@40052
   589
  force_modes_and_compilations pred_name
bulwahn@40052
   590
    (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
bulwahn@40052
   591
    fun_names)
bulwahn@40052
   592
bulwahn@40052
   593
end;