src/HOL/thy_syntax.ML
author berghofe
Tue Jun 30 20:42:47 1998 +0200 (1998-06-30)
changeset 5097 6c4a7ad6ebc7
parent 4873 b5999638979e
child 5183 89f162de39cf
permissions -rw-r--r--
Adapted to new inductive definition package.
     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 fun inductive_decl coind =
    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       in
    56         ";\n\n\
    57         \local\n\
    58         \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
    59         \  InductivePackage.add_inductive true " ^
    60         (if coind then "true " else "false ") ^ srec_tms ^ " " ^
    61          sintrs ^ " " ^ monos ^ " " ^ con_defs ^ " thy;\n\
    62         \in\n\
    63         \structure " ^ big_rec_name ^ " =\n\
    64         \struct\n\
    65         \  val defs = defs;\n\
    66         \  val mono = mono;\n\
    67         \  val unfold = unfold;\n\
    68         \  val intrs = intrs;\n\
    69         \  val elims = elims;\n\
    70         \  val elim = hd elims;\n\
    71         \  val " ^ (if coind then "co" else "") ^ "induct = induct;\n\
    72         \  val mk_cases = mk_cases;\n\
    73         \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\
    74         \end;\n\
    75         \val thy = thy;\nend;\n\
    76         \val thy = thy\n"
    77       end
    78     val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    79     fun optstring s = optional (s $$-- string >> trim) "[]"
    80   in
    81     repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
    82       >> mk_params
    83   end;
    84 
    85 
    86 (** datatype **)
    87 
    88 local
    89   (* FIXME err -> add_datatype *)
    90   fun mk_cons cs =
    91     (case duplicates (map (fst o fst) cs) of
    92       [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
    93     | dups => error ("Duplicate constructors: " ^ commas_quote dups));
    94 
    95   (*generate names of distinctiveness axioms*)
    96   fun mk_distinct_rules cs tname =
    97     let
    98       val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
    99       (*combine all constructor names with all others w/o duplicates*)
   100       fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
   101       fun neg1 [] = []
   102         | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
   103     in
   104       if length uqcs < dtK then neg1 uqcs
   105       else quote (tname ^ "_ord_distinct") ::
   106         map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
   107     end;
   108 
   109   fun mk_rules tname cons pre = " map (get_axiom thy) " ^
   110     mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
   111 
   112   (*generate string for calling add_datatype and build_record*)
   113   fun mk_params ((ts, tname), cons) =
   114     "val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqns) =\n\
   115     \    Datatype.add_datatype\n"
   116     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
   117     \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)\n\
   118     \val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
   119     \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
   120     \structure " ^ tname ^ " =\n\
   121     \struct\n\
   122     \ val inject = map (get_axiom thy) " ^
   123         mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
   124           (filter_out (null o snd o fst) cons)) ^ ";\n\
   125     \ val distinct = " ^
   126         (if length cons < dtK then "let val distinct' = " else "") ^
   127         "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
   128         (if length cons < dtK then
   129           "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
   130           \ distinct') end"
   131          else "") ^ ";\n\
   132     \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
   133     \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
   134     \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
   135     \ val simps = inject @ distinct @ cases @ recs;\n\
   136     \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
   137     \end;\n\
   138     \val thy = thy |> Dtype.add_record " ^
   139       mk_triple
   140         ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
   141           mk_list (map (fst o fst) cons),
   142           tname ^ ".induct_tac") ^ ";\n\
   143     \val dummy = context thy;\n\
   144     \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
   145     \val dummy = AddIffs " ^ tname ^ ".inject;\n\
   146     \val dummy = " ^
   147       (if length cons < dtK then "AddIffs " else "Addsimps ") ^
   148       tname ^ ".distinct;\n\
   149     \val dummy = Addsimps(map (fn (_,eqn) =>\n\
   150     \ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
   151                      "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
   152     \val split_"^tname^"_case = prove_goal thy (#1(split_"^tname^"_eqns))\n\
   153     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
   154       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
   155     \            ALLGOALS Asm_simp_tac]);\n\
   156     \val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
   157     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
   158       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
   159     \            ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex]))]);\n\
   160     \val thy = thy\n";
   161 
   162 (*
   163 The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
   164 is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
   165 specific exhaustion tactic from the theory associated with the proof
   166 state. However, the exhaustion tactic for the current datatype has only just
   167 been added to !datatypes (a few lines above) but is not yet associated with
   168 the theory. Hope this can be simplified in the future.
   169 *)
   170 
   171   (*parsers*)
   172   val tvars = type_args >> map (cat "dtVar");
   173 
   174   val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
   175     type_var >> cat "dtVar";
   176 
   177   fun complex_typ toks =
   178     let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
   179         val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
   180     in
   181      (typ -- repeat (ident>>quote) >>
   182         (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
   183       "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
   184        (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
   185                          mk_pair (brackets x, y)) (commas fst, ids))) toks
   186     end;
   187 
   188   val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
   189   val constructor = name -- opt_typs -- opt_mixfix;
   190 in
   191   val datatype_decl =
   192     tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
   193 end;
   194 
   195 
   196 
   197 (** primrec **)
   198 
   199 (*recursion equations have user-supplied names*)
   200 fun mk_primrec_decl_1 ((fname, tname), axms) =
   201   let
   202     (*Isolate type name from the structure's identifier it may be stored in*)
   203     val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
   204 
   205     fun mk_prove (name, eqn) =
   206       "val " ^ name ^ " = store_thm (" ^ quote name
   207       ^ ", prove_goalw thy [get_def thy "
   208       ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
   209       \  (fn _ => [Simp_tac 1]));";
   210 
   211     val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
   212   in ("|> " ^ tname ^ "_add_primrec " ^ axs
   213       , 
   214       cat_lines (map mk_prove axms)
   215       ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
   216   end;
   217 
   218 (*recursion equations have no names*)
   219 fun mk_primrec_decl_2 ((fname, tname), axms) =
   220   let
   221     (*Isolate type name from the structure's identifier it may be stored in*)
   222     val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
   223 
   224     fun mk_prove eqn =
   225       "prove_goalw thy [get_def thy "
   226       ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
   227       \(fn _ => [Simp_tac 1])";
   228 
   229     val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
   230   in ("|> " ^ tname ^ "_add_primrec " ^ axs
   231       ,
   232       "val dummy = Addsimps " ^
   233       brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
   234   end;
   235 
   236 (*function name, argument type and either (name,axiom) pairs or just axioms*)
   237 val primrec_decl =
   238   (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
   239   (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
   240 
   241 
   242 
   243 
   244 (** rec: interface to Slind's TFL **)
   245 
   246 
   247 (*fname: name of function being defined; rel: well-founded relation*)
   248 fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
   249   let val fid = trim fname
   250       val intrnl_name = fid ^ "_Intrnl"
   251   in
   252 	 (";\n\n\
   253           \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   254           \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
   255 	                 quote fid ^ " " ^ 
   256 	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
   257           \val thy = thy"
   258          ,
   259           "structure " ^ fid ^ " =\n\
   260           \  struct\n\
   261           \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
   262           \  val {rules, induct, tcs} = \n\
   263           \    \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
   264           \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
   265           \  end;\n\
   266           \val pats_" ^ intrnl_name ^ " = ();\n")
   267   end;
   268 
   269 val rec_decl = (name -- string -- 
   270 		optional ("congs" $$-- string >> trim) "[]" -- 
   271 		optional ("simpset" $$-- string >> trim) "simpset()" -- 
   272 		repeat1 string >> mk_rec_decl) ;
   273 
   274 
   275 
   276 (** augment thy syntax **)
   277 
   278 in
   279 
   280 val _ = ThySyn.add_syntax
   281  ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
   282  [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
   283   section "record" "|> RecordPackage.add_record" record_decl,
   284   section "inductive" "" (inductive_decl false),
   285   section "coinductive" "" (inductive_decl true),
   286   section "datatype" "" datatype_decl,
   287   ("primrec", primrec_decl),
   288   ("recdef", rec_decl)];
   289 
   290 end;