src/ZF/Inductive.thy
 changeset 22814 4cd25f1706bb parent 16417 9bc16273c2d4 child 24826 78e6a3cea367
```     1.1 --- a/src/ZF/Inductive.thy	Thu Apr 26 15:41:49 2007 +0200
1.2 +++ b/src/ZF/Inductive.thy	Thu Apr 26 15:42:04 2007 +0200
1.3 @@ -3,6 +3,11 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5      Copyright   1993  University of Cambridge
1.6
1.7 +Inductive definitions use least fixedpoints with standard products and sums
1.8 +Coinductive definitions use greatest fixedpoints with Quine products and sums
1.9 +
1.10 +Sums are used only for mutual recursion;
1.11 +Products are used only to derive "streamlined" induction rules for relations
1.12  *)
1.13
1.15 @@ -19,4 +24,102 @@
1.16  setup IndCases.setup
1.17  setup DatatypeTactics.setup
1.18
1.19 +ML_setup {*
1.20 +val iT = Ind_Syntax.iT
1.21 +and oT = FOLogic.oT;
1.22 +
1.23 +structure Lfp =
1.24 +  struct
1.25 +  val oper      = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT)
1.26 +  val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
1.27 +  val bnd_monoI = bnd_monoI
1.28 +  val subs      = def_lfp_subset
1.29 +  val Tarski    = def_lfp_unfold
1.30 +  val induct    = def_induct
1.31 +  end;
1.32 +
1.33 +structure Standard_Prod =
1.34 +  struct
1.35 +  val sigma     = Const("Sigma", [iT, iT-->iT]--->iT)
1.36 +  val pair      = Const("Pair", [iT,iT]--->iT)
1.37 +  val split_name = "split"
1.38 +  val pair_iff  = Pair_iff
1.39 +  val split_eq  = split
1.40 +  val fsplitI   = splitI
1.41 +  val fsplitD   = splitD
1.42 +  val fsplitE   = splitE
1.43 +  end;
1.44 +
1.45 +structure Standard_CP = CartProd_Fun (Standard_Prod);
1.46 +
1.47 +structure Standard_Sum =
1.48 +  struct
1.49 +  val sum       = Const("op +", [iT,iT]--->iT)
1.50 +  val inl       = Const("Inl", iT-->iT)
1.51 +  val inr       = Const("Inr", iT-->iT)
1.52 +  val elim      = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
1.53 +  val case_inl  = case_Inl
1.54 +  val case_inr  = case_Inr
1.55 +  val inl_iff   = Inl_iff
1.56 +  val inr_iff   = Inr_iff
1.57 +  val distinct  = Inl_Inr_iff
1.58 +  val distinct' = Inr_Inl_iff
1.59 +  val free_SEs  = Ind_Syntax.mk_free_SEs
1.60 +            [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
1.61 +  end;
1.62 +
1.63 +
1.64 +structure Ind_Package =
1.66 +      (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
1.67 +       and Su=Standard_Sum val coind = false);
1.68 +
1.69 +
1.70 +structure Gfp =
1.71 +  struct
1.72 +  val oper      = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT)
1.73 +  val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
1.74 +  val bnd_monoI = bnd_monoI
1.75 +  val subs      = def_gfp_subset
1.76 +  val Tarski    = def_gfp_unfold
1.77 +  val induct    = def_Collect_coinduct
1.78 +  end;
1.79 +
1.80 +structure Quine_Prod =
1.81 +  struct
1.82 +  val sigma     = Const("QPair.QSigma", [iT, iT-->iT]--->iT)
1.83 +  val pair      = Const("QPair.QPair", [iT,iT]--->iT)
1.84 +  val split_name = "QPair.qsplit"
1.85 +  val pair_iff  = QPair_iff
1.86 +  val split_eq  = qsplit
1.87 +  val fsplitI   = qsplitI
1.88 +  val fsplitD   = qsplitD
1.89 +  val fsplitE   = qsplitE
1.90 +  end;
1.91 +
1.92 +structure Quine_CP = CartProd_Fun (Quine_Prod);
1.93 +
1.94 +structure Quine_Sum =
1.95 +  struct
1.96 +  val sum       = Const("QPair.op <+>", [iT,iT]--->iT)
1.97 +  val inl       = Const("QPair.QInl", iT-->iT)
1.98 +  val inr       = Const("QPair.QInr", iT-->iT)
1.99 +  val elim      = Const("QPair.qcase", [iT-->iT, iT-->iT, iT]--->iT)
1.100 +  val case_inl  = qcase_QInl
1.101 +  val case_inr  = qcase_QInr
1.102 +  val inl_iff   = QInl_iff
1.103 +  val inr_iff   = QInr_iff
1.104 +  val distinct  = QInl_QInr_iff
1.105 +  val distinct' = QInr_QInl_iff
1.106 +  val free_SEs  = Ind_Syntax.mk_free_SEs
1.107 +            [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
1.108 +  end;
1.109 +
1.110 +
1.111 +structure CoInd_Package =
1.112 +  Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
1.113 +    and Su=Quine_Sum val coind = true);
1.114 +
1.115 +*}
1.116 +
1.117  end
```