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