(*Make atomic rewrite rules*) fun atomize r = case Thm.concl_of r of
\<^Const_>\<open>Trueprop for \<open>Abs(_,_,a)\<close> \<open>Abs(_,_,c)\<close>\<close> =>
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
([], [p]) =>
(case p of
\<^Const_>\<open>imp for _ _\<close> => atomize(r RS @{thm mp_R})
| \<^Const_>\<open>conj for _ _\<close> => atomize(r RS @{thm conjunct1}) @
atomize(r RS @{thm conjunct2})
| \<^Const_>\<open>All _ for _\<close> => atomize(r RS @{thm spec})
| \<^Const_>\<open>True\<close> => [] (*True is DELETED*)
| \<^Const_>\<open>False\<close> => [] (*should False do something?*)
| _ => [r])
| _ => []) (*ignore theorem unless it has precisely one conclusion*)
| _ => [r];
(*Make meta-equalities.*) fun mk_meta_eq ctxt th = case Thm.concl_of th of
\<^Const_>\<open>Pure.eq _ for _ _\<close> => th
| \<^Const_>\<open>Trueprop for \<open>Abs(_,_,a)\<close> \<open>Abs(_,_,c)\<close>\<close> =>
(case (Cla.forms_of_seq a, Cla.forms_of_seq c) of
([], [p]) =>
(case p of
\<^Const_>\<open>equal _ for _ _\<close> => th RS @{thm eq_reflection}
| \<^Const_>\<open>iff for _ _\<close> => th RS @{thm iff_reflection}
| \<^Const_>\<open>Not for _\<close> => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T})
| _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));
(*Replace premises x=y, X<->Y by X==Y*) fun mk_meta_prems ctxt =
rule_by_tactic ctxt
(REPEAT_FIRST (resolve_tac ctxt [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}]));
(*Congruence rules for = or <-> (instead of ==)*) fun mk_meta_cong ctxt rl =
Drule.zero_var_indexes (mk_meta_eq ctxt (mk_meta_prems ctxt rl)) handle THM _ =>
error("Premises and conclusion of congruence rules must use =-equality or <->");
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung:
(vorverarbeitet)
¤
