src/HOL/Option.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 7030 53934985426a
child 8423 3c19160b6432
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     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 "the";
    46 
    47 Goalw [the_def] "the (Some x) = x";
    48 by (Simp_tac 1);
    49 qed "the_Some";
    50 
    51 Addsimps [the_Some];
    52 
    53 
    54 
    55 section "option_map";
    56 
    57 Goalw [option_map_def] "option_map f None = None";
    58 by (Simp_tac 1);
    59 qed "option_map_None";
    60 
    61 Goalw [option_map_def] "option_map f (Some x) = Some (f x)";
    62 by (Simp_tac 1);
    63 qed "option_map_Some";
    64 
    65 Addsimps [option_map_None, option_map_Some];
    66 
    67 Goalw [option_map_def]
    68     "(option_map f xo = Some y) = (? z. xo = Some z & f z = y)";
    69 by (asm_full_simp_tac (simpset() addsplits [option.split]) 1);
    70 qed "option_map_eq_Some";
    71 AddIffs[option_map_eq_Some];
    72 
    73 
    74 section "o2s";
    75 
    76 Goal "[| !x:o2s A. P x; A = Some x |] ==> P x";
    77 by Auto_tac;
    78 qed "ospec";
    79 AddDs[ospec];
    80 
    81 claset_ref() := claset() addSD2 ("ospec", ospec);
    82 
    83 
    84 Goal "x : o2s xo = (xo = Some x)";
    85 by (exhaust_tac "xo" 1);
    86 by Auto_tac;
    87 qed "elem_o2s";
    88 AddIffs [elem_o2s];
    89 
    90 Goal "(o2s xo = {}) = (xo = None)";
    91 by (exhaust_tac "xo" 1);
    92 by Auto_tac;
    93 qed "o2s_empty_eq";
    94 
    95 Addsimps [o2s_empty_eq];
    96