180 then mk_atom_set_ty ty t |
180 then mk_atom_set_ty ty t |
181 else if is_atom_fset ctxt ty |
181 else if is_atom_fset ctxt ty |
182 then mk_atom_fset_ty ty t |
182 then mk_atom_fset_ty ty t |
183 else if is_atom_list ctxt ty |
183 else if is_atom_list ctxt ty |
184 then mk_atom_list_ty ty t |
184 then mk_atom_list_ty ty t |
185 else raise TERM ("atomify", [t]) |
185 else raise TERM ("atomify: term is not an atom, set or list of atoms", [t]) |
186 |
186 |
187 fun setify_ty ctxt ty t = |
187 fun setify_ty ctxt ty t = |
188 if is_atom ctxt ty |
188 if is_atom ctxt ty |
189 then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] |
189 then HOLogic.mk_set @{typ atom} [mk_atom_ty ty t] |
190 else if is_atom_set ctxt ty |
190 else if is_atom_set ctxt ty |
191 then mk_atom_set_ty ty t |
191 then mk_atom_set_ty ty t |
192 else if is_atom_fset ctxt ty |
192 else if is_atom_fset ctxt ty |
193 then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t |
193 then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t |
194 else if is_atom_list ctxt ty |
194 else if is_atom_list ctxt ty |
195 then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t |
195 then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t |
196 else raise TERM ("setify", [t]) |
196 else raise TERM ("setify: term is not an atom, set or list of atoms", [t]) |
197 |
197 |
198 fun listify_ty ctxt ty t = |
198 fun listify_ty ctxt ty t = |
199 if is_atom ctxt ty |
199 if is_atom ctxt ty |
200 then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] |
200 then HOLogic.mk_list @{typ atom} [mk_atom_ty ty t] |
201 else if is_atom_list ctxt ty |
201 else if is_atom_list ctxt ty |
202 then mk_atom_list_ty ty t |
202 then mk_atom_list_ty ty t |
203 else raise TERM ("listify", [t]) |
203 else raise TERM ("listify: term is not an atom or list of atoms", [t]) |
204 |
204 |
205 fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t |
205 fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t |
206 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
206 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
207 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
207 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
208 |
208 |
487 |
487 |
488 fun transform_prem2 ctxt names thm = |
488 fun transform_prem2 ctxt names thm = |
489 map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm |
489 map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm |
490 |
490 |
491 |
491 |
492 (* transformes a theorem into one of the object logic *) |
492 (* transforms a theorem into one of the object logic *) |
493 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars; |
493 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars; |
494 fun atomize_rule i thm = |
494 fun atomize_rule i thm = |
495 Conv.fconv_rule (Conv.concl_conv i Object_Logic.atomize) thm |
495 Conv.fconv_rule (Conv.concl_conv i Object_Logic.atomize) thm |
496 fun atomize_concl thm = atomize_rule (length (prems_of thm)) thm |
496 fun atomize_concl thm = atomize_rule (length (prems_of thm)) thm |
497 |
|
498 |
497 |
499 |
498 |
500 (* applies a tactic to a formula composed of conjunctions *) |
499 (* applies a tactic to a formula composed of conjunctions *) |
501 fun conj_tac tac i = |
500 fun conj_tac tac i = |
502 let |
501 let |