src/HOL/Option.ML
author paulson
Mon, 07 Oct 1996 10:28:44 +0200
changeset 2056 93c093620c28
parent 2031 03a843f0f447
child 2935 998cb95fdd43
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2019
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     1
(*  Title:      Option.ML
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     2
    ID:         $Id$
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     4
    Copyright   1996  TU Muenchen
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     5
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     6
Derived rules
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     7
*)
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     8
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     9
open Option;
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    10
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    11
val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    12
 br (prem RS rev_mp) 1;
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    13
 by (option.induct_tac "opt" 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    14
 by (ALLGOALS(Fast_tac));
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    15
bind_thm("optionE", standard(result() RS disjE));
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    16
(*
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    17
goal Option.thy "opt=None | (? x.opt=Some(x))"; 
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    18
by (option.induct_tac "opt" 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    19
by (Simp_tac 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    20
by (rtac disjI2 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    21
by (rtac exI 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    22
by (Asm_full_simp_tac 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    23
qed"option_cases";
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    24
*)
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    25
goal Option.thy "P(case opt of None => a | Some(x) => b(x)) = \
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    26
\                ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    27
by (option.induct_tac "opt" 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    28
by (Simp_tac 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    29
by (Asm_full_simp_tac 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    30
qed"expand_option_case";