src/HOL/Tools/inductive_realizer.ML
author wenzelm
Sat Feb 01 18:41:48 2014 +0100 (2014-02-01)
changeset 55235 4b4627f5912b
parent 54742 7a86358a3c0b
child 55954 a29aefc88c8d
permissions -rw-r--r--
more explicit low-level exception;
berghofe@13710
     1
(*  Title:      HOL/Tools/inductive_realizer.ML
berghofe@13710
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@13710
     3
krauss@36043
     4
Program extraction from proofs involving inductive predicates:
wenzelm@29265
     5
Realizers for induction and elimination rules.
berghofe@13710
     6
*)
berghofe@13710
     7
berghofe@13710
     8
signature INDUCTIVE_REALIZER =
berghofe@13710
     9
sig
berghofe@13710
    10
  val add_ind_realizers: string -> string list -> theory -> theory
wenzelm@18708
    11
  val setup: theory -> theory
berghofe@13710
    12
end;
berghofe@13710
    13
berghofe@13710
    14
structure InductiveRealizer : INDUCTIVE_REALIZER =
berghofe@13710
    15
struct
berghofe@13710
    16
berghofe@22606
    17
fun name_of_thm thm =
wenzelm@28800
    18
  (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
wenzelm@28814
    19
      [Thm.proof_of thm] [] of
wenzelm@28800
    20
    [name] => name
wenzelm@55235
    21
  | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
berghofe@22271
    22
berghofe@13710
    23
fun prf_of thm =
wenzelm@44060
    24
  Reconstruct.proof_of thm
wenzelm@44060
    25
  |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)];  (* FIXME *)
berghofe@13710
    26
berghofe@13710
    27
fun subsets [] = [[]]
berghofe@13710
    28
  | subsets (x::xs) =
berghofe@13710
    29
      let val ys = subsets xs
berghofe@13710
    30
      in ys @ map (cons x) ys end;
berghofe@13710
    31
berghofe@22271
    32
val pred_of = fst o dest_Const o head_of;
berghofe@13710
    33
berghofe@22271
    34
fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
berghofe@22271
    35
      let val (s', names') = (case names of
wenzelm@43324
    36
          [] => (singleton (Name.variant_list used) s, [])
berghofe@22271
    37
        | name :: names' => (name, names'))
berghofe@22271
    38
      in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
berghofe@22271
    39
  | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
berghofe@22271
    40
      t $ strip_all' used names Q
berghofe@22271
    41
  | strip_all' _ _ t = t;
berghofe@22271
    42
wenzelm@29281
    43
fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
berghofe@22271
    44
berghofe@22271
    45
fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
berghofe@22271
    46
      (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
berghofe@22271
    47
  | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
berghofe@13710
    48
berghofe@37233
    49
fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
berghofe@37233
    50
     (case strip_type T of
haftmann@36692
    51
        (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
berghofe@37233
    52
      | _ => vs)) (Term.add_vars prop []) [];
berghofe@37233
    53
berghofe@37233
    54
val attach_typeS = map_types (map_atyps
berghofe@37233
    55
  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
berghofe@37233
    56
    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
berghofe@37233
    57
    | T => T));
berghofe@13710
    58
berghofe@22271
    59
fun dt_of_intrs thy vs nparms intrs =
berghofe@13710
    60
  let
berghofe@37233
    61
    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
berghofe@22271
    62
    val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
berghofe@22271
    63
      (Logic.strip_imp_concl (prop_of (hd intrs))));
haftmann@33957
    64
    val params = map dest_Var (take nparms ts);
wenzelm@30364
    65
    val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
wenzelm@30364
    66
    fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
wenzelm@35845
    67
      map (Logic.unvarifyT_global o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
berghofe@13710
    68
        filter_out (equal Extraction.nullT) (map
wenzelm@35845
    69
          (Logic.unvarifyT_global o Extraction.etype_of thy vs []) (prems_of intr)),
berghofe@13710
    70
            NoSyn);
