# [isabelle] interpretations and *** exception Option raised

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?

kind regards

```
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 M genr proof qed

lemma (in genr) reflexive: "Refeq p p"
unfolding Refeq_def by simp

lemma (in Pref) refl: " a_a"

```
```header {* Atomic Labeled Transition System *}
theory Except
imports Main
begin

locale  genr =
fixes   Ent :: "'a set" ("Ent")
fixes   Xi :: "'x set"  ("\<Xi>")
fixes   User  ::  "'a  \<Rightarrow>  'x \<Rightarrow> (('atom) list) set"  ("Ob '(_\<parallel>_')"  100)

context genr begin
text {* we need to lift maps between atoms to maps between traces and sets of traces  I think these definitions exist somewhere but I can not find them!*}

text {*
As \$Obs \subseteq \Xi \subseteq Ent\$ only one mapping is needed in homomorphism *}

definition    Ref :: "'a  \<Rightarrow>  'a \<Rightarrow> bool" (infixl "\<sqsubseteq>"  100)
where  "(a \<sqsubseteq> c) \<equiv> (\<forall> x. (x \<in> \<Xi>) \<longrightarrow> Ob(a \<parallel> x) \<supseteq>  Ob(c \<parallel> x ))"
definition   Refeq :: "'a  \<Rightarrow>  'a \<Rightarrow> bool" (infixl "\<bowtie>"  100)
where   "(a \<bowtie> c) = (\<forall> x. (x \<in> \<Xi>) \<longrightarrow> Ob(a \<parallel> x) =  Ob(c \<parallel> x ))"
end

locale  Prefinement =
fixes   PEntities :: "int set" ("Ent")
fixes   PXi :: "int set"  ("\<Xi>")
fixes   PUser  ::  "int  \<Rightarrow> int  \<Rightarrow> ((int)list)set" ("Ob'(_\<parallel>_')" 100)
defines user: "Ob(E \<parallel> X)  \<equiv>  {[E,X]}"

interpretation Prefinement \<subseteq> genr proof qed

lemma (in genr) reflexive: "Refeq p p"
unfolding Refeq_def by simp

lemma (in Prefinement) reflexive: "Refeq (p::int) p"

end

```

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