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