author | clasohm |
Tue, 30 Jan 1996 13:42:57 +0100 | |
changeset 1461 | 6bcb44e4d6e5 |
parent 1208 | bc3093616ba4 |
child 1924 | 0f1a583457da |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/rel_is_fun.ML |
992 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
992 | 4 |
|
5 |
Lemmas needed to state when a finite relation is a function. |
|
6 |
||
7 |
The criteria are cardinalities of the relation and its domain. |
|
8 |
Used in WO6WO1.ML |
|
9 |
*) |
|
10 |
||
1070 | 11 |
(*Using AC we could trivially prove, for all u, domain(u) lepoll u*) |
992 | 12 |
goalw Cardinal.thy [lepoll_def] |
13 |
"!!m. [| m:nat; u lepoll m |] ==> domain(u) lepoll m"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1070
diff
changeset
|
14 |
by (etac exE 1); |
992 | 15 |
by (res_inst_tac [("x", |
1461 | 16 |
"lam x:domain(u). LEAST i. EX y. <x,y> : u & f`<x,y> = i")] exI 1); |
992 | 17 |
by (res_inst_tac [("d","%y. fst(converse(f)`y)")] lam_injective 1); |
18 |
by (fast_tac (ZF_cs addIs [LeastI2, nat_into_Ord RS Ord_in_Ord, |
|
1461 | 19 |
inj_is_fun RS apply_type]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1070
diff
changeset
|
20 |
by (etac domainE 1); |
992 | 21 |
by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1070
diff
changeset
|
22 |
by (rtac LeastI2 1); |
992 | 23 |
by (REPEAT (fast_tac (ZF_cs addIs [fst_conv, left_inverse RS ssubst] |
1461 | 24 |
addSEs [nat_into_Ord RS Ord_in_Ord]) 1)); |
992 | 25 |
val lepoll_m_imp_domain_lepoll_m = result(); |
26 |
||
27 |
goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1070
diff
changeset
|
28 |
by (rtac equalityI 1); |
992 | 29 |
by (fast_tac (ZF_cs addSIs [domain_mono]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1070
diff
changeset
|
30 |
by (rtac subsetI 1); |
992 | 31 |
by (excluded_middle_tac "x = a" 1); |
32 |
by (REPEAT (fast_tac (ZF_cs addSIs [domainI] addSEs [domainE]) 1)); |
|
1070 | 33 |
val domain_Diff_eq_domain = result(); |
992 | 34 |
|
1070 | 35 |
goalw Cardinal.thy [function_def] |
992 | 36 |
"!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat |] ==> \ |
1461 | 37 |
\ function(r)"; |
1070 | 38 |
by (safe_tac ZF_cs); |
992 | 39 |
by (resolve_tac [excluded_middle RS disjE] 1 THEN (atac 2)); |
40 |
by (fast_tac (ZF_cs addSEs [lepoll_trans RS succ_lepoll_natE, |
|
1461 | 41 |
Diff_sing_lepoll RSN (2, lepoll_m_imp_domain_lepoll_m)] |
42 |
addEs [not_sym RSN (2, domain_Diff_eq_domain) RS subst]) 1); |
|
992 | 43 |
val rel_domain_ex1 = result(); |
44 |
||
45 |
goal Cardinal.thy |
|
46 |
"!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat; \ |
|
1461 | 47 |
\ r<=A*B; A=domain(r) |] ==> r: A->B"; |
992 | 48 |
by (hyp_subst_tac 1); |
1070 | 49 |
by (asm_simp_tac (ZF_ss addsimps [Pi_iff, rel_domain_ex1]) 1); |
992 | 50 |
val rel_is_fun = result(); |