151 map2 fv_bn_constr constrs (args_in_bns ~~ bmll) |
151 map2 fv_bn_constr constrs (args_in_bns ~~ bmll) |
152 end |
152 end |
153 *} |
153 *} |
154 |
154 |
155 ML {* |
155 ML {* |
156 fun fv_bns thy dt_info fv_frees bns bmlll = |
156 fun fv_bns thy dt_info fv_frees bn_funs bclauses = |
157 let |
157 let |
158 fun mk_fvbn_free (bn, ith, _) = |
158 fun mk_fvbn_free (bn, ith, _) = |
159 let |
159 let |
160 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
160 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
161 in |
161 in |
162 (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) |
162 (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) |
163 end; |
163 end; |
164 val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bns); |
164 val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); |
165 val bn_fvbn = (map (fn (bn, _, _) => bn) bns) ~~ fvbn_frees |
165 val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees |
166 val bmlls = map (fn (_, i, _) => nth bmlll i) bns; |
166 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 ~~ bns); |
167 val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs); |
168 in |
168 in |
169 (bn_fvbn, (fvbn_names, eqs)) |
169 (bn_fvbn, fvbn_names, eqs) |
170 end |
170 end |
171 *} |
171 *} |
172 |
172 |
173 ML {* |
173 ML {* |
174 fun fv_bm thy dts args fv_frees bn_fvbn bm = |
174 fun fv_bm thy dts args fv_frees bn_fvbn bm = |
218 Function.termination_proof NONE |
218 Function.termination_proof NONE |
219 #> Proof.global_terminal_proof (Method.Basic method, NONE) |
219 #> Proof.global_terminal_proof (Method.Basic method, NONE) |
220 *} |
220 *} |
221 |
221 |
222 ML {* |
222 ML {* |
223 fun define_raw_fv dt_info bns bmlll lthy = |
223 fun define_raw_fv dt_info bn_funs bclauses lthy = |
224 let |
224 let |
225 val thy = ProofContext.theory_of lthy; |
225 val thy = ProofContext.theory_of lthy; |
226 val {descr, sorts, ...} = dt_info; |
226 val {descr as dt_descr, sorts, ...} = dt_info; |
227 |
227 |
228 val fv_names = prefix_dt_names descr sorts "fv_" |
228 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
229 |
229 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; |
230 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) descr; |
|
231 val fv_frees = map Free (fv_names ~~ fv_types); |
230 val fv_frees = map Free (fv_names ~~ fv_types); |
232 val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll; |
231 |
|
232 val (bn_fvbn, fv_bn_names, fv_bn_eqs) = |
|
233 fv_bns thy dt_info fv_frees bn_funs bclauses; |
233 |
234 |
234 val fvbns = map snd bn_fvbn; |
235 val fvbns = map snd bn_fvbn; |
235 val fv_nums = 0 upto (length fv_frees - 1) |
236 val fv_nums = 0 upto (length fv_frees - 1) |
236 |
237 |
237 val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bmlll (fv_frees ~~ fv_nums); |
238 val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums); |
238 val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
239 val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
239 val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs) |
240 val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs) |
240 |
241 |
241 val lthy' = |
242 val lthy' = |
242 lthy |
243 lthy |