equal
deleted
inserted
replaced
377 Goal "([] = rev xs) = (xs = [])"; |
377 Goal "([] = rev xs) = (xs = [])"; |
378 by (induct_tac "xs" 1); |
378 by (induct_tac "xs" 1); |
379 by Auto_tac; |
379 by Auto_tac; |
380 qed "Nil_is_rev_conv"; |
380 qed "Nil_is_rev_conv"; |
381 AddIffs [Nil_is_rev_conv]; |
381 AddIffs [Nil_is_rev_conv]; |
|
382 |
|
383 Goal "!ys. (rev xs = rev ys) = (xs = ys)"; |
|
384 by(induct_tac "xs" 1); |
|
385 by (Force_tac 1); |
|
386 br allI 1; |
|
387 by(exhaust_tac "ys" 1); |
|
388 by (Asm_simp_tac 1); |
|
389 by (Force_tac 1); |
|
390 qed_spec_mp "rev_is_rev_conv"; |
|
391 AddIffs [rev_is_rev_conv]; |
382 |
392 |
383 val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs"; |
393 val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs"; |
384 by (stac (rev_rev_ident RS sym) 1); |
394 by (stac (rev_rev_ident RS sym) 1); |
385 by (res_inst_tac [("list", "rev xs")] list.induct 1); |
395 by (res_inst_tac [("list", "rev xs")] list.induct 1); |
386 by (ALLGOALS Simp_tac); |
396 by (ALLGOALS Simp_tac); |