src/HOL/Option.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9343 1c4754938980
child 11655 923e4d0d36d5
permissions -rw-r--r--
improved theory reference in comment
     1 (*  Title:      Option.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996  TU Muenchen
     5 
     6 Derived rules
     7 *)
     8 
     9 Goal "(x ~= None) = (? y. x = Some y)";
    10 by (induct_tac "x" 1);
    11 by Auto_tac;
    12 qed "not_None_eq";
    13 AddIffs[not_None_eq];
    14 
    15 Goal "(!y. x ~= Some y) = (x = None)";
    16 by (induct_tac "x" 1);
    17 by Auto_tac;
    18 qed "not_Some_eq";
    19 AddIffs[not_Some_eq];
    20 
    21 
    22 section "case analysis in premises";
    23 
    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";
    32 
    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";
    43 
    44 
    45 section "option_map";
    46 
    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 
    55 Addsimps [option_map_None, option_map_Some];
    56 
    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";
    61 AddIffs[option_map_eq_Some];
    62 
    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 
    70 
    71 section "o2s";
    72 
    73 Goal "[| !x:o2s A. P x; A = Some x |] ==> P x";
    74 by Auto_tac;
    75 qed "ospec";
    76 AddDs[ospec];
    77 
    78 claset_ref() := claset() addSD2 ("ospec", ospec);
    79 
    80 
    81 Goal "x : o2s xo = (xo = Some x)";
    82 by (case_tac "xo" 1);
    83 by Auto_tac;
    84 qed "elem_o2s";
    85 AddIffs [elem_o2s];
    86 
    87 Goal "(o2s xo = {}) = (xo = None)";
    88 by (case_tac "xo" 1);
    89 by Auto_tac;
    90 qed "o2s_empty_eq";
    91 
    92 Addsimps [o2s_empty_eq];
    93