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