src/Doc/Eisbach/Base.thy
changeset 60288 d7f636331176
child 60791 e3f2262786ea
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/Eisbach/Base.thy	Sun May 17 23:03:49 2015 +0200
     1.3 @@ -0,0 +1,39 @@
     1.4 +section \<open>Basic setup that is not included in the document\<close>
     1.5 +
     1.6 +theory Base
     1.7 +imports Main
     1.8 +begin
     1.9 +
    1.10 +ML_file "~~/src/Doc/antiquote_setup.ML"
    1.11 +
    1.12 +ML\<open>
    1.13 +fun get_split_rule ctxt target =
    1.14 +  let
    1.15 +    val (head, args) = strip_comb (Envir.eta_contract target);
    1.16 +    val (const_name, _) = dest_Const head;
    1.17 +    val const_name_components = Long_Name.explode const_name;
    1.18 +
    1.19 +    val _ =
    1.20 +      if String.isPrefix "case_" (List.last const_name_components) then ()
    1.21 +      else raise TERM ("Not a case statement", [target]);
    1.22 +
    1.23 +    val type_name = Long_Name.implode (rev (tl (rev const_name_components)));
    1.24 +    val split = Proof_Context.get_thm ctxt (type_name ^ ".split");
    1.25 +    val vars = Term.add_vars (Thm.prop_of split) [];
    1.26 +
    1.27 +    val datatype_name = nth (rev const_name_components) 1;
    1.28 +
    1.29 +    fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name
    1.30 +      | is_datatype _ = false;
    1.31 +
    1.32 +    val datatype_var =
    1.33 +      (case find_first (fn (_, T') => is_datatype T') vars of
    1.34 +        SOME var => Thm.cterm_of ctxt (Term.Var var)
    1.35 +      | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name));
    1.36 +  in
    1.37 +    SOME (Drule.cterm_instantiate [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
    1.38 +  end
    1.39 +  handle TERM _ => NONE;
    1.40 +\<close>
    1.41 +
    1.42 +end