Download The Eisbach User Manual - Isabelle

CHAPTER 3. METHOD DEVELOPMENT
20
the same name into an attribute. When applied to a cast distinction over a
datatype, it retrieves its corresponding split rule.
We can then integrate this intro a method that applies the split rule, fist
matching to ensure that fetching the rule was successful.
method splits =
(match conclusion in ?P f for f ⇒
hmatch [[get_split_rule f ]] in U : (_ :: bool ) = _ ⇒
hrule U [THEN iffD2]ii)
lemma L 6= [] =⇒ case L of [] ⇒ False | _ ⇒ True
by (splits, prop_solver intros: allI )