src/HOL/MiniML/Maybe.ML
changeset 2525 477c05586286
parent 2058 ff04984186e9
child 2625 69c1b8a493de
equal deleted inserted replaced
2524:dd0f298b024c 2525:477c05586286
     1 open Maybe;
     1 (* Title:     HOL/MiniML/Maybe.ML
       
     2    ID:        $Id$
       
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
       
     4    Copyright  1996 TU Muenchen
       
     5 *)
     2 
     6 
     3 (* constructor laws for bind *)
     7 (* constructor laws for option_bind *)
     4 goalw thy [bind_def] "(Ok s) bind f = (f s)";
     8 goalw thy [option_bind_def] "option_bind (Some s) f = (f s)";
     5 by (Simp_tac 1);
     9 by (Simp_tac 1);
     6 qed "bind_Ok";
    10 qed "option_bind_Some";
     7 
    11 
     8 goalw thy [bind_def] "Fail bind f = Fail";
    12 goalw thy [option_bind_def] "option_bind None f = None";
     9 by (Simp_tac 1);
    13 by (Simp_tac 1);
    10 qed "bind_Fail";
    14 qed "option_bind_None";
    11 
    15 
    12 Addsimps [bind_Ok,bind_Fail];
    16 Addsimps [option_bind_Some,option_bind_None];
    13 
    17 
    14 (* expansion of bind *)
    18 (* expansion of option_bind *)
    15 goal thy
    19 goal thy
    16   "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
    20   "P(option_bind res f) = ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
    17 by (maybe.induct_tac "res" 1);
    21 by (option.induct_tac "res" 1);
    18 by (fast_tac (HOL_cs addss !simpset) 1);
    22 by (fast_tac (HOL_cs addss !simpset) 1);
    19 by (Asm_simp_tac 1);
    23 by (Asm_simp_tac 1);
    20 qed "expand_bind";
    24 qed "expand_option_bind";
    21 
    25 
    22 goal Maybe.thy
    26 goal Maybe.thy
    23   "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
    27   "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    24 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    28 by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
    25 qed "bind_eq_Fail";
    29 qed "option_bind_eq_None";
    26 
    30 
    27 Addsimps [bind_eq_Fail];
    31 Addsimps [option_bind_eq_None];