[isabelle] Functions in locales cause duplicate fact declaration error



Hello,

is "context" and "in ..." supposed to be equivalent for function
definitions?  When I use "in ..." to define a function with a
termination proof, I get "duplicate fact declaration" errors mentioning
a completely unrelated function (see the example below).


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.