author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9343  1c4754938980 
child 11655  923e4d0d36d5 
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 "option_map"; 

46 

7030  47 
Goalw [option_map_def] "option_map f None = None"; 
48 
by (Simp_tac 1); 

49 
qed "option_map_None"; 

50 

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

52 
by (Simp_tac 1); 

53 
qed "option_map_Some"; 

54 

4133  55 
Addsimps [option_map_None, option_map_Some]; 
56 

7030  57 
Goalw [option_map_def] 
58 
"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)"; 

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

60 
qed "option_map_eq_Some"; 

4836  61 
AddIffs[option_map_eq_Some]; 
4752  62 

9343  63 
Goal 
64 
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"; 

65 
by (rtac ext 1); 

66 
by (simp_tac (simpset() addsplits [sum.split]) 1); 

67 
qed "option_map_o_sum_case"; 

68 
Addsimps [option_map_o_sum_case]; 

69 

5445  70 

4752  71 
section "o2s"; 
72 

7030  73 
Goal "[ !x:o2s A. P x; A = Some x ] ==> P x"; 
74 
by Auto_tac; 

75 
qed "ospec"; 

5520  76 
AddDs[ospec]; 
7030  77 

5520  78 
claset_ref() := claset() addSD2 ("ospec", ospec); 
5445  79 

5293  80 

7030  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  83 
by Auto_tac; 
84 
qed "elem_o2s"; 

5293  85 
AddIffs [elem_o2s]; 
4752  86 

7030  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  89 
by Auto_tac; 
90 
qed "o2s_empty_eq"; 

91 

4752  92 
Addsimps [o2s_empty_eq]; 
5293  93 