120 HOL_basic_ss addsimps thms |
120 HOL_basic_ss addsimps thms |
121 |
121 |
122 fun symmetric thms = |
122 fun symmetric thms = |
123 map (fn thm => thm RS @{thm sym}) thms |
123 map (fn thm => thm RS @{thm sym}) thms |
124 |
124 |
125 val supp_abs_set = @{thms supp_abs(1)[symmetric]} |
125 val supp_Abs_set = @{thms supp_Abs(1)[symmetric]} |
126 val supp_abs_res = @{thms supp_abs(2)[symmetric]} |
126 val supp_Abs_res = @{thms supp_Abs(2)[symmetric]} |
127 val supp_abs_lst = @{thms supp_abs(3)[symmetric]} |
127 val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]} |
128 |
128 |
129 fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_set |
129 fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set |
130 | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_res |
130 | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res |
131 | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_lst |
131 | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst |
132 |
132 |
133 fun mk_supp_abs_tac ctxt [] = [] |
133 fun mk_supp_abs_tac ctxt [] = [] |
134 | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs |
134 | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs |
135 | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs |
135 | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs |
136 |
136 |
137 fun mk_bn_supp_abs_tac trm = |
137 fun mk_bn_supp_abs_tac trm = |
138 trm |
138 trm |
139 |> fastype_of |
139 |> fastype_of |
140 |> body_type |
140 |> body_type |
141 |> (fn ty => case ty of |
141 |> (fn ty => case ty of |
142 @{typ "atom set"} => simp_tac (add_ss supp_abs_set) |
142 @{typ "atom set"} => simp_tac (add_ss supp_Abs_set) |
143 | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst) |
143 | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst) |
144 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
144 | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) |
145 |
145 |
146 |
146 |
147 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
147 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} |
148 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |
148 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} |