src/HOL/Option.ML
author oheimb
Tue Nov 04 20:48:38 1997 +0100 (1997-11-04)
changeset 4133 0a08c2b9b1ed
parent 4071 4747aefbbc52
child 4477 b3e5857d8d99
permissions -rw-r--r--
added the, option_map, and case analysis theorems
nipkow@2019
     1
(*  Title:      Option.ML
nipkow@2019
     2
    ID:         $Id$
nipkow@2019
     3
    Author:     Tobias Nipkow
nipkow@2019
     4
    Copyright   1996  TU Muenchen
nipkow@2019
     5
nipkow@2019
     6
Derived rules
nipkow@2019
     7
*)
oheimb@4133
     8
open Option;
oheimb@4133
     9
oheimb@4133
    10
qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
oheimb@4133
    11
	(K [option.induct_tac "x" 1, Auto_tac()]);
oheimb@4133
    12
oheimb@4133
    13
section "case analysis in premises";
oheimb@4133
    14
oheimb@4133
    15
val optionE = prove_goal thy 
oheimb@4133
    16
	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" (fn prems => [
oheimb@4133
    17
	case_tac "opt = None" 1,
oheimb@4133
    18
	 eresolve_tac prems 1,
oheimb@4133
    19
	dtac (not_None_eq RS iffD1) 1,
oheimb@4133
    20
	etac exE 1,
oheimb@4133
    21
	eresolve_tac prems 1]);
oheimb@4133
    22
fun optionE_tac s i = EVERY [
oheimb@4133
    23
	res_inst_tac [("opt",s)] optionE i,
oheimb@4133
    24
	 hyp_subst_tac (i+1),
oheimb@4133
    25
	hyp_subst_tac i];
oheimb@4133
    26
oheimb@4133
    27
qed_goal "option_caseE" thy "[|case x of None => P | Some y => Q y; \
oheimb@4133
    28
\                  [|x = None;   P  |] ==> R; \
oheimb@4133
    29
\             !!y. [|x = Some y; Q y|] ==> R|] ==> R" (fn prems => [
oheimb@4133
    30
	cut_facts_tac prems 1,
oheimb@4133
    31
	res_inst_tac [("opt","x")] optionE 1,
oheimb@4133
    32
	 forward_tac prems 1,
oheimb@4133
    33
	  forward_tac prems 3, 
oheimb@4133
    34
	   Auto_tac()]);
oheimb@4133
    35
fun option_case_tac i = EVERY [
oheimb@4133
    36
	etac option_caseE i,
oheimb@4133
    37
	 hyp_subst_tac (i+1),
oheimb@4133
    38
	hyp_subst_tac i];
oheimb@4133
    39
oheimb@4133
    40
oheimb@4133
    41
section "the";
oheimb@4133
    42
oheimb@4133
    43
qed_goalw "the_Some" thy [the_def]
oheimb@4133
    44
	"the (Some x) = x" (K [Simp_tac 1]);
oheimb@4133
    45
Addsimps [the_Some];
oheimb@4133
    46
oheimb@4133
    47
oheimb@4133
    48
section "option_map";
oheimb@4133
    49
oheimb@4133
    50
qed_goalw "option_map_None" thy [option_map_def] 
oheimb@4133
    51
	"option_map f None = None" (K [Simp_tac 1]);
oheimb@4133
    52
qed_goalw "option_map_Some" thy [option_map_def] 
oheimb@4133
    53
	"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]);
oheimb@4133
    54
Addsimps [option_map_None, option_map_Some];
oheimb@4133
    55
oheimb@4133
    56
val option_map_SomeD = prove_goalw thy [option_map_def]
oheimb@4133
    57
	"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
oheimb@4133
    58
	optionE_tac "x" 1,
oheimb@4133
    59
	 Auto_tac()]);