equal
deleted
inserted
replaced
54 definition fun_upds :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" where |
54 definition fun_upds :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" where |
55 "fun_upds f xs y z = (if z \<in> xs then y else f z)" |
55 "fun_upds f xs y z = (if z \<in> xs then y else f z)" |
56 |
56 |
57 syntax |
57 syntax |
58 "_updsbind" :: "['a, 'a] => updbind" ("(2_ [:=]/ _)") |
58 "_updsbind" :: "['a, 'a] => updbind" ("(2_ [:=]/ _)") |
|
59 |
|
60 syntax_consts |
|
61 "_updsbind" == fun_upds |
59 |
62 |
60 translations |
63 translations |
61 "f(xs[:=]y)" == "CONST fun_upds f xs y" |
64 "f(xs[:=]y)" == "CONST fun_upds f xs y" |
62 |
65 |
63 lemma fun_upds_in [simp]: "z \<in> xs \<Longrightarrow> (f(xs [:=] y)) z = y" |
66 lemma fun_upds_in [simp]: "z \<in> xs \<Longrightarrow> (f(xs [:=] y)) z = y" |