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