*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] interpretations and *** exception Option raised*From*: David Streader <dstr at cs.waikato.ac.nz>*Date*: Wed, 10 Sep 2008 10:12:34 +1200*User-agent*: Thunderbird 1.5.0.12 (X11/20070719)

*** exception Option raised *** At command "lemma".

Have I made some silly mistake? kind regards david streader

begin locale genr = fixes Ent :: "'a set"

definition Refeq :: "'a ^ 'a ^ bool" where "(Refeq a c) = (a = c)" end locale Pref = fixes PEntities :: "int 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

**Follow-Ups**:**Re: [isabelle] interpretations and *** exception Option raised***From:*Clemens Ballarin

**Re: [isabelle] interpretations and *** exception Option raised***From:*Clemens Ballarin

- Previous by Date: [isabelle] Special issue on Programming Languages and Mechanized Mathematics Systems (JAR)
- Next by Date: Re: [isabelle] interpretations and *** exception Option raised
- Previous by Thread: [isabelle] Special issue on Programming Languages and Mechanized Mathematics Systems (JAR)
- Next by Thread: Re: [isabelle] interpretations and *** exception Option raised
- Cl-isabelle-users September 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list