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);
nipkow@2525
     1
(* Title:     HOL/MiniML/Maybe.ML
nipkow@2525
     2
   ID:        $Id$
nipkow@2525
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
nipkow@2525
     4
   Copyright  1996 TU Muenchen
nipkow@2525
     5
*)
nipkow@1300
     6
nipkow@2525
     7
(* constructor laws for option_bind *)
wenzelm@5069
     8
Goalw [option_bind_def] "option_bind (Some s) f = (f s)";
nipkow@1300
     9
by (Simp_tac 1);
nipkow@2525
    10
qed "option_bind_Some";
nipkow@1300
    11
wenzelm@5069
    12
Goalw [option_bind_def] "option_bind None f = None";
nipkow@2525
    13
by (Simp_tac 1);
nipkow@2525
    14
qed "option_bind_None";
nipkow@1300
    15
nipkow@2525
    16
Addsimps [option_bind_Some,option_bind_None];
nipkow@2525
    17
nipkow@2525
    18
(* expansion of option_bind *)
wenzelm@5069
    19
Goalw [option_bind_def] "P(option_bind res f) = \
nipkow@4072
    20
\         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
berghofe@5184
    21
by (rtac option.split 1);
nipkow@4072
    22
qed "split_option_bind";
nipkow@1751
    23
wenzelm@5069
    24
Goal
nipkow@2525
    25
  "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
wenzelm@4423
    26
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
nipkow@2525
    27
qed "option_bind_eq_None";
nipkow@1757
    28
nipkow@2525
    29
Addsimps [option_bind_eq_None];
narasche@2625
    30
narasche@2625
    31
(* auxiliary lemma *)
wenzelm@5069
    32
Goal "(y = Some x) = (Some x = y)";
wenzelm@4423
    33
by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
narasche@2625
    34
qed "rotate_Some";