src/HOL/Library/FuncSet.thy
changeset 53015 a1119cf551e8
parent 50123 69b35a75caf3
child 53381 355a4cac5440
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -342,21 +342,21 @@
     1.4  definition PiE :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set" where
     1.5    "PiE S T = Pi S T \<inter> extensional S"
     1.6  
     1.7 -abbreviation "Pi\<^isub>E A B \<equiv> PiE A B"
     1.8 +abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
     1.9  
    1.10  syntax "_PiE"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PIE _:_./ _)" 10)
    1.11  
    1.12 -syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
    1.13 +syntax (xsymbols) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
    1.14  
    1.15 -syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^isub>E _\<in>_./ _)" 10)
    1.16 +syntax (HTML output) "_PiE" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
    1.17  
    1.18 -translations "PIE x:A. B" == "CONST Pi\<^isub>E A (%x. B)"
    1.19 +translations "PIE x:A. B" == "CONST Pi\<^sub>E A (%x. B)"
    1.20  
    1.21 -abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^isub>E" 60) where
    1.22 -  "A ->\<^isub>E B \<equiv> (\<Pi>\<^isub>E i\<in>A. B)"
    1.23 +abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60) where
    1.24 +  "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
    1.25  
    1.26  notation (xsymbols)
    1.27 -  extensional_funcset  (infixr "\<rightarrow>\<^isub>E" 60)
    1.28 +  extensional_funcset  (infixr "\<rightarrow>\<^sub>E" 60)
    1.29  
    1.30  lemma extensional_funcset_def: "extensional_funcset S T = (S -> T) \<inter> extensional S"
    1.31    by (simp add: PiE_def)
    1.32 @@ -368,16 +368,16 @@
    1.33    unfolding PiE_def by auto
    1.34  
    1.35  lemma PiE_eq_empty_iff:
    1.36 -  "Pi\<^isub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
    1.37 +  "Pi\<^sub>E I F = {} \<longleftrightarrow> (\<exists>i\<in>I. F i = {})"
    1.38  proof
    1.39 -  assume "Pi\<^isub>E I F = {}"
    1.40 +  assume "Pi\<^sub>E I F = {}"
    1.41    show "\<exists>i\<in>I. F i = {}"
    1.42    proof (rule ccontr)
    1.43      assume "\<not> ?thesis"
    1.44      then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
    1.45      from choice[OF this] guess f ..
    1.46 -    then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
    1.47 -    with `Pi\<^isub>E I F = {}` show False by auto
    1.48 +    then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
    1.49 +    with `Pi\<^sub>E I F = {}` show False by auto
    1.50    qed
    1.51  qed (auto simp: PiE_def)
    1.52  
    1.53 @@ -405,11 +405,11 @@
    1.54    then show ?thesis using assms by (auto intro: PiE_fun_upd)
    1.55  qed
    1.56  
    1.57 -lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
    1.58 +lemma PiE_Int: "(Pi\<^sub>E I A) \<inter> (Pi\<^sub>E I B) = Pi\<^sub>E I (\<lambda>x. A x \<inter> B x)"
    1.59    by (auto simp: PiE_def)
    1.60  
    1.61  lemma PiE_cong:
    1.62 -  "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^isub>E I A = Pi\<^isub>E I B"
    1.63 +  "(\<And>i. i\<in>I \<Longrightarrow> A i = B i) \<Longrightarrow> Pi\<^sub>E I A = Pi\<^sub>E I B"
    1.64    unfolding PiE_def by (auto simp: Pi_cong)
    1.65  
    1.66  lemma PiE_E [elim]:
    1.67 @@ -433,22 +433,22 @@
    1.68  
    1.69  lemma PiE_eq_subset:
    1.70    assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
    1.71 -  assumes eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and "i \<in> I"
    1.72 +  assumes eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'" and "i \<in> I"
    1.73    shows "F i \<subseteq> F' i"
    1.74  proof
    1.75    fix x assume "x \<in> F i"
    1.76    with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
    1.77    from choice[OF this] guess f .. note f = this
    1.78 -  then have "f \<in> Pi\<^isub>E I F" by (auto simp: extensional_def PiE_def)
    1.79 -  then have "f \<in> Pi\<^isub>E I F'" using assms by simp
    1.80 +  then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
    1.81 +  then have "f \<in> Pi\<^sub>E I F'" using assms by simp
    1.82    then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
    1.83  qed
    1.84  
    1.85  lemma PiE_eq_iff_not_empty:
    1.86    assumes ne: "\<And>i. i \<in> I \<Longrightarrow> F i \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> F' i \<noteq> {}"
    1.87 -  shows "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
    1.88 +  shows "Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i)"
    1.89  proof (intro iffI ballI)
    1.90 -  fix i assume eq: "Pi\<^isub>E I F = Pi\<^isub>E I F'" and i: "i \<in> I"
    1.91 +  fix i assume eq: "Pi\<^sub>E I F = Pi\<^sub>E I F'" and i: "i \<in> I"
    1.92    show "F i = F' i"
    1.93      using PiE_eq_subset[of I F F', OF ne eq i]
    1.94      using PiE_eq_subset[of I F' F, OF ne(2,1) eq[symmetric] i]
    1.95 @@ -456,21 +456,21 @@
    1.96  qed (auto simp: PiE_def)
    1.97  
    1.98  lemma PiE_eq_iff:
    1.99 -  "Pi\<^isub>E I F = Pi\<^isub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   1.100 +  "Pi\<^sub>E I F = Pi\<^sub>E I F' \<longleftrightarrow> (\<forall>i\<in>I. F i = F' i) \<or> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   1.101  proof (intro iffI disjCI)
   1.102 -  assume eq[simp]: "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   1.103 +  assume eq[simp]: "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   1.104    assume "\<not> ((\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {}))"
   1.105    then have "(\<forall>i\<in>I. F i \<noteq> {}) \<and> (\<forall>i\<in>I. F' i \<noteq> {})"
   1.106      using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by auto
   1.107    with PiE_eq_iff_not_empty[of I F F'] show "\<forall>i\<in>I. F i = F' i" by auto
   1.108  next
   1.109    assume "(\<forall>i\<in>I. F i = F' i) \<or> (\<exists>i\<in>I. F i = {}) \<and> (\<exists>i\<in>I. F' i = {})"
   1.110 -  then show "Pi\<^isub>E I F = Pi\<^isub>E I F'"
   1.111 +  then show "Pi\<^sub>E I F = Pi\<^sub>E I F'"
   1.112      using PiE_eq_empty_iff[of I F] PiE_eq_empty_iff[of I F'] by (auto simp: PiE_def)
   1.113  qed
   1.114  
   1.115  lemma extensional_funcset_fun_upd_restricts_rangeI: 
   1.116 -  "\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f : (insert x S) \<rightarrow>\<^isub>E T ==> f(x := undefined) : S \<rightarrow>\<^isub>E (T - {f x})"
   1.117 +  "\<forall>y \<in> S. f x \<noteq> f y \<Longrightarrow> f : (insert x S) \<rightarrow>\<^sub>E T ==> f(x := undefined) : S \<rightarrow>\<^sub>E (T - {f x})"
   1.118    unfolding extensional_funcset_def extensional_def
   1.119    apply auto
   1.120    apply (case_tac "x = xa")
   1.121 @@ -478,21 +478,21 @@
   1.122    done
   1.123  
   1.124  lemma extensional_funcset_fun_upd_extends_rangeI:
   1.125 -  assumes "a \<in> T" "f \<in> S \<rightarrow>\<^isub>E (T - {a})"
   1.126 -  shows "f(x := a) \<in> (insert x S) \<rightarrow>\<^isub>E  T"
   1.127 +  assumes "a \<in> T" "f \<in> S \<rightarrow>\<^sub>E (T - {a})"
   1.128 +  shows "f(x := a) \<in> (insert x S) \<rightarrow>\<^sub>E  T"
   1.129    using assms unfolding extensional_funcset_def extensional_def by auto
   1.130  
   1.131  subsubsection {* Injective Extensional Function Spaces *}
   1.132  
   1.133  lemma extensional_funcset_fun_upd_inj_onI:
   1.134 -  assumes "f \<in> S \<rightarrow>\<^isub>E (T - {a})" "inj_on f S"
   1.135 +  assumes "f \<in> S \<rightarrow>\<^sub>E (T - {a})" "inj_on f S"
   1.136    shows "inj_on (f(x := a)) S"
   1.137    using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
   1.138  
   1.139  lemma extensional_funcset_extend_domain_inj_on_eq:
   1.140    assumes "x \<notin> S"
   1.141 -  shows"{f. f \<in> (insert x S) \<rightarrow>\<^isub>E T \<and> inj_on f (insert x S)} =
   1.142 -    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T - {y}) \<and> inj_on g S}"
   1.143 +  shows"{f. f \<in> (insert x S) \<rightarrow>\<^sub>E T \<and> inj_on f (insert x S)} =
   1.144 +    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
   1.145  proof -
   1.146    from assms show ?thesis
   1.147      apply (auto del: PiE_I PiE_E)
   1.148 @@ -508,7 +508,7 @@
   1.149  
   1.150  lemma extensional_funcset_extend_domain_inj_onI:
   1.151    assumes "x \<notin> S"
   1.152 -  shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^isub>E (T - {y}) \<and> inj_on g S}"
   1.153 +  shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> S \<rightarrow>\<^sub>E (T - {y}) \<and> inj_on g S}"
   1.154  proof -
   1.155    from assms show ?thesis
   1.156      apply (auto intro!: inj_onI)
   1.157 @@ -522,9 +522,9 @@
   1.158  lemma finite_PiE: "finite S \<Longrightarrow> (\<And>i. i \<in> S \<Longrightarrow> finite (T i)) \<Longrightarrow> finite (PIE i : S. T i)"
   1.159    by (induct S arbitrary: T rule: finite_induct) (simp_all add: PiE_insert_eq)
   1.160  
   1.161 -lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^isub>E S T)"
   1.162 +lemma inj_combinator: "x \<notin> S \<Longrightarrow> inj_on (\<lambda>(y, g). g(x := y)) (T x \<times> Pi\<^sub>E S T)"
   1.163  proof (safe intro!: inj_onI ext)
   1.164 -  fix f y g z assume "x \<notin> S" and fg: "f \<in> Pi\<^isub>E S T" "g \<in> Pi\<^isub>E S T"
   1.165 +  fix f y g z assume "x \<notin> S" and fg: "f \<in> Pi\<^sub>E S T" "g \<in> Pi\<^sub>E S T"
   1.166    assume "f(x := y) = g(x := z)"
   1.167    then have *: "\<And>i. (f(x := y)) i = (g(x := z)) i"
   1.168      unfolding fun_eq_iff by auto