theory Summon
imports Main
begin

attribute_setup summon_ind_cases = \<open>Args.prop >>
  (fn t => Thm.rule_attribute (fn context => fn _ => Inductive.mk_cases (Context.proof_of context) t))
\<close> "Proves an ad-hoc instance of an elimination rule"

attribute_setup summon_fun_cases = \<open>Args.prop >>
  (fn t => Thm.rule_attribute (fn context => fn _ => Fun_Cases.mk_fun_cases (Context.proof_of context) t))
\<close> "Proves an ad-hoc instance of an elimination rule"

subsection "Examples"

thm [[summon_ind_cases "sorted (x # xs)"]]
thm [[summon_fun_cases "splice [] xs = []"]]

end