adding extensional function spaces to the FuncSet library theory
authorbulwahn
Mon Nov 22 10:41:51 2010 +0100 (2010-11-22)
changeset 40631b3f85ba3dae4
parent 40630 3b5c31e55540
child 40632 dc55e6752046
adding extensional function spaces to the FuncSet library theory
src/HOL/Library/FuncSet.thy
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Nov 22 09:19:34 2010 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Nov 22 10:41:51 2010 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/Library/FuncSet.thy
     1.5 -    Author:     Florian Kammueller and Lawrence C Paulson
     1.6 +    Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
     1.7  *)
     1.8  
     1.9  header {* Pi and Function Sets *}
    1.10 @@ -251,4 +251,158 @@
    1.11       g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
    1.12  by (blast intro: card_inj order_antisym)
    1.13  
    1.14 +subsection {* Extensional Function Spaces *} 
    1.15 +
    1.16 +definition extensional_funcset
    1.17 +where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
    1.18 +
    1.19 +lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
    1.20 +unfolding extensional_def by (auto intro: ext)
    1.21 +
    1.22 +lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
    1.23 +unfolding extensional_funcset_def by simp
    1.24 +
    1.25 +lemma extensional_funcset_empty_range:
    1.26 +  assumes "S \<noteq> {}"
    1.27 +  shows "extensional_funcset S {} = {}"
    1.28 +using assms unfolding extensional_funcset_def by auto
    1.29 +
    1.30 +lemma extensional_funcset_arb:
    1.31 +  assumes "f \<in> extensional_funcset S T" "x \<notin> S"
    1.32 +  shows "f x = undefined"
    1.33 +using assms
    1.34 +unfolding extensional_funcset_def by auto (auto dest!: extensional_arb)
    1.35 +
    1.36 +lemma extensional_funcset_mem: "f \<in> extensional_funcset S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T"
    1.37 +unfolding extensional_funcset_def by auto
    1.38 +
    1.39 +lemma extensional_subset: "f : extensional A ==> A <= B ==> f : extensional B"
    1.40 +unfolding extensional_def by auto
    1.41 +
    1.42 +lemma extensional_funcset_extend_domainI: "\<lbrakk> y \<in> T; f \<in> extensional_funcset S T\<rbrakk> \<Longrightarrow> f(x := y) \<in> extensional_funcset (insert x S) T"
    1.43 +unfolding extensional_funcset_def extensional_def by auto
    1.44 +
    1.45 +lemma extensional_funcset_restrict_domain:
    1.46 +  "x \<notin> S \<Longrightarrow> f \<in> extensional_funcset (insert x S) T \<Longrightarrow> f(x := undefined) \<in> extensional_funcset S T"
    1.47 +unfolding extensional_funcset_def extensional_def by auto
    1.48 +
    1.49 +lemma extensional_funcset_extend_domain_eq:
    1.50 +  assumes "x \<notin> S"
    1.51 +  shows
    1.52 +    "extensional_funcset (insert x S) T = (\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S T}"
    1.53 +  using assms
    1.54 +proof -
    1.55 +  {
    1.56 +    fix f
    1.57 +    assume "f : extensional_funcset (insert x S) T"
    1.58 +    from this assms have "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
    1.59 +      unfolding image_iff
    1.60 +      apply (rule_tac x="(f x, f(x := undefined))" in bexI)
    1.61 +    apply (auto intro: extensional_funcset_extend_domainI extensional_funcset_restrict_domain extensional_funcset_mem) done 
    1.62 +  }
    1.63 +  moreover
    1.64 +  {
    1.65 +    fix f
    1.66 +    assume "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
    1.67 +    from this assms have "f : extensional_funcset (insert x S) T"
    1.68 +      by (auto intro: extensional_funcset_extend_domainI)
    1.69 +  }
    1.70 +  ultimately show ?thesis by auto
    1.71 +qed
    1.72 +
    1.73 +lemma extensional_funcset_fun_upd_restricts_rangeI:  "\<forall> y \<in> S. f x \<noteq> f y ==> f : extensional_funcset (insert x S) T ==> f(x := undefined) : extensional_funcset S (T - {f x})"
    1.74 +unfolding extensional_funcset_def extensional_def
    1.75 +apply auto
    1.76 +apply (case_tac "x = xa")
    1.77 +apply auto done
    1.78 +
    1.79 +lemma extensional_funcset_fun_upd_extends_rangeI:
    1.80 +  assumes "a \<in> T" "f : extensional_funcset S (T - {a})"
    1.81 +  shows "f(x := a) : extensional_funcset (insert x S) T"
    1.82 +  using assms unfolding extensional_funcset_def extensional_def by auto
    1.83 +
    1.84 +subsubsection {* Injective Extensional Function Spaces *}
    1.85 +
    1.86 +lemma extensional_funcset_fun_upd_inj_onI:
    1.87 +  assumes "f \<in> extensional_funcset S (T - {a})" "inj_on f S"
    1.88 +  shows "inj_on (f(x := a)) S"
    1.89 +  using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
    1.90 +
    1.91 +lemma extensional_funcset_extend_domain_inj_on_eq:
    1.92 +  assumes "x \<notin> S"
    1.93 +  shows"{f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} =
    1.94 +    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
    1.95 +proof -
    1.96 +  from assms show ?thesis
    1.97 +    apply auto
    1.98 +    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI)
    1.99 +    apply (auto simp add: image_iff inj_on_def)
   1.100 +    apply (rule_tac x="xa x" in exI)
   1.101 +    apply (auto intro: extensional_funcset_mem)
   1.102 +    apply (rule_tac x="xa(x := undefined)" in exI)
   1.103 +    apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
   1.104 +    apply (auto dest!: extensional_funcset_mem split: split_if_asm)
   1.105 +    done
   1.106 +qed
   1.107 +
   1.108 +lemma extensional_funcset_extend_domain_inj_onI:
   1.109 +  assumes "x \<notin> S"
   1.110 +  shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
   1.111 +proof -
   1.112 +  from assms show ?thesis
   1.113 +    apply (auto intro!: inj_onI)
   1.114 +    apply (metis fun_upd_same)
   1.115 +    by (metis assms extensional_funcset_arb fun_upd_triv fun_upd_upd)
   1.116 +qed
   1.117 +  
   1.118 +
   1.119 +subsubsection {* Cardinality *}
   1.120 +
   1.121 +lemma card_extensional_funcset:
   1.122 +  assumes "finite S"
   1.123 +  shows "card (extensional_funcset S T) = (card T) ^ (card S)"
   1.124 +using assms
   1.125 +proof (induct rule: finite_induct)
   1.126 +  case empty
   1.127 +  show ?case
   1.128 +    by (auto simp add: extensional_funcset_empty_domain)
   1.129 +next
   1.130 +  case (insert x S)
   1.131 +  {
   1.132 +    fix g g' y y'
   1.133 +    assume assms: "g \<in> extensional_funcset S T"
   1.134 +      "g' \<in> extensional_funcset S T"
   1.135 +      "y \<in> T" "y' \<in> T"
   1.136 +      "g(x := y) = g'(x := y')"
   1.137 +    from this have "y = y'"
   1.138 +      by (metis fun_upd_same)
   1.139 +    have "g = g'"
   1.140 +      by (metis assms(1) assms(2) assms(5) extensional_funcset_arb fun_upd_triv fun_upd_upd insert(2))
   1.141 +  from `y = y'` `g = g'` have "y = y' & g = g'" by simp
   1.142 +  }
   1.143 +  from this have "inj_on (\<lambda>(y, g). g (x := y)) (T \<times> extensional_funcset S T)"
   1.144 +    by (auto intro: inj_onI)
   1.145 +  from this insert.hyps show ?case
   1.146 +    by (simp add: extensional_funcset_extend_domain_eq card_image card_cartesian_product)
   1.147 +qed
   1.148 +
   1.149 +lemma finite_extensional_funcset:
   1.150 +  assumes "finite S" "finite T"
   1.151 +  shows "finite (extensional_funcset S T)"
   1.152 +proof -
   1.153 +  from card_extensional_funcset[OF assms(1), of T] assms(2)
   1.154 +  have "(card (extensional_funcset S T) \<noteq> 0) \<or> (S \<noteq> {} \<and> T = {})"
   1.155 +    by auto
   1.156 +  from this show ?thesis
   1.157 +  proof
   1.158 +    assume "card (extensional_funcset S T) \<noteq> 0"
   1.159 +    from this show ?thesis
   1.160 +      by (auto intro: card_ge_0_finite)
   1.161 +  next
   1.162 +    assume "S \<noteq> {} \<and> T = {}"
   1.163 +    from this show ?thesis
   1.164 +      by (auto simp add: extensional_funcset_empty_range)
   1.165 +  qed
   1.166 +qed
   1.167 +
   1.168  end