src/ZF/AC/AC1_WO2.ML
author paulson
Fri, 08 Nov 1996 14:02:51 +0100
changeset 2167 5819e85ad261
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
permissions -rw-r--r--
Adjusting to new version of uresult
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
     1
(*  Title:      ZF/AC/AC1_WO2.ML
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
     3
    Author:     Krzysztof Grabczewski
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     4
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     5
The proof of AC1 ==> WO2
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     6
*)
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     7
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     8
open AC1_WO2;
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
     9
2167
5819e85ad261 Adjusting to new version of uresult
paulson
parents: 1461
diff changeset
    10
(*Establishing the existence of a bijection -- hence the need for uresult*)
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    11
val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==>  \
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1206
diff changeset
    12
\       ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    13
by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
    14
by (rtac f_subsets_imp_UN_HH_eq_x 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    15
by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    16
by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1);
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    17
by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1);
2167
5819e85ad261 Adjusting to new version of uresult
paulson
parents: 1461
diff changeset
    18
val lemma1 = uresult() |> standard;
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    19
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    20
goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2";
1206
30df104ceb91 Ran expandshort and changed spelling of Grabczewski
lcp
parents: 1196
diff changeset
    21
by (rtac allI 1);
1123
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    22
by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
5dfdc1464966 Krzysztof Grabczewski's (nearly) complete AC proofs
lcp
parents:
diff changeset
    23
by (fast_tac (AC_cs addSDs [lemma1] addSIs [Ord_Least]) 1);
1196
d43c1f7a53fe Numerous small improvements by KG and LCP
lcp
parents: 1123
diff changeset
    24
qed "AC1_WO2";