wenzelm@45839
    71
  in
wenzelm@45839
    72
    ((tname, map (rpair dummyS) (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs), NoSyn),
wenzelm@45839
    73
      map constr_of_intr intrs)
berghofe@13710
    74
  end;
berghofe@13710
    75
berghofe@13710
    76
fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
berghofe@13710
    77
berghofe@22271
    78
(** turn "P" into "%r x. realizes r (P x)" **)
berghofe@13710
    79
berghofe@13710
    80
fun gen_rvar vs (t as Var ((a, 0), T)) =
berghofe@22271
    81
      if body_type T <> HOLogic.boolT then t else
berghofe@22271
    82
        let
berghofe@37233
    83
          val U = TVar (("'" ^ a, 0), [])
berghofe@22271
    84
          val Ts = binder_types T;
berghofe@22271
    85
          val i = length Ts;
berghofe@22271
    86
          val xs = map (pair "x") Ts;
berghofe@22271
    87
          val u = list_comb (t, map Bound (i - 1 downto 0))
berghofe@22271
    88
        in 
haftmann@36692
    89
          if member (op =) vs a then
wenzelm@46219
    90
            fold_rev Term.abs (("r", U) :: xs) (mk_rlz U $ Bound i $ u)
wenzelm@46219
    91
          else
wenzelm@46219
    92
            fold_rev Term.abs xs (mk_rlz Extraction.nullT $ Extraction.nullt $ u)
berghofe@22271
    93
        end
berghofe@13710
    94
  | gen_rvar _ t = t;
berghofe@13710
    95
berghofe@22271
    96
fun mk_realizes_eqn n vs nparms intrs =
berghofe@13710
    97
  let
berghofe@37233
    98
    val intr = map_types Type.strip_sorts (prop_of (hd intrs));
berghofe@37233
    99
    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
berghofe@37233
   100
    val iTs = rev (Term.add_tvars intr []);
berghofe@13710
   101
    val Tvs = map TVar iTs;
berghofe@22271
   102
    val (h as Const (s, T), us) = strip_comb concl;
berghofe@22271
   103
    val params = List.take (us, nparms);
berghofe@22271
   104
    val elTs = List.drop (binder_types T, nparms);
berghofe@22271
   105
    val predT = elTs ---> HOLogic.boolT;
berghofe@22271
   106
    val used = map (fst o fst o dest_Var) params;
berghofe@22271
   107
    val xs = map (Var o apfst (rpair 0))
berghofe@22271
   108
      (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
berghofe@13710
   109
    val rT = if n then Extraction.nullT
berghofe@13710
   110
      else Type (space_implode "_" (s ^ "T" :: vs),
berghofe@37233
   111
        map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
wenzelm@30364
   112
    val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
berghofe@22271
   113
    val S = list_comb (h, params @ xs);
berghofe@13710
   114
    val rvs = relevant_vars S;
haftmann@33040
   115
    val vs' = subtract (op =) vs (map fst rvs);
berghofe@13710
   116
    val rname = space_implode "_" (s ^ "R" :: vs);
berghofe@13710
   117
berghofe@13710
   118
    fun mk_Tprem n v =
haftmann@17485
   119
      let val T = (the o AList.lookup (op =) rvs) v
berghofe@13710
   120
      in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
berghofe@13710
   121
        Extraction.mk_typ (if n then Extraction.nullT
berghofe@37233
   122
          else TVar (("'" ^ v, 0), [])))
berghofe@13710
   123
      end;
berghofe@13710
   124
berghofe@13710
   125
    val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
berghofe@22271
   126
    val ts = map (gen_rvar vs) params;
berghofe@13710
   127
    val argTs = map fastype_of ts;
berghofe@13710
   128
berghofe@22271
   129
  in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S,
berghofe@13710
   130
       Extraction.mk_typ rT)),
