Deleted obsolete proofs. But option_case_tac will be obsolete too
(* 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";