Email Gateway (Aug 22 2022 at 18:25): Email Gateway (Aug 22 2022 at 18:25):From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Can the empty relation (i.e., R x y = False for R :: 'a => 'a => bool) be
defined as an inductive relation in Isabelle, or it must be defined as a
definition?
Thanks!
Email Gateway (Aug 22 2022 at 18:26):From: Makarius <makarius@sketis.net>
Here is the classic Knaster-Tarski definition of predicate logic for Coq
users:
inductive FALSE :: bool
inductive TRUE :: bool
where TRUE: "TRUE"
inductive AND for A B
where AND: "A ⟹ B ⟹ AND A B"
inductive OR for A B
where OR1: "A ⟹ OR A B"
| OR2: "B ⟹ OR A B"
inductive EXISTS for B :: "'a ⇒ bool"
where EXISTS: "B a ⟹ EXISTS B"
inductive EQUAL :: "'a ⇒ 'a ⇒ bool" for a
where EQUAL: "EQUAL a a"
lemmas False_elim = FALSE.induct
and True_intro = TRUE
and AND_intro = AND
and AND_elim = AND.induct
and OR_intro1 = OR1
and OR_intro2 = OR2
and OR_elim = OR.induct
and EXISTS_intro = EXISTS
and EXISTS_elim = EXISTS.induct
and EQUAL_refl = EQUAL
and EQUAL_subst = EQUAL.induct
I often use this in basic tutorials about Isabelle/HOL, just for the fun
of it.
It also shows why equality is usually characterized via refl/subst,
which was challenged by Askar on a recent thread "refl can be proved".
Makarius
Email Gateway (Aug 22 2022 at 18:26):From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Got it. Thanks!
Last updated: Apr 25 2024 at 08:20 UTC