author | nipkow |
Thu, 22 Feb 1996 18:35:16 +0100 | |
changeset 1519 | f999804f11ea |
parent 1300 | c7a8f374339b |
child 1751 | 946efd210837 |
permissions | -rw-r--r-- |
open Maybe; (* constructor laws for bind *) goalw thy [bind_def] "(Ok s) bind f = (f s)"; by (Simp_tac 1); qed "bind_Ok"; goalw thy [bind_def] "Fail bind f = Fail"; by (Simp_tac 1); qed "bind_Fail"; Addsimps [bind_Ok,bind_Fail]; (* expansion of bind *) goal thy "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))"; by (maybe.induct_tac "res" 1); by (fast_tac (HOL_cs addss !simpset) 1); by (Asm_simp_tac 1); qed "expand_bind";