equal
deleted
inserted
replaced
192 if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else |
192 if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else |
193 if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) |
193 if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x) |
194 else mk_supp ty x |
194 else mk_supp ty x |
195 val lhss = map mk_supp_arg (frees ~~ tys) |
195 val lhss = map mk_supp_arg (frees ~~ tys) |
196 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
196 val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool}) |
197 val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs) |
197 val eq = HOLogic.mk_Trueprop (supports $ fold_union lhss $ rhs) |
198 in |
198 in |
199 (names, eq) |
199 (names, eq) |
200 end |
200 end |
201 *} |
201 *} |
202 |
202 |
203 ML {* |
203 ML {* |
204 fun prove_supports ctxt perms cnst = |
204 fun prove_supports ctxt perms cnst = |
205 let |
205 let |
206 val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst |
206 val (names, eq) = mk_supports_eq ctxt cnst |
207 in |
207 in |
208 Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) |
208 Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1) |
209 end |
209 end |
210 *} |
210 *} |
211 |
211 |