src/HOL/thy_syntax.ML
author berghofe
Tue Jun 30 20:42:47 1998 +0200 (1998-06-30)
changeset 5097 6c4a7ad6ebc7
parent 4873 b5999638979e
child 5183 89f162de39cf
permissions -rw-r--r--
Adapted to new inductive definition package.
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
clasohm@923
     8
(*the kind of distinctiveness axioms depends on number of constructors*)
nipkow@2930
     9
val dtK = 7;  (* FIXME rename?, move? *)
clasohm@923
    10
wenzelm@3622
    11
wenzelm@3622
    12
local
clasohm@923
    13
clasohm@923
    14
open ThyParse;
clasohm@923
    15
clasohm@923
    16
clasohm@1475
    17
(** typedef **)
clasohm@923
    18
clasohm@1475
    19
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
clasohm@923
    20
  let
clasohm@923
    21
    val name' = if_none opt_name t;
clasohm@923
    22
    val name = strip_quotes name';
clasohm@923
    23
  in
clasohm@923
    24
    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
clasohm@923
    25
      [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
clasohm@923
    26
        "Abs_" ^ name ^ "_inverse"])
clasohm@923
    27
  end;
clasohm@923
    28
clasohm@1475
    29
val typedef_decl =
clasohm@923
    30
  optional ("(" $$-- name --$$ ")" >> Some) None --
clasohm@923
    31
  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
clasohm@1475
    32
  >> mk_typedef_decl;
clasohm@923
    33
clasohm@923
    34
clasohm@923
    35
wenzelm@3980
    36
(** record **)
wenzelm@3980
    37
wenzelm@3980
    38
val record_decl =
wenzelm@4225
    39
  (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "="
wenzelm@4226
    40
    -- optional (typ --$$ "+" >> (parens o cat "Some")) "None"
wenzelm@4225
    41
    -- repeat1 ((name --$$ "::" -- typ) >> mk_pair)
wenzelm@4001
    42
  >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
wenzelm@3980
    43
wenzelm@3980
    44
clasohm@923
    45
(** (co)inductive **)
clasohm@923
    46
berghofe@5097
    47
fun inductive_decl coind =
clasohm@923
    48
  let
clasohm@923
    49
    fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
clasohm@923
    50
      if Syntax.is_identifier s then "op " ^ s else "_";
clasohm@923
    51
    fun mk_params (((recs, ipairs), monos), con_defs) =
clasohm@923
    52
      let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
clasohm@923
    53
          and srec_tms = mk_list recs
clasohm@923
    54
          and sintrs   = mk_big_list (map snd ipairs)
clasohm@923
    55
      in
berghofe@5097
    56
        ";\n\n\
berghofe@5097
    57
        \local\n\
berghofe@5097
    58
        \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
berghofe@5097
    59
        \  InductivePackage.add_inductive true " ^
berghofe@5097
    60
        (if coind then "true " else "false ") ^ srec_tms ^ " " ^
berghofe@5097
    61
         sintrs ^ " " ^ monos ^ " " ^ con_defs ^ " thy;\n\
berghofe@5097
    62
        \in\n\
berghofe@5097
    63
        \structure " ^ big_rec_name ^ " =\n\
berghofe@5097
    64
        \struct\n\
berghofe@5097
    65
        \  val defs = defs;\n\
berghofe@5097
    66
        \  val mono = mono;\n\
berghofe@5097
    67
        \  val unfold = unfold;\n\
berghofe@5097
    68
        \  val intrs = intrs;\n\
berghofe@5097
    69
        \  val elims = elims;\n\
berghofe@5097
    70
        \  val elim = hd elims;\n\
berghofe@5097
    71
        \  val " ^ (if coind then "co" else "") ^ "induct = induct;\n\
berghofe@5097
    72
        \  val mk_cases = mk_cases;\n\
berghofe@5097
    73
        \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\
berghofe@5097
    74
        \end;\n\
berghofe@5097
    75
        \val thy = thy;\nend;\n\
berghofe@5097
    76
        \val thy = thy\n"
clasohm@923
    77
      end
clasohm@923
    78
    val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
paulson@3403
    79
    fun optstring s = optional (s $$-- string >> trim) "[]"
clasohm@923
    80
  in
paulson@1788
    81
    repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
clasohm@923
    82
      >> mk_params
clasohm@923
    83
  end;
clasohm@923
    84
clasohm@923
    85
clasohm@923
    86
(** datatype **)
clasohm@923
    87
clasohm@923
    88
local
clasohm@923
    89
  (* FIXME err -> add_datatype *)
clasohm@923
    90
  fun mk_cons cs =
clasohm@923
    91
    (case duplicates (map (fst o fst) cs) of
clasohm@923
    92
      [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
clasohm@923
    93
    | dups => error ("Duplicate constructors: " ^ commas_quote dups));
clasohm@923
    94
clasohm@923
    95
  (*generate names of distinctiveness axioms*)
clasohm@923
    96
  fun mk_distinct_rules cs tname =
clasohm@923
    97
    let
clasohm@923
    98
      val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
clasohm@923
    99
      (*combine all constructor names with all others w/o duplicates*)
clasohm@923
   100
      fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
clasohm@923
   101
      fun neg1 [] = []
clasohm@923
   102
        | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
clasohm@923
   103
    in
clasohm@923
   104
      if length uqcs < dtK then neg1 uqcs
clasohm@923
   105
      else quote (tname ^ "_ord_distinct") ::
clasohm@923
   106
        map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
clasohm@923
   107
    end;
clasohm@923
   108
clasohm@923
   109
  fun mk_rules tname cons pre = " map (get_axiom thy) " ^
paulson@3194
   110
    mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
clasohm@923
   111
clasohm@1668
   112
  (*generate string for calling add_datatype and build_record*)
clasohm@923
   113
  fun mk_params ((ts, tname), cons) =
nipkow@4184
   114
    "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqns) =\n\
nipkow@4032
   115
    \    Datatype.add_datatype\n"
clasohm@923
   116
    ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
wenzelm@4106
   117
    \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\
wenzelm@4106
   118
    \val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
nipkow@3665
   119
    \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
nipkow@3665
   120
    \structure " ^ tname ^ " =\n\
clasohm@923
   121
    \struct\n\
clasohm@923
   122
    \ val inject = map (get_axiom thy) " ^
clasohm@923
   123
        mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
clasohm@923
   124
          (filter_out (null o snd o fst) cons)) ^ ";\n\
clasohm@923
   125
    \ val distinct = " ^
clasohm@923
   126
        (if length cons < dtK then "let val distinct' = " else "") ^
clasohm@923
   127
        "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
clasohm@923
   128
        (if length cons < dtK then
clasohm@923
   129
          "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
clasohm@923
   130
          \ distinct') end"
clasohm@923
   131
         else "") ^ ";\n\
clasohm@923
   132
    \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
clasohm@923
   133
    \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
clasohm@923
   134
    \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
clasohm@923
   135
    \ val simps = inject @ distinct @ cases @ recs;\n\
clasohm@923
   136
    \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
clasohm@1264
   137
    \end;\n\
wenzelm@4106
   138
    \val thy = thy |> Dtype.add_record " ^
wenzelm@4106
   139
      mk_triple
wenzelm@4106
   140
        ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
wenzelm@4106
   141
          mk_list (map (fst o fst) cons),
wenzelm@4106
   142
          tname ^ ".induct_tac") ^ ";\n\
wenzelm@4106
   143
    \val dummy = context thy;\n\
