src/Doc/Eisbach/Base.thy
author wenzelm
Sun May 17 23:03:49 2015 +0200 (2015-05-17)
changeset 60288 d7f636331176
child 60791 e3f2262786ea
permissions -rw-r--r--
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
     1 section \<open>Basic setup that is not included in the document\<close>
     2 
     3 theory Base
     4 imports Main
     5 begin
     6 
     7 ML_file "~~/src/Doc/antiquote_setup.ML"
     8 
     9 ML\<open>
    10 fun get_split_rule ctxt target =
    11   let
    12     val (head, args) = strip_comb (Envir.eta_contract target);
    13     val (const_name, _) = dest_Const head;
    14     val const_name_components = Long_Name.explode const_name;
    15 
    16     val _ =
    17       if String.isPrefix "case_" (List.last const_name_components) then ()
    18       else raise TERM ("Not a case statement", [target]);
    19 
    20     val type_name = Long_Name.implode (rev (tl (rev const_name_components)));
    21     val split = Proof_Context.get_thm ctxt (type_name ^ ".split");
    22     val vars = Term.add_vars (Thm.prop_of split) [];
    23 
    24     val datatype_name = nth (rev const_name_components) 1;
    25 
    26     fun is_datatype (Type (a, _)) = Long_Name.base_name a = Long_Name.base_name datatype_name
    27       | is_datatype _ = false;
    28 
    29     val datatype_var =
    30       (case find_first (fn (_, T') => is_datatype T') vars of
    31         SOME var => Thm.cterm_of ctxt (Term.Var var)
    32       | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name));
    33   in
    34     SOME (Drule.cterm_instantiate [(datatype_var, Thm.cterm_of ctxt (List.last args))] split)
    35   end
    36   handle TERM _ => NONE;
    37 \<close>
    38 
    39 end