Yiming Xu (Dec 10 2024 at 09:42): Yiming Xu (Dec 10 2024 at 09:42):I am attempting to write such a definition:
inductive_set nth_worlds::
"('m,'p,'a) model ⇒'a ⇒
(nat ⇒ ('m,'p) cform set) ⇒ (('m,'p) cform ⇒ 'a list) ⇒
nat ⇒ 'a set"
for M :: "('m,'p,'a) model" and r:: 'a
and f :: "nat ⇒ ('m,'p) cform set"
and cwl :: "('m,'p) cform ⇒ 'a list"
where
zero : "w = r ⟹ w ∈ nth_worlds M r f cwl 0 "
| suc: "v ∈ nth_worlds M r f cwl n ⟹
cDIAM m fl ∈ f n ⟹
asatis M v (cDIAM m fl) ⟹
w ∈ set (cwl (cDIAM m fl))
⟹ w ∈ nth_worlds M r f cwl (n+1)"
That is, I am trying to define a family of sets indexed by natural numbers (the last argument among the inductive set inputs). And Isabelle is complaining:
Argument types
'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool), 'a,
nat ⇒ ('m, 'p) cform set, ('m, 'p) cform ⇒ 'a list, nat
of nth_worlds do not agree with types
'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool), 'a,
nat ⇒ ('m, 'p) cform set, ('m, 'p) cform ⇒ 'a list
of declared parameters
May I please ask what is wrong here? The error message from Isabelle is not always helpful.
Yiming Xu (Dec 10 2024 at 09:43):Or am I allowed to declare indexed inductive sets at all? Should it be an inductive predicate on pairs instead?
Yiming Xu (Dec 10 2024 at 09:50):This one works for me:
inductive_set nth_worlds::
"('m,'p,'a) model ⇒'a ⇒
(nat ⇒ (('m,'p) cform) set) ⇒ (('m,'p) cform ⇒ 'a list) ⇒
(nat×'a) set"
for M :: "('m,'p,'a) model" and r:: 'a
and f :: "nat ⇒ ('m,'p) cform set"
and cwl :: "('m,'p) cform ⇒ 'a list"
where
zero : "w = r ⟹ (0,w) ∈ nth_worlds M r f cwl "
| suc: "(n,v) ∈ nth_worlds M r f cwl⟹
cDIAM m fl ∈ f n ⟹
asatis M v (cDIAM m fl) ⟹
w ∈ set (cwl (cDIAM m fl))
⟹ (n+1,w) ∈ nth_worlds M r f cwl"
But I am still not clear if it is the heart of the problem, can we vary a parameter when making a inductive_set declaration?
Mathias Fleury (Dec 10 2024 at 13:38):$ git diff --no-index --word-diff /tmp/a.txt /tmp/b.txt
diff --git a/tmp/a.txt b/tmp/b.txt
index 6656e1b8..22872e0e 100644
--- a/tmp/a.txt
+++ b/tmp/b.txt
@@ -1,3 +1,3 @@
[-Argument-]{+of nth_worlds do not agree with+} types
'a set × ('m ⇒ 'a list ⇒ bool) × ('p ⇒ 'a ⇒ bool), 'a,
nat ⇒ ('m, 'p) cform set, ('m, 'p) cform ⇒ 'a [-list, nat-]{+list+}
(a: typed, b: declared)
Mathias Fleury (Dec 10 2024 at 13:41):So it is matter of last argument
Mathias Fleury (Dec 10 2024 at 13:50):MMMhhhh, I did not know that you need to declarre all arguments:
inductive_set nth_worlds ::
"'b ⇒ 'a set"
(* for M :: 'b (*does not work without*) *)
where
zero : "(w::'a) ∈ (nth_worlds (M::'b) :: 'a set)"
But apparently you do need to put all the variable in a for
Yiming Xu (Dec 10 2024 at 13:57):Mathias Fleury said:
But apparently you do need to put all the variable in a for
Ha? put all variables in which sense? I did get this work:
inductive height_le ::
"'a ⇒ 'm set ⇒ ('m ⇒ 'a list ⇒ bool) ⇒ 'a ⇒ nat ⇒ bool"
for r :: 'a and Op :: "'m set" and R :: "('m ⇒ 'a list ⇒ bool)"
where
root : "height_le r Op R r 0"
| rel: "height_le r Op R w n ⟹ m ∈ Op ⟹ R m (w # vl) ⟹ v ∈ set vl
⟹ height_le r Op R v (n+1)"
Yup, but this is inductive, not inductive_set
Yiming Xu (Dec 10 2024 at 13:59):I see. So inductive_set is not happy with defining a indexed family. But inductive would be enough to give me an indexed family effectively.
Yiming Xu (Dec 10 2024 at 14:00):Good to know. I will just go for inductive predicate then.
Mathias Fleury (Dec 10 2024 at 14:01):BTW nth_words seems to be a variation of a standard concept:
inductive suc_world ::
"('m,'p,'a) model ⇒
(nat ⇒ ('m,'p) cform set) ⇒ (('m,'p) cform ⇒ 'a list) ⇒
'a ⇒ 'a ⇒ bool" where
(* readd this, but I do not have cDIAM defined:
cDIAM m fl ∈ f n ⟹
asatis M v (cDIAM m fl) ⟹
w ∈ set (cwl (cDIAM m fl)) ⟹ *)‹suc_world M f cwl r v›
term "rtranclp^^n (suc_world M f cwl)"
Do you mean like this?
inductive suc_world ::
"('m,'p,'a) model ⇒
(nat ⇒ ('m,'p) cform set) ⇒ (('m,'p) cform ⇒ 'a list) ⇒
'a ⇒ 'a ⇒ bool" where
"cDIAM m fl ∈ f n ⟹
asatis M v (cDIAM m fl) ⟹
w ∈ set (cwl (cDIAM m fl)) ⟹ suc_world M f cwl r v"
?
Mathias Fleury (Dec 10 2024 at 14:06):Yes (I get some 'a itself because cDIAM and asatis are not defined in my theories)
Mathias Fleury (Dec 10 2024 at 14:08):The set version works the same way actually:
inductive_set suc_world ::
"('m,'p,'a) model ⇒
(nat ⇒ ('m,'p) cform set) ⇒ (('m,'p) cform ⇒ 'a list) ⇒
('a × 'a) set"
for M :: "('m,'p,'a) model"
and f :: "nat ⇒ ('m,'p) cform set"
and cwl :: "('m,'p) cform ⇒ 'a list" where
(* readd this, but I do not have cDIAM defined:
cDIAM m fl ∈ f n ⟹
asatis M v (cDIAM m fl) ⟹
w ∈ set (cwl (cDIAM m fl)) ⟹ *)‹ (r,v) ∈ suc_world M f cwl›
term "rtrancl^^n (suc_world M f cwl)"
Seems sensible because I am defining a family indexed by n which is reachable from r in n steps.
Yiming Xu (Dec 10 2024 at 14:11):Thanks and I will think about the rtrancl stuff!
Last updated: Dec 21 2024 at 16:20 UTC