Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2004 proofterm bug/failure

Email Gateway (Aug 17 2022 at 13:45):

From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,

When I run the following function on the theorem
"Product_Type.split_comp_eq"
I get an exception

*** Non-unifiable types:
*** ?'t27 => ?'t26

*** 'a => 'd

This does not happen to any of the thousands of other theorems I've
tried it on,
so I figure it must be some minor bug in the reconstruction algorithm
(though
I'm frequently blaming my mistakes on others)

fun proof_of_thm thm =
let
val {prop, der=(_, prf), sign, ...} = rep_thm thm
val prf' = Reconstruct.reconstruct_proof sign prop
(Proofterm.strip_thm prf)
val prf'' = Reconstruct.expand_proof sign [("", None)] prf'
in
prf''
end

Best,

Sean

Last updated: May 03 2024 at 08:18 UTC