ML ‹
Lfp =
struct
val oper = Const‹lfp›
val bnd_mono = Const‹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 = Const‹Sigma›
val pair = Const‹Pair›
val split_name = const_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 = Const‹sum›
val inl = Const‹Inl›
val inr = Const‹Inr›
val elim = Const‹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 = Const‹gfp›
val bnd_mono = Const‹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 = Const‹QSigma›
val pair = Const‹QPair›
val split_name = const_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 = Const‹qsum›
val inl = Const‹QInl›
val inr = Const‹QInr›
val elim = Const‹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-29)
¤
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.
