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";