src/ZF/AC/rel_is_fun.ML

better miniscoping rules: the premise C~={} is not good
because Safe_tac eliminates such assumptions.

(*  Title:      ZF/AC/rel_is_fun.ML
    ID:         $Id$
    Author:     Krzysztof Grabczewski

Lemmas needed to state when a finite relation is a function.

The criteria are cardinalities of the relation and its domain.
Used in WO6WO1.ML
*)

(*Using AC we could trivially prove, for all u, domain(u) lepoll u*)
goalw Cardinal.thy [lepoll_def]
     "!!m. [| m:nat; u lepoll m |] ==> domain(u) lepoll m";
by (etac exE 1);
by (res_inst_tac [("x",
        "lam x:domain(u). LEAST i. EX y. <x,y> : u & f`<x,y> = i")] exI 1);
by (res_inst_tac [("d","%y. fst(converse(f)`y)")] lam_injective 1);
by (fast_tac (claset() addIs [LeastI2, nat_into_Ord RS Ord_in_Ord,
                        inj_is_fun RS apply_type]) 1);
by (etac domainE 1);
by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
by (rtac LeastI2 1);
by (REPEAT (fast_tac (claset() addSEs [nat_into_Ord RS Ord_in_Ord]
              addss (simpset() addsimps [left_inverse])) 1));
qed "lepoll_m_imp_domain_lepoll_m";

goalw Cardinal.thy [function_def]
    "!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat |] ==> \
\         function(r)";
by Safe_tac;
by (resolve_tac [excluded_middle RS disjE] 1 THEN (atac 2));
by (fast_tac (claset() addSEs [lepoll_trans RS succ_lepoll_natE, 
                        Diff_sing_lepoll RSN (2, lepoll_m_imp_domain_lepoll_m)]
                addEs [not_sym RSN (2, domain_Diff_eq) RS subst]) 1);
qed "rel_domain_ex1";

goal Cardinal.thy
    "!!r. [| succ(m) lepoll domain(r);  r lepoll succ(m);  m:nat;  \
\            r<=A*B; A=domain(r) |] ==> r: A->B";
by (hyp_subst_tac 1);
by (asm_simp_tac (simpset() addsimps [Pi_iff, rel_domain_ex1]) 1);
qed "rel_is_fun";