wenzelm@60288: section \<open>Basic setup that is not included in the document\<close>
wenzelm@60288: 
wenzelm@60288: theory Base
wenzelm@60288: imports Main
wenzelm@60288: begin
wenzelm@60288: 
wenzelm@60288: ML_file "~~/src/Doc/antiquote_setup.ML"
wenzelm@60288: 
wenzelm@60288: ML\<open>
wenzelm@60288: fun get_split_rule ctxt target =
wenzelm@60288:   let
wenzelm@60288:     val (head, args) = strip_comb (Envir.eta_contract target);
wenzelm@60288:     val (const_name, _) = dest_Const head;
wenzelm@60288:     val const_name_components = Long_Name.explode const_name;
wenzelm@60288: 
wenzelm@60288:     val _ =
wenzelm@60288:       if String.isPrefix "case_" (List.last const_name_components) then ()
wenzelm@60288:       else raise TERM ("Not a case statement", [target]);
wenzelm@60288: 
wenzelm@60288:     val type_name = Long_Name.implode (rev (tl (rev const_name_components)));
wenzelm@60288:     val split = Proof_Context.get_thm ctxt (type_name ^ ".split");
wenzelm@60288:     val vars = Term.add_vars (Thm.prop_of split) [];
wenzelm@60288: 
wenzelm@60288:     val datatype_name = nth (rev const_name_components) 1;
wenzelm@60288: 
wenzelm@60288:     fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name
wenzelm@60288:       | is_datatype _ = false;
wenzelm@60288: 
wenzelm@60288:     val datatype_var =
wenzelm@60288:       (case find_first (fn (_, T') => is_datatype T') vars of
wenzelm@60288:         SOME var => Thm.cterm_of ctxt (Term.Var var)
wenzelm@60288:       | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name));
wenzelm@60288:   in
wenzelm@60288:     SOME (Drule.cterm_instantiate [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
wenzelm@60288:   end
wenzelm@60288:   handle TERM _ => NONE;
wenzelm@60288: \<close>
wenzelm@60288: 
wenzelm@60288: end