author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8442  96023903c2df 
child 9343  1c4754938980 
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 

5445  63 

4752  64 
section "o2s"; 
65 

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

68 
qed "ospec"; 

5520  69 
AddDs[ospec]; 
7030  70 

5520  71 
claset_ref() := claset() addSD2 ("ospec", ospec); 
5445  72 

5293  73 

7030  74 
Goal "x : o2s xo = (xo = Some x)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

75 
by (case_tac "xo" 1); 
7030  76 
by Auto_tac; 
77 
qed "elem_o2s"; 

5293  78 
AddIffs [elem_o2s]; 
4752  79 

7030  80 
Goal "(o2s xo = {}) = (xo = None)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

81 
by (case_tac "xo" 1); 
7030  82 
by Auto_tac; 
83 
qed "o2s_empty_eq"; 

84 

4752  85 
Addsimps [o2s_empty_eq]; 
5293  86 