[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
      david streader


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.