src/HOL/Nominal/nominal_datatype.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46961 5c6955f487e5
child 49170 03bee3a6a1b7
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31936
9466169dc8e0 nominal.ML is nominal_datatype.ML
haftmann
parents: 31784
diff changeset
     1
(*  Title:      HOL/Nominal/nominal_datatype.ML
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
     2
    Author:     Stefan Berghofer and Christian Urban, TU Muenchen
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
     3
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
     4
Nominal datatype package for Isabelle/HOL.
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
     5
*)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     6
31936
9466169dc8e0 nominal.ML is nominal_datatype.ML
haftmann
parents: 31784
diff changeset
     7
signature NOMINAL_DATATYPE =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     8
sig
45863
afdb92130f5a tuned signature;
wenzelm
parents: 45839
diff changeset
     9
  val nominal_datatype : Datatype.config -> Datatype.spec list -> theory -> theory
afdb92130f5a tuned signature;
wenzelm
parents: 45839
diff changeset
    10
  val nominal_datatype_cmd : Datatype.config -> Datatype.spec_cmd list -> theory -> theory
22433
400fa18e951f - Changed format of descriptor contained in nominal_datatype_info
berghofe
parents: 22311
diff changeset
    11
  type descr
21540
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    12
  type nominal_datatype_info
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    13
  val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    14
  val get_nominal_datatype : theory -> string -> nominal_datatype_info option
22311
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
    15
  val mk_perm: typ list -> term -> term -> term
22529
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
    16
  val perm_of_pair: term * term -> term
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
    17
  val mk_not_sym: thm list -> thm list
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
    18
  val perm_simproc: simproc
25823
5d75f4b179e2 Added function fresh_const.
berghofe
parents: 25674
diff changeset
    19
  val fresh_const: typ -> typ -> term
28373
5e2c526cfaf0 Added fresh_star_const.
berghofe
parents: 28084
diff changeset
    20
  val fresh_star_const: typ -> typ -> term
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    21
end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    22
31936
9466169dc8e0 nominal.ML is nominal_datatype.ML
haftmann
parents: 31784
diff changeset
    23
structure NominalDatatype : NOMINAL_DATATYPE =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    24
struct
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    25
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    26
val finite_emptyI = @{thm finite.emptyI};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    27
val finite_Diff = @{thm finite_Diff};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    28
val finite_Un = @{thm finite_Un};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    29
val Un_iff = @{thm Un_iff};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    30
val In0_eq = @{thm In0_eq};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    31
val In1_eq = @{thm In1_eq};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    32
val In0_not_In1 = @{thm In0_not_In1};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    33
val In1_not_In0 = @{thm In1_not_In0};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    34
val Un_assoc = @{thm Un_assoc};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    35
val Collect_disj_eq = @{thm Collect_disj_eq};
32129
d2aea34845d4 explicit antiquotation
haftmann
parents: 32124
diff changeset
    36
val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]};
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    37
val empty_iff = @{thm empty_iff};
21669
c68717c16013 removed legacy ML bindings;
wenzelm
parents: 21540
diff changeset
    38
18068
e8c3d371594e Moved atom stuff to new file nominal_atoms.ML
berghofe
parents: 18067
diff changeset
    39
open NominalAtoms;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    40
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
    41
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22812
diff changeset
    42
(* theory data *)
21540
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    43
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
    44
type descr =
45896
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
    45
  (int * (string * Datatype.dtyp list *
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
    46
      (string * (Datatype.dtyp list * Datatype.dtyp) list) list)) list;
22433
400fa18e951f - Changed format of descriptor contained in nominal_datatype_info
berghofe
parents: 22311
diff changeset
    47
21540
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    48
type nominal_datatype_info =
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    49
  {index : int,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    50
   descr : descr,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    51
   rec_names : string list,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    52
   rec_rewrites : thm list,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    53
   induction : thm,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    54
   distinct : thm list,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    55
   inject : thm list};
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    56
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33368
diff changeset
    57
structure NominalDatatypesData = Theory_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22812
diff changeset
    58
(
21540
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    59
  type T = nominal_datatype_info Symtab.table;
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    60
  val empty = Symtab.empty;
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    61
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33368
diff changeset
    62
  fun merge data = Symtab.merge (K true) data;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22812
diff changeset
    63
);
21540
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    64
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    65
val get_nominal_datatypes = NominalDatatypesData.get;
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    66
val put_nominal_datatypes = NominalDatatypesData.put;
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    67
val map_nominal_datatypes = NominalDatatypesData.map;
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    68
val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22812
diff changeset
    69
21540
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    70
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    71
(**** make datatype info ****)
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    72
45822
843dc212f69e datatype dtyp with explicit sort information;
wenzelm
parents: 45741
diff changeset
    73
fun make_dt_info descr induct reccomb_names rec_thms
33063
4d462963a7db map_range (and map_index) combinator
haftmann
parents: 33040
diff changeset
    74
    (i, (((_, (tname, _, _)), distinct), inject)) =
21540
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    75
  (tname,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    76
   {index = i,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    77
    descr = descr,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    78
    rec_names = reccomb_names,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    79
    rec_rewrites = rec_thms,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    80
    induction = induct,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    81
    distinct = distinct,
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    82
    inject = inject});
f3faed8276e6 Additional information about nominal datatypes (descriptor,
berghofe
parents: 21516
diff changeset
    83
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
    84
(*******************************)
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
    85
45909
6fe61da4c467 tuned signature;
wenzelm
parents: 45906
diff changeset
    86
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of Datatype.distinct_lemma);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    87
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    88
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
    89
(** simplification procedure for sorting permutations **)
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
    90
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
    91
val dj_cp = @{thm dj_cp};
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
    92
37677
c5a8b612e571 qualified constants Set.member and Set.Collect
haftmann
parents: 37391
diff changeset
    93
fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
    94
      Type ("fun", [_, U])])) = (T, U);
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
    95
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
    96
fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
    97
  | permTs_of _ = [];
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
    98
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
    99
