1(*:maxLineLen=78:*)
2
3section \<open>Basic setup that is not included in the document\<close>
4
5theory Base
6imports Main
7begin
8
9ML_file "~~/src/Doc/antiquote_setup.ML"
10
11ML\<open>
12fun get_split_rule ctxt target =
13  let
14    val (head, args) = strip_comb (Envir.eta_contract target);
15    val (const_name, _) = dest_Const head;
16    val const_name_components = Long_Name.explode const_name;
17
18    val _ =
19      if String.isPrefix "case_" (List.last const_name_components) then ()
20      else raise TERM ("Not a case statement", [target]);
21
22    val type_name = Long_Name.implode (rev (tl (rev const_name_components)));
23    val split = Proof_Context.get_thm ctxt (type_name ^ ".split");
24    val vars = Term.add_vars (Thm.prop_of split) [];
25
26    val datatype_name = nth (rev const_name_components) 1;
27
28    fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name
29      | is_datatype _ = false;
30
31    val datatype_var =
32      (case find_first (fn (_, T') => is_datatype T') vars of
33        SOME (xi, _) => xi
34      | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name));
35  in
36    SOME (infer_instantiate ctxt [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
37  end
38  handle TERM _ => NONE;
39\<close>
40
41end
42