src/HOL/Fun.thy
changeset 56608 8e3c848008fa
parent 56154 f0a927235162
child 57282 7da3e398804c
     1.1 --- a/src/HOL/Fun.thy	Wed Apr 16 18:28:13 2014 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Apr 16 21:51:41 2014 +0200
     1.3 @@ -641,17 +641,31 @@
     1.4  
     1.5  subsection {* @{text swap} *}
     1.6  
     1.7 -definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
     1.8 +definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
     1.9 +where
    1.10    "swap a b f = f (a := f b, b:= f a)"
    1.11  
    1.12 -lemma swap_self [simp]: "swap a a f = f"
    1.13 -by (simp add: swap_def)
    1.14 +lemma swap_apply [simp]:
    1.15 +  "swap a b f a = f b"
    1.16 +  "swap a b f b = f a"
    1.17 +  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> swap a b f c = f c"
    1.18 +  by (simp_all add: swap_def)
    1.19 +
    1.20 +lemma swap_self [simp]:
    1.21 +  "swap a a f = f"
    1.22 +  by (simp add: swap_def)
    1.23  
    1.24 -lemma swap_commute: "swap a b f = swap b a f"
    1.25 -by (rule ext, simp add: fun_upd_def swap_def)
    1.26 +lemma swap_commute:
    1.27 +  "swap a b f = swap b a f"
    1.28 +  by (simp add: fun_upd_def swap_def fun_eq_iff)
    1.29  
    1.30 -lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
    1.31 -by (rule ext, simp add: fun_upd_def swap_def)
    1.32 +lemma swap_nilpotent [simp]:
    1.33 +  "swap a b (swap a b f) = f"
    1.34 +  by (rule ext, simp add: fun_upd_def swap_def)
    1.35 +
    1.36 +lemma swap_comp_involutory [simp]:
    1.37 +  "swap a b \<circ> swap a b = id"
    1.38 +  by (rule ext) simp
    1.39  
    1.40  lemma swap_triple:
    1.41    assumes "a \<noteq> c" and "b \<noteq> c"
    1.42 @@ -659,7 +673,7 @@
    1.43    using assms by (simp add: fun_eq_iff swap_def)
    1.44  
    1.45  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
    1.46 -by (rule ext, simp add: fun_upd_def swap_def)
    1.47 +  by (rule ext, simp add: fun_upd_def swap_def)
    1.48  
    1.49  lemma swap_image_eq [simp]:
    1.50    assumes "a \<in> A" "b \<in> A" shows "swap a b f ` A = f ` A"
    1.51 @@ -701,6 +715,7 @@
    1.52  
    1.53  hide_const (open) swap
    1.54  
    1.55 +
    1.56  subsection {* Inversion of injective functions *}
    1.57  
    1.58  definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where