src/FOL/ex/cla.ML
changeset 644 112cf8574cf1
parent 492 7bc980c7585e
child 665 97e9ad6c1c4a
equal deleted inserted replaced
643:1e8fea151d2e 644:112cf8574cf1
   466 by (fast_tac FOL_cs 1);
   466 by (fast_tac FOL_cs 1);
   467 result();
   467 result();
   468 
   468 
   469 writeln"Problem 58  NOT PROVED AUTOMATICALLY";
   469 writeln"Problem 58  NOT PROVED AUTOMATICALLY";
   470 goal FOL.thy "(ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
   470 goal FOL.thy "(ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
   471 val f_cong = read_instantiate [("t","f")] subst_context;
   471 by (fast_tac (FOL_cs addEs [subst_context]) 1);
   472 by (fast_tac (FOL_cs addIs [f_cong]) 1);
       
   473 result();
   472 result();
   474 
   473 
   475 writeln"Problem 59";
   474 writeln"Problem 59";
   476 goal FOL.thy "(ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
   475 goal FOL.thy "(ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
   477 by (best_tac FOL_dup_cs 1);
   476 by (best_tac FOL_dup_cs 1);