src/HOL/Option.ML
author wenzelm
Mon, 13 Mar 2000 16:23:34 +0100
changeset 8442 96023903c2df
parent 8423 3c19160b6432
child 9001 93af64f54bf2
permissions -rw-r--r--
case_tac now subsumes both boolean and datatype cases;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2019
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     1
(*  Title:      Option.ML
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     2
    ID:         $Id$
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     4
    Copyright   1996  TU Muenchen
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     5
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     6
Derived rules
b45d9f2042e0 Moved Option out of IOA into core HOL
nipkow
parents:
diff changeset
     7
*)
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
     8
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
     9
Goal "(x ~= None) = (? y. x = Some y)";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    10
by (induct_tac "x" 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    11
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    12
qed "not_None_eq";
5445
3905974ad555 AddIffs[not_None_eq];
oheimb
parents: 5293
diff changeset
    13
AddIffs[not_None_eq];
3905974ad555 AddIffs[not_None_eq];
oheimb
parents: 5293
diff changeset
    14
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    15
Goal "(!y. x ~= Some y) = (x = None)";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    16
by (induct_tac "x" 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    17
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    18
qed "not_Some_eq";
5520
e2484f1786b7 added addD2, addE2, addSD2, and addSE2
oheimb
parents: 5445
diff changeset
    19
AddIffs[not_Some_eq];
e2484f1786b7 added addD2, addE2, addSD2, and addSE2
oheimb
parents: 5445
diff changeset
    20
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    21
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    22
section "case analysis in premises";
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    23
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    24
val prems = Goal
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    25
	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    26
by (case_tac "opt = None" 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    27
by (eresolve_tac prems 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    28
by (dtac (not_None_eq RS iffD1) 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    29
by (etac exE 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    30
by (eresolve_tac prems 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    31
qed "optionE";
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    32
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    33
val prems = Goal
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    34
     "[| case x of None => P | Some y => Q y; \
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    35
\        [| x = None;   P  |] ==> R; \
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    36
\        !!y. [|x = Some y; Q y|] ==> R|] ==> R";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    37
by (cut_facts_tac prems 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    38
by (res_inst_tac [("opt","x")] optionE 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    39
by (forward_tac prems 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    40
by (forward_tac prems 3);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    41
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    42
qed "option_caseE";
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    43
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    44
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    45
section "the";
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    46
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    47
Goalw [the_def] "the (Some x) = x";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    48
by (Simp_tac 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    49
qed "the_Some";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    50
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    51
Addsimps [the_Some];
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    52
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    53
5445
3905974ad555 AddIffs[not_None_eq];
oheimb
parents: 5293
diff changeset
    54
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    55
section "option_map";
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    56
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    57
Goalw [option_map_def] "option_map f None = None";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    58
by (Simp_tac 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    59
qed "option_map_None";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    60
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    61
Goalw [option_map_def] "option_map f (Some x) = Some (f x)";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    62
by (Simp_tac 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    63
qed "option_map_Some";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    64
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    65
Addsimps [option_map_None, option_map_Some];
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    66
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    67
Goalw [option_map_def]
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    68
    "(option_map f xo = Some y) = (? z. xo = Some z & f z = y)";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    69
by (asm_full_simp_tac (simpset() addsplits [option.split]) 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    70
qed "option_map_eq_Some";
4836
fc5773ae2790 added option_map_eq_Some via AddIffs
oheimb
parents: 4800
diff changeset
    71
AddIffs[option_map_eq_Some];
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    72
5445
3905974ad555 AddIffs[not_None_eq];
oheimb
parents: 5293
diff changeset
    73
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    74
section "o2s";
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    75
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    76
Goal "[| !x:o2s A. P x; A = Some x |] ==> P x";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    77
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    78
qed "ospec";
5520
e2484f1786b7 added addD2, addE2, addSD2, and addSE2
oheimb
parents: 5445
diff changeset
    79
AddDs[ospec];
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    80
5520
e2484f1786b7 added addD2, addE2, addSD2, and addSE2
oheimb
parents: 5445
diff changeset
    81
claset_ref() := claset() addSD2 ("ospec", ospec);
5445
3905974ad555 AddIffs[not_None_eq];
oheimb
parents: 5293
diff changeset
    82
5293
4ce5539aa969 added ospec
oheimb
parents: 5183
diff changeset
    83
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    84
Goal "x : o2s xo = (xo = Some x)";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    85
by (case_tac "xo" 1);
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    86
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    87
qed "elem_o2s";
5293
4ce5539aa969 added ospec
oheimb
parents: 5183
diff changeset
    88
AddIffs [elem_o2s];
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    89
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    90
Goal "(o2s xo = {}) = (xo = None)";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    91
by (case_tac "xo" 1);
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    92
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    93
qed "o2s_empty_eq";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    94
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    95
Addsimps [o2s_empty_eq];
5293
4ce5539aa969 added ospec
oheimb
parents: 5183
diff changeset
    96