src/HOL/thy_syntax.ML
author wenzelm
Tue Jan 12 16:42:21 1999 +0100 (1999-01-12)
changeset 6103 36f272ea9413
parent 6035 c041fc54ab4c
child 6356 6c01697e082e
permissions -rw-r--r--
get_tthms witness theorems;
clasohm@923
     1
(*  Title:      HOL/thy_syntax.ML
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author:     Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
clasohm@923
     4
clasohm@923
     5
Additional theory file sections for HOL.
clasohm@923
     6
*)
clasohm@923
     7
wenzelm@3622
     8
local
clasohm@923
     9
clasohm@923
    10
open ThyParse;
clasohm@923
    11
clasohm@923
    12
clasohm@1475
    13
(** typedef **)
clasohm@923
    14
clasohm@1475
    15
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
clasohm@923
    16
  let
clasohm@923
    17
    val name' = if_none opt_name t;
clasohm@923
    18
    val name = strip_quotes name';
clasohm@923
    19
  in
clasohm@923
    20
    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
clasohm@923
    21
      [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
clasohm@923
    22
        "Abs_" ^ name ^ "_inverse"])
clasohm@923
    23
  end;
clasohm@923
    24
clasohm@1475
    25
val typedef_decl =
clasohm@923
    26
  optional ("(" $$-- name --$$ ")" >> Some) None --
clasohm@923
    27
  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
clasohm@1475
    28
  >> mk_typedef_decl;
clasohm@923
    29
clasohm@923
    30
clasohm@923
    31
wenzelm@3980
    32
(** record **)
wenzelm@3980
    33
wenzelm@3980
    34
val record_decl =
wenzelm@4225
    35
  (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "="
wenzelm@4226
    36
    -- optional (typ --$$ "+" >> (parens o cat "Some")) "None"
wenzelm@4225
    37
    -- repeat1 ((name --$$ "::" -- typ) >> mk_pair)
wenzelm@4001
    38
  >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
wenzelm@3980
    39
wenzelm@3980
    40
clasohm@923
    41
(** (co)inductive **)
clasohm@923
    42
berghofe@5097
    43
fun inductive_decl coind =
clasohm@923
    44
  let
clasohm@923
    45
    fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
clasohm@923
    46
      if Syntax.is_identifier s then "op " ^ s else "_";
clasohm@923
    47
    fun mk_params (((recs, ipairs), monos), con_defs) =
paulson@6035
    48
      let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
clasohm@923
    49
          and srec_tms = mk_list recs
clasohm@923
    50
          and sintrs   = mk_big_list (map snd ipairs)
clasohm@923
    51
      in
berghofe@5097
    52
        ";\n\n\
berghofe@5097
    53
        \local\n\
berghofe@5097
    54
        \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
berghofe@5097
    55
        \  InductivePackage.add_inductive true " ^
berghofe@5097
    56
        (if coind then "true " else "false ") ^ srec_tms ^ " " ^
berghofe@5716
    57
         sintrs ^ " " ^ mk_list monos ^ " " ^ mk_list con_defs ^ " thy;\n\
berghofe@5097
    58
        \in\n\
berghofe@5097
    59
        \structure " ^ big_rec_name ^ " =\n\
berghofe@5097
    60
        \struct\n\
berghofe@5097
    61
        \  val defs = defs;\n\
berghofe@5097
    62
        \  val mono = mono;\n\
berghofe@5097
    63
        \  val unfold = unfold;\n\
berghofe@5097
    64
        \  val intrs = intrs;\n\
berghofe@5097
    65
        \  val elims = elims;\n\
berghofe@5097
    66
        \  val elim = hd elims;\n\
berghofe@5097
    67
        \  val " ^ (if coind then "co" else "") ^ "induct = induct;\n\
berghofe@5097
    68
        \  val mk_cases = mk_cases;\n\
berghofe@5097
    69
        \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\
berghofe@5097
    70
        \end;\n\
berghofe@5097
    71
        \val thy = thy;\nend;\n\
berghofe@5097
    72
        \val thy = thy\n"
clasohm@923
    73
      end
clasohm@923
    74
    val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
berghofe@5716
    75
    fun optlist s = optional (s $$-- list1 name) []
clasohm@923
    76
  in
berghofe@5716
    77
    repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs"
clasohm@923
    78
      >> mk_params
clasohm@923
    79
  end;
clasohm@923
    80
clasohm@923
    81
clasohm@923
    82
(** datatype **)
clasohm@923
    83
clasohm@923
    84
local
berghofe@5183
    85
  (*** generate string for calling add_datatype ***)
berghofe@5183
    86
  (*** and bindig theorems to ML identifiers    ***)
clasohm@923
    87
berghofe@5183
    88
  fun mk_bind_thms_string names =
berghofe@5183
    89
   (case find_first (not o Syntax.is_identifier) names of
berghofe@5183
    90
      Some id => (warning (id ^ " is not a valid identifier"); "")
berghofe@5183
    91
    | None =>
berghofe@5183
    92
        let
berghofe@5183
    93
          fun mk_dt_struct (s, (id, i)) =
berghofe@5183
    94
            s ^ "structure " ^ id ^ " =\n\
berghofe@5183
    95
            \struct\n\
berghofe@5183
    96
            \  val distinct = nth_elem (" ^ i ^ ", distinct);\n\
berghofe@5183
    97
            \  val inject = nth_elem (" ^ i ^ ", inject);\n\
berghofe@5183
    98
            \  val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\
berghofe@5183
    99
            \  val cases = nth_elem (" ^ i ^ ", case_thms);\n\
berghofe@5183
   100
            \  val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^
berghofe@5183
   101
              (if length names = 1 then
berghofe@5183
   102
                 "  val induct = induction;\n\
berghofe@5183
   103
                 \  val recs = rec_thms;\n\
berghofe@5183
   104
                 \  val simps = simps;\n\
berghofe@5183
   105
                 \  val size = size;\n"
berghofe@5183
   106
               else "") ^
berghofe@5183
   107
            "end;\n";
berghofe@5183
   108
berghofe@5183
   109
          val structs = foldl mk_dt_struct
berghofe@5183
   110
            ("", (names ~~ (map string_of_int (0 upto length names - 1))));
berghofe@5183
   111
berghofe@5183
   112
        in
berghofe@5183
   113
          (if length names > 1 then
berghofe@5183
   114
             "structure " ^ (space_implode "_" names) ^ " =\n\
berghofe@5183
   115
             \struct\n\
berghofe@5658
   116
             \  val induct = induction;\n\
berghofe@5658
   117
             \  val recs = rec_thms;\n\
berghofe@5658
   118
             \  val simps = simps;\n\
berghofe@5658
   119
             \  val size = size;\nend;\n"
berghofe@5658
   120
           else "") ^ structs
berghofe@5183
   121
        end);
berghofe@5183
   122
berghofe@5183
   123
  fun mk_dt_string dts =
clasohm@923
   124
    let
berghofe@5183
   125
      val names = map (fn ((((alt_name, _), name), _), _) =>
berghofe@5183
   126
        strip_quotes (if_none alt_name name)) dts;
berghofe@5183
   127
berghofe@5183
   128
      val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
berghofe@5183
   129
        brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
berghofe@5183
   130
          parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
berghofe@5183
   131
            brackets (commas cs))) dts));
