src/HOL/Tools/inductive_realizer.ML
author blanchet
Mon, 01 Sep 2014 16:17:46 +0200
changeset 58111 82db9ad610b9
parent 56254 a2dd9200854d
child 58112 8081087096ad
permissions -rw-r--r--
tuned structure inclusion
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
    Author:     Stefan Berghofer, TU Muenchen
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     3
36043
d149c3886e7e removed dead code; fixed typo
krauss
parents: 35845
diff changeset
     4
Program extraction from proofs involving inductive predicates:
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 28965
diff changeset
     5
Realizers for induction and elimination rules.
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     6
*)
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
signature INDUCTIVE_REALIZER =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
     9
sig
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    10
  val add_ind_realizers: string -> string list -> theory -> theory
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18358
diff changeset
    11
  val setup: theory -> theory
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    12
end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    13
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    14
structure InductiveRealizer : INDUCTIVE_REALIZER =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    15
struct
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    16
22606
962f824c2df9 - Tried to make name_of_thm more robust against changes of the
berghofe
parents: 22596
diff changeset
    17
fun name_of_thm thm =
28800
48f7bfebd31d name_of_thm: Proofterm.fold_proof_atoms;
wenzelm
parents: 28328
diff changeset
    18
  (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
28814
463c9e9111ae clarified Thm.proof_body_of vs. Thm.proof_of;
wenzelm
parents: 28800
diff changeset
    19
      [Thm.proof_of thm] [] of
28800
48f7bfebd31d name_of_thm: Proofterm.fold_proof_atoms;
wenzelm
parents: 28328
diff changeset
    20
    [name] => name
55235
4b4627f5912b more explicit low-level exception;
wenzelm
parents: 54742
diff changeset
    21
  | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    22
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    23
fun prf_of thm =
44060
656ff92bad48 added Reconstruct.proof_of convenience;
wenzelm
parents: 43324
diff changeset
    24
  Reconstruct.proof_of thm
656ff92bad48 added Reconstruct.proof_of convenience;
wenzelm
parents: 43324
diff changeset
    25
  |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)];  (* FIXME *)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    26
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    27
fun subsets [] = [[]]
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    28
  | subsets (x::xs) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    29
      let val ys = subsets xs
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    30
      in ys @ map (cons x) ys end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    31
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    32
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
    33
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55958
diff changeset
    34
fun strip_all' used names (Const (@{const_name Pure.all}, _) $ Abs (s, T, t)) =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    35
      let val (s', names') = (case names of
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 42375
diff changeset
    36
          [] => (singleton (Name.variant_list used) s, [])
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    37
        | name :: names' => (name, names'))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    38
      in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55958
diff changeset
    39
  | strip_all' used names ((t as Const (@{const_name Pure.imp}, _) $ P) $ Q) =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    40
      t $ strip_all' used names Q
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    41
  | strip_all' _ _ t = t;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    42
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29271
diff changeset
    43
fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    44
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55958
diff changeset
    45
fun strip_one name
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55958
diff changeset
    46
    (Const (@{const_name Pure.all}, _) $ Abs (s, T, Const (@{const_name Pure.imp}, _) $ P $ Q)) =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    47
      (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55958
diff changeset
    48
  | strip_one _ (Const (@{const_name Pure.imp}, _) $ P $ Q) = (P, Q);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    49
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    50
fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    51
     (case strip_type T of
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
    52
        (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    53
      | _ => vs)) (Term.add_vars prop []) [];
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    54
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    55
val attach_typeS = map_types (map_atyps
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56245
diff changeset
    56
  (fn TFree (s, []) => TFree (s, @{sort type})
a2dd9200854d more antiquotations;
wenzelm
parents: 56245
diff changeset
    57
    | TVar (ixn, []) => TVar (ixn, @{sort type})
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    58
    | T => T));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    59
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    60
fun dt_of_intrs thy vs nparms intrs =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    61
  let
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    62
    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    63
    val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    64
      (Logic.strip_imp_concl (prop_of (hd intrs))));
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
    65
    val params = map dest_Var (take nparms ts);
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
    66
    val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
    67
    fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35625
