src/HOL/Option.ML
author paulson
Thu, 22 May 1997 15:09:09 +0200
changeset 3295 c9c99aa082fb
parent 2935 998cb95fdd43
child 3344 b3e39a2987c1
permissions -rw-r--r--
Deleted obsolete proofs. But option_case_tac will be obsolete too
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
3295
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    11
val opt_exhaustion = #nchotomy (the (datatype_info Option.thy "option")) 
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    12
                     RS spec;
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    13
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    14
(*---------------------------------------------------------------------------
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    15
 * Do a case analysis on something of type 'a option. 
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    16
 *---------------------------------------------------------------------------*)
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    17
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    18
fun option_case_tac t =
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    19
    (cut_inst_tac [("x",t)] opt_exhaustion 
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    20
      THEN' etac disjE 
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    21
      THEN' rotate_tac ~1 
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    22
      THEN' Asm_full_simp_tac 
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    23
      THEN' etac exE
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    24
      THEN' rotate_tac ~1 
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    25
      THEN' Asm_full_simp_tac);
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    26
c9c99aa082fb Deleted obsolete proofs. But option_case_tac will be obsolete too
paulson
parents: 2935
diff changeset
    27
2019
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    28
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
    29
\                ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    30
by (option.induct_tac "opt" 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    31
by (Simp_tac 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    32
by (Asm_full_simp_tac 1);
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
    33
qed"expand_option_case";