equal
deleted
inserted
replaced
11 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \ |
11 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \ |
12 \ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})"; |
12 \ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})"; |
13 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); |
13 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); |
14 by (rtac f_subsets_imp_UN_HH_eq_x 1); |
14 by (rtac f_subsets_imp_UN_HH_eq_x 1); |
15 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
15 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
16 by (fast_tac (claset() addSEs [equals0E] addSDs [prem RS apply_type]) 1); |
16 by (fast_tac (claset() addSDs [prem RS apply_type]) 1); |
17 by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); |
17 by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); |
18 val lemma1 = uresult() |> standard; |
18 val lemma1 = uresult() |> standard; |
19 |
19 |
20 Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2"; |
20 Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2"; |
21 by (rtac allI 1); |
21 by (rtac allI 1); |