isabelle: src/HOL/MiniML/Maybe.ML@a129b817b58a (annotated)

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 *)
477c05586286 The new version of MiniML including "let". nipkow parents: 2058 diff changeset	8	goalw thy [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
2525 477c05586286 The new version of MiniML including "let". nipkow parents: 2058 diff changeset	12	goalw thy [option_bind_def] "option_bind None f = None";
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 *)
4072 d0d32dd77440 expand_option_bind -> split_option_bind nipkow parents: 3919 diff changeset	19	goalw thy [option_bind_def] "P(option_bind res f) = \
d0d32dd77440 expand_option_bind -> split_option_bind nipkow parents: 3919 diff changeset	20	\ ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
4423 a129b817b58a expandshort; wenzelm parents: 4089 diff changeset	21	by (rtac split_option_case 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
2625 69c1b8a493de Some lemmas changed to valuesd narasche parents: 2525 diff changeset	24	goal thy
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 *)
69c1b8a493de Some lemmas changed to valuesd narasche parents: 2525 diff changeset	32	goal Maybe.thy "(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";

author	wenzelm
	Tue, 16 Dec 1997 17:58:03 +0100
changeset 4423	a129b817b58a
parent 4089	96fba19bcbe2
child 5069	3ea049f7979d
permissions	-rw-r--r--