src/HOL/MiniML/Maybe.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2525 477c05586286
child 2625 69c1b8a493de
permissions -rw-r--r--
added AxClasses test;
     1 (* Title:     HOL/MiniML/Maybe.ML
     2    ID:        $Id$
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1996 TU Muenchen
     5 *)
     6 
     7 (* constructor laws for option_bind *)
     8 goalw thy [option_bind_def] "option_bind (Some s) f = (f s)";
     9 by (Simp_tac 1);
    10 qed "option_bind_Some";
    11 
    12 goalw thy [option_bind_def] "option_bind None f = None";
    13 by (Simp_tac 1);
    14 qed "option_bind_None";
    15 
    16 Addsimps [option_bind_Some,option_bind_None];
    17 
    18 (* expansion of option_bind *)
    19 goal thy
    20   "P(option_bind res f) = ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
    21 by (option.induct_tac "res" 1);
    22 by (fast_tac (HOL_cs addss !simpset) 1);
    23 by (Asm_simp_tac 1);
    24 qed "expand_option_bind";
    25 
    26 goal Maybe.thy
    27   "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    28 by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
    29 qed "option_bind_eq_None";
    30 
    31 Addsimps [option_bind_eq_None];