src/HOL/Option.ML
author nipkow
Tue Sep 24 09:02:34 1996 +0200 (1996-09-24)
changeset 2019 b45d9f2042e0
child 2031 03a843f0f447
permissions -rw-r--r--
Moved Option out of IOA into core HOL
nipkow@2019
     1
(*  Title:      Option.ML
nipkow@2019
     2
    ID:         $Id$
nipkow@2019
     3
    Author:     Tobias Nipkow
nipkow@2019
     4
    Copyright   1996  TU Muenchen
nipkow@2019
     5
nipkow@2019
     6
Derived rules
nipkow@2019
     7
*)
nipkow@2019
     8
nipkow@2019
     9
open Option;
nipkow@2019
    10
nipkow@2019
    11
val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
nipkow@2019
    12
 br (prem RS rev_mp) 1;
nipkow@2019
    13
 by (option.induct_tac "opt" 1);
nipkow@2019
    14
 by (ALLGOALS(Fast_tac));
nipkow@2019
    15
bind_thm("optionE", standard(result() RS disjE));
nipkow@2019
    16
(*
nipkow@2019
    17
goal Option.thy "opt=None | (? x.opt=Some(x))"; 
nipkow@2019
    18
by (option.induct_tac "opt" 1);
nipkow@2019
    19
by (Simp_tac 1);
nipkow@2019
    20
by (rtac disjI2 1);
nipkow@2019
    21
by (rtac exI 1);
nipkow@2019
    22
by (Asm_full_simp_tac 1);
nipkow@2019
    23
qed"option_cases";
nipkow@2019
    24
*)
nipkow@2019
    25
goal Option.thy "P(case opt of None => a | Some(x) => b(x)) = \
nipkow@2019
    26
\                ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
nipkow@2019
    27
by (option.induct_tac "opt" 1);
nipkow@2019
    28
by (Simp_tac 1);
nipkow@2019
    29
by (Asm_full_simp_tac 1);
nipkow@2019
    30
by(Fast_tac 1);
nipkow@2019
    31
qed"expand_option_case";