src/HOL/Tools/inductive_realizer.ML
author wenzelm
Mon, 06 Feb 2006 20:58:54 +0100
changeset 18929 d81435108688
parent 18728 6790126ab5f6
child 19046 bc5c6c9b114e
permissions -rw-r--r--
Envir.(beta_)eta_contract;
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
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    18
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
    19
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    20
fun prf_of thm =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    21
  let val {sign, prop, der = (_, prf), ...} = rep_thm thm
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    22
  in Reconstruct.reconstruct_proof sign prop prf end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    23
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    24
fun forall_intr_prf (t, prf) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    25
  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
    26
  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
    27
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    28
fun subsets [] = [[]]
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    29
  | subsets (x::xs) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    30
      let val ys = subsets xs
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    31
      in ys @ map (cons x) ys end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    32
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    33
val set_of = fst o dest_Const o head_of o snd o HOLogic.dest_mem;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    34
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    35
fun strip_all t =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    36
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    37
    fun strip used (Const ("all", _) $ Abs (s, T, t)) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    38
          let val s' = variant used s
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    39
          in strip (s'::used) (subst_bound (Free (s', T), t)) end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    40
      | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    41
      | strip _ t = t;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    42
  in strip (add_term_free_names (t, [])) t end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    43
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
    44
fun relevant_vars prop = foldr (fn
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    45
      (Var ((a, i), T), vs) => (case strip_type T of
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    46
        (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    47
      | _ => vs)
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
    48
    | (_, vs) => vs) [] (term_vars prop);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    49
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    50
fun params_of intr = map (fst o fst o dest_Var) (term_vars
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    51
  (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    52
    (Logic.strip_imp_concl intr)))));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    53
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    54
fun dt_of_intrs thy vs intrs =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    55
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    56
    val iTs = term_tvars (prop_of (hd intrs));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    57
    val Tvs = map TVar iTs;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    58
    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    59
    val (Const (s, _), ts) = strip_comb S;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    60
    val params = map dest_Var ts;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    61
    val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    62
    fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
    63
      map (Type.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
    64
        filter_out (equal Extraction.nullT) (map
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    65
          (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    66
            NoSyn);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    67
  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
    68
    map constr_of_intr intrs)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    69
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    70
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    71
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
    72
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    73
(** turn "P" into "%r x. realizes r (P x)" or "%r x. realizes r (x : P)" **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    74
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    75
fun gen_rvar vs (t as Var ((a, 0), T)) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    76
      let val U = TVar (("'" ^ a, 0), HOLogic.typeS)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    77
      in case try HOLogic.dest_setT T of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    78
          NONE => if body_type T <> HOLogic.boolT then t else
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    79
            let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    80
              val Ts = binder_types T;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    81
              val i = length Ts;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    82
              val xs = map (pair "x") Ts;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    83
              val u = list_comb (t, map Bound (i - 1 downto 0))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    84
            in 
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    85
              if a mem vs then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    86
                list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    87
              else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    88
            end
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    89
        | SOME T' => if a mem vs then
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    90
              Abs ("r", U, Abs ("x", T', mk_rlz U $ Bound 1 $
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    91
                (HOLogic.mk_mem (Bound 0, t))))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    92
            else Abs ("x", T', mk_rlz Extraction.nullT $ Extraction.nullt $
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    93
              (HOLogic.mk_mem (Bound 0, t)))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    94
      end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    95
  | gen_rvar _ t = t;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    96
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    97
fun mk_realizes_eqn n vs intrs =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    98
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    99
    val iTs = term_tvars (prop_of (hd intrs));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   100
    val Tvs = map TVar iTs;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   101
    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   102
    val (Const (s, T), ts') = strip_comb S;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   103
    val setT = body_type T;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   104
    val elT = HOLogic.dest_setT setT;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   105
    val x = Var (("x", 0), elT);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   106
    val rT = if n then Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   107
      else Type (space_implode "_" (s ^ "T" :: vs),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   108
        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   109
    val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   110
    val rvs = relevant_vars S;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   111
    val vs' = map fst rvs \\ vs;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   112
    val rname = space_implode "_" (s ^ "R" :: vs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   113
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   114
    fun mk_Tprem n v =
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   115
      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
   116
      in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   117
        Extraction.mk_typ (if n then Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   118
          else TVar (("'" ^ v, 0), HOLogic.typeS)))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   119
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   120
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   121
    val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   122
    val ts = map (gen_rvar vs) ts';
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   123
    val argTs = map fastype_of ts;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   124
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   125
  in ((prems, (Const ("typeof", setT --> Type ("Type", [])) $ S,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   126
       Extraction.mk_typ rT)),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   127
    (prems, (mk_rlz rT $ r $ HOLogic.mk_mem (x, S),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   128
       if n then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   129
         HOLogic.mk_mem (x, list_comb (Const (rname, argTs ---> setT), ts))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   130
       else HOLogic.mk_mem (HOLogic.mk_prod (r, x), list_comb (Const (rname,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   131
         argTs ---> HOLogic.mk_setT (HOLogic.mk_prodT (rT, elT))), ts)))))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   132
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   133
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   134
fun fun_of_prem thy rsets vs params rule intr =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   135
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   136
    (* add_term_vars and Term.add_vars may return variables in different order *)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   137
    val args = map (Free o apfst fst o dest_Var)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   138
      (add_term_vars (prop_of intr, []) \\ map Var params);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   139
    val args' = map (Free o apfst fst)
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   140
      (Term.add_vars (prop_of intr) [] \\ params);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   141
    val rule' = strip_all rule;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   142
    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
   143
    val used = map (fst o dest_Free) args;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   144
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   145
    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
   146
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   147
    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
   148
      | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   149
      | is_meta (Const ("Trueprop", _) $ (Const ("op :", _) $ _ $ _)) = true
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   150
      | is_meta _ = false;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   151
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   152
    fun fun_of ts rts args used (prem :: prems) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   153
          let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   154
            val T = Extraction.etype_of thy vs [] prem;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   155
            val [x, r] = variantlist (["x", "r"], used)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   156
          in if T = Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   157
            then fun_of ts rts args used prems
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   158
            else if is_rec prem then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   159
              if is_meta prem then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   160
                let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   161
                  val prem' :: prems' = prems;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   162
                  val U = Extraction.etype_of thy vs [] prem';
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   163
                in if U = Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   164
                  then fun_of (Free (x, T) :: ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   165
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   166
                    (Free (x, T) :: args) (x :: r :: used) prems'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   167
                  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
   168
                    (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
   169
                end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   170
              else (case strip_type T of
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   171
                  (Ts, Type ("*", [T1, T2])) =>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   172
                    let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   173
                      val fx = Free (x, Ts ---> T1);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   174
                      val fr = Free (r, Ts ---> T2);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   175
                      val bs = map Bound (length Ts - 1 downto 0);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   176
                      val t = list_abs (map (pair "z") Ts,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   177
                        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
   178
                    in fun_of (fx :: ts) (fr :: rts) (t::args)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   179
                      (x :: r :: used) prems
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   180
                    end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   181
                | (Ts, U) => fun_of (Free (x, T) :: ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   182
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   183
                    (Free (x, T) :: args) (x :: r :: used) prems)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   184
            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
   185
              (x :: used) prems
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   186
          end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   187
      | fun_of ts rts args used [] =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   188
          let val xs = rev (rts @ ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   189
          in if conclT = Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   190
            then list_abs_free (map dest_Free xs, HOLogic.unit)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   191
            else list_abs_free (map dest_Free xs, list_comb
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   192
              (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   193
                map fastype_of (rev args) ---> conclT), rev args))
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
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   196
  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
   197
18008
f193815cab2c swapped add_datatype result
haftmann
parents: 17959
diff changeset
   198
fun find_first f = Library.find_first f;
f193815cab2c swapped add_datatype result
haftmann
parents: 17959
diff changeset
   199
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   200
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
   201
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   202
    val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   203
    val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   204
      SOME (map (fn r => List.nth (prems_of raw_induct,
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   205
        find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   206
    val concls' = List.mapPartial (fn (s, _) => if s mem rsets then
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   207
        find_first (fn concl => s mem term_consts concl) concls
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   208
      else NONE) rss;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   209
    val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   210
      let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   211
        val (intrs1, intrs2) = splitAt (length prems, intrs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   212
        val fs = map (fn (rule, intr) =>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   213
          fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   214
      in (intrs2, if dummy then Const ("arbitrary",
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   215
          HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   216
        else fs)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   217
      end) (intrs, (premss ~~ dummies))));
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   218
    val frees = fold Term.add_frees fs [];
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   219
    val Ts = map fastype_of fs;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   220
    val rlzs = List.mapPartial (fn (a, concl) =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   221
      let val T = Extraction.etype_of thy vs [] concl
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   222
      in if T = Extraction.nullT then NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   223
        else SOME (list_comb (Const (a, Ts ---> T), fs))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   224
      end) (rec_names ~~ concls')
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   225
  in if null rlzs then Extraction.nullt else
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   226
    let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   227
      val r = foldr1 HOLogic.mk_prod rlzs;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   228
      val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   229
      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   230
      val r' = list_abs_free (List.mapPartial (fn intr =>
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   231
        Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   232
          if length concls = 1 then r $ x else r)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   233
    in
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   234
      if length concls = 1 then lambda x r' else r'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   235
    end
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))) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   239
  if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
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';
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   251
        val dname = 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
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   257
fun mk_realizer thy vs params ((rule, rrule), rt) =
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 prems = prems_of rule ~~ prems_of rrule;
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   260
    val rvs = map fst (relevant_vars (prop_of rule));
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   261
    val xs = rev (Term.add_vars (prop_of rule) []);
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   262
    val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   263
    val rlzvs = rev (Term.add_vars (prop_of rrule) []);
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   264
    val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   265
    val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   266
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   267
    fun mk_prf _ [] prf = prf
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   268
      | mk_prf rs ((prem, rprem) :: prems) prf =
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   269
          if Extraction.etype_of thy vs [] prem = Extraction.nullT
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   270
          then AbsP ("H", SOME rprem, mk_prf rs prems prf)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   271
          else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   272
            mk_prf (tl rs) prems prf));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   273
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   274
  in (Thm.name_of_thm rule, (vs,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   275
    if rt = Extraction.nullt then rt else
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   276
      foldr (uncurry lambda) rt vs1,
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   277
    foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   278
      (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   279
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   280
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   281
fun add_rule r rss =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   282
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   283
    val _ $ (_ $ _ $ S) = concl_of r;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   284
    val (Const (s, _), _) = strip_comb S;
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   285
  in
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   286
    rss
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   287
    |> AList.default (op =) (s, [])
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   288
    |> AList.map_entry (op =) s (fn rs => rs @ [r])
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   289
  end;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   290
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   291
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
   292
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   293
    val iTs = term_tvars (prop_of (hd intrs));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   294
    val ar = length vs + length iTs;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   295
    val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   296
    val (_, params) = strip_comb S;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   297
    val params' = map dest_Var params;
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   298
    val rss = [] |> Library.fold add_rule intrs;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   299
    val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   300
    val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
16123
1381e90c2694 Theory.restore_naming;
wenzelm
parents: 15706
diff changeset
   301
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   302
    val thy1 = thy |>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   303
      Theory.root_path |>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   304
      Theory.add_path (NameSpace.pack prfx);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   305
    val (ty_eqs, rlz_eqs) = split_list
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   306
      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   307
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   308
    val thy1' = thy1 |>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   309
      Theory.copy |>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   310
      Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   311
      Theory.add_arities_i (map (fn s =>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   312
        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   313
        Extraction.add_typeof_eqns_i ty_eqs;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   314
    val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   315
      SOME (dt_of_intrs thy1' vs rs) else NONE) rss;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   316
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   317
    (** datatype representing computational content of inductive set **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   318
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   319
    val ((dummies, dt_info), thy2) =
18008
f193815cab2c swapped add_datatype result
haftmann
parents: 17959
diff changeset
   320
      thy1
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   321
      |> add_dummies
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   322
           (DatatypePackage.add_datatype_i false false (map #2 dts))
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   323
           (map (pair false) dts) []
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   324
      ||> Extraction.add_typeof_eqns_i ty_eqs
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   325
      ||> Extraction.add_realizes_eqns_i rlz_eqs;
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   326
    fun get f = (these oo Option.map) f;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   327
    val rec_names = distinct (map (fst o dest_Const o head_of o fst o
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   328
      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
   329
    val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   330
      if s mem rsets then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   331
        let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   332
          val (d :: dummies') = dummies;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   333
          val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   334
        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
   335
          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
   336
        end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   337
      else ((recs, dummies), replicate (length rs) Extraction.nullt))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   338
        ((get #rec_thms dt_info, dummies), rss);
18929
d81435108688 Envir.(beta_)eta_contract;
wenzelm
parents: 18728
diff changeset
   339
    val rintrs = map (fn (intr, c) => Envir.eta_contract
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   340
      (Extraction.realizes_of thy2 vs
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   341
        c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   342
          (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   343
            (intrs ~~ List.concat constrss);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   344
    val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   345
      (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   346
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   347
    (** realizability predicate **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   348
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   349
    val (thy3', ind_info) = thy2 |>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   350
      InductivePackage.add_inductive_i false true "" false false false
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   351
        (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   352
          ((Sign.base_name (Thm.name_of_thm intr), strip_all
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   353
            (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   354
      Theory.absolute_path;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   355
    val thy3 = PureThy.hide_thms false
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   356
      (map Thm.name_of_thm (#intrs ind_info)) thy3';
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   357
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   358
    (** realizer for induction rule **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   359
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   360
    val Ps = List.mapPartial (fn _ $ M $ P => if set_of M mem rsets then
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   361
      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
   362
        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
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
    fun add_ind_realizer (thy, Ps) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   365
      let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   366
        val r = indrule_realizer thy induct raw_induct rsets params'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   367
          (vs @ Ps) rec_names rss intrs dummies;
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   368
        val rlz = strip_all (Logic.unvarify
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   369
          (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   370
        val rews = map mk_meta_eq
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   371
          (fst_conv :: snd_conv :: get #rec_thms dt_info);
17959
8db36a108213 OldGoals;
wenzelm
parents: 17485
diff changeset
   372
        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   373
          [if length rss = 1 then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   374
             cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   375
           else EVERY [rewrite_goals_tac (rews @ all_simps),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   376
             REPEAT (rtac allI 1), rtac (#induct ind_info) 1],
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   377
           rewrite_goals_tac rews,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   378
           REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   379
             [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   380
              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
   381
        val (thm', thy') = PureThy.store_thm ((space_implode "_"
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   382
          (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   383
      in
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   384
        Extraction.add_realizers_i
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   385
          [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   386
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   387
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   388
    (** realizer for elimination rules **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   389
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   390
    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
   391
      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
   392
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   393
    fun add_elim_realizer Ps
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   394
      (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   395
      let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   396
        val (prem :: prems) = prems_of elim;
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   397
        fun reorder1 (p, intr) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   398
          Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   399
            (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   400
        fun reorder2 (intr, i) =
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   401
          let
13928
d572aeea3ff3 Fixed problem in add_elim_realizer (concerning inductive predicates with
berghofe
parents: 13921
diff changeset
   402
            val fs1 = term_vars (prop_of intr) \\ params;
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   403
            val fs2 = Term.add_vars (prop_of intr) [] \\ params'
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   404
          in Library.foldl (fn (t, x) => lambda (Var x) t)
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   405
            (list_comb (Bound (i + length fs1), fs1), fs2)
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   406
          end;
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   407
        val p = Logic.list_implies
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   408
          (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   409
        val T' = Extraction.etype_of thy (vs @ Ps) [] p;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   410
        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
   411
        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
   412
        val r = if null Ps then Extraction.nullt
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   413
          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
   414
            (if dummy then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   415
               [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))]
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   416
             else []) @
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   417
            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
   418
            [Bound (length prems)]));
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   419
        val rlz = strip_all (Logic.unvarify
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   420
          (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   421
        val rews = map mk_meta_eq case_thms;
17959
8db36a108213 OldGoals;
wenzelm
parents: 17485
diff changeset
   422
        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   423
          [cut_facts_tac [hd prems] 1,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   424
           etac elimR 1,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   425
           ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   426
           rewrite_goals_tac rews,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   427
           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   428
             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
   429
        val (thm', thy') = PureThy.store_thm ((space_implode "_"
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   430
          (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   431
      in
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   432
        Extraction.add_realizers_i
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   433
          [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   434
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   435
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   436
    (** add realizers to theory **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   437
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   438
    val rintr_thms = List.concat (map (fn (_, rs) => map (fn r => List.nth
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   439
      (#intrs ind_info, find_index_eq r intrs)) rs) rss);
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   440
    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
   441
    val thy5 = Extraction.add_realizers_i
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   442
      (map (mk_realizer thy4 vs params')
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   443
         (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   444
            map Var (rev (Term.add_vars (prop_of rule) []) \\ params')))) 
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   445
              (List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4;
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   446
    val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   447
        Option.map (rpair intrs) (find_first (fn (thm, _) =>
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   448
          s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   449
      else NONE) rss;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   450
    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
   451
      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
   452
        (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   453
           elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   454
16123
1381e90c2694 Theory.restore_naming;
wenzelm
parents: 15706
diff changeset
   455
  in Theory.restore_naming thy thy6 end;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   456
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   457
fun add_ind_realizers name rsets thy =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   458
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   459
    val (_, {intrs, induct, raw_induct, elims, ...}) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   460
      (case InductivePackage.get_inductive thy name of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   461
         NONE => error ("Unknown inductive set " ^ quote name)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   462
       | SOME info => info);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   463
    val _ $ (_ $ _ $ S) = concl_of (hd intrs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   464
    val vss = sort (int_ord o pairself length)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   465
      (subsets (map fst (relevant_vars S)))
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   466
  in
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   467
    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
   468
  end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   469
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   470
fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   471
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   472
    fun err () = error "ind_realizer: bad rule";
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   473
    val sets =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   474
      (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   475
           [_] => [set_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   476
         | xs => map (set_of o fst o HOLogic.dest_imp) xs)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   477
         handle TERM _ => err () | Empty => err ();
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   478
  in 
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   479
    add_ind_realizers (hd sets)
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   480
      (case arg of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   481
        NONE => sets | SOME NONE => []
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   482
      | SOME (SOME sets') => sets \\ sets')
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   483
  end);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   484
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   485
val ind_realizer = Attrib.syntax
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   486
 ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15574
diff changeset
   487
    Scan.option (Scan.lift (Args.colon) |--
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   488
      Scan.repeat1 Args.const))) >> rlz_attrib);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   489
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18358
diff changeset
   490
val setup =
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   491
  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
   492
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   493
end;
15706
bc264e730103 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
   494