src/HOL/Tools/inductive_realizer.ML
author berghofe
Wed Nov 27 17:06:47 2002 +0100 (2002-11-27)
changeset 13725 12404b452034
parent 13710 75bec2c1bfd5
child 13921 69c627b6b28d
permissions -rw-r--r--
Changed format of realizers / correctness proofs.
berghofe@13710
     1
(*  Title:      HOL/Tools/inductive_realizer.ML
berghofe@13710
     2
    ID:         $Id$
berghofe@13710
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@13710
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
berghofe@13710
     5
berghofe@13710
     6
Porgram extraction from proofs involving inductive predicates:
berghofe@13710
     7
Realizers for induction and elimination rules
berghofe@13710
     8
*)
berghofe@13710
     9
berghofe@13710
    10
signature INDUCTIVE_REALIZER =
berghofe@13710
    11
sig
berghofe@13710
    12
  val add_ind_realizers: string -> string list -> theory -> theory
berghofe@13710
    13
  val setup: (theory -> theory) list
berghofe@13710
    14
end;
berghofe@13710
    15
berghofe@13710
    16
structure InductiveRealizer : INDUCTIVE_REALIZER =
berghofe@13710
    17
struct
berghofe@13710
    18
berghofe@13710
    19
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
berghofe@13710
    20
berghofe@13710
    21
fun prf_of thm =
berghofe@13710
    22
  let val {sign, prop, der = (_, prf), ...} = rep_thm thm
berghofe@13710
    23
  in Reconstruct.reconstruct_proof sign prop prf end;
berghofe@13710
    24
berghofe@13710
    25
fun forall_intr_prf (t, prf) =
berghofe@13710
    26
  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
berghofe@13710
    27
  in Abst (a, Some T, Proofterm.prf_abstract_over t prf) end;
berghofe@13710
    28
berghofe@13710
    29
fun subsets [] = [[]]
berghofe@13710
    30
  | subsets (x::xs) =
berghofe@13710
    31
      let val ys = subsets xs
berghofe@13710
    32
      in ys @ map (cons x) ys end;
berghofe@13710
    33
berghofe@13710
    34
val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem;
berghofe@13710
    35
berghofe@13710
    36
fun strip_all t =
berghofe@13710
    37
  let
berghofe@13710
    38
    fun strip used (Const ("all", _) $ Abs (s, T, t)) =
berghofe@13710
    39
          let val s' = variant used s
berghofe@13710
    40
          in strip (s'::used) (subst_bound (Free (s', T), t)) end
berghofe@13710
    41
      | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
berghofe@13710
    42
      | strip _ t = t;
berghofe@13710
    43
  in strip (add_term_free_names (t, [])) t end;
berghofe@13710
    44
berghofe@13710
    45
fun relevant_vars prop = foldr (fn
berghofe@13710
    46
      (Var ((a, i), T), vs) => (case strip_type T of
berghofe@13710
    47
        (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
berghofe@13710
    48
      | _ => vs)
berghofe@13710
    49
    | (_, vs) => vs) (term_vars prop, []);
berghofe@13710
    50
berghofe@13710
    51
fun params_of intr = map (fst o fst o dest_Var) (term_vars
berghofe@13710
    52
  (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
berghofe@13710
    53
    (Logic.strip_imp_concl intr)))));
berghofe@13710
    54
berghofe@13710
    55
fun dt_of_intrs thy vs intrs =
berghofe@13710
    56
  let
berghofe@13710
    57
    val iTs = term_tvars (prop_of (hd intrs));
berghofe@13710
    58
    val Tvs = map TVar iTs;
berghofe@13710
    59
    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
berghofe@13710
    60
    val (Const (s, _), ts) = strip_comb S;
berghofe@13710
    61
    val params = map dest_Var ts;
berghofe@13710
    62
    val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
berghofe@13710
    63
    fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
berghofe@13710
    64
      map (Type.unvarifyT o snd) (rev (Term.add_vars ([], prop_of intr)) \\ params) @
berghofe@13710
    65
        filter_out (equal Extraction.nullT) (map
berghofe@13710
    66
          (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
berghofe@13710
    67
            NoSyn);
berghofe@13710
    68
  in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
berghofe@13710
    69
    map constr_of_intr intrs)
