src/HOL/Option.ML
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 2031 03a843f0f447
child 2935 998cb95fdd43
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
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
qed"expand_option_case";