isabelle: src/HOL/Option.ML@2a726de6e124 (annotated)

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

author	wenzelm
	Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220	2a726de6e124
parent 9343	1c4754938980
child 11655	923e4d0d36d5
permissions	-rw-r--r--