Yiming Xu (Oct 12 2024 at 14:27): Yiming Xu (Oct 12 2024 at 14:27):I defined a function collecting the set of certain symbols in a formula:
function mops :: "('m, 'p) form ⇒ 'm set" where
"mops TRUE = {}"
| "mops FALSE = {}"
| "mops (VAR p) = {}"
| "mops (CONJ f1 f2) = mops f1 ∪ mops f2"
| "mops (DISJ f1 f2) = mops f1 ∪ mops f2"
| "mops (IMP f1 f2) = mops f1 ∪ mops f2"
| "mops (NOT f) = mops f"
| "mops (DIAM m fl) = {m} ∪ (⋃{ mops f | f. f ∈ list.set fl })"
| "mops (BOX m fl) = {m} ∪ (⋃{ mops f | f. f ∈ list.set fl })"
apply auto
using form.exhaust by blast
termination proof
and Isabelle asked me to prove this termination.
Yiming Xu (Oct 12 2024 at 14:27):However, it gives the following goal:
proof (state)
goal (10 subgoals):
1. wf ?R
2. ⋀f1 f2. (f1, CONJ f1 f2) ∈ ?R
3. ⋀f1 f2. (f2, CONJ f1 f2) ∈ ?R
4. ⋀f1 f2. (f1, DISJ f1 f2) ∈ ?R
5. ⋀f1 f2. (f2, DISJ f1 f2) ∈ ?R
6. ⋀f1 f2. (f1, IMP f1 f2) ∈ ?R
7. ⋀f1 f2. (f2, IMP f1 f2) ∈ ?R
8. ⋀f. (f, NOT f) ∈ ?R
9. ⋀m fl x xa. (xa, ♢m fl) ∈ ?R
10. ⋀m fl x xa. (xa, □m fl) ∈ ?R
I did not expect such a goal since in 8 and 9, it just assumes xa to be arbitrary, whereas I expect that I have an assumption that xa is a member of the list fl. I expect this because in the definition corresponding to these two subgoals, the induction clause only considers the members of the list, where the list is a part of the formula.
Yiming Xu (Oct 12 2024 at 14:30):May I please ask why it gives that goal instead and how should I get the assumption that xa in fl?
Yong Kiam (Oct 12 2024 at 14:54):you should define it in a way that is more obvious that you are taking f \in set fl
you are getting that because your set comprehension goes over all f then restricts to the comprehension
Yiming Xu (Oct 12 2024 at 15:08):Should I use list.map instead?
Yiming Xu (Oct 12 2024 at 15:08):Let me just try...
Yiming Xu (Oct 12 2024 at 15:10):Aha Isabelle got that!
Yiming Xu (Oct 12 2024 at 15:11):Now the goal is:
goal (10 subgoals):
1. wf ?R
2. ⋀f1 f2. (f1, CONJ f1 f2) ∈ ?R
3. ⋀f1 f2. (f2, CONJ f1 f2) ∈ ?R
4. ⋀f1 f2. (f1, DISJ f1 f2) ∈ ?R
5. ⋀f1 f2. (f2, DISJ f1 f2) ∈ ?R
6. ⋀f1 f2. (f1, IMP f1 f2) ∈ ?R
7. ⋀f1 f2. (f2, IMP f1 f2) ∈ ?R
8. ⋀f. (f, NOT f) ∈ ?R
9. ⋀m fl x.
x ∈ list.set fl ⟹ (x, ♢m fl) ∈ ?R
10. ⋀m fl x.
x ∈ list.set fl ⟹ (x, □m fl) ∈ ?R
Thank you very much!
Yong Kiam (Oct 12 2024 at 15:14):you could probably just use fun at that point
Yiming Xu (Oct 12 2024 at 15:14):Yes, indeed! Thanks for pointing it out! It does not even ask about proving it is a function.
Yiming Xu (Oct 12 2024 at 15:15):Just checked that folds also works!
irvin (Oct 12 2024 at 15:17):for more information
text ‹
┉
Translate between ‹{e | x1…xn. P}› and ‹{u. ∃x1…xn. u = e ∧ P}›;
‹{y. ∃x1…xn. y = e ∧ P}› is only translated if ‹[0..n] ⊆ bvs e›.
›
Should [0..n] be [x1,...,xn] instead, saying that e is a term constructed from x1 ...xn? Or did I misunderstand?
irvin (Oct 12 2024 at 15:24):Yiming Xu said:
Should
[0..n]be [x1,...,xn] instead, saying that e is a term constructed from x1 ...xn? Or did I misunderstand?
might be a typo i quoted it from Set.thy
Yiming Xu (Oct 12 2024 at 15:25):I see. Thanks for the reference!
irvin (Oct 12 2024 at 15:25):The easiest way to check is probably to write it out in its un set comprehension form and see whether its printed the same in the console
Yiming Xu (Oct 12 2024 at 15:29):I see. So both
term "{(mops f)| f. f ∈ list.set fl }"
term "{u . (∃f. u = mops f ∧ f ∈ list.set fl) }"
are printed as
"{mops f |f. f ∈ list.set fl}"
:: "'a set"
Yiming Xu said:
I see. So both
term "{(mops f)| f. f ∈ list.set fl }"
term "{u . (∃f. u = mops f ∧ f ∈ list.set fl) }"are printed as
"{mops f |f. f ∈ list.set fl}" :: "'a set"
Yup set comprehension is just syntax sugar
Yiming Xu (Oct 12 2024 at 15:33):Good to know this. Thanks for teaching!
Last updated: Dec 21 2024 at 16:20 UTC