src/HOL/thy_syntax.ML
author nipkow
Fri Nov 07 08:25:02 1997 +0100 (1997-11-07)
changeset 4184 23a09f2fd687
parent 4106 01fa6e7e7196
child 4204 7b15e7eee982
permissions -rw-r--r--
Each datatype t now proves a theorem split_t_case_prem

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))
) )
     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^"_eqns) =\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 (#1(split_"^tname^"_eqns))\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 split_"^tname^"_case_prem = prove_goal thy (#2(split_"^tname^"_eqns))\n\
   169     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
   170       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
   171     \            ALLGOALS Asm_simp_tac]);\n\
   172     \val thy = thy\n";
   173 
   174 (*
   175 The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
   176 is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
   177 specific exhaustion tactic from the theory associated with the proof
   178 state. However, the exhaustion tactic for the current datatype has only just
   179 been added to !datatypes (a few lines above) but is not yet associated with
   180 the theory. Hope this can be simplified in the future.
   181 *)
   182 
   183   (*parsers*)
   184   val tvars = type_args >> map (cat "dtVar");
   185 
   186   val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
   187     type_var >> cat "dtVar";
   188 
   189   fun complex_typ toks =
   190     let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
   191         val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
   192     in
   193      (typ -- repeat (ident>>quote) >>
   194         (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
   195       "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
   196        (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
   197                          mk_pair (brackets x, y)) (commas fst, ids))) toks
   198     end;
   199 
   200   val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
   201   val constructor = name -- opt_typs -- opt_mixfix;
   202 in
   203   val datatype_decl =
   204     tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
   205 end;
   206 
   207 
   208 
   209 (** primrec **)
   210 
   211 (*recursion equations have user-supplied names*)
   212 fun mk_primrec_decl_1 ((fname, tname), axms) =
   213   let
   214     (*Isolate type name from the structure's identifier it may be stored in*)
   215     val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
   216 
   217     fun mk_prove (name, eqn) =
   218       "val " ^ name ^ " = store_thm (" ^ quote name
   219       ^ ", prove_goalw thy [get_def thy "
   220       ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
   221       \  (fn _ => [Simp_tac 1]));";
   222 
   223     val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
   224   in ("|> " ^ tname ^ "_add_primrec " ^ axs
   225       , 
   226       cat_lines (map mk_prove axms)
   227       ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
   228   end;
   229 
   230 (*recursion equations have no names*)
   231 fun mk_primrec_decl_2 ((fname, tname), axms) =
   232   let
   233     (*Isolate type name from the structure's identifier it may be stored in*)
   234     val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
   235 
   236     fun mk_prove eqn =
   237       "prove_goalw thy [get_def thy "
   238       ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
   239       \(fn _ => [Simp_tac 1])";
   240 
   241     val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
   242   in ("|> " ^ tname ^ "_add_primrec " ^ axs
   243       ,
   244       "val dummy = Addsimps " ^
   245       brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
   246   end;
   247 
   248 (*function name, argument type and either (name,axiom) pairs or just axioms*)
   249 val primrec_decl =
   250   (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
   251   (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
   252 
   253 
   254 
   255 
   256 (** rec: interface to Slind's TFL **)
   257 
   258 
   259 (*fname: name of function being defined; rel: well-founded relation*)
   260 fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
   261   let val fid = trim fname
   262       val intrnl_name = fid ^ "_Intrnl"
   263   in
   264 	 (";\n\n\
   265           \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   266           \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
   267 	                 quote fid ^ " " ^ 
   268 	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
   269           \val thy = thy"
   270          ,
   271           "structure " ^ fid ^ " =\n\
   272           \  struct\n\
   273           \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
   274           \  val {rules, induct, tcs} = \n\
   275           \    \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
   276           \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
   277           \  end;\n\
   278           \val pats_" ^ intrnl_name ^ " = ();\n")
   279   end;
   280 
   281 val rec_decl = (name -- string -- 
   282 		optional ("congs" $$-- string >> trim) "[]" -- 
   283 		optional ("simpset" $$-- string >> trim) "simpset()" -- 
   284 		repeat1 string >> mk_rec_decl) ;
   285 
   286 
   287 
   288 (** augment thy syntax **)
   289 
   290 in
   291 
   292 val _ = ThySyn.add_syntax
   293  ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
   294  [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
   295   (section "record" "|> Record.add_record" record_decl),
   296   ("inductive", inductive_decl ""),
   297   ("coinductive", inductive_decl "Co"),
   298   (section "datatype" "" datatype_decl),
   299   ("primrec", primrec_decl),
   300   ("recdef", rec_decl)];
   301 
   302 end;