src/HOL/Option.ML

New operator "lists" for formalizing sets of lists

(*  Title:      Option.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1996  TU Muenchen

Derived rules
*)

open Option;

val opt_exhaustion = #nchotomy (the (datatype_info Option.thy "option")) 
                     RS spec;

(*---------------------------------------------------------------------------
 * Do a case analysis on something of type 'a option. 
 *---------------------------------------------------------------------------*)

fun option_case_tac t =
    (cut_inst_tac [("x",t)] opt_exhaustion 
      THEN' etac disjE 
      THEN' rotate_tac ~1 
      THEN' Asm_full_simp_tac 
      THEN' etac exE
      THEN' rotate_tac ~1 
      THEN' Asm_full_simp_tac);


goal Option.thy "P(case opt of None => a | Some(x) => b(x)) = \
\                ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
by (option.induct_tac "opt" 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
qed"expand_option_case";