Defining inductive predicate: fun vs primrec vs inductive? · Beginner Questions

Stream: Beginner Questions

Topic: Defining inductive predicate: fun vs primrec vs inductive?

Yiming Xu (Sep 11 2024 at 08:13):

I would like to translate the following type declaration into Isabelle/HOL.

Yiming Xu (Sep 11 2024 at 08:13):

Yiming Xu (Sep 11 2024 at 08:15):

The definitions above serves for evaluating a modal formula in the basic modal language. I defined formula, frame and model in Isabelle as follows. (Is everything good up to now?)

Yiming Xu (Sep 11 2024 at 08:15):

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"

Yiming Xu (Sep 11 2024 at 08:16):

But then I think I get confused on the translation of the "satis" predicate. It seems to be a bunch of options. There are primrec, fun and inductive. Is there any consideration that I should take before picking one?

Yiming Xu (Sep 11 2024 at 08:18):

I am attempting to do "fun". I wrote:
fun satis :: "'a model ⇒ 'a ⇒ form ⇒ bool"
where
"satis M w (VAR p) = M.valt p v ∧ M.frame.world w
| satis M w FALSE = false"

And it already started complaining:
image.png

Yiming Xu (Sep 11 2024 at 08:18):

May I please ask if there is any quick fix? Thanks in advance!

Yong Kiam (Sep 11 2024 at 08:30):

I'm not so familiar with record syntax in Isabelle, but that should be valt M

Yiming Xu (Sep 11 2024 at 08:59):

Yong Kiam said:

I'm not so familiar with record syntax in Isabelle, but that should be valt M

Thanks so much! The underscore before disappears.

Yiming Xu (Sep 11 2024 at 09:00):

Now I type (world (frame M)) and it does not look correct:
image.png

Yiming Xu (Sep 11 2024 at 09:01):

The "frame" is green, and may I please ask a "human language" translation of the error message?

Mathias Fleury (Sep 11 2024 at 13:41):

= is binding to strongly. Use statis M w ... <--> ... or statis M w ... = (...)

Mathias Fleury (Sep 11 2024 at 13:41):

And it is False

Mathias Fleury (Sep 11 2024 at 13:41):

instead of false

Yiming Xu (Sep 11 2024 at 16:29):

Thanks! I changed it into False and <-->.
image.png

Yiming Xu (Sep 11 2024 at 16:30):

Any clue why it thinks "frame" is green? M.frame also does not work.

Yiming Xu (Sep 11 2024 at 16:31):

Not obvious from https://isabelle.in.tum.de/doc/isar-ref.pdf how can we extract fields of a record term.

Mathias Fleury (Sep 11 2024 at 17:42):

frame is a type, you cannot use it as a function in a term

Mathias Fleury (Sep 11 2024 at 17:42):

I do not even know what you are trying to achieve

Yiming Xu (Sep 11 2024 at 17:47):

I would like the effect to be "a model consists of a frame and a valuation". So I should be able to type M.frame to extract the field "frame" from "M" and then type (M.frame).world to extract the field "world" from the frame "M.frame". But your comment does give a hint! I have just figured out the type "model" will not take "frame" as its field. So what I need is just "world M". Thank you!