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