Stream: Beginner Questions

Topic: Construct a term of types constructed using type_definition

Yiming Xu (Oct 01 2024 at 05:22):

Say, I have a structure constructed by the conditions of a locale

locale struct =
  fixes
    M :: ‹'m set› and
    FN :: ‹'f ⇒ 'm list ⇒ 'm› and
    REL :: ‹'p ⇒ 'm list set› (* in hol-ligh a boolean is returned instead *)
  assumes
    M_nonempty: ‹M ≠ {}› and
    FN_dom_to_dom: ‹∀ f es. (∀ e ∈ list.set es. e ∈ M) ⟶ FN f es ∈ M› and
    REL_to_dom: ‹∀ p. ∀ es ∈ REL p. ∀ e ∈ list.set es. e ∈ M›

typedef ('f,'p,'m) intrp =
  ‹{ (M :: 'm set, FN :: 'f ⇒ 'm list ⇒ 'm, REL :: 'p ⇒ 'm list set). struct M FN REL }›
  using struct.intro
  by fastforce

How can I declare a term of of type ('f,'p,'m) intrp ?

I think I only need to know how to write the syntax but I do not find an example. An example will be very nice!

Mathias Fleury (Oct 01 2024 at 05:57):

So you are looking for a function to create a ('f,'p,'m) intrp. When you know the type of something, you can search for constants: Query panel > find constants > ‹_set × (_ ⇒ _ list ⇒ _) × (_ => _ list set) ⇒ (_, _, _) intrp› and you will the function to do the conversion:

find_consts
  "_set × (_ ⇒ _ list ⇒ _) × (_ => _ list set) ⇒ (_, _, _) intrp"

found 1 constant(s):
  Scratch.intrp.Abs_intrp :: "'m set × ('f ⇒ 'm list ⇒ 'm) × ('p ⇒ 'm list set) ⇒ ('f, 'p, 'm) intrp"

The keyword morphisms allows you to change the names

Mathias Fleury (Oct 01 2024 at 06:02):

The typedef stuff is explained in the tutorial https://isabelle.in.tum.de/doc/tutorial.pdf (Documentation panel > tutorial, sources: https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Doc/Tutorial/Typedefs.html)

Mathias Fleury (Oct 01 2024 at 06:03):

And the next thing to look for is probably lift_definition and transfer for the proofs

Mathias Fleury (Oct 01 2024 at 06:03):

and this is the point where you know why very few people use typedef ;-)

Yiming Xu (Oct 01 2024 at 06:52):

I see... Many thanks especially for the technique about constant-finding!

I hope the reason why people rarely use typedef is it looks intimidating. From logic aspect I think I do like this feature.
And also you also have taught me the fact that sledgehammer does not like record type (and the truncation stuff looks ugly as well...). I have the options of: type_def, with locales. record type, plus assumptions on it, and, ordered pairs, with assumptions on it.

Are there better alternatives and is there any folklore about how to choose which one to use?

Yiming Xu (Oct 01 2024 at 06:52):

No worries if the answer is everything is plainly aesthetical! I am just a bit overwhelmed with these whole bunch of choice and would like to know about the consequences if possible.

Mathias Fleury (Oct 01 2024 at 08:09):

From my experience:

• records: mostly for things that will be extended later (there is a whole algebra theory based on that). I have never used that.
• typedef: mostly for objects that you want to handle as a whole and never want to reason on the details (like integers or machine words).
  + For example if you have a list without duplicate, you cannot use the lifted append without knowing that the object was not there. In my experience this approach does not scale due to that complicated setup: you usually end up needed all invariants on your state every time for everything.
  + Also there are things that you cannot express. Think of finite set vs mset: with sets you cannot express that you functions do not add duplicates because it does not. Can be an issue for refinement.
  + requires to understand transfer eventually, especially when it goes wrong.
• invariants: usual approach. Often more modular (you can have several invariants that work independently of each other) and easier to extend.

(remark that I did a CDCL formalization with 4 components in a state and 7 groups of invariants so your mileage may vary on how important modular is for you)

Yiming Xu (Oct 01 2024 at 15:02):

Thank you for such a detailed explanation! I think maybe I tend to just use tuples then... (don't know if I will change my mind later, but I hope it is not too tedious.)

Last updated: Dec 21 2024 at 16:20 UTC