src/HOL/Option.ML
author oheimb
Mon Sep 21 23:06:37 1998 +0200 (1998-09-21)
changeset 5520 e2484f1786b7
parent 5445 3905974ad555
child 7030 53934985426a
permissions -rw-r--r--
added addD2, addE2, addSD2, and addSE2
added not_Some_eq, also to simpset() and claset()
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)"
berghofe@5183
    11
	(K [induct_tac "x" 1, Auto_tac]);
oheimb@5445
    12
AddIffs[not_None_eq];
oheimb@5445
    13
oheimb@5520
    14
qed_goal "not_Some_eq" thy "(!y. x ~= Some y) = (x = None)"
oheimb@5520
    15
	(K [induct_tac "x" 1, Auto_tac]);
oheimb@5520
    16
AddIffs[not_Some_eq];
oheimb@5520
    17
oheimb@4133
    18
oheimb@4133
    19
section "case analysis in premises";
oheimb@4133
    20
oheimb@4133
    21
val optionE = prove_goal thy 
oheimb@4133
    22
	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" (fn prems => [
oheimb@4133
    23
	case_tac "opt = None" 1,
oheimb@4133
    24
	 eresolve_tac prems 1,
oheimb@4133
    25
	dtac (not_None_eq RS iffD1) 1,
oheimb@4133
    26
	etac exE 1,
oheimb@4133
    27
	eresolve_tac prems 1]);
oheimb@5293
    28
fun optionE_tac s = res_inst_tac [("opt",s)] optionE THEN_ALL_NEW hyp_subst_tac;
oheimb@4133
    29
oheimb@4133
    30
qed_goal "option_caseE" thy "[|case x of None => P | Some y => Q y; \
oheimb@4133
    31
\                  [|x = None;   P  |] ==> R; \
oheimb@4133
    32
\             !!y. [|x = Some y; Q y|] ==> R|] ==> R" (fn prems => [
oheimb@4133
    33
	cut_facts_tac prems 1,
oheimb@4133
    34
	res_inst_tac [("opt","x")] optionE 1,
oheimb@4133
    35
	 forward_tac prems 1,
oheimb@4133
    36
	  forward_tac prems 3, 
paulson@4477
    37
	   Auto_tac]);
oheimb@4133
    38
fun option_case_tac i = EVERY [
oheimb@4133
    39
	etac option_caseE i,
oheimb@4133
    40
	 hyp_subst_tac (i+1),
oheimb@4133
    41
	hyp_subst_tac i];
oheimb@4133
    42
oheimb@4133
    43
oheimb@4133
    44
section "the";
oheimb@4133
    45
oheimb@4133
    46
qed_goalw "the_Some" thy [the_def]
oheimb@4133
    47
	"the (Some x) = x" (K [Simp_tac 1]);
oheimb@4133
    48
Addsimps [the_Some];
oheimb@4133
    49
oheimb@4133
    50
oheimb@5445
    51
oheimb@4133
    52
section "option_map";
oheimb@4133
    53
oheimb@4133
    54
qed_goalw "option_map_None" thy [option_map_def] 
oheimb@4133
    55
	"option_map f None = None" (K [Simp_tac 1]);
oheimb@4133
    56
qed_goalw "option_map_Some" thy [option_map_def] 
oheimb@4133
    57
	"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]);
oheimb@4133
    58
Addsimps [option_map_None, option_map_Some];
oheimb@4133
    59
oheimb@4800
    60
val option_map_eq_Some = prove_goalw thy [option_map_def]
oheimb@4800
    61
	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
berghofe@5183
    62
 (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
oheimb@4836
    63
AddIffs[option_map_eq_Some];
oheimb@4752
    64
oheimb@5445
    65
oheimb@4752
    66
section "o2s";
oheimb@4752
    67
oheimb@5293
    68
qed_goal "ospec" thy 
oheimb@5293
    69
	"!!x. [| !x:o2s A. P x; A = Some x |] ==> P x" (K [Auto_tac]);
oheimb@5520
    70
AddDs[ospec];
oheimb@5520
    71
claset_ref() := claset() addSD2 ("ospec", ospec);
oheimb@5445
    72
oheimb@5293
    73
oheimb@4752
    74
val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
oheimb@4800
    75
 (K [optionE_tac "xo" 1, Auto_tac]);
oheimb@5293
    76
AddIffs [elem_o2s];
oheimb@4752
    77
oheimb@4752
    78
val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
oheimb@4800
    79
 (K [optionE_tac "xo" 1, Auto_tac]);
oheimb@4752
    80
Addsimps [o2s_empty_eq];
oheimb@5293
    81