author  oheimb 
Mon, 21 Sep 1998 23:06:37 +0200  
changeset 5520  e2484f1786b7 
parent 5445  3905974ad555 
child 7030  53934985426a 
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 
open Option; 
9 

10 
qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)" 

5183  11 
(K [induct_tac "x" 1, Auto_tac]); 
5445  12 
AddIffs[not_None_eq]; 
13 

5520  14 
qed_goal "not_Some_eq" thy "(!y. x ~= Some y) = (x = None)" 
15 
(K [induct_tac "x" 1, Auto_tac]); 

16 
AddIffs[not_Some_eq]; 

17 

4133  18 

19 
section "case analysis in premises"; 

20 

21 
val optionE = prove_goal thy 

22 
"[ opt = None ==> P; !!x. opt = Some x ==> P ] ==> P" (fn prems => [ 

23 
case_tac "opt = None" 1, 

24 
eresolve_tac prems 1, 

25 
dtac (not_None_eq RS iffD1) 1, 

26 
etac exE 1, 

27 
eresolve_tac prems 1]); 

5293  28 
fun optionE_tac s = res_inst_tac [("opt",s)] optionE THEN_ALL_NEW hyp_subst_tac; 
4133  29 

30 
qed_goal "option_caseE" thy "[case x of None => P  Some y => Q y; \ 

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

32 
\ !!y. [x = Some y; Q y] ==> R] ==> R" (fn prems => [ 

33 
cut_facts_tac prems 1, 

34 
res_inst_tac [("opt","x")] optionE 1, 

35 
forward_tac prems 1, 

36 
forward_tac prems 3, 

4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4133
diff
changeset

37 
Auto_tac]); 
4133  38 
fun option_case_tac i = EVERY [ 
39 
etac option_caseE i, 

40 
hyp_subst_tac (i+1), 

41 
hyp_subst_tac i]; 

42 

43 

44 
section "the"; 

45 

46 
qed_goalw "the_Some" thy [the_def] 

47 
"the (Some x) = x" (K [Simp_tac 1]); 

48 
Addsimps [the_Some]; 

49 

50 

5445  51 

4133  52 
section "option_map"; 
53 

54 
qed_goalw "option_map_None" thy [option_map_def] 

55 
"option_map f None = None" (K [Simp_tac 1]); 

56 
qed_goalw "option_map_Some" thy [option_map_def] 

57 
"option_map f (Some x) = Some (f x)" (K [Simp_tac 1]); 

58 
Addsimps [option_map_None, option_map_Some]; 

59 

4800
97c3a45d092b
replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
oheimb
parents:
4752
diff
changeset

60 
val option_map_eq_Some = prove_goalw thy [option_map_def] 
97c3a45d092b
replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
oheimb
parents:
4752
diff
changeset

61 
"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
5183  62 
(K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]); 
4836  63 
AddIffs[option_map_eq_Some]; 
4752  64 

5445  65 

4752  66 
section "o2s"; 
67 

5293  68 
qed_goal "ospec" thy 
69 
"!!x. [ !x:o2s A. P x; A = Some x ] ==> P x" (K [Auto_tac]); 

5520  70 
AddDs[ospec]; 
71 
claset_ref() := claset() addSD2 ("ospec", ospec); 

5445  72 

5293  73 

4752  74 
val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)" 
4800
97c3a45d092b
replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
oheimb
parents:
4752
diff
changeset

75 
(K [optionE_tac "xo" 1, Auto_tac]); 
5293  76 
AddIffs [elem_o2s]; 
4752  77 

78 
val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)" 

4800
97c3a45d092b
replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
oheimb
parents:
4752
diff
changeset

79 
(K [optionE_tac "xo" 1, Auto_tac]); 
4752  80 
Addsimps [o2s_empty_eq]; 
5293  81 