[isabelle] size_change raises DUP



Dear all,

I ran into a case where size_change raises the exception DUP. As this is a low-level exception that normally should not propagate to the user, I consider this as a bug report. Here's the reduced example:

datatype foo = A | B foo | C foo foo | D foo foo

function F :: "foo => unit set set"
where
  "F A = {{()}}"
| "F (C _ _) = {}"
| "F (D _ _) = {}"
| "F (B A) = {{()}}"
| "F (B (B f)) = F f"
| "F (B (D f f')) = F (C (B f) (B f'))"
| "F (B (C f f')) = F (B f') Un F (B f')"
by pat_completeness simp_all
termination apply size_change (* raises DUP *)
by(relation
  "measure (foo_rec 0 (%_. op + 1) (%_ _ n m. n + m + 1) (%_ _ n m. 2 * n + 2 * m + 3))")
  simp_all

*** exception DUP (Const ("Set.Collect", "((Scratch.foo, Scratch.foo) Product_Type.prod => HOL.bool) => (Scratch.foo, Scratch.foo) Product_Type.prod Set.set") $ Abs ("uu_", "(Scratch.foo, Scratch.foo) Product_Type.prod", Const ("HOL.Ex", "(Scratch.foo => HOL.bool) => HOL.bool") $ Abs ("f", "Scratch.foo", Const ("HOL.Ex", "(Scratch.foo => HOL.bool) => HOL.bool") $ Abs ("f'", "Scratch.foo", Const ("HOL.conj", "HOL.bool => HOL.bool => HOL.bool") $ (Const ("HOL.eq", "(Scratch.foo, Scratch.foo) Product_Type.prod => (Scratch.foo, Scratch.foo) Product_Type.prod => HOL.bool") $ Bound 2 $ (Const ("Product_Type.Pair", "Scratch.foo => Scratch.foo => (Scratch.foo, Scratch.foo) Product_Type.prod") $ (Const ("Scratch.foo.B", "Scratch.foo => Scratch.foo") $ Bound 0) $ (Const ("Scratch.foo.B", "Scratch.foo => Scratch.foo") $ (Const ("Scratch.foo.C", "Scratch.foo => Scratch.foo => Scratch.foo") $ Bound 1 $ Bound 0)))) $ Const ("HOL.True", "HOL.bool"))))) raised (line 261 of "General/table.ML")
*** At command "apply"

Exception trace for exception - DUP raised in General/table.ML line 261

Termination.mk_dgraph(2)
Termination.decompose_tac(1)(2)
Termination.CALLS(3)
Tactical.THEN_ALL_NEW(4)
Seq.maps(2)(1)
Seq.append(2)copy(1)(1)
Seq.append(2)copy(1)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.append(2)copy(1)(1)
Seq.first_result(2)result(3)
Seq.first_result(2)
Toplevel.proofs'(1)(1)(1)
End of trace

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.