isabelle: src/HOL/MiniML/Maybe.ML@946efd210837 (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";
1751 946efd210837 Added thm I_complete_wrt_W to I. nipkow parents: 1300 diff changeset	21
946efd210837 Added thm I_complete_wrt_W to I. nipkow parents: 1300 diff changeset	22	goal Maybe.thy "!!x. x = Ok y ==> x ~= Fail";
946efd210837 Added thm I_complete_wrt_W to I. nipkow parents: 1300 diff changeset	23	by(Asm_simp_tac 1);
946efd210837 Added thm I_complete_wrt_W to I. nipkow parents: 1300 diff changeset	24	qed "eq_OkD";

author	nipkow
	Mon, 20 May 1996 18:41:55 +0200
changeset 1751	946efd210837
parent 1300	c7a8f374339b
child 1757	f7a573c46611
permissions	-rw-r--r--