src/HOL/Tools/inductive_realizer.ML
author wenzelm
Wed Dec 31 18:53:16 2008 +0100 (2008-12-31)
changeset 29271 1d685baea08e
parent 29265 5b4247055bd7
child 29281 b22ccb3998db
permissions -rw-r--r--
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
use exists_Const directly;
berghofe@13710
     1
(*  Title:      HOL/Tools/inductive_realizer.ML
berghofe@13710
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@13710
     3
berghofe@13710
     4
Porgram 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
wenzelm@28800
    17
(* FIXME: LocalTheory.note should return theorems with proper names! *)  (* FIXME ?? *)
berghofe@22606
    18
fun name_of_thm thm =
wenzelm@28800
    19
  (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
wenzelm@28814
    20
      [Thm.proof_of thm] [] of
wenzelm@28800
    21
    [name] => name
wenzelm@28800
    22
  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
berghofe@22271
    23
berghofe@13710
    24
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
berghofe@13710
    25
berghofe@13710
    26
fun prf_of thm =
wenzelm@26626
    27
  let
wenzelm@26626
    28
    val thy = Thm.theory_of_thm thm;
wenzelm@28814
    29
    val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
wenzelm@26626
    30
  in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
berghofe@13710
    31
wenzelm@27330
    32
fun forall_intr_prf t prf =
berghofe@13710
    33
  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
skalberg@15531
    34
  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
berghofe@13710
    35
berghofe@13710
    36
fun subsets [] = [[]]
berghofe@13710
    37
  | subsets (x::xs) =
berghofe@13710
    38
      let val ys = subsets xs
berghofe@13710
    39
      in ys @ map (cons x) ys end;
berghofe@13710
    40
berghofe@22271
    41
val pred_of = fst o dest_Const o head_of;
berghofe@13710
    42
berghofe@22271
    43
fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
berghofe@22271
    44
      let val (s', names') = (case names of
berghofe@22271
    45
          [] => (Name.variant used s, [])
berghofe@22271
    46
        | name :: names' => (name, names'))
berghofe@22271
    47
      in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
berghofe@22271
    48
  | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
berghofe@22271
    49
      t $ strip_all' used names Q
berghofe@22271
    50
  | strip_all' _ _ t = t;
berghofe@22271
    51
wenzelm@29271
    52
fun strip_all t = strip_all' (OldTerm.add_term_free_names (t, [])) [] t;
berghofe@22271
    53
berghofe@22271
    54
fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
berghofe@22271
    55
      (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
berghofe@22271
    56
  | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
berghofe@13710
    57
skalberg@15574
    58
fun relevant_vars prop = foldr (fn
berghofe@13710
    59
      (Var ((a, i), T), vs) => (case strip_type T of
berghofe@22271
    60
        (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
berghofe@13710
    61
      | _ => vs)
wenzelm@29265
    62
    | (_, vs) => vs) [] (OldTerm.term_vars prop);
berghofe@13710
    63
berghofe@22271
    64
fun dt_of_intrs thy vs nparms intrs =
berghofe@13710
    65
  let
wenzelm@29271
    66
    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
berghofe@13710
    67
    val Tvs = map TVar iTs;
berghofe@22271
    68
    val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
berghofe@22271
    69
      (Logic.strip_imp_concl (prop_of (hd intrs))));
berghofe@22271
    70
    val params = map dest_Var (Library.take (nparms, ts));
berghofe@13710
    71
    val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
berghofe@22271
    72
    fun constr_of_intr intr = (Sign.base_name (name_of_thm intr),
wenzelm@19806
    73
      map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
berghofe@13710
    74
        filter_out (equal Extraction.nullT) (map
wenzelm@19806
    75
          (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
berghofe@13710
    76
            NoSyn);
berghofe@13710
    77
  in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
berghofe@13710
    78
    map constr_of_intr intrs)
berghofe@13710
    79
  end;
berghofe@13710
    80
berghofe@13710
    81
fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
berghofe@13710
    82
berghofe@22271
    83
(** turn "P" into "%r x. realizes r (P x)" **)
berghofe@13710
    84
berghofe@13710
    85
fun gen_rvar vs (t as Var ((a, 0), T)) =
berghofe@22271
    86
      if body_type T <> HOLogic.boolT then t else
berghofe@22271
    87
        let
berghofe@22271
    88
          val U = TVar (("'" ^ a, 0), HOLogic.typeS)
berghofe@22271
    89
          val Ts = binder_types T;
berghofe@22271
    90
          val i = length Ts;
berghofe@22271
    91
          val xs = map (pair "x") Ts;
berghofe@22271
    92
          val u = list_comb (t, map Bound (i - 1 downto 0))
berghofe@22271
    93
        in 
berghofe@22271
    94
          if a mem vs then
berghofe@22271
    95
            list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
berghofe@22271
    96
          else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
berghofe@22271
    97
        end
berghofe@13710
    98
  | gen_rvar _ t = t;
berghofe@13710
    99
berghofe@22271
   100
fun mk_realizes_eqn n vs nparms intrs =
berghofe@13710
   101
  let
berghofe@22271
   102
    val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
wenzelm@29271
   103
    val iTs = OldTerm.term_tvars concl;
berghofe@13710
   104
    val Tvs = map TVar iTs;
berghofe@22271
   105
    val (h as Const (s, T), us) = strip_comb concl;
berghofe@22271
   106
    val params = List.take (us, nparms);
berghofe@22271
   107
    val elTs = List.drop (binder_types T, nparms);
berghofe@22271
   108
    val predT = elTs ---> HOLogic.boolT;
berghofe@22271
   109
    val used = map (fst o fst o dest_Var) params;
berghofe@22271
   110
    val xs = map (Var o apfst (rpair 0))
berghofe@22271
   111
      (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
berghofe@13710
   112
    val rT = if n then Extraction.nullT
berghofe@13710
   113
      else Type (space_implode "_" (s ^ "T" :: vs),
berghofe@13710
   114
        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
berghofe@13710
   115
    val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
berghofe@22271
   116
    val S = list_comb (h, params @ xs);
berghofe@13710
   117
    val rvs = relevant_vars S;
berghofe@13710
   118
    val vs' = map fst rvs \\ vs;
berghofe@13710
   119
    val rname = space_implode "_" (s ^ "R" :: vs);
berghofe@13710
   120
berghofe@13710
   121
    fun mk_Tprem n v =
haftmann@17485
   122
      let val T = (the o AList.lookup (op =) rvs) v
berghofe@13710
   123
      in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
berghofe@13710
   124
        Extraction.mk_typ (if n then Extraction.nullT
berghofe@13710
   125
          else TVar (("'" ^ v, 0), HOLogic.typeS)))
berghofe@13710
   126
      end;
berghofe@13710
   127
berghofe@13710
   128
    val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
berghofe@22271
   129
    val ts = map (gen_rvar vs) params;
berghofe@13710
   130
    val argTs = map fastype_of ts;
berghofe@13710
   131
berghofe@22271
   132
  in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S,
berghofe@13710
   133
       Extraction.mk_typ rT)),
berghofe@22271
   134
    (prems, (mk_rlz rT $ r $ S,
berghofe@22271
   135
       if n then list_comb (Const (rname, argTs ---> predT), ts @ xs)
berghofe@22271
   136
       else list_comb (Const (rname, argTs @ [rT] ---> predT), ts @ [r] @ xs))))
berghofe@13710
   137
  end;
berghofe@13710
   138
berghofe@22271
   139
fun fun_of_prem thy rsets vs params rule ivs intr =
berghofe@13710
   140
  let
berghofe@22271
   141
    val ctxt = ProofContext.init thy
berghofe@22271
   142
    val args = map (Free o apfst fst o dest_Var) ivs;
berghofe@13710
   143
    val args' = map (Free o apfst fst)
wenzelm@16861
   144
      (Term.add_vars (prop_of intr) [] \\ params);
berghofe@13710
   145
    val rule' = strip_all rule;
berghofe@13710
   146
    val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
berghofe@13710
   147
    val used = map (fst o dest_Free) args;
berghofe@13710
   148
wenzelm@29271
   149
    val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
berghofe@13710
   150
berghofe@13710
   151
    fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
berghofe@13710
   152
      | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
berghofe@22271
   153
      | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
berghofe@22271
   154
          Const (s, _) => can (InductivePackage.the_inductive ctxt) s
berghofe@22271
   155
        | _ => true)
