src/HOL/Tools/induct_method.ML
changeset 8815 187547eae4c5
parent 8695 850e84526745
child 9066 b1e874e38dab
equal deleted inserted replaced
8814:0a5edcbe0695 8815:187547eae4c5
   362 val ruleN = "rule";
   362 val ruleN = "rule";
   363 
   363 
   364 
   364 
   365 (* attributes *)
   365 (* attributes *)
   366 
   366 
   367 fun spec k = (Args.$$$ k -- Args.$$$ ":") |-- Args.!!! Args.name;
   367 fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
   368 
   368 
   369 fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   369 fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   370   let val sg = sign_of x in
   370   let val sg = sign_of x in
   371     spec typeN >> (add_type o Sign.intern_tycon sg) ||
   371     spec typeN >> (add_type o Sign.intern_tycon sg) ||
   372     spec setN  >> (add_set o Sign.intern_const sg)
   372     spec setN  >> (add_set o Sign.intern_const sg)
   393   Scan.depend (fn ctxt =>
   393   Scan.depend (fn ctxt =>
   394     let val sg = ProofContext.sign_of ctxt in
   394     let val sg = ProofContext.sign_of ctxt in
   395       spec typeN >> (err typeN (get_type ctxt) o Sign.intern_tycon sg) ||
   395       spec typeN >> (err typeN (get_type ctxt) o Sign.intern_tycon sg) ||
   396       spec setN >> (err setN (get_set ctxt) o Sign.intern_const sg)
   396       spec setN >> (err setN (get_set ctxt) o Sign.intern_const sg)
   397     end >> pair ctxt) ||
   397     end >> pair ctxt) ||
   398   Scan.lift (Args.$$$ ruleN -- Args.$$$ ":") |-- Attrib.local_thm;
   398   Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
   399 
   399 
   400 val cases_rule = rule lookup_casesT lookup_casesS;
   400 val cases_rule = rule lookup_casesT lookup_casesS;
   401 val induct_rule = rule lookup_inductT lookup_inductS;
   401 val induct_rule = rule lookup_inductT lookup_inductS;
   402 
   402 
   403 val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.$$$ ":";
   403 val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon;
   404 val term = Scan.unless (Scan.lift kind) Args.local_term;
   404 val term = Scan.unless (Scan.lift kind) Args.local_term;
   405 val term_dummy = Scan.unless (Scan.lift kind)
   405 val term_dummy = Scan.unless (Scan.lift kind)
   406   (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
   406   (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
   407 
   407 
   408 fun mode name =
   408 fun mode name =
   409   Scan.lift (Scan.optional (Args.$$$ name -- Args.$$$ ":" >> K true) false);
   409   Scan.lift (Scan.optional (Args.parens (Args.$$$ name) >> K true) false);
   410 
   410 
   411 in
   411 in
   412 
   412 
   413 val cases_args = Method.syntax (mode simplifiedN -- (Scan.option term -- Scan.option cases_rule));
   413 val cases_args = Method.syntax (mode simplifiedN -- (Scan.option term -- Scan.option cases_rule));
   414 val induct_args = Method.syntax
   414 val induct_args = Method.syntax