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
     1 (*  Title:      Option.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996  TU Muenchen
     5 
     6 Derived rules
     7 *)
     8 
     9 open Option;
    10 
    11 val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
    12  br (prem RS rev_mp) 1;
    13  by (option.induct_tac "opt" 1);
    14  by (ALLGOALS(Fast_tac));
    15 bind_thm("optionE", standard(result() RS disjE));
    16 (*
    17 goal Option.thy "opt=None | (? x.opt=Some(x))"; 
    18 by (option.induct_tac "opt" 1);
    19 by (Simp_tac 1);
    20 by (rtac disjI2 1);
    21 by (rtac exI 1);
    22 by (Asm_full_simp_tac 1);
    23 qed"option_cases";
    24 *)
    25 goal Option.thy "P(case opt of None => a | Some(x) => b(x)) = \
    26 \                ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
    27 by (option.induct_tac "opt" 1);
    28 by (Simp_tac 1);
    29 by (Asm_full_simp_tac 1);
    30 qed"expand_option_case";