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.16    by (simp add: PiE_def)
    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: