src/ZF/Inductive.thy
changeset 68490 eb53f944c8cd
parent 63435 7743df69a6b4
child 69593 3dda49e08b9d
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Inductive.thy	Sun Jun 24 15:57:48 2018 +0200
@@ -0,0 +1,132 @@
+(*  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\<open>Inductive and Coinductive Definitions\<close>
+
+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 \<longleftrightarrow> 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 \<open>
+structure 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;
+
+structure 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;
+
+structure Standard_CP = CartProd_Fun (Standard_Prod);
+
+structure 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;
+
+
+structure Ind_Package =
+    Add_inductive_def_Fun
+      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+       and Su=Standard_Sum val coind = false);
+
+
+structure 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;
+
+structure 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;
+
+structure Quine_CP = CartProd_Fun (Quine_Prod);
+
+structure 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;
+
+
+structure CoInd_Package =
+  Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
+    and Su=Quine_Sum val coind = true);
+
+\<close>
+
+end