|
theory Star imports Main
begin
inductive
star :: "('a \ 'a \ bool) \ 'a \ 'a \ bool"
for r where
refl: "star r x x" |
step: "r x y \ star r y z \ star r x z"
hide_fact (open) refl step \<comment> \<open>names too generic\<close>
lemma star_trans:
"star r x y \ star r y z \ star r x z"
proof(induction rule: star.induct)
case refl thus ?case .
next
case step thus ?case by (metis star.step)
qed
lemmas star_induct =
star.induct[of "r:: 'a*'b \ 'a*'b \ bool", split_format(complete)]
declare star.refl[simp,intro]
lemma star_step1[simp, intro]: "r x y \ star r x y"
by(metis star.refl star.step)
code_pred star .
end
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
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 ist noch experimentell.
|
