src/HOL/thy_syntax.ML
 author nipkow Thu Oct 30 09:45:03 1997 +0100 (1997-10-30) changeset 4032 4b1c69d8b767 parent 4001 b6a3c2665c45 child 4091 771b1f6422a8 permissions -rw-r--r--
For each datatype t' there is now a theorem split_t_case' of the form

P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))&
...
(!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn)))

The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x
to (..t.. & ..t..) --> P t
(and similarly for t=x).
     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;