Quelle Mutual.thy Sprache: Isabelle

(*<*)theory Mutual imports Main begin(*>*)

subsection‹Mutually Inductive Definitions›

text‹
as there are datatypes defined by mutual recursion, there are sets defined
mutual induction. As a trivial example we consider the even and odd
numbers:
›

inductive_set
  Even :: "nat set" and
  Odd  :: "nat set"
where
  zero:  "0 ∈ Even"
| EvenI: "n ∈ Odd ==> Suc n ∈ Even"
| OddI:  "n ∈ Even ==> Suc n ∈ Odd"

text‹\noindent
mutually inductive definition of multiple sets is no different from
of a single set, except for induction: just as for mutually recursive
, induction needs to involve all the simultaneously defined sets. In
above case, the induction rule is called @{thm[source]Even_Odd.induct}
simply concatenate the names of the sets involved) and has the conclusion
{text[display]"(?x ∈ Even ⟶ ?P ?x) ∧ (?y ∈ Odd ⟶ ?Q ?y)"}

we want to prove that all even numbers are divisible by two, we have to
the statement as follows:
›

lemma "(m ∈ Even ⟶ 2 dvd m) ∧ (n ∈ Odd ⟶ 2 dvd (Suc n))"

txt‹\noindent
proof is by rule induction. Because of the form of the induction theorem,
is applied by ‹rule› rather than ‹erule› as for ordinary
definitions:
›

apply(rule Even_Odd.induct)

txt‹
{subgoals[display,indent=0]}
first two subgoals are proved by simplification and the final one can be
in the same manner as in \S\ref{sec:rule-induction}
the same subgoal was encountered before.
do not show the proof script.
›
(*<*)
  apply simp
apply simp
apply(simp add: dvd_def)
apply(clarify)
apply(rule_tac x = "Suc k" in exI)
apply simp
done
(*>*)

subsection‹Inductively Defined Predicates\label{sec:ind-predicates}›

text‹\index{inductive predicates|(}
of a set of even numbers one can also define a predicate on typ‹nat›:
›

inductive evn :: "nat → bool" where
zero: "evn 0" |
step: "evn n ==> evn(Suc(Suc n))"

text‹\noindent Everything works as before, except that
write \commdx{inductive} instead of \isacommand{inductive\_set} and
prop‹evn n› instead of prop‹n ∈ Even›.
defining an n-ary relation as a predicate, it is recommended to curry
predicate: its type should be \mbox{‹τ₁ → … → τ_n → bool›}
than
‹τ₁ × … × τ_n → bool›. The curried version facilitates inductions.

should you choose sets and when predicates? If you intend to combine your notion with set theoretic notation, define it as an inductive set. If not, define it as an inductive predicate, thus avoiding the ‹∈› notation. But note that predicates of more than one argument cannot be combined with the usual set theoretic operators: term‹P ∪ Q› is not well-typed if ‹P, Q :: τ₁ → τ₂ → bool›, you have to write term‹%x y. P x y & Q x y› instead.
index{inductive predicates|)}
›

(*<*)end(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet am 2026-09-28) ¤

Wurzel

Suchen

PVS Prover

Isabelle Prover

NIST Cobol Testsuite

Cephes Mathematical Library

Vienna Development Method

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.