berghofe@5183
   132
clasohm@923
   133
    in
berghofe@5183
   134
      ";\nlocal\n\
berghofe@5183
   135
      \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
berghofe@5183
   136
      \  case_thms, split_thms, induction, size, simps}) =\n\
wenzelm@6103
   137
      \ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
berghofe@5183
   138
      \in\n" ^ mk_bind_thms_string names ^
berghofe@5183
   139
      "val thy = thy;\nend;\nval thy = thy\n"
clasohm@923
   140
    end;
clasohm@923
   141
wenzelm@6103
   142
  fun mk_thmss namess = "(map (PureThy.get_thmss thy) " ^ mk_list (map mk_list namess) ^ ")";
wenzelm@6103
   143
  fun mk_thm name = "(PureThy.get_thm thy " ^ name ^ ")";
wenzelm@6103
   144
berghofe@5183
   145
  fun mk_rep_dt_string (((names, distinct), inject), induct) =
berghofe@5183
   146
    ";\nlocal\n\
berghofe@5183
   147
    \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
berghofe@5183
   148
    \  case_thms, split_thms, induction, size, simps}) =\n\
wenzelm@6103
   149
    \ DatatypePackage.rep_datatype " ^
berghofe@5183
   150
    (case names of
wenzelm@6103
   151
        Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
wenzelm@6103
   152
          mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
wenzelm@6103
   153
            "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
wenzelm@6103
   154
      | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
wenzelm@6103
   155
            "\n " ^ mk_thm induct ^ " thy;\nin\n") ^
berghofe@5183
   156
    "val thy = thy;\nend;\nval thy = thy\n";
clasohm@923
   157
berghofe@5183
   158
  (*** parsers ***)
wenzelm@4106
   159
berghofe@5183
   160
  val simple_typ = ident || (type_var >> strip_quotes);
clasohm@1316
   161
clasohm@1251
   162
  fun complex_typ toks =
clasohm@1316
   163
    let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
clasohm@1316
   164
        val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
clasohm@1316
   165
    in
berghofe@5183
   166
     (typ ^^ (repeat ident >> (cat "" o space_implode " ")) ||
berghofe@5183
   167
      "(" $$-- !! (list1 typ2 >> (parens o commas)) --$$ ")" ^^ !!
berghofe@5183
   168
        (repeat1 ident >> (cat "" o space_implode " "))) toks
