--- a/src/HOL/Fun.thy Wed Feb 09 12:08:46 2005 +0100
+++ b/src/HOL/Fun.thy Wed Feb 09 18:32:28 2005 +0100
@@ -6,7 +6,7 @@
Notions about functions.
*)
-theory Fun
+theory Fun
imports Typedef
begin
@@ -93,6 +93,16 @@
lemma id_apply [simp]: "id x = x"
by (simp add: id_def)
+lemma inj_on_id: "inj_on id A"
+by (simp add: inj_on_def)
+
+lemma surj_id: "surj id"
+by (simp add: surj_def)
+
+lemma bij_id: "bij id"
+by (simp add: bij_def inj_on_id surj_id)
+
+
subsection{*The Composition Operator: @{term "f \<circ> g"}*}
@@ -378,6 +388,10 @@
lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
by(fastsimp simp:inj_on_def image_def)
+lemma fun_upd_image:
+ "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
+by auto
+
subsection{* overwrite *}
lemma overwrite_emptyset[simp]: "f(g|{}) = f"
@@ -389,6 +403,58 @@
lemma overwrite_apply_in[simp]: "a : A ==> (f(g|A)) a = g a"
by(simp add:overwrite_def)
+subsection{* swap *}
+
+constdefs
+ swap :: "['a, 'a, 'a => 'b] => ('a => 'b)"
+ "swap a b f == f(a := f b, b:= f a)"
+
+lemma swap_self: "swap a a f = f"
+by (simp add: swap_def)
+
+lemma swap_commute: "swap a b f = swap b a f"
+by (rule ext, simp add: fun_upd_def swap_def)
+
+lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
+by (rule ext, simp add: fun_upd_def swap_def)
+
+lemma inj_on_imp_inj_on_swap:
+ "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
+by (simp add: inj_on_def swap_def, blast)
+
+lemma inj_on_swap_iff [simp]:
+ assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
+proof
+ assume "inj_on (swap a b f) A"
+ with A have "inj_on (swap a b (swap a b f)) A"
+ by (rules intro: inj_on_imp_inj_on_swap)
+ thus "inj_on f A" by simp
+next
+ assume "inj_on f A"
+ with A show "inj_on (swap a b f) A" by (rules intro: inj_on_imp_inj_on_swap)
+qed
+
+lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
+apply (simp add: surj_def swap_def, clarify)
+apply (rule_tac P = "y = f b" in case_split_thm, blast)
+apply (rule_tac P = "y = f a" in case_split_thm, auto)
+ --{*We don't yet have @{text case_tac}*}
+done
+
+lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
+proof
+ assume "surj (swap a b f)"
+ hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
+ thus "surj f" by simp
+next
+ assume "surj f"
+ thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
+qed
+
+lemma bij_swap_iff: "bij (swap a b f) = bij f"
+by (simp add: bij_def)
+
+
text{*The ML section includes some compatibility bindings and a simproc
for function updates, in addition to the usual ML-bindings of theorems.*}
ML