diff changeset
    68
      map (Logic.unvarifyT_global o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    69
        filter_out (equal Extraction.nullT) (map
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35625
diff changeset
    70
          (Logic.unvarifyT_global o Extraction.etype_of thy vs []) (prems_of intr)),
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    71
            NoSyn);
45839
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45701
diff changeset
    72
  in
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45701
diff changeset
    73
    ((tname, map (rpair dummyS) (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs), NoSyn),
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45701
diff changeset
    74
      map constr_of_intr intrs)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    75
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    76
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    77
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
    78
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    79
(** turn "P" into "%r x. realizes r (P x)" **)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    80
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    81
fun gen_rvar vs (t as Var ((a, 0), T)) =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    82
      if body_type T <> HOLogic.boolT then t else
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    83
        let
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    84
          val U = TVar (("'" ^ a, 0), [])
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    85
          val Ts = binder_types T;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    86
          val i = length Ts;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    87
          val xs = map (pair "x") Ts;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    88
          val u = list_comb (t, map Bound (i - 1 downto 0))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    89
        in 
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
    90
          if member (op =) vs a then
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
    91
            fold_rev Term.abs (("r", U) :: xs) (mk_rlz U $ Bound i $ u)
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
    92
          else
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
    93
            fold_rev Term.abs xs (mk_rlz Extraction.nullT $ Extraction.nullt $ u)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    94
        end
13710
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
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
    97
