117 val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf}) |
117 val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf}) |
118 fun mk_conjl props = |
118 fun mk_conjl props = |
119 fold (fn a => fn b => |
119 fold (fn a => fn b => |
120 if a = @{term True} then b else |
120 if a = @{term True} then b else |
121 if b = @{term True} then a else |
121 if b = @{term True} then a else |
122 HOLogic.mk_conj (a, b)) props @{term True}; |
122 HOLogic.mk_conj (a, b)) (rev props) @{term True}; |
123 fun mk_diff a b = |
123 fun mk_diff a b = |
124 if b = noatoms then a else |
124 if b = noatoms then a else |
125 if b = a then noatoms else |
125 if b = a then noatoms else |
126 HOLogic.mk_binop @{const_name minus} (a, b); |
126 HOLogic.mk_binop @{const_name minus} (a, b); |
127 fun mk_atoms t = |
127 fun mk_atoms t = |
716 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
716 asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric] |
717 swap_fresh_fresh fresh_atom swap_at_base_simps(3)})) |
717 swap_fresh_fresh fresh_atom swap_at_base_simps(3)})) |
718 *} |
718 *} |
719 |
719 |
720 ML {* |
720 ML {* |
721 fun mk_supports_eq cnstr = |
721 fun mk_supp ty x = |
|
722 Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x |
|
723 *} |
|
724 |
|
725 ML {* |
|
726 fun mk_supports_eq thy cnstr = |
722 let |
727 let |
723 val (tys, ty) = (strip_type o fastype_of) cnstr |
728 val (tys, ty) = (strip_type o fastype_of) cnstr |
724 val names = Datatype_Prop.make_tnames tys |
729 val names = Datatype_Prop.make_tnames tys |
725 val frees = map Free (names ~~ tys) |
730 val frees = map Free (names ~~ tys) |
726 val rhs = list_comb (cnstr, frees) |
731 val rhs = list_comb (cnstr, frees) |
727 fun mk_supp ty x = |
732 |
728 Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x |
|
729 fun mk_supp_arg (x, ty) = |
733 fun mk_supp_arg (x, ty) = |
730 if is_atom @{theory} ty then mk_supp @{typ atom} (mk_atom ty $ x) else |
734 if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else |
731 if is_atom_set @{theory} ty then mk_supp @{typ "atom set"} (mk_atoms x) |
735 if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atoms x) |
732 else mk_supp ty x |
736 else mk_supp ty x |
733 val lhss = map mk_supp_arg (frees ~~ tys) |
737 val lhss = map mk_supp_arg (frees ~~ tys) |
734 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
738 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
735 val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) |
739 val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) |
736 in |
740 in |
737 (names, eq) |
741 (names, eq) |
738 end |
742 end |
739 *} |
743 *} |
740 |
744 |
741 end |
745 ML {* |
|
746 fun prove_supports ctxt perms cnst = |
|
747 let |
|
748 val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst |
|
749 in |
|
750 Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) |
|
751 end |
|
752 *} |
|
753 |
|
754 ML {* |
|
755 fun mk_fs tys = |
|
756 let |
|
757 val names = Datatype_Prop.make_tnames tys |
|
758 val frees = map Free (names ~~ tys) |
|
759 val supps = map2 mk_supp tys frees |
|
760 val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps |
|
761 in |
|
762 (names, HOLogic.mk_Trueprop (mk_conjl fin_supps)) |
|
763 end |
|
764 *} |
|
765 |
|
766 ML {* |
|
767 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW ( |
|
768 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
|
769 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom finite_insert finite.emptyI finite_Un}) |
|
770 *} |
|
771 |
|
772 ML {* |
|
773 fun prove_fs ctxt induct supports tys = |
|
774 let |
|
775 val (names, eq) = mk_fs tys |
|
776 in |
|
777 Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1) |
|
778 end |
|
779 *} |
|
780 |
|
781 end |