berghofe@13710
    70
  end;
berghofe@13710
    71
berghofe@13710
    72
fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
berghofe@13710
    73
berghofe@13710
    74
(** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **)
berghofe@13710
    75
berghofe@13710
    76
fun gen_rvar vs (t as Var ((a, 0), T)) =
berghofe@13710
    77
      let val U = TVar (("'" ^ a, 0), HOLogic.typeS)
berghofe@13710
    78
      in case try HOLogic.dest_setT T of
berghofe@13710
    79
          None => if body_type T <> HOLogic.boolT then t else
berghofe@13710
    80
            let
berghofe@13710
    81
              val Ts = binder_types T;
berghofe@13710
    82
              val i = length Ts;
berghofe@13710
    83
              val xs = map (pair "x") Ts;
berghofe@13710
    84
              val u = list_comb (t, map Bound (i - 1 downto 0))
berghofe@13710
    85
            in 
berghofe@13710
    86
              if a mem vs then
berghofe@13710
    87
                list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
berghofe@13710
    88
              else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
berghofe@13710
    89
            end
berghofe@13710
    90
        | Some T' => if a mem vs then
berghofe@13710
    91
              Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $
berghofe@13710
    92
                (HOLogic.mk_mem (Bound 0, t))))
berghofe@13710
    93
            else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $
berghofe@13710
    94
              (HOLogic.mk_mem (Bound 0, t)))
berghofe@13710
    95
      end
berghofe@13710
    96
  | gen_rvar _ t = t;
berghofe@13710
    97
berghofe@13710
    98
fun mk_realizes_eqn n vs intrs =
berghofe@13710
    99
  let
berghofe@13710
   100
    val iTs = term_tvars (prop_of (hd intrs));
berghofe@13710
   101
    val Tvs = map TVar iTs;
berghofe@13710
   102
    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
berghofe@13710
   103
    val (Const (s, T), ts') = strip_comb S;
berghofe@13710
   104
    val setT = body_type T;
berghofe@13710
   105
    val elT = HOLogic.dest_setT setT;
berghofe@13710
   106
    val x = Var (("x", 0), elT);
berghofe@13710
   107
    val rT = if n then Extraction.nullT
berghofe@13710
   108
      else Type (space_implode "_" (s ^ "T" :: vs),
berghofe@13710
   109
        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
berghofe@13710
   110
    val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
berghofe@13710
   111
    val rvs = relevant_vars S;
berghofe@13710
   112
    val vs' = map fst rvs \\ vs;
berghofe@13710
   113
    val rname = space_implode "_" (s ^ "R" :: vs);
berghofe@13710
   114
berghofe@13710
   115
    fun mk_Tprem n v =
berghofe@13710
   116
      let val Some T = assoc (rvs, v)
berghofe@13710
   117
      in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
berghofe@13710
   118
        Extraction.mk_typ (if n then Extraction.nullT
berghofe@13710
   119
          else TVar (("'" ^ v, 0), HOLogic.typeS)))
berghofe@13710
   120
      end;
berghofe@13710
   121
berghofe@13710
   122
    val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
berghofe@13710
   123
    val ts = map (gen_rvar vs) ts';
berghofe@13710
   124
    val argTs = map fastype_of ts;
berghofe@13710
   125
berghofe@13710
   126
  in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S,
berghofe@13710
   127
       Extraction.mk_typ rT)),
berghofe@13710
   128
    (prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S),
berghofe@13710
   129
       if n then
berghofe@13710
   130
         HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts))
berghofe@13710
   131
       else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname,
berghofe@13710
   132
         argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts)))))
berghofe@13710
   133
  end;
berghofe@13710
   134
berghofe@13710
   135
fun fun_of_prem thy rsets vs params rule intr =
berghofe@13710
   136
  let
berghofe@13710
   137
    (* add_term_vars and Term.add_vars may return variables in different order *)
berghofe@13710
   138
    val args = map (Free o apfst fst o dest_Var)
berghofe@13710
   139
      (add_term_vars (prop_of intr, []) \\ map Var params);
berghofe@13710
   140
    val args' = map (Free o apfst fst)
