equal
deleted
inserted
replaced
80 then @{term "set::atom list \<Rightarrow> atom set"} $ x |
80 then @{term "set::atom list \<Rightarrow> atom set"} $ x |
81 else x |
81 else x |
82 *} |
82 *} |
83 |
83 |
84 ML {* |
84 ML {* |
|
85 fun fv_body thy dts args fv_frees supp i = |
|
86 let |
|
87 val x = nth args i; |
|
88 val dt = nth dts i; |
|
89 in |
|
90 if Datatype_Aux.is_rec_type dt |
|
91 then nth fv_frees (Datatype_Aux.body_index dt) $ x |
|
92 else (if supp then mk_supp x else atoms thy x) |
|
93 end |
|
94 *} |
|
95 |
|
96 ML {* |
85 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
97 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
86 let |
98 let |
87 fun fv_body supp i = |
99 val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys) |
88 let |
|
89 val x = nth args i; |
|
90 val dt = nth dts i; |
|
91 in |
|
92 if Datatype_Aux.is_rec_type dt |
|
93 then nth fv_frees (Datatype_Aux.body_index dt) $ x |
|
94 else (if supp then mk_supp x else atoms thy x) |
|
95 end |
|
96 val fv_bodys = mk_union (map (fv_body true) bodys) |
|
97 val bound_vars = |
100 val bound_vars = |
98 case binds of |
101 case binds of |
99 [(SOME bn, i)] => setify (bn $ nth args i) |
102 [(SOME bn, i)] => setify (bn $ nth args i) |
100 | _ => mk_union (map (fv_body false) (map snd binds)); |
103 | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds)); |
101 val non_rec_vars = |
104 val non_rec_vars = |
102 case binds of |
105 case binds of |
103 [(SOME bn, i)] => |
106 [(SOME bn, i)] => |
104 if i mem bodys |
107 if i mem bodys |
105 then noatoms |
108 then noatoms |
204 map2 fv_constr constrs bclausess |
207 map2 fv_constr constrs bclausess |
205 end |
208 end |
206 *} |
209 *} |
207 |
210 |
208 ML {* |
211 ML {* |
209 *} |
|
210 |
|
211 ML {* |
|
212 fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy = |
212 fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy = |
213 let |
213 let |
214 val thy = ProofContext.theory_of lthy; |
214 val thy = ProofContext.theory_of lthy; |
215 val {descr as dt_descr, sorts, ...} = dt_info; |
215 val {descr as dt_descr, sorts, ...} = dt_info; |
216 |
216 |
219 val fv_frees = map Free (fv_names ~~ fv_types); |
219 val fv_frees = map Free (fv_names ~~ fv_types); |
220 |
220 |
221 val (bn_fvbn, fv_bn_names, fv_bn_eqs) = |
221 val (bn_fvbn, fv_bn_names, fv_bn_eqs) = |
222 fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; |
222 fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; |
223 |
223 |
224 val fvbns = map snd bn_fvbn; |
224 val fv_bns = map snd bn_fvbn; |
225 val fv_nums = 0 upto (length fv_frees - 1) |
225 val fv_nums = 0 upto (length fv_frees - 1) |
226 |
226 |
227 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclausesss (fv_frees ~~ fv_nums); |
227 val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclausesss (fv_frees ~~ fv_nums); |
228 |
228 |
229 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
229 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
239 |
239 |
240 val (info, lthy') = Function.add_function all_fv_names all_fv_eqs |
240 val (info, lthy') = Function.add_function all_fv_names all_fv_eqs |
241 Function_Common.default_config pat_completeness_auto lthy |
241 Function_Common.default_config pat_completeness_auto lthy |
242 |
242 |
243 val lthy'' = prove_termination (Local_Theory.restore lthy') |
243 val lthy'' = prove_termination (Local_Theory.restore lthy') |
244 in |
244 |
245 ((fv_frees, fvbns), info, lthy'') |
245 val morphism = ProofContext.export_morphism lthy'' lthy |
246 end |
246 val fv_frees_exp = map (Morphism.term morphism) fv_frees |
247 *} |
247 val fv_bns_exp = map (Morphism.term morphism) fv_bns |
248 |
248 |
249 end |
249 in |
|
250 ((fv_frees_exp, fv_bns_exp), info, lthy'') |
|
251 end |
|
252 *} |
|
253 |
|
254 end |