Re: [isabelle] Functions in locales cause duplicate fact declaration error



"termination" looks at the last function definition in the current
context. As a solution to your problem you need to add (in TestLocale)
to termination:

function (in TestLocale) g :: "nat â nat"
  where "g i = i" by auto
termination (in TestLocale) by lexicographic_order

works.

 - Johannes

 
Am Dienstag, den 02.06.2015, 12:12 +0200 schrieb Christoph Dittmann:
> 
> theory test imports Main begin
> 
> (* unrelated function, never mentioned below *)
> fun foo :: "nat â nat" where "foo n = 0"
> 
> locale TestLocale
> 
> context TestLocale begin
> (* works fine *)
> function f :: "nat â nat"
>   where "f i = i" by auto
>   termination by lexicographic_order
> end
> 
> (* breaks *)
> function (in TestLocale) g :: "nat â nat"
>   where "g i = i" by auto
>   (* The next line produces:
> Ignoring duplicate rewrite rule:
> foo ?n1 â 0
> Duplicate fact declaration "test.foo.simps" vs. "test.foo.simps" *)
>   termination by lexicographic_order
> 
> end






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