src/HOL/MiniML/Maybe.ML
changeset 5184 9b8547a9496a
parent 5069 3ea049f7979d
equal deleted inserted replaced
5183:89f162de39cf 5184:9b8547a9496a
    16 Addsimps [option_bind_Some,option_bind_None];
    16 Addsimps [option_bind_Some,option_bind_None];
    17 
    17 
    18 (* expansion of option_bind *)
    18 (* expansion of option_bind *)
    19 Goalw [option_bind_def] "P(option_bind res f) = \
    19 Goalw [option_bind_def] "P(option_bind res f) = \
    20 \         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
    20 \         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
    21 by (rtac split_option_case 1);
    21 by (rtac option.split 1);
    22 qed "split_option_bind";
    22 qed "split_option_bind";
    23 
    23 
    24 Goal
    24 Goal
    25   "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    25   "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    26 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    26 by (simp_tac (simpset() addsplits [split_option_bind]) 1);