src/ZF/Inductive_ZF.thy
author wenzelm
Thu Mar 15 22:08:53 2012 +0100 (2012-03-15 ago)
changeset 46950 d0181abdbdac
parent 46947 b8c7eb0c2f89
child 48891 c0eafbd55de3
permissions -rw-r--r--
declare command keywords via theory header, including strict checking outside Pure;
     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   "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
    18   "inductive_cases" :: thy_script and
    19   "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
    20   "elimination" "induction" "case_eqns" "recursor_eqns"
    21 uses
    22   ("ind_syntax.ML")
    23   ("Tools/cartprod.ML")
    24   ("Tools/ind_cases.ML")
    25   ("Tools/inductive_package.ML")
    26   ("Tools/induct_tacs.ML")
    27   ("Tools/primrec_package.ML")
    28 begin
    29 
    30 lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
    31   by blast
    32 
    33 lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
    34   by simp
    35 
    36 lemma refl_thin: "!!P. a = a ==> P ==> P" .
    37 
    38 use "ind_syntax.ML"
    39 use "Tools/ind_cases.ML"
    40 use "Tools/cartprod.ML"
    41 use "Tools/inductive_package.ML"
    42 use "Tools/induct_tacs.ML"
    43 use "Tools/primrec_package.ML"
    44 
    45 setup IndCases.setup
    46 setup DatatypeTactics.setup
    47 
    48 ML {*
    49 structure Lfp =
    50   struct
    51   val oper      = @{const lfp}
    52   val bnd_mono  = @{const bnd_mono}
    53   val bnd_monoI = @{thm bnd_monoI}
    54   val subs      = @{thm def_lfp_subset}
    55   val Tarski    = @{thm def_lfp_unfold}
    56   val induct    = @{thm def_induct}
    57   end;
    58 
    59 structure Standard_Prod =
    60   struct
    61   val sigma     = @{const Sigma}
    62   val pair      = @{const Pair}
    63   val split_name = @{const_name split}
    64   val pair_iff  = @{thm Pair_iff}
    65   val split_eq  = @{thm split}
    66   val fsplitI   = @{thm splitI}
    67   val fsplitD   = @{thm splitD}
    68   val fsplitE   = @{thm splitE}
    69   end;
    70 
    71 structure Standard_CP = CartProd_Fun (Standard_Prod);
    72 
    73 structure Standard_Sum =
    74   struct
    75   val sum       = @{const sum}
    76   val inl       = @{const Inl}
    77   val inr       = @{const Inr}
    78   val elim      = @{const case}
    79   val case_inl  = @{thm case_Inl}
    80   val case_inr  = @{thm case_Inr}
    81   val inl_iff   = @{thm Inl_iff}
    82   val inr_iff   = @{thm Inr_iff}
    83   val distinct  = @{thm Inl_Inr_iff}
    84   val distinct' = @{thm Inr_Inl_iff}
    85   val free_SEs  = Ind_Syntax.mk_free_SEs
    86             [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
    87   end;
    88 
    89 
    90 structure Ind_Package =
    91     Add_inductive_def_Fun
    92       (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
    93        and Su=Standard_Sum val coind = false);
    94 
    95 
    96 structure Gfp =
    97   struct
    98   val oper      = @{const gfp}
    99   val bnd_mono  = @{const bnd_mono}
   100   val bnd_monoI = @{thm bnd_monoI}
   101   val subs      = @{thm def_gfp_subset}
   102   val Tarski    = @{thm def_gfp_unfold}
   103   val induct    = @{thm def_Collect_coinduct}
   104   end;
   105 
   106 structure Quine_Prod =
   107   struct
   108   val sigma     = @{const QSigma}
   109   val pair      = @{const QPair}
   110   val split_name = @{const_name qsplit}
   111   val pair_iff  = @{thm QPair_iff}
   112   val split_eq  = @{thm qsplit}
   113   val fsplitI   = @{thm qsplitI}
   114   val fsplitD   = @{thm qsplitD}
   115   val fsplitE   = @{thm qsplitE}
   116   end;
   117 
   118 structure Quine_CP = CartProd_Fun (Quine_Prod);
   119 
   120 structure Quine_Sum =
   121   struct
   122   val sum       = @{const qsum}
   123   val inl       = @{const QInl}
   124   val inr       = @{const QInr}
   125   val elim      = @{const qcase}
   126   val case_inl  = @{thm qcase_QInl}
   127   val case_inr  = @{thm qcase_QInr}
   128   val inl_iff   = @{thm QInl_iff}
   129   val inr_iff   = @{thm QInr_iff}
   130   val distinct  = @{thm QInl_QInr_iff}
   131   val distinct' = @{thm QInr_QInl_iff}
   132   val free_SEs  = Ind_Syntax.mk_free_SEs
   133             [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
   134   end;
   135 
   136 
   137 structure CoInd_Package =
   138   Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
   139     and Su=Quine_Sum val coind = true);
   140 
   141 *}
   142 
   143 end