src/HOL/Option.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9343 1c4754938980
child 11655 923e4d0d36d5
permissions -rw-r--r--
hide many names from Datatype_Universe.
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 "option_map";
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 [option_map_def] "option_map f None = None";
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 "option_map_None";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    50
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    51
Goalw [option_map_def] "option_map f (Some x) = Some (f x)";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    52
by (Simp_tac 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    53
qed "option_map_Some";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    54
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    55
Addsimps [option_map_None, option_map_Some];
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]
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    58
    "(option_map f xo = Some y) = (? z. xo = Some z & f z = y)";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    59
by (asm_full_simp_tac (simpset() addsplits [option.split]) 1);
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    60
qed "option_map_eq_Some";
4836
fc5773ae2790 added option_map_eq_Some via AddIffs
oheimb
parents: 4800
diff changeset
    61
AddIffs[option_map_eq_Some];
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    62
9343
1c4754938980 added option_map_o_sum_case (also to simpset)
oheimb
parents: 9001
diff changeset
    63
Goal 
1c4754938980 added option_map_o_sum_case (also to simpset)
oheimb
parents: 9001
diff changeset
    64
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)";
1c4754938980 added option_map_o_sum_case (also to simpset)
oheimb
parents: 9001
diff changeset
    65
by (rtac ext 1);
1c4754938980 added option_map_o_sum_case (also to simpset)
oheimb
parents: 9001
diff changeset
    66
by (simp_tac (simpset() addsplits [sum.split]) 1);
1c4754938980 added option_map_o_sum_case (also to simpset)
oheimb
parents: 9001
diff changeset
    67
qed "option_map_o_sum_case";
1c4754938980 added option_map_o_sum_case (also to simpset)
oheimb
parents: 9001
diff changeset
    68
Addsimps [option_map_o_sum_case];
1c4754938980 added option_map_o_sum_case (also to simpset)
oheimb
parents: 9001
diff changeset
    69
5445
3905974ad555 AddIffs[not_None_eq];
oheimb
parents: 5293
diff changeset
    70
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    71
section "o2s";
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    72
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    73
Goal "[| !x:o2s A. P x; A = Some x |] ==> P x";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    74
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    75
qed "ospec";
5520
e2484f1786b7 added addD2, addE2, addSD2, and addSE2
oheimb
parents: 5445
diff changeset
    76
AddDs[ospec];
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    77
5520
e2484f1786b7 added addD2, addE2, addSD2, and addSE2
oheimb
parents: 5445
diff changeset
    78
claset_ref() := claset() addSD2 ("ospec", ospec);
5445
3905974ad555 AddIffs[not_None_eq];
oheimb
parents: 5293
diff changeset
    79
5293
4ce5539aa969 added ospec
oheimb
parents: 5183
diff changeset
    80
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    81
Goal "x : o2s xo = (xo = Some x)";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    82
by (case_tac "xo" 1);
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    83
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    84
qed "elem_o2s";
5293
4ce5539aa969 added ospec
oheimb
parents: 5183
diff changeset
    85
AddIffs [elem_o2s];
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    86
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    87
Goal "(o2s xo = {}) = (xo = None)";
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    88
by (case_tac "xo" 1);
7030
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    89
by Auto_tac;
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    90
qed "o2s_empty_eq";
53934985426a getting rid of qed_goal
paulson
parents: 5520
diff changeset
    91
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    92
Addsimps [o2s_empty_eq];
5293
4ce5539aa969 added ospec
oheimb
parents: 5183
diff changeset
    93