berghofe@13710
   156
      | is_meta _ = false;
berghofe@13710
   157
berghofe@13710
   158
    fun fun_of ts rts args used (prem :: prems) =
berghofe@13710
   159
          let
berghofe@13710
   160
            val T = Extraction.etype_of thy vs [] prem;
wenzelm@20071
   161
            val [x, r] = Name.variant_list used ["x", "r"]
berghofe@13710
   162
          in if T = Extraction.nullT
berghofe@13710
   163
            then fun_of ts rts args used prems
berghofe@13710
   164
            else if is_rec prem then
berghofe@13710
   165
              if is_meta prem then
berghofe@13710
   166
                let
berghofe@13710
   167
                  val prem' :: prems' = prems;
berghofe@13710
   168
                  val U = Extraction.etype_of thy vs [] prem';
berghofe@13710
   169
                in if U = Extraction.nullT
berghofe@13710
   170
                  then fun_of (Free (x, T) :: ts)
berghofe@13710
   171
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
berghofe@13710
   172
                    (Free (x, T) :: args) (x :: r :: used) prems'
berghofe@13710
   173
                  else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
berghofe@13710
   174
                    (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
berghofe@13710
   175
                end
berghofe@13710
   176
              else (case strip_type T of
berghofe@13710
   177
                  (Ts, Type ("*", [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);
berghofe@13710
   182
                      val t = list_abs (map (pair "z") Ts,
berghofe@13710
   183
                        HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
berghofe@13710
   184
                    in fun_of (fx :: ts) (fr :: rts) (t::args)
berghofe@13710
   185
                      (x :: r :: used) prems
berghofe@13710
   186
                    end
berghofe@13710
   187
                | (Ts, U) => fun_of (Free (x, T) :: ts)
berghofe@13710
   188
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
berghofe@13710
   189
                    (Free (x, T) :: args) (x :: r :: used) prems)
berghofe@13710
   190
            else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args)
berghofe@13710
   191
              (x :: used) prems
berghofe@13710
   192
          end
berghofe@13710
   193
      | fun_of ts rts args used [] =
berghofe@13710
   194
          let val xs = rev (rts @ ts)
berghofe@13710
   195
          in if conclT = Extraction.nullT
berghofe@13710
   196
            then list_abs_free (map dest_Free xs, HOLogic.unit)
berghofe@13710
   197
            else list_abs_free (map dest_Free xs, list_comb
berghofe@22271
   198
              (Free ("r" ^ Sign.base_name (name_of_thm intr),
berghofe@13710
   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));
skalberg@15570
   207
    val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
berghofe@22271
   208
      SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
skalberg@15570
   209
        find_index_eq (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)
haftmann@27982
   214
      in if dummy then Const ("HOL.default_class.default",
berghofe@13710
   215
          HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
berghofe@22271
   216
        else fs
berghofe@22271
   217
      end) (premss ~~ dummies);
wenzelm@16861
   218
    val frees = fold Term.add_frees fs [];
berghofe@13710
   219
    val Ts = map fastype_of fs;
berghofe@22271
   220
    fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr)
berghofe@22271
   221
  in
berghofe@22271
   222
    fst (fold_map (fn concl => fn names =>
berghofe@13710
   223
      let val T = Extraction.etype_of thy vs [] concl
berghofe@22271
   224
      in if T = Extraction.nullT then (Extraction.nullt, names) else
berghofe@22271
   225
        let
berghofe@22271
   226
          val Type ("fun", [U, _]) = T;
berghofe@22271
   227
          val a :: names' = names
berghofe@22271
   228
        in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
berghofe@22271
   229
          Option.map (pair (name_of_fn intr))
berghofe@22271
   230
            (AList.lookup (op =) frees (name_of_fn intr))) intrs,
berghofe@22271
   231
          list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
berghofe@22271
   232
        end
berghofe@22271
   233
      end) concls rec_names)
berghofe@13710
   234
  end;
berghofe@13710
   235
berghofe@13710
   236
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
wenzelm@23577
   237
  if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
berghofe@13710
   238
  else x;
berghofe@13710
   239
haftmann@18314
   240
fun add_dummies f [] _ thy =
haftmann@18314
   241
      (([], NONE), thy)
haftmann@18314
   242
  | add_dummies f dts used thy =
haftmann@18314
   243
      thy
haftmann@18314
   244
      |> f (map snd dts)
haftmann@18314
   245
      |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
haftmann@18314
   246
    handle DatatypeAux.Datatype_Empty name' =>
berghofe@13710
   247
      let
berghofe@14888
   248
        val name = Sign.base_name name';
wenzelm@20071
   249
        val dname = Name.variant used "Dummy"
haftmann@18314
   250
      in
haftmann@18314
   251
        thy
haftmann@18314
   252
        |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
berghofe@14888
   253
      end;
berghofe@13710
   254
berghofe@22271
   255
fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
berghofe@13710
   256
  let
berghofe@13725
   257
    val rvs = map fst (relevant_vars (prop_of rule));
wenzelm@16861
   258
    val xs = rev (Term.add_vars (prop_of rule) []);
berghofe@13725
   259
    val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
wenzelm@16861
   260
    val rlzvs = rev (Term.add_vars (prop_of rrule) []);
haftmann@17485
   261
    val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
berghofe@22271
   262
    val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
wenzelm@27330
   263
    val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
wenzelm@27330
   264
    val rlz'' = fold_rev Logic.all vs2 rlz
berghofe@22271
   265
  in (name, (vs,
berghofe@13710
   266
    if rt = Extraction.nullt then rt else
skalberg@15574
   267
      foldr (uncurry lambda) rt vs1,
berghofe@22271
   268
    ProofRewriteRules.un_hhf_proof rlz' rlz''
wenzelm@27330
   269
      (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
berghofe@13710
   270
  end;
berghofe@13710
   271
berghofe@24157
   272
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
berghofe@24157
   273
berghofe@13710
   274
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
berghofe@13710
   275
  let
berghofe@22271
   276
    val qualifier = NameSpace.qualifier (name_of_thm induct);
wenzelm@26343
   277
    val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
wenzelm@29271
   278
    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
berghofe@13710
   279
    val ar = length vs + length iTs;
berghofe@22790
   280
    val params = InductivePackage.params_of raw_induct;
berghofe@22790
   281
    val arities = InductivePackage.arities_of raw_induct;
berghofe@22271
   282
    val nparms = length params;
berghofe@13710
   283
    val params' = map dest_Var params;
berghofe@22790
   284
    val rss = InductivePackage.partition_rules raw_induct intrs;
berghofe@22271
   285
    val rss' = map (fn (((s, rs), (_, arity)), elim) =>
berghofe@22790
   286
      (s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs)))
berghofe@22790
   287
        (rss ~~ arities ~~ elims);
wenzelm@21858
   288
    val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
berghofe@13710
   289
    val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
wenzelm@16123
   290
berghofe@13710
   291
    val thy1 = thy |>
wenzelm@24712
   292
      Sign.root_path |>
wenzelm@24712
   293
      Sign.add_path (NameSpace.implode prfx);
berghofe@13710
   294
    val (ty_eqs, rlz_eqs) = split_list
berghofe@22271
   295
      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
berghofe@13710
   296
berghofe@13710
   297
    val thy1' = thy1 |>
berghofe@13710
   298
      Theory.copy |>
wenzelm@24712
   299
      Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
wenzelm@24926
   300
      fold (fn s => AxClass.axiomatize_arity
wenzelm@19510
   301
        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
berghofe@13710
   302
        Extraction.add_typeof_eqns_i ty_eqs;
skalberg@15570
   303
    val dts = List.mapPartial (fn (s, rs) => if s mem rsets 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@18314
   308
    val ((dummies, dt_info), thy2) =
haftmann@18008
   309
      thy1
haftmann@18314
   310
      |> add_dummies
haftmann@27112
   311
           (DatatypePackage.add_datatype false false (map #2 dts))
haftmann@18314
   312
           (map (pair false) dts) []
haftmann@18314
   313
      ||> Extraction.add_typeof_eqns_i ty_eqs
haftmann@18314
   314
      ||> Extraction.add_realizes_eqns_i rlz_eqs;
haftmann@18314
   315
    fun get f = (these oo Option.map) f;
wenzelm@19046
   316
    val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
berghofe@13710
   317
      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
berghofe@13710
   318
    val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
berghofe@13710
   319
      if s mem rsets then
berghofe@13710
   320
        let
berghofe@13710
   321
          val (d :: dummies') = dummies;
wenzelm@19473
   322
          val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
berghofe@13710
   323
        in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
berghofe@13710
   324
          fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
berghofe@13710
   325
        end
berghofe@13710
   326
      else ((recs, dummies), replicate (length rs) Extraction.nullt))
berghofe@13710
   327
        ((get #rec_thms dt_info, dummies), rss);
wenzelm@18929
   328
    val rintrs = map (fn (intr, c) => Envir.eta_contract
berghofe@13710
   329
      (Extraction.realizes_of thy2 vs
berghofe@22271
   330
        (if c = Extraction.nullt then c else list_comb (c, map Var (rev
berghofe@22271
   331
          (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
berghofe@22271
   332
            (maps snd rss ~~ List.concat constrss);
berghofe@22271
   333
    val (rlzpreds, rlzpreds') = split_list
berghofe@22271
   334
      (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
berghofe@22271
   335
        let
berghofe@22271
   336
          val Const (s, T) = head_of (HOLogic.dest_Trueprop
berghofe@22271
   337
            (Logic.strip_assums_concl rintr));
berghofe@22271
   338
          val s' = Sign.base_name s;
berghofe@22271
   339
          val T' = Logic.unvarifyT T
haftmann@28965
   340
        in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
berghofe@24746
   341
    val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
berghofe@22271
   342
      (List.take (snd (strip_comb
berghofe@22271
   343
        (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
berghofe@13710
   344
berghofe@13710
   345
    (** realizability predicate **)
berghofe@13710
   346
berghofe@22271
   347
    val (ind_info, thy3') = thy2 |>
wenzelm@26128
   348
      InductivePackage.add_inductive_global (serial_string ())
haftmann@28965
   349
        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
berghofe@26535
   350
          coind = false, no_elim = false, no_ind = false, skip_mono = false}
berghofe@22271
   351
        rlzpreds rlzparams (map (fn (rintr, intr) =>
haftmann@28965
   352
          ((Binding.name (Sign.base_name (name_of_thm intr)), []),
berghofe@22271
   353
           subst_atomic rlzpreds' (Logic.unvarify rintr)))
berghofe@22271
   354
             (rintrs ~~ maps snd rss)) [] ||>
wenzelm@24712
   355
      Sign.absolute_path;
wenzelm@26663
   356
    val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
berghofe@13710
   357
berghofe@13710
   358
    (** realizer for induction rule **)
berghofe@13710
   359
berghofe@22271
   360
    val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
skalberg@15531
   361
      SOME (fst (fst (dest_Var (head_of P)))) else NONE)
berghofe@13710
   362
        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
berghofe@13710
   363
berghofe@13710
   364
    fun add_ind_realizer (thy, Ps) =
berghofe@13710
   365
      let
berghofe@24157
   366
        val vs' = rename (map (pairself (fst o fst o dest_Var))
berghofe@24157
   367
          (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
berghofe@24157
   368
            (hd (prems_of (hd inducts))))), nparms))) vs;
berghofe@22271
   369
        val rs = indrule_realizer thy induct raw_induct rsets params'
berghofe@24157
   370
          (vs' @ Ps) rec_names rss' intrs dummies;
berghofe@24157
   371
        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
berghofe@22271
   372
          (prop_of ind)) (rs ~~ inducts);
wenzelm@29271
   373
        val used = foldr OldTerm.add_term_free_names [] rlzs;
berghofe@22271
   374
        val rnames = Name.variant_list used (replicate (length inducts) "r");
berghofe@22271
   375
        val rnames' = Name.variant_list
berghofe@22271
   376
          (used @ rnames) (replicate (length intrs) "s");
berghofe@22271
   377
        val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
berghofe@22271
   378
          let
berghofe@22271
   379
            val (P, Q) = strip_one name (Logic.unvarify rlz);
berghofe@22271
   380
            val Q' = strip_all' [] rnames' Q
berghofe@22271
   381
          in
berghofe@22271
   382
            (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
berghofe@22271
   383
          end) (rlzs ~~ rnames);
berghofe@22271
   384
        val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
berghofe@22271
   385
          (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
berghofe@13710
   386
        val rews = map mk_meta_eq
berghofe@13710
   387
          (fst_conv :: snd_conv :: get #rec_thms dt_info);
wenzelm@26711
   388
        val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
berghofe@22271
   389
          [rtac (#raw_induct ind_info) 1,
berghofe@13710
   390
           rewrite_goals_tac rews,
berghofe@13710
   391
           REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
wenzelm@23590
   392
             [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
berghofe@13710
   393
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
wenzelm@26481
   394
        val (thm', thy') = PureThy.store_thm (space_implode "_"
wenzelm@26481
   395
          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
berghofe@22271
   396
        val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
berghofe@22271
   397
          (DatatypeAux.split_conj_thm thm');
berghofe@22271
   398
        val ([thms'], thy'') = PureThy.add_thmss
berghofe@22271
   399
          [((space_implode "_"
berghofe@24157
   400
             (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
berghofe@22271
   401
               ["correctness"]), thms), [])] thy';
berghofe@22271
   402
        val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
berghofe@13710
   403
      in
berghofe@13710
   404
        Extraction.add_realizers_i
berghofe@22271
   405
          (map (fn (((ind, corr), rlz), r) =>
berghofe@24157
   406
              mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
berghofe@22271
   407
            realizers @ (case realizers of
berghofe@22271
   408
             [(((ind, corr), rlz), r)] =>
berghofe@24157
   409
               [mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct",
berghofe@22271
   410
                  ind, corr, rlz, r)]
berghofe@22271
   411
           | _ => [])) thy''
berghofe@13710
   412
      end;
berghofe@13710
   413
berghofe@13710
   414
    (** realizer for elimination rules **)
berghofe@13710
   415
berghofe@13710
   416
    val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
berghofe@13710
   417
      HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
berghofe@13710
   418
berghofe@13921
   419
    fun add_elim_realizer Ps
berghofe@13921
   420
      (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
berghofe@13710
   421
      let
berghofe@13710
   422
        val (prem :: prems) = prems_of elim;
berghofe@22271
   423
        fun reorder1 (p, (_, intr)) =
wenzelm@27330
   424
          Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t)
wenzelm@16861
   425
            (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
berghofe@22271
   426
        fun reorder2 ((ivs, intr), i) =
berghofe@22271
   427
          let val fs = Term.add_vars (prop_of intr) [] \\ params'
skalberg@15570
   428
          in Library.foldl (fn (t, x) => lambda (Var x) t)
berghofe@22271
   429
            (list_comb (Bound (i + length ivs), ivs), fs)
berghofe@13921
   430
          end;
berghofe@13921
   431
        val p = Logic.list_implies
berghofe@13921
   432
          (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
berghofe@13710
   433
        val T' = Extraction.etype_of thy (vs @ Ps) [] p;
berghofe@13710
   434
        val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
berghofe@13921
   435
        val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
berghofe@13710
   436
        val r = if null Ps then Extraction.nullt
berghofe@13710
   437
          else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
berghofe@13710
   438
            (if dummy then
haftmann@27982
   439
               [Abs ("x", HOLogic.unitT, Const ("HOL.default_class.default", body_type T))]
berghofe@13710
   440
             else []) @
berghofe@13921
   441
            map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
berghofe@13921
   442
            [Bound (length prems)]));
berghofe@22271
   443
        val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
berghofe@22271
   444
        val rlz' = strip_all (Logic.unvarify rlz);
berghofe@13710
   445
        val rews = map mk_meta_eq case_thms;
berghofe@22271
   446
        val thm = Goal.prove_global thy []
wenzelm@26711
   447
          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
berghofe@13710
   448
          [cut_facts_tac [hd prems] 1,
berghofe@13710
   449
           etac elimR 1,
berghofe@22271
   450
           ALLGOALS (asm_simp_tac HOL_basic_ss),
berghofe@13710
   451
           rewrite_goals_tac rews,
wenzelm@23590
   452
           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
berghofe@13710
   453
             DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
wenzelm@26481
   454
        val (thm', thy') = PureThy.store_thm (space_implode "_"
wenzelm@26481
   455
          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
berghofe@13710
   456
      in
berghofe@13710
   457
        Extraction.add_realizers_i
berghofe@22271
   458
          [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
berghofe@13710
   459
      end;
berghofe@13710
   460
berghofe@13710
   461
    (** add realizers to theory **)
berghofe@13710
   462
skalberg@15570
   463
    val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
berghofe@13710
   464
    val thy5 = Extraction.add_realizers_i
berghofe@22271
   465
      (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
berghofe@22271
   466
         (name_of_thm rule, rule, rrule, rlz,
berghofe@22271
   467
            list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
berghofe@22271
   468
              (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
berghofe@22271
   469
                 List.concat constrss))) thy4;
berghofe@22271
   470
    val elimps = List.mapPartial (fn ((s, intrs), p) =>
berghofe@22271
   471
      if s mem rsets then SOME (p, intrs) else NONE)
berghofe@22271
   472
        (rss' ~~ (elims ~~ #elims ind_info));
skalberg@15570
   473
    val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
berghofe@13710
   474
      add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
berghofe@13710
   475
        (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
berghofe@13710
   476
           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
berghofe@13710
   477
wenzelm@24712
   478
  in Sign.restore_naming thy thy6 end;
berghofe@13710
   479
berghofe@13710
   480
fun add_ind_realizers name rsets thy =
berghofe@13710
   481
  let
berghofe@13710
   482
    val (_, {intrs, induct, raw_induct, elims, ...}) =
berghofe@22271
   483
      InductivePackage.the_inductive (ProofContext.init thy) name;
berghofe@13710
   484
    val vss = sort (int_ord o pairself length)
berghofe@22271
   485
      (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
berghofe@13710
   486
  in
skalberg@15570
   487
    Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
berghofe@13710
   488
  end
berghofe@13710
   489
wenzelm@20897
   490
fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
berghofe@13710
   491
  let
berghofe@13710
   492
    fun err () = error "ind_realizer: bad rule";
berghofe@13710
   493
    val sets =
berghofe@13710
   494
      (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
berghofe@22271
   495
           [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
berghofe@22271
   496
         | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
skalberg@15570
   497
         handle TERM _ => err () | Empty => err ();
berghofe@13710
   498
  in 
wenzelm@18728
   499
    add_ind_realizers (hd sets)
wenzelm@18728
   500
      (case arg of
skalberg@15531
   501
        NONE => sets | SOME NONE => []
wenzelm@15703
   502
      | SOME (SOME sets') => sets \\ sets')
wenzelm@20897
   503
  end I);
berghofe@13710
   504
wenzelm@18728
   505
val ind_realizer = Attrib.syntax
wenzelm@15703
   506
 ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
wenzelm@15703
   507
    Scan.option (Scan.lift (Args.colon) |--
wenzelm@18728
   508
      Scan.repeat1 Args.const))) >> rlz_attrib);
berghofe@13710
   509
wenzelm@18708
   510
val setup =
wenzelm@18728
   511
  Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
berghofe@13710
   512
berghofe@13710
   513
end;
wenzelm@15706
   514