equal
deleted
inserted
replaced
22 |
22 |
23 val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \ |
23 val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \ |
24 \ ALL x<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m"; |
24 \ ALL x<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m"; |
25 by (rtac oallI 1); |
25 by (rtac oallI 1); |
26 by (dresolve_tac [ltD RS less_Least_subset_x] 1); |
26 by (dresolve_tac [ltD RS less_Least_subset_x] 1); |
27 by (forward_tac [HH_subset_imp_eq] 1); |
27 by (ftac HH_subset_imp_eq 1); |
28 by (etac ssubst 1); |
28 by (etac ssubst 1); |
29 by (fast_tac (claset() addIs [prem RS ballE] |
29 by (fast_tac (claset() addIs [prem RS ballE] |
30 addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); |
30 addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); |
31 val lemma2 = result(); |
31 val lemma2 = result(); |
32 |
32 |