*To*: Gerwin Klein <gerwin.klein at nicta.com.au>*Subject*: Re: [isabelle] automatic case splitting during simp*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Thu, 10 Dec 2009 15:55:44 +1100*Cc*: Lucas Dixon <ldixon at inf.ed.ac.uk>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <9BF61E1B-74C2-4A94-ACD3-1F4E2D8B3749@nicta.com.au>*References*: <4B1D4464.1050601@inf.ed.ac.uk> <4B1D4BF6.4050207@in.tum.de> <4B1D8C0B.2050504@inf.ed.ac.uk> <9BF61E1B-74C2-4A94-ACD3-1F4E2D8B3749@nicta.com.au>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

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".

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

**References**:**[isabelle] automatic case splitting during simp***From:*Lucas Dixon

**Re: [isabelle] automatic case splitting during simp***From:*Tobias Nipkow

**Re: [isabelle] automatic case splitting during simp***From:*Lucas Dixon

**Re: [isabelle] automatic case splitting during simp***From:*Gerwin Klein

- Previous by Date: Re: [isabelle] Fwd: Re: Unicode tokens
- Next by Date: [isabelle] closing heap images?
- Previous by Thread: Re: [isabelle] automatic case splitting during simp
- Next by Thread: Re: [isabelle] automatic case splitting during simp
- Cl-isabelle-users December 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list