berghofe@13710
   141
      (Term.add_vars ([], prop_of intr) \\ params);
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
berghofe@13710
   146
    fun is_rec t = not (null (term_consts t inter rsets));
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
berghofe@13710
   150
      | is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true
berghofe@13710
   151
      | is_meta _ = false;
berghofe@13710
   152
berghofe@13710
   153
    fun fun_of ts rts args used (prem :: prems) =
berghofe@13710
   154
          let
berghofe@13710
   155
            val T = Extraction.etype_of thy vs [] prem;
berghofe@13710
   156
            val [x, r] = variantlist (["x", "r"], used)
berghofe@13710
   157
          in if T = Extraction.nullT
berghofe@13710
   158
            then fun_of ts rts args used prems
berghofe@13710
   159
            else if is_rec prem then
berghofe@13710
   160
              if is_meta prem then
berghofe@13710
   161
                let
berghofe@13710
   162
                  val prem' :: prems' = prems;
berghofe@13710
   163
                  val U = Extraction.etype_of thy vs [] prem';
berghofe@13710
   164
                in if U = Extraction.nullT
berghofe@13710
   165
                  then fun_of (Free (x, T) :: ts)
berghofe@13710
   166
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
berghofe@13710
   167
                    (Free (x, T) :: args) (x :: r :: used) prems'
berghofe@13710
   168
                  else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
berghofe@13710
   169
                    (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
berghofe@13710
   170
                end
berghofe@13710
   171
              else (case strip_type T of
berghofe@13710
   172
                  (Ts, Type ("*", [T1, T2])) =>
berghofe@13710
   173
                    let
berghofe@13710
   174
                      val fx = Free (x, Ts ---> T1);
berghofe@13710
   175
                      val fr = Free (r, Ts ---> T2);
berghofe@13710
   176
                      val bs = map Bound (length Ts - 1 downto 0);
berghofe@13710
   177
                      val t = list_abs (map (pair "z") Ts,
berghofe@13710
   178
                        HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
berghofe@13710
   179
                    in fun_of (fx :: ts) (fr :: rts) (t::args)
berghofe@13710
   180
                      (x :: r :: used) prems
berghofe@13710
   181
                    end
berghofe@13710
   182
                | (Ts, U) => fun_of (Free (x, T) :: ts)
berghofe@13710
   183
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
berghofe@13710
   184
                    (Free (x, T) :: args) (x :: r :: used) prems)
berghofe@13710
   185
            else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args)
berghofe@13710
   186
              (x :: used) prems
berghofe@13710
   187
          end
berghofe@13710
   188
      | fun_of ts rts args used [] =
berghofe@13710
   189
          let val xs = rev (rts @ ts)
berghofe@13710
   190
          in if conclT = Extraction.nullT
berghofe@13710
   191
            then list_abs_free (map dest_Free xs, HOLogic.unit)
berghofe@13710
   192
            else list_abs_free (map dest_Free xs, list_comb
berghofe@13710
   193
              (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr),
berghofe@13710
   194
                map fastype_of (rev args) ---> conclT), rev args))
berghofe@13710
   195
          end
berghofe@13710
   196
berghofe@13710
   197
  in fun_of (rev args) [] args' used (Logic.strip_imp_prems rule') end;
berghofe@13710
   198
berghofe@13710
   199
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
berghofe@13710
   200
  let
berghofe@13710
   201
    val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
berghofe@13710
   202
    val premss = mapfilter (fn (s, rs) => if s mem rsets then
berghofe@13710
   203
      Some (map (fn r => nth_elem (find_index_eq (prop_of r) (map prop_of intrs),
berghofe@13710
   204
        prems_of raw_induct)) rs) else None) rss;
berghofe@13710
   205
    val concls' = mapfilter (fn (s, _) => if s mem rsets then
berghofe@13710
   206
        find_first (fn concl => s mem term_consts concl) concls
berghofe@13710
   207
      else None) rss;
berghofe@13710
   208
    val fs = flat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
berghofe@13710
   209
      let
berghofe@13710
   210
        val (intrs1, intrs2) = splitAt (length prems, intrs);
