File PartComp.ML

goal PartComp.thy "dom(f o; g) = {x. x:dom(f) & (the (f x)):dom g}";
by (simp_tac (simpset() addsimps [dom_def,partcomp_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "dom_partcomp";

fun Rewrite_subgoal_tac thms i =
     SELECT_GOAL (rewrite_goals_tac (map mk_meta_eq thms)) i
     handle _ =>    SELECT_GOAL (rewrite_goals_tac thms) i;

goal PartComp.thy "dom(f o; g) <= dom(f)";
by (Rewrite_subgoal_tac [dom_partcomp] 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "dom_partcomp_subs";