src/HOL/Option.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9343 1c4754938980
child 11655 923e4d0d36d5
permissions -rw-r--r--
improved theory reference in comment
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
paulson@7030
     9
Goal "(x ~= None) = (? y. x = Some y)";
paulson@7030
    10
by (induct_tac "x" 1);
paulson@7030
    11
by Auto_tac;
paulson@7030
    12
qed "not_None_eq";
oheimb@5445
    13
AddIffs[not_None_eq];
oheimb@5445
    14
paulson@7030
    15
Goal "(!y. x ~= Some y) = (x = None)";
paulson@7030
    16
by (induct_tac "x" 1);
paulson@7030
    17
by Auto_tac;
paulson@7030
    18
qed "not_Some_eq";
oheimb@5520
    19
AddIffs[not_Some_eq];
oheimb@5520
    20
oheimb@4133
    21
oheimb@4133
    22
section "case analysis in premises";
oheimb@4133
    23
paulson@7030
    24
val prems = Goal
paulson@7030
    25
	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P";
paulson@7030
    26
by (case_tac "opt = None" 1);
paulson@7030
    27
by (eresolve_tac prems 1);
paulson@7030
    28
by (dtac (not_None_eq RS iffD1) 1);
paulson@7030
    29
by (etac exE 1);
paulson@7030
    30
by (eresolve_tac prems 1);
paulson@7030
    31
qed "optionE";
oheimb@4133
    32
paulson@7030
    33
val prems = Goal
paulson@7030
    34
     "[| case x of None => P | Some y => Q y; \
paulson@7030
    35
\        [| x = None;   P  |] ==> R; \
paulson@7030
    36
\        !!y. [|x = Some y; Q y|] ==> R|] ==> R";
paulson@7030
    37
by (cut_facts_tac prems 1);
paulson@7030
    38
by (res_inst_tac [("opt","x")] optionE 1);
paulson@7030
    39
by (forward_tac prems 1);
paulson@7030
    40
by (forward_tac prems 3);
paulson@7030
    41
by Auto_tac;
paulson@7030
    42
qed "option_caseE";
oheimb@4133
    43
oheimb@4133
    44
oheimb@4133
    45
section "option_map";
oheimb@4133
    46
paulson@7030
    47
Goalw [option_map_def] "option_map f None = None";
paulson@7030
    48
by (Simp_tac 1);
paulson@7030
    49
qed "option_map_None";
paulson@7030
    50
paulson@7030
    51
Goalw [option_map_def] "option_map f (Some x) = Some (f x)";
paulson@7030
    52
by (Simp_tac 1);
paulson@7030
    53
qed "option_map_Some";
paulson@7030
    54
oheimb@4133
    55
Addsimps [option_map_None, option_map_Some];
oheimb@4133
    56
paulson@7030
    57
Goalw [option_map_def]
paulson@7030
    58
    "(option_map f xo = Some y) = (? z. xo = Some z & f z = y)";
paulson@7030
    59
by (asm_full_simp_tac (simpset() addsplits [option.split]) 1);
paulson@7030
    60
qed "option_map_eq_Some";
oheimb@4836
    61
AddIffs[option_map_eq_Some];
oheimb@4752
    62
oheimb@9343
    63
Goal 
oheimb@9343
    64
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)";
oheimb@9343
    65
by (rtac ext 1);
oheimb@9343
    66
by (simp_tac (simpset() addsplits [sum.split]) 1);
oheimb@9343
    67
qed "option_map_o_sum_case";
oheimb@9343
    68
Addsimps [option_map_o_sum_case];
oheimb@9343
    69
oheimb@5445
    70
oheimb@4752
    71
section "o2s";
oheimb@4752
    72
paulson@7030
    73
Goal "[| !x:o2s A. P x; A = Some x |] ==> P x";
paulson@7030
    74
by Auto_tac;
paulson@7030
    75
qed "ospec";
oheimb@5520
    76
AddDs[ospec];
paulson@7030
    77
oheimb@5520
    78
claset_ref() := claset() addSD2 ("ospec", ospec);
oheimb@5445
    79
oheimb@5293
    80
paulson@7030
    81
Goal "x : o2s xo = (xo = Some x)";
wenzelm@8442
    82
by (case_tac "xo" 1);
paulson@7030
    83
by Auto_tac;
paulson@7030
    84
qed "elem_o2s";
oheimb@5293
    85
AddIffs [elem_o2s];
oheimb@4752
    86
paulson@7030
    87
Goal "(o2s xo = {}) = (xo = None)";
wenzelm@8442
    88
by (case_tac "xo" 1);
paulson@7030
    89
by Auto_tac;
paulson@7030
    90
qed "o2s_empty_eq";
paulson@7030
    91
oheimb@4752
    92
Addsimps [o2s_empty_eq];
oheimb@5293
    93