489 fun single_rule [rule] = rule |
489 fun single_rule [rule] = rule |
490 | single_rule _ = error "Single rule expected"; |
490 | single_rule _ = error "Single rule expected"; |
491 |
491 |
492 fun named_rule k arg get = |
492 fun named_rule k arg get = |
493 Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :-- |
493 Scan.lift (Args.$$$ k -- Args.colon) |-- Scan.repeat arg :-- |
494 (fn names => Scan.peek (fn ctxt => Scan.succeed (names |> map (fn name => |
494 (fn names => Scan.peek (fn context => Scan.succeed (names |> map (fn name => |
495 (case get ctxt name of SOME x => x |
495 (case get (Context.proof_of context) name of SOME x => x |
496 | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2; |
496 | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))) >> #2; |
497 |
497 |
498 fun rule get_type get_set = |
498 fun rule get_type get_set = |
499 named_rule InductAttrib.typeN Args.local_tyname get_type || |
499 named_rule InductAttrib.typeN Args.tyname get_type || |
500 named_rule InductAttrib.setN Args.local_const get_set || |
500 named_rule InductAttrib.setN Args.const get_set || |
501 Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thmss; |
501 Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms; |
502 |
502 |
503 val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS >> single_rule; |
503 val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS >> single_rule; |
504 val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS; |
504 val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS; |
505 val coinduct_rule = |
505 val coinduct_rule = |
506 rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule; |
506 rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS >> single_rule; |
507 |
507 |
508 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME; |
508 val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.term >> SOME; |
509 |
509 |
510 val def_inst = |
510 val def_inst = |
511 ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME) |
511 ((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME) |
512 -- Args.local_term) >> SOME || |
512 -- Args.term) >> SOME || |
513 inst >> Option.map (pair NONE); |
513 inst >> Option.map (pair NONE); |
514 |
514 |
515 val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) => |
515 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) => |
516 error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t)); |
516 error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t)); |
517 |
517 |
518 fun unless_more_args scan = Scan.unless (Scan.lift |
518 fun unless_more_args scan = Scan.unless (Scan.lift |
519 ((Args.$$$ fixingN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN || |
519 ((Args.$$$ fixingN || Args.$$$ takingN || Args.$$$ InductAttrib.typeN || |
520 Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan; |
520 Args.$$$ InductAttrib.setN || Args.$$$ ruleN) -- Args.colon)) scan; |
521 |
521 |