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"
> begin

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:
>
> 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.

- Brian





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