berghofe@13710
   211
        val fs = map (fn (rule, intr) =>
berghofe@13710
   212
          fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
berghofe@13710
   213
      in (intrs2, if dummy then Const ("arbitrary",
berghofe@13710
   214
          HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
berghofe@13710
   215
        else fs)
berghofe@13710
   216
      end) (intrs, (premss ~~ dummies))));
berghofe@13710
   217
    val frees = foldl Term.add_frees ([], fs);
berghofe@13710
   218
    val Ts = map fastype_of fs;
berghofe@13710
   219
    val rlzs = mapfilter (fn (a, concl) =>
berghofe@13710
   220
      let val T = Extraction.etype_of thy vs [] concl
berghofe@13710
   221
      in if T = Extraction.nullT then None
berghofe@13710
   222
        else Some (list_comb (Const (a, Ts ---> T), fs))
berghofe@13710
   223
      end) (rec_names ~~ concls')
berghofe@13710
   224
  in if null rlzs then Extraction.nullt else
berghofe@13710
   225
    let
berghofe@13710
   226
      val r = foldr1 HOLogic.mk_prod rlzs;
berghofe@13710
   227
      val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
berghofe@13710
   228
      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
berghofe@13710
   229
      val r' = list_abs_free (mapfilter (fn intr =>
berghofe@13710
   230
        apsome (pair (name_of_fn intr)) (assoc (frees, name_of_fn intr))) intrs,
berghofe@13710
   231
          if length concls = 1 then r $ x else r)
berghofe@13710
   232
    in
berghofe@13710
   233
      if length concls = 1 then lambda x r' else r'
berghofe@13710
   234
    end
berghofe@13710
   235
  end;
berghofe@13710
   236
berghofe@13710
   237
val nonempty_msg = explode "Nonemptiness check failed for datatype ";
berghofe@13710
   238
berghofe@13710
   239
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
berghofe@13710
   240
  if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
berghofe@13710
   241
  else x;
berghofe@13710
   242
berghofe@13710
   243
fun add_dummies f dts used thy =
berghofe@13710
   244
  apsnd (pair (map fst dts)) (transform_error (f (map snd dts)) thy)
berghofe@13710
   245
  handle ERROR_MESSAGE msg => if nonempty_msg prefix explode msg then
berghofe@13710
   246
      let
berghofe@13710
   247
        val name = Sign.base_name
berghofe@13710
   248
          (implode (drop (length nonempty_msg, explode msg)));
berghofe@13710
   249
        val dname = variant used "Dummy"
berghofe@13710
   250
      in add_dummies f (map (add_dummy name dname) dts) (dname :: used) thy
berghofe@13710
   251
      end
berghofe@13710
   252
    else error msg;
berghofe@13710
   253
berghofe@13710
   254
fun mk_realizer thy vs params ((rule, rrule), rt) =
berghofe@13710
   255
  let
berghofe@13725
   256
    val prems = prems_of rule ~~ prems_of rrule;
berghofe@13725
   257
    val rvs = map fst (relevant_vars (prop_of rule));
berghofe@13710
   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);
berghofe@13725
   260
    val rlzvs = rev (Term.add_vars ([], prop_of rrule));
berghofe@13725
   261
    val vs2 = map (fn (ixn, _) => Var (ixn, the (assoc (rlzvs, ixn)))) xs;
berghofe@13725
   262
    val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
berghofe@13710
   263
berghofe@13710
   264
    fun mk_prf _ [] prf = prf
berghofe@13725
   265
      | mk_prf rs ((prem, rprem) :: prems) prf =
berghofe@13725
   266
          if Extraction.etype_of thy vs [] prem = Extraction.nullT
berghofe@13725
   267
          then AbsP ("H", Some rprem, mk_prf rs prems prf)
berghofe@13725
   268
          else forall_intr_prf (Var (hd rs), AbsP ("H", Some rprem,
berghofe@13725
   269
            mk_prf (tl rs) prems prf));
berghofe@13710
   270
berghofe@13710
   271
  in (Thm.name_of_thm rule, (vs,
berghofe@13710
   272
    if rt = Extraction.nullt then rt else
berghofe@13725
   273
      foldr (uncurry lambda) (vs1, rt),
berghofe@13725
   274
    foldr forall_intr_prf (vs2, mk_prf rs prems (Proofterm.proof_combP
berghofe@13725
   275
      (prf_of rrule, map PBound (length prems - 1 downto 0))))))
