Re: [isabelle] FuncSet without extensional?

Since this is a library theory, you can expect a number of client
theories to break if you make such a drastic change. For example

lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B"

within FuncSet would no longer hold, although it is a standard law about
function spaces.

At the moment users have the choice: they can always adjoin
"extensional" in their context if needed. Your suggestion deprives them
of that choice.


Joachim Breitner schrieb:
> Hi,
> I was trying to prove the statement that there is a bijection between
> Hom(F(X),C2) and Pow(X). I started with
>   "∃ f. bij_betw f (Pow X) (hom (ℱ\<^bsub>X\<^esub>) C2)"
> and it went relatively well... until I noticed that hom is not suitable
> here. Group.hom is defined via FuncSet.Pi, which has the following
> definition:
> Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where
>   "Pi A B = {f. ∀x. x ∈ A --> f x ∈ B x}"
> (With an abbreviation A -> B).
> This means that for example ({} -> {}) is not a one-element-set, but is
> actually the set UNIV::('a -> 'b).
> Right below the definition of Pi, there is a predicate specifying that
> functions are undefined outside their definition:
> definition
>   extensional :: "'a set => ('a => 'b) set" where
>   "extensional A = {f. ∀x. x~:A --> f x = undefined}"
> For my current goal, it would be great if this were part of the
> definition of Pi. Would this be generally useful? Or are there hard
> reasons not to require "extensional A" for function in "A -> B"?
> Thanks,
> Joachim

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