equal
deleted
inserted
replaced
379 writeln"Problem 49 NOT PROVED AUTOMATICALLY"; |
379 writeln"Problem 49 NOT PROVED AUTOMATICALLY"; |
380 (*Hard because it involves substitution for Vars; |
380 (*Hard because it involves substitution for Vars; |
381 the type constraint ensures that x,y,z have the same type as a,b,u. *) |
381 the type constraint ensures that x,y,z have the same type as a,b,u. *) |
382 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \ |
382 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \ |
383 \ --> (! u::'a. P(u))"; |
383 \ --> (! u::'a. P(u))"; |
384 by (Classical.safe_tac (claset())); |
384 by (Classical.Safe_tac); |
385 by (res_inst_tac [("x","a")] allE 1); |
385 by (res_inst_tac [("x","a")] allE 1); |
386 by (assume_tac 1); |
386 by (assume_tac 1); |
387 by (res_inst_tac [("x","b")] allE 1); |
387 by (res_inst_tac [("x","b")] allE 1); |
388 by (assume_tac 1); |
388 by (assume_tac 1); |
389 by (Blast_tac 1); |
389 by (Blast_tac 1); |