48 val ty = fastype_of t; |
48 val ty = fastype_of t; |
49 val atom_ty = dest_fsetT ty --> @{typ atom}; |
49 val atom_ty = dest_fsetT ty --> @{typ atom}; |
50 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
50 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
51 val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"} |
51 val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"} |
52 in |
52 in |
53 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ mk_atom_ty atom_ty t) |
53 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
54 end; |
54 end; |
55 |
55 |
56 fun mk_diff a b = |
56 fun mk_diff a b = |
57 if b = noatoms then a else |
57 if b = noatoms then a else |
58 if b = a then noatoms else |
58 if b = a then noatoms else |
207 |
207 |
208 ML {* |
208 ML {* |
209 *} |
209 *} |
210 |
210 |
211 ML {* |
211 ML {* |
212 fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclauses 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 |
217 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
217 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
218 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; |
218 val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; |
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 bclauses; |
222 fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss; |
223 |
223 |
224 val fvbns = map snd bn_fvbn; |
224 val fvbns = 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) bclauses (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) |
230 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
230 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
231 |
231 |
232 fun pat_completeness_auto ctxt = |
232 fun pat_completeness_auto ctxt = |