src/HOL/Tools/inductive_realizer.ML
author wenzelm
Mon, 25 Feb 2008 16:31:15 +0100
changeset 26128 fe2d24c26e0c
parent 25977 b0604cd8e5e1
child 26336 a0e2b706ce73
permissions -rw-r--r--
inductive package: simplified group handling;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Tools/inductive_realizer.ML
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     2
    ID:         $Id$
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     4
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     5
Porgram extraction from proofs involving inductive predicates:
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     6
Realizers for induction and elimination rules
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     7
*)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     8
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     9
signature INDUCTIVE_REALIZER =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    10
sig
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    11
  val add_ind_realizers: string -> string list -> theory -> theory
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18358
diff changeset
    12
  val setup: theory -> theory
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    13
end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    14
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    15
structure InductiveRealizer : INDUCTIVE_REALIZER =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    16
struct
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    17
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    18
(* FIXME: LocalTheory.note should return theorems with proper names! *)
22606
962f824c2df9 - Tried to make name_of_thm more robust against changes of the
berghofe
parents: 22596
diff changeset
    19
fun name_of_thm thm =
962f824c2df9 - Tried to make name_of_thm more robust against changes of the
berghofe
parents: 22596
diff changeset
    20
  (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of
962f824c2df9 - Tried to make name_of_thm more robust against changes of the
berghofe
parents: 22596
diff changeset
    21
     [(name, _)] => name
962f824c2df9 - Tried to make name_of_thm more robust against changes of the
berghofe
parents: 22596
diff changeset
    22
   | _ => error ("name_of_thm: bad proof of theorem\n" ^ string_of_thm thm));
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    23
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    24
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    25
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    26
fun prf_of thm =
22596
d0d2af4db18f rep_thm/cterm/ctyp: removed obsolete sign field;
wenzelm
parents: 22271
diff changeset
    27
  let val {thy, prop, der = (_, prf), ...} = rep_thm thm
