98 let |
99 let |
99 val Ts = map (typ_of_dtyp descr sorts) dts; |
100 val Ts = map (typ_of_dtyp descr sorts) dts; |
100 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
101 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
101 val args = map Free (names ~~ Ts); |
102 val args = map Free (names ~~ Ts); |
102 val c = Const (cname, Ts ---> (nth_dtyp i)); |
103 val c = Const (cname, Ts ---> (nth_dtyp i)); |
103 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
104 val fv_c = nth fv_frees i; |
104 fun fv_bind (NONE, i) = |
105 fun fv_bind (NONE, i) = |
105 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
106 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
106 (* TODO we assume that all can be 'atomized' *) |
107 (* TODO we assume that all can be 'atomized' *) |
107 if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else |
108 if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else |
108 mk_single_atom (nth args i) |
109 mk_single_atom (nth args i) |
126 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
127 (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))) |
127 end; |
128 end; |
128 fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; |
129 fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds; |
129 val fv_eqs = flat (map2 fv_eq descr bindsall) |
130 val fv_eqs = flat (map2 fv_eq descr bindsall) |
130 in |
131 in |
|
132 (* The snd will be removed later *) |
131 snd (Primrec.add_primrec |
133 snd (Primrec.add_primrec |
132 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
134 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy) |
133 end |
135 end |
134 *} |
136 *} |
135 |
137 |
136 (* tests: |
138 ML {* |
|
139 fun define_alpha full_tname bindsall lthy = |
|
140 let |
|
141 val thy = ProofContext.theory_of lthy; |
|
142 val {descr, ...} = Datatype.the_info thy full_tname; |
|
143 val sorts = []; (* TODO *) |
|
144 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
|
145 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
|
146 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
|
147 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
|
148 val alpha_frees = map Free (alpha_names ~~ alpha_types); |
|
149 fun alpha_eq_constr i (cname, dts) bindcs = |
|
150 let |
|
151 val Ts = map (typ_of_dtyp descr sorts) dts; |
|
152 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
|
153 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
|
154 val args = map Free (names ~~ Ts); |
|
155 val args2 = map Free (names2 ~~ Ts); |
|
156 val c = Const (cname, Ts ---> (nth_dtyp i)); |
|
157 val alpha = nth alpha_frees i; |
|
158 in |
|
159 (Attrib.empty_binding, HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)))) |
|
160 end; |
|
161 fun alpha_eq (i, (_, _, constrs)) binds = map2 (alpha_eq_constr i) constrs binds; |
|
162 val alpha_eqs = flat (map2 alpha_eq descr bindsall) |
|
163 in |
|
164 (* The snd will be removed later *) |
|
165 snd (Inductive.add_inductive_i |
|
166 {quiet_mode = false, verbose = true, alt_name = Binding.empty, |
|
167 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
|
168 (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] (alpha_eqs) [] lthy) |
|
169 end |
|
170 *} |
137 |
171 |
138 atom_decl name |
172 atom_decl name |
139 |
173 |
140 datatype ty = |
174 (*datatype ty = |
141 Var "name set" |
175 Var "name set" |
142 |
176 |
143 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} |
177 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *} |
144 |
178 |
145 local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *} |
179 local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *} |
146 print_theorems |
180 print_theorems |
|
181 *) |
147 |
182 |
148 datatype rtrm1 = |
183 datatype rtrm1 = |
149 rVr1 "name" |
184 rVr1 "name" |
150 | rAp1 "rtrm1" "rtrm1" |
185 | rAp1 "rtrm1" "rtrm1" |
151 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
186 | rLm1 "name" "rtrm1" --"name is bound in trm1" |
167 local_setup {* define_raw_fv "Fv.rtrm1" |
202 local_setup {* define_raw_fv "Fv.rtrm1" |
168 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
203 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
169 [[], [[]], [[], []]]] *} |
204 [[], [[]], [[], []]]] *} |
170 print_theorems |
205 print_theorems |
171 |
206 |
172 *) |
207 local_setup {* define_alpha "Fv.rtrm1" |
|
208 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]], |
|
209 [[], [[]], [[], []]]] *} |
|
210 print_theorems |
|
211 |
173 |
212 |
174 end |
213 end |