2019

1 
(* Title: Option.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1996 TU Muenchen


5 


6 
Derived rules


7 
*)

4133

8 

7030

9 
Goal "(x ~= None) = (? y. x = Some y)";


10 
by (induct_tac "x" 1);


11 
by Auto_tac;


12 
qed "not_None_eq";

5445

13 
AddIffs[not_None_eq];


14 

7030

15 
Goal "(!y. x ~= Some y) = (x = None)";


16 
by (induct_tac "x" 1);


17 
by Auto_tac;


18 
qed "not_Some_eq";

5520

19 
AddIffs[not_Some_eq];


20 

4133

21 


22 
section "case analysis in premises";


23 

7030

24 
val prems = Goal


25 
"[ opt = None ==> P; !!x. opt = Some x ==> P ] ==> P";


26 
by (case_tac "opt = None" 1);


27 
by (eresolve_tac prems 1);


28 
by (dtac (not_None_eq RS iffD1) 1);


29 
by (etac exE 1);


30 
by (eresolve_tac prems 1);


31 
qed "optionE";

4133

32 

7030

33 
val prems = Goal


34 
"[ case x of None => P  Some y => Q y; \


35 
\ [ x = None; P ] ==> R; \


36 
\ !!y. [x = Some y; Q y] ==> R] ==> R";


37 
by (cut_facts_tac prems 1);


38 
by (res_inst_tac [("opt","x")] optionE 1);


39 
by (forward_tac prems 1);


40 
by (forward_tac prems 3);


41 
by Auto_tac;


42 
qed "option_caseE";

4133

43 


44 


45 
section "the";


46 

7030

47 
Goalw [the_def] "the (Some x) = x";


48 
by (Simp_tac 1);


49 
qed "the_Some";


50 

4133

51 
Addsimps [the_Some];


52 


53 

5445

54 

4133

55 
section "option_map";


56 

7030

57 
Goalw [option_map_def] "option_map f None = None";


58 
by (Simp_tac 1);


59 
qed "option_map_None";


60 


61 
Goalw [option_map_def] "option_map f (Some x) = Some (f x)";


62 
by (Simp_tac 1);


63 
qed "option_map_Some";


64 

4133

65 
Addsimps [option_map_None, option_map_Some];


66 

7030

67 
Goalw [option_map_def]


68 
"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)";


69 
by (asm_full_simp_tac (simpset() addsplits [option.split]) 1);


70 
qed "option_map_eq_Some";

4836

71 
AddIffs[option_map_eq_Some];

4752

72 

5445

73 

4752

74 
section "o2s";


75 

7030

76 
Goal "[ !x:o2s A. P x; A = Some x ] ==> P x";


77 
by Auto_tac;


78 
qed "ospec";

5520

79 
AddDs[ospec];

7030

80 

5520

81 
claset_ref() := claset() addSD2 ("ospec", ospec);

5445

82 

5293

83 

7030

84 
Goal "x : o2s xo = (xo = Some x)";

8423

85 
by (cases_tac "xo" 1);

7030

86 
by Auto_tac;


87 
qed "elem_o2s";

5293

88 
AddIffs [elem_o2s];

4752

89 

7030

90 
Goal "(o2s xo = {}) = (xo = None)";

8423

91 
by (cases_tac "xo" 1);

7030

92 
by Auto_tac;


93 
qed "o2s_empty_eq";


94 

4752

95 
Addsimps [o2s_empty_eq];

5293

96 