berghofe@13710
   276
  end;
berghofe@13710
   277
berghofe@13710
   278
fun add_rule (rss, r) =
berghofe@13710
   279
  let
berghofe@13710
   280
    val _ $ (_ $ _ $ S) = concl_of r;
berghofe@13710
   281
    val (Const (s, _), _) = strip_comb S;
berghofe@13710
   282
    val rs = if_none (assoc (rss, s)) [];
berghofe@13710
   283
  in overwrite (rss, (s, rs @ [r])) end;
berghofe@13710
   284
berghofe@13710
   285
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
berghofe@13710
   286
  let
berghofe@13710
   287
    val iTs = term_tvars (prop_of (hd intrs));
berghofe@13710
   288
    val ar = length vs + length iTs;
berghofe@13710
   289
    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
berghofe@13710
   290
    val (_, params) = strip_comb S;
berghofe@13710
   291
    val params' = map dest_Var params;
berghofe@13710
   292
    val rss = foldl add_rule ([], intrs);
berghofe@13710
   293
    val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
berghofe@13710
   294
    val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
berghofe@13710
   295
    val {path, ...} = Sign.rep_sg (sign_of thy);
berghofe@13710
   296
    val thy1 = thy |>
berghofe@13710
   297
      Theory.root_path |>
berghofe@13710
   298
      Theory.add_path (NameSpace.pack prfx);
berghofe@13710
   299
    val (ty_eqs, rlz_eqs) = split_list
berghofe@13710
   300
      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
berghofe@13710
   301
berghofe@13710
   302
    val thy1' = thy1 |>
berghofe@13710
   303
      Theory.copy |>
berghofe@13710
   304
      Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
