# HG changeset patch
# User hoelzl
# Date 1302016251 -7200
# Node ID 461624ffd382a905f4c7f4af0a9c3ab1dd1bd47a
# Parent  e48baf91aeabfe1afe8ff93fa19b0695b2bd3450
Rename extensional to extensionalD (extensional is also defined in FuncSet)

diff -r e48baf91aeab -r 461624ffd382 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Apr 05 15:15:33 2011 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Apr 05 17:10:51 2011 +0200
@@ -95,11 +95,11 @@
 lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
   by auto
 
-definition extensional :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
-  "extensional d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
+definition extensionalD :: "'b \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
+  "extensionalD d A = {f. \<forall>x. x \<notin> A \<longrightarrow> f x = d}"
 
-lemma extensional_empty[simp]: "extensional d {} = {\<lambda>x. d}"
-  unfolding extensional_def by (simp add: set_eq_iff fun_eq_iff)
+lemma extensionalD_empty[simp]: "extensionalD d {} = {\<lambda>x. d}"
+  unfolding extensionalD_def by (simp add: set_eq_iff fun_eq_iff)
 
 lemma funset_eq_UN_fun_upd_I:
   assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
@@ -121,16 +121,16 @@
   from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
 qed
 
-lemma extensional_insert[simp]:
+lemma extensionalD_insert[simp]:
   assumes "a \<notin> A"
-  shows "extensional d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
+  shows "extensionalD d (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensionalD d A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
   apply (rule funset_eq_UN_fun_upd_I)
   using assms
-  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
+  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensionalD_def)
 
-lemma finite_extensional_funcset[simp, intro]:
+lemma finite_extensionalD_funcset[simp, intro]:
   assumes "finite A" "finite B"
-  shows "finite (extensional d A \<inter> (A \<rightarrow> B))"
+  shows "finite (extensionalD d A \<inter> (A \<rightarrow> B))"
   using assms by induct auto
 
 lemma fun_upd_eq_iff: "f(a := b) = g(a := b') \<longleftrightarrow> b = b' \<and> f(a := d) = g(a := d)"
@@ -138,27 +138,27 @@
 
 lemma card_funcset:
   assumes "finite A" "finite B"
-  shows "card (extensional d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
+  shows "card (extensionalD d A \<inter> (A \<rightarrow> B)) = card B ^ card A"
 using `finite A` proof induct
-  case (insert a A) thus ?case unfolding extensional_insert[OF `a \<notin> A`]
+  case (insert a A) thus ?case unfolding extensionalD_insert[OF `a \<notin> A`]
   proof (subst card_UN_disjoint, safe, simp_all)
-    show "finite (extensional d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
+    show "finite (extensionalD d A \<inter> (A \<rightarrow> B))" "\<And>f. finite (fun_upd f a ` B)"
       using `finite B` `finite A` by simp_all
   next
     fix f g b b' assume "f \<noteq> g" and eq: "f(a := b) = g(a := b')" and
-      ext: "f \<in> extensional d A" "g \<in> extensional d A"
+      ext: "f \<in> extensionalD d A" "g \<in> extensionalD d A"
     have "f a = d" "g a = d"
-      using ext `a \<notin> A` by (auto simp add: extensional_def)
+      using ext `a \<notin> A` by (auto simp add: extensionalD_def)
     with `f \<noteq> g` eq show False unfolding fun_upd_eq_iff[of _ _ b _ _ d]
       by (auto simp: fun_upd_idem fun_upd_eq_iff)
   next
-    { fix f assume "f \<in> extensional d A \<inter> (A \<rightarrow> B)"
+    { fix f assume "f \<in> extensionalD d A \<inter> (A \<rightarrow> B)"
       have "card (fun_upd f a ` B) = card B"
       proof (auto intro!: card_image inj_onI)
         fix b b' assume "f(a := b) = f(a := b')"
         from fun_upd_eq_iff[THEN iffD1, OF this] show "b = b'" by simp
       qed }
-    then show "(\<Sum>i\<in>extensional d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
+    then show "(\<Sum>i\<in>extensionalD d A \<inter> (A \<rightarrow> B). card (fun_upd i a ` B)) = card B * card B ^ card A"
       using insert by simp
   qed
 qed simp
@@ -301,11 +301,11 @@
 
 lemma card_T_bound: "card ((t\<circ>OB)`msgs) \<le> (n+1)^card observations"
 proof -
-  have "(t\<circ>OB)`msgs \<subseteq> extensional 0 observations \<inter> (observations \<rightarrow> {.. n})"
-    unfolding observations_def extensional_def OB_def msgs_def
+  have "(t\<circ>OB)`msgs \<subseteq> extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n})"
+    unfolding observations_def extensionalD_def OB_def msgs_def
     by (auto simp add: t_def comp_def image_iff)
-  with finite_extensional_funcset
-  have "card ((t\<circ>OB)`msgs) \<le> card (extensional 0 observations \<inter> (observations \<rightarrow> {.. n}))"
+  with finite_extensionalD_funcset
+  have "card ((t\<circ>OB)`msgs) \<le> card (extensionalD 0 observations \<inter> (observations \<rightarrow> {.. n}))"
     by (rule card_mono) auto
   also have "\<dots> = (n + 1) ^ card observations"
     by (subst card_funcset) auto