1(* Title: HOL/Tools/Function/fun_cases.ML 2 Author: Manuel Eberl, TU Muenchen 3 4The fun_cases command for generating specialised elimination rules for 5function package functions. 6*) 7 8signature FUN_CASES = 9sig 10 val mk_fun_cases: Proof.context -> term -> thm 11 val fun_cases: (Attrib.binding * term list) list -> local_theory -> 12 (string * thm list) list * local_theory 13 val fun_cases_cmd: (Attrib.binding * string list) list -> local_theory -> 14 (string * thm list) list * local_theory 15end; 16 17structure Fun_Cases : FUN_CASES = 18struct 19 20fun mk_fun_cases ctxt prop = 21 let 22 fun err () = 23 error (Pretty.string_of (Pretty.block 24 [Pretty.str "Proposition is not a function equation:", 25 Pretty.fbrk, Syntax.pretty_term ctxt prop])); 26 val ((f, _), _) = 27 Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop) 28 handle TERM _ => err (); 29 val info = Function.get_info ctxt f handle List.Empty => err (); 30 val {elims, pelims, is_partial, ...} = info; 31 val elims = if is_partial then pelims else the elims; 32 val cprop = Thm.cterm_of ctxt prop; 33 fun mk_elim rl = 34 Thm.implies_intr cprop 35 (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl)) 36 |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); 37 in 38 (case get_first (try mk_elim) (flat elims) of 39 SOME r => r 40 | NONE => err ()) 41 end; 42 43fun gen_fun_cases prep_att prep_prop args lthy = 44 let 45 val thmss = 46 map snd args 47 |> burrow (grouped 10 Par_List.map_independent (mk_fun_cases lthy o prep_prop lthy)); 48 val facts = 49 map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])])) 50 args thmss; 51 in lthy |> Local_Theory.notes facts end; 52 53val fun_cases = gen_fun_cases (K I) Syntax.check_prop; 54val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop; 55 56val _ = 57 Outer_Syntax.local_theory \<^command_keyword>\<open>fun_cases\<close> 58 "create simplified instances of elimination rules for function equations" 59 (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo fun_cases_cmd)); 60 61end; 62 63