header {* Examples of automatically derived induction rules *}

theory Induction_Schema

imports Main

begin

subsection {* Some simple induction principles on nat *}

lemma nat_standard_induct:

"[|P 0; !!n. P n ==> P (Suc n)|] ==> P x"

by induction_schema (pat_completeness, lexicographic_order)

lemma nat_induct2:

"[| P 0; P (Suc 0); !!k. P k ==> P (Suc k) ==> P (Suc (Suc k)) |]

==> P n"

by induction_schema (pat_completeness, lexicographic_order)

lemma minus_one_induct:

"[|!!n::nat. (n ≠ 0 ==> P (n - 1)) ==> P n|] ==> P x"

by induction_schema (pat_completeness, lexicographic_order)

theorem diff_induct:

"(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>

(!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"

by induction_schema (pat_completeness, lexicographic_order)

lemma list_induct2':

"[| P [] [];

!!x xs. P (x#xs) [];

!!y ys. P [] (y#ys);

!!x xs y ys. P xs ys ==> P (x#xs) (y#ys) |]

==> P xs ys"

by induction_schema (pat_completeness, lexicographic_order)

theorem even_odd_induct:

assumes "R 0"

assumes "Q 0"

assumes "!!n. Q n ==> R (Suc n)"

assumes "!!n. R n ==> Q (Suc n)"

shows "R n" "Q n"

using assms

by induction_schema (pat_completeness+, lexicographic_order)

end