src/HOL/thy_syntax.ML
author wenzelm
Mon Nov 03 21:13:24 1997 +0100 (1997-11-03)
changeset 4106 01fa6e7e7196
parent 4091 771b1f6422a8
child 4184 23a09f2fd687
permissions -rw-r--r--
tuned;
     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   name --$$ "=" -- optional (name --$$ "+" >> (parens o cat "Some")) "None" --
    40   repeat1 ((name --$$ "::" -- typ) >> mk_pair)
    41   >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
    42 
    43 
    44 (** (co)inductive **)
    45 
    46 (*co is either "" or "Co"*)
    47 fun inductive_decl co =
    48   let
    49     fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
    50       if Syntax.is_identifier s then "op " ^ s else "_";
    51     fun mk_params (((recs, ipairs), monos), con_defs) =
    52       let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
    53           and srec_tms = mk_list recs
    54           and sintrs   = mk_big_list (map snd ipairs)
    55           val intrnl_name = big_rec_name ^ "_Intrnl"
    56       in
    57          (";\n\n\
    58           \structure " ^ intrnl_name ^ " =\n\
    59           \  struct\n\
    60           \  val _ = writeln \"" ^ co ^
    61                      "Inductive definition " ^ big_rec_name ^ "\"\n\
    62           \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) "
    63                            ^ srec_tms ^ "\n\
    64           \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
    65                            ^ sintrs ^ "\n\
    66           \  end;\n\n\
    67           \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
    68              intrnl_name ^ ".rec_tms, " ^
    69              intrnl_name ^ ".intr_tms)"
    70          ,
    71           "structure " ^ big_rec_name ^ " =\n\
    72           \ let\n\
    73           \  val _ = writeln \"Proofs for " ^ co ^ 
    74                      "Inductive definition " ^ big_rec_name ^ "\"\n\
    75           \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    76           \\t  (open " ^ intrnl_name ^ "\n\
    77           \\t   val thy\t\t= thy\n\
    78           \\t   val monos\t\t= " ^ monos ^ "\n\
    79           \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    80           \ in\n\
    81           \  struct\n\
    82           \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
    83           \  open Result\n\
    84           \  end\n\
    85           \ end;\n\n\
    86           \structure " ^ intrnl_name ^ " = struct end;\n\n"
    87          )
    88       end
    89     val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    90     fun optstring s = optional (s $$-- string >> trim) "[]"
    91   in
    92     repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
    93       >> mk_params
    94   end;
    95 
    96 
    97 
    98 (** datatype **)
    99 
   100 local
   101   (* FIXME err -> add_datatype *)
   102   fun mk_cons cs =
   103     (case duplicates (map (fst o fst) cs) of
   104       [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
   105     | dups => error ("Duplicate constructors: " ^ commas_quote dups));
   106 
   107   (*generate names of distinctiveness axioms*)
   108   fun mk_distinct_rules cs tname =
   109     let
   110       val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
   111       (*combine all constructor names with all others w/o duplicates*)
   112       fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
   113       fun neg1 [] = []
   114         | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
   115     in
   116       if length uqcs < dtK then neg1 uqcs
   117       else quote (tname ^ "_ord_distinct") ::
   118         map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
   119     end;
   120 
   121   fun mk_rules tname cons pre = " map (get_axiom thy) " ^
   122     mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
   123 
   124   (*generate string for calling add_datatype and build_record*)
   125   fun mk_params ((ts, tname), cons) =
   126     "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqn) =\n\
   127     \    Datatype.add_datatype\n"
   128     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
   129     \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\
   130     \val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
   131     \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
   132     \structure " ^ tname ^ " =\n\
   133     \struct\n\
   134     \ val inject = map (get_axiom thy) " ^
   135         mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
   136           (filter_out (null o snd o fst) cons)) ^ ";\n\
   137     \ val distinct = " ^
   138         (if length cons < dtK then "let val distinct' = " else "") ^
   139         "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
   140         (if length cons < dtK then
   141           "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
   142           \ distinct') end"
   143          else "") ^ ";\n\
   144     \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
   145     \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
   146     \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
   147     \ val simps = inject @ distinct @ cases @ recs;\n\
   148     \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
   149     \end;\n\
   150     \val thy = thy |> Dtype.add_record " ^
   151       mk_triple
   152         ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
   153           mk_list (map (fst o fst) cons),
   154           tname ^ ".induct_tac") ^ ";\n\
   155     \val dummy = context thy;\n\
   156     \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
   157     \val dummy = AddIffs " ^ tname ^ ".inject;\n\
   158     \val dummy = " ^
   159       (if length cons < dtK then "AddIffs " else "Addsimps ") ^
   160       tname ^ ".distinct;\n\
   161     \val dummy = Addsimps(map (fn (_,eqn) =>\n\
   162     \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
   163                      "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
   164     \val split_"^tname^"_case = prove_goal thy split_"^tname^"_eqn\n\
   165     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
   166       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
   167     \            ALLGOALS Asm_simp_tac]);\n\
   168     \val thy = thy\n";
   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   (section "datatype" "" datatype_decl),
   295   ("primrec", primrec_decl),
   296   ("recdef", rec_decl)];
   297 
   298 end;