Stream: Beginner Questions

Topic: Extending/Restricting Sub-record type (instead of fields)

Yiming Xu (Sep 12 2024 at 17:17):

Firstly, code:

Background:

datatype form = VAR "num"
  | FALSE
  | DISJ "form" "form"
  | NOT "form"
  | DIAM "form"

record 'a frame =
  world :: "'a ⇒ bool"
  rel :: "'a ⇒ 'a ⇒ bool"


record 'a model = "'a frame" +
  valt :: "num ⇒ 'a ⇒ bool"

fun satis :: "'a model ⇒ 'a ⇒ form ⇒ bool"
where
"satis M w (VAR p) ⟷ (valt M p w ∧ world M w)"
| "satis M w FALSE ⟷ False"
| "satis M w (NOT f) ⟷ world M w ∧ ¬ satis M w f"
| "satis M w (DISJ f1 f2) ⟷ satis M w f1 ∨ satis M w f2"
| "satis M w (DIAM f) ⟷ world M w ∧ (∃ v. rel M w v ∧ world M v ∧ satis M v f)"

Yiming Xu (Sep 12 2024 at 17:18):

And the problem arises when I am attempting to translate this piece of HOL4 definition:

Yiming Xu (Sep 12 2024 at 17:18):

val valid_frame_state_def = Define`
    valid_frame_state f w form = !M. M.frame = f ==> satis M w form`;

Yiming Xu (Sep 12 2024 at 17:20):

The difference is: in HOL4, a "frame" is a "field" of a term of the record type "model". Like this:

Datatype:
  frame = <| world : 'a set ;
             rel : 'a -> 'a -> bool
          |>
End

Datatype:
  model = <| frame : 'a frame;
             valt : num -> 'a -> bool
          |>
End

Yiming Xu (Sep 12 2024 at 17:20):

However, now I cannot write frame M to extract the frame of a model as a field.

Yiming Xu (Sep 12 2024 at 17:21):

So the naive guess

definition valid_frame_state_def:
"valid_frame_state Fr w phi ≡ (⋀M. frame M = Fr ⟹ satis M w phi)"

will not work.

Yiming Xu (Sep 12 2024 at 17:22):

The definition "valid_frame_state" says "a modal formula phi is satisfied in a world w in a frame Fr iff for every model based on this frame, whatever the valuation of propositional letters are, the formula phi is satisfied at w".

Yiming Xu (Sep 12 2024 at 17:23):

How can I state that? Maybe it would be possible to re-assemble each component? But sound very not neat.

Yiming Xu (Sep 12 2024 at 17:26):

I just realized that there exists the option of let a frame be a field of M, and not to use the "+". But I think the canonical Isabelle treatment in the code above would look (and possibly work?) better.

Mathias Fleury (Sep 12 2024 at 17:37):

https://isabelle.in.tum.de/library/Doc/Tutorial/Records.html

Mathias Fleury (Sep 12 2024 at 17:39):

Yiming Xu (Sep 12 2024 at 17:42):

That's a nice feature. Thank you! It is quickly fixed.

Last updated: Dec 21 2024 at 16:20 UTC