139 fun is_atom thy typ = |
139 fun is_atom thy typ = |
140 Sign.of_sort thy (typ, @{sort at}) |
140 Sign.of_sort thy (typ, @{sort at}) |
141 |
141 |
142 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t |
142 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t |
143 | is_atom_set thy _ = false; |
143 | is_atom_set thy _ = false; |
144 *} |
144 |
|
145 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t |
|
146 | is_atom_fset thy _ = false; |
|
147 |
|
148 val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"} |
|
149 *} |
|
150 |
145 |
151 |
146 |
152 |
147 |
153 |
148 (* Like map2, only if the second list is empty passes empty lists insted of error *) |
154 (* Like map2, only if the second list is empty passes empty lists insted of error *) |
149 ML {* |
155 ML {* |
199 HOLogic.mk_conj (a, b)) (rev props) @{term True}; |
205 HOLogic.mk_conj (a, b)) (rev props) @{term True}; |
200 fun mk_diff a b = |
206 fun mk_diff a b = |
201 if b = noatoms then a else |
207 if b = noatoms then a else |
202 if b = a then noatoms else |
208 if b = a then noatoms else |
203 HOLogic.mk_binop @{const_name minus} (a, b); |
209 HOLogic.mk_binop @{const_name minus} (a, b); |
204 fun mk_atoms t = |
210 fun mk_atom_set t = |
205 let |
211 let |
206 val ty = fastype_of t; |
212 val ty = fastype_of t; |
207 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
213 val atom_ty = HOLogic.dest_setT ty --> @{typ atom}; |
208 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
214 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
209 in |
215 in |
210 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
216 (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
|
217 end; |
|
218 fun mk_atom_fset t = |
|
219 let |
|
220 val ty = fastype_of t; |
|
221 val atom_ty = dest_fsetT ty --> @{typ atom}; |
|
222 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
|
223 in |
|
224 fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)) |
211 end; |
225 end; |
212 (* Similar to one in USyntax *) |
226 (* Similar to one in USyntax *) |
213 fun mk_pair (fst, snd) = |
227 fun mk_pair (fst, snd) = |
214 let val ty1 = fastype_of fst |
228 let val ty1 = fastype_of fst |
215 val ty2 = fastype_of snd |
229 val ty2 = fastype_of snd |
286 if arg_no mem args_in_bn then |
300 if arg_no mem args_in_bn then |
287 (if is_rec_type dt then |
301 (if is_rec_type dt then |
288 (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.") |
302 (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.") |
289 else @{term "{} :: atom set"}) else |
303 else @{term "{} :: atom set"}) else |
290 if is_atom thy ty then mk_single_atom x else |
304 if is_atom thy ty then mk_single_atom x else |
291 if is_atom_set thy ty then mk_atoms x else |
305 if is_atom_set thy ty then mk_atom_set x else |
|
306 if is_atom_fset thy ty then mk_atom_fset x else |
292 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
307 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
293 @{term "{} :: atom set"} |
308 @{term "{} :: atom set"} |
294 end; |
309 end; |
295 val arg_nos = 0 upto (length dts - 1) |
310 val arg_nos = 0 upto (length dts - 1) |
296 in |
311 in |
400 val alpha = nth alpha_frees ith_dtyp; |
415 val alpha = nth alpha_frees ith_dtyp; |
401 val arg_nos = 0 upto (length dts - 1) |
416 val arg_nos = 0 upto (length dts - 1) |
402 fun fv_bind args (NONE, i, _) = |
417 fun fv_bind args (NONE, i, _) = |
403 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
418 if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else |
404 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
419 if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else |
405 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else |
420 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else |
|
421 if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else |
406 (* TODO we do not know what to do with non-atomizable things *) |
422 (* TODO we do not know what to do with non-atomizable things *) |
407 @{term "{} :: atom set"} |
423 @{term "{} :: atom set"} |
408 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
424 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
409 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
425 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
410 fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE |
426 fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE |
418 | NONE => |
434 | NONE => |
419 let |
435 let |
420 val arg = |
436 val arg = |
421 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
437 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
422 if ((is_atom thy) o fastype_of) x then mk_single_atom x else |
438 if ((is_atom thy) o fastype_of) x then mk_single_atom x else |
423 if ((is_atom_set thy) o fastype_of) x then mk_atoms x else |
439 if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else |
|
440 if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else |
424 (* TODO we do not know what to do with non-atomizable things *) |
441 (* TODO we do not know what to do with non-atomizable things *) |
425 @{term "{} :: atom set"}; |
442 @{term "{} :: atom set"}; |
426 (* If i = j then we generate it only once *) |
443 (* If i = j then we generate it only once *) |
427 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
444 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
428 val sub = fv_binds args relevant |
445 val sub = fv_binds args relevant |
834 ML {* |
851 ML {* |
835 fun supports_tac perm = |
852 fun supports_tac perm = |
836 simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( |
853 simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW ( |
837 REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN' |
854 REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN' |
838 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
855 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
839 swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh})) |
856 swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh |
|
857 supp_fset_to_set supp_fmap_atom})) |
840 *} |
858 *} |
841 |
859 |
842 ML {* |
860 ML {* |
843 fun mk_supp ty x = |
861 fun mk_supp ty x = |
844 Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x |
862 Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x |
852 val frees = map Free (names ~~ tys) |
870 val frees = map Free (names ~~ tys) |
853 val rhs = list_comb (cnstr, frees) |
871 val rhs = list_comb (cnstr, frees) |
854 |
872 |
855 fun mk_supp_arg (x, ty) = |
873 fun mk_supp_arg (x, ty) = |
856 if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else |
874 if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else |
857 if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atoms x) |
875 if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else |
|
876 if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) |
858 else mk_supp ty x |
877 else mk_supp ty x |
859 val lhss = map mk_supp_arg (frees ~~ tys) |
878 val lhss = map mk_supp_arg (frees ~~ tys) |
860 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
879 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
861 val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) |
880 val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) |
862 in |
881 in |
886 *} |
905 *} |
887 |
906 |
888 ML {* |
907 ML {* |
889 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW ( |
908 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW ( |
890 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
909 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
891 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image finite_insert finite.emptyI finite_Un}) |
910 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set |
|
911 supp_fmap_atom finite_insert finite.emptyI finite_Un}) |
892 *} |
912 *} |
893 |
913 |
894 ML {* |
914 ML {* |
895 fun prove_fs ctxt induct supports tys = |
915 fun prove_fs ctxt induct supports tys = |
896 let |
916 let |