fun mk_realizes_eqn n vs nparms intrs =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
    98
  let
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
    99
    val intr = map_types Type.strip_sorts (prop_of (hd intrs));
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   100
    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   101
    val iTs = rev (Term.add_tvars intr []);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   102
    val Tvs = map TVar iTs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   103
    val (h as Const (s, T), us) = strip_comb concl;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   104
    val params = List.take (us, nparms);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   105
    val elTs = List.drop (binder_types T, nparms);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   106
    val predT = elTs ---> HOLogic.boolT;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   107
    val used = map (fst o fst o dest_Var) params;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   108
    val xs = map (Var o apfst (rpair 0))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   109
      (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   110
    val rT = if n then Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   111
      else Type (space_implode "_" (s ^ "T" :: vs),
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   112
        map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   113
    val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   114
    val S = list_comb (h, params @ xs);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   115
    val rvs = relevant_vars S;
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 32952
diff changeset
   116
    val vs' = subtract (op =) vs (map fst rvs);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   117
    val rname = space_implode "_" (s ^ "R" :: vs);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   118
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   119
    fun mk_Tprem n v =
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   120
      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
   121
      in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   122
        Extraction.mk_typ (if n then Extraction.nullT
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   123
          else TVar (("'" ^ v, 0), [])))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   124
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   125
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   126
    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
   127
    val ts = map (gen_rvar vs) params;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   128
    val argTs = map fastype_of ts;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   129
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   130
  in ((prems, (Const ("typeof", HOLogic.boolT --> Type ("Type", [])) $ S,
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   131
       Extraction.mk_typ rT)),
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   132
    (prems, (mk_rlz rT $ r $ S,
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   133
       if n then list_comb (Const (rname, argTs ---> predT), ts @ xs)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   134
       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
   135
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   136
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   137
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
   138
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39557
diff changeset
   139
    val ctxt = Proof_Context.init_global thy
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   140
    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
   141
    val args' = map (Free o apfst fst)
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 32952
diff changeset
   142
      (subtract (op =) params (Term.add_vars (prop_of intr) []));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   143
    val rule' = strip_all rule;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   144
    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
   145
    val used = map (fst o dest_Free) args;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   146
29271
1d685baea08e moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents: 29265
diff changeset
   147
    val is_rec = exists_Const (fn (c, _) => member (op =) rsets c);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   148
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55958
diff changeset
   149
    fun is_meta (Const (@{const_name Pure.all}, _) $ Abs (s, _, P)) = is_meta P
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55958
diff changeset
   150
      | is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 33968
diff changeset
   151
      | is_meta (Const (@{const_name Trueprop}, _) $ t) =
b8c62d60195c more antiquotations;
wenzelm
parents: 33968
diff changeset
   152
          (case head_of t of
b8c62d60195c more antiquotations;
wenzelm
parents: 33968
diff changeset
   153
            Const (s, _) => can (Inductive.the_inductive ctxt) s
b8c62d60195c more antiquotations;
wenzelm
parents: 33968
diff changeset
   154
          | _ => true)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   155
      | is_meta _ = false;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   156
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   157
    fun fun_of ts rts args used (prem :: prems) =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   158
          let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   159
            val T = Extraction.etype_of thy vs [] prem;
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 19806
diff changeset
   160
            val [x, r] = Name.variant_list used ["x", "r"]
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   161
          in if T = Extraction.nullT
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   162
            then fun_of ts rts args used prems
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   163
            else if is_rec prem then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   164
              if is_meta prem then
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   165
                let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   166
                  val prem' :: prems' = prems;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   167
                  val U = Extraction.etype_of thy vs [] prem';
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   168
                in
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   169
                  if U = Extraction.nullT
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   170
                  then fun_of (Free (x, T) :: ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   171
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   172
                    (Free (x, T) :: args) (x :: r :: used) prems'
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   173
                  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
   174
                    (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
   175
                end
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   176
              else
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   177
                (case strip_type T of
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37236
diff changeset
   178
                  (Ts, Type (@{type_name Product_Type.prod}, [T1, T2])) =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   179
                    let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   180
                      val fx = Free (x, Ts ---> T1);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   181
                      val fr = Free (r, Ts ---> T2);
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   182
                      val bs = map Bound (length Ts - 1 downto 0);
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   183
                      val t =
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   184
                        fold_rev (Term.abs o pair "z") Ts
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   185
                          (HOLogic.mk_prod (list_comb (fx, bs), list_comb (fr, bs)));
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   186
                    in fun_of (fx :: ts) (fr :: rts) (t::args) (x :: r :: used) prems end
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   187
                | (Ts, U) => fun_of (Free (x, T) :: ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   188
                    (Free (r, binder_types T ---> HOLogic.unitT) :: rts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   189
                    (Free (x, T) :: args) (x :: r :: used) prems)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   190
            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
   191
              (x :: used) prems
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   192
          end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   193
      | fun_of ts rts args used [] =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   194
          let val xs = rev (rts @ ts)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   195
          in if conclT = Extraction.nullT
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   196
            then fold_rev (absfree o dest_Free) xs HOLogic.unit
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   197
            else fold_rev (absfree o dest_Free) xs
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   198
              (list_comb
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   199
                (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   200
                  map fastype_of (rev args) ---> conclT), rev args))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   201
          end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   202
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   203
  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
   204
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   205
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
   206
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   207
    val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
31986
a68f88d264f7 dropped find_index_eq
haftmann
parents: 31784
diff changeset
   208
    val premss = map_filter (fn (s, rs) => if member (op =) rsets s then
a68f88d264f7 dropped find_index_eq
haftmann
parents: 31784
diff changeset
   209
      SOME (rs, map (fn (_, r) => nth (prems_of raw_induct)
a68f88d264f7 dropped find_index_eq
haftmann
parents: 31784
diff changeset
   210
        (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   211
    val fs = maps (fn ((intrs, prems), dummy) =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   212
      let
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   213
        val fs = map (fn (rule, (ivs, intr)) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   214
          fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 33968
diff changeset
   215
      in
b8c62d60195c more antiquotations;
wenzelm
parents: 33968
diff changeset
   216
        if dummy then Const (@{const_name default},
b8c62d60195c more antiquotations;
wenzelm
parents: 33968
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;
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   222
    fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr)
22271
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
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   230
        in
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   231
          (fold_rev absfree (("x", U) :: map_filter (fn intr =>
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   232
            Option.map (pair (name_of_fn intr))
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   233
              (AList.lookup (op =) frees (name_of_fn intr))) intrs)
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 44060
diff changeset
   234
            (list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   235
        end
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   236
      end) concls rec_names)
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   237
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   238
45839
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45701
diff changeset
   239
fun add_dummy name dname (x as (_, ((s, vs, mx), cs))) =
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45701
diff changeset
   240
  if Binding.eq_name (name, s)
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45701
diff changeset
   241
  then (true, ((s, vs, mx), (dname, [HOLogic.unitT], NoSyn) :: cs))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   242
  else x;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   243
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   244
fun add_dummies f [] _ thy =
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   245
      (([], NONE), thy)
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   246
  | add_dummies f dts used thy =
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   247
      thy
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   248
      |> f (map snd dts)
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   249
      |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
33968
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33957
diff changeset
   250
    handle Datatype_Aux.Datatype_Empty name' =>
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   251
      let
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   252
        val name = Long_Name.base_name name';
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 42375
diff changeset
   253
        val dname = singleton (Name.variant_list used) "Dummy";
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   254
      in
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   255
        thy
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   256
        |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
14888
99ac3eb0f84e add_dummies no longer uses transform_error but handles specific
berghofe
parents: 13928
diff changeset
   257
      end;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   258
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   259
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
   260
  let
13725
12404b452034 Changed format of realizers / correctness proofs.
berghofe
parents: 13710
diff changeset
   261
    val rvs = map fst (relevant_vars (prop_of rule));
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   262
    val xs = rev (Term.add_vars (prop_of rule) []);
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   263
    val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16123
diff changeset
   264
    val rlzvs = rev (Term.add_vars (prop_of rrule) []);
17485
c39871c52977 introduced AList module
haftmann
parents: 17325
diff changeset
   265
    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
   266
    val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   267
    val rlz' = fold_rev Logic.all rs (prop_of rrule)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   268
  in (name, (vs,
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33244
diff changeset
   269
    if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   270
    Extraction.abs_corr_shyps thy rule vs vs2
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   271
      (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   272
         (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   273
  end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   274
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   275
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
   276
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   277
fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   278
  let
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   279
    val qualifier = Long_Name.qualifier (name_of_thm induct);
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 37678
diff changeset
   280
    val inducts = Global_Theory.get_thms thy (Long_Name.qualify qualifier "inducts");
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   281
    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   282
    val ar = length vs + length iTs;
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31668
diff changeset
   283
    val params = Inductive.params_of raw_induct;
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31668
diff changeset
   284
    val arities = Inductive.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;
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31668
diff changeset
   287
    val rss = Inductive.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) =>
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31668
diff changeset
   289
      (s, (Inductive.infer_intro_vars elim arity rs ~~ rs)))
22790
e1cff9268177 Moved functions infer_intro_vars, arities_of, params_of, and
berghofe
parents: 22606
diff changeset
   290
        (rss ~~ arities ~~ elims);
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   291
    val (prfx, _) = split_last (Long_Name.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 |>
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   296
      Sign.add_path (Long_Name.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
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   298
      (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) 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 |>
42375
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42361
diff changeset
   301
      Sign.add_types_global
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42361
diff changeset
   302
        (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
774df7c59508 report Name_Space.declare/define, relatively to context;
wenzelm
parents: 42361
diff changeset
   303
      Extraction.add_typeof_eqns_i ty_eqs;
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   304
    val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   305
      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
   306
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   307
    (** datatype representing computational content of inductive set **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   308
31783
cfbe9609ceb1 add_datatypes does not yield particular rules any longer
haftmann
parents: 31781
diff changeset
   309
    val ((dummies, some_dt_names), thy2) =
18008
f193815cab2c swapped add_datatype result
haftmann
parents: 17959
diff changeset
   310
      thy1
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 44241
diff changeset
   311
      |> add_dummies (Datatype.add_datatype {strict = false, quiet = false})
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 44241
diff changeset
   312
        (map (pair false) dts) []
18314
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   313
      ||> Extraction.add_typeof_eqns_i ty_eqs
4595eb4627fa oriented pairs theory * 'a to 'a * theory
haftmann
parents: 18008
diff changeset
   314
      ||> Extraction.add_realizes_eqns_i rlz_eqs;
31783
cfbe9609ceb1 add_datatypes does not yield particular rules any longer
haftmann
parents: 31781
diff changeset
   315
    val dt_names = these some_dt_names;
58111
82db9ad610b9 tuned structure inclusion
blanchet
parents: 56254
diff changeset
   316
    val case_thms = map (#case_rewrites o Datatype_Data.the_info thy2) dt_names;
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 44241
diff changeset
   317
    val rec_thms =
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 44241
diff changeset
   318
      if null dt_names then []
58111
82db9ad610b9 tuned structure inclusion
blanchet
parents: 56254
diff changeset
   319
      else #rec_rewrites (Datatype_Data.the_info thy2 (hd dt_names));
19046
bc5c6c9b114e removed distinct, renamed gen_distinct to distinct;
wenzelm
parents: 18929
diff changeset
   320
    val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
31781
861e675f01e6 add_datatype interface yields type names and less rules
haftmann
parents: 31723
diff changeset
   321
      HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
31458
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 31177
diff changeset
   322
    val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 31177
diff changeset
   323
      if member (op =) rsets s then
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   324
        let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   325
          val (d :: dummies') = dummies;
19473
wenzelm
parents: 19046
diff changeset
   326
          val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
31458
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 31177
diff changeset
   327
        in (map (head_of o hd o rev o snd o strip_comb o fst o
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 31177
diff changeset
   328
          HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   329
        end
31458
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 31177
diff changeset
   330
      else (replicate (length rs) Extraction.nullt, (recs, dummies)))
31781
861e675f01e6 add_datatype interface yields type names and less rules
haftmann
parents: 31723
diff changeset
   331
        rss (rec_thms, dummies);
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   332
    val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   333
      (Extraction.realizes_of thy2 vs
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   334
        (if c = Extraction.nullt then c else list_comb (c, map Var (rev
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   335
          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32131
diff changeset
   336
            (maps snd rss ~~ flat constrss);
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   337
    val (rlzpreds, rlzpreds') =
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   338
      rintrs |> map (fn rintr =>
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   339
        let
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   340
          val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   341
          val s' = Long_Name.base_name s;
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35625
diff changeset
   342
          val T' = Logic.unvarifyT_global T;
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   343
        in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   344
      |> distinct (op = o pairself (#1 o #1))
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   345
      |> map (apfst (apfst (apfst Binding.name)))
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   346
      |> split_list;
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   347
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35625
diff changeset
   348
    val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT_global T))
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   349
      (List.take (snd (strip_comb
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   350
        (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
   351
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   352
    (** realizability predicate **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   353
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   354
    val (ind_info, thy3') = thy2 |>
33726
0878aecbf119 eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents: 33671
diff changeset
   355
      Inductive.add_inductive_global
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33666
diff changeset
   356
        {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
49170
03bee3a6a1b7 discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents: 47060
diff changeset
   357
          no_elim = false, no_ind = false, skip_mono = false}
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   358
        rlzpreds rlzparams (map (fn (rintr, intr) =>
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   359
          ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35625
diff changeset
   360
           subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   361
             (rintrs ~~ maps snd rss)) [] ||>
30435
e62d6ecab6ad explicit Binding.qualified_name -- prevents implicitly qualified bstring;
wenzelm
parents: 30364
diff changeset
   362
      Sign.root_path;
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 37678
diff changeset
   363
    val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   364
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   365
    (** realizer for induction rule **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   366
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   367
    val Ps = map_filter (fn _ $ M $ P => if member (op =) rsets (pred_of M) then
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   368
      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
   369
        (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   370
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   371
    fun add_ind_realizer Ps thy =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   372
      let
24157
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   373
        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
   374
          (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   375
            (hd (prems_of (hd inducts))))), nparms))) vs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   376
        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
   377
          (vs' @ Ps) rec_names rss' intrs dummies;
409cd6eaa7ea Added renaming function to prevent correctness proof for realizer
berghofe
parents: 23590
diff changeset
   378
        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
   379
          (prop_of ind)) (rs ~~ inducts);
29281
b22ccb3998db eliminated OldTerm.add_term_free_names;
wenzelm
parents: 29271
diff changeset
   380
        val used = fold Term.add_free_names rlzs [];
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   381
        val rnames = Name.variant_list used (replicate (length inducts) "r");
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   382
        val rnames' = Name.variant_list
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   383
          (used @ rnames) (replicate (length intrs) "s");
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   384
        val rlzs' as (prems, _, _) :: _ = map (fn (rlz, name) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   385
          let
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35625
diff changeset
   386
            val (P, Q) = strip_one name (Logic.unvarify_global rlz);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   387
            val Q' = strip_all' [] rnames' Q
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   388
          in
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   389
            (Logic.strip_imp_prems Q', P, Logic.strip_imp_concl Q')
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   390
          end) (rlzs ~~ rnames);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   391
        val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   392
          (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
37136
e0c9d3e49e15 dropped legacy theorem bindings
haftmann
parents: 36945
diff changeset
   393
        val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   394
        val thm = Goal.prove_global thy []
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   395
          (map attach_typeS prems) (attach_typeS concl)
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52788
diff changeset
   396
          (fn {context = ctxt, prems} => EVERY
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   397
          [rtac (#raw_induct ind_info) 1,
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52788
diff changeset
   398
           rewrite_goals_tac ctxt rews,
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   399
           REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52788
diff changeset
   400
             [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   401
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 37678
diff changeset
   402
        val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   403
          (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   404
        val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
33968
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33957
diff changeset
   405
          (Datatype_Aux.split_conj_thm thm');
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 37678
diff changeset
   406
        val ([thms'], thy'') = Global_Theory.add_thmss
30435
e62d6ecab6ad explicit Binding.qualified_name -- prevents implicitly qualified bstring;
wenzelm
parents: 30364
diff changeset
   407
          [((Binding.qualified_name (space_implode "_"
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   408
             (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29389
diff changeset
   409
               ["correctness"])), thms), [])] thy';
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   410
        val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   411
      in
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   412
        Extraction.add_realizers_i
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   413
          (map (fn (((ind, corr), rlz), r) =>
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   414
              mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   415
            realizers @ (case realizers of
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   416
             [(((ind, corr), rlz), r)] =>
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   417
               [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   418
                  ind, corr, rlz, r)]
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   419
           | _ => [])) thy''
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   420
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   421
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   422
    (** realizer for elimination rules **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   423
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   424
    val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o
31781
861e675f01e6 add_datatype interface yields type names and less rules
haftmann
parents: 31723
diff changeset
   425
      HOLogic.dest_Trueprop o prop_of o hd) case_thms;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   426
13921
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   427
    fun add_elim_realizer Ps
69c627b6b28d Fixed problem in add_elim_realizer which caused bound variables to
berghofe
parents: 13725
diff changeset
   428
      (((((elim, elimR), intrs), case_thms), case_name), dummy) thy =
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   429
      let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   430
        val (prem :: prems) = prems_of elim;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   431
        fun reorder1 (p, (_, intr)) =
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   432
          fold (fn ((s, _), T) => Logic.all (Free (s, T)))
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   433
            (subtract (op =) params' (Term.add_vars (prop_of intr) []))
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   434
            (strip_all p);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   435
        fun reorder2 ((ivs, intr), i) =
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 32952
diff changeset
   436
          let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) [])
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   437
          in fold (lambda o Var) fs (list_comb (Bound (i + length ivs), ivs)) end;
13921
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);
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   443
        val r =
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   444
          if null Ps then Extraction.nullt
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   445
          else
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   446
            fold_rev (Term.abs o pair "x") Ts
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   447
              (list_comb (Const (case_name, T),
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   448
                (if dummy then
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   449
                   [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   450
                 else []) @
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   451
                map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 45839
diff changeset
   452
                [Bound (length prems)]));
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   453
        val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   454
        val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   455
        val rews = map mk_meta_eq case_thms;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   456
        val thm = Goal.prove_global thy []
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49170
diff changeset
   457
          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz')
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49170
diff changeset
   458
          (fn {context = ctxt, prems, ...} => EVERY
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49170
diff changeset
   459
            [cut_tac (hd prems) 1,
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49170
diff changeset
   460
             etac elimR 1,
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49170
diff changeset
   461
             ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52788
diff changeset
   462
             rewrite_goals_tac ctxt rews,
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52788
diff changeset
   463
             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49170
diff changeset
   464
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 37678
diff changeset
   465
        val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29389
diff changeset
   466
          (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   467
      in
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   468
        Extraction.add_realizers_i
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   469
          [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
   470
      end;
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   471
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   472
    (** add realizers to theory **)
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   473
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   474
    val thy4 = fold add_ind_realizer (subsets Ps) thy3;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   475
    val thy5 = Extraction.add_realizers_i
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   476
      (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   477
         (name_of_thm rule, rule, rrule, rlz,
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 32952
diff changeset
   478
            list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) []))))))
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32131
diff changeset
   479
              (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32131
diff changeset
   480
    val elimps = map_filter (fn ((s, intrs), p) =>
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   481
      if member (op =) rsets s then SOME (p, intrs) else NONE)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   482
        (rss' ~~ (elims ~~ #elims ind_info));
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   483
    val thy6 =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   484
      fold (fn p as (((((elim, _), _), _), _), _) =>
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   485
        add_elim_realizer [] p #>
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   486
        add_elim_realizer [fst (fst (dest_Var (HOLogic.dest_Trueprop (concl_of elim))))] p)
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   487
      (elimps ~~ case_thms ~~ case_names ~~ dummies) thy5;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   488
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24157
diff changeset
   489
  in Sign.restore_naming thy thy6 end;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   490
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   491
fun add_ind_realizers name rsets thy =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   492
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   493
    val (_, {intrs, induct, raw_induct, elims, ...}) =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39557
diff changeset
   494
      Inductive.the_inductive (Proof_Context.init_global thy) name;
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   495
    val vss = sort (int_ord o pairself length)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   496
      (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   497
  in
37233
b78f31ca4675 Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents: 36945
diff changeset
   498
    fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   499
  end
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   500
20897
3f8d2834b2c4 attribute: Context.mapping;
wenzelm
parents: 20071
diff changeset
   501
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
   502
  let
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   503
    fun err () = error "ind_realizer: bad rule";
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   504
    val sets =
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   505
      (case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   506
           [_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21858
diff changeset
   507
         | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
47060
e2741ec9ae36 prefer explicitly qualified exception List.Empty;
wenzelm
parents: 46708
diff changeset
   508
         handle TERM _ => err () | List.Empty => err ();
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   509
  in 
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   510
    add_ind_realizers (hd sets)
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   511
      (case arg of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
   512
        NONE => sets | SOME NONE => []
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 32952
diff changeset
   513
      | SOME (SOME sets') => subtract (op =) sets' sets)
20897
3f8d2834b2c4 attribute: Context.mapping;
wenzelm
parents: 20071
diff changeset
   514
  end I);
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   515
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18358
diff changeset
   516
val setup =
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30528
diff changeset
   517
  Attrib.setup @{binding ind_realizer}
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30528
diff changeset
   518
    ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
55954
a29aefc88c8d more uniform check_const/read_const;
wenzelm
parents: 55235
diff changeset
   519
      Scan.option (Scan.lift (Args.colon) |--
55958
4ec984df4f45 more rigid const demands, based on educated guesses about the tools involved here;
wenzelm
parents: 55954
diff changeset
   520
        Scan.repeat1 (Args.const {proper = true, strict = true})))) >> rlz_attrib)
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30528
diff changeset
   521
    "add realizers for inductive set";
13710
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   522
75bec2c1bfd5 New package for constructing realizers for introduction and elimination
berghofe
parents:
diff changeset
   523
end;
15706
bc264e730103 *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
   524