[isabelle-dev] default cases rule
c.sternagel at gmail.com
Fri Sep 5 12:27:06 CEST 2014
routinely checking IsaFoR against the development version of Isabelle
(more precisely d0dffec0da2b) I stumbled across the following
In Isabelle2014 and earlier we could do
fix p :: "('a × 'b × 'c)" and xs
assume "p ∈ set xs"
then obtain x y z where "(x, y, z) ∈ set xs"
by (cases p) auto
i.e., relying on the default cases rule the proof went through.
In the development version, however, the following subgoals remain after
"apply (cases p)"
goal (2 subgoals):
1. ⋀z2. (⋀x y z. (x, y, z) ∈ set xs ⟹ thesis) ⟹
xs = p # z2 ⟹ thesis
2. ⋀z1 z2.
(⋀x y z. (x, y, z) ∈ set xs ⟹ thesis) ⟹
xs = z1 # z2 ⟹ p ∈ set z2 ⟹ thesis
That is, the default rule changed for assumptions of the form "_ : set _".
First question: is this intentional and what is the current default rule?
Second question: is it considered "bad form" to rely on default rules?
More information about the isabelle-dev