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

1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	1	open Maybe;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	2
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	3	(* constructor laws for bind *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	4	goalw thy [bind_def] "(Ok s) bind f = (f s)";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	5	by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	6	qed "bind_Ok";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	7
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	8	goalw thy [bind_def] "Fail bind f = Fail";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	9	by (Simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	10	qed "bind_Fail";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	11
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	12	Addsimps [bind_Ok,bind_Fail];
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	13
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	14	(* expansion of bind *)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	15	goal thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	16	"P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	17	by (maybe.induct_tac "res" 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	18	by (fast_tac (HOL_cs addss !simpset) 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	19	by (Asm_simp_tac 1);
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	20	qed "expand_bind";

author	nipkow
	Thu, 22 Feb 1996 18:35:16 +0100
changeset 1519	f999804f11ea
parent 1300	c7a8f374339b
child 1751	946efd210837
permissions	-rw-r--r--