src/HOL/MiniML/Maybe.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5184 9b8547a9496a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 [option_bind_def] "option_bind (Some s) f = (f s)";
     9 by (Simp_tac 1);
    10 qed "option_bind_Some";
    11 
    12 Goalw [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 Goalw [option_bind_def] "P(option_bind res f) = \
    20 \         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
    21 by (rtac option.split 1);
    22 qed "split_option_bind";
    23 
    24 Goal
    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);
    27 qed "option_bind_eq_None";
    28 
    29 Addsimps [option_bind_eq_None];
    30 
    31 (* auxiliary lemma *)
    32 Goal "(y = Some x) = (Some x = y)";
    33 by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    34 qed "rotate_Some";