446 "update(f,a,b) \<equiv> \<lambda>x\<in>cons(a, domain(f)). if(x=a, b, f`x)" |
446 "update(f,a,b) \<equiv> \<lambda>x\<in>cons(a, domain(f)). if(x=a, b, f`x)" |
447 |
447 |
448 nonterminal updbinds and updbind |
448 nonterminal updbinds and updbind |
449 |
449 |
450 syntax |
450 syntax |
451 |
|
452 (* Let expressions *) |
|
453 |
|
454 "_updbind" :: "[i, i] \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>) |
451 "_updbind" :: "[i, i] \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>) |
455 "" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>) |
452 "" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>) |
456 "_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>) |
453 "_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>) |
457 "_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900) |
454 "_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900) |
458 |
|
459 translations |
455 translations |
460 "_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)" |
456 "_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)" |
461 "f(x:=y)" == "CONST update(f,x,y)" |
457 "f(x:=y)" == "CONST update(f,x,y)" |
462 |
458 syntax_consts "_Update" "_updbind" \<rightleftharpoons> update |
463 |
459 |
464 lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)" |
460 lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)" |
465 apply (simp add: update_def) |
461 apply (simp add: update_def) |
466 apply (case_tac "z \<in> domain(f)") |
462 apply (case_tac "z \<in> domain(f)") |
467 apply (simp_all add: apply_0) |
463 apply (simp_all add: apply_0) |