Quelle Inductive.thy

Sprache: Isabelle

(*  Title:      ZF/Inductive.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Inductive definitions use least fixedpoints with standard products and sums
Coinductive definitions use greatest fixedpoints with Quine products and sums

Sums are used only for mutual recursion;
Products are used only to derive "streamlined" induction rules for relations
*)

section‹Inductive and Coinductive Definitions›

theory Inductive
imports Fixedpt QPair Nat
keywords
  "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
    "elimination" "induction" "case_eqns" "recursor_eqns" :: quasi_command
begin

lemma def_swap_iff: "a ≡ b ==> a = c ⟷ c = b"
  by blast

lemma def_trans: "f ≡ g ==> g(a) = b ==> f(a) = b"
  by simp

lemma refl_thin: "∧P. a = a ==> P ==> P" .

ML_file ‹ind_syntax.ML›
ML_file ‹Tools/ind_cases.ML›
ML_file ‹Tools/cartprod.ML›
ML_file ‹Tools/inductive_package.ML›
ML_file ‹Tools/induct_tacs.ML›
ML_file ‹Tools/primrec_package.ML›

ML ‹
Lfp =
struct
val oper = 🍋‹lfp›
val bnd_mono = 🍋‹bnd_mono›
val bnd_monoI = @{thm bnd_monoI}
val subs = @{thm def_lfp_subset}
val Tarski = @{thm def_lfp_unfold}
val induct = @{thm def_induct}
end;

Standard_Prod =
struct
val sigma = 🍋‹Sigma›
val pair = 🍋‹Pair›
val split_name = 🍋‹split›
val pair_iff = @{thm Pair_iff}
val split_eq = @{thm split}
val fsplitI = @{thm splitI}
val fsplitD = @{thm splitD}
val fsplitE = @{thm splitE}
end;

Standard_CP = CartProd_Fun (Standard_Prod);

Standard_Sum =
struct
val sum = 🍋‹sum›
val inl = 🍋‹Inl›
val inr = 🍋‹Inr›
val elim = 🍋‹case›
val case_inl = @{thm case_Inl}
val case_inr = @{thm case_Inr}
val inl_iff = @{thm Inl_iff}
val inr_iff = @{thm Inr_iff}
val distinct = @{thm Inl_Inr_iff}
val distinct' = @{thm Inr_Inl_iff}
val free_SEs = Ind_Syntax.mk_free_SEs
[distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
end;

Ind_Package =
Add_inductive_def_Fun
(structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
and Su=Standard_Sum val coind = false);

Gfp =
struct
val oper = 🍋‹gfp›
val bnd_mono = 🍋‹bnd_mono›
val bnd_monoI = @{thm bnd_monoI}
val subs = @{thm def_gfp_subset}
val Tarski = @{thm def_gfp_unfold}
val induct = @{thm def_Collect_coinduct}
end;

Quine_Prod =
struct
val sigma = 🍋‹QSigma›
val pair = 🍋‹QPair›
val split_name = 🍋‹qsplit›
val pair_iff = @{thm QPair_iff}
val split_eq = @{thm qsplit}
val fsplitI = @{thm qsplitI}
val fsplitD = @{thm qsplitD}
val fsplitE = @{thm qsplitE}
end;

Quine_CP = CartProd_Fun (Quine_Prod);

Quine_Sum =
struct
val sum = 🍋‹qsum›
val inl = 🍋‹QInl›
val inr = 🍋‹QInr›
val elim = 🍋‹qcase›
val case_inl = @{thm qcase_QInl}
val case_inr = @{thm qcase_QInr}
val inl_iff = @{thm QInl_iff}
val inr_iff = @{thm QInr_iff}
val distinct = @{thm QInl_QInr_iff}
val distinct' = @{thm QInr_QInl_iff}
val free_SEs = Ind_Syntax.mk_free_SEs
[distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
end;

CoInd_Package =
Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
and Su=Quine_Sum val coind = true);

›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-06-09) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.