berghofe@13710
   305
      Theory.add_arities_i (map (fn s =>
berghofe@13710
   306
        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |>
berghofe@13710
   307
        Extraction.add_typeof_eqns_i ty_eqs;
berghofe@13710
   308
    val dts = mapfilter (fn (s, rs) => if s mem rsets then
berghofe@13710
   309
      Some (dt_of_intrs thy1' vs rs) else None) rss;
berghofe@13710
   310
berghofe@13710
   311
    (** datatype representing computational content of inductive set **)
berghofe@13710
   312
berghofe@13710
   313
    val (thy2, (dummies, dt_info)) = thy1 |>
berghofe@13710
   314
      (if null dts then rpair ([], None) else
berghofe@13710
   315
        apsnd (apsnd Some) o add_dummies (DatatypePackage.add_datatype_i false
berghofe@13710
   316
          (map #2 dts)) (map (pair false) dts) []) |>>
berghofe@13710
   317
      Extraction.add_typeof_eqns_i ty_eqs |>>
berghofe@13710
   318
      Extraction.add_realizes_eqns_i rlz_eqs;
berghofe@13710
   319
    fun get f x = if_none (apsome f x) [];
berghofe@13710
   320
    val rec_names = distinct (map (fst o dest_Const o head_of o fst o
berghofe@13710
   321
      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
berghofe@13710
   322
    val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
berghofe@13710
   323
      if s mem rsets then
berghofe@13710
   324
        let
berghofe@13710
   325
          val (d :: dummies') = dummies;
berghofe@13710
   326
          val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs)
berghofe@13710
   327
        in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
berghofe@13710
   328
          fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
berghofe@13710
   329
        end
berghofe@13710
   330
      else ((recs, dummies), replicate (length rs) Extraction.nullt))
berghofe@13710
   331
        ((get #rec_thms dt_info, dummies), rss);
berghofe@13725
   332
    val rintrs = map (fn (intr, c) => Pattern.eta_contract
berghofe@13710
   333
      (Extraction.realizes_of thy2 vs
berghofe@13710
   334
        c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
berghofe@13725
   335
          (rev (Term.add_vars ([], prop_of intr)) \\ params')) intr))))
berghofe@13710
   336
            (intrs ~~ flat constrss);
berghofe@13710
   337
    val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem
berghofe@13710
   338
      (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
berghofe@13710
   339
berghofe@13710
   340
    (** realizability predicate **)
berghofe@13710
   341
berghofe@13710
   342
    val (thy3', ind_info) = thy2 |>
berghofe@13710
   343
      InductivePackage.add_inductive_i false true "" false false false
berghofe@13710
   344
        (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
berghofe@13710
   345
          ((Sign.base_name (Thm.name_of_thm intr), strip_all
berghofe@13710
   346
            (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
berghofe@13710
   347
      Theory.absolute_path;
berghofe@13710
   348
    val thy3 = PureThy.hide_thms false
berghofe@13710
   349
      (map Thm.name_of_thm (#intrs ind_info)) thy3';
berghofe@13710
   350
berghofe@13710
   351
    (** realizer for induction rule **)
berghofe@13710
   352
berghofe@13710
   353
    val Ps = mapfilter (fn _ $ M $ P => if set_of M mem rsets then
berghofe@13710
   354
      Some (fst (fst (dest_Var (head_of P)))) else None)
berghofe@13710
   355
        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
berghofe@13710
   356
berghofe@13710
   357
    fun add_ind_realizer (thy, Ps) =
berghofe@13710
   358
      let
berghofe@13710
   359
        val r = indrule_realizer thy induct raw_induct rsets params'
berghofe@13710
   360
          (vs @ Ps) rec_names rss intrs dummies;
berghofe@13725
   361
        val rlz = strip_all (Logic.unvarify
berghofe@13725
   362
          (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
berghofe@13710
   363
        val rews = map mk_meta_eq
berghofe@13710
   364
          (fst_conv :: snd_conv :: get #rec_thms dt_info);
berghofe@13710
   365
        val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
berghofe@13710
   366
          [if length rss = 1 then
berghofe@13710
   367
             cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
berghofe@13710
   368
           else EVERY [rewrite_goals_tac (rews @ all_simps),
berghofe@13710
   369
             REPEAT (rtac allI 1), rtac (#induct ind_info) 1],
berghofe@13710
   370
           rewrite_goals_tac rews,
berghofe@13710
   371
           REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
berghofe@13710
   372
             [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
berghofe@13710
   373
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
berghofe@13710
   374
        val (thy', thm') = PureThy.store_thm ((space_implode "_"
berghofe@13710
   375
          (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
berghofe@13710
   376
      in
berghofe@13710
   377
        Extraction.add_realizers_i
berghofe@13710
   378
          [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
berghofe@13710
   379
      end;
berghofe@13710
   380
berghofe@13710
   381
    (** realizer for elimination rules **)
berghofe@13710
   382
berghofe@13710
   383
    val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
berghofe@13710
   384
      HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
berghofe@13710
   385
berghofe@13710
   386
    fun add_elim_realizer Ps ((((elim, elimR), case_thms), case_name), dummy) thy =
berghofe@13710
   387
      let
berghofe@13710
   388
        val (prem :: prems) = prems_of elim;
berghofe@13710
   389
        val p = Logic.list_implies (prems @ [prem], concl_of elim);
berghofe@13710
   390
        val T' = Extraction.etype_of thy (vs @ Ps) [] p;
berghofe@13710
   391
        val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
berghofe@13710
   392
        val Ts = filter_out (equal Extraction.nullT)
berghofe@13710
   393
          (map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim));
berghofe@13710
   394
        val r = if null Ps then Extraction.nullt
berghofe@13710
   395
          else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
berghofe@13710
   396
            (if dummy then
berghofe@13710
   397
               [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
berghofe@13710
   398
             else []) @
berghofe@13710
   399
            map Bound ((length prems - 1 downto 0) @ [length prems])));
berghofe@13725
   400
        val rlz = strip_all (Logic.unvarify
berghofe@13725
   401
          (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
berghofe@13710
   402
        val rews = map mk_meta_eq case_thms;
berghofe@13710
   403
        val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
berghofe@13710
   404
          [cut_facts_tac [hd prems] 1,
berghofe@13710
   405
           etac elimR 1,
berghofe@13710
   406
           ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
berghofe@13710
   407
           rewrite_goals_tac rews,
berghofe@13710
   408
           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
berghofe@13710
   409
             DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
berghofe@13710
   410
        val (thy', thm') = PureThy.store_thm ((space_implode "_"
berghofe@13710
   411
          (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
berghofe@13710
   412
      in
berghofe@13710
   413
        Extraction.add_realizers_i
berghofe@13710
   414
          [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
berghofe@13710
   415
      end;
berghofe@13710
   416
berghofe@13710
   417
    (** add realizers to theory **)
berghofe@13710
   418
berghofe@13710
   419
    val rintr_thms = flat (map (fn (_, rs) => map (fn r => nth_elem
berghofe@13710
   420
      (find_index_eq r intrs, #intrs ind_info)) rs) rss);
berghofe@13710
   421
    val thy4 = foldl add_ind_realizer (thy3, subsets Ps);
berghofe@13710
   422
    val thy5 = Extraction.add_realizers_i
berghofe@13710
   423
      (map (mk_realizer thy4 vs params')
berghofe@13710
   424
         (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
berghofe@13710
   425
            map Var (rev (Term.add_vars ([], prop_of rule)) \\ params')))) 
berghofe@13710
   426
              (flat (map snd rss) ~~ rintr_thms ~~ flat constrss))) thy4;
berghofe@13710
   427
    val elimps = mapfilter (fn (s, _) => if s mem rsets then
berghofe@13710
   428
        find_first (fn (thm, _) => s mem term_consts (hd (prems_of thm)))
berghofe@13710
   429
          (elims ~~ #elims ind_info)
berghofe@13710
   430
      else None) rss;
berghofe@13710
   431
    val thy6 = foldl (fn (thy, p as ((((elim, _), _), _), _)) => thy |>
berghofe@13710
   432
      add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
berghofe@13710
   433
        (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
berghofe@13710
   434
           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
berghofe@13710
   435
berghofe@13710
   436
  in Theory.add_path (NameSpace.pack (if_none path [])) thy6 end;
berghofe@13710
   437
berghofe@13710
   438
fun add_ind_realizers name rsets thy =
berghofe@13710
   439
  let
berghofe@13710
   440
    val (_, {intrs, induct, raw_induct, elims, ...}) =
berghofe@13710
   441
      (case InductivePackage.get_inductive thy name of
berghofe@13710
   442
         None => error ("Unknown inductive set " ^ quote name)
berghofe@13710
   443
       | Some info => info);
berghofe@13710
   444
    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
berghofe@13710
   445
    val vss = sort (int_ord o pairself length)
berghofe@13710
   446
      (subsets (map fst (relevant_vars S)))
berghofe@13710
   447
  in
berghofe@13710
   448
    foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
berghofe@13710
   449
  end
berghofe@13710
   450
berghofe@13710
   451
fun rlz_attrib arg (thy, thm) =
berghofe@13710
   452
  let
berghofe@13710
   453
    fun err () = error "ind_realizer: bad rule";
berghofe@13710
   454
    val sets =
berghofe@13710
   455
      (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
berghofe@13710
   456
           [_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
berghofe@13710
   457
         | xs => map (set_of o fst o HOLogic.dest_imp) xs)
berghofe@13710
   458
         handle TERM _ => err () | LIST _ => err ();
berghofe@13710
   459
  in 
berghofe@13710
   460
    (add_ind_realizers (hd sets) (case arg of
berghofe@13710
   461
        None => sets | Some None => []
berghofe@13710
   462
      | Some (Some sets') => sets \\ map (Sign.intern_const (sign_of thy)) sets')
berghofe@13710
   463
      thy, thm)
berghofe@13710
   464
  end;
berghofe@13710
   465
berghofe@13710
   466
val rlz_attrib_global = Attrib.syntax (Scan.lift
berghofe@13710
   467
  (Scan.option (Args.$$$ "irrelevant" |--
berghofe@13710
   468
    Scan.option (Args.colon |-- Scan.repeat1 Args.name))) >> rlz_attrib);
berghofe@13710
   469
berghofe@13710
   470
val setup = [Attrib.add_attributes [("ind_realizer",
berghofe@13710
   471
  (rlz_attrib_global, K Attrib.undef_local_attribute),
berghofe@13710
   472
  "add realizers for inductive set")]];
berghofe@13710
   473
berghofe@13710
   474
end;