fun perm_simproc' thy ss (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   100
      let
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   101
        val (aT as Type (a, []), S) = dest_permT T;
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   102
        val (bT as Type (b, []), _) = dest_permT U
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
   103
      in if member (op =) (permTs_of u) aT andalso aT <> bT then
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   104
          let
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   105
            val cp = cp_inst_of thy a b;
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   106
            val dj = dj_thm_of thy b a;
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   107
            val dj_cp' = [cp, dj] MRS dj_cp;
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   108
            val cert = SOME o cterm_of thy
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   109
          in
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   110
            SOME (mk_meta_eq (Drule.instantiate' [SOME (ctyp_of thy S)]
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   111
              [cert t, cert r, cert s] dj_cp'))
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   112
          end
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   113
        else NONE
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   114
      end
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   115
  | perm_simproc' thy ss _ = NONE;
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   116
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   117
val perm_simproc =
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 38558
diff changeset
   118
  Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
   119
18582
4f4cc426b440 provide projections of induct_weak, induct_unsafe;
wenzelm
parents: 18579
diff changeset
   120
fun projections rule =
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41489
diff changeset
   121
  Project_Rule.projections (Proof_Context.init_global (Thm.theory_of_thm rule)) rule
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33968
diff changeset
   122
  |> map (Drule.export_without_context #> Rule_Cases.save rule);
18582
4f4cc426b440 provide projections of induct_weak, induct_unsafe;
wenzelm
parents: 18579
diff changeset
   123
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
   124
val supp_prod = @{thm supp_prod};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
   125
val fresh_prod = @{thm fresh_prod};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
   126
val supports_fresh = @{thm supports_fresh};
44685
f5bc7d9d0d74 assert Pure equations for theorem references; avoid dynamic reference to fact
haftmann
parents: 44241
diff changeset
   127
val supports_def = Simpdata.mk_eq @{thm Nominal.supports_def};
f5bc7d9d0d74 assert Pure equations for theorem references; avoid dynamic reference to fact
haftmann
parents: 44241
diff changeset
   128
val fresh_def = Simpdata.mk_eq @{thm fresh_def};
f5bc7d9d0d74 assert Pure equations for theorem references; avoid dynamic reference to fact
haftmann
parents: 44241
diff changeset
   129
val supp_def = Simpdata.mk_eq @{thm supp_def};
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
   130
val rev_simps = @{thms rev.simps};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
   131
val app_simps = @{thms append.simps};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
   132
val at_fin_set_supp = @{thm at_fin_set_supp};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
   133
val at_fin_set_fresh = @{thm at_fin_set_fresh};
0dec18004e75 more antiquotations;
wenzelm
parents: 38864
diff changeset
   134
val abs_fun_eq1 = @{thm abs_fun_eq1};
20267
1154363129be Additional freshness constraints for FCB.
berghofe
parents: 20179
diff changeset
   135
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   136
val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   137
22311
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
   138
fun mk_perm Ts t u =
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
   139
  let
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
   140
    val T = fastype_of1 (Ts, t);
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
   141
    val U = fastype_of1 (Ts, u)
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
   142
  in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
   143
22529
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   144
fun perm_of_pair (x, y) =
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   145
  let
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   146
    val T = fastype_of x;
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   147
    val pT = mk_permT T
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   148
  in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   149
    HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   150
  end;
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   151
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   152
fun mk_not_sym ths = maps (fn th => case prop_of th of
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
   153
    _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
22529
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   154
  | _ => [th]) ths;
902ed60d53a7 Exported perm_of_pair, mk_not_sym, and perm_simproc.
berghofe
parents: 22433
diff changeset
   155
25823
5d75f4b179e2 Added function fresh_const.
berghofe
parents: 25674
diff changeset
   156
fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
28373
5e2c526cfaf0 Added fresh_star_const.
berghofe
parents: 28084
diff changeset
   157
fun fresh_star_const T U =
5e2c526cfaf0 Added fresh_star_const.
berghofe
parents: 28084
diff changeset
   158
  Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
25823
5d75f4b179e2 Added function fresh_const.
berghofe
parents: 25674
diff changeset
   159
45863
afdb92130f5a tuned signature;
wenzelm
parents: 45839
diff changeset
   160
fun gen_nominal_datatype prep_specs config dts thy =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   161
  let
45839
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   162
    val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts;
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   163
45839
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   164
    val (dts', _) = prep_specs dts thy;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   165
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   166
    val atoms = atoms_of thy;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   167
45839
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   168
    val tyvars = map (fn ((_, tvs, _), _) => tvs) dts';
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   169
    val sorts = flat tyvars;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   170
42388
a44b0fdaa6c2 standardized aliases of operations on tsig;
wenzelm
parents: 42375
diff changeset
   171
    fun inter_sort thy S S' = Sign.inter_sort thy (S, S');
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   172
    fun augment_sort_typ thy S =
36428
874843c1e96e really minimize sorts after certification -- looks like this is intended here;
wenzelm
parents: 35994
diff changeset
   173
      let val S = Sign.minimize_sort thy (Sign.certify_sort thy S)
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   174
      in map_type_tfree (fn (s, S') => TFree (s,
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   175
        if member (op = o apsnd fst) sorts s then inter_sort thy S S' else S'))
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   176
      end;
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   177
    fun augment_sort thy S = map_types (augment_sort_typ thy S);
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   178
45839
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   179
    val types_syntax = map (fn ((tname, tvs, mx), constrs) => (tname, mx)) dts';
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   180
    val constr_syntax = map (fn (_, constrs) =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   181
      map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   182
45839
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   183
    val ps = map (fn ((n, _, _), _) =>
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   184
      (Sign.full_name thy n, Sign.full_name thy (Binding.suffix_name "_Rep" n))) dts;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   185
    val rps = map Library.swap ps;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   186
21365
4ee8e2702241 InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents: 21291
diff changeset
   187
    fun replace_types (Type ("Nominal.ABS", [T, U])) =
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   188
          Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   189
      | replace_types (Type (s, Ts)) =
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32960
diff changeset
   190
          Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   191
      | replace_types T = T;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   192
45839
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   193
    val dts'' = map (fn ((tname, tvs, mx), constrs) =>
43a5b86bc102 'datatype' specifications allow explicit sort constraints;
wenzelm
parents: 45838
diff changeset
   194
      ((Binding.suffix_name "_Rep" tname, tvs, NoSyn),
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   195
        map (fn (cname, cargs, mx) => (Binding.suffix_name "_Rep" cname,
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   196
          map replace_types cargs, NoSyn)) constrs)) dts';
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   197
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   198
    val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   199
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   200
    val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   201
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   202
    val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
45896
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
   203
    fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype.DtRec i);
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
   204
26651
e630c789ef2b overloading perm: use big_name;
wenzelm
parents: 26646
diff changeset
   205
    val big_name = space_implode "_" new_type_names;
e630c789ef2b overloading perm: use big_name;
wenzelm
parents: 26646
diff changeset
   206
e630c789ef2b overloading perm: use big_name;
wenzelm
parents: 26646
diff changeset
   207
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   208
    (**** define permutation functions ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   209
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   210
    val permT = mk_permT (TFree ("'x", HOLogic.typeS));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   211
    val pi = Free ("pi", permT);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   212
    val perm_types = map (fn (i, _) =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   213
      let val T = nth_dtyp i
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   214
      in permT --> T --> T end) descr;
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
   215
    val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   216
      "perm_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   217
    val perm_names = replicate (length new_type_names) "Nominal.perm" @
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28736
diff changeset
   218
      map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   219
    val perm_names_types = perm_names ~~ perm_types;
26680
18ff77116937 Adapted to new primrec package.
berghofe
parents: 26663
diff changeset
   220
    val perm_names_types' = perm_names' ~~ perm_types;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   221
26680
18ff77116937 Adapted to new primrec package.
berghofe
parents: 26663
diff changeset
   222
    val perm_eqs = maps (fn (i, (_, _, constrs)) =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   223
      let val T = nth_dtyp i
21365
4ee8e2702241 InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents: 21291
diff changeset
   224
      in map (fn (cname, dts) =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   225
        let
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   226
          val Ts = map (Datatype_Aux.typ_of_dtyp descr) dts;
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
   227
          val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   228
          val args = map Free (names ~~ Ts);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   229
          val c = Const (cname, Ts ---> T);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   230
          fun perm_arg (dt, x) =
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   231
            let val T = type_of x
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   232
            in if Datatype_Aux.is_rec_type dt then
40844
5895c525739d more direct use of binder_types/body_type;
wenzelm
parents: 40627
diff changeset
   233
                let val Us = binder_types T
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   234
                in
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   235
                  fold_rev (Term.abs o pair "x") Us
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   236
                    (Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   237
                      list_comb (x, map (fn (i, U) =>
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   238
                        Const ("Nominal.perm", permT --> U --> U) $
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   239
                          (Const ("List.rev", permT --> permT) $ pi) $
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 46218
diff changeset
   240
                          Bound i) ((length Us - 1 downto 0) ~~ Us)))
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   241
                end
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   242
              else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
21365
4ee8e2702241 InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents: 21291
diff changeset
   243
            end;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   244
        in
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28736
diff changeset
   245
          (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
26680
18ff77116937 Adapted to new primrec package.
berghofe
parents: 26663
diff changeset
   246
            (Free (nth perm_names_types' i) $
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   247
               Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   248
               list_comb (c, args),
26680
18ff77116937 Adapted to new primrec package.
berghofe
parents: 26663
diff changeset
   249
             list_comb (c, map perm_arg (dts ~~ args)))))
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   250
        end) constrs
26680
18ff77116937 Adapted to new primrec package.
berghofe
parents: 26663
diff changeset
   251
      end) descr;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   252
26689
105031879f4a Auxiliary permutation functions are no longer declared using add_consts_i,
berghofe
parents: 26680
diff changeset
   253
    val (perm_simps, thy2) =
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31671
diff changeset
   254
      Primrec.add_primrec_overloaded
26689
105031879f4a Auxiliary permutation functions are no longer declared using add_consts_i,
berghofe
parents: 26680
diff changeset
   255
        (map (fn (s, sT) => (s, sT, false))
105031879f4a Auxiliary permutation functions are no longer declared using add_consts_i,
berghofe
parents: 26680
diff changeset
   256
           (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28736
diff changeset
   257
        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   258
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   259
    (**** prove that permutation functions introduced by unfolding are ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   260
    (**** equivalent to already existing permutation functions         ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   261
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   262
    val _ = warning ("length descr: " ^ string_of_int (length descr));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   263
    val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   264
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
   265
    val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
44685
f5bc7d9d0d74 assert Pure equations for theorem references; avoid dynamic reference to fact
haftmann
parents: 44241
diff changeset
   266
    val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def};
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   267
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   268
    val unfolded_perm_eq_thms =
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   269
      if length descr = length new_type_names then []
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   270
      else map Drule.export_without_context (List.drop (Datatype_Aux.split_conj_thm
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   271
        (Goal.prove_global thy2 [] []
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   272
          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   273
            (map (fn (c as (s, T), x) =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   274
               let val [T1, T2] = binder_types T
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   275
               in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   276
                 Const ("Nominal.perm", T) $ pi $ Free (x, T2))
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   277
               end)
18010
c885c93a9324 Removed legacy prove_goalw_cterm command.
berghofe
parents: 17874
diff changeset
   278
             (perm_names_types ~~ perm_indnames))))
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
   279
          (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   280
            ALLGOALS (asm_full_simp_tac
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   281
              (global_simpset_of thy2 addsimps [perm_fun_def]))])),
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   282
        length new_type_names));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   283
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   284
    (**** prove [] \<bullet> t = t ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   285
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   286
    val _ = warning "perm_empty_thms";
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   287
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   288
    val perm_empty_thms = maps (fn a =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   289
      let val permT = mk_permT (Type (a, []))
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   290
      in map Drule.export_without_context (List.take (Datatype_Aux.split_conj_thm
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   291
        (Goal.prove_global thy2 [] []
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   292
          (augment_sort thy2 [pt_class_of thy2 a]
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   293
            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   294
              (map (fn ((s, T), x) => HOLogic.mk_eq
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   295
                  (Const (s, permT --> T --> T) $
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   296
                     Const ("List.list.Nil", permT) $ Free (x, T),
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   297
                   Free (x, T)))
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   298
               (perm_names ~~
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   299
                map body_type perm_types ~~ perm_indnames)))))
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
   300
          (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   301
            ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])),
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   302
        length new_type_names))
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   303
      end)
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   304
      atoms;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   305
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   306
    (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   307
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   308
    val _ = warning "perm_append_thms";
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   309
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   310
    (*FIXME: these should be looked up statically*)
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   311
    val at_pt_inst = Global_Theory.get_thm thy2 "at_pt_inst";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   312
    val pt2 = Global_Theory.get_thm thy2 "pt2";
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   313
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   314
    val perm_append_thms = maps (fn a =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   315
      let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   316
        val permT = mk_permT (Type (a, []));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   317
        val pi1 = Free ("pi1", permT);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   318
        val pi2 = Free ("pi2", permT);
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   319
        val pt_inst = pt_inst_of thy2 a;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   320
        val pt2' = pt_inst RS pt2;
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   321
        val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   322
      in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   323
        (Goal.prove_global thy2 [] []
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   324
           (augment_sort thy2 [pt_class_of thy2 a]
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   325
             (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   326
                (map (fn ((s, T), x) =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   327
                    let val perm = Const (s, permT --> T --> T)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   328
                    in HOLogic.mk_eq
23029
79ee75dc1e59 constant op @ now named append
haftmann
parents: 22846
diff changeset
   329
                      (perm $ (Const ("List.append", permT --> permT --> permT) $
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   330
                         pi1 $ pi2) $ Free (x, T),
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   331
                       perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   332
                    end)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   333
                  (perm_names ~~
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   334
                   map body_type perm_types ~~ perm_indnames)))))
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
   335
           (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   336
              ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   337
         length new_type_names)
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   338
      end) atoms;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   339
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   340
    (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   341
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   342
    val _ = warning "perm_eq_thms";
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   343
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   344
    val pt3 = Global_Theory.get_thm thy2 "pt3";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   345
    val pt3_rev = Global_Theory.get_thm thy2 "pt3_rev";
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   346
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   347
    val perm_eq_thms = maps (fn a =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   348
      let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   349
        val permT = mk_permT (Type (a, []));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   350
        val pi1 = Free ("pi1", permT);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   351
        val pi2 = Free ("pi2", permT);
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   352
        val at_inst = at_inst_of thy2 a;
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   353
        val pt_inst = pt_inst_of thy2 a;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   354
        val pt3' = pt_inst RS pt3;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   355
        val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   356
        val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   357
      in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   358
        (Goal.prove_global thy2 [] []
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   359
          (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   360
             (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   361
                permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   362
              HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   363
                (map (fn ((s, T), x) =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   364
                    let val perm = Const (s, permT --> T --> T)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   365
                    in HOLogic.mk_eq
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   366
                      (perm $ pi1 $ Free (x, T),
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   367
                       perm $ pi2 $ Free (x, T))
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   368
                    end)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   369
                  (perm_names ~~
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   370
                   map body_type perm_types ~~ perm_indnames))))))
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
   371
           (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   372
              ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   373
         length new_type_names)
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   374
      end) atoms;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   375
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   376
    (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   377
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   378
    val cp1 = Global_Theory.get_thm thy2 "cp1";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   379
    val dj_cp = Global_Theory.get_thm thy2 "dj_cp";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   380
    val pt_perm_compose = Global_Theory.get_thm thy2 "pt_perm_compose";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   381
    val pt_perm_compose_rev = Global_Theory.get_thm thy2 "pt_perm_compose_rev";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   382
    val dj_perm_perm_forget = Global_Theory.get_thm thy2 "dj_perm_perm_forget";
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   383
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   384
    fun composition_instance name1 name2 thy =
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   385
      let
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   386
        val cp_class = cp_class_of thy name1 name2;
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   387
        val pt_class =
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   388
          if name1 = name2 then [pt_class_of thy name1]
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   389
          else [];
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   390
        val permT1 = mk_permT (Type (name1, []));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   391
        val permT2 = mk_permT (Type (name2, []));
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   392
        val Ts = map body_type perm_types;
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   393
        val cp_inst = cp_inst_of thy name1 name2;
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   394
        val simps = global_simpset_of thy addsimps (perm_fun_def ::
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   395
          (if name1 <> name2 then
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   396
             let val dj = dj_thm_of thy name2 name1
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   397
             in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   398
           else
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   399
             let
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   400
               val at_inst = at_inst_of thy name1;
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   401
               val pt_inst = pt_inst_of thy name1;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   402
             in
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   403
               [cp_inst RS cp1 RS sym,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   404
                at_inst RS (pt_inst RS pt_perm_compose) RS sym,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   405
                at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   406
            end))
36428
874843c1e96e really minimize sorts after certification -- looks like this is intended here;
wenzelm
parents: 35994
diff changeset
   407
        val sort = Sign.minimize_sort thy (Sign.certify_sort thy (cp_class :: pt_class));
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   408
        val thms = Datatype_Aux.split_conj_thm (Goal.prove_global thy [] []
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   409
          (augment_sort thy sort
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   410
            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   411
              (map (fn ((s, T), x) =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   412
                  let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   413
                    val pi1 = Free ("pi1", permT1);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   414
                    val pi2 = Free ("pi2", permT2);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   415
                    val perm1 = Const (s, permT1 --> T --> T);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   416
                    val perm2 = Const (s, permT2 --> T --> T);
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   417
                    val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   418
                  in HOLogic.mk_eq
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   419
                    (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   420
                     perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   421
                  end)
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   422
                (perm_names ~~ Ts ~~ perm_indnames)))))
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
   423
          (fn _ => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   424
             ALLGOALS (asm_full_simp_tac simps)]))
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   425
      in
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   426
        fold (fn (s, tvs) => fn thy => AxClass.prove_arity
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   427
            (s, map (inter_sort thy sort o snd) tvs, [cp_class])
24218
fbf1646b267c ClassPackage renamed to Class
haftmann
parents: 24110
diff changeset
   428
            (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   429
          (full_new_type_names' ~~ tyvars) thy
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   430
      end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   431
18381
246807ef6dfb changed the types in accordance with Florian's changes
urbanc
parents: 18366
diff changeset
   432
    val (perm_thmss,thy3) = thy2 |>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   433
      fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   434
      fold (fn atom => fn thy =>
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   435
        let val pt_name = pt_class_of thy atom
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   436
        in
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   437
          fold (fn (s, tvs) => fn thy => AxClass.prove_arity
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   438
              (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   439
              (EVERY
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   440
                [Class.intro_classes_tac [],
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   441
                 resolve_tac perm_empty_thms 1,
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   442
                 resolve_tac perm_append_thms 1,
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   443
                 resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   444
            (full_new_type_names' ~~ tyvars) thy
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   445
        end) atoms |>
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   446
      Global_Theory.add_thmss
29585
c23295521af5 binding replaces bstring
haftmann
parents: 29389
diff changeset
   447
        [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
18759
2f55e3e47355 Updated to Isabelle 2006-01-23
krauss
parents: 18707
diff changeset
   448
          unfolded_perm_eq_thms), [Simplifier.simp_add]),
29585
c23295521af5 binding replaces bstring
haftmann
parents: 29389
diff changeset
   449
         ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"),
18759
2f55e3e47355 Updated to Isabelle 2006-01-23
krauss
parents: 18707
diff changeset
   450
          perm_empty_thms), [Simplifier.simp_add]),
29585
c23295521af5 binding replaces bstring
haftmann
parents: 29389
diff changeset
   451
         ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"),
18759
2f55e3e47355 Updated to Isabelle 2006-01-23
krauss
parents: 18707
diff changeset
   452
          perm_append_thms), [Simplifier.simp_add]),
29585
c23295521af5 binding replaces bstring
haftmann
parents: 29389
diff changeset
   453
         ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"),
18759
2f55e3e47355 Updated to Isabelle 2006-01-23
krauss
parents: 18707
diff changeset
   454
          perm_eq_thms), [Simplifier.simp_add])];
21365
4ee8e2702241 InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents: 21291
diff changeset
   455
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   456
    (**** Define representing sets ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   457
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   458
    val _ = warning "representing sets";
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   459
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   460
    val rep_set_names =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   461
      Datatype_Prop.indexify_names
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   462
        (map (fn (i, _) => Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   463
    val big_rep_name =
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
   464
      space_implode "_" (Datatype_Prop.indexify_names (map_filter
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   465
        (fn (i, ("Nominal.noption", _, _)) => NONE
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   466
          | (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   467
    val _ = warning ("big_rep_name: " ^ big_rep_name);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   468
45896
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
   469
    fun strip_option (dtf as Datatype.DtType ("fun", [dt, Datatype.DtRec i])) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   470
          (case AList.lookup op = descr i of
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   471
             SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   472
               apfst (cons dt) (strip_option dt')
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   473
           | _ => ([], dtf))
45896
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
   474
      | strip_option (Datatype.DtType ("fun",
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
   475
            [dt, Datatype.DtType ("Nominal.noption", [dt'])])) =
18261
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   476
          apfst (cons dt) (strip_option dt')
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   477
      | strip_option dt = ([], dt);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   478
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   479
    val dt_atomTs = distinct op = (map (Datatype_Aux.typ_of_dtyp descr)
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   480
      (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr));
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   481
    val dt_atoms = map (fst o dest_Type) dt_atomTs;
18280
45e139675daf Corrected atom class constraints in strong induction rule.
berghofe
parents: 18261
diff changeset
   482
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   483
    fun make_intr s T (cname, cargs) =
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   484
      let
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   485
        fun mk_prem dt (j, j', prems, ts) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   486
          let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   487
            val (dts, dt') = strip_option dt;
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   488
            val (dts', dt'') = Datatype_Aux.strip_dtyp dt';
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   489
            val Ts = map (Datatype_Aux.typ_of_dtyp descr) dts;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   490
            val Us = map (Datatype_Aux.typ_of_dtyp descr) dts';
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   491
            val T = Datatype_Aux.typ_of_dtyp descr dt'';
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   492
            val free = Datatype_Aux.mk_Free "x" (Us ---> T) j;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   493
            val free' = Datatype_Aux.app_bnds free (length Us);
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   494
            fun mk_abs_fun T (i, t) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   495
              let val U = fastype_of t
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   496
              in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   497
                Type ("Nominal.noption", [U])) $ Datatype_Aux.mk_Free "y" T i $ t)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   498
              end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   499
          in (j + 1, j' + length Ts,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   500
            case dt'' of
46218
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 46215
diff changeset
   501
                Datatype.DtRec k => Logic.list_all (map (pair "x") Us,
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
   502
                  HOLogic.mk_Trueprop (Free (nth rep_set_names k,
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   503
                    T --> HOLogic.boolT) $ free')) :: prems
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   504
              | _ => prems,
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   505
            snd (fold_rev mk_abs_fun Ts (j', free)) :: ts)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   506
          end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   507
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   508
        val (_, _, prems, ts) = fold_rev mk_prem cargs (1, 1, [], []);
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   509
        val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   510
          list_comb (Const (cname, map fastype_of ts ---> T), ts))
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   511
      in Logic.list_implies (prems, concl)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   512
      end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   513
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   514
    val (intr_ts, (rep_set_names', recTs')) =
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   515
      apfst flat (apsnd ListPair.unzip (ListPair.unzip (map_filter
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   516
        (fn ((_, ("Nominal.noption", _, _)), _) => NONE
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   517
          | ((i, (_, _, constrs)), rep_set_name) =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   518
              let val T = nth_dtyp i
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   519
              in SOME (map (make_intr rep_set_name T) constrs,
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   520
                (rep_set_name, T))
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   521
              end)
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   522
                (descr ~~ rep_set_names))));
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28736
diff changeset
   523
    val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   524
21365
4ee8e2702241 InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents: 21291
diff changeset
   525
    val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
33278
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33244
diff changeset
   526
      thy3
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33244
diff changeset
   527
      |> Sign.map_naming Name_Space.conceal
33726
0878aecbf119 eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents: 33669
diff changeset
   528
      |> Inductive.add_inductive_global
33669
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33643
diff changeset
   529
          {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
ae9a2ea9a989 inductive: eliminated obsolete kind;
wenzelm
parents: 33643
diff changeset
   530
           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28736
diff changeset
   531
          (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
26128
fe2d24c26e0c inductive package: simplified group handling;
wenzelm
parents: 26067
diff changeset
   532
             (rep_set_names' ~~ recTs'))
33278
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33244
diff changeset
   533
          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
ba9f52f56356 conceal internal bindings;
wenzelm
parents: 33244
diff changeset
   534
      ||> Sign.restore_naming thy3;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   535
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   536
    (**** Prove that representing set is closed under permutation ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   537
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   538
    val _ = warning "proving closure under permutation...";
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   539
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   540
    val abs_perm = Global_Theory.get_thms thy4 "abs_perm";
25951
6ebe26bfed18 Reimplemented proof of strong induction theorem.
berghofe
parents: 25823
diff changeset
   541
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   542
    val perm_indnames' = map_filter
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   543
      (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   544
      (perm_indnames ~~ descr);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   545
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33968
diff changeset
   546
    fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   547
      (List.take (Datatype_Aux.split_conj_thm (Goal.prove_global thy4 [] []
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   548
        (augment_sort thy4
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33035
diff changeset
   549
          (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms))
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   550
          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   551
            (fn ((s, T), x) =>
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   552
               let
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   553
                 val S = Const (s, T --> HOLogic.boolT);
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   554
                 val permT = mk_permT (Type (name, []))
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   555
               in HOLogic.mk_imp (S $ Free (x, T),
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   556
                 S $ (Const ("Nominal.perm", permT --> T --> T) $
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   557
                   Free ("pi", permT) $ Free (x, T)))
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   558
               end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   559
        (fn _ => EVERY
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
   560
           [Datatype_Aux.ind_tac rep_induct [] 1,
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   561
            ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36692
diff changeset
   562
              (Thm.symmetric perm_fun_def :: abs_perm))),
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   563
            ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   564
        length new_type_names));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   565
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   566
    val perm_closed_thmss = map mk_perm_closed atoms;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   567
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   568
    (**** typedef ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   569
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   570
    val _ = warning "defining type...";
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   571
18366
78b4f225b640 Adapted to new type of PureThy.add_defs_i.
berghofe
parents: 18350
diff changeset
   572
    val (typedefs, thy6) =
26651
e630c789ef2b overloading perm: use big_name;
wenzelm
parents: 26646
diff changeset
   573
      thy4
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   574
      |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   575
          Typedef.add_typedef_global false NONE
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   576
            (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
37677
c5a8b612e571 qualified constants Set.member and Set.Collect
haftmann
parents: 37391
diff changeset
   577
            (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   578
               Const (cname, U --> HOLogic.boolT)) NONE
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   579
            (rtac exI 1 THEN rtac CollectI 1 THEN
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   580
              QUIET_BREADTH_FIRST (has_fewer_prems 1)
26475
3cc1e48d0ce1 eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents: 26359
diff changeset
   581
              (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   582
        let
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   583
          val permT = mk_permT
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 42388
diff changeset
   584
            (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   585
          val pi = Free ("pi", permT);
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   586
          val T = Type (Sign.full_name thy name, map TFree tvs);
18366
78b4f225b640 Adapted to new type of PureThy.add_defs_i.
berghofe
parents: 18350
diff changeset
   587
        in apfst (pair r o hd)
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   588
          (Global_Theory.add_defs_unchecked true
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   589
            [((Binding.map_name (fn n => "prm_" ^ n ^ "_def") name, Logic.mk_equals
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   590
              (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   591
               Const (Sign.intern_const thy ("Abs_" ^ Binding.name_of name), U --> T) $
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   592
                 (Const ("Nominal.perm", permT --> U --> U) $ pi $
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   593
                   (Const (Sign.intern_const thy ("Rep_" ^ Binding.name_of name), T --> U) $
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   594
                     Free ("x", T))))), [])] thy)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   595
        end))
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   596
        (types_syntax ~~ tyvars ~~ List.take (rep_set_names'' ~~ recTs', length new_type_names));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   597
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   598
    val perm_defs = map snd typedefs;
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35845
diff changeset
   599
    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35845
diff changeset
   600
    val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35845
diff changeset
   601
    val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   602
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   603
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   604
    (** prove that new types are in class pt_<name> **)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   605
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   606
    val _ = warning "prove that new types are in class pt_<name> ...";
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   607
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   608
    fun pt_instance (atom, perm_closed_thms) =
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   609
      fold (fn ((((((Abs_inverse, Rep_inverse), Rep),
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   610
        perm_def), name), tvs), perm_closed) => fn thy =>
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   611
          let
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   612
            val pt_class = pt_class_of thy atom;
36428
874843c1e96e really minimize sorts after certification -- looks like this is intended here;
wenzelm
parents: 35994
diff changeset
   613
            val sort = Sign.minimize_sort thy (Sign.certify_sort thy
874843c1e96e really minimize sorts after certification -- looks like this is intended here;
wenzelm
parents: 35994
diff changeset
   614
              (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms)))
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   615
          in AxClass.prove_arity
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   616
            (Sign.intern_type thy name,
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   617
              map (inter_sort thy sort o snd) tvs, [pt_class])
24218
fbf1646b267c ClassPackage renamed to Class
haftmann
parents: 24110
diff changeset
   618
            (EVERY [Class.intro_classes_tac [],
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   619
              rewrite_goals_tac [perm_def],
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   620
              asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1,
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   621
              asm_full_simp_tac (global_simpset_of thy addsimps
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   622
                [Rep RS perm_closed RS Abs_inverse]) 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: 39159
diff changeset
   623
              asm_full_simp_tac (HOL_basic_ss addsimps [Global_Theory.get_thm thy
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   624
                ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   625
          end)
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   626
        (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   627
           new_type_names ~~ tyvars ~~ perm_closed_thms);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   628
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   629
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   630
    (** prove that new types are in class cp_<name1>_<name2> **)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   631
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   632
    val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   633
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   634
    fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   635
      let
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   636
        val cp_class = cp_class_of thy atom1 atom2;
36428
874843c1e96e really minimize sorts after certification -- looks like this is intended here;
wenzelm
parents: 35994
diff changeset
   637
        val sort = Sign.minimize_sort thy (Sign.certify_sort thy
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33035
diff changeset
   638
          (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (remove (op =) atom1 dt_atoms) @
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   639
           (if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
36428
874843c1e96e really minimize sorts after certification -- looks like this is intended here;
wenzelm
parents: 35994
diff changeset
   640
            pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms))));
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   641
        val cp1' = cp_inst_of thy atom1 atom2 RS cp1
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   642
      in fold (fn ((((((Abs_inverse, Rep),
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   643
        perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
19275
3d10de7a8ca7 add_inst_arity_i renamed to prove_arity.
berghofe
parents: 19251
diff changeset
   644
          AxClass.prove_arity
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   645
            (Sign.intern_type thy name,
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
   646
              map (inter_sort thy sort o snd) tvs, [cp_class])
24218
fbf1646b267c ClassPackage renamed to Class
haftmann
parents: 24110
diff changeset
   647
            (EVERY [Class.intro_classes_tac [],
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   648
              rewrite_goals_tac [perm_def],
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   649
              asm_full_simp_tac (global_simpset_of thy addsimps
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   650
                ((Rep RS perm_closed1 RS Abs_inverse) ::
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   651
                 (if atom1 = atom2 then []
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   652
                  else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   653
              cong_tac 1,
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   654
              rtac refl 1,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   655
              rtac cp1' 1]) thy)
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   656
        (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   657
           tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   658
      end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   659
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   660
    val thy7 = fold (fn x => fn thy => thy |>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   661
      pt_instance x |>
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   662
      fold (cp_instance x) (atoms ~~ perm_closed_thmss))
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   663
        (atoms ~~ perm_closed_thmss) thy6;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   664
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   665
    (**** constructors ****)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   666
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   667
    fun mk_abs_fun x t =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   668
      let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   669
        val T = fastype_of x;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   670
        val U = fastype_of t
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   671
      in
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   672
        Const ("Nominal.abs_fun", T --> U --> T -->
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   673
          Type ("Nominal.noption", [U])) $ x $ t
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   674
      end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   675
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29585
diff changeset
   676
    val (ty_idxs, _) = List.foldl
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   677
      (fn ((i, ("Nominal.noption", _, _)), p) => p
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   678
        | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   679
45896
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
   680
    fun reindex (Datatype.DtType (s, dts)) = Datatype.DtType (s, map reindex dts)
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
   681
      | reindex (Datatype.DtRec i) = Datatype.DtRec (the (AList.lookup op = ty_idxs i))
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   682
      | reindex dt = dt;
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   683
40627
becf5d5187cc renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents: 39557
diff changeset
   684
    fun strip_suffix i s = implode (List.take (raw_explode s, size s - i));  (* FIXME Symbol.explode (?) *)
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   685
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   686
    (** strips the "_Rep" in type names *)
21365
4ee8e2702241 InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents: 21291
diff changeset
   687
    fun strip_nth_name i s =
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   688
      let val xs = Long_Name.explode s;
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   689
      in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   690
31458
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 30450
diff changeset
   691
    val (descr'', ndescr) = ListPair.unzip (map_filter
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   692
      (fn (i, ("Nominal.noption", _, _)) => NONE
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
   693
        | (i, (s, dts, constrs)) =>
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
   694
             let
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
   695
               val SOME index = AList.lookup op = ty_idxs i;
31458
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 30450
diff changeset
   696
               val (constrs2, constrs1) =
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 30450
diff changeset
   697
                 map_split (fn (cname, cargs) =>
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 30450
diff changeset
   698
                   apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 30450
diff changeset
   699
                   (fold_map (fn dt => fn dts =>
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
   700
                     let val (dts', dt') = strip_option dt
31458
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 30450
diff changeset
   701
                     in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end)
b1cf26f2919b avoid Library.foldl_map
haftmann
parents: 30450
diff changeset
   702
                       cargs [])) constrs
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
   703
             in SOME ((index, (strip_nth_name 1 s,  map reindex dts, constrs1)),
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
   704
               (index, constrs2))
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
   705
             end) descr);
18045
6d69a4190eb2 1) have adjusted the swapping of the result type
urbanc
parents: 18017
diff changeset
   706
19489
4441b637871b SplitAt -> chop
berghofe
parents: 19403
diff changeset
   707
    val (descr1, descr2) = chop (length new_type_names) descr'';
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   708
    val descr' = [descr1, descr2];
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
   709
19710
ee9c7fa80d21 Extended strong induction rule with additional
berghofe
parents: 19649
diff changeset
   710
    fun partition_cargs idxs xs = map (fn (i, j) =>
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
   711
      (List.take (List.drop (xs, i), j), nth xs (i + j))) idxs;
19710
ee9c7fa80d21 Extended strong induction rule with additional
berghofe
parents: 19649
diff changeset
   712
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   713
    val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts,
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   714
      map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   715
        (constrs ~~ idxss)))) (descr'' ~~ ndescr);
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   716
45896
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
   717
    fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype.DtRec i);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   718
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   719
    val rep_names = map (fn s =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   720
      Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   721
    val abs_names = map (fn s =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   722
      Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   723
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   724
    val recTs = Datatype_Aux.get_rec_types descr'';
33957
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   725
    val newTs' = take (length new_type_names) recTs';
e9afca2118d4 normalized uncurry take/drop
haftmann
parents: 33955
diff changeset
   726
    val newTs = take (length new_type_names) recTs;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   727
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28736
diff changeset
   728
    val full_new_type_names = map (Sign.full_bname thy) new_type_names;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   729
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   730
    fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   731
        (thy, defs, eqns) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   732
      let
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   733
        fun constr_arg (dts, dt) (j, l_args, r_args) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   734
          let
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   735
            val xs =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   736
              map (fn (dt, i) => Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) i)
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   737
                (dts ~~ (j upto j + length dts - 1))
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   738
            val x = Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts)
18261
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   739
          in
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   740
            (j + length dts + 1,
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   741
             xs @ x :: l_args,
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   742
             fold_rev mk_abs_fun xs
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   743
               (case dt of
45896
100fb1f33e3e tuned signature;
wenzelm
parents: 45890
diff changeset
   744
                  Datatype.DtRec k => if k < length new_type_names then
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   745
                      Const (nth rep_names k, Datatype_Aux.typ_of_dtyp descr'' dt -->
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   746
                        Datatype_Aux.typ_of_dtyp descr dt) $ x
18261
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   747
                    else error "nested recursion not (yet) supported"
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   748
                | _ => x) :: r_args)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   749
          end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   750
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   751
        val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 22543
diff changeset
   752
        val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 22543
diff changeset
   753
        val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   754
        val constrT = map fastype_of l_args ---> T;
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   755
        val lhs = list_comb (Const (cname, constrT), l_args);
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   756
        val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   757
        val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   758
        val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   759
          (Const (rep_name, T --> T') $ lhs, rhs));
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   760
        val def_name = (Long_Name.base_name cname) ^ "_def";
18366
78b4f225b640 Adapted to new type of PureThy.add_defs_i.
berghofe
parents: 18350
diff changeset
   761
        val ([def_thm], thy') = thy |>
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 45654
diff changeset
   762
          Sign.add_consts_i [(cname', constrT, mx)] |>
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   763
          (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   764
      in (thy', defs @ [def_thm], eqns @ [eqn]) end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   765
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   766
    fun dt_constr_defs ((((((_, (_, _, constrs)),
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   767
        (_, (_, _, constrs'))), tname), T), T'), constr_syntax) (thy, defs, eqns, dist_lemmas) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   768
      let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   769
        val rep_const = cterm_of thy
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   770
          (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   771
        val dist =
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33968
diff changeset
   772
          Drule.export_without_context
45909
6fe61da4c467 tuned signature;
wenzelm
parents: 45906
diff changeset
   773
            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] Datatype.distinct_lemma);
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   774
        val (thy', defs', eqns') = fold (make_constr_def tname T T')
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   775
          (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   776
      in
32124
954321008785 dropped ancient flat_names option
haftmann
parents: 32010
diff changeset
   777
        (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   778
      end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   779
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   780
    val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = fold dt_constr_defs
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   781
      (List.take (descr, length new_type_names) ~~
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   782
        List.take (pdescr, length new_type_names) ~~
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   783
        new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
   784
      (thy7, [], [], []);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   785
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35845
diff changeset
   786
    val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35845
diff changeset
   787
    val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   788
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   789
    (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
21365
4ee8e2702241 InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents: 21291
diff changeset
   790
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   791
    fun prove_constr_rep_thm eqn =
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   792
      let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   793
        val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   794
        val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   795
      in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   796
        [resolve_tac inj_thms 1,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   797
         rewrite_goals_tac rewrites,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   798
         rtac refl 3,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   799
         resolve_tac rep_intrs 2,
21021
6f19e5eb3a44 Adapted to new inductive definition package.
berghofe
parents: 20548
diff changeset
   800
         REPEAT (resolve_tac Rep_thms 1)])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   801
      end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   802
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   803
    val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   804
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   805
    (* prove theorem  pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   806
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   807
    fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   808
      let
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35842
diff changeset
   809
        val _ $ (_ $ (Rep $ x)) = Logic.unvarify_global (prop_of th);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   810
        val Type ("fun", [T, U]) = fastype_of Rep;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   811
        val permT = mk_permT (Type (atom, []));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   812
        val pi = Free ("pi", permT);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   813
      in
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   814
        Goal.prove_global thy8 [] []
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   815
          (augment_sort thy8
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33035
diff changeset
   816
            (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   817
            (HOLogic.mk_Trueprop (HOLogic.mk_eq
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   818
              (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   819
               Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
18010
c885c93a9324 Removed legacy prove_goalw_cterm command.
berghofe
parents: 17874
diff changeset
   820
          (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   821
            perm_closed_thms @ Rep_thms)) 1)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   822
      end) Rep_thms;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   823
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   824
    val perm_rep_perm_thms = maps prove_perm_rep_perm (atoms ~~ perm_closed_thmss);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   825
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   826
    (* prove distinctness theorems *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   827
45822
843dc212f69e datatype dtyp with explicit sort information;
wenzelm
parents: 45741
diff changeset
   828
    val distinct_props = Datatype_Prop.make_distincts descr';
27300
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27275
diff changeset
   829
    val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27275
diff changeset
   830
      dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
4cb3101d2bf7 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
haftmann
parents: 27275
diff changeset
   831
        constr_rep_thmss dist_lemmas;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   832
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45879
diff changeset
   833
    fun prove_distinct_thms _ [] = []
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45879
diff changeset
   834
      | prove_distinct_thms (p as (rep_thms, dist_lemma)) (t :: ts) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   835
          let
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   836
            val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   837
              simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33968
diff changeset
   838
          in
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33968
diff changeset
   839
            dist_thm :: Drule.export_without_context (dist_thm RS not_sym) ::
45889
4ff377493dbb misc tuning and simplification;
wenzelm
parents: 45879
diff changeset
   840
              prove_distinct_thms p ts
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   841
          end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   842
26969
cf3f998d0631 moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents: 26966
diff changeset
   843
    val distinct_thms = map2 prove_distinct_thms
cf3f998d0631 moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
haftmann
parents: 26966
diff changeset
   844
      (constr_rep_thmss ~~ dist_lemmas) distinct_props;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   845
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   846
    (** prove equations for permutation functions **)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   847
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   848
    val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   849
      let val T = nth_dtyp' i
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   850
      in maps (fn (atom, perm_closed_thms) =>
21365
4ee8e2702241 InductivePackage.add_inductive_i: canonical argument order;
wenzelm
parents: 21291
diff changeset
   851
          map (fn ((cname, dts), constr_rep_thm) =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   852
        let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   853
          val cname = Sign.intern_const thy8
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   854
            (Long_Name.append tname (Long_Name.base_name cname));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   855
          val permT = mk_permT (Type (atom, []));
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   856
          val pi = Free ("pi", permT);
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   857
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   858
          fun perm t =
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   859
            let val T = fastype_of t
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   860
            in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   861
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   862
          fun constr_arg (dts, dt) (j, l_args, r_args) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   863
            let
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   864
              val Ts = map (Datatype_Aux.typ_of_dtyp descr'') dts;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   865
              val xs =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   866
                map (fn (T, i) => Datatype_Aux.mk_Free "x" T i)
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   867
                  (Ts ~~ (j upto j + length dts - 1));
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   868
              val x =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   869
                Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts);
18261
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   870
            in
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   871
              (j + length dts + 1,
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   872
               xs @ x :: l_args,
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   873
               map perm (xs @ [x]) @ r_args)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   874
            end
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   875
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   876
          val (_, l_args, r_args) = fold_rev constr_arg dts (1, [], []);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   877
          val c = Const (cname, map fastype_of l_args ---> T)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   878
        in
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   879
          Goal.prove_global thy8 [] []
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   880
            (augment_sort thy8
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33035
diff changeset
   881
              (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   882
              (HOLogic.mk_Trueprop (HOLogic.mk_eq
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   883
                (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
18010
c885c93a9324 Removed legacy prove_goalw_cterm command.
berghofe
parents: 17874
diff changeset
   884
            (fn _ => EVERY
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   885
              [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   886
               simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   887
                 constr_defs @ perm_closed_thms)) 1,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   888
               TRY (simp_tac (HOL_basic_ss addsimps
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36692
diff changeset
   889
                 (Thm.symmetric perm_fun_def :: abs_perm)) 1),
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   890
               TRY (simp_tac (HOL_basic_ss addsimps
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   891
                 (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   892
                    perm_closed_thms)) 1)])
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   893
        end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss)
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   894
      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   895
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   896
    (** prove injectivity of constructors **)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   897
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   898
    val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   899
    val alpha = Global_Theory.get_thms thy8 "alpha";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
   900
    val abs_fresh = Global_Theory.get_thms thy8 "abs_fresh";
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   901
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   902
    val pt_cp_sort =
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   903
      map (pt_class_of thy8) dt_atoms @
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33035
diff changeset
   904
      maps (fn s => map (cp_class_of thy8 s) (remove (op =) s dt_atoms)) dt_atoms;
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   905
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   906
    val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   907
      let val T = nth_dtyp' i
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   908
      in map_filter (fn ((cname, dts), constr_rep_thm) =>
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   909
        if null dts then NONE else SOME
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   910
        let
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   911
          val cname = Sign.intern_const thy8
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   912
            (Long_Name.append tname (Long_Name.base_name cname));
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   913
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   914
          fun make_inj (dts, dt) (j, args1, args2, eqs) =
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   915
            let
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   916
              val Ts_idx =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   917
                map (Datatype_Aux.typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1);
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   918
              val xs = map (fn (T, i) => Datatype_Aux.mk_Free "x" T i) Ts_idx;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   919
              val ys = map (fn (T, i) => Datatype_Aux.mk_Free "y" T i) Ts_idx;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   920
              val x =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   921
                Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts);
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   922
              val y =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   923
                Datatype_Aux.mk_Free "y" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts);
18261
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   924
            in
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   925
              (j + length dts + 1,
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   926
               xs @ (x :: args1), ys @ (y :: args2),
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   927
               HOLogic.mk_eq
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   928
                 (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   929
            end;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   930
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   931
          val (_, args1, args2, eqs) = fold_rev make_inj dts (1, [], [], []);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   932
          val Ts = map fastype_of args1;
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   933
          val c = Const (cname, Ts ---> T)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   934
        in
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   935
          Goal.prove_global thy8 [] []
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   936
            (augment_sort thy8 pt_cp_sort
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   937
              (HOLogic.mk_Trueprop (HOLogic.mk_eq
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   938
                (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   939
                 foldr1 HOLogic.mk_conj eqs))))
18010
c885c93a9324 Removed legacy prove_goalw_cterm command.
berghofe
parents: 17874
diff changeset
   940
            (fn _ => EVERY
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
   941
               [asm_full_simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm ::
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   942
                  rep_inject_thms')) 1,
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   943
                TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   944
                  alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   945
                  perm_rep_perm_thms)) 1)])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   946
        end) (constrs ~~ constr_rep_thms)
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   947
      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   948
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   949
    (** equations for support and freshness **)
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   950
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   951
    val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   952
      (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   953
      let val T = nth_dtyp' i
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   954
      in maps (fn (cname, dts) => map (fn atom =>
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   955
        let
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   956
          val cname = Sign.intern_const thy8
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
   957
            (Long_Name.append tname (Long_Name.base_name cname));
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   958
          val atomT = Type (atom, []);
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   959
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   960
          fun process_constr (dts, dt) (j, args1, args2) =
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   961
            let
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   962
              val Ts_idx =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   963
                map (Datatype_Aux.typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1);
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   964
              val xs = map (fn (T, i) => Datatype_Aux.mk_Free "x" T i) Ts_idx;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   965
              val x =
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
   966
                Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts);
18261
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   967
            in
1318955d57ac Corrected treatment of non-recursive abstraction types.
berghofe
parents: 18246
diff changeset
   968
              (j + length dts + 1,
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   969
               xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   970
            end;
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   971
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
   972
          val (_, args1, args2) = fold_rev process_constr dts (1, [], []);
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   973
          val Ts = map fastype_of args1;
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   974
          val c = list_comb (Const (cname, Ts ---> T), args1);
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   975
          fun supp t =
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19489
diff changeset
   976
            Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
25823
5d75f4b179e2 Added function fresh_const.
berghofe
parents: 25674
diff changeset
   977
          fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   978
          val supp_thm = Goal.prove_global thy8 [] []
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   979
            (augment_sort thy8 pt_cp_sort
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   980
              (HOLogic.mk_Trueprop (HOLogic.mk_eq
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   981
                (supp c,
30450
7655e6533209 HOLogic.mk_set, HOLogic.dest_set
haftmann
parents: 30364
diff changeset
   982
                 if null dts then HOLogic.mk_set atomT []
35402
115a5a95710a clarified @{const_name} vs. @{const_abbrev};
wenzelm
parents: 35351
diff changeset
   983
                 else foldr1 (HOLogic.mk_binop @{const_abbrev union}) (map supp args2)))))
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   984
            (fn _ =>
18010
c885c93a9324 Removed legacy prove_goalw_cterm command.
berghofe
parents: 17874
diff changeset
   985
              simp_tac (HOL_basic_ss addsimps (supp_def ::
46161
4ed94d92ae19 prefer antiquotations;
wenzelm
parents: 45909
diff changeset
   986
                 Un_assoc :: @{thm de_Morgan_conj} :: Collect_disj_eq :: finite_Un ::
45654
cf10bde35973 more antiquotations;
wenzelm
parents: 44693
diff changeset
   987
                 Collect_False_empty :: finite_emptyI :: @{thms simp_thms} @
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
   988
                 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   989
        in
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   990
          (supp_thm,
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   991
           Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   992
             (HOLogic.mk_Trueprop (HOLogic.mk_eq
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   993
               (fresh c,
45740
132a3e1c0fe5 more antiquotations;
wenzelm
parents: 45735
diff changeset
   994
                if null dts then @{term True}
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
   995
                else foldr1 HOLogic.mk_conj (map fresh args2)))))
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
   996
             (fn _ =>
24459
fd114392bca9 Got rid of large simpset in proof of characteristic equations
berghofe
parents: 24218
diff changeset
   997
               simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
   998
        end) atoms) constrs
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
   999
      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
17872
f08fc98a164a Implemented proofs for support and freshness theorems.
berghofe
parents: 17870
diff changeset
  1000
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1001
    (**** weak induction theorem ****)
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1002
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
  1003
    fun mk_indrule_lemma (((i, _), T), U) (prems, concls) =
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1004
      let
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1005
        val Rep_t = Const (nth rep_names i, T --> U) $ Datatype_Aux.mk_Free "x" T i;
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1006
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
  1007
        val Abs_t =  Const (nth abs_names i, U --> T);
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1008
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1009
      in
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1010
        (prems @ [HOLogic.imp $
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
  1011
            (Const (nth rep_set_names'' i, U --> HOLogic.boolT) $ Rep_t) $
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1012
              (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1013
         concls @
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1014
           [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i])
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1015
      end;
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1017
    val (indrule_lemma_prems, indrule_lemma_concls) =
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33171
diff changeset
  1018
      fold mk_indrule_lemma (descr'' ~~ recTs ~~ recTs') ([], []);
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1019
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
  1020
    val indrule_lemma = Goal.prove_global thy8 [] []
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1021
      (Logic.mk_implies
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1022
        (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems),
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1023
         HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls))) (fn _ => EVERY
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1024
           [REPEAT (etac conjE 1),
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1025
            REPEAT (EVERY
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1026
              [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
  1027
               etac mp 1, resolve_tac Rep_thms 1])]);
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1028
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1029
    val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1030
    val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1031
      map (Free o apfst fst o dest_Var) Ps;
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1032
    val indrule_lemma' = cterm_instantiate
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1033
      (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1034
19833
3a3f591c838d - Changed naming scheme: names of "internal" constructors now have
berghofe
parents: 19710
diff changeset
  1035
    val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1036
45822
843dc212f69e datatype dtyp with explicit sort information;
wenzelm
parents: 45741
diff changeset
  1037
    val dt_induct_prop = Datatype_Prop.make_ind descr';
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
  1038
    val dt_induct = Goal.prove_global thy8 []
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1039
      (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
26711
3a478bfa1650 prove_global: pass context;
wenzelm
parents: 26689
diff changeset
  1040
      (fn {prems, ...} => EVERY
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1041
        [rtac indrule_lemma' 1,
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
  1042
         (Datatype_Aux.ind_tac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1043
         EVERY (map (fn (prem, r) => (EVERY
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1044
           [REPEAT (eresolve_tac Abs_inverse_thms' 1),
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36692
diff changeset
  1045
            simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1,
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1046
            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 19985
diff changeset
  1047
                (prems ~~ constr_defs))]);
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1048
45906
0aaeb5520f2f tuned signature;
wenzelm
parents: 45896
diff changeset
  1049
    val case_names_induct = Datatype.mk_case_names_induct descr'';
18016
8f3a80033ba4 Implemented proof of weak induction theorem.
berghofe
parents: 18010
diff changeset
  1050
18066
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1051
    (**** prove that new datatypes have finite support ****)
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1052
18246
676d2e625d98 added fsub.thy (poplmark challenge) to the examples
urbanc
parents: 18245
diff changeset
  1053
    val _ = warning "proving finite support for the new datatype";
676d2e625d98 added fsub.thy (poplmark challenge) to the examples
urbanc
parents: 18245
diff changeset
  1054
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
  1055
    val indnames = Datatype_Prop.make_tnames recTs;
18066
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1056
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1057
    val abs_supp = Global_Theory.get_thms thy8 "abs_supp";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1058
    val supp_atm = Global_Theory.get_thms thy8 "supp_atm";
18066
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1059
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1060
    val finite_supp_thms = map (fn atom =>
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1061
      let val atomT = Type (atom, [])
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 33968
diff changeset
  1062
      in map Drule.export_without_context (List.take
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1063
        (Datatype_Aux.split_conj_thm (Goal.prove_global thy8 [] []
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1064
           (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1065
             (HOLogic.mk_Trueprop
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1066
               (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1067
                 Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1068
                   (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1069
                   (indnames ~~ recTs)))))
45735
7d7d7af647a9 tuned signature;
wenzelm
parents: 45701
diff changeset
  1070
           (fn _ => Datatype_Aux.ind_tac dt_induct indnames 1 THEN
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 32134
diff changeset
  1071
            ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
18067
8b9848d150ba - completed the list of thms for supp_atm
urbanc
parents: 18066
diff changeset
  1072
              (abs_supp @ supp_atm @
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1073
               Global_Theory.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1074
               flat supp_thms))))),
18066
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1075
         length new_type_names))
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1076
      end) atoms;
d1e47ee13070 Added code for proving that new datatype has finite support.
berghofe
parents: 18054
diff changeset
  1077
18759
2f55e3e47355 Updated to Isabelle 2006-01-23
krauss
parents: 18707
diff changeset
  1078
    val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1079
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32957
diff changeset
  1080
        (* Function to add both the simp and eqvt attributes *)
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22231
diff changeset
  1081
        (* These two attributes are duplicated on all the types in the mutual nominal datatypes *)
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22231
diff changeset
  1082
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22231
diff changeset
  1083
    val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, NominalThmDecls.eqvt_add];
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22231
diff changeset
  1084
 
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1085
    val (_, thy9) = thy8 |>
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24459
diff changeset
  1086
      Sign.add_path big_name |>
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1087
      Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1088
      Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24459
diff changeset
  1089
      Sign.parent_path ||>>
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
  1090
      Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33957
diff changeset
  1091
      Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33957
diff changeset
  1092
      Datatype_Aux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33957
diff changeset
  1093
      Datatype_Aux.store_thmss "inject" new_type_names inject_thms ||>>
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33957
diff changeset
  1094
      Datatype_Aux.store_thmss "supp" new_type_names supp_thms ||>>
f94fb13ecbb3 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33957
diff changeset
  1095
      Datatype_Aux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1096
      fold (fn (atom, ths) => fn thy =>
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
  1097
        let
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
  1098
          val class = fs_class_of thy atom;
36428
874843c1e96e really minimize sorts after certification -- looks like this is intended here;
wenzelm
parents: 35994
diff changeset
  1099
          val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort));
28736
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
  1100
        in fold (fn Type (s, Ts) => AxClass.prove_arity
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
  1101
          (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
b1fd60fee652 Some modifications in code for proving arities to make it work for datatype
berghofe
parents: 28731
diff changeset
  1102
          (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1103
        end) (atoms ~~ finite_supp_thms);
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1104
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1105
    (**** strong induction theorem ****)
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1106
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1107
    val pnames = if length descr'' = 1 then ["P"]
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1108
      else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
18245
65e60434b3c2 Fixed problem with strong induction theorem for datatypes containing
berghofe
parents: 18142
diff changeset
  1109
    val ind_sort = if null dt_atomTs then HOLogic.typeS
36428
874843c1e96e really minimize sorts after certification -- looks like this is intended here;
wenzelm
parents: 35994
diff changeset
  1110
      else Sign.minimize_sort thy9 (Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms));
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1111
    val fsT = TFree ("'n", ind_sort);
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1112
    val fsT' = TFree ("'n", HOLogic.typeS);
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1113
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1114
    val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
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
  1115
      (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1116
42364
8c674b3b8e44 eliminated old List.nth;
wenzelm
parents: 42361
diff changeset
  1117
    fun make_pred fsT i T = Free (nth pnames i, fsT --> T --> HOLogic.boolT);
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1118
19851
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1119
    fun mk_fresh1 xs [] = []
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1120
      | mk_fresh1 xs ((y as (_, T)) :: ys) = map (fn x => HOLogic.mk_Trueprop
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1121
            (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x))))
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1122
              (filter (fn (_, U) => T = U) (rev xs)) @
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1123
          mk_fresh1 (y :: xs) ys;
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1124
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1125
    fun mk_fresh2 xss [] = []
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1126
      | mk_fresh2 xss ((p as (ys, _)) :: yss) = maps (fn y as (_, T) =>
19851
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1127
            map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1128
              (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys @
19851
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1129
          mk_fresh2 (p :: xss) yss;
10162c01bd78 Completely rewrote code for defining graph of recursion combinator.
berghofe
parents: 19833
diff changeset
  1130
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1131
    fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1132
      let
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1133
        val recs = filter Datatype_Aux.is_rec_type cargs;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1134
        val Ts = map (Datatype_Aux.typ_of_dtyp descr'') cargs;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1135
        val recTs' = map (Datatype_Aux.typ_of_dtyp descr'') recs;
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
  1136
        val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1137
        val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1138
        val frees = tnames ~~ Ts;
19710
ee9c7fa80d21 Extended strong induction rule with additional
berghofe
parents: 19649
diff changeset
  1139
        val frees' = partition_cargs idxs frees;
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 42388
diff changeset
  1140
        val z = (singleton (Name.variant_list tnames) "z", fsT);
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1141
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1142
        fun mk_prem ((dt, s), T) =
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1143
          let
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1144
            val (Us, U) = strip_type T;
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1145
            val l = length Us;
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1146
          in
46218
ecf6375e2abb renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents: 46215
diff changeset
  1147
            Logic.list_all (z :: map (pair "x") Us,
45838
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1148
              HOLogic.mk_Trueprop
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1149
                (make_pred fsT (Datatype_Aux.body_index dt) U $ Bound l $
653c84d5c6c9 do not open ML structures;
wenzelm
parents: 45822
diff changeset
  1150
                  Datatype_Aux.app_bnds (Free (s, T)) l))
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1151
          end;
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1152
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1153
        val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1154
        val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1155
            (f T (Free p) (Free z))) (maps fst frees') @
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1156
          mk_fresh1 [] (maps fst frees') @
19710
ee9c7fa80d21 Extended strong induction rule with additional
berghofe
parents: 19649
diff changeset
  1157
          mk_fresh2 [] frees'
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1158
46215
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 46161
diff changeset
  1159
      in
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 46161
diff changeset
  1160
        fold_rev (Logic.all o Free) (frees @ [z])
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 46161
diff changeset
  1161
          (Logic.list_implies (prems' @ prems,
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 46161
diff changeset
  1162
            HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 46161
diff changeset
  1163
              list_comb (Const (cname, Ts ---> T), map Free frees))))
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1164
      end;
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1165
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1166
    val ind_prems = maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1167
      map (make_ind_prem fsT (fn T => fn t => fn u =>
25823
5d75f4b179e2 Added function fresh_const.
berghofe
parents: 25674
diff changeset
  1168
        fresh_const T fsT $ t $ u) i T)
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1169
          (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
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
  1170
    val tnames = Datatype_Prop.make_tnames recTs;
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 20046
diff changeset
  1171
    val zs = Name.variant_list tnames (replicate (length descr'') "z");
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38715
diff changeset
  1172
    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1173
      (map (fn ((((i, _), T), tname), z) =>
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1174
        make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1175
        (descr'' ~~ recTs ~~ tnames ~~ zs)));
18107
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1176
    val induct = Logic.list_implies (ind_prems, ind_concl);
ee6b4d3af498 Added strong induction theorem (currently only axiomatized!).
berghofe
parents: 18104
diff changeset
  1177
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1178
    val ind_prems' =
46215
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 46161
diff changeset
  1179
      map (fn (_, f as Free (_, T)) => Logic.all (Free ("x", fsT'))
0da9433f959e discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents: 46161
diff changeset
  1180
        (HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
44692
ccfc7c193d2b modify nominal packages to better respect set/pred distinction
huffman
parents: 44241
diff changeset
  1181
          Term.range_type T -->
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26711
diff changeset
  1182
            HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1183
      maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1184
        map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1185
          HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32727
diff changeset
  1186
            (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38715
diff changeset
  1187
    val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1188
      (map (fn ((((i, _), T), tname), z) =>
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1189
        make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1190
        (descr'' ~~ recTs ~~ tnames ~~ zs)));
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1191
    val induct' = Logic.list_implies (ind_prems', ind_concl');
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1192
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1193
    val aux_ind_vars =
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
  1194
      (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1195
       map mk_permT dt_atomTs) @ [("z", fsT')];
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1196
    val aux_ind_Ts = rev (map snd aux_ind_vars);
38795
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents: 38715
diff changeset
  1197
    val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1198
      (map (fn (((i, _), T), tname) =>
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1199
        HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
22311
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
  1200
          fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
ebcd44cb8d61 Curried and exported mk_perm.
berghofe
parents: 22274
diff changeset
  1201
            (Free (tname, T))))
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1202
        (descr'' ~~ recTs ~~ tnames)));
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1203
28731
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1204
    val fin_set_supp = map (fn s =>
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1205
      at_inst_of thy9 s RS at_fin_set_supp) dt_atoms;
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1206
    val fin_set_fresh = map (fn s =>
c60ac7923a06 Added support for parametric datatypes.
berghofe
parents: 28662
diff changeset
  1207
      at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
25951
6ebe26bfed18 Reimplemented proof of strong induction theorem.
berghofe
parents: 25823
diff changeset
  1208
    val pt1_atoms = map (fn Type (s, _) =>
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1209
      Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
25951
6ebe26bfed18 Reimplemented proof of strong induction theorem.
berghofe
parents: 25823
diff changeset
  1210
    val pt2_atoms = map (fn Type (s, _) =>
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1211
      Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1212
    val exists_fresh' = Global_Theory.get_thms thy9 "exists_fresh'";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1213
    val fs_atoms = Global_Theory.get_thms thy9 "fin_supp";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1214
    val abs_supp = Global_Theory.get_thms thy9 "abs_supp";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1215
    val perm_fresh_fresh = Global_Theory.get_thms thy9 "perm_fresh_fresh";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1216
    val calc_atm = Global_Theory.get_thms thy9 "calc_atm";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1217
    val fresh_atm = Global_Theory.get_thms thy9 "fresh_atm";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1218
    val fresh_left = Global_Theory.get_thms thy9 "fresh_left";
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39159
diff changeset
  1219
    val perm_swap = Global_Theory.get_thms thy9 "perm_swap";
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1220
25951
6ebe26bfed18 Reimplemented proof of strong induction theorem.
berghofe
parents: 25823
diff changeset
  1221
    fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
18658
317a6f0ef8b9 Implemented proof of (strong) induction rule.
berghofe
parents: 18582
diff changeset
  1222
      let
25951
6ebe26bfed18 Reimplemented proof of strong induction theorem.
berghofe
parents: 25823
diff changeset
  1223
        val p = foldr1 HOLogic.mk_prod (ts @ freshs1);
6ebe26bfed18 Reimplemented proof of strong induction theorem.
berghofe
parents: 25823
diff changeset
  1224
        val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
6ebe26bfed18 Reimplemented proof of strong induction theorem.
berghofe
parents: 25823
diff changeset
  1225
            (HOLogic.exists_const T $ Abs ("x", T,
6ebe26bfed18 Reimplemented proof of strong induction theorem.
ber