src/FOL/ex/cla.ML
 changeset 644 112cf8574cf1 parent 492 7bc980c7585e child 665 97e9ad6c1c4a
equal 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);`