berghofe@22271
   131
    (prems, (mk_rlz rT $ r $ S,
berghofe@22271
   132
       if n then list_comb (Const (rname, argTs ---> predT), ts @ xs)
berghofe@22271
   133
       else list_comb (Const (rname, argTs @ [rT] ---> predT), ts @ [r] @ xs))))
berghofe@13710
   134
  end;
berghofe@13710
   135
berghofe@22271
   136
fun fun_of_prem thy rsets vs params rule ivs intr =
berghofe@13710
   137
  let
wenzelm@42361
   138
    val ctxt = Proof_Context.init_global thy
berghofe@22271
   139
    val args = map (Free o apfst fst o dest_Var) ivs;
berghofe@13710
   140
    val args' = map (Free o apfst fst)
haftmann@33040
   141
      (subtract (op =) params (Term.add_vars (prop_of intr) []));
berghofe@13710
   142
    val rule' = strip_all rule;
berghofe@13710
   143
    val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
berghofe@13710
   144
    val used = map (fst o dest_Free) args;
berghofe@13710
   145
wenzelm@29271
   146
    val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
berghofe@13710
   147
berghofe@13710
   148
    fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
berghofe@13710
   149
      | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
wenzelm@35364
   150
      | is_meta (Const (@{const_name Trueprop}, _) $ t) =
wenzelm@35364
   151
          (case head_of t of
wenzelm@35364
   152
            Const (s, _) => can (Inductive.the_inductive ctxt) s
wenzelm@35364
   153
          | _ => true)
berghofe@13710
   154
      | is_meta _ = false;
berghofe@13710
   155
berghofe@13710
   156
    fun fun_of ts rts args used (prem :: prems) =
berghofe@13710
   157
          let
berghofe@13710
   158
            val T = Extraction.etype_of thy vs [] prem;
wenzelm@20071
   159
            val [x, r] = Name.variant_list used ["x", "r"]
berghofe@13710
   160
          in if T = Extraction.nullT
berghofe@13710
   161
            then fun_of ts rts args used prems
berghofe@13710
   162
            else if is_rec prem then
berghofe@13710
   163
              if is_meta prem then
berghofe@13710
   164
                let
berghofe@13710
   165
                  val prem' :: prems' = prems;
berghofe@13710
   166
                  val U = Extraction.etype_of thy vs [] prem';
wenzelm@46219
   167
                in
wenzelm@46219
   168
                  if U = Extraction.nullT
berghofe@13710
   169
                  then fun_of (Free (x, T) :: ts)
berghofe@13710
   170
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
berghofe@13710
   171
                    (Free (x, T) :: args) (x :: r :: used) prems'
berghofe@13710
   172
                  else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
berghofe@13710
   173
                    (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
berghofe@13710
   174
                end
wenzelm@46219
   175
              else
wenzelm@46219
   176
                (case strip_type T of
haftmann@37678
   177
                  (Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) =>
berghofe@13710
   178
                    let
berghofe@13710
   179
                      val fx = Free (x, Ts ---> T1);
berghofe@13710
   180
                      val fr = Free (r, Ts ---> T2);
berghofe@13710
   181
                      val bs = map Bound (length Ts - 1 downto 0);
wenzelm@46219
   182
                      val t =
wenzelm@46219
   183
                        fold_rev (Term.abs o pair "z") Ts
wenzelm@46219
   184
                          (HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)));
wenzelm@46219
   185
                    in fun_of (fx :: ts) (fr :: rts) (t::args) (x :: r :: used) prems end
berghofe@13710
   186
                | (Ts, U) => fun_of (Free (x, T) :: ts)
berghofe@13710
   187
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
berghofe@13710
   188
                    (Free (x, T) :: args) (x :: r :: used) prems)
berghofe@13710
   189
            else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args)
berghofe@13710
   190
              (x :: used) prems
berghofe@13710
   191
          end
berghofe@13710
   192
      | fun_of ts rts args used [] =
berghofe@13710
   193
          let val xs = rev (rts @ ts)
berghofe@13710
   194
          in if conclT = Extraction.nullT
