src/HOL/thy_syntax.ML
author paulson
Thu, 05 Jun 1997 13:22:25 +0200
changeset 3403 6cc663f6d62e
parent 3345 4d888ddd6284
child 3456 fdb1768ebd3e
permissions -rw-r--r--
A slight simplification of optstring The new "simpset" keyword in the "recdef" declaration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/thy_syntax.ML
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
Additional theory file sections for HOL.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
TODO:
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
  move datatype / primrec stuff to pre_datatype.ML (?)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
(*the kind of distinctiveness axioms depends on number of constructors*)
2930
602cdeabb89b Turned Addsimps into AddIffs for datatype laws.
nipkow
parents: 2922
diff changeset
    12
val dtK = 7;  (* FIXME rename?, move? *)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
structure ThySynData: THY_SYN_DATA =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
struct
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
open ThyParse;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
    20
(** typedef **)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
    22
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
  let
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
    val name' = if_none opt_name t;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
    val name = strip_quotes name';
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
  in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
      [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
        "Abs_" ^ name ^ "_inverse"])
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
    32
val typedef_decl =
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    33
  optional ("(" $$-- name --$$ ")" >> Some) None --
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
    35
  >> mk_typedef_decl;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    36
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
(** (co)inductive **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
(*co is either "" or "Co"*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
fun inductive_decl co =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
  let
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
    fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
      if Syntax.is_identifier s then "op " ^ s else "_";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
    fun mk_params (((recs, ipairs), monos), con_defs) =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
      let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
          and srec_tms = mk_list recs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
          and sintrs   = mk_big_list (map snd ipairs)
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
    50
          val intrnl_name = big_rec_name ^ "_Intrnl"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
      in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
         (";\n\n\
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
    53
          \structure " ^ intrnl_name ^ " =\n\
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    54
          \  struct\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
          \  val _ = writeln \"" ^ co ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
                     "Inductive definition " ^ big_rec_name ^ "\"\n\
1430
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    57
          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) "
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
                           ^ srec_tms ^ "\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
          \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
                           ^ sintrs ^ "\n\
1430
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    61
          \  end;\n\n\
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    62
          \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
    63
             intrnl_name ^ ".rec_tms, " ^
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
    64
             intrnl_name ^ ".intr_tms)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
         ,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
          "structure " ^ big_rec_name ^ " =\n\
1430
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    67
          \ let\n\
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    68
          \  val _ = writeln \"Proofs for " ^ co ^ 
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    69
                     "Inductive definition " ^ big_rec_name ^ "\"\n\
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    70
          \  structure Result = " ^ co ^ "Ind_section_Fun\n\
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
    71
          \\t  (open " ^ intrnl_name ^ "\n\
1430
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    72
          \\t   val thy\t\t= thy\n\
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    73
          \\t   val monos\t\t= " ^ monos ^ "\n\
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    74
          \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1430
diff changeset
    75
          \ in\n\
1430
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    76
          \  struct\n\
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
          \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
          \  open Result\n\
1430
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    79
          \  end\n\
439e1476a7f8 Improving space efficiency of inductive/datatype definitions.
paulson
parents: 1316
diff changeset
    80
          \ end;\n\n\
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
    81
          \structure " ^ intrnl_name ^ " = struct end;\n\n"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
         )
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
      end
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
    val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
3403
6cc663f6d62e A slight simplification of optstring
paulson
parents: 3345
diff changeset
    85
    fun optstring s = optional (s $$-- string >> trim) "[]"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
  in
1788
ca62fab4ce92 Quotes now optional around inductive set
paulson
parents: 1668
diff changeset
    87
    repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    88
      >> mk_params
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    89
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    90
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    91
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    92
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    93
(** datatype **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    94
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    95
local
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    96
  (* FIXME err -> add_datatype *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    97
  fun mk_cons cs =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    98
    (case duplicates (map (fst o fst) cs) of
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    99
      [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   100
    | dups => error ("Duplicate constructors: " ^ commas_quote dups));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   101
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   102
  (*generate names of distinctiveness axioms*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   103
  fun mk_distinct_rules cs tname =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   104
    let
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   105
      val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   106
      (*combine all constructor names with all others w/o duplicates*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   107
      fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   108
      fun neg1 [] = []
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   109
        | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   110
    in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   111
      if length uqcs < dtK then neg1 uqcs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   112
      else quote (tname ^ "_ord_distinct") ::
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   113
        map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   114
    end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   115
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   116
  fun mk_rules tname cons pre = " map (get_axiom thy) " ^
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   117
    mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   118
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   119
  (*generate string for calling add_datatype and build_record*)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   120
  fun mk_params ((ts, tname), cons) =
3308
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3194
diff changeset
   121
   ("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   122
    ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
3308
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3194
diff changeset
   123
    \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   124
    ,
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   125
    "structure " ^ tname ^ " =\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   126
    \struct\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   127
    \ val inject = map (get_axiom thy) " ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   128
        mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   129
          (filter_out (null o snd o fst) cons)) ^ ";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   130
    \ val distinct = " ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   131
        (if length cons < dtK then "let val distinct' = " else "") ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   132
        "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   133
        (if length cons < dtK then
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   134
          "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   135
          \ distinct') end"
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   136
         else "") ^ ";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   137
    \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   138
    \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   139
    \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   140
    \ val simps = inject @ distinct @ cases @ recs;\n\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   141
    \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   142
    \end;\n\
1668
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   143
    \val dummy = datatypes := Dtype.build_record (thy, " ^
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   144
      mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^
8ead1fe65aad added Konrad's code for the datatype package
clasohm
parents: 1574
diff changeset
   145
      ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
2930
602cdeabb89b Turned Addsimps into AddIffs for datatype laws.
nipkow
parents: 2922
diff changeset
   146
    \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
602cdeabb89b Turned Addsimps into AddIffs for datatype laws.
nipkow
parents: 2922
diff changeset
   147
    \val dummy = AddIffs " ^ tname ^ ".inject;\n\
602cdeabb89b Turned Addsimps into AddIffs for datatype laws.
nipkow
parents: 2922
diff changeset
   148
    \val dummy = " ^
602cdeabb89b Turned Addsimps into AddIffs for datatype laws.
nipkow
parents: 2922
diff changeset
   149
      (if length cons < dtK then "AddIffs " else "Addsimps ") ^
3308
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3194
diff changeset
   150
      tname ^ ".distinct;\n\
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3194
diff changeset
   151
    \val dummy = Addsimps(map (fn (_,eqn) =>\n\
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3194
diff changeset
   152
    \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3194
diff changeset
   153
                     "] eqn (fn _ => [Simp_tac 1]))\n" ^
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3194
diff changeset
   154
    tname^"_size_eqns)\n"
da002cef7090 Added overloaded function `size' for all datatypes.
nipkow
parents: 3194
diff changeset
   155
   );
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   156
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   157
  (*parsers*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   158
  val tvars = type_args >> map (cat "dtVar");
1316
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   159
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   160
  val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   161
    type_var >> cat "dtVar";
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   162
1251
81fc4d8e3eda added nested types on right hand side of datatype definitions
clasohm
parents: 977
diff changeset
   163
  fun complex_typ toks =
1316
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   164
    let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   165
        val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   166
    in
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   167
     (typ -- repeat (ident>>quote) >>
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   168
        (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   169
      "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   170
       (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   171
                         mk_pair (brackets x, y)) (commas fst, ids))) toks
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   172
    end;
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   173
977
5d57287e5e1e changed syntax of datatype declarations (curried types for constructor
clasohm
parents: 923
diff changeset
   174
  val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   175
  val constructor = name -- opt_typs -- opt_mixfix;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   176
in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   177
  val datatype_decl =
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   178
    tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   179
end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   180
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   181
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   182
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   183
(** primrec **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   184
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   185
(*recursion equations have user-supplied names*)
1845
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   186
fun mk_primrec_decl_1 ((fname, tname), axms) =
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   187
  let
1574
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1475
diff changeset
   188
    (*Isolate type name from the structure's identifier it may be stored in*)
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1475
diff changeset
   189
    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1475
diff changeset
   190
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   191
    fun mk_prove (name, eqn) =
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   192
      "val " ^ name ^ " = store_thm (" ^ quote name
1574
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1475
diff changeset
   193
      ^ ", prove_goalw thy [get_def thy "
5a63ab90ee8a modified primrec so it can be used in MiniML/Type.thy
clasohm
parents: 1475
diff changeset
   194
      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   195
      \  (fn _ => [Simp_tac 1]));";
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   196
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   197
    val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   198
  in ("|> " ^ tname ^ "_add_primrec " ^ axs
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   199
      , 
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   200
      cat_lines (map mk_prove axms)
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   201
      ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1251
diff changeset
   202
  end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   203
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   204
(*recursion equations have no names*)
1845
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   205
fun mk_primrec_decl_2 ((fname, tname), axms) =
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   206
  let
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   207
    (*Isolate type name from the structure's identifier it may be stored in*)
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   208
    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   209
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   210
    fun mk_prove eqn =
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   211
      "prove_goalw thy [get_def thy "
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   212
      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   213
      \(fn _ => [Simp_tac 1])";
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   214
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   215
    val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   216
  in ("|> " ^ tname ^ "_add_primrec " ^ axs
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   217
      ,
1845
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   218
      "val dummy = Addsimps " ^
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   219
      brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   220
  end;
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   221
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   222
(*function name, argument type and either (name,axiom) pairs or just axioms*)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   223
val primrec_decl =
1845
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   224
  (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
afa622bc829d Simplified syntax of primrec definitions.
berghofe
parents: 1788
diff changeset
   225
  (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   226
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   227
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   228
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   229
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   230
(** rec: interface to Slind's TFL **)
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   231
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   232
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   233
(*fname: name of function being defined; rel: well-founded relation*)
3403
6cc663f6d62e A slight simplification of optstring
paulson
parents: 3345
diff changeset
   234
fun mk_rec_decl (((fname, rel), ss), axms) =
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   235
  let val fid = trim fname
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   236
      val intrnl_name = fid ^ "_Intrnl"
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   237
  in
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   238
	 (";\n\n\
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   239
          \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   240
          \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
3345
4d888ddd6284 Now recdef checks the name of the function being defined.
paulson
parents: 3308
diff changeset
   241
	                 quote fid ^ " " ^ 
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   242
	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   243
          \val thy = thy"
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   244
         ,
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   245
          "structure " ^ fid ^ " =\n\
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   246
          \  struct\n\
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   247
          \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   248
          \  val {rules, induct, tcs} = \n\
3403
6cc663f6d62e A slight simplification of optstring
paulson
parents: 3345
diff changeset
   249
          \    \t Tfl.simplify_defn (" ^ ss ^ ") (thy, (" ^ quote fid ^ 
3345
4d888ddd6284 Now recdef checks the name of the function being defined.
paulson
parents: 3308
diff changeset
   250
					  ", pats_" ^ intrnl_name ^ "))\n\
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   251
          \  end;\n\
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   252
          \val pats_" ^ intrnl_name ^ " = ();\n")
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   253
  end;
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   254
3403
6cc663f6d62e A slight simplification of optstring
paulson
parents: 3345
diff changeset
   255
val rec_decl = (name -- string -- 
6cc663f6d62e A slight simplification of optstring
paulson
parents: 3345
diff changeset
   256
		optional ("simpset" $$-- string >> trim) "!simpset" -- 
6cc663f6d62e A slight simplification of optstring
paulson
parents: 3345
diff changeset
   257
		repeat1 string >> mk_rec_decl) ;
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   258
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   259
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   260
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   261
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   262
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   263
(** sections **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   264
3403
6cc663f6d62e A slight simplification of optstring
paulson
parents: 3345
diff changeset
   265
val user_keywords = ["intrs", "monos", "con_defs", "simpset", "|"];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   266
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   267
val user_sections =
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
   268
 [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   269
  ("inductive", inductive_decl ""),
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   270
  ("coinductive", inductive_decl "Co"),
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   271
  ("datatype", datatype_decl),
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   272
  ("primrec", primrec_decl),
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   273
  ("recdef", rec_decl)];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   274
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   275
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   276
end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   277
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   278
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   279
structure ThySyn = ThySynFun(ThySynData);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   280
init_thy_reader ();
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   281