Re: [isabelle] Comparing polymorphic functions

```Thanks for the explanation.

>  * Schematic term/type variables can be instantiated.  For type variables
>    this effectively means some kind of naive polymorphism.
>
>
I see. But why do you call it naive? If the variables can be instantiated,
then that's polymorphism -- is it not?

>
> Before this is getting more complicated: What is your actual application?
>
>
Basically, I'm puzzled by two things:

1) If we look at the following:

axiomatization
func1 :: "nat => nat" and
func2 :: "(nat => nat) => nat" and
func3 :: "'a => 'b => 'c"
where
*: "func2 func1 = 0"

schematic_lemma lem: "EX f (c::?'a). f c = 0"
apply (intro exI)
apply (rule_tac[!] *)
done

thm lem

EX (f::nat => nat) c::nat. f c = (0::nat)

I wasn't expecting c to be of type "nat". Since it uses *, c should be
instantiated to "func1", which is of type "nat => nat". According to the
prf:

protectI % EX f c. f c = 0 %%
(exI % (%x. EX c. x c = 0) % (%a. a) %% (OfClass type_class % TYPE(nat =>
nat)) %% (exI % (%x. x = 0) % func2 func1 %% (OfClass type_class %
TYPE(nat)) ...

f is instantiated to func2 and c is instantiated to func1. How come ?'a is
instantiated to "nat" and not "nat => nat"?

2) For the following:

declare [[unify_search_bound=5]]

ML {*
val p = term_of @{cpat "?f (?c::?'a) = ?v"};
val t = @{term "x (y::nat=>nat) (z::nat=>nat) = (0::nat)"};
val mtchers = Unify.matchers @{theory} [(p,t)] |> Seq.list_of;
pretty_insts @{context} (map (fn x => (x,0)) mtchers)
*}

It returns 3 matchers:
(1) [?c::nat := (x::(nat => nat) => (nat => nat) => nat) (y::nat => nat)
(z::nat => nat), ?f::nat => nat := %a::nat. a, ?v::nat := 0::nat]

[?'a := nat, ?'a1 := nat]

(2) [?c::?'a := ?c::?'a, ?f::?'a => nat := %a::?'a. (x::(nat => nat) => (nat
=> nat) => nat) (y::nat => nat) (z::nat => nat), ?v::nat := 0::nat]

[?'a1 := nat]

(3) [?c::?'a := z::nat => nat, ?f::?'a => ?'a1 := (x::(nat => nat) => (nat
=> nat) => nat) (y::nat => nat), ?v::?'a1 := 0::nat]

[?'a := nat => nat, ?'a1 := nat]

How come "?c" can't be instantiated to "z" but can be instantiated to
"y"? It can do that only if the type of ?c is changed from ?'a to, e.g.,
?'a=>?'b. Since the schematic type variables, e.g., ?'a can be instantiated,
e.g., to "nat" in (1) and to "nat => nat" in (3), why does the type of ?c
need to be explicitly rewritten to, e.g., ?a=>?'b, in order for ?c to be
instantiated to functions like "y" or %x.x? Is this what you mean by "naive
polymorphism"?

Note that even when ?c::?'a=>?'b, there are 2 matchers with ?c := z whereas
there's only 1 matcher with ?c := y. Do you know what's behind
this asymmetry?