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
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 *)
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
25 lemma def_swap_iff: "a == b ==> a = c <-> c = b"
26   by blast
28 lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
29   by simp
31 lemma refl_thin: "!!P. a = a ==> P ==> P" .
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"
40 setup IndCases.setup
41 setup DatatypeTactics.setup
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;
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;
66 structure Standard_CP = CartProd_Fun (Standard_Prod);
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;
85 structure Ind_Package =
87       (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
88        and Su=Standard_Sum val coind = false);
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;
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;
113 structure Quine_CP = CartProd_Fun (Quine_Prod);
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;
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);
136 *}
138 end