theory SplitSimps

imports Main

begin

ML {*

structure SplitSimps = struct

val conjunct_rules = foldr1 (uncurry Conjunction.intr);

fun was_split t = let
    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
              o fst o HOLogic.dest_imp;
    val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop;
    fun dest_alls (Const ("All", _) $ Abs (_, _, t)) = dest_alls t
      | dest_alls t = t;
  in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
        handle TERM _ => false;

fun apply_split split t = Seq.of_list let
    val (t', thaw) = freeze_thaw t;
  in (map thaw (filter (was_split o prop_of) ([t'] RL [split]))) end;

fun forward_tac rules t = Seq.of_list ([t] RL rules);

val refl_imp = refl RSN (2, mp);

val get_rules_once_split =
  REPEAT (forward_tac [conjunct1, conjunct2])
    THEN REPEAT (forward_tac [spec])
    THEN (forward_tac [refl_imp]);

fun do_split split = let
    val split' = split RS iffD1;
    val split_rhs = concl_of (fst (freeze_thaw split'));
  in if was_split split_rhs
     then apply_split split' THEN get_rules_once_split
     else raise TERM ("malformed split rule", [split_rhs])
  end;

val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq];

fun better_split splitthms thm = conjunct_rules
  (Seq.list_of ((TRY atomize_meta_eq
                 THEN (REPEAT (FIRST (map do_split splitthms)))) thm));

val split_att
  = Attrib.thms >> (Thm.rule_attribute o K o better_split);

end;

*}

(* Isabelle 2008 version
ML {* 
val split_att_setup =
  Attrib.add_attributes
    [("split_simps", Attrib.syntax SplitSimps.split_att,
      "split rule involving case construct into multiple simp rules")]
*} *)

(* Isabelle 2009 version *)
ML {*
val split_att_setup =
  Attrib.setup @{binding split_simps} SplitSimps.split_att
    "split rule involving case construct into multiple simp rules";
 *}

setup split_att_setup

definition
  split_rule_test :: "((nat => 'a) + ('b * (('b => 'a) option))) => ('a => nat) => nat"
where
 "split_rule_test x f = f (case x of Inl af \<Rightarrow> af 1
    | Inr (b, None) => inv f 0
    | Inr (b, Some g) => g b)"

lemmas split_rule_test_simps
    = split_rule_test_def[split_simps sum.split prod.split option.split]

end