clasohm@1316
   169
    end;
clasohm@1316
   170
berghofe@5183
   171
  val opt_typs = repeat ((string >> strip_quotes) ||
berghofe@5183
   172
    simple_typ || ("(" $$-- complex_typ --$$ ")"));
berghofe@5183
   173
  val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
berghofe@5716
   174
    parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
berghofe@5183
   175
  val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
berghofe@5183
   176
berghofe@5716
   177
  fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]]
berghofe@5716
   178
clasohm@923
   179
in
clasohm@923
   180
  val datatype_decl =
berghofe@5183
   181
    enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
berghofe@5183
   182
      enum1 "|" constructor) >> mk_dt_string;
berghofe@5183
   183
  val rep_datatype_decl =
berghofe@5183
   184
    ((optional ((repeat1 (name >> strip_quotes)) >> Some) None) --
berghofe@5716
   185
      optlistlist "distinct" -- optlistlist "inject" --
berghofe@5716
   186
        ("induct" $$-- name)) >> mk_rep_dt_string;
clasohm@923
   187
end;
clasohm@923
   188
clasohm@923
   189
clasohm@923
   190
(** primrec **)
clasohm@923
   191
berghofe@5716
   192
fun mk_primrec_decl (alt_name, eqns) =
berghofe@5716
   193
  let
berghofe@5716
   194
    val names = map (fn (s, _) => if s = "" then "_" else s) eqns
berghofe@5716
   195
  in
berghofe@5716
   196
    ";\nval (thy, " ^ mk_list names ^
berghofe@5716
   197
    ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
berghofe@5716
   198
      mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
berghofe@5716
   199
    \val thy = thy\n"
berghofe@5716
   200
  end;
clasohm@923
   201
berghofe@5183
   202
(* either names and axioms or just axioms *)
berghofe@5716
   203
val primrec_decl = (optional ("(" $$-- name --$$ ")") "\"\"" --
berghofe@5716
   204
  (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
clasohm@923
   205
paulson@2922
   206
paulson@2922
   207
(** rec: interface to Slind's TFL **)
paulson@2922
   208
paulson@2922
   209
paulson@3194
   210
(*fname: name of function being defined; rel: well-founded relation*)
paulson@3456
   211
fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
paulson@6035
   212
  let val fid = strip_quotes fname
paulson@3194
   213
      val intrnl_name = fid ^ "_Intrnl"
paulson@2922
   214
  in
paulson@2922
   215
	 (";\n\n\
paulson@3194
   216
          \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
paulson@3194
   217
          \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
paulson@3345
   218
	                 quote fid ^ " " ^ 
paulson@3194
   219
	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
paulson@2922
   220
          \val thy = thy"
paulson@2922
   221
         ,
paulson@3194
   222
          "structure " ^ fid ^ " =\n\
paulson@3194
   223
          \  struct\n\
paulson@3194
   224
          \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
paulson@3194
   225
          \  val {rules, induct, tcs} = \n\
paulson@3456
   226
          \    \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
paulson@3456
   227
          \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
paulson@3194
   228
          \  end;\n\
paulson@3194
   229
          \val pats_" ^ intrnl_name ^ " = ();\n")
paulson@2922
   230
  end;
paulson@2922
   231
paulson@6035
   232
val rec_decl = 
paulson@6035
   233
    (name -- string -- 
paulson@6035
   234
     optional ("congs" $$-- string >> strip_quotes) "[]" -- 
paulson@6035
   235
     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
paulson@6035
   236
     repeat1 string >> mk_rec_decl) ;
paulson@2922
   237
paulson@2922
   238
paulson@2922
   239
wenzelm@3622
   240
(** augment thy syntax **)
clasohm@923
   241
wenzelm@3622
   242
in
clasohm@923
   243
wenzelm@3622
   244
val _ = ThySyn.add_syntax
berghofe@5183
   245
 ["intrs", "monos", "con_defs", "congs", "simpset", "|",
berghofe@5183
   246
  "and", "distinct", "inject", "induct"]
wenzelm@4873
   247
 [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
berghofe@5097
   248
  section "record" "|> RecordPackage.add_record" record_decl,
berghofe@5097
   249
  section "inductive" "" (inductive_decl false),
berghofe@5097
   250
  section "coinductive" "" (inductive_decl true),
berghofe@5097
   251
  section "datatype" "" datatype_decl,
berghofe@5183
   252
  section "rep_datatype" "" rep_datatype_decl,
berghofe@5183
   253
  section "primrec" "" primrec_decl,
paulson@2922
   254
  ("recdef", rec_decl)];
clasohm@923
   255
clasohm@923
   256
end;