Re: [isabelle] Proving theorems bridging between two theories/locales
On Sun, Nov 29, 2009 at 7:58 AM, <s.wong.731 at googlemail.com> wrote:
> locale A =
> fixes foo
> assumes eq: "foo = 0"
> locale B =
> fixes bar
> assumes neq: "bar ~= 0"
> lemma A_B_inconsistent:
> assumes "A foo"
> and "B foo"
> shows "False"
> proof -
> interpret A foo
> by fact
> interpret B foo
> by fact
> show "False"
> using A.eq B.neq
> by simp
> I think the simplifier can't find rules to finish off the proof. Could you
> please shed some light on this?
What's happening here is that A.eq and B.neq do not refer to the
theorems that you want.
After the "using" command, the goal window shows the content of those theorems:
A ?foo ==> ?foo = (0::?'a)
B ?bar ==> ?bar ~= (0::?'a)
So the names "A.eq" and "B.neq" refer to the generic theorems
parameterized by the locale predicates "A" and "B".
If you say "using eq neq" or "using local.eq local.neq" instead, you
will get what you want:
foo = (0::'a)
foo ~= (0::'a)
Alternatively, you can specify a name for each interpretation; then
you can refer to the instantiated theorems unambiguously using the
qualified names. (This is especially helpful when the locales involved
have some overlapping theorem names!)
assumes "A foo"
and "B foo"
interpret localA: A foo
interpret localB: B foo
using localA.eq localB.neq
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and