isabelle: src/HOL/MiniML/Maybe.ML@7ec405405dd7 (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 *)
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";

author	wenzelm
	Fri, 12 May 2000 11:52:44 +0200
changeset 8857	7ec405405dd7
parent 5184	9b8547a9496a
permissions	-rw-r--r--