129 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y |
129 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y |
130 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y |
130 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y |
131 *} |
131 *} |
132 |
132 |
133 ML {* |
133 ML {* |
134 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees |
134 fun fv_bn thy dt_descr sorts fv_frees |
135 bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) = |
135 bn_fvbn bmll (fvbn, (_, ith_dtyp, args_in_bns)) = |
136 let |
136 let |
137 val {descr, sorts, ...} = dt_info; |
|
138 fun fv_bn_constr (cname, dts) (args_in_bn, bml) = |
137 fun fv_bn_constr (cname, dts) (args_in_bn, bml) = |
139 let |
138 let |
140 val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts; |
139 val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; |
141 val names = Datatype_Prop.make_tnames Ts; |
140 val names = Datatype_Prop.make_tnames Ts; |
142 val args = map Free (names ~~ Ts); |
141 val args = map Free (names ~~ Ts); |
143 val c = Const (cname, Ts ---> (nth_dtyp descr sorts ith_dtyp)); |
142 val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp)); |
144 val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn |
143 val fv_bn_bm = fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn |
145 in |
144 in |
146 HOLogic.mk_Trueprop (HOLogic.mk_eq |
145 HOLogic.mk_Trueprop (HOLogic.mk_eq |
147 (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml))) |
146 (fvbn $ list_comb (c, args), mk_union (map fv_bn_bm bml))) |
148 end; |
147 end; |
149 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
148 val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; |
150 in |
149 in |
151 map2 fv_bn_constr constrs (args_in_bns ~~ bmll) |
150 map2 fv_bn_constr constrs (args_in_bns ~~ bmll) |
152 end |
151 end |
153 *} |
152 *} |
154 |
153 |
155 ML {* |
154 ML {* |
156 fun fv_bns thy dt_info fv_frees bn_funs bclauses = |
155 fun fv_bns thy dt_descr sorts fv_frees bn_funs bclauses = |
157 let |
156 let |
158 fun mk_fvbn_free (bn, ith, _) = |
157 fun mk_fvbn_free (bn, ith, _) = |
159 let |
158 let |
160 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
159 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
161 in |
160 in |
162 (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) |
161 (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) |
163 end; |
162 end; |
164 val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); |
163 val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); |
165 val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees |
164 val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees |
166 val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs; |
165 val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs; |
167 val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs); |
166 val eqs = map2 (fv_bn thy dt_descr sorts fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs); |
168 in |
167 in |
169 (bn_fvbn, fvbn_names, eqs) |
168 (bn_fvbn, fvbn_names, eqs) |
170 end |
169 end |
171 *} |
170 *} |
172 |
171 |
186 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y |
185 | BSet (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y |
187 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y |
186 | BRes (x, y) => fv_bm_lsts thy dts args fv_frees bn_fvbn x y |
188 *} |
187 *} |
189 |
188 |
190 ML {* |
189 ML {* |
191 fun fv thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn bmll (fv_free, ith_dtyp) = |
190 fun fv thy dt_descr sorts fv_frees bn_fvbn bmll (fv_free, ith_dtyp) = |
192 let |
191 let |
193 val {descr, sorts, ...} = dt_info; |
|
194 fun fv_constr (cname, dts) bml = |
192 fun fv_constr (cname, dts) bml = |
195 let |
193 let |
196 val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts; |
194 val Ts = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts; |
197 val names = Datatype_Prop.make_tnames Ts; |
195 val names = Datatype_Prop.make_tnames Ts; |
198 val args = map Free (names ~~ Ts); |
196 val args = map Free (names ~~ Ts); |
199 val c = Const (cname, Ts ---> (nth_dtyp descr sorts ith_dtyp)); |
197 val c = Const (cname, Ts ---> (nth_dtyp dt_descr sorts ith_dtyp)); |
200 val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn |
198 val fv_bn_bm = fv_bm thy dts args fv_frees bn_fvbn |
201 in |
199 in |
202 HOLogic.mk_Trueprop (HOLogic.mk_eq |
200 HOLogic.mk_Trueprop (HOLogic.mk_eq |
203 (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml))) |
201 (fv_free $ list_comb (c, args), mk_union (map fv_bn_bm bml))) |
204 end; |
202 end; |
205 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
203 val (_, (_, _, constrs)) = nth dt_descr ith_dtyp; |
206 in |
204 in |
207 map2 fv_constr constrs bmll |
205 map2 fv_constr constrs bmll |
208 end |
206 end |
209 *} |
207 *} |
210 |
208 |
218 Function.termination_proof NONE |
216 Function.termination_proof NONE |
219 #> Proof.global_terminal_proof (Method.Basic method, NONE) |
217 #> Proof.global_terminal_proof (Method.Basic method, NONE) |
220 *} |
218 *} |
221 |
219 |
222 ML {* |
220 ML {* |
223 fun define_raw_fv dt_info bn_funs bclauses lthy = |
221 fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclauses lthy = |
224 let |
222 let |
225 val thy = ProofContext.theory_of lthy; |
223 val thy = ProofContext.theory_of lthy; |
226 val {descr as dt_descr, sorts, ...} = dt_info; |
224 val {descr as dt_descr, sorts, ...} = dt_info; |
227 |
225 |
228 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
226 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
229 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; |
227 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; |
230 val fv_frees = map Free (fv_names ~~ fv_types); |
228 val fv_frees = map Free (fv_names ~~ fv_types); |
231 |
229 |
232 val (bn_fvbn, fv_bn_names, fv_bn_eqs) = |
230 val (bn_fvbn, fv_bn_names, fv_bn_eqs) = |
233 fv_bns thy dt_info fv_frees bn_funs bclauses; |
231 fv_bns thy dt_descr sorts fv_frees bn_funs bclauses; |
234 |
232 |
235 val fvbns = map snd bn_fvbn; |
233 val fvbns = map snd bn_fvbn; |
236 val fv_nums = 0 upto (length fv_frees - 1) |
234 val fv_nums = 0 upto (length fv_frees - 1) |
237 |
235 |
238 val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums); |
236 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums); |
239 val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
237 val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
240 val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs) |
238 val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs) |
241 |
239 |
242 val lthy' = |
240 val lthy' = |
243 lthy |
241 lthy |