Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to write this rule to isabelle？

Email Gateway (Aug 22 2022 at 18:55):

From: jackx <xf930813@foxmail.com>
Hello everyone, I am reading a paper recently. I mentioned these rules（see attached rule.jpg）in this paper, so I came up with an idea. I want to formalize these rules in isabelle. I tried to write it in, but it Wrong(see attached wrong1.jpg),
Fistly, I want to ask the question is the existence of the colon (x:y:z) allowed in isabelle/hol? And how should the rules of this cross product be represented in isabelle/hol?
Secondly, how to define the relationship between Q (∀, ∃, ∑, ∏, MIN, MAX) and q (∧, ∨, +, *, min, max), I tried to define but made a mistake(see attached wrong2.jpg).
rule.png
wrong1.jpg
wrong2.jpg

Last updated: Apr 29 2024 at 20:15 UTC