author  paulson 
Wed, 24 Dec 1997 10:02:30 +0100  
changeset 4477  b3e5857d8d99 
parent 4133  0a08c2b9b1ed 
child 4752  1c334bd00038 
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)" 

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

11 
(K [option.induct_tac "x" 1, Auto_tac]); 
4133  12 

13 
section "case analysis in premises"; 

14 

15 
val optionE = prove_goal thy 

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

17 
case_tac "opt = None" 1, 

18 
eresolve_tac prems 1, 

19 
dtac (not_None_eq RS iffD1) 1, 

20 
etac exE 1, 

21 
eresolve_tac prems 1]); 

22 
fun optionE_tac s i = EVERY [ 

23 
res_inst_tac [("opt",s)] optionE i, 

24 
hyp_subst_tac (i+1), 

25 
hyp_subst_tac i]; 

26 

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

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

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

30 
cut_facts_tac prems 1, 

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

32 
forward_tac prems 1, 

33 
forward_tac prems 3, 

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

34 
Auto_tac]); 
4133  35 
fun option_case_tac i = EVERY [ 
36 
etac option_caseE i, 

37 
hyp_subst_tac (i+1), 

38 
hyp_subst_tac i]; 

39 

40 

41 
section "the"; 

42 

43 
qed_goalw "the_Some" thy [the_def] 

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

45 
Addsimps [the_Some]; 

46 

47 

48 
section "option_map"; 

49 

50 
qed_goalw "option_map_None" thy [option_map_def] 

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

52 
qed_goalw "option_map_Some" thy [option_map_def] 

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

54 
Addsimps [option_map_None, option_map_Some]; 

55 

56 
val option_map_SomeD = prove_goalw thy [option_map_def] 

57 
"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [ 

58 
optionE_tac "x" 1, 

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

59 
Auto_tac]); 