2019
|
1 |
(* Title: Option.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1996 TU Muenchen
|
|
5 |
|
|
6 |
Derived rules
|
|
7 |
*)
|
4133
|
8 |
open Option;
|
|
9 |
|
|
10 |
qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
|
|
11 |
(K [option.induct_tac "x" 1, Auto_tac()]);
|
|
12 |
|
|
13 |
section "case analysis in premises";
|
|
14 |
|
|
15 |
val optionE = prove_goal thy
|
|
16 |
"[| opt = None ==> P; !!x. opt = Some x ==> P |] ==> P" (fn prems => [
|
|
17 |
case_tac "opt = None" 1,
|
|
18 |
eresolve_tac prems 1,
|
|
19 |
dtac (not_None_eq RS iffD1) 1,
|
|
20 |
etac exE 1,
|
|
21 |
eresolve_tac prems 1]);
|
|
22 |
fun optionE_tac s i = EVERY [
|
|
23 |
res_inst_tac [("opt",s)] optionE i,
|
|
24 |
hyp_subst_tac (i+1),
|
|
25 |
hyp_subst_tac i];
|
|
26 |
|
|
27 |
qed_goal "option_caseE" thy "[|case x of None => P | Some y => Q y; \
|
|
28 |
\ [|x = None; P |] ==> R; \
|
|
29 |
\ !!y. [|x = Some y; Q y|] ==> R|] ==> R" (fn prems => [
|
|
30 |
cut_facts_tac prems 1,
|
|
31 |
res_inst_tac [("opt","x")] optionE 1,
|
|
32 |
forward_tac prems 1,
|
|
33 |
forward_tac prems 3,
|
|
34 |
Auto_tac()]);
|
|
35 |
fun option_case_tac i = EVERY [
|
|
36 |
etac option_caseE i,
|
|
37 |
hyp_subst_tac (i+1),
|
|
38 |
hyp_subst_tac i];
|
|
39 |
|
|
40 |
|
|
41 |
section "the";
|
|
42 |
|
|
43 |
qed_goalw "the_Some" thy [the_def]
|
|
44 |
"the (Some x) = x" (K [Simp_tac 1]);
|
|
45 |
Addsimps [the_Some];
|
|
46 |
|
|
47 |
|
|
48 |
section "option_map";
|
|
49 |
|
|
50 |
qed_goalw "option_map_None" thy [option_map_def]
|
|
51 |
"option_map f None = None" (K [Simp_tac 1]);
|
|
52 |
qed_goalw "option_map_Some" thy [option_map_def]
|
|
53 |
"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]);
|
|
54 |
Addsimps [option_map_None, option_map_Some];
|
|
55 |
|
|
56 |
val option_map_SomeD = prove_goalw thy [option_map_def]
|
|
57 |
"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
|
|
58 |
optionE_tac "x" 1,
|
|
59 |
Auto_tac()]);
|