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.14  header{*Inductive and Coinductive Definitions*}
    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.65 +    Add_inductive_def_Fun
    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