isabelle: src/HOL/W0/Maybe.ML@1056cbbaeb29 (annotated)

2520 aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	1	(* Title: HOL/W0/Maybe.ML
aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	2	ID: $Id$
aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	3	Author: Dieter Nazareth and Tobias Nipkow
aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	4	Copyright 1995 TU Muenchen
aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	5	*)
aecaa76e7eff Incorporated Larry's changes. nipkow parents: 2518 diff changeset	6
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	7
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	8	(* constructor laws for bind *)
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4831 diff changeset	9	Goalw [bind_def] "(Ok s) bind f = (f s)";
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	10	by (Simp_tac 1);
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	11	qed "bind_Ok";
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	12
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4831 diff changeset	13	Goalw [bind_def] "Fail bind f = Fail";
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	14	by (Simp_tac 1);
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	15	qed "bind_Fail";
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	16
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	17	Addsimps [bind_Ok,bind_Fail];
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	18
4831 dae4d63a1318 Renamed expand_const -> split_const. nipkow parents: 4089 diff changeset	19	(* case splitting of bind *)
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4831 diff changeset	20	Goal
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	21	"P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
4831 dae4d63a1318 Renamed expand_const -> split_const. nipkow parents: 4089 diff changeset	22	by (induct_tac "res" 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3919 diff changeset	23	by (fast_tac (HOL_cs addss simpset()) 1);
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	24	by (Asm_simp_tac 1);
4831 dae4d63a1318 Renamed expand_const -> split_const. nipkow parents: 4089 diff changeset	25	qed "split_bind";
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	26
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4831 diff changeset	27	Goal
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	28	"((m bind f) = Fail) = ((m=Fail) \| (? p. m = Ok p & f p = Fail))";
4831 dae4d63a1318 Renamed expand_const -> split_const. nipkow parents: 4089 diff changeset	29	by (simp_tac (simpset() addsplits [split_bind]) 1);
2518 bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	30	qed "bind_eq_Fail";
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	31
bee082efaa46 This is the old version og MiniML for the monomorphic case. nipkow parents: diff changeset	32	Addsimps [bind_eq_Fail];

author	oheimb
	Fri, 02 Jun 2000 17:46:32 +0200
changeset 9020	1056cbbaeb29
parent 5069	3ea049f7979d
child 9476	2210dffb9764
permissions	-rw-r--r--