Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 12:21):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi David,

this looks like a bug. Which precise version of Isabelle are you using?

Clemens

Email Gateway (Aug 18 2022 at 12:27):

From: Clemens Ballarin <ballarin@in.tum.de>
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

Last updated: Nov 21 2024 at 12:39 UTC