d0d2af4db18f rep_thm/cterm/ctyp: removed obsolete sign field;
wenzelm
parents: 22271
diff changeset
    28
  in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    29
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    30
fun forall_intr_prf (t, prf) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    31
  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    32
  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    33
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    34
fun forall_intr_term (t, u) =
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    35
  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    36
  in all T $ Abs (a, T, abstract_over (t, u)) end;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    37
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    38
fun subsets [] = [[]]
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    39
  | subsets (x::xs) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    40
      let val ys = subsets xs
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    41
      in ys @ map (cons x) ys end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    42
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    43
val pred_of = fst o dest_Const o head_of;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    44
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    45
fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    46
      let val (s', names') = (case names of
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    47
          [] => (Name.variant used s, [])
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    48
        | name :: names' => (name, names'))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    49
      in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    50
  | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    51
      t $ strip_all' used names Q
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    52
  | strip_all' _ _ t = t;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    53
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    54
fun strip_all t = strip_all' (add_term_free_names (t, [])) [] t;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    55
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    56
fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    57
      (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    58
  | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    59
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
    60
fun relevant_vars prop = foldr (fn
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    61
      (Var ((a, i), T), vs) => (case strip_type T of
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    62
        (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    63
      | _ => vs)
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
    64
    | (_, vs) => vs) [] (term_vars prop);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    65
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    66
fun dt_of_intrs thy vs nparms intrs =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    67
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    68
    val iTs = term_tvars (prop_of (hd intrs));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    69
    val Tvs = map TVar iTs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    70
    val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    71
      (Logic.strip_imp_concl (prop_of (hd intrs))));
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    72
    val params = map dest_Var (Library.take (nparms, ts));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    73
    val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    74
    fun constr_of_intr intr = (Sign.base_name (name_of_thm intr),
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19617
diff changeset
    75
      map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    76
        filter_out (equal Extraction.nullT) (map
19806
f860b7a98445 renamed Type.(un)varifyT to Logic.(un)varifyT;
wenzelm
parents: 19617
diff changeset
    77
          (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    78
            NoSyn);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    79
  in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    80
    map constr_of_intr intrs)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    81
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    82
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    83
fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    84
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    85
(** turn "P" into "%r x. realizes r (P x)" **)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    86
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    87
fun gen_rvar vs (t as Var ((a, 0), T)) =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    88
      if body_type T <> HOLogic.boolT then t else
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    89
        let
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    90
          val U = TVar (("'" ^ a, 0), HOLogic.typeS)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    91
          val Ts = binder_types T;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    92
          val i = length Ts;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    93
          val xs = map (pair "x") Ts;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    94
          val u = list_comb (t, map Bound (i - 1 downto 0))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    95
        in 
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    96
          if a mem vs then
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    97
            list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    98
          else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    99
        end
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   100
  | gen_rvar _ t = t;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   101
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   102
fun mk_realizes_eqn n vs nparms intrs =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   103
  let
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   104
    val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   105
    val iTs = term_tvars concl;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   106
    val Tvs = map TVar iTs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   107
    val (h as Const (s, T), us) = strip_comb concl;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   108
    val params = List.take (us, nparms);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   109
    val elTs = List.drop (binder_types T, nparms);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   110
    val predT = elTs ---> HOLogic.boolT;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   111
    val used = map (fst o fst o dest_Var) params;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   112
    val xs = map (Var o apfst (rpair 0))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   113
      (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   114
    val rT = if n then Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   115
      else Type (space_implode "_" (s ^ "T" :: vs),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   116
        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   117
    val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   118
    val S = list_comb (h, params @ xs);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   119
    val rvs = relevant_vars S;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   120
    val vs' = map fst rvs \\ vs;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   121
    val rname = space_implode "_" (s ^ "R" :: vs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   122
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   123
    fun mk_Tprem n v =
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   124
      let val T = (the o AList.lookup (op =) rvs) v
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   125
      in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   126
        Extraction.mk_typ (if n then Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   127
          else TVar (("'" ^ v, 0), HOLogic.typeS)))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   128
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   129
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   130
    val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   131
    val ts = map (gen_rvar vs) params;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   132
    val argTs = map fastype_of ts;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   133
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   134
  in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S,
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   135
       Extraction.mk_typ rT)),
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   136
    (prems, (mk_rlz rT $ r $ S,
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   137
       if n then list_comb (Const (rname, argTs ---> predT), ts @ xs)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   138
       else list_comb (Const (rname, argTs @ [rT] ---> predT), ts @ [r] @ xs))))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   139
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   140
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   141
fun fun_of_prem thy rsets vs params rule ivs intr =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   142
  let
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   143
    val ctxt = ProofContext.init thy
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   144
    val args = map (Free o apfst fst o dest_Var) ivs;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   145
    val args' = map (Free o apfst fst)
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   146
      (Term.add_vars (prop_of intr) [] \\ params);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   147
    val rule' = strip_all rule;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   148
    val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   149
    val used = map (fst o dest_Free) args;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   150
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   151
    fun is_rec t = not (null (term_consts t inter rsets));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   152
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   153
    fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   154
      | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   155
      | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   156
          Const (s, _) => can (InductivePackage.the_inductive ctxt) s
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   157
        | _ => true)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   158
      | is_meta _ = false;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   159
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   160
    fun fun_of ts rts args used (prem :: prems) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   161
          let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   162
            val T = Extraction.etype_of thy vs [] prem;
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 19806
diff changeset
   163
            val [x, r] = Name.variant_list used ["x", "r"]
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   164
          in if T = Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   165
            then fun_of ts rts args used prems
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   166
            else if is_rec prem then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   167
              if is_meta prem then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   168
                let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   169
                  val prem' :: prems' = prems;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   170
                  val U = Extraction.etype_of thy vs [] prem';
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   171
                in if U = Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   172
                  then fun_of (Free (x, T) :: ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   173
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   174
                    (Free (x, T) :: args) (x :: r :: used) prems'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   175
                  else fun_of (Free (x, T) :: ts) (Free (r, U) :: rts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   176
                    (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   177
                end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   178
              else (case strip_type T of
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   179
                  (Ts, Type ("*", [T1, T2])) =>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   180
                    let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   181
                      val fx = Free (x, Ts ---> T1);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   182
                      val fr = Free (r, Ts ---> T2);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   183
                      val bs = map Bound (length Ts - 1 downto 0);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   184
                      val t = list_abs (map (pair "z") Ts,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   185
                        HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   186
                    in fun_of (fx :: ts) (fr :: rts) (t::args)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   187
                      (x :: r :: used) prems
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   188
                    end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   189
                | (Ts, U) => fun_of (Free (x, T) :: ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   190
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   191
                    (Free (x, T) :: args) (x :: r :: used) prems)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   192
            else fun_of (Free (x, T) :: ts) rts (Free (x, T) :: args)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   193
              (x :: used) prems
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   194
          end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   195
      | fun_of ts rts args used [] =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   196
          let val xs = rev (rts @ ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   197
          in if conclT = Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   198
            then list_abs_free (map dest_Free xs, HOLogic.unit)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   199
            else list_abs_free (map dest_Free xs, list_comb
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   200
              (Free ("r" ^ Sign.base_name (name_of_thm intr),
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   201
                map fastype_of (rev args) ---> conclT), rev args))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   202
          end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   203
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   204
  in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   205
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   206
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   207
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   208
    val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   209
    val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   210
      SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   211
        find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   212
    val fs = maps (fn ((intrs, prems), dummy) =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   213
      let
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   214
        val fs = map (fn (rule, (ivs, intr)) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   215
          fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   216
      in if dummy then Const ("arbitrary",
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   217
          HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   218
        else fs
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   219
      end) (premss ~~ dummies);
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   220
    val frees = fold Term.add_frees fs [];
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   221
    val Ts = map fastype_of fs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   222
    fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   223
  in
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   224
    fst (fold_map (fn concl => fn names =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   225
      let val T = Extraction.etype_of thy vs [] concl
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   226
      in if T = Extraction.nullT then (Extraction.nullt, names) else
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   227
        let
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   228
          val Type ("fun", [U, _]) = T;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   229
          val a :: names' = names
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   230
        in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   231
          Option.map (pair (name_of_fn intr))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   232
            (AList.lookup (op =) frees (name_of_fn intr))) intrs,
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   233
          list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   234
        end
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   235
      end) concls rec_names)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   236
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   237
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   238
fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
23577
c5b93c69afd3 avoid polymorphic equality;
wenzelm
parents: 22790
diff changeset
   239
  if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   240
  else x;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   241
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   242
fun add_dummies f [] _ thy =
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   243
      (([], NONE), thy)
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   244
  | add_dummies f dts used thy =
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   245
      thy
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   246
      |> f (map snd dts)
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   247
      |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   248
    handle DatatypeAux.Datatype_Empty name' =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   249
      let
14888
99ac3eb0f84e add_dummies no longer uses transform_error but handles specific
berghofe
parents: 13928
diff changeset
   250
        val name = Sign.base_name name';
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 19806
diff changeset
   251
        val dname = Name.variant used "Dummy"
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   252
      in
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   253
        thy
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   254
        |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
14888
99ac3eb0f84e add_dummies no longer uses transform_error but handles specific
berghofe
parents: 13928
diff changeset
   255
      end;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   256
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   257
fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   258
  let
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   259
    val rvs = map fst (relevant_vars (prop_of rule));
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   260
    val xs = rev (Term.add_vars (prop_of rule) []);
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   261
    val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   262
    val rlzvs = rev (Term.add_vars (prop_of rrule) []);
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   263
    val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   264
    val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   265
    val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   266
    val rlz'' = foldr forall_intr_term rlz vs2
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   267
  in (name, (vs,
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   268
    if rt = Extraction.nullt then rt else
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   269
      foldr (uncurry lambda) rt vs1,
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   270
    ProofRewriteRules.un_hhf_proof rlz' rlz''
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   271
      (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   272
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   273
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   274
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   275
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   276
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   277
  let
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   278
    val qualifier = NameSpace.qualifier (name_of_thm induct);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   279
    val inducts = PureThy.get_thms thy (Name
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   280
      (NameSpace.qualified qualifier "inducts"));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   281
    val iTs = term_tvars (prop_of (hd intrs));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   282
    val ar = length vs + length iTs;
22790
e1cff9268177 Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents: 22606
diff changeset
   283
    val params = InductivePackage.params_of raw_induct;
e1cff9268177 Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents: 22606
diff changeset
   284
    val arities = InductivePackage.arities_of raw_induct;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   285
    val nparms = length params;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   286
    val params' = map dest_Var params;
22790
e1cff9268177 Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents: 22606
diff changeset
   287
    val rss = InductivePackage.partition_rules raw_induct intrs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   288
    val rss' = map (fn (((s, rs), (_, arity)), elim) =>
22790
e1cff9268177 Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents: 22606
diff changeset
   289
      (s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs)))
e1cff9268177 Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents: 22606
diff changeset
   290
        (rss ~~ arities ~~ elims);
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21646
diff changeset
   291
    val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   292
    val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
16123
1381e90c2694 Theory.restore_naming;
wenzelm
parents: 15706
diff changeset
   293
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   294
    val thy1 = thy |>
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24157
diff changeset
   295
      Sign.root_path |>
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24157
diff changeset
   296
      Sign.add_path (NameSpace.implode prfx);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   297
    val (ty_eqs, rlz_eqs) = split_list
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   298
      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   299
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   300
    val thy1' = thy1 |>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   301
      Theory.copy |>
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24157
diff changeset
   302
      Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
24926
bcb6b098df11 AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents: 24816
diff changeset
   303
      fold (fn s => AxClass.axiomatize_arity
19510
29fc4e5a638c AxClass.axiomatize_arity_i;
wenzelm
parents: 19473
diff changeset
   304
        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   305
        Extraction.add_typeof_eqns_i ty_eqs;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   306
    val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   307
      SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   308
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   309
    (** datatype representing computational content of inductive set **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   310
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   311
    val ((dummies, dt_info), thy2) =
18008
f193815cab2c swapped add_datatype result
haftmann
parents: 17959
diff changeset
   312
      thy1
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   313
      |> add_dummies
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   314
           (DatatypePackage.add_datatype_i false false (map #2 dts))
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   315
           (map (pair false) dts) []
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   316
      ||> Extraction.add_typeof_eqns_i ty_eqs
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   317
      ||> Extraction.add_realizes_eqns_i rlz_eqs;
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   318
    fun get f = (these oo Option.map) f;
19046
bc5c6c9b114e removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 18929
diff changeset
   319
    val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   320
      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   321
    val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   322
      if s mem rsets then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   323
        let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   324
          val (d :: dummies') = dummies;
19473
wenzelm
parents: 19046
diff changeset
   325
          val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   326
        in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   327
          fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   328
        end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   329
      else ((recs, dummies), replicate (length rs) Extraction.nullt))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   330
        ((get #rec_thms dt_info, dummies), rss);
18929
d81435108688 Envir.(beta_)eta_contract;
wenzelm
parents: 18728
diff changeset
   331
    val rintrs = map (fn (intr, c) => Envir.eta_contract
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   332
      (Extraction.realizes_of thy2 vs
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   333
        (if c = Extraction.nullt then c else list_comb (c, map Var (rev
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   334
          (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   335
            (maps snd rss ~~ List.concat constrss);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   336
    val (rlzpreds, rlzpreds') = split_list
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   337
      (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   338
        let
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   339
          val Const (s, T) = head_of (HOLogic.dest_Trueprop
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   340
            (Logic.strip_assums_concl rintr));
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   341
          val s' = Sign.base_name s;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   342
          val T' = Logic.unvarifyT T
24746
6d42be359d57 Adapted to changes in interface of add_inductive_i.
berghofe
parents: 24712
diff changeset
   343
        in (((s', T'), NoSyn),
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   344
          (Const (s, T'), Free (s', T')))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   345
        end) rintrs));
24746
6d42be359d57 Adapted to changes in interface of add_inductive_i.
berghofe
parents: 24712
diff changeset
   346
    val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   347
      (List.take (snd (strip_comb
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   348
        (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   349
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   350
    (** realizability predicate **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   351
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   352
    val (ind_info, thy3') = thy2 |>
26128
fe2d24c26e0c inductive package: simplified group handling;
wenzelm
parents: 25977
diff changeset
   353
      InductivePackage.add_inductive_global (serial_string ())
fe2d24c26e0c inductive package: simplified group handling;
wenzelm
parents: 25977
diff changeset
   354
        {verbose = false, kind = Thm.theoremK, alt_name = "",
fe2d24c26e0c inductive package: simplified group handling;
wenzelm
parents: 25977
diff changeset
   355
          coind = false, no_elim = false, no_ind = false}
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   356
        rlzpreds rlzparams (map (fn (rintr, intr) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   357
          ((Sign.base_name (name_of_thm intr), []),
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   358
           subst_atomic rlzpreds' (Logic.unvarify rintr)))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   359
             (rintrs ~~ maps snd rss)) [] ||>
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24157
diff changeset
   360
      Sign.absolute_path;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   361
    val thy3 = PureThy.hide_thms false
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   362
      (map name_of_thm (#intrs ind_info)) thy3';
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   363
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   364
    (** realizer for induction rule **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   365
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   366
    val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   367
      SOME (fst (fst (dest_Var (head_of P)))) else NONE)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   368
        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   369
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   370
    fun add_ind_realizer (thy, Ps) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   371
      let
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   372
        val vs' = rename (map (pairself (fst o fst o dest_Var))
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   373
          (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   374
            (hd (prems_of (hd inducts))))), nparms))) vs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   375
        val rs = indrule_realizer thy induct raw_induct rsets params'
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   376
          (vs' @ Ps) rec_names rss' intrs dummies;
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   377
        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   378
          (prop_of ind)) (rs ~~ inducts);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   379
        val used = foldr add_term_free_names [] rlzs;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   380
        val rnames = Name.variant_list used (replicate (length inducts) "r");
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   381
        val rnames' = Name.variant_list
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   382
          (used @ rnames) (replicate (length intrs) "s");
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   383
        val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   384
          let
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   385
            val (P, Q) = strip_one name (Logic.unvarify rlz);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   386
            val Q' = strip_all' [] rnames' Q
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   387
          in
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   388
            (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   389
          end) (rlzs ~~ rnames);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   390
        val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   391
          (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   392
        val rews = map mk_meta_eq
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   393
          (fst_conv :: snd_conv :: get #rec_thms dt_info);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   394
        val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   395
          [rtac (#raw_induct ind_info) 1,
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   396
           rewrite_goals_tac rews,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   397
           REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
23590
ad95084a5c63 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents: 23577
diff changeset
   398
             [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   399
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
18358
0a733e11021a re-oriented some result tuples in PureThy
haftmann
parents: 18314
diff changeset
   400
        val (thm', thy') = PureThy.store_thm ((space_implode "_"
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   401
          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   402
             ["correctness"]), thm), []) thy;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   403
        val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   404
          (DatatypeAux.split_conj_thm thm');
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   405
        val ([thms'], thy'') = PureThy.add_thmss
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   406
          [((space_implode "_"
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   407
             (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   408
               ["correctness"]), thms), [])] thy';
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   409
        val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   410
      in
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   411
        Extraction.add_realizers_i
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   412
          (map (fn (((ind, corr), rlz), r) =>
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   413
              mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   414
            realizers @ (case realizers of
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   415
             [(((ind, corr), rlz), r)] =>
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   416
               [mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct",
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   417
                  ind, corr, rlz, r)]
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   418
           | _ => [])) thy''
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   419
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   420
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   421
    (** realizer for elimination rules **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   422
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   423
    val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   424
      HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   425
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   426
    fun add_elim_realizer Ps
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   427
      (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   428
      let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   429
        val (prem :: prems) = prems_of elim;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   430
        fun reorder1 (p, (_, intr)) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   431
          Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   432
            (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   433
        fun reorder2 ((ivs, intr), i) =
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   434
          let val fs = Term.add_vars (prop_of intr) [] \\ params'
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   435
          in Library.foldl (fn (t, x) => lambda (Var x) t)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   436
            (list_comb (Bound (i + length ivs), ivs), fs)
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   437
          end;
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   438
        val p = Logic.list_implies
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   439
          (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   440
        val T' = Extraction.etype_of thy (vs @ Ps) [] p;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   441
        val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T';
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   442
        val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   443
        val r = if null Ps then Extraction.nullt
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   444
          else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   445
            (if dummy then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   446
               [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   447
             else []) @
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   448
            map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   449
            [Bound (length prems)]));
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   450
        val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   451
        val rlz' = strip_all (Logic.unvarify rlz);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   452
        val rews = map mk_meta_eq case_thms;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   453
        val thm = Goal.prove_global thy []
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   454
          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   455
          [cut_facts_tac [hd prems] 1,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   456
           etac elimR 1,
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   457
           ALLGOALS (asm_simp_tac HOL_basic_ss),
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   458
           rewrite_goals_tac rews,
23590
ad95084a5c63 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents: 23577
diff changeset
   459
           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   460
             DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
18358
0a733e11021a re-oriented some result tuples in PureThy
haftmann
parents: 18314
diff changeset
   461
        val (thm', thy') = PureThy.store_thm ((space_implode "_"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   462
          (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   463
      in
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   464
        Extraction.add_realizers_i
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   465
          [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   466
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   467
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   468
    (** add realizers to theory **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   469
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   470
    val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   471
    val thy5 = Extraction.add_realizers_i
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   472
      (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   473
         (name_of_thm rule, rule, rrule, rlz,
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   474
            list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   475
              (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   476
                 List.concat constrss))) thy4;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   477
    val elimps = List.mapPartial (fn ((s, intrs), p) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   478
      if s mem rsets then SOME (p, intrs) else NONE)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   479
        (rss' ~~ (elims ~~ #elims ind_info));
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   480
    val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   481
      add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   482
        (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   483
           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   484
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24157
diff changeset
   485
  in Sign.restore_naming thy thy6 end;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   486
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   487
fun add_ind_realizers name rsets thy =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   488
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   489
    val (_, {intrs, induct, raw_induct, elims, ...}) =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   490
      InductivePackage.the_inductive (ProofContext.init thy) name;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   491
    val vss = sort (int_ord o pairself length)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   492
      (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   493
  in
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   494
    Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   495
  end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   496
20897
3f8d2834b2c4 attribute: Context.mapping;
wenzelm
parents: 20071
diff changeset
   497
fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   498
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   499
    fun err () = error "ind_realizer: bad rule";
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   500
    val sets =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   501
      (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   502
           [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   503
         | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   504
         handle TERM _ => err () | Empty => err ();
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   505
  in 
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   506
    add_ind_realizers (hd sets)
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   507
      (case arg of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   508
        NONE => sets | SOME NONE => []
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   509
      | SOME (SOME sets') => sets \\ sets')
20897
3f8d2834b2c4 attribute: Context.mapping;
wenzelm
parents: 20071
diff changeset
   510
  end I);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   511
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   512
val ind_realizer = Attrib.syntax
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   513
 ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   514
    Scan.option (Scan.lift (Args.colon) |--
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   515
      Scan.repeat1 Args.const))) >> rlz_attrib);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   516
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18358
diff changeset
   517
val setup =
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   518
  Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   519
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   520
end;
15706
bc264e730103 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
   521