[isabelle-dev] auto raises a TYPE exception
Johannes Hölzl
hoelzl at in.tum.de
Fri Apr 5 13:37:36 CEST 2013
Hi,
In Isabelle2013 as well as the current development revision (#0a7b4e0384d0)
the following call to "auto" raises a TYPE exception in envir.ML
---- 8< ----
theory Scratch
imports Main
begin
class test =
fixes P :: "'a set ⇒ bool"
lemma
shows P_UNIV [intro]: "P UNIV"
and P_Int [intro]: "P S ⟹ P T ⟹ P (S ∩ T)"
and P_Union [intro]: "∀S∈K. P S ⟹ P (⋃ K)"
and P_INT [intro]: "finite A ⟹ ∀x∈A. P (B x) ⟹ P (⋂x∈A. B x)"
sorry
lemma
fixes Q :: "'b ⇒ bool" and f :: "'a::test ⇒ 'b"
shows "(∃S. P S ∧ x ∈ S ∧ (∀xa∈S. Q (f xa)))"
apply (auto simp only:)
oops
------------
It looks like the problem is somewhere in the call to Classical.inst0_step_tac in nodup_depth_tac (clasimp.ML):
---- clasimp.ML ----
fun nodup_depth_tac ctxt m i st =
SELECT_GOAL
(Classical.safe_steps_tac ctxt 1 THEN_ELSE
(DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
(slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
-----------------------
Dmitriy and I tried to simplify the testcase by replicating the goal on
which inst0_step_tac is called but could not replicated the failure.
* Has anybody a idea what is causing this exception?
* Any helpful tips how to continue to debug this bug?
* How can I activate backtraces in ML to get an better understand of the
problem? I tried declare [[ML_trace = true]] but I didn't get a
backtrace.
Greetings,
Johannes
More information about the isabelle-dev
mailing list