Re: [isabelle] Locale expression and contradiction



On Thu, Jun 3, 2010 at 3:46 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:
> On Wed, Jun 2, 2010 at 10:54 AM, John Munroe <munddr at gmail.com> wrote:

>
> Your lemma is completely trivial, and its proof does not depend on any
> assumptions of any of your locales. LocB does not fix a variable F',
> so F' is considered as an ordinary free variable in lemma "lem". You
> could just as well prove it at the top level:
>
> lemma "EX f s. f s = F' s"
> by auto
>

What I actually wanted to prove is that whether there's a function in
LocB such that it'd return the same value as that returned by a
function in LocC for the same argument. Would I need to parameterise F
and G in locB and F in locC?

Thanks again.
John

>>, i.e. there exists
>> some function f and some argument s to f in the locale LocB such that
>> all values returned are same as those returned by F in LocC for the
>> same argument?
>
> How do you reconcile "there exists ... some argument s" with "all
> values returned"? Maybe you really meant this:
>
> lemma "EX f. ALL s. f s = F' s"
> by auto
>
> Either way, the lemma is trivially true, regardless of any locales.
> Whether or not any of your locales are inconsistent has no effect
> whatsoever on the proof.
>
> - Brian
>





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