src/HOL/Option.ML
author berghofe
Tue May 30 18:02:49 2000 +0200 (2000-05-30)
changeset 9001 93af64f54bf2
parent 8442 96023903c2df
child 9343 1c4754938980
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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@5445
    63
oheimb@4752
    64
section "o2s";
oheimb@4752
    65
paulson@7030
    66
Goal "[| !x:o2s A. P x; A = Some x |] ==> P x";
paulson@7030
    67
by Auto_tac;
paulson@7030
    68
qed "ospec";
oheimb@5520
    69
AddDs[ospec];
paulson@7030
    70
oheimb@5520
    71
claset_ref() := claset() addSD2 ("ospec", ospec);
oheimb@5445
    72
oheimb@5293
    73
paulson@7030
    74
Goal "x : o2s xo = (xo = Some x)";
wenzelm@8442
    75
by (case_tac "xo" 1);
paulson@7030
    76
by Auto_tac;
paulson@7030
    77
qed "elem_o2s";
oheimb@5293
    78
AddIffs [elem_o2s];
oheimb@4752
    79
paulson@7030
    80
Goal "(o2s xo = {}) = (xo = None)";
wenzelm@8442
    81
by (case_tac "xo" 1);
paulson@7030
    82
by Auto_tac;
paulson@7030
    83
qed "o2s_empty_eq";
paulson@7030
    84
oheimb@4752
    85
Addsimps [o2s_empty_eq];
oheimb@5293
    86