src/HOL/Fun.thy
changeset 13910 f9a9ef16466f
parent 13637 02aa63636ab8
child 14565 c6dc17aab88a
     1.1 --- a/src/HOL/Fun.thy	Mon Apr 14 13:51:31 2003 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Apr 14 18:52:13 2003 +0200
     1.3 @@ -37,11 +37,15 @@
     1.4  *)
     1.5  
     1.6  constdefs
     1.7 -  id :: "'a => 'a"
     1.8 -    "id == %x. x"
     1.9 + overwrite :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
    1.10 +              ("_/'(_|/_')"  [900,0,0]900)
    1.11 +"f(g|A) == %a. if a : A then g a else f a"
    1.12  
    1.13 -  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
    1.14 -    "f o g == %x. f(g(x))"
    1.15 + id :: "'a => 'a"
    1.16 +"id == %x. x"
    1.17 +
    1.18 + comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
    1.19 +"f o g == %x. f(g(x))"
    1.20  
    1.21  text{*compatibility*}
    1.22  lemmas o_def = comp_def
    1.23 @@ -335,6 +339,17 @@
    1.24  lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
    1.25  by (rule ext, auto)
    1.26  
    1.27 +subsection{* overwrite *}
    1.28 +
    1.29 +lemma overwrite_emptyset[simp]: "f(g|{}) = f"
    1.30 +by(simp add:overwrite_def)
    1.31 +
    1.32 +lemma overwrite_apply_notin[simp]: "a ~: A ==> (f(g|A)) a = f a"
    1.33 +by(simp add:overwrite_def)
    1.34 +
    1.35 +lemma overwrite_apply_in[simp]: "a : A ==> (f(g|A)) a = g a"
    1.36 +by(simp add:overwrite_def)
    1.37 +
    1.38  text{*The ML section includes some compatibility bindings and a simproc
    1.39  for function updates, in addition to the usual ML-bindings of theorems.*}
    1.40  ML