more on bij_betw
authorpaulson
Tue Jun 01 11:25:26 2004 +0200 (2004-06-01)
changeset 148538d710bece29f
parent 14852 fffab59e0050
child 14854 61bdf2ae4dc5
more on bij_betw
src/HOL/Algebra/Bij.thy
src/HOL/Library/FuncSet.thy
     1.1 --- a/src/HOL/Algebra/Bij.thy	Tue Jun 01 11:25:01 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Tue Jun 01 11:25:26 2004 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  constdefs
     1.5    Bij :: "'a set => ('a => 'a) set"
     1.6      --{*Only extensional functions, since otherwise we get too many.*}
     1.7 -  "Bij S == extensional S \<inter> {f. f`S = S & inj_on f S}"
     1.8 +  "Bij S == extensional S \<inter> {f. bij_betw f S S}"
     1.9  
    1.10    BijGroup :: "'a set => ('a => 'a) monoid"
    1.11    "BijGroup S ==
    1.12 @@ -25,53 +25,23 @@
    1.13    by (simp add: Bij_def)
    1.14  
    1.15  lemma Bij_imp_funcset: "f \<in> Bij S ==> f \<in> S -> S"
    1.16 -  by (auto simp add: Bij_def Pi_def)
    1.17 -
    1.18 -lemma Bij_imp_apply: "f \<in> Bij S ==> f ` S = S"
    1.19 -  by (simp add: Bij_def)
    1.20 -
    1.21 -lemma Bij_imp_inj_on: "f \<in> Bij S ==> inj_on f S"
    1.22 -  by (simp add: Bij_def)
    1.23 -
    1.24 -lemma BijI: "[| f \<in> extensional(S); f`S = S; inj_on f S |] ==> f \<in> Bij S"
    1.25 -  by (simp add: Bij_def)
    1.26 +  by (auto simp add: Bij_def bij_betw_imp_funcset)
    1.27  
    1.28  
    1.29  subsection {*Bijections Form a Group *}
    1.30  
    1.31  lemma restrict_Inv_Bij: "f \<in> Bij S ==> (%x:S. (Inv S f) x) \<in> Bij S"
    1.32 -apply (simp add: Bij_def)
    1.33 -apply (intro conjI)
    1.34 -txt{*Proving @{term "restrict (Inv S f) S ` S = S"}*}
    1.35 - apply (rule equalityI)
    1.36 -  apply (force simp add: Inv_mem) --{*first inclusion*}
    1.37 - apply (rule subsetI)   --{*second inclusion*}
    1.38 - apply (rule_tac x = "f x" in image_eqI)
    1.39 -  apply (force intro:  simp add: Inv_f_f, blast)
    1.40 -txt{*Remaining goal: @{term "inj_on (restrict (Inv S f) S) S"}*}
    1.41 -apply (rule inj_onI)
    1.42 -apply (auto elim: Inv_injective)
    1.43 -done
    1.44 +  by (simp add: Bij_def bij_betw_Inv)
    1.45  
    1.46  lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
    1.47 -apply (rule BijI)
    1.48 -apply (auto simp add: inj_on_def)
    1.49 -done
    1.50 +  by (auto simp add: Bij_def bij_betw_def inj_on_def)
    1.51  
    1.52  lemma compose_Bij: "[| x \<in> Bij S; y \<in> Bij S|] ==> compose S x y \<in> Bij S"
    1.53 -apply (rule BijI)
    1.54 -  apply (simp add: compose_extensional)
    1.55 - apply (blast del: equalityI
    1.56 -              intro: surj_compose dest: Bij_imp_apply Bij_imp_inj_on)
    1.57 -apply (blast intro: inj_on_compose dest: Bij_imp_apply Bij_imp_inj_on)
    1.58 -done
    1.59 +  by (auto simp add: Bij_def bij_betw_compose) 
    1.60  
    1.61  lemma Bij_compose_restrict_eq:
    1.62       "f \<in> Bij S ==> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
    1.63 -apply (rule compose_Inv_id)
    1.64 - apply (simp add: Bij_imp_inj_on)
    1.65 -apply (simp add: Bij_imp_apply)
    1.66 -done
    1.67 +  by (simp add: Bij_def compose_Inv_id)
    1.68  
    1.69  theorem group_BijGroup: "group (BijGroup S)"
    1.70  apply (simp add: BijGroup_def)
    1.71 @@ -87,16 +57,16 @@
    1.72  
    1.73  subsection{*Automorphisms Form a Group*}
    1.74  
    1.75 -lemma Bij_Inv_mem: "[|  f \<in> Bij S;  x : S |] ==> Inv S f x : S"
    1.76 -by (simp add: Bij_def Inv_mem)
    1.77 +lemma Bij_Inv_mem: "[|  f \<in> Bij S;  x \<in> S |] ==> Inv S f x \<in> S"
    1.78 +by (simp add: Bij_def bij_betw_def Inv_mem)
    1.79  
    1.80  lemma Bij_Inv_lemma:
    1.81   assumes eq: "!!x y. [|x \<in> S; y \<in> S|] ==> h(g x y) = g (h x) (h y)"
    1.82   shows "[| h \<in> Bij S;  g \<in> S \<rightarrow> S \<rightarrow> S;  x \<in> S;  y \<in> S |]
    1.83          ==> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
    1.84 -apply (simp add: Bij_def)
    1.85 -apply (subgoal_tac "EX x':S. EX y':S. x = h x' & y = h y'", clarify)
    1.86 - apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
    1.87 +apply (simp add: Bij_def bij_betw_def)
    1.88 +apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
    1.89 + apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast )
    1.90  done
    1.91  
    1.92  constdefs
    1.93 @@ -130,7 +100,7 @@
    1.94  apply (rule group.subgroupI)
    1.95      apply (rule group_BijGroup)
    1.96     apply (force simp add: auto_def BijGroup_def)
    1.97 -  apply (blast intro: dest: id_in_auto)
    1.98 +  apply (blast dest: id_in_auto)
    1.99   apply (simp del: restrict_apply
   1.100               add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
   1.101  apply (auto simp add: BijGroup_def auto_def Bij_imp_funcset group.hom_compose
     2.1 --- a/src/HOL/Library/FuncSet.thy	Tue Jun 01 11:25:01 2004 +0200
     2.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jun 01 11:25:26 2004 +0200
     2.3 @@ -100,10 +100,6 @@
     2.4  lemma surj_compose: "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C"
     2.5    by (auto simp add: image_def compose_eq)
     2.6  
     2.7 -lemma inj_on_compose:
     2.8 -    "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A"
     2.9 -  by (auto simp add: inj_on_def compose_eq)
    2.10 -
    2.11  
    2.12  subsection{*Bounded Abstraction: @{term restrict}*}
    2.13  
    2.14 @@ -121,7 +117,7 @@
    2.15      "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
    2.16    by (simp add: expand_fun_eq Pi_def Pi_def restrict_def)
    2.17  
    2.18 -lemma inj_on_restrict_eq: "inj_on (restrict f A) A = inj_on f A"
    2.19 +lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
    2.20    by (simp add: inj_on_def restrict_def)
    2.21  
    2.22  lemma Id_compose:
    2.23 @@ -132,41 +128,8 @@
    2.24      "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
    2.25    by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
    2.26  
    2.27 -
    2.28 -subsection{*Extensionality*}
    2.29 -
    2.30 -lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
    2.31 -  by (simp add: extensional_def)
    2.32 -
    2.33 -lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
    2.34 -  by (simp add: restrict_def extensional_def)
    2.35 -
    2.36 -lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
    2.37 -  by (simp add: compose_def)
    2.38 -
    2.39 -lemma extensionalityI:
    2.40 -    "[| f \<in> extensional A; g \<in> extensional A;
    2.41 -      !!x. x\<in>A ==> f x = g x |] ==> f = g"
    2.42 -  by (force simp add: expand_fun_eq extensional_def)
    2.43 -
    2.44 -lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
    2.45 -  by (unfold Inv_def) (fast intro: restrict_in_funcset someI2)
    2.46 -
    2.47 -lemma compose_Inv_id:
    2.48 -    "[| inj_on f A;  f ` A = B |]
    2.49 -      ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
    2.50 -  apply (simp add: compose_def)
    2.51 -  apply (rule restrict_ext, auto)
    2.52 -  apply (erule subst)
    2.53 -  apply (simp add: Inv_f_f)
    2.54 -  done
    2.55 -
    2.56 -lemma compose_id_Inv:
    2.57 -    "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
    2.58 -  apply (simp add: compose_def)
    2.59 -  apply (rule restrict_ext)
    2.60 -  apply (simp add: f_Inv_f)
    2.61 -  done
    2.62 +lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
    2.63 +  by (auto simp add: restrict_def) 
    2.64  
    2.65  
    2.66  subsection{*Bijections Between Sets*}
    2.67 @@ -190,12 +153,55 @@
    2.68  apply (simp add: image_def Inv_f_f) 
    2.69  done
    2.70  
    2.71 +lemma inj_on_compose:
    2.72 +    "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
    2.73 +  by (auto simp add: bij_betw_def inj_on_def compose_eq)
    2.74 +
    2.75  lemma bij_betw_compose:
    2.76      "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
    2.77  apply (simp add: bij_betw_def compose_eq inj_on_compose)
    2.78  apply (auto simp add: compose_def image_def)
    2.79  done
    2.80  
    2.81 +lemma bij_betw_restrict_eq [simp]:
    2.82 +     "bij_betw (restrict f A) A B = bij_betw f A B"
    2.83 +  by (simp add: bij_betw_def)
    2.84 +
    2.85 +
    2.86 +subsection{*Extensionality*}
    2.87 +
    2.88 +lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
    2.89 +  by (simp add: extensional_def)
    2.90 +
    2.91 +lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
    2.92 +  by (simp add: restrict_def extensional_def)
    2.93 +
    2.94 +lemma compose_extensional [simp]: "compose A f g \<in> extensional A"
    2.95 +  by (simp add: compose_def)
    2.96 +
    2.97 +lemma extensionalityI:
    2.98 +    "[| f \<in> extensional A; g \<in> extensional A;
    2.99 +      !!x. x\<in>A ==> f x = g x |] ==> f = g"
   2.100 +  by (force simp add: expand_fun_eq extensional_def)
   2.101 +
   2.102 +lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
   2.103 +  by (unfold Inv_def) (fast intro: restrict_in_funcset someI2)
   2.104 +
   2.105 +lemma compose_Inv_id:
   2.106 +    "bij_betw f A B ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
   2.107 +  apply (simp add: bij_betw_def compose_def)
   2.108 +  apply (rule restrict_ext, auto)
   2.109 +  apply (erule subst)
   2.110 +  apply (simp add: Inv_f_f)
   2.111 +  done
   2.112 +
   2.113 +lemma compose_id_Inv:
   2.114 +    "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
   2.115 +  apply (simp add: compose_def)
   2.116 +  apply (rule restrict_ext)
   2.117 +  apply (simp add: f_Inv_f)
   2.118 +  done
   2.119 +
   2.120  
   2.121  subsection{*Cardinality*}
   2.122