src/HOL/Library/FuncSet.thy
 changeset 64910 6108dddad9f0 parent 63092 a949b2a5f51d child 64917 5db5b8cf6dc6
```     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Jan 16 21:53:44 2017 +0100
1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Jan 17 11:26:21 2017 +0100
1.3 @@ -5,7 +5,9 @@
1.4  section \<open>Pi and Function Sets\<close>
1.5
1.6  theory FuncSet
1.7 -imports Hilbert_Choice Main
1.8 +  imports Hilbert_Choice Main
1.9 +  abbrevs PiE = "Pi\<^sub>E"
1.10 +    PIE = "\<Pi>\<^sub>E"
1.11  begin
1.12
1.13  definition Pi :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow> 'b) set"
1.14 @@ -360,10 +362,10 @@
1.15  lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
1.17
1.18 -lemma PiE_empty_domain[simp]: "PiE {} T = {\<lambda>x. undefined}"
1.19 +lemma PiE_empty_domain[simp]: "Pi\<^sub>E {} T = {\<lambda>x. undefined}"
1.20    unfolding PiE_def by simp
1.21
1.22 -lemma PiE_UNIV_domain: "PiE UNIV T = Pi UNIV T"
1.23 +lemma PiE_UNIV_domain: "Pi\<^sub>E UNIV T = Pi UNIV T"
1.24    unfolding PiE_def by simp
1.25
1.26  lemma PiE_empty_range[simp]: "i \<in> I \<Longrightarrow> F i = {} \<Longrightarrow> (\<Pi>\<^sub>E i\<in>I. F i) = {}"
1.27 @@ -386,29 +388,29 @@
1.28    qed
1.29  qed (auto simp: PiE_def)
1.30
1.31 -lemma PiE_arb: "f \<in> PiE S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
1.32 +lemma PiE_arb: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<notin> S \<Longrightarrow> f x = undefined"
1.33    unfolding PiE_def by auto (auto dest!: extensional_arb)
1.34
1.35 -lemma PiE_mem: "f \<in> PiE S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
1.36 +lemma PiE_mem: "f \<in> Pi\<^sub>E S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T x"
1.37    unfolding PiE_def by auto
1.38
1.39 -lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> PiE S T \<Longrightarrow> f(x := y) \<in> PiE (insert x S) T"
1.40 +lemma PiE_fun_upd: "y \<in> T x \<Longrightarrow> f \<in> Pi\<^sub>E S T \<Longrightarrow> f(x := y) \<in> Pi\<^sub>E (insert x S) T"
1.41    unfolding PiE_def extensional_def by auto
1.42
1.43 -lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
1.44 +lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> Pi\<^sub>E (insert x S) T \<Longrightarrow> f(x := undefined) \<in> Pi\<^sub>E S T"
1.45    unfolding PiE_def extensional_def by auto
1.46
1.47 -lemma PiE_insert_eq: "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.48 +lemma PiE_insert_eq: "Pi\<^sub>E (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
1.49  proof -
1.50    {
1.51 -    fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
1.52 -    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.53 +    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<notin> S"
1.54 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
1.55        by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
1.56    }
1.57    moreover
1.58    {
1.59 -    fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
1.60 -    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
1.61 +    fix f assume "f \<in> Pi\<^sub>E (insert x S) T" "x \<in> S"
1.62 +    then have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> Pi\<^sub>E S T)"
1.63        by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
1.64    }
1.65    ultimately show ?thesis
1.66 @@ -422,25 +424,25 @@
1.67    unfolding PiE_def by (auto simp: Pi_cong)
1.68
1.69  lemma PiE_E [elim]:
1.70 -  assumes "f \<in> PiE A B"
1.71 +  assumes "f \<in> Pi\<^sub>E A B"
1.72    obtains "x \<in> A" and "f x \<in> B x"
1.73      | "x \<notin> A" and "f x = undefined"
1.74    using assms by (auto simp: Pi_def PiE_def extensional_def)
1.75
1.76  lemma PiE_I[intro!]:
1.77 -  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> PiE A B"
1.78 +  "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> B x) \<Longrightarrow> (\<And>x. x \<notin> A \<Longrightarrow> f x = undefined) \<Longrightarrow> f \<in> Pi\<^sub>E A B"
1.79    by (simp add: PiE_def extensional_def)
1.80
1.81 -lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> PiE A B \<subseteq> PiE A C"
1.82 +lemma PiE_mono: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C x) \<Longrightarrow> Pi\<^sub>E A B \<subseteq> Pi\<^sub>E A C"
1.83    by auto
1.84
1.85 -lemma PiE_iff: "f \<in> PiE I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
1.86 +lemma PiE_iff: "f \<in> Pi\<^sub>E I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i) \<and> f \<in> extensional I"
1.87    by (simp add: PiE_def Pi_iff)
1.88
1.89 -lemma PiE_restrict[simp]:  "f \<in> PiE A B \<Longrightarrow> restrict f A = f"
1.90 +lemma PiE_restrict[simp]:  "f \<in> Pi\<^sub>E A B \<Longrightarrow> restrict f A = f"
1.91    by (simp add: extensional_restrict PiE_def)
1.92
1.93 -lemma restrict_PiE[simp]: "restrict f I \<in> PiE I S \<longleftrightarrow> f \<in> Pi I S"
1.94 +lemma restrict_PiE[simp]: "restrict f I \<in> Pi\<^sub>E I S \<longleftrightarrow> f \<in> Pi I S"
1.95    by (auto simp: PiE_iff)
1.96
1.97  lemma PiE_eq_subset:
```