[isabelle-dev] interpretation command: "show ?thesis" causes type error
makarius at sketis.net
Tue Oct 26 13:53:07 CEST 2010
On Tue, 5 Oct 2010, Brian Huffman wrote:
> When proving a lemma, the term abbreviation ?thesis typically has type
> "bool", and saying "show ?thesis" usually works.
> But with "interpretation", it doesn't work. Here is a toy example that
> shows what I mean:
> locale foo = fixes x :: "'a::type" assumes x: "x = x"
> term "foo" (* it has type 'a => bool, as expected. *)
> interpretation myfoo: foo True
> proof -
> term ?thesis (* "foo True" :: prop *)
> show ?thesis
> *** Type unification failed: Clash of types "prop" and "bool"
> *** Type error in application: incompatible operand type
> *** Operator: Trueprop :: bool => prop
> *** Operand: PROP ?thesis :: prop
> *** At command "show"
Interpretation poses a slightly different atomic prop internally and
refines the goal state before presenting it to the user. Since ?thesis is
always derived from the statement, not from the goal, you see that
Here is a some workaround involving slightly odd prop magic:
locale foo = fixes x :: "'a::type" assumes x: "x = x"
interpretation myfoo: foo True
let "prop ?goal" = "PROP ?thesis"
show "PROP ?goal" sorry
More information about the isabelle-dev