author  wenzelm 
Mon, 13 Mar 2000 16:23:34 +0100  
changeset 8442  96023903c2df 
parent 8423  3c19160b6432 
child 9001  93af64f54bf2 
permissions  rwrr 
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)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

85 
by (case_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)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

91 
by (case_tac "xo" 1); 
7030  92 
by Auto_tac; 
93 
qed "o2s_empty_eq"; 

94 

4752  95 
Addsimps [o2s_empty_eq]; 
5293  96 