src/HOL/Option.ML
author berghofe
Tue May 30 18:02:49 2000 +0200 (2000-05-30)
changeset 9001 93af64f54bf2
parent 8442 96023903c2df
child 9343 1c4754938980
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
     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 
    64 section "o2s";
    65 
    66 Goal "[| !x:o2s A. P x; A = Some x |] ==> P x";
    67 by Auto_tac;
    68 qed "ospec";
    69 AddDs[ospec];
    70 
    71 claset_ref() := claset() addSD2 ("ospec", ospec);
    72 
    73 
    74 Goal "x : o2s xo = (xo = Some x)";
    75 by (case_tac "xo" 1);
    76 by Auto_tac;
    77 qed "elem_o2s";
    78 AddIffs [elem_o2s];
    79 
    80 Goal "(o2s xo = {}) = (xo = None)";
    81 by (case_tac "xo" 1);
    82 by Auto_tac;
    83 qed "o2s_empty_eq";
    84 
    85 Addsimps [o2s_empty_eq];
    86