src/ZF/thy_syntax.ML
author nipkow
Sun, 05 Jan 2003 21:03:14 +0100
changeset 13771 6cd59cc885a1
parent 12183 c10cea75dd56
child 14598 7009f59711e3
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     1
(*  Title:      ZF/thy_syntax.ML
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     2
    ID:         $Id$
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     5
12050
6934c005aec4 tuned comment;
wenzelm
parents: 8813
diff changeset
     6
Additional sections for *old-style* theory files in ZF.
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     7
*)
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
     8
3622
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3613
diff changeset
     9
local
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    10
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    11
open ThyParse;
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    12
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    13
fun mk_bind suffix s =
6093
87bf8c03b169 eliminated global/local names;
wenzelm
parents: 6070
diff changeset
    14
    if ThmDatabase.is_ml_identifier s then
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    15
        "op " ^ s ^ suffix  (*the "op" cancels any infix status*)
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    16
    else "_";               (*bad name, don't try to bind*)
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    17
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    18
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    19
(*For lists of theorems.  Either a string (an ML list expression) or else
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    20
  a list of identifiers.*)
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    21
fun optlist s =
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    22
    optional (s $$--
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    23
              (string >> unenclose
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    24
               || list1 (name>>unenclose) >> mk_list))
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    25
    "[]";
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    26
8813
abc0f3722aed added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents: 8127
diff changeset
    27
(*Skipping initial blanks, find the first identifier*)  (* FIXME slightly broken! *)
abc0f3722aed added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents: 8127
diff changeset
    28
fun scan_to_id s =
abc0f3722aed added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents: 8127
diff changeset
    29
    s |> Symbol.explode
abc0f3722aed added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents: 8127
diff changeset
    30
    |> Scan.error (Scan.finite Symbol.stopper
abc0f3722aed added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents: 8127
diff changeset
    31
      (Scan.!! (fn _ => "Expected to find an identifier in " ^ s)
abc0f3722aed added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents: 8127
diff changeset
    32
        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
abc0f3722aed added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents: 8127
diff changeset
    33
    |> #1;
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    34
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    35
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    36
(* (Co)Inductive definitions *)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    37
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    38
fun inductive_decl coind =
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    39
  let
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    40
    fun mk_params ((((((recs, sdom_sum), ipairs),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1428
diff changeset
    41
                      monos), con_defs), type_intrs), type_elims) =
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    42
      let val big_rec_name = space_implode "_"
6642
732af87c0650 strip_quotes replaced by unenclose;
wenzelm
parents: 6112
diff changeset
    43
                           (map (scan_to_id o unenclose) recs)
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    44
          and srec_tms = mk_list recs
12132
1ef58b332ca9 support co/inductive definitions in new-style theories;
wenzelm
parents: 12050
diff changeset
    45
          and sintrs   =
1ef58b332ca9 support co/inductive definitions in new-style theories;
wenzelm
parents: 12050
diff changeset
    46
            mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs)
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    47
          and inames   = mk_list (map (mk_bind "" o fst) ipairs)
1428
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    48
      in
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    49
         ";\n\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    50
         \local\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    51
         \val (thy, {defs, intrs, elim, mk_cases, \
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    52
                    \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    53
         \  " ^
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    54
         (if coind then "Co" else "") ^
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    55
         "Ind_Package.add_inductive_x (" ^  srec_tms ^ ", " ^ sdom_sum ^ ") " ^ sintrs ^
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    56
           " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    57
         \in\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    58
         \structure " ^ big_rec_name ^ " =\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    59
         \struct\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    60
         \  val defs = defs\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    61
         \  val bnd_mono = bnd_mono\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    62
         \  val dom_subset = dom_subset\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    63
         \  val intrs = intrs\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    64
         \  val elim = elim\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    65
         \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    66
         \  val mutual_induct = mutual_induct\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    67
         \  val mk_cases = mk_cases\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    68
         \  val " ^ inames ^ " = intrs\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    69
         \end;\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    70
         \val thy = thy;\nend;\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    71
         \val thy = thy\n"
1428
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    72
      end
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    73
    val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
15a69dd0a145 Reduced indentation; no change in function
paulson
parents: 1418
diff changeset
    74
    val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    75
  in domains -- ipairs -- optlist "monos" -- optlist "con_defs"
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    76
             -- optlist "type_intrs" -- optlist "type_elims"
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    77
     >> mk_params
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    78
  end;
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    79
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
    80
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    81
(* Datatype definitions *)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    82
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    83
fun datatype_decl coind =
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    84
  let
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    85
    fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    86
    val mk_data = mk_list o map mk_const o snd
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    87
    val mk_scons = mk_big_list o map mk_data
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    88
    fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
6642
732af87c0650 strip_quotes replaced by unenclose;
wenzelm
parents: 6112
diff changeset
    89
      let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    90
          val big_rec_name = space_implode "_" rec_names
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    91
          and srec_tms = mk_list (map fst rec_pairs)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    92
          and scons    = mk_scons rec_pairs
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    93
          val con_names = flat (map (map (unenclose o #1 o #1) o snd)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    94
                                rec_pairs)
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    95
          val inames = mk_list (map (mk_bind "_I") con_names)
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
    96
      in
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    97
         ";\n\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    98
         \local\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
    99
         \val (thy,\n\
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   100
         \     {defs, intrs, elim, mk_cases, \
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   101
                    \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   102
         \     {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   103
         \  " ^
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   104
         (if coind then "Co" else "") ^
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   105
         "Data_Package.add_datatype_x (" ^  sdom ^ ", " ^ srec_tms ^ ") " ^ scons ^
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   106
           " (" ^ monos ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   107
         \in\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   108
         \structure " ^ big_rec_name ^ " =\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   109
         \struct\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   110
         \  val defs = defs\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   111
         \  val bnd_mono = bnd_mono\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   112
         \  val dom_subset = dom_subset\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   113
         \  val intrs = intrs\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   114
         \  val elim = elim\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   115
         \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   116
         \  val mutual_induct = mutual_induct\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   117
         \  val mk_cases = mk_cases\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   118
         \  val con_defs = con_defs\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   119
         \  val case_eqns = case_eqns\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   120
         \  val recursor_eqns = recursor_eqns\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   121
         \  val free_iffs = free_iffs\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   122
         \  val free_SEs = free_SEs\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   123
         \  val mk_free = mk_free\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   124
         \  val " ^ inames ^ " = intrs;\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   125
         \end;\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   126
         \val thy = thy;\nend;\n\
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   127
         \val thy = thy\n"
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   128
      end
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   129
    val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   130
    val construct = name -- string_list -- opt_mixfix;
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   131
  in optional ("<=" $$-- string) "\"\"" --
8127
68c6159440f1 new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
paulson
parents: 6642
diff changeset
   132
     enum1 "and" (name --$$ "=" -- enum1 "|" construct) --
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   133
     optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   134
     >> mk_params
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   135
end;
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   136
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   137
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   138
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   139
(** rep_datatype **)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   140
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   141
fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) =
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   142
  "|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n    " ^
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   143
  mk_list case_eqns ^ " " ^ mk_list recursor_eqns;
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   144
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   145
val rep_datatype_decl =
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   146
  (("elim" $$-- ident) --
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   147
   ("induct" $$-- ident) --
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   148
   ("case_eqns" $$-- list1 ident) --
6112
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
   149
   optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string;
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   150
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   151
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   152
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   153
(** primrec **)
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   154
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   155
fun mk_primrec_decl eqns =
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   156
  let val binds = map (mk_bind "" o fst) eqns in
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   157
    ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   158
      mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   159
    \val thy = thy\n"
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   160
  end;
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   161
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   162
(* either names and axioms or just axioms *)
12183
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   163
val primrec_decl =
c10cea75dd56 adapted primrec/datatype to Isar;
wenzelm
parents: 12132
diff changeset
   164
    ((repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   165
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3925
diff changeset
   166
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   167
3622
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3613
diff changeset
   168
(** augment thy syntax **)
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3613
diff changeset
   169
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3613
diff changeset
   170
in
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   171
3622
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3613
diff changeset
   172
val _ = ThySyn.add_syntax
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3613
diff changeset
   173
 ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   174
  "<=", "domains", "intrs", "monos", "con_defs", "type_intrs", "type_elims",
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   175
  (*rep_datatype*)
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   176
  "elim", "induct", "case_eqns", "recursor_eqns"]
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   177
 [section "inductive"    "" (inductive_decl false),
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   178
  section "coinductive"  "" (inductive_decl true),
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   179
  section "datatype"     "" (datatype_decl false),
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   180
  section "codatatype"   "" (datatype_decl true),
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   181
  section "rep_datatype" "" rep_datatype_decl,
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 6053
diff changeset
   182
  section "primrec"      "" primrec_decl];
3622
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3613
diff changeset
   183
797
713efca1f0aa Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff changeset
   184
end;