Re: [isabelle] automatic case splitting during simp



As Gerwin said, I wrote an Isar attribute to convert a "f x = case x of ..." definition into the standard simp rules for f.

There were some issues with variables of function type, which I've just got around to addressing now. Here's a somewhat robust version.

The attached theory file should define an Isar attribute split_simps which is used like so:

definition "f x a b = (case x of True => a | False => b)"

lemmas f_simps[simp] = f_def[split_rule bool.split]

The f_simps rule will be "f True a b = a && f False a b = b".

(We make this theory file available under a BSD license, feel free to use it. The maintainers might consider adding it to the repository.)

Yours,
   Thomas.

Gerwin Klein wrote:
On 08/12/2009, at 10:13 AM, Lucas Dixon wrote:
It would be nice to have some tools that let one derive case statements
from function definitions and visa-versa. Having the function definition
style of equations provides nice simp rules which don't expand the case
statements.

Thomas actually has made up a nice Isar attribute for that: it gives you (from a case statement) the standard simp rules you'd write in a function definition.

I'll see if we can dig this up and release it.

The other way would be to have the function package automatically prove the split rule instead.

Cheers,
Gerwin

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.