src/HOL/Fun.thy
changeset 15510 9de204d7b699
parent 15439 71c0f98e31f1
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Fun.thy	Wed Feb 09 12:08:46 2005 +0100
     1.2 +++ b/src/HOL/Fun.thy	Wed Feb 09 18:32:28 2005 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Notions about functions.
     1.5  *)
     1.6  
     1.7 -theory Fun 
     1.8 +theory Fun
     1.9  imports Typedef
    1.10  begin
    1.11  
    1.12 @@ -93,6 +93,16 @@
    1.13  lemma id_apply [simp]: "id x = x"
    1.14  by (simp add: id_def)
    1.15  
    1.16 +lemma inj_on_id: "inj_on id A"
    1.17 +by (simp add: inj_on_def) 
    1.18 +
    1.19 +lemma surj_id: "surj id"
    1.20 +by (simp add: surj_def) 
    1.21 +
    1.22 +lemma bij_id: "bij id"
    1.23 +by (simp add: bij_def inj_on_id surj_id) 
    1.24 +
    1.25 +
    1.26  
    1.27  subsection{*The Composition Operator: @{term "f \<circ> g"}*}
    1.28  
    1.29 @@ -378,6 +388,10 @@
    1.30  lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
    1.31  by(fastsimp simp:inj_on_def image_def)
    1.32  
    1.33 +lemma fun_upd_image:
    1.34 +     "f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
    1.35 +by auto
    1.36 +
    1.37  subsection{* overwrite *}
    1.38  
    1.39  lemma overwrite_emptyset[simp]: "f(g|{}) = f"
    1.40 @@ -389,6 +403,58 @@
    1.41  lemma overwrite_apply_in[simp]: "a : A ==> (f(g|A)) a = g a"
    1.42  by(simp add:overwrite_def)
    1.43  
    1.44 +subsection{* swap *}
    1.45 +
    1.46 +constdefs
    1.47 +  swap :: "['a, 'a, 'a => 'b] => ('a => 'b)"
    1.48 +   "swap a b f == f(a := f b, b:= f a)"
    1.49 +
    1.50 +lemma swap_self: "swap a a f = f"
    1.51 +by (simp add: swap_def) 
    1.52 +
    1.53 +lemma swap_commute: "swap a b f = swap b a f"
    1.54 +by (rule ext, simp add: fun_upd_def swap_def)
    1.55 +
    1.56 +lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
    1.57 +by (rule ext, simp add: fun_upd_def swap_def)
    1.58 +
    1.59 +lemma inj_on_imp_inj_on_swap:
    1.60 +     "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
    1.61 +by (simp add: inj_on_def swap_def, blast)
    1.62 +
    1.63 +lemma inj_on_swap_iff [simp]:
    1.64 +  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
    1.65 +proof 
    1.66 +  assume "inj_on (swap a b f) A"
    1.67 +  with A have "inj_on (swap a b (swap a b f)) A" 
    1.68 +    by (rules intro: inj_on_imp_inj_on_swap) 
    1.69 +  thus "inj_on f A" by simp 
    1.70 +next
    1.71 +  assume "inj_on f A"
    1.72 +  with A show "inj_on (swap a b f) A" by (rules intro: inj_on_imp_inj_on_swap)
    1.73 +qed
    1.74 +
    1.75 +lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
    1.76 +apply (simp add: surj_def swap_def, clarify)
    1.77 +apply (rule_tac P = "y = f b" in case_split_thm, blast)
    1.78 +apply (rule_tac P = "y = f a" in case_split_thm, auto)
    1.79 +  --{*We don't yet have @{text case_tac}*}
    1.80 +done
    1.81 +
    1.82 +lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
    1.83 +proof 
    1.84 +  assume "surj (swap a b f)"
    1.85 +  hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap) 
    1.86 +  thus "surj f" by simp 
    1.87 +next
    1.88 +  assume "surj f"
    1.89 +  thus "surj (swap a b f)" by (rule surj_imp_surj_swap) 
    1.90 +qed
    1.91 +
    1.92 +lemma bij_swap_iff: "bij (swap a b f) = bij f"
    1.93 +by (simp add: bij_def)
    1.94 + 
    1.95 +
    1.96  text{*The ML section includes some compatibility bindings and a simproc
    1.97  for function updates, in addition to the usual ML-bindings of theorems.*}
    1.98  ML