src/HOL/Option.ML
author berghofe
Fri, 24 Jul 1998 13:03:20 +0200
changeset 5183 89f162de39cf
parent 4836 fc5773ae2790
child 5293 4ce5539aa969
permissions -rw-r--r--
Adapted to new datatype package.
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
open Option;
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
     9
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    10
qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 4836
diff changeset
    11
	(K [induct_tac "x" 1, Auto_tac]);
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    12
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    13
section "case analysis in premises";
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    14
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    15
val optionE = prove_goal thy 
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    16
	"[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" (fn prems => [
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    17
	case_tac "opt = None" 1,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    18
	 eresolve_tac prems 1,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    19
	dtac (not_None_eq RS iffD1) 1,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    20
	etac exE 1,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    21
	eresolve_tac prems 1]);
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    22
fun optionE_tac s i = EVERY [
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    23
	res_inst_tac [("opt",s)] optionE i,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    24
	 hyp_subst_tac (i+1),
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    25
	hyp_subst_tac i];
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    26
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    27
qed_goal "option_caseE" thy "[|case x of None => P | Some y => Q y; \
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    28
\                  [|x = None;   P  |] ==> R; \
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    29
\             !!y. [|x = Some y; Q y|] ==> R|] ==> R" (fn prems => [
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    30
	cut_facts_tac prems 1,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    31
	res_inst_tac [("opt","x")] optionE 1,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    32
	 forward_tac prems 1,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    33
	  forward_tac prems 3, 
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4133
diff changeset
    34
	   Auto_tac]);
4133
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    35
fun option_case_tac i = EVERY [
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    36
	etac option_caseE i,
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    37
	 hyp_subst_tac (i+1),
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    38
	hyp_subst_tac i];
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    39
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    40
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    41
section "the";
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    42
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    43
qed_goalw "the_Some" thy [the_def]
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    44
	"the (Some x) = x" (K [Simp_tac 1]);
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    45
Addsimps [the_Some];
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    46
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    47
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    48
section "option_map";
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    49
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    50
qed_goalw "option_map_None" thy [option_map_def] 
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    51
	"option_map f None = None" (K [Simp_tac 1]);
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    52
qed_goalw "option_map_Some" thy [option_map_def] 
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    53
	"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]);
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    54
Addsimps [option_map_None, option_map_Some];
0a08c2b9b1ed added the, option_map, and case analysis theorems
oheimb
parents: 4071
diff changeset
    55
4800
97c3a45d092b replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
oheimb
parents: 4752
diff changeset
    56
val option_map_eq_Some = prove_goalw thy [option_map_def]
97c3a45d092b replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
oheimb
parents: 4752
diff changeset
    57
	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 4836
diff changeset
    58
 (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
4836
fc5773ae2790 added option_map_eq_Some via AddIffs
oheimb
parents: 4800
diff changeset
    59
AddIffs[option_map_eq_Some];
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    60
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    61
section "o2s";
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    62
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    63
val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
4800
97c3a45d092b replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
oheimb
parents: 4752
diff changeset
    64
 (K [optionE_tac "xo" 1, Auto_tac]);
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    65
AddSDs [elem_o2s RS iffD1];
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    66
Addsimps [elem_o2s];
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    67
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    68
val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
4800
97c3a45d092b replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
oheimb
parents: 4752
diff changeset
    69
 (K [optionE_tac "xo" 1, Auto_tac]);
4752
1c334bd00038 added o2s
oheimb
parents: 4477
diff changeset
    70
Addsimps [o2s_empty_eq];