src/ZF/Inductive_ZF.thy
 author wenzelm Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) changeset 58957 c9e744ea8a38 parent 58871 c399ae4b836f child 60770 240563fbf41d permissions -rw-r--r--
proper context for match_tac etc.;
1 (*  Title:      ZF/Inductive_ZF.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1993  University of Cambridge
5 Inductive definitions use least fixedpoints with standard products and sums
6 Coinductive definitions use greatest fixedpoints with Quine products and sums
8 Sums are used only for mutual recursion;
9 Products are used only to derive "streamlined" induction rules for relations
10 *)
12 section{*Inductive and Coinductive Definitions*}
14 theory Inductive_ZF
15 imports Fixedpt QPair Nat_ZF
16 keywords
17   "inductive" "coinductive" "inductive_cases" "rep_datatype" "primrec" :: thy_decl and
18   "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
19   "elimination" "induction" "case_eqns" "recursor_eqns"
20 begin
22 lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
23   by blast
25 lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
26   by simp
28 lemma refl_thin: "!!P. a = a ==> P ==> P" .
30 ML_file "ind_syntax.ML"
31 ML_file "Tools/ind_cases.ML"
32 ML_file "Tools/cartprod.ML"
33 ML_file "Tools/inductive_package.ML"
34 ML_file "Tools/induct_tacs.ML"
35 ML_file "Tools/primrec_package.ML"
37 ML {*
38 structure Lfp =
39   struct
40   val oper      = @{const lfp}
41   val bnd_mono  = @{const bnd_mono}
42   val bnd_monoI = @{thm bnd_monoI}
43   val subs      = @{thm def_lfp_subset}
44   val Tarski    = @{thm def_lfp_unfold}
45   val induct    = @{thm def_induct}
46   end;
48 structure Standard_Prod =
49   struct
50   val sigma     = @{const Sigma}
51   val pair      = @{const Pair}
52   val split_name = @{const_name split}
53   val pair_iff  = @{thm Pair_iff}
54   val split_eq  = @{thm split}
55   val fsplitI   = @{thm splitI}
56   val fsplitD   = @{thm splitD}
57   val fsplitE   = @{thm splitE}
58   end;
60 structure Standard_CP = CartProd_Fun (Standard_Prod);
62 structure Standard_Sum =
63   struct
64   val sum       = @{const sum}
65   val inl       = @{const Inl}
66   val inr       = @{const Inr}
67   val elim      = @{const case}
68   val case_inl  = @{thm case_Inl}
69   val case_inr  = @{thm case_Inr}
70   val inl_iff   = @{thm Inl_iff}
71   val inr_iff   = @{thm Inr_iff}
72   val distinct  = @{thm Inl_Inr_iff}
73   val distinct' = @{thm Inr_Inl_iff}
74   val free_SEs  = Ind_Syntax.mk_free_SEs
75             [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff]
76   end;
79 structure Ind_Package =
81       (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
82        and Su=Standard_Sum val coind = false);
85 structure Gfp =
86   struct
87   val oper      = @{const gfp}
88   val bnd_mono  = @{const bnd_mono}
89   val bnd_monoI = @{thm bnd_monoI}
90   val subs      = @{thm def_gfp_subset}
91   val Tarski    = @{thm def_gfp_unfold}
92   val induct    = @{thm def_Collect_coinduct}
93   end;
95 structure Quine_Prod =
96   struct
97   val sigma     = @{const QSigma}
98   val pair      = @{const QPair}
99   val split_name = @{const_name qsplit}
100   val pair_iff  = @{thm QPair_iff}
101   val split_eq  = @{thm qsplit}
102   val fsplitI   = @{thm qsplitI}
103   val fsplitD   = @{thm qsplitD}
104   val fsplitE   = @{thm qsplitE}
105   end;
107 structure Quine_CP = CartProd_Fun (Quine_Prod);
109 structure Quine_Sum =
110   struct
111   val sum       = @{const qsum}
112   val inl       = @{const QInl}
113   val inr       = @{const QInr}
114   val elim      = @{const qcase}
115   val case_inl  = @{thm qcase_QInl}
116   val case_inr  = @{thm qcase_QInr}
117   val inl_iff   = @{thm QInl_iff}
118   val inr_iff   = @{thm QInr_iff}
119   val distinct  = @{thm QInl_QInr_iff}
120   val distinct' = @{thm QInr_QInl_iff}
121   val free_SEs  = Ind_Syntax.mk_free_SEs
122             [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff]
123   end;
126 structure CoInd_Package =
127   Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
128     and Su=Quine_Sum val coind = true);
130 *}
132 end