src/HOL/MiniML/Maybe.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5184 9b8547a9496a
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
     1
(* Title:     HOL/MiniML/Maybe.ML
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
     2
   ID:        $Id$
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
     4
   Copyright  1996 TU Muenchen
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
     5
*)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     6
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
     7
(* constructor laws for option_bind *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4423
diff changeset
     8
Goalw [option_bind_def] "option_bind (Some s) f = (f s)";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     9
by (Simp_tac 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    10
qed "option_bind_Some";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    11
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    12
Goalw [option_bind_def] "option_bind None f = None";
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    13
by (Simp_tac 1);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    14
qed "option_bind_None";
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    15
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    16
Addsimps [option_bind_Some,option_bind_None];
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    17
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    18
(* expansion of option_bind *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    19
Goalw [option_bind_def] "P(option_bind res f) = \
4072
d0d32dd77440 expand_option_bind -> split_option_bind
nipkow
parents: 3919
diff changeset
    20
\         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    21
by (rtac option.split 1);
4072
d0d32dd77440 expand_option_bind -> split_option_bind
nipkow
parents: 3919
diff changeset
    22
qed "split_option_bind";
1751
946efd210837 Added thm I_complete_wrt_W to I.
nipkow
parents: 1300
diff changeset
    23
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    24
Goal
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    25
  "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    26
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    27
qed "option_bind_eq_None";
1757
f7a573c46611 Added the second half of the W/I correspondence.
nipkow
parents: 1751
diff changeset
    28
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 2058
diff changeset
    29
Addsimps [option_bind_eq_None];
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    30
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    31
(* auxiliary lemma *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    32
Goal "(y = Some x) = (Some x = y)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4089
diff changeset
    33
by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
2625
69c1b8a493de Some lemmas changed to valuesd
narasche
parents: 2525
diff changeset
    34
qed "rotate_Some";