wenzelm@44241
   195
            then fold_rev (absfree o dest_Free) xs HOLogic.unit
wenzelm@44241
   196
            else fold_rev (absfree o dest_Free) xs
wenzelm@44241
   197
              (list_comb
wenzelm@44241
   198
                (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
wenzelm@44241
   199
                  map fastype_of (rev args) ---> conclT), rev args))
berghofe@13710
   200
          end
berghofe@13710
   201
berghofe@13921
   202
  in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
berghofe@13710
   203
berghofe@13710
   204
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
berghofe@13710
   205
  let
berghofe@13710
   206
    val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
haftmann@31986
   207
    val premss = map_filter (fn (s, rs) => if member (op =) rsets s then
haftmann@31986
   208
      SOME (rs, map (fn (_, r) => nth (prems_of raw_induct)
haftmann@31986
   209
        (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss;
berghofe@22271
   210
    val fs = maps (fn ((intrs, prems), dummy) =>
berghofe@13710
   211
      let
berghofe@22271
   212
        val fs = map (fn (rule, (ivs, intr)) =>
berghofe@22271
   213
          fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
wenzelm@35364
   214
      in
wenzelm@35364
   215
        if dummy then Const (@{const_name default},
wenzelm@35364
   216
            HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
berghofe@22271
   217
        else fs
berghofe@22271
   218
      end) (premss ~~ dummies);
wenzelm@16861
   219
    val frees = fold Term.add_frees fs [];
berghofe@13710
   220
    val Ts = map fastype_of fs;
wenzelm@30364
   221
    fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr)
berghofe@22271
   222
  in
berghofe@22271
   223
    fst (fold_map (fn concl => fn names =>
berghofe@13710
   224
      let val T = Extraction.etype_of thy vs [] concl
berghofe@22271
   225
      in if T = Extraction.nullT then (Extraction.nullt, names) else
berghofe@22271
   226
        let
berghofe@22271
   227
          val Type ("fun", [U, _]) = T;
berghofe@22271
   228
          val a :: names' = names
wenzelm@44241
   229
        in
wenzelm@44241
   230
          (fold_rev absfree (("x", U) :: map_filter (fn intr =>
wenzelm@44241
   231
            Option.map (pair (name_of_fn intr))
wenzelm@44241
   232
              (AList.lookup (op =) frees (name_of_fn intr))) intrs)
wenzelm@44241
   233
            (list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
berghofe@22271
   234
        end
berghofe@22271
   235
      end) concls rec_names)
berghofe@13710
   236
  end;
berghofe@13710
   237
wenzelm@45839
   238
fun add_dummy name dname (x as (_, ((s, vs, mx), cs))) =
wenzelm@45839
   239
  if Binding.eq_name (name, s)
wenzelm@45839
   240
  then (true, ((s, vs, mx), (dname, [HOLogic.unitT], NoSyn) :: cs))
berghofe@13710
   241
  else x;
berghofe@13710
   242
haftmann@18314
   243
fun add_dummies f [] _ thy =
haftmann@18314
   244
      (([], NONE), thy)
haftmann@18314
   245
  | add_dummies f dts used thy =
haftmann@18314
   246
      thy
haftmann@18314
   247
      |> f (map snd dts)
wenzelm@30345
   248
      |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
haftmann@33968
   249
    handle Datatype_Aux.Datatype_Empty name' =>
berghofe@13710
   250
      let
wenzelm@30364
   251
        val name = Long_Name.base_name name';
wenzelm@43324
   252
        val dname = singleton (Name.variant_list used) "Dummy";
haftmann@18314
   253
      in
haftmann@18314
   254
        thy
wenzelm@30345
   255
        |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
berghofe@14888
   256
      end;
berghofe@13710
   257
berghofe@22271
   258
fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
berghofe@13710
   259
  let
berghofe@13725
   260
    val rvs = map fst (relevant_vars (prop_of rule));
wenzelm@16861
   261
    val xs = rev (Term.add_vars (prop_of rule) []);
haftmann@36692
   262
    val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
wenzelm@16861
   263
    val rlzvs = rev (Term.add_vars (prop_of rrule) []);
haftmann@17485
   264
    val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
berghofe@22271
   265
    val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
berghofe@37233
   266
    val rlz' = fold_rev Logic.all rs (prop_of rrule)
berghofe@22271
   267
  in (name, (vs,
wenzelm@33338
   268
    if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
berghofe@37233
   269
    Extraction.abs_corr_shyps thy rule vs vs2
berghofe@37233
   270
      (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
berghofe@37233
   271
         (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
berghofe@13710
   272
  end;
berghofe@13710
   273
berghofe@24157
   274
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
berghofe@24157
   275
wenzelm@33244
   276
fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
berghofe@13710
   277
  let
wenzelm@30364
   278
    val qualifier = Long_Name.qualifier (name_of_thm induct);
wenzelm@39557
   279
    val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts");
berghofe@37233
   280
    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
berghofe@13710
   281
    val ar = length vs + length iTs;
haftmann@31723
   282
    val params = Inductive.params_of raw_induct;
haftmann@31723
   283
    val arities = Inductive.arities_of raw_induct;
berghofe@22271
   284
    val nparms = length params;
berghofe@13710
   285
    val params' = map dest_Var params;
haftmann@31723
   286
    val rss = Inductive.partition_rules raw_induct intrs;
berghofe@22271
   287
    val rss' = map (fn (((s, rs), (_, arity)), elim) =>
haftmann@31723
   288
      (s, (Inductive.infer_intro_vars elim arity rs ~~ rs)))
berghofe@22790
   289
        (rss ~~ arities ~~ elims);
wenzelm@30364
   290
    val (prfx, _) = split_last (Long_Name.explode (fst (hd rss)));
berghofe@13710
   291
    val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
wenzelm@16123
   292
berghofe@13710
   293
    val thy1 = thy |>
wenzelm@24712
   294
      Sign.root_path |>
wenzelm@30364
   295
      Sign.add_path (Long_Name.implode prfx);
berghofe@13710
   296
    val (ty_eqs, rlz_eqs) = split_list
haftmann@36692
   297
      (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss);
berghofe@13710
   298
berghofe@13710
   299
    val thy1' = thy1 |>
wenzelm@42375
   300
      Sign.add_types_global
wenzelm@42375
   301
        (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
wenzelm@42375
   302
      Extraction.add_typeof_eqns_i ty_eqs;
haftmann@36692
   303
    val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
berghofe@22271
   304
      SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
berghofe@13710
   305
berghofe@13710
   306
    (** datatype representing computational content of inductive set **)
berghofe@13710
   307
haftmann@31783
   308
    val ((dummies, some_dt_names), thy2) =
haftmann@18008
   309
      thy1
wenzelm@45701
   310
      |> add_dummies (Datatype.add_datatype {strict = false, quiet = false})
wenzelm@45701
   311
        (map (pair false) dts) []
haftmann@18314
   312
      ||> Extraction.add_typeof_eqns_i ty_eqs
haftmann@18314
   313
      ||> Extraction.add_realizes_eqns_i rlz_eqs;
haftmann@31783
   314
    val dt_names = these some_dt_names;
haftmann@31784
   315
    val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names;
wenzelm@45701
   316
    val rec_thms =
wenzelm@45701
   317
      if null dt_names then []
wenzelm@45701
   318
      else #rec_rewrites (Datatype.the_info thy2 (hd dt_names));
wenzelm@19046
   319
    val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
haftmann@31781
   320
      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
haftmann@31458
   321
    val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
haftmann@31458
   322
      if member (op =) rsets s then
berghofe@13710
   323
        let
berghofe@13710
   324
          val (d :: dummies') = dummies;
wenzelm@19473
   325
          val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
haftmann@31458
   326
        in (map (head_of o hd o rev o snd o strip_comb o fst o
haftmann@31458
   327
          HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
berghofe@13710
   328
        end
haftmann@31458
   329
      else (replicate (length rs) Extraction.nullt, (recs, dummies)))
haftmann@31781
   330
        rss (rec_thms, dummies);
berghofe@37233
   331
    val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
berghofe@13710
   332
      (Extraction.realizes_of thy2 vs
berghofe@22271
   333
        (if c = Extraction.nullt then c else list_comb (c, map Var (rev
berghofe@37233
   334
          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
wenzelm@32952
   335
            (maps snd rss ~~ flat constrss);
wenzelm@30345
   336
    val (rlzpreds, rlzpreds') =
wenzelm@30345
   337
      rintrs |> map (fn rintr =>
berghofe@22271
   338
        let
wenzelm@30345
   339
          val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
wenzelm@30364
   340
          val s' = Long_Name.base_name s;
wenzelm@35845
   341
          val T' = Logic.unvarifyT_global T;
wenzelm@30345
   342
        in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
wenzelm@30345
   343
      |> distinct (op = o pairself (#1 o #1))
wenzelm@30345
   344
      |> map (apfst (apfst (apfst Binding.name)))
wenzelm@30345
   345
      |> split_list;
wenzelm@30345
   346
wenzelm@35845
   347
    val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT_global T))
berghofe@22271
   348
      (List.take (snd (strip_comb
berghofe@22271
   349
        (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
berghofe@13710
   350
berghofe@13710
   351
    (** realizability predicate **)
berghofe@13710
   352
berghofe@22271
   353
    val (ind_info, thy3') = thy2 |>
wenzelm@33726
   354
      Inductive.add_inductive_global
wenzelm@33669
   355
        {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
wenzelm@49170
   356
          no_elim = false, no_ind = false, skip_mono = false}
berghofe@22271
   357
        rlzpreds rlzparams (map (fn (rintr, intr) =>
wenzelm@30364
   358
          ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
wenzelm@35845
   359
           subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
berghofe@22271
   360
             (rintrs ~~ maps snd rss)) [] ||>
wenzelm@30435
   361
      Sign.root_path;
wenzelm@39557
   362
    val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
berghofe@13710
   363
berghofe@13710
   364
    (** realizer for induction rule **)
berghofe@13710
   365
haftmann@36692
   366
    val Ps = map_filter (fn _ $ M $ P => if member (op =) rsets (pred_of M) then
skalberg@15531
   367
      SOME (fst (fst (dest_Var (head_of P)))) else NONE)
berghofe@13710
   368
        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
berghofe@13710
   369
wenzelm@33244
   370
    fun add_ind_realizer Ps thy =
berghofe@13710
   371
      let
berghofe@24157
   372
        val vs' = rename (map (pairself (fst o fst o dest_Var))
berghofe@24157
   373
          (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
berghofe@24157
   374
            (hd (prems_of (hd inducts))))), nparms))) vs;
berghofe@22271
   375
        val rs = indrule_realizer thy induct raw_induct rsets params'
berghofe@24157
   376
          (vs' @ Ps) rec_names rss' intrs dummies;
berghofe@24157
   377
        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
berghofe@22271
   378
          (prop_of ind)) (rs ~~ inducts);
wenzelm@29281
   379
        val used = fold Term.add_free_names rlzs [];
berghofe@22271
   380
        val rnames = Name.variant_list used (replicate (length inducts) "r");
berghofe@22271
   381
        val rnames' = Name.variant_list
berghofe@22271
   382
          (used @ rnames) (replicate (length intrs) "s");
berghofe@22271
   383
        val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
berghofe@22271
   384
          let
wenzelm@35845
   385
            val (P, Q) = strip_one name (Logic.unvarify_global rlz);
berghofe@22271
   386
            val Q' = strip_all' [] rnames' Q
berghofe@22271
   387
          in
berghofe@22271
   388
            (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
berghofe@22271
   389
          end) (rlzs ~~ rnames);
berghofe@22271
   390
        val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
berghofe@22271
   391
          (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
haftmann@37136
   392
        val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
berghofe@37233
   393
        val thm = Goal.prove_global thy []
berghofe@37233
   394
          (map attach_typeS prems) (attach_typeS concl)
wenzelm@54742
   395
          (fn {context = ctxt, prems} => EVERY
berghofe@22271
   396
          [rtac (#raw_induct ind_info) 1,
wenzelm@54742
   397
           rewrite_goals_tac ctxt rews,
berghofe@13710
   398
           REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
wenzelm@54742
   399
             [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
berghofe@13710
   400
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
wenzelm@39557
   401
        val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
wenzelm@30364
   402
          (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
berghofe@22271
   403
        val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
haftmann@33968
   404
          (Datatype_Aux.split_conj_thm thm');
wenzelm@39557
   405
        val ([thms'], thy'') = Global_Theory.add_thmss
wenzelm@30435
   406
          [((Binding.qualified_name (space_implode "_"
wenzelm@30364
   407
             (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
haftmann@29579
   408
               ["correctness"])), thms), [])] thy';
berghofe@22271
   409
        val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
berghofe@13710
   410
      in
berghofe@13710
   411
        Extraction.add_realizers_i
berghofe@22271
   412
          (map (fn (((ind, corr), rlz), r) =>
berghofe@37233
   413
              mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
berghofe@22271
   414
            realizers @ (case realizers of
berghofe@22271
   415
             [(((ind, corr), rlz), r)] =>
berghofe@37233
   416
               [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
berghofe@22271
   417
                  ind, corr, rlz, r)]
berghofe@22271
   418
           | _ => [])) thy''
berghofe@13710
   419
      end;
berghofe@13710
   420
berghofe@13710
   421
    (** realizer for elimination rules **)
berghofe@13710
   422
berghofe@13710
   423
    val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
haftmann@31781
   424
      HOLogic.dest_Trueprop o prop_of o hd) case_thms;
berghofe@13710
   425
berghofe@13921
   426
    fun add_elim_realizer Ps
berghofe@13921
   427
      (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
berghofe@13710
   428
      let
berghofe@13710
   429
        val (prem :: prems) = prems_of elim;
berghofe@22271
   430
        fun reorder1 (p, (_, intr)) =
wenzelm@33244
   431
          fold (fn ((s, _), T) => Logic.all (Free (s, T)))
wenzelm@33244
   432
            (subtract (op =) params' (Term.add_vars (prop_of intr) []))
wenzelm@33244
   433
            (strip_all p);
berghofe@22271
   434
        fun reorder2 ((ivs, intr), i) =
haftmann@33040
   435
          let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) [])
wenzelm@33244
   436
          in fold (lambda o Var) fs (list_comb (Bound (i + length ivs), ivs)) end;
berghofe@13921
   437
        val p = Logic.list_implies
berghofe@13921
   438
          (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
berghofe@13710
   439
        val T' = Extraction.etype_of thy (vs @ Ps) [] p;
berghofe@13710
   440
        val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
berghofe@13921
   441
        val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
wenzelm@46219
   442
        val r =
wenzelm@46219
   443
          if null Ps then Extraction.nullt
wenzelm@46219
   444
          else
wenzelm@46219
   445
            fold_rev (Term.abs o pair "x") Ts
wenzelm@46219
   446
              (list_comb (Const (case_name, T),
wenzelm@46219
   447
                (if dummy then
wenzelm@46219
   448
                   [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
wenzelm@46219
   449
                 else []) @
wenzelm@46219
   450
                map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
wenzelm@46219
   451
                [Bound (length prems)]));
berghofe@22271
   452
        val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
berghofe@37233
   453
        val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
berghofe@13710
   454
        val rews = map mk_meta_eq case_thms;
berghofe@22271
   455
        val thm = Goal.prove_global thy []
wenzelm@51717
   456
          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz')
wenzelm@51717
   457
          (fn {context = ctxt, prems, ...} => EVERY
wenzelm@51717
   458
            [cut_tac (hd prems) 1,
wenzelm@51717
   459
             etac elimR 1,
wenzelm@51717
   460
             ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
wenzelm@54742
   461
             rewrite_goals_tac ctxt rews,
wenzelm@54742
   462
             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
wenzelm@51717
   463
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
wenzelm@39557
   464
        val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
haftmann@29579
   465
          (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
berghofe@13710
   466
      in
berghofe@13710
   467
        Extraction.add_realizers_i
berghofe@22271
   468
          [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
berghofe@13710
   469
      end;
berghofe@13710
   470
berghofe@13710
   471
    (** add realizers to theory **)
berghofe@13710
   472
wenzelm@33244
   473
    val thy4 = fold add_ind_realizer (subsets Ps) thy3;
berghofe@13710
   474
    val thy5 = Extraction.add_realizers_i
berghofe@22271
   475
      (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
berghofe@22271
   476
         (name_of_thm rule, rule, rrule, rlz,
haftmann@33040
   477
            list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) []))))))
wenzelm@32952
   478
              (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
wenzelm@32952
   479
    val elimps = map_filter (fn ((s, intrs), p) =>
haftmann@36692
   480
      if member (op =) rsets s then SOME (p, intrs) else NONE)
berghofe@22271
   481
        (rss' ~~ (elims ~~ #elims ind_info));
wenzelm@33244
   482
    val thy6 =
wenzelm@33244
   483
      fold (fn p as (((((elim, _), _), _), _), _) =>
wenzelm@33244
   484
        add_elim_realizer [] p #>
wenzelm@33244
   485
        add_elim_realizer [fst (fst (dest_Var (HOLogic.dest_Trueprop (concl_of elim))))] p)
wenzelm@33244
   486
      (elimps ~~ case_thms ~~ case_names ~~ dummies) thy5;
berghofe@13710
   487
wenzelm@24712
   488
  in Sign.restore_naming thy thy6 end;
berghofe@13710
   489
berghofe@13710
   490
fun add_ind_realizers name rsets thy =
berghofe@13710
   491
  let
berghofe@13710
   492
    val (_, {intrs, induct, raw_induct, elims, ...}) =
wenzelm@42361
   493
      Inductive.the_inductive (Proof_Context.init_global thy) name;
berghofe@13710
   494
    val vss = sort (int_ord o pairself length)
berghofe@22271
   495
      (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
berghofe@13710
   496
  in
berghofe@37233
   497
    fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
berghofe@13710
   498
  end
berghofe@13710
   499
wenzelm@20897
   500
fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
berghofe@13710
   501
  let
berghofe@13710
   502
    fun err () = error "ind_realizer: bad rule";
berghofe@13710
   503
    val sets =
berghofe@13710
   504
      (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
berghofe@22271
   505
           [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
berghofe@22271
   506
         | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
wenzelm@47060
   507
         handle TERM _ => err () | List.Empty => err ();
berghofe@13710
   508
  in 
wenzelm@18728
   509
    add_ind_realizers (hd sets)
wenzelm@18728
   510
      (case arg of
skalberg@15531
   511
        NONE => sets | SOME NONE => []
haftmann@33040
   512
      | SOME (SOME sets') => subtract (op =) sets' sets)
wenzelm@20897
   513
  end I);
berghofe@13710
   514
wenzelm@18708
   515
val setup =
wenzelm@30722
   516
  Attrib.setup @{binding ind_realizer}
wenzelm@30722
   517
    ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
wenzelm@35402
   518
      Scan.option (Scan.lift (Args.colon) |-- Scan.repeat1 (Args.const true)))) >> rlz_attrib)
wenzelm@30722
   519
    "add realizers for inductive set";
berghofe@13710
   520
berghofe@13710
   521
end;
wenzelm@15706
   522