isabelle: src/HOL/MiniML/Maybe.ML@03a843f0f447 (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
1757 f7a573c46611 Added the second half of the W/I correspondence. nipkow parents: 1751 diff changeset	22	goal Maybe.thy
f7a573c46611 Added the second half of the W/I correspondence. nipkow parents: 1751 diff changeset	23	"((m bind f) = Fail) = ((m=Fail) \| (? p. m = Ok p & f p = Fail))";
2031 03a843f0f447 Ran expandshort paulson parents: 1757 diff changeset	24	by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
03a843f0f447 Ran expandshort paulson parents: 1757 diff changeset	25	by (fast_tac HOL_cs 1);
1757 f7a573c46611 Added the second half of the W/I correspondence. nipkow parents: 1751 diff changeset	26	qed "bind_eq_Fail";
f7a573c46611 Added the second half of the W/I correspondence. nipkow parents: 1751 diff changeset	27
f7a573c46611 Added the second half of the W/I correspondence. nipkow parents: 1751 diff changeset	28	Addsimps [bind_eq_Fail];

author	paulson
	Thu, 26 Sep 1996 12:47:47 +0200
changeset 2031	03a843f0f447
parent 1757	f7a573c46611
child 2058	ff04984186e9
permissions	-rw-r--r--