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
```