55 |
55 |
56 (* ********************************************************************** *) |
56 (* ********************************************************************** *) |
57 (* Two cases for lemma ii *) |
57 (* Two cases for lemma ii *) |
58 (* ********************************************************************** *) |
58 (* ********************************************************************** *) |
59 Goalw [lesspoll_def] |
59 Goalw [lesspoll_def] |
60 "!! a f u. ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m ==> \ |
60 "ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m \ |
61 \ (ALL b<a. f`b ~= 0 --> (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & \ |
61 \ ==> (ALL b<a. f`b ~= 0 --> \ |
62 \ u(f,b,g,d) lesspoll m)) | \ |
62 \ (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & u(f,b,g,d) lesspoll m)) \ |
63 \ (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \ |
63 \ | (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \ |
64 \ u(f,b,g,d) eqpoll m))"; |
64 \ u(f,b,g,d) eqpoll m))"; |
65 by (Asm_simp_tac 1); |
65 by (Asm_simp_tac 1); |
66 by (blast_tac (claset() delrules [equalityI]) 1); |
66 by (blast_tac (claset() delrules [equalityI]) 1); |
67 qed "cases"; |
67 qed "cases"; |
68 |
68 |