I want to define a locale `fin`

but I am struggling to force `'a`

to refer to the same type:

```
locale fin =
fixes fn :: "'a ⇒ 'a" and N :: nat
assumes card: "card (UNIV :: 'a set) = N" "0 < N"
begin
lemma f: "finite (f ` UNIV)"
apply (rule finite_imageI)
using card_ge_0_finite[OF card(2)[folded card(1)]]
(*
using this:
finite UNIV
goal (1 subgoal):
1. finite UNIV
*)
sorry
end
interpretation Fin_bool: fin Not 2
by standard simp_all
declare [[show_types]]
lemmas yikes = Fin_bool.f (* finite (range (?f::?'c ⇒ ?'b)) *)
```

Types for `yikes`

are not what I expected, it should be `finite (range (?f::bool ⇒ bool)`

. How do I model this with locales?

Not sure if I understand you correctly... How about replacing

```
lemma f: "finite (f ` UNIV)"
```

with

```
lemma f: "finite ((f::_⇒'a) ` (UNIV::'a set))"
```

which adds more type constraints.

Isn't the issue that fin specifies `fn`

as function name, while the lemma uses `f`

? Maybe this is a typo. Or this intended as such and Wenda is right.

Aye, nvm this is something lost in translation when converting to a minimal example. Thanks for the help! the problem resolved itself as the implementation progressed (and more assumptions rolledin, restricting the types to what I wanted)

cai has marked this topic as resolved.

cai has marked this topic as unresolved.

Actually not resolved, the issue is still available. For example here:

```
locale f =
fixes g :: "'a list ⇒ 'a list" and κ :: nat
assumes
"card (UNIV :: 'a set) = κ"
begin (* ... *) end
declare [[show_types]]
interpretation f "λx. take 1 x" 2
apply (standard)
using card_UNIV_bool
(* it is not possible to prove this *)
```

And how can I enabled the type annotations for `UNIV`

? It only shows `card UNIV = (2::nat)`

but I want `card (UNIV :: bool set) = (2::nat)`

or (what there is now (??) `card (UNIV :: ?'a) = (2::nat)`

)..

When I changed the function to `'a => 'a list`

or `'a => 'a`

it works but I cannot express the real `g`

in terms of those generically :'(

Is there something like `-XScopedTypeVariables`

for Isabelle/HOL ?

have you tried to to specify the type of `λx. take 1 x`

?

```
interpretation f "λx. take 1 (x::bool list)" 2
apply (standard)
apply (rule card_UNIV_bool)
done
```

Or

```
interpretation f "take 1 :: bool list ⇒ _" 2
```

I see, that does solve the issue indeed. Now I feel stupid. It does not show they type of `UNIV`

but now that is not necessary.

cai has marked this topic as resolved.

Last updated: Dec 07 2023 at 20:16 UTC