equal
deleted
inserted
replaced
18 (* f x = y ==> f(x:=y) = f *) |
18 (* f x = y ==> f(x:=y) = f *) |
19 bind_thm("update_idem", update_idem_iff RS iffD2); |
19 bind_thm("update_idem", update_idem_iff RS iffD2); |
20 |
20 |
21 AddIffs [refl RS update_idem]; |
21 AddIffs [refl RS update_idem]; |
22 |
22 |
23 Goal "(f(x:=y))z = (if x=z then y else f z)"; |
23 Goal "(f(x:=y))z = (if z=x then y else f z)"; |
24 by (simp_tac (simpset() addsimps [update_def]) 1); |
24 by (simp_tac (simpset() addsimps [update_def]) 1); |
25 qed "update_apply"; |
25 qed "update_apply"; |
26 Addsimps [update_apply]; |
26 Addsimps [update_apply]; |