products/Sources/formale Sprachen/PVS/summaries/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Induction_Schema.thy   Sprache: Lisp

(*  Title:      HOL/Examples/Induction_Schema.thy
    Author:     Alexander Krauss, TU Muenchen
*)

section \<open>Examples of automatically derived induction rules\<close>

theory Induction_Schema
imports Main
begin

subsection \<open>Some simple induction principles on nat\<close>

lemma nat_standard_induct: (* cf. Nat.thy *)
  "\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)) \
  \<Longrightarrow> 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: (* cf. Nat.thy *)
  "(!!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': (* cf. List.thy *)
  "\ P [] [];
  \<And>x xs. P (x#xs) [];
  \<And>y ys. P [] (y#ys);
   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
 \<Longrightarrow> 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

[ zur Elbe Produktseite wechseln0.0Quellennavigators  Analyse erneut starten  ]