nipkow@2930
   144
    \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
nipkow@2930
   145
    \val dummy = AddIffs " ^ tname ^ ".inject;\n\
nipkow@2930
   146
    \val dummy = " ^
nipkow@2930
   147
      (if length cons < dtK then "AddIffs " else "Addsimps ") ^
nipkow@3308
   148
      tname ^ ".distinct;\n\
nipkow@3308
   149
    \val dummy = Addsimps(map (fn (_,eqn) =>\n\
nipkow@3308
   150
    \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
nipkow@4032
   151
                     "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
nipkow@4184
   152
    \val split_"^tname^"_case = prove_goal thy (#1(split_"^tname^"_eqns))\n\
nipkow@4184
   153
    \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
nipkow@4184
   154
      ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
nipkow@4184
   155
    \            ALLGOALS Asm_simp_tac]);\n\
oheimb@4204
   156
    \val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
wenzelm@4106
   157
    \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
wenzelm@4106
   158
      ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
oheimb@4536
   159
    \            ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex]))]);\n\
wenzelm@4106
   160
    \val thy = thy\n";
wenzelm@4106
   161
nipkow@4032
   162
(*
nipkow@4032
   163
The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
nipkow@4032
   164
is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
nipkow@4032
   165
specific exhaustion tactic from the theory associated with the proof
nipkow@4032
   166
state. However, the exhaustion tactic for the current datatype has only just
nipkow@4032
   167
been added to !datatypes (a few lines above) but is not yet associated with
nipkow@4032
   168
the theory. Hope this can be simplified in the future.
nipkow@4032
   169
*)
clasohm@923
   170
clasohm@923
   171
  (*parsers*)
clasohm@923
   172
  val tvars = type_args >> map (cat "dtVar");
clasohm@1316
   173
clasohm@1316
   174
  val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
clasohm@1316
   175
    type_var >> cat "dtVar";
clasohm@1316
   176
clasohm@1251
   177
  fun complex_typ toks =
clasohm@1316
   178
    let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
clasohm@1316
   179
        val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
clasohm@1316
   180
    in
clasohm@1316
   181
     (typ -- repeat (ident>>quote) >>
clasohm@1316
   182
        (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
clasohm@1316
   183
      "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
clasohm@1316
   184
       (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
clasohm@1316
   185
                         mk_pair (brackets x, y)) (commas fst, ids))) toks
clasohm@1316
   186
    end;
clasohm@1316
   187
clasohm@977
   188
  val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
clasohm@923
   189
  val constructor = name -- opt_typs -- opt_mixfix;
clasohm@923
   190
