54 val free_SEs = Ind_Syntax.mk_free_SEs |
54 val free_SEs = Ind_Syntax.mk_free_SEs |
55 [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff] |
55 [distinct, distinct', inl_iff, inr_iff, Standard_Prod.pair_iff] |
56 end; |
56 end; |
57 |
57 |
58 |
58 |
59 functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
59 structure Ind_Package = |
60 : sig include INTR_ELIM INDRULE end = |
60 Add_inductive_def_Fun |
61 let |
61 (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP |
62 structure Intr_elim = |
62 and Su=Standard_Sum); |
63 Intr_elim_Fun(structure Inductive=Inductive and Fp=Lfp and |
|
64 Pr=Standard_Prod and Su=Standard_Sum); |
|
65 |
|
66 structure Indrule = |
|
67 Indrule_Fun (structure Inductive=Inductive and |
|
68 Pr=Standard_Prod and CP=Standard_CP and |
|
69 Su=Standard_Sum and |
|
70 Intr_elim=Intr_elim) |
|
71 in |
|
72 struct |
|
73 val thy = Intr_elim.thy |
|
74 val defs = Intr_elim.defs |
|
75 val bnd_mono = Intr_elim.bnd_mono |
|
76 val dom_subset = Intr_elim.dom_subset |
|
77 val intrs = Intr_elim.intrs |
|
78 val elim = Intr_elim.elim |
|
79 val mk_cases = Intr_elim.mk_cases |
|
80 open Indrule |
|
81 end |
|
82 end; |
|
83 |
|
84 |
|
85 structure Ind = Add_inductive_def_Fun |
|
86 (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP |
|
87 and Su=Standard_Sum); |
|
88 |
63 |
89 |
64 |
90 structure Gfp = |
65 structure Gfp = |
91 struct |
66 struct |
92 val oper = Const("gfp", [iT,iT-->iT]--->iT) |
67 val oper = Const("gfp", [iT,iT-->iT]--->iT) |
126 val free_SEs = Ind_Syntax.mk_free_SEs |
101 val free_SEs = Ind_Syntax.mk_free_SEs |
127 [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff] |
102 [distinct, distinct', inl_iff, inr_iff, Quine_Prod.pair_iff] |
128 end; |
103 end; |
129 |
104 |
130 |
105 |
131 signature COINDRULE = |
106 structure CoInd_Package = |
132 sig |
|
133 val coinduct : thm |
|
134 end; |
|
135 |
|
136 |
|
137 functor CoInd_section_Fun |
|
138 (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) |
|
139 : sig include INTR_ELIM COINDRULE end = |
|
140 let |
|
141 structure Intr_elim = |
|
142 Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and |
|
143 Pr=Quine_Prod and CP=Standard_CP and |
|
144 Su=Quine_Sum); |
|
145 in |
|
146 struct |
|
147 val thy = Intr_elim.thy |
|
148 val defs = Intr_elim.defs |
|
149 val bnd_mono = Intr_elim.bnd_mono |
|
150 val dom_subset = Intr_elim.dom_subset |
|
151 val intrs = Intr_elim.intrs |
|
152 val elim = Intr_elim.elim |
|
153 val mk_cases = Intr_elim.mk_cases |
|
154 val coinduct = Intr_elim.raw_induct |
|
155 end |
|
156 end; |
|
157 |
|
158 structure CoInd = |
|
159 Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP |
107 Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP |
160 and Su=Quine_Sum); |
108 and Su=Quine_Sum); |
161 |
109 |