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 section\<open>Inductive and Coinductive Definitions\<close> |
|
13 |
|
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" :: quasi_command |
|
20 begin |
|
21 |
|
22 lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b" |
|
23 by blast |
|
24 |
|
25 lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b" |
|
26 by simp |
|
27 |
|
28 lemma refl_thin: "!!P. a = a ==> P ==> P" . |
|
29 |
|
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" |
|
36 |
|
37 ML \<open> |
|
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; |
|
47 |
|
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; |
|
59 |
|
60 structure Standard_CP = CartProd_Fun (Standard_Prod); |
|
61 |
|
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; |
|
77 |
|
78 |
|
79 structure Ind_Package = |
|
80 Add_inductive_def_Fun |
|
81 (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP |
|
82 and Su=Standard_Sum val coind = false); |
|
83 |
|
84 |
|
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; |
|
94 |
|
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; |
|
106 |
|
107 structure Quine_CP = CartProd_Fun (Quine_Prod); |
|
108 |
|
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; |
|
124 |
|
125 |
|
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); |
|
129 |
|
130 \<close> |
|
131 |
|
132 end |
|