Re: [isabelle] locale expressions?
On Tue, Aug 23, 2011 at 12:41 PM, Randy Pollack <rpollack at inf.ed.ac.uk> wrote:
> Consider the following (HOL/Main, Isabelle 2011)
> locale preordX2 = le: preorder le lt + le': preorder le' lt'
> for le::"'a => 'a => bool" and lt::"'a => 'a => bool"
> and le'::"'b => 'b => bool" and lt'::"'b => 'b => bool"
> fixes preordX2_opn:: "'a => 'b => 'a"
Within this locale, you have these two lemmas in scope:
le.less_irrefl: "~ lt x x"
le'.less_irrefl: "~ lt' x x"
> Now consider the trivial lemma:
> fixes a::'a
> shows "~ (lt a a)"
> using less_irrefl . --"less_irrefl from typeclass preorder"
The unqualified lemma name "less_irrefl" is ambiguous here. Isabelle
resolves the ambiguity by picking the most-recently-introduced name
that matches, which happens to be "le'.less_irrefl". If you explicitly
say "using le.less_irrefl" the proof will work.
This archive was generated by a fusion of
Pipermail (Mailman edition) and