--- a/src/HOL/MiniML/Maybe.ML Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/Maybe.ML Fri Jan 17 18:50:04 1997 +0100
@@ -1,27 +1,31 @@
-open Maybe;
+(* Title: HOL/MiniML/Maybe.ML
+ ID: $Id$
+ Author: Wolfgang Naraschewski and Tobias Nipkow
+ Copyright 1996 TU Muenchen
+*)
-(* 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";
+(* constructor laws for option_bind *)
+goalw thy [option_bind_def] "option_bind (Some s) f = (f s)";
by (Simp_tac 1);
-qed "bind_Fail";
+qed "option_bind_Some";
-Addsimps [bind_Ok,bind_Fail];
+goalw thy [option_bind_def] "option_bind None f = None";
+by (Simp_tac 1);
+qed "option_bind_None";
-(* expansion of bind *)
+Addsimps [option_bind_Some,option_bind_None];
+
+(* expansion of option_bind *)
goal thy
- "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
-by (maybe.induct_tac "res" 1);
+ "P(option_bind res f) = ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
+by (option.induct_tac "res" 1);
by (fast_tac (HOL_cs addss !simpset) 1);
by (Asm_simp_tac 1);
-qed "expand_bind";
+qed "expand_option_bind";
goal Maybe.thy
- "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
-by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
-qed "bind_eq_Fail";
+ "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
+by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
+qed "option_bind_eq_None";
-Addsimps [bind_eq_Fail];
+Addsimps [option_bind_eq_None];