src/ZF/Tools/datatype_package.ML
author wenzelm
Tue, 29 Sep 2009 22:48:24 +0200
changeset 32765 3032c0308019
parent 30364 577edc39b501
child 32952 aeb1e44fbc19
permissions -rw-r--r--
modernized Balanced_Tree;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6052
diff changeset
     1
(*  Title:      ZF/Tools/datatype_package.ML
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     3
    Copyright   1994  University of Cambridge
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     4
6065
3b4a29166f26 induct_tac and exhaust_tac
paulson
parents: 6052
diff changeset
     5
Datatype/Codatatype Definitions
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     6
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     7
The functor will be instantiated for normal sums/products (datatype defs)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     8
                         and non-standard sums/products (codatatype defs)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     9
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    10
Sums are used only for mutual recursion;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    11
Products are used only to derive "streamlined" induction rules for relations
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    12
*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    13
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    14
type datatype_result =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    15
   {con_defs   : thm list,             (*definitions made in thy*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    16
    case_eqns  : thm list,             (*equations for case operator*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    17
    recursor_eqns : thm list,          (*equations for the recursor*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    18
    free_iffs  : thm list,             (*freeness rewrite rules*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    19
    free_SEs   : thm list,             (*freeness destruct rules*)
6112
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
    20
    mk_free    : string -> thm};       (*function to make freeness theorems*)
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    21
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    22
signature DATATYPE_ARG =
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    23
sig
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    24
  val intrs : thm list
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    25
  val elims : thm list
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    26
end;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    27
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    28
signature DATATYPE_PACKAGE =
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
    29
sig
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    30
  (*Insert definitions for the recursive sets, which
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    31
     must *already* be declared as constants in parent theory!*)
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    32
  val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    33
    thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    34
  val add_datatype: string * string list -> (string * string list * mixfix) list list ->
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26190
diff changeset
    35
    (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 26190
diff changeset
    36
    (Facts.ref * Attrib.src list) list -> theory -> theory * inductive_result * datatype_result
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
    37
end;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    38
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
    39
functor Add_datatype_def_Fun
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    40
 (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    41
  and Ind_Package : INDUCTIVE_PACKAGE
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    42
  and Datatype_Arg : DATATYPE_ARG
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    43
  val coind : bool): DATATYPE_PACKAGE =
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    44
struct
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    45
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    46
(*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *)
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    47
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    48
(*univ or quniv constitutes the sum domain for mutual recursion;
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    49
  it is applied to the datatype parameters and to Consts occurring in the
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    50
  definition other than Nat.nat and the datatype sets themselves.
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    51
  FIXME: could insert all constant set expressions, e.g. nat->nat.*)
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    52
fun data_domain co (rec_tms, con_ty_lists) =
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    53
    let val rec_hds = map head_of rec_tms
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    54
        val dummy = assert_all is_Const rec_hds
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    55
          (fn t => "Datatype set not previously declared as constant: " ^
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26336
diff changeset
    56
                   Syntax.string_of_term_global @{theory IFOL} t);
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    57
        val rec_names = (*nat doesn't have to be added*)
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    58
	    @{const_name nat} :: map (#1 o dest_Const) rec_hds
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    59
	val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    60
	val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    61
          (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    62
            | _ => I)) con_ty_lists [];
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    63
    in  u $ Ind_Syntax.union_params (hd rec_tms, cs)  end;
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
    64
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
    65
fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    66
 let
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    67
  val dummy = (*has essential ancestors?*)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 25985
diff changeset
    68
    Theory.requires thy "Datatype_ZF" "(co)datatype definitions";
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    69
13150
0c50d13d449a better error messages for datatypes not declared Const
paulson
parents: 12876
diff changeset
    70
  val rec_hds = map head_of rec_tms;
0c50d13d449a better error messages for datatypes not declared Const
paulson
parents: 12876
diff changeset
    71
0c50d13d449a better error messages for datatypes not declared Const
paulson
parents: 12876
diff changeset
    72
  val dummy = assert_all is_Const rec_hds
0c50d13d449a better error messages for datatypes not declared Const
paulson
parents: 12876
diff changeset
    73
          (fn t => "Datatype set not previously declared as constant: " ^
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26336
diff changeset
    74
                   Syntax.string_of_term_global thy t);
13150
0c50d13d449a better error messages for datatypes not declared Const
paulson
parents: 12876
diff changeset
    75
0c50d13d449a better error messages for datatypes not declared Const
paulson
parents: 12876
diff changeset
    76
  val rec_names = map (#1 o dest_Const) rec_hds
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30345
diff changeset
    77
  val rec_base_names = map Long_Name.base_name rec_names
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    78
  val big_rec_base_name = space_implode "_" rec_base_names
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    79
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24707
diff changeset
    80
  val thy_path = thy |> Sign.add_path big_rec_base_name
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    81
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 22101
diff changeset
    82
  val big_rec_name = Sign.intern_const thy_path big_rec_base_name;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    83
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 22101
diff changeset
    84
  val intr_tms = Ind_Syntax.mk_all_intr_tms thy_path (rec_tms, con_ty_lists);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    85
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
    86
  val dummy =
12243
wenzelm
parents: 12226
diff changeset
    87
    writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    88
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    89
  val case_varname = "f";                (*name for case variables*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    90
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    91
  (** Define the constructors **)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    92
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    93
  (*The empty tuple is 0*)
26190
cf51a23c0cd0 tuned ML code, more antiquotations;
wenzelm
parents: 26189
diff changeset
    94
  fun mk_tuple [] = @{const "0"}
7696
wenzelm
parents: 6154
diff changeset
    95
    | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    96
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 30364
diff changeset
    97
  fun mk_inject n k u = Balanced_Tree.access
23419
8c30dd4b3b22 BalancedTree;
wenzelm
parents: 22578
diff changeset
    98
    {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = u} n k;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    99
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   100
  val npart = length rec_names;  (*number of mutually recursive parts*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   101
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   102
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28839
diff changeset
   103
  val full_name = Sign.full_bname thy_path;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   104
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   105
  (*Make constructor definition;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   106
    kpart is the number of this mutually recursive part*)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   107
  fun mk_con_defs (kpart, con_ty_list) =
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   108
    let val ncon = length con_ty_list    (*number of constructors*)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   109
        fun mk_def (((id,T,syn), name, args, prems), kcon) =
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   110
              (*kcon is index of constructor*)
24255
d86dbde1000c PrimitiveDefs.mk_defpair;
wenzelm
parents: 23419
diff changeset
   111
            PrimitiveDefs.mk_defpair (list_comb (Const (full_name name, T), args),
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   112
                        mk_inject npart kpart
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   113
                        (mk_inject ncon kcon (mk_tuple args)))
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   114
    in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   115
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   116
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   117
  (*** Define the case operator ***)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   118
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   119
  (*Combine split terms using case; yields the case operator for one part*)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   120
  fun call_case case_list =
26190
cf51a23c0cd0 tuned ML code, more antiquotations;
wenzelm
parents: 26189
diff changeset
   121
    let fun call_f (free,[]) = Abs("null", @{typ i}, free)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   122
          | call_f (free,args) =
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   123
                CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
26190
cf51a23c0cd0 tuned ML code, more antiquotations;
wenzelm
parents: 26189
diff changeset
   124
                            @{typ i}
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   125
                            free
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 30364
diff changeset
   126
    in  Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   127
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   128
  (** Generating function variables for the case definition
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   129
      Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   130
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   131
  (*The function variable for a single constructor*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   132
  fun add_case (((_, T, _), name, args, _), (opno, cases)) =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   133
    if Syntax.is_identifier name then
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   134
      (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   135
    else
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   136
      (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   137
       :: cases);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   138
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   139
  (*Treatment of a list of constructors, for one part
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   140
    Result adds a list of terms, each a function variable with arguments*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   141
  fun add_case_list (con_ty_list, (opno, case_lists)) =
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29579
diff changeset
   142
    let val (opno', case_list) = List.foldr add_case (opno, []) con_ty_list
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   143
    in (opno', case_list :: case_lists) end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   144
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   145
  (*Treatment of all parts*)
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29579
diff changeset
   146
  val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   147
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   148
  (*extract the types of all the variables*)
26190
cf51a23c0cd0 tuned ML code, more antiquotations;
wenzelm
parents: 26189
diff changeset
   149
  val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"};
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   150
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   151
  val case_base_name = big_rec_base_name ^ "_case";
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   152
  val case_name = full_name case_base_name;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   153
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   154
  (*The list of all the function variables*)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   155
  val case_args = List.concat (map (map #1) case_lists);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   156
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   157
  val case_const = Const (case_name, case_typ);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   158
  val case_tm = list_comb (case_const, case_args);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   159
24255
d86dbde1000c PrimitiveDefs.mk_defpair;
wenzelm
parents: 23419
diff changeset
   160
  val case_def = PrimitiveDefs.mk_defpair
32765
3032c0308019 modernized Balanced_Tree;
wenzelm
parents: 30364
diff changeset
   161
    (case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   162
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   163
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   164
  (** Generating function variables for the recursor definition
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   165
      Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   166
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   167
  (*a recursive call for x is the application rec`x  *)
26190
cf51a23c0cd0 tuned ML code, more antiquotations;
wenzelm
parents: 26189
diff changeset
   168
  val rec_call = @{const apply} $ Free ("rec", @{typ i});
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   169
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   170
  (*look back down the "case args" (which have been reversed) to
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   171
    determine the de Bruijn index*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   172
  fun make_rec_call ([], _) arg = error
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   173
          "Internal error in datatype (variable name mismatch)"
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   174
    | make_rec_call (a::args, i) arg =
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   175
           if a = arg then rec_call $ Bound i
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   176
           else make_rec_call (args, i+1) arg;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   177
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   178
  (*creates one case of the "X_case" definition of the recursor*)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   179
  fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) =
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   180
      let fun add_abs (Free(a,T), u) = Abs(a,T,u)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   181
          val ncase_args = length case_args
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   182
          val bound_args = map Bound ((ncase_args - 1) downto 0)
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   183
          val rec_args = map (make_rec_call (rev case_args,0))
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   184
                         (List.drop(recursor_args, ncase_args))
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   185
      in
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29579
diff changeset
   186
          List.foldr add_abs
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   187
            (list_comb (recursor_var,
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   188
                        bound_args @ rec_args)) case_args
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   189
      end
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   190
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   191
  (*Find each recursive argument and add a recursive call for it*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   192
  fun rec_args [] = []
24826
78e6a3cea367 avoid unnamed infixes;
wenzelm
parents: 24725
diff changeset
   193
    | rec_args ((Const(@{const_name mem},_)$arg$X)::prems) =
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   194
       (case head_of X of
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   195
            Const(a,_) => (*recursive occurrence?*)
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   196
                          if a mem_string rec_names
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   197
                              then arg :: rec_args prems
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   198
                          else rec_args prems
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   199
          | _ => rec_args prems)
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   200
    | rec_args (_::prems) = rec_args prems;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   201
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   202
  (*Add an argument position for each occurrence of a recursive set.
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   203
    Strictly speaking, the recursive arguments are the LAST of the function
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   204
    variable, but they all have type "i" anyway*)
26190
cf51a23c0cd0 tuned ML code, more antiquotations;
wenzelm
parents: 26189
diff changeset
   205
  fun add_rec_args args' T = (map (fn _ => @{typ i}) args') ---> T
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   206
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   207
  (*Plug in the function variable type needed for the recursor
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   208
    as well as the new arguments (recursive calls)*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   209
  fun rec_ty_elem ((id, T, syn), name, args, prems) =
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   210
      let val args' = rec_args prems
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   211
      in ((id, add_rec_args args' T, syn),
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   212
          name, args @ args', prems)
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   213
      end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   214
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   215
  val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   216
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   217
  (*Treatment of all parts*)
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29579
diff changeset
   218
  val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   219
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   220
  (*extract the types of all the variables*)
26190
cf51a23c0cd0 tuned ML code, more antiquotations;
wenzelm
parents: 26189
diff changeset
   221
  val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"};
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   222
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   223
  val recursor_base_name = big_rec_base_name ^ "_rec";
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   224
  val recursor_name = full_name recursor_base_name;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   225
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   226
  (*The list of all the function variables*)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   227
  val recursor_args = List.concat (map (map #1) recursor_lists);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   228
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   229
  val recursor_tm =
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   230
    list_comb (Const (recursor_name, recursor_typ), recursor_args);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   231
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   232
  val recursor_cases = map call_recursor
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   233
                         (List.concat case_lists ~~ List.concat recursor_lists)
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   234
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   235
  val recursor_def =
24255
d86dbde1000c PrimitiveDefs.mk_defpair;
wenzelm
parents: 23419
diff changeset
   236
      PrimitiveDefs.mk_defpair
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   237
        (recursor_tm,
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   238
         @{const Univ.Vrecursor} $
26190
cf51a23c0cd0 tuned ML code, more antiquotations;
wenzelm
parents: 26189
diff changeset
   239
           absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   240
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   241
  (* Build the new theory *)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   242
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   243
  val need_recursor = (not coind andalso recursor_typ <> case_typ);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   244
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   245
  fun add_recursor thy =
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   246
      if need_recursor then
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24707
diff changeset
   247
           thy |> Sign.add_consts_i
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   248
                    [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   249
               |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   250
      else thy;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   251
18358
0a733e11021a re-oriented some result tuples in PureThy
haftmann
parents: 18185
diff changeset
   252
  val (con_defs, thy0) = thy_path
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24707
diff changeset
   253
             |> Sign.add_consts_i
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   254
                 (map (fn (c, T, mx) => (Binding.name c, T, mx))
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   255
                  ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)))
27691
ce171cbd4b93 PureThy: dropped note_thmss_qualified, dropped _i suffix
haftmann
parents: 27261
diff changeset
   256
             |> PureThy.add_defs false
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   257
                 (map (Thm.no_attributes o apfst Binding.name)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   258
                  (case_def ::
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   259
                   List.concat (ListPair.map mk_con_defs
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   260
                         (1 upto npart, con_ty_lists))))
18358
0a733e11021a re-oriented some result tuples in PureThy
haftmann
parents: 18185
diff changeset
   261
             ||> add_recursor
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24707
diff changeset
   262
             ||> Sign.parent_path
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   263
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28839
diff changeset
   264
  val intr_names = map (Binding.name o #2) (List.concat con_ty_lists);
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   265
  val (thy1, ind_result) =
12187
a1000fcf636e use proper intr_names (for required case_names);
wenzelm
parents: 12183
diff changeset
   266
    thy0 |> Ind_Package.add_inductive_i
a1000fcf636e use proper intr_names (for required case_names);
wenzelm
parents: 12183
diff changeset
   267
      false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
a1000fcf636e use proper intr_names (for required case_names);
wenzelm
parents: 12183
diff changeset
   268
      (monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   269
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   270
  (**** Now prove the datatype theorems in this theory ****)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   271
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   272
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   273
  (*** Prove the case theorems ***)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   274
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   275
  (*Each equation has the form
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   276
    case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   277
  fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   278
    FOLogic.mk_Trueprop
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   279
      (FOLogic.mk_eq
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   280
       (case_tm $
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 22101
diff changeset
   281
         (list_comb (Const (Sign.intern_const thy1 name,T),
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   282
                     args)),
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   283
        list_comb (case_free, args)));
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   284
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   285
  val case_trans = hd con_defs RS @{thm def_trans}
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   286
  and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS @{thm trans};
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   287
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   288
  fun prove_case_eqn (arg, con_def) =
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 18728
diff changeset
   289
    Goal.prove_global thy1 [] []
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   290
      (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   291
      (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   292
      (fn _ => EVERY
28839
32d498cf7595 eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
wenzelm
parents: 28678
diff changeset
   293
        [rewrite_goals_tac [con_def],
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   294
         rtac case_trans 1,
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 18728
diff changeset
   295
         REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   296
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   297
  val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   298
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   299
  val case_eqns =
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   300
      map prove_case_eqn
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   301
         (List.concat con_ty_lists ~~ case_args ~~ tl con_defs);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   302
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   303
  (*** Prove the recursor theorems ***)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   304
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 30280
diff changeset
   305
  val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15461
diff changeset
   306
     NONE => (writeln "  [ No recursion operator ]";
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   307
              [])
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15461
diff changeset
   308
   | SOME recursor_def =>
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   309
      let
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   310
        (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
24826
78e6a3cea367 avoid unnamed infixes;
wenzelm
parents: 24725
diff changeset
   311
        fun subst_rec (Const(@{const_name apply},_) $ Free _ $ arg) = recursor_tm $ arg
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   312
          | subst_rec tm =
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   313
              let val (head, args) = strip_comb tm
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   314
              in  list_comb (head, map subst_rec args)  end;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   315
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   316
        (*Each equation has the form
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   317
          REC(coni(args)) = f_coni(args, REC(rec_arg), ...)
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   318
          where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   319
          constructor argument.*)
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   320
        fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   321
          FOLogic.mk_Trueprop
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   322
           (FOLogic.mk_eq
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   323
            (recursor_tm $
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 22101
diff changeset
   324
             (list_comb (Const (Sign.intern_const thy1 name,T),
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   325
                         args)),
18185
9d51fad6bb1f Term.betapplys;
wenzelm
parents: 17985
diff changeset
   326
             subst_rec (Term.betapplys (recursor_case, args))));
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   327
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24867
diff changeset
   328
        val recursor_trans = recursor_def RS @{thm def_Vrecursor} RS trans;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   329
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   330
        fun prove_recursor_eqn arg =
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 18728
diff changeset
   331
          Goal.prove_global thy1 [] []
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   332
            (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg))
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   333
            (*Proves a single recursor equation.*)
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   334
            (fn _ => EVERY
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   335
              [rtac recursor_trans 1,
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   336
               simp_tac (rank_ss addsimps case_eqns) 1,
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 18728
diff changeset
   337
               IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   338
      in
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   339
         map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases)
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   340
      end
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   341
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   342
  val constructors =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   343
      map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   344
12187
a1000fcf636e use proper intr_names (for required case_names);
wenzelm
parents: 12183
diff changeset
   345
  val free_SEs = map standard (Ind_Syntax.mk_free_SEs free_iffs);
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   346
6154
6a00a5baef2b automatic insertion of datatype intr rules into claset
paulson
parents: 6141
diff changeset
   347
  val {intrs, elim, induct, mutual_induct, ...} = ind_result
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   348
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   349
  (*Typical theorems have the form ~con1=con2, con1=con2==>False,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   350
    con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   351
  fun mk_free s =
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   352
    let val thy = theory_of_thm elim in (*Don't use thy1: it will be stale*)
24707
dfeb98f84e93 Syntax.parse/check/read;
wenzelm
parents: 24255
diff changeset
   353
      Goal.prove_global thy [] [] (Syntax.read_prop_global thy s)
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   354
        (fn _ => EVERY
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   355
         [rewrite_goals_tac con_defs,
20046
9c8909fc5865 Goal.prove_global;
wenzelm
parents: 18728
diff changeset
   356
          fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1])
17985
d5d576b72371 avoid legacy goals;
wenzelm
parents: 17959
diff changeset
   357
    end;
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   358
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   359
  val simps = case_eqns @ recursor_eqns;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   360
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   361
  val dt_info =
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   362
        {inductive = true,
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   363
         constructors = constructors,
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   364
         rec_rewrites = recursor_eqns,
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   365
         case_rewrites = case_eqns,
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   366
         induct = induct,
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   367
         mutual_induct = mutual_induct,
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   368
         exhaustion = elim};
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   369
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   370
  val con_info =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   371
        {big_rec_name = big_rec_name,
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   372
         constructors = constructors,
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   373
            (*let primrec handle definition by cases*)
12131
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   374
         free_iffs = free_iffs,
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   375
         rec_rewrites = (case recursor_eqns of
673bc8469a08 adapted to add_inductive_x;
wenzelm
parents: 9329
diff changeset
   376
                             [] => case_eqns | _ => recursor_eqns)};
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   377
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   378
  (*associate with each constructor the datatype name and rewrites*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   379
  val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   380
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   381
 in
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   382
  (*Updating theory components: simprules and datatype info*)
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24707
diff changeset
   383
  (thy1 |> Sign.add_path big_rec_base_name
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   384
        |> PureThy.add_thmss
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   385
         [((Binding.name "simps", simps), [Simplifier.simp_add]),
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   386
          ((Binding.empty , intrs), [Classical.safe_intro NONE]),
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   387
          ((Binding.name "con_defs", con_defs), []),
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   388
          ((Binding.name "case_eqns", case_eqns), []),
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   389
          ((Binding.name "recursor_eqns", recursor_eqns), []),
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   390
          ((Binding.name "free_iffs", free_iffs), []),
cb520b766e00 binding replaces bstring
haftmann
parents: 28965
diff changeset
   391
          ((Binding.name "free_elims", free_SEs), [])] |> snd
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
   392
        |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
   393
        |> ConstructorsData.map (fold Symtab.update con_pairs)
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24707
diff changeset
   394
        |> Sign.parent_path,
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   395
   ind_result,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   396
   {con_defs = con_defs,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   397
    case_eqns = case_eqns,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   398
    recursor_eqns = recursor_eqns,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   399
    free_iffs = free_iffs,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   400
    free_SEs = free_SEs,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   401
    mk_free = mk_free})
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   402
  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   403
17936
308b19d78764 removed obsolete add_datatype_x;
wenzelm
parents: 17412
diff changeset
   404
fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   405
  let
24725
04b676d1a1fe Attrib.eval_thms;
wenzelm
parents: 24712
diff changeset
   406
    val ctxt = ProofContext.init thy;
27261
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 26939
diff changeset
   407
    fun read_is strs =
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 26939
diff changeset
   408
      map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 26939
diff changeset
   409
      |> Syntax.check_terms ctxt;
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 26939
diff changeset
   410
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 26939
diff changeset
   411
    val rec_tms = read_is srec_tms;
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 26939
diff changeset
   412
    val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists;
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   413
    val dom_sum =
26189
9808cca5c54d misc cleanup of embedded ML code;
wenzelm
parents: 26056
diff changeset
   414
      if sdom = "" then data_domain coind (rec_tms, con_ty_lists)
27261
5b3101338f42 eliminated old Sign.read_term/Thm.read_cterm etc.;
wenzelm
parents: 26939
diff changeset
   415
      else singleton read_is sdom;
24725
04b676d1a1fe Attrib.eval_thms;
wenzelm
parents: 24712
diff changeset
   416
    val monos = Attrib.eval_thms ctxt raw_monos;
04b676d1a1fe Attrib.eval_thms;
wenzelm
parents: 24712
diff changeset
   417
    val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
04b676d1a1fe Attrib.eval_thms;
wenzelm
parents: 24712
diff changeset
   418
    val type_elims = Attrib.eval_thms ctxt raw_type_elims;
04b676d1a1fe Attrib.eval_thms;
wenzelm
parents: 24712
diff changeset
   419
  in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end;
04b676d1a1fe Attrib.eval_thms;
wenzelm
parents: 24712
diff changeset
   420
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   421
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   422
(* outer syntax *)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   423
17057
0934ac31985f OuterKeyword;
wenzelm
parents: 15705
diff changeset
   424
local structure P = OuterParse and K = OuterKeyword in
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   425
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   426
fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   427
  #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   428
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   429
val con_decl =
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   430
  P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12243
diff changeset
   431
  >> P.triple1;
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   432
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   433
val datatype_decl =
25985
8d69087f6a4b avoid redundant escaping of Isabelle symbols;
wenzelm
parents: 24893
diff changeset
   434
  (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   435
  P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21350
diff changeset
   436
  Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] --
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21350
diff changeset
   437
  Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] --
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21350
diff changeset
   438
  Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) []
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   439
  >> (Toplevel.theory o mk_datatype);
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   440
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   441
val coind_prefix = if coind then "co" else "";
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   442
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24826
diff changeset
   443
val _ = OuterSyntax.command (coind_prefix ^ "datatype")
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   444
  ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   445
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   446
end;
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   447
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12131
diff changeset
   448
end;
15705
b5edb9dcec9a *** MESSAGE REFERS TO PREVIOUS VERSION ***
wenzelm
parents: 15703
diff changeset
   449