src/ZF/Inductive_ZF.thy
author wenzelm
Thu Mar 15 19:02:34 2012 +0100 (2012-03-15 ago)
changeset 46947 b8c7eb0c2f89
parent 46821 ff6b0c1087f2
child 46950 d0181abdbdac
permissions -rw-r--r--
declare minor keywords via theory header;
     1 (*  Title:      ZF/Inductive_ZF.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Inductive definitions use least fixedpoints with standard products and sums
     6 Coinductive definitions use greatest fixedpoints with Quine products and sums
     7 
     8 Sums are used only for mutual recursion;
     9 Products are used only to derive "streamlined" induction rules for relations
    10 *)
    11 
    12 header{*Inductive and Coinductive Definitions*}
    13 
    14 theory Inductive_ZF
    15 imports Fixedpt QPair Nat_ZF
    16 keywords
    17   "elimination" "induction" "case_eqns" "recursor_eqns"
    18   "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
    19 uses
    20   ("ind_syntax.ML")
    21   ("Tools/cartprod.ML")
    22   ("Tools/ind_cases.ML")
    23   ("Tools/inductive_package.ML")
    24   ("Tools/induct_tacs.ML")
    25   ("Tools/primrec_package.ML")
    26 begin
    27 
    28 lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
    29   by blast
    30 
    31 lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
    32   by simp
    33 
    34 lemma refl_thin: "!!P. a = a ==> P ==> P" .
    35 
    36 use "ind_syntax.ML"
    37 use "Tools/ind_cases.ML"
    38 use "Tools/cartprod.ML"
    39 use "Tools/inductive_package.ML"
    40 use "Tools/induct_tacs.ML"
    41 use "Tools/primrec_package.ML"
    42 
    43 setup IndCases.setup
    44 setup DatatypeTactics.setup
    45 
    46 ML {*
    47 structure Lfp =
    48   struct
    49   val oper      = @{const lfp}
    50   val bnd_mono  = @{const bnd_mono}
    51   val bnd_monoI = @{thm bnd_monoI}
    52   val subs      = @{thm def_lfp_subset}
    53   val Tarski    = @{thm def_lfp_unfold}
    54   val induct    = @{thm def_induct}
    55   end;
    56 
    57 structure Standard_Prod =
    58   struct
    59   val sigma     = @{const Sigma}
    60   val pair      = @{const Pair}
    61   val split_name = @{const_name split}
    62   val pair_iff  = @{thm Pair_iff}
    63   val split_eq  = @{thm split}
    64   val fsplitI   = @{thm splitI}
    65   val fsplitD   = @{thm splitD}
    66   val fsplitE   = @{thm splitE}
    67   end;
    68 
    69 structure Standard_CP = CartProd_Fun (Standard_Prod);
    70 
    71 structure Standard_Sum =
    72   struct
    73   val sum       = @{const sum}
    74   val inl       = @{const Inl}
    75   val inr       = @{const Inr}
    76   val elim      = @{const case}
    77   val case_inl  = @{thm case_Inl}
    78   val case_inr  = @{thm case_Inr}
    79   val inl_iff   = @{thm Inl_iff}
    80   val inr_iff   = @{thm Inr_iff}
    81   val distinct  = @{thm Inl_Inr_iff}
    82   val distinct' = @{thm Inr_Inl_iff}
    83   val free_SEs  = Ind_Syntax.mk_free_SEs
    84             [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
    85   end;
    86 
    87 
    88 structure Ind_Package =
    89     Add_inductive_def_Fun
    90       (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    91        and Su=Standard_Sum val coind = false);
    92 
    93 
    94 structure Gfp =
    95   struct
    96   val oper      = @{const gfp}
    97   val bnd_mono  = @{const bnd_mono}
    98   val bnd_monoI = @{thm bnd_monoI}
    99   val subs      = @{thm def_gfp_subset}
   100   val Tarski    = @{thm def_gfp_unfold}
   101   val induct    = @{thm def_Collect_coinduct}
   102   end;
   103 
   104 structure Quine_Prod =
   105   struct
   106   val sigma     = @{const QSigma}
   107   val pair      = @{const QPair}
   108   val split_name = @{const_name qsplit}
   109   val pair_iff  = @{thm QPair_iff}
   110   val split_eq  = @{thm qsplit}
   111   val fsplitI   = @{thm qsplitI}
   112   val fsplitD   = @{thm qsplitD}
   113   val fsplitE   = @{thm qsplitE}
   114   end;
   115 
   116 structure Quine_CP = CartProd_Fun (Quine_Prod);
   117 
   118 structure Quine_Sum =
   119   struct
   120   val sum       = @{const qsum}
   121   val inl       = @{const QInl}
   122   val inr       = @{const QInr}
   123   val elim      = @{const qcase}
   124   val case_inl  = @{thm qcase_QInl}
   125   val case_inr  = @{thm qcase_QInr}
   126   val inl_iff   = @{thm QInl_iff}
   127   val inr_iff   = @{thm QInr_iff}
   128   val distinct  = @{thm QInl_QInr_iff}
   129   val distinct' = @{thm QInr_QInl_iff}
   130   val free_SEs  = Ind_Syntax.mk_free_SEs
   131             [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
   132   end;
   133 
   134 
   135 structure CoInd_Package =
   136   Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
   137     and Su=Quine_Sum val coind = true);
   138 
   139 *}
   140 
   141 end