Nominal/Equivp.thy
changeset 2288 3b83960f9544
parent 2108 c5b7be27f105
child 2296 45a69c9cc4cc
equal deleted inserted replaced
2164:a5dc3558cdec 2288:3b83960f9544
   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