Re: [isabelle] interpretations and *** exception Option raised



Hi David,

I have now found time to look into this. Sorry for the delay. It turns out that this is not a bug in the locale implementation as I had suspected earlier.

Hi I am lost as to what is wrong! The last lemma (see below or attached for simplified theory) results in error:
*** exception Option raised
*** At command "lemma".

but if the lemma is moved to line --"Lemma works here" then the error disapears.

Have I made some silly mistake?

The problem lies in the interpretation command issued, which doesn't make sense and should have been rejected.

theory Except imports Main
begin

locale  genr =
fixes   Ent :: "'a set"
fixes Xi :: "'x set" fixes User :: "'a => 'x => (('atom) list) set"
context genr begin
definition   Refeq :: "'a  ^  'a ^ bool"
   where   "(Refeq a c) = (a = c)"
end

locale  Pref =
fixes   PEntities :: "int set"
fixes PXi :: "int set" fixes PUser :: "int => int => ((int) list)set"
defines user: "PUser E  X  ==  {[E,X]}"

--"Lemma works here"

interpretation Pref < genr proof qed

The locale expression on the right hand side implicitly refers to parameters Ent, Xi and User, which are not declared in the locale on the left hand side. Hence this interpretation is illegal and should have been rejected. (It screws up the locale Pref and trying to enter this subsequently fails.)

I guess what you meant is the following interpretation, which works as expected:

interpretation Pref < gen PEntities PXi PUser
  proof qed

Clemens





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