in
clasohm@923
   191
  val datatype_decl =
clasohm@923
   192
    tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
clasohm@923
   193
end;
clasohm@923
   194
clasohm@923
   195
clasohm@923
   196
clasohm@923
   197
(** primrec **)
clasohm@923
   198
paulson@2922
   199
(*recursion equations have user-supplied names*)
berghofe@1845
   200
fun mk_primrec_decl_1 ((fname, tname), axms) =
clasohm@923
   201
  let
clasohm@1574
   202
    (*Isolate type name from the structure's identifier it may be stored in*)
clasohm@1574
   203
    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
clasohm@1574
   204
clasohm@923
   205
    fun mk_prove (name, eqn) =
clasohm@1264
   206
      "val " ^ name ^ " = store_thm (" ^ quote name
clasohm@1574
   207
      ^ ", prove_goalw thy [get_def thy "
clasohm@1574
   208
      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
clasohm@1264
   209
      \  (fn _ => [Simp_tac 1]));";
clasohm@1264
   210
clasohm@923
   211
    val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
paulson@2922
   212
  in ("|> " ^ tname ^ "_add_primrec " ^ axs
paulson@2922
   213
      , 
paulson@2922
   214
      cat_lines (map mk_prove axms)
clasohm@1264
   215
      ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
clasohm@1264
   216
  end;
clasohm@923
   217
paulson@2922
   218
(*recursion equations have no names*)
berghofe@1845
   219
fun mk_primrec_decl_2 ((fname, tname), axms) =
berghofe@1845
   220
  let
berghofe@1845
   221
    (*Isolate type name from the structure's identifier it may be stored in*)
berghofe@1845
   222
    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
berghofe@1845
   223
berghofe@1845
   224
    fun mk_prove eqn =
berghofe@1845
   225
      "prove_goalw thy [get_def thy "
berghofe@1845
   226
      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
berghofe@1845
   227
      \(fn _ => [Simp_tac 1])";
berghofe@1845
   228
berghofe@1845
   229
    val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
paulson@2922
   230
  in ("|> " ^ tname ^ "_add_primrec " ^ axs
paulson@2922
   231
      ,
berghofe@1845
   232
      "val dummy = Addsimps " ^
berghofe@1845
   233
      brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
berghofe@1845
   234
  end;
berghofe@1845
   235
paulson@2922
   236
(*function name, argument type and either (name,axiom) pairs or just axioms*)
clasohm@923
   237
val primrec_decl =
berghofe@1845
   238
  (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
berghofe@1845
   239
  (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
clasohm@923
   240
clasohm@923
   241
clasohm@923
   242
paulson@2922
   243
paulson@2922
   244
(** rec: interface to Slind's TFL **)
paulson@2922
   245
paulson@2922
   246
paulson@3194
   247
(*fname: name of function being defined; rel: well-founded relation*)
paulson@3456
   248
fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
paulson@2922
   249
  let val fid = trim fname
paulson@3194
   250
      val intrnl_name = fid ^ "_Intrnl"
paulson@2922
   251
  in
paulson@2922
   252
	 (";\n\n\
paulson@3194
   253
          \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
paulson@3194
   254
          \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
paulson@3345
   255
	                 quote fid ^ " " ^ 
paulson@3194
   256
	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
paulson@2922
   257
          \val thy = thy"
paulson@2922
   258
         ,
paulson@3194
   259
          "structure " ^ fid ^ " =\n\
paulson@3194
   260
          \  struct\n\
paulson@3194
   261
          \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
paulson@3194
   262
          \  val {rules, induct, tcs} = \n\
paulson@3456
   263
          \    \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
paulson@3456
   264
          \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
paulson@3194
   265
          \  end;\n\
paulson@3194
   266
          \val pats_" ^ intrnl_name ^ " = ();\n")
paulson@2922
   267
  end;
paulson@2922
   268
paulson@3403
   269
val rec_decl = (name -- string -- 
paulson@3456
   270
		optional ("congs" $$-- string >> trim) "[]" -- 
wenzelm@4091
   271
		optional ("simpset" $$-- string >> trim) "simpset()" -- 
paulson@3403
   272
		repeat1 string >> mk_rec_decl) ;
paulson@2922
   273
paulson@2922
   274
paulson@2922
   275
wenzelm@3622
   276
(** augment thy syntax **)
clasohm@923
   277
wenzelm@3622
   278
in
clasohm@923
   279
wenzelm@3622
   280
val _ = ThySyn.add_syntax
wenzelm@3622
   281
 ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
wenzelm@4873
   282
 [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
berghofe@5097
   283
  section "record" "|> RecordPackage.add_record" record_decl,
berghofe@5097
   284
  section "inductive" "" (inductive_decl false),
berghofe@5097
   285
  section "coinductive" "" (inductive_decl true),
berghofe@5097
   286
  section "datatype" "" datatype_decl,
paulson@2922
   287
  ("primrec", primrec_decl),
paulson@2922
   288
  ("recdef", rec_decl)];
clasohm@923
   289
clasohm@923
   290
end;