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