equal
deleted
inserted
replaced
63 end; |
63 end; |
64 |
64 |
65 signature INDUCTIVE = (** Description of a (co)inductive defn **) |
65 signature INDUCTIVE = (** Description of a (co)inductive defn **) |
66 sig |
66 sig |
67 val thy : theory (*parent theory*) |
67 val thy : theory (*parent theory*) |
|
68 val thy_name : string (*name of generated theory*) |
68 val rec_doms : (string*string) list (*recursion ops and their domains*) |
69 val rec_doms : (string*string) list (*recursion ops and their domains*) |
69 val sintrs : string list (*desired introduction rules*) |
70 val sintrs : string list (*desired introduction rules*) |
70 val monos : thm list (*monotonicity of each M operator*) |
71 val monos : thm list (*monotonicity of each M operator*) |
71 val con_defs : thm list (*definitions of the constructors*) |
72 val con_defs : thm list (*definitions of the constructors*) |
72 val type_intrs : thm list (*type-checking intro rules*) |
73 val type_intrs : thm list (*type-checking intro rules*) |
74 end; |
75 end; |
75 |
76 |
76 signature INTR_ELIM = |
77 signature INTR_ELIM = |
77 sig |
78 sig |
78 val thy : theory (*new theory*) |
79 val thy : theory (*new theory*) |
|
80 val thy_name : string (*name of generated theory*) |
79 val defs : thm list (*definitions made in thy*) |
81 val defs : thm list (*definitions made in thy*) |
80 val bnd_mono : thm (*monotonicity for the lfp definition*) |
82 val bnd_mono : thm (*monotonicity for the lfp definition*) |
81 val unfold : thm (*fixed-point equation*) |
83 val unfold : thm (*fixed-point equation*) |
82 val dom_subset : thm (*inclusion of recursive set in dom*) |
84 val dom_subset : thm (*inclusion of recursive set in dom*) |
83 val intrs : thm list (*introduction rules*) |
85 val intrs : thm list (*introduction rules*) |
208 map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); |
210 map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); |
209 |
211 |
210 val thy = |
212 val thy = |
211 Ind.thy |
213 Ind.thy |
212 |> add_axioms_i axpairs |
214 |> add_axioms_i axpairs |
213 |> add_thyname (big_rec_name ^ "_Inductive"); |
215 |> add_thyname thy_name; |
214 |
216 |
215 val defs = map (get_axiom thy o #1) axpairs; |
217 val defs = map (get_axiom thy o #1) axpairs; |
216 |
218 |
217 val big_rec_def::part_rec_defs = defs; |
219 val big_rec_def::part_rec_defs = defs; |
218 |
220 |