src/HOL/MiniML/Maybe.ML
changeset 1300 c7a8f374339b
child 1751 946efd210837
equal deleted inserted replaced
1299:e74f694ca1da 1300:c7a8f374339b
       
     1 open Maybe;
       
     2 
       
     3 (* constructor laws for bind *)
       
     4 goalw thy [bind_def] "(Ok s) bind f = (f s)";
       
     5 by (Simp_tac 1);
       
     6 qed "bind_Ok";
       
     7 
       
     8 goalw thy [bind_def] "Fail bind f = Fail";
       
     9 by (Simp_tac 1);
       
    10 qed "bind_Fail";
       
    11 
       
    12 Addsimps [bind_Ok,bind_Fail];
       
    13 
       
    14 (* expansion of bind *)
       
    15 goal thy
       
    16   "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
       
    17 by (maybe.induct_tac "res" 1);
       
    18 by (fast_tac (HOL_cs addss !simpset) 1);
       
    19 by (Asm_simp_tac 1);
       
    20 qed "expand_bind";