diff -r e74f694ca1da -r c7a8f374339b src/HOL/MiniML/Maybe.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/MiniML/Maybe.ML Wed Oct 25 09:46:46 1995 +0100 @@ -0,0 +1,20 @@ +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";