equal
deleted
inserted
replaced
17 by (maybe.induct_tac "res" 1); |
17 by (maybe.induct_tac "res" 1); |
18 by (fast_tac (HOL_cs addss !simpset) 1); |
18 by (fast_tac (HOL_cs addss !simpset) 1); |
19 by (Asm_simp_tac 1); |
19 by (Asm_simp_tac 1); |
20 qed "expand_bind"; |
20 qed "expand_bind"; |
21 |
21 |
22 goal Maybe.thy "!!x. x = Ok y ==> x ~= Fail"; |
22 goal Maybe.thy |
23 by(Asm_simp_tac 1); |
23 "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; |
24 qed "eq_OkD"; |
24 by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
|
25 by(fast_tac HOL_cs 1); |
|
26 qed "bind_eq_Fail"; |
|
27 |
|
28 Addsimps [bind_eq_Fail]; |