Stream: Beginner Questions

Topic: ✔ locale align/fix type variables.

cai (Mar 11 2022 at 22:37):

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?

Wenda Li (Mar 12 2022 at 10:17):

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.

Mathias Fleury (Mar 12 2022 at 11:43):

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.

cai (Mar 15 2022 at 22:49):

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)

Notification Bot (Mar 15 2022 at 22:49):

cai has marked this topic as resolved.

Notification Bot (Mar 15 2022 at 23:06):

cai has marked this topic as unresolved.

cai (Mar 15 2022 at 23:14):

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))..

cai (Mar 15 2022 at 23:15):

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 :'(

cai (Mar 15 2022 at 23:16):

Is there something like -XScopedTypeVariables for Isabelle/HOL ?

Mathias Fleury (Mar 16 2022 at 07:54):

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

Mathias Fleury (Mar 16 2022 at 07:56):

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

Mathias Fleury (Mar 16 2022 at 07:57):

Or

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

cai (Mar 16 2022 at 18:50):

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.

Notification Bot (Mar 16 2022 at 18:50):

cai has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC