13 |
13 |
14 ML {* |
14 ML {* |
15 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
15 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
16 |
16 |
17 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x]; |
17 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x]; |
|
18 |
18 val noatoms = @{term "{} :: atom set"}; |
19 val noatoms = @{term "{} :: atom set"}; |
19 fun mk_union sets = |
20 fun mk_union sets = |
20 fold (fn a => fn b => |
21 fold (fn a => fn b => |
21 if a = noatoms then b else |
22 if a = noatoms then b else |
22 if b = noatoms then a else |
23 if b = noatoms then a else |
23 if a = b then a else |
24 if a = b then a else |
24 HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; |
25 HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms; |
25 *} |
26 *} |
26 |
27 |
27 ML {* |
28 ML {* |
28 fun is_atom thy typ = |
29 fun is_atom thy ty = |
29 Sign.of_sort thy (typ, @{sort at}) |
30 Sign.of_sort thy (ty, @{sort at}) |
30 |
31 |
31 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t |
32 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t |
32 | is_atom_set _ _ = false; |
33 | is_atom_set _ _ = false; |
33 |
34 |
34 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t |
35 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t |
38 let |
39 let |
39 val ty = fastype_of t; |
40 val ty = fastype_of t; |
40 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
41 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
41 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
42 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
42 in |
43 in |
43 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
44 (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t) |
44 end; |
45 end; |
45 |
46 |
46 fun mk_atom_fset t = |
47 fun mk_atom_fset t = |
47 let |
48 let |
48 val ty = fastype_of t; |
49 val ty = fastype_of t; |
49 val atom_ty = dest_fsetT ty --> @{typ atom}; |
50 val atom_ty = dest_fsetT ty --> @{typ atom}; |
50 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
51 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
51 val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"} |
52 val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"} |
52 in |
53 in |
53 fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)) |
54 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ mk_atom_ty atom_ty t) |
54 end; |
55 end; |
55 |
56 |
56 fun mk_diff a b = |
57 fun mk_diff a b = |
57 if b = noatoms then a else |
58 if b = noatoms then a else |
58 if b = a then noatoms else |
59 if b = a then noatoms else |
59 HOLogic.mk_binop @{const_name minus} (a, b); |
60 HOLogic.mk_binop @{const_name minus} (a, b); |
60 *} |
61 *} |
61 |
62 |
62 ML {* |
63 ML {* |
63 fun atoms thy x = |
64 fun atoms thy t = |
64 let |
65 let |
65 val ty = fastype_of x; |
66 val ty = fastype_of t; |
66 in |
67 in |
67 if is_atom thy ty then mk_single_atom x else |
68 if is_atom thy ty |
68 if is_atom_set thy ty then mk_atom_set x else |
69 then mk_single_atom t |
69 if is_atom_fset thy ty then mk_atom_fset x else |
70 else if is_atom_set thy ty |
70 @{term "{} :: atom set"} |
71 then mk_atom_set t |
|
72 else if is_atom_fset thy ty |
|
73 then mk_atom_fset t |
|
74 else noatoms |
71 end |
75 end |
72 *} |
76 *} |
73 |
77 |
74 ML {* |
78 ML {* |
75 fun setify x = |
79 fun setify x = |
76 if fastype_of x = @{typ "atom list"} then |
80 if fastype_of x = @{typ "atom list"} |
77 Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x |
81 then @{term "set::atom list \<Rightarrow> atom set"} $ x |
|
82 else x |
78 *} |
83 *} |
79 |
84 |
80 ML {* |
85 ML {* |
81 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
86 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
82 let |
87 let |
197 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
202 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
198 in |
203 in |
199 map2 fv_constr constrs bmll |
204 map2 fv_constr constrs bmll |
200 end |
205 end |
201 *} |
206 *} |
|
207 |
202 ML {* |
208 ML {* |
203 val by_pat_completeness_auto = |
209 val by_pat_completeness_auto = |
204 Proof.global_terminal_proof |
210 Proof.global_terminal_proof |
205 (Method.Basic Pat_Completeness.pat_completeness, |
211 (Method.Basic Pat_Completeness.pat_completeness, |
206 SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) |
212 SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) |
211 *} |
217 *} |
212 |
218 |
213 |
219 |
214 |
220 |
215 ML {* |
221 ML {* |
216 fun define_fv dt_info bns bmlll lthy = |
222 fun define_raw_fv dt_info bns bmlll lthy = |
217 let |
223 let |
218 val thy = ProofContext.theory_of lthy; |
224 val thy = ProofContext.theory_of lthy; |
219 val {descr, sorts, ...} = dt_info; |
225 val {descr, sorts, ...} = dt_info; |
220 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
226 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
221 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
227 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |