[isabelle-dev] default cases rule

Christian Sternagel c.sternagel at gmail.com
Fri Sep 5 12:27:06 CEST 2014

Dear all,

routinely checking IsaFoR against the development version of Isabelle 
(more precisely d0dffec0da2b) I stumbled across the following 
proof-breaking inconvenience:

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 mailing list