src/HOL/MiniML/Maybe.ML
changeset 2625 69c1b8a493de
parent 2525 477c05586286
child 3919 c036caebfc75
equal deleted inserted replaced
2624:ab311b6e5e29 2625:69c1b8a493de
    21 by (option.induct_tac "res" 1);
    21 by (option.induct_tac "res" 1);
    22 by (fast_tac (HOL_cs addss !simpset) 1);
    22 by (fast_tac (HOL_cs addss !simpset) 1);
    23 by (Asm_simp_tac 1);
    23 by (Asm_simp_tac 1);
    24 qed "expand_option_bind";
    24 qed "expand_option_bind";
    25 
    25 
    26 goal Maybe.thy
    26 goal thy
    27   "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    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);
    28 by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
    29 qed "option_bind_eq_None";
    29 qed "option_bind_eq_None";
    30 
    30 
    31 Addsimps [option_bind_eq_None];
    31 Addsimps [option_bind_eq_None];
       
    32 
       
    33 (* auxiliary lemma *)
       
    34 goal Maybe.thy "(y = Some x) = (Some x = y)";
       
    35 by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
       
    36 qed "rotate_Some";