[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Tobias Nipkow wrote:

>> According to my understanding, the disunity of types came recursively from the
>> pattern/unify implementation itself.  My guess is that certain schematic
>> variables first started as ?x::?'a and then diverged with more concrete type
>> here, and the original general type there.
>
> it would be good to have an example of that.

To make this more concrete, here is the reduced example by Johannes in 
Bad2.thy together with a changeset to help isolating the crash.

Applying this to Isabelle/6228806b2605 reveals various additional details:


The crash happens in Thm.bicompose_no_flatten (via Goal.retrofit, which is 
the basis of SELECT_GOAL).

This explains why there is no extra incrementing of Vars, unlike the 
normal resolution-family of operations.  These low-level compose things 
are not part of regular user-space, but occasionally required to implement 
certain system infrastructure. The basic assumption is that raw 
composition is able to solve problems modulo alpha/beta/eta/polymorphism, 
without taking any of the !!/==> rule structure into account.

Here is also the concrete crash-pair:

   st:
     ?n6 (?a10 xa)
     ?n6 :: ?'b10 => 'a => nat

   st':
     ?n6 (?j12 xa + Suc (?n13 xa))
     ?n6 :: nat => 'a => nat

So the nested subproof has merely made the types more concrete. 
Goal.retrofit then hopes to be able to retrofit that result into the 
original goal state.

This technique occurs quite often in certain proof infrastructure, e.g. 
also in SUBPROOF.


Note that the input satisfies the "specification" in unify.ML that the 
types are equal (prop), but additional variance is hidden in the 
substructure.


 	Makarius
-------------- next part --------------
theory Bad2
imports "~~/src/HOL/Nat"
begin

ML {* toplevel_pp ["term"] "Proof_Display.pp_term Pure.thy" *}

consts P :: "'a set => bool"
lemma P_Int [intro]:  "P A ==> P B ==> P (A Int B)" sorry
lemma P_UNIV [intro]: "P UNIV" sorry
lemma P_INT [intro]: "ALL x : A. P (B x) ==> P (INT x : A. B x)" sorry
lemma P_UNION [intro]: "ALL x : A. P (B x) ==> P (UN x : A. B x)" sorry

lemma 
  fixes x :: "'a" and Q :: "'b => bool" and f :: "'a => 'b"
  shows "EX S. P S & x : S & (ALL xa : S. Q (f xa))"
  apply (auto simp only: )

  oops

end
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1369741469 -7200
# Node ID 4594a3aaacb73cb13e348c0416f6d93644497521
# Parent  6228806b2605b466ea77666279cbef35c13a2984
test;

diff -r 6228806b2605 -r 4594a3aaacb7 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon May 27 15:57:38 2013 +0200
+++ b/src/Pure/goal.ML	Tue May 28 13:44:29 2013 +0200
@@ -4,6 +4,8 @@
 Goals in tactical theorem proving, with support for forked proofs.
 *)
 
+exception BAD_GOAL of {st': thm, st: thm, exn: exn};
+
 signature BASIC_GOAL =
 sig
   val skip_proofs: bool Unsynchronized.ref
@@ -359,7 +361,8 @@
 fun retrofit i n st' st =
   (if n = 1 then st
    else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
-  |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
+  |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i
+  handle exn as Thm.BAD _ => raise BAD_GOAL {st' = st', st = st, exn = exn};
 
 fun SELECT_GOAL tac i st =
   if Thm.nprems_of st = 1 andalso i = 1 then tac st
diff -r 6228806b2605 -r 4594a3aaacb7 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon May 27 15:57:38 2013 +0200
+++ b/src/Pure/thm.ML	Tue May 28 13:44:29 2013 +0200
@@ -38,6 +38,10 @@
 
   (*theorems*)
   type thm
+  exception BAD of
+   {state: thm, orule: thm,
+    BBi: term * term, rtpairs: (term * term) list, stpairs: (term * term) list,
+    unify: theory * Envir.env * ((term * term) list), exn: exn}
   type conv = cterm -> thm
   val rep_thm: thm ->
    {thy_ref: theory_ref,
@@ -347,6 +351,12 @@
   body: Proofterm.proof_body}
 with
 
+exception BAD of
+ {state: thm, orule: thm,
+  BBi: term * term, rtpairs: (term * term) list, stpairs: (term * term) list,
+  unify: theory * Envir.env * ((term * term) list), exn: exn};
+
+
 type conv = cterm -> thm;
 
 (*errors involving theorems*)
@@ -1686,7 +1696,11 @@
 
      (*ordinary resolution*)
      fun res () =
-       (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
+       (case Seq.pull (Unify.unifiers (thy, env, dpairs))
+          handle exn =>
+            raise BAD {state = state, orule = orule, BBi = BBi,
+              rtpairs = rtpairs, stpairs = stpairs, unify = (thy, env, dpairs), exn = exn}
+        of
          NONE => Seq.empty
        | cell as SOME ((_, tpairs), _) =>
            Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))