[isabelle] Can the empty relation be inductive?

[Ching-Tsun Chou]

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!
- Ching Tsun

[Makarius]

Post by Ching-Tsun Chou
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?

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

[Ching-Tsun Chou]

Got it. Thanks!

- Ching Tsun

Post by Makarius

Post by Ching-Tsun Chou
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?

Here is the classic Knaster-Tarski definition of predicate logic for Coq
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