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