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)) *)
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)"
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
interpretation f "take 1 :: bool list ⇒ _" 2
Last updated: Jul 15 2022 at 23:21 UTC