src/HOL/Library/FuncSet.thy
changeset 14853 8d710bece29f
parent 14762 bd349ff7907a
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Jun 01 11:25:01 2004 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jun 01 11:25:26 2004 +0200
     1.3 @@ -100,10 +100,6 @@
     1.4  lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
     1.5    by (auto simp add: image_def compose_eq)
     1.6  
     1.7 -lemma inj_on_compose:
     1.8 -    "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
     1.9 -  by (auto simp add: inj_on_def compose_eq)
    1.10 -
    1.11  
    1.12  subsection{*Bounded Abstraction: @{term restrict}*}
    1.13  
    1.14 @@ -121,7 +117,7 @@
    1.15      "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
    1.16    by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
    1.17  
    1.18 -lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A"
    1.19 +lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
    1.20    by (simp add: inj_on_def restrict_def)
    1.21  
    1.22  lemma Id_compose:
    1.23 @@ -132,41 +128,8 @@
    1.24      "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
    1.25    by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
    1.26  
    1.27 -
    1.28 -subsection{*Extensionality*}
    1.29 -
    1.30 -lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
    1.31 -  by (simp add: extensional_def)
    1.32 -
    1.33 -lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
    1.34 -  by (simp add: restrict_def extensional_def)
    1.35 -
    1.36 -lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
    1.37 -  by (simp add: compose_def)
    1.38 -
    1.39 -lemma extensionalityI:
    1.40 -    "[| f \<in> extensional A; g \<in> extensional A;
    1.41 -      !!x. x\<in>A ==> f x = g x |] ==> f = g"
    1.42 -  by (force simp add: expand_fun_eq extensional_def)
    1.43 -
    1.44 -lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
    1.45 -  by (unfold Inv_def) (fast intro: restrict_in_funcset someI2)
    1.46 -
    1.47 -lemma compose_Inv_id:
    1.48 -    "[| inj_on f A;  f ` A = B |]
    1.49 -      ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
    1.50 -  apply (simp add: compose_def)
    1.51 -  apply (rule restrict_ext, auto)
    1.52 -  apply (erule subst)
    1.53 -  apply (simp add: Inv_f_f)
    1.54 -  done
    1.55 -
    1.56 -lemma compose_id_Inv:
    1.57 -    "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
    1.58 -  apply (simp add: compose_def)
    1.59 -  apply (rule restrict_ext)
    1.60 -  apply (simp add: f_Inv_f)
    1.61 -  done
    1.62 +lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
    1.63 +  by (auto simp add: restrict_def) 
    1.64  
    1.65  
    1.66  subsection{*Bijections Between Sets*}
    1.67 @@ -190,12 +153,55 @@
    1.68  apply (simp add: image_def Inv_f_f) 
    1.69  done
    1.70  
    1.71 +lemma inj_on_compose:
    1.72 +    "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
    1.73 +  by (auto simp add: bij_betw_def inj_on_def compose_eq)
    1.74 +
    1.75  lemma bij_betw_compose:
    1.76      "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
    1.77  apply (simp add: bij_betw_def compose_eq inj_on_compose)
    1.78  apply (auto simp add: compose_def image_def)
    1.79  done
    1.80  
    1.81 +lemma bij_betw_restrict_eq [simp]:
    1.82 +     "bij_betw (restrict f A) A B = bij_betw f A B"
    1.83 +  by (simp add: bij_betw_def)
    1.84 +
    1.85 +
    1.86 +subsection{*Extensionality*}
    1.87 +
    1.88 +lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
    1.89 +  by (simp add: extensional_def)
    1.90 +
    1.91 +lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
    1.92 +  by (simp add: restrict_def extensional_def)
    1.93 +
    1.94 +lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
    1.95 +  by (simp add: compose_def)
    1.96 +
    1.97 +lemma extensionalityI:
    1.98 +    "[| f \<in> extensional A; g \<in> extensional A;
    1.99 +      !!x. x\<in>A ==> f x = g x |] ==> f = g"
   1.100 +  by (force simp add: expand_fun_eq extensional_def)
   1.101 +
   1.102 +lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
   1.103 +  by (unfold Inv_def) (fast intro: restrict_in_funcset someI2)
   1.104 +
   1.105 +lemma compose_Inv_id:
   1.106 +    "bij_betw f A B ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
   1.107 +  apply (simp add: bij_betw_def compose_def)
   1.108 +  apply (rule restrict_ext, auto)
   1.109 +  apply (erule subst)
   1.110 +  apply (simp add: Inv_f_f)
   1.111 +  done
   1.112 +
   1.113 +lemma compose_id_Inv:
   1.114 +    "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
   1.115 +  apply (simp add: compose_def)
   1.116 +  apply (rule restrict_ext)
   1.117 +  apply (simp add: f_Inv_f)
   1.118 +  done
   1.119 +
   1.120  
   1.121  subsection{*Cardinality*}
   1.122