src/HOL/Option.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5520 e2484f1786b7
child 7030 53934985426a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (*  Title:      Option.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996  TU Muenchen
     5 
     6 Derived rules
     7 *)
     8 open Option;
     9 
    10 qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
    11 	(K [induct_tac "x" 1, Auto_tac]);
    12 AddIffs[not_None_eq];
    13 
    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 
    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]);
    28 fun optionE_tac s = res_inst_tac [("opt",s)] optionE THEN_ALL_NEW hyp_subst_tac;
    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, 
    37 	   Auto_tac]);
    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 
    51 
    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 
    60 val option_map_eq_Some = prove_goalw thy [option_map_def]
    61 	"(option_map f xo = Some y) = (? z. xo = Some z & f z = y)" 
    62  (K [asm_full_simp_tac (simpset() addsplits [option.split]) 1]);
    63 AddIffs[option_map_eq_Some];
    64 
    65 
    66 section "o2s";
    67 
    68 qed_goal "ospec" thy 
    69 	"!!x. [| !x:o2s A. P x; A = Some x |] ==> P x" (K [Auto_tac]);
    70 AddDs[ospec];
    71 claset_ref() := claset() addSD2 ("ospec", ospec);
    72 
    73 
    74 val elem_o2s = prove_goal thy "!!X. x : o2s xo = (xo = Some x)"
    75  (K [optionE_tac "xo" 1, Auto_tac]);
    76 AddIffs [elem_o2s];
    77 
    78 val o2s_empty_eq = prove_goal thy "(o2s xo = {}) = (xo = None)"
    79  (K [optionE_tac "xo" 1, Auto_tac]);
    80 Addsimps [o2s_empty_eq];
    81