[isabelle-dev] interpretation command: "show ?thesis" causes type error

[Makarius]

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 
internal version.

Here is a some workaround involving slightly odd prop magic:

   locale foo = fixes x :: "'a::type" assumes x: "x = x"

   interpretation myfoo: foo True
   proof -
     let "prop ?goal" = "PROP ?thesis"
     show "PROP ?goal" sorry
   qed


 	Makarius