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
notepad
begin
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
end
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?
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
