# HG changeset patch
# User huffman
# Date 1293071044 28800
# Node ID 51c866d1b53b3d9ff54e590ea32b0ef490f9f41c
# Parent  17bf4ddd0833d7e8f1501c6c2f442739d7bd9ede
rename function ideal_completion.basis_fun to ideal_completion.extension

diff -r 17bf4ddd0833 -r 51c866d1b53b src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/Algebraic.thy	Wed Dec 22 18:24:04 2010 -0800
@@ -152,12 +152,12 @@
 definition
   cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
 where
-  "cast = defl.basis_fun Rep_fin_defl"
+  "cast = defl.extension Rep_fin_defl"
 
 lemma cast_defl_principal:
   "cast\<cdot>(defl_principal a) = Rep_fin_defl a"
 unfolding cast_def
-apply (rule defl.basis_fun_principal)
+apply (rule defl.extension_principal)
 apply (simp only: below_fin_defl_def)
 done
 
@@ -219,14 +219,14 @@
 
 definition
   "defl_fun1 e p f =
-    defl.basis_fun (\<lambda>a.
+    defl.extension (\<lambda>a.
       defl_principal (Abs_fin_defl
         (e oo f\<cdot>(Rep_fin_defl a) oo p)))"
 
 definition
   "defl_fun2 e p f =
-    defl.basis_fun (\<lambda>a.
-      defl.basis_fun (\<lambda>b.
+    defl.extension (\<lambda>a.
+      defl.extension (\<lambda>b.
         defl_principal (Abs_fin_defl
           (e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"
 
@@ -242,8 +242,8 @@
   show ?thesis
     by (induct A rule: defl.principal_induct, simp)
        (simp only: defl_fun1_def
-                   defl.basis_fun_principal
-                   defl.basis_fun_mono
+                   defl.extension_principal
+                   defl.extension_mono
                    defl.principal_mono
                    Abs_fin_defl_mono [OF 1 1]
                    monofun_cfun below_refl
@@ -267,8 +267,8 @@
     apply (induct A rule: defl.principal_induct, simp)
     apply (induct B rule: defl.principal_induct, simp)
     by (simp only: defl_fun2_def
-                   defl.basis_fun_principal
-                   defl.basis_fun_mono
+                   defl.extension_principal
+                   defl.extension_mono
                    defl.principal_mono
                    Abs_fin_defl_mono [OF 1 1]
                    monofun_cfun below_refl
diff -r 17bf4ddd0833 -r 51c866d1b53b src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/Completion.thy	Wed Dec 22 18:24:04 2010 -0800
@@ -291,10 +291,10 @@
 subsection {* Defining functions in terms of basis elements *}
 
 definition
-  basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
-  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
+  extension :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
+  "extension = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
 
-lemma basis_fun_lemma:
+lemma extension_lemma:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "\<exists>u. f ` rep x <<| u"
@@ -320,14 +320,14 @@
   thus ?thesis ..
 qed
 
-lemma basis_fun_beta:
+lemma extension_beta:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
-  shows "basis_fun f\<cdot>x = lub (f ` rep x)"
-unfolding basis_fun_def
+  shows "extension f\<cdot>x = lub (f ` rep x)"
+unfolding extension_def
 proof (rule beta_cfun)
   have lub: "\<And>x. \<exists>u. f ` rep x <<| u"
-    using f_mono by (rule basis_fun_lemma)
+    using f_mono by (rule extension_lemma)
   show cont: "cont (\<lambda>x. lub (f ` rep x))"
     apply (rule contI2)
      apply (rule monofunI)
@@ -341,11 +341,11 @@
     done
 qed
 
-lemma basis_fun_principal:
+lemma extension_principal:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
-  shows "basis_fun f\<cdot>(principal a) = f a"
-apply (subst basis_fun_beta, erule f_mono)
+  shows "extension f\<cdot>(principal a) = f a"
+apply (subst extension_beta, erule f_mono)
 apply (subst rep_principal)
 apply (rule lub_eqI)
 apply (rule is_lub_maximal)
@@ -355,34 +355,34 @@
 apply (simp add: r_refl)
 done
 
-lemma basis_fun_mono:
+lemma extension_mono:
   assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
   assumes below: "\<And>a. f a \<sqsubseteq> g a"
-  shows "basis_fun f \<sqsubseteq> basis_fun g"
+  shows "extension f \<sqsubseteq> extension g"
  apply (rule cfun_belowI)
- apply (simp only: basis_fun_beta f_mono g_mono)
+ apply (simp only: extension_beta f_mono g_mono)
  apply (rule is_lub_thelub_ex)
-  apply (rule basis_fun_lemma, erule f_mono)
+  apply (rule extension_lemma, erule f_mono)
  apply (rule ub_imageI, rename_tac a)
  apply (rule below_trans [OF below])
  apply (rule is_ub_thelub_ex)
-  apply (rule basis_fun_lemma, erule g_mono)
+  apply (rule extension_lemma, erule g_mono)
  apply (erule imageI)
 done
 
-lemma cont_basis_fun:
+lemma cont_extension:
   assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b"
   assumes f_cont: "\<And>a. cont (\<lambda>x. f x a)"
-  shows "cont (\<lambda>x. basis_fun (\<lambda>a. f x a))"
+  shows "cont (\<lambda>x. extension (\<lambda>a. f x a))"
  apply (rule contI2)
   apply (rule monofunI)
-  apply (rule basis_fun_mono, erule f_mono, erule f_mono)
+  apply (rule extension_mono, erule f_mono, erule f_mono)
   apply (erule cont2monofunE [OF f_cont])
  apply (rule cfun_belowI)
  apply (rule principal_induct, simp)
  apply (simp only: contlub_cfun_fun)
- apply (simp only: basis_fun_principal f_mono)
+ apply (simp only: extension_principal f_mono)
  apply (simp add: cont2contlubE [OF f_cont])
 done
 
diff -r 17bf4ddd0833 -r 51c866d1b53b src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 22 18:24:04 2010 -0800
@@ -168,11 +168,11 @@
 
 definition
   convex_unit :: "'a \<rightarrow> 'a convex_pd" where
-  "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
+  "convex_unit = compact_basis.extension (\<lambda>a. convex_principal (PDUnit a))"
 
 definition
   convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
-  "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
+  "convex_plus = convex_pd.extension (\<lambda>t. convex_pd.extension (\<lambda>u.
       convex_principal (PDPlus t u)))"
 
 abbreviation
@@ -190,13 +190,13 @@
 lemma convex_unit_Rep_compact_basis [simp]:
   "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
 unfolding convex_unit_def
-by (simp add: compact_basis.basis_fun_principal PDUnit_convex_mono)
+by (simp add: compact_basis.extension_principal PDUnit_convex_mono)
 
 lemma convex_plus_principal [simp]:
   "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
 unfolding convex_plus_def
-by (simp add: convex_pd.basis_fun_principal
-    convex_pd.basis_fun_mono PDPlus_convex_mono)
+by (simp add: convex_pd.extension_principal
+    convex_pd.extension_mono PDPlus_convex_mono)
 
 interpretation convex_add: semilattice convex_add proof
   fix xs ys zs :: "'a convex_pd"
@@ -342,7 +342,7 @@
 
 definition
   convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
-  "convex_bind = convex_pd.basis_fun convex_bind_basis"
+  "convex_bind = convex_pd.extension convex_bind_basis"
 
 syntax
   "_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
@@ -354,7 +354,7 @@
 lemma convex_bind_principal [simp]:
   "convex_bind\<cdot>(convex_principal t) = convex_bind_basis t"
 unfolding convex_bind_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
 apply (erule convex_bind_basis_mono)
 done
 
@@ -521,12 +521,12 @@
 
 definition
   convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where
-  "convex_to_upper = convex_pd.basis_fun upper_principal"
+  "convex_to_upper = convex_pd.extension upper_principal"
 
 lemma convex_to_upper_principal [simp]:
   "convex_to_upper\<cdot>(convex_principal t) = upper_principal t"
 unfolding convex_to_upper_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
 apply (rule upper_pd.principal_mono)
 apply (erule convex_le_imp_upper_le)
 done
@@ -560,12 +560,12 @@
 
 definition
   convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where
-  "convex_to_lower = convex_pd.basis_fun lower_principal"
+  "convex_to_lower = convex_pd.extension lower_principal"
 
 lemma convex_to_lower_principal [simp]:
   "convex_to_lower\<cdot>(convex_principal t) = lower_principal t"
 unfolding convex_to_lower_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
 apply (rule lower_pd.principal_mono)
 apply (erule convex_le_imp_lower_le)
 done
diff -r 17bf4ddd0833 -r 51c866d1b53b src/HOL/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Wed Dec 22 18:24:04 2010 -0800
@@ -569,18 +569,18 @@
 definition
   defl_approx :: "nat \<Rightarrow> 'a defl \<rightarrow> 'a defl"
 where
-  "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
+  "defl_approx = (\<lambda>i. defl.extension (\<lambda>d. defl_principal (fd_take i d)))"
 
 lemma defl_approx_principal:
   "defl_approx i\<cdot>(defl_principal d) = defl_principal (fd_take i d)"
 unfolding defl_approx_def
-by (simp add: defl.basis_fun_principal fd_take_mono)
+by (simp add: defl.extension_principal fd_take_mono)
 
 lemma defl_approx: "approx_chain defl_approx"
 proof
   show chain: "chain defl_approx"
     unfolding defl_approx_def
-    by (simp add: chainI defl.basis_fun_mono fd_take_mono fd_take_chain)
+    by (simp add: chainI defl.extension_mono fd_take_mono fd_take_chain)
   show idem: "\<And>i x. defl_approx i\<cdot>(defl_approx i\<cdot>x) = defl_approx i\<cdot>x"
     apply (induct_tac x rule: defl.principal_induct, simp)
     apply (simp add: defl_approx_principal fd_take_idem)
@@ -594,7 +594,7 @@
     apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
     apply (induct_tac x rule: defl.principal_induct, simp)
     apply (simp add: contlub_cfun_fun chain)
-    apply (simp add: compact_below_lub_iff defl.compact_principal chain)
+    apply (simp add: compact_below_lub_iff chain)
     apply (simp add: defl_approx_principal)
     apply (subgoal_tac "\<exists>i. fd_take i a = a", metis below_refl)
     apply (rule fd_take_covers)
diff -r 17bf4ddd0833 -r 51c866d1b53b src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Wed Dec 22 18:24:04 2010 -0800
@@ -123,11 +123,11 @@
 
 definition
   lower_unit :: "'a \<rightarrow> 'a lower_pd" where
-  "lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))"
+  "lower_unit = compact_basis.extension (\<lambda>a. lower_principal (PDUnit a))"
 
 definition
   lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
-  "lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u.
+  "lower_plus = lower_pd.extension (\<lambda>t. lower_pd.extension (\<lambda>u.
       lower_principal (PDPlus t u)))"
 
 abbreviation
@@ -145,13 +145,13 @@
 lemma lower_unit_Rep_compact_basis [simp]:
   "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
 unfolding lower_unit_def
-by (simp add: compact_basis.basis_fun_principal PDUnit_lower_mono)
+by (simp add: compact_basis.extension_principal PDUnit_lower_mono)
 
 lemma lower_plus_principal [simp]:
   "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
 unfolding lower_plus_def
-by (simp add: lower_pd.basis_fun_principal
-    lower_pd.basis_fun_mono PDPlus_lower_mono)
+by (simp add: lower_pd.extension_principal
+    lower_pd.extension_mono PDPlus_lower_mono)
 
 interpretation lower_add: semilattice lower_add proof
   fix xs ys zs :: "'a lower_pd"
@@ -335,7 +335,7 @@
 
 definition
   lower_bind :: "'a lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
-  "lower_bind = lower_pd.basis_fun lower_bind_basis"
+  "lower_bind = lower_pd.extension lower_bind_basis"
 
 syntax
   "_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
@@ -347,7 +347,7 @@
 lemma lower_bind_principal [simp]:
   "lower_bind\<cdot>(lower_principal t) = lower_bind_basis t"
 unfolding lower_bind_def
-apply (rule lower_pd.basis_fun_principal)
+apply (rule lower_pd.extension_principal)
 apply (erule lower_bind_basis_mono)
 done
 
diff -r 17bf4ddd0833 -r 51c866d1b53b src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 22 18:24:04 2010 -0800
@@ -856,17 +856,17 @@
 definition
   udom_emb :: "'a \<rightarrow> udom"
 where
-  "udom_emb = compact_basis.basis_fun (\<lambda>x. udom_principal (basis_emb x))"
+  "udom_emb = compact_basis.extension (\<lambda>x. udom_principal (basis_emb x))"
 
 definition
   udom_prj :: "udom \<rightarrow> 'a"
 where
-  "udom_prj = udom.basis_fun (\<lambda>x. Rep_compact_basis (basis_prj x))"
+  "udom_prj = udom.extension (\<lambda>x. Rep_compact_basis (basis_prj x))"
 
 lemma udom_emb_principal:
   "udom_emb\<cdot>(Rep_compact_basis x) = udom_principal (basis_emb x)"
 unfolding udom_emb_def
-apply (rule compact_basis.basis_fun_principal)
+apply (rule compact_basis.extension_principal)
 apply (rule udom.principal_mono)
 apply (erule basis_emb_mono)
 done
@@ -874,7 +874,7 @@
 lemma udom_prj_principal:
   "udom_prj\<cdot>(udom_principal x) = Rep_compact_basis (basis_prj x)"
 unfolding udom_prj_def
-apply (rule udom.basis_fun_principal)
+apply (rule udom.extension_principal)
 apply (rule compact_basis.principal_mono)
 apply (erule basis_prj_mono)
 done
@@ -903,7 +903,7 @@
   udom_approx :: "nat \<Rightarrow> udom \<rightarrow> udom"
 where
   "udom_approx i =
-    udom.basis_fun (\<lambda>x. udom_principal (ubasis_until (\<lambda>y. y \<le> i) x))"
+    udom.extension (\<lambda>x. udom_principal (ubasis_until (\<lambda>y. y \<le> i) x))"
 
 lemma udom_approx_mono:
   "ubasis_le a b \<Longrightarrow>
@@ -923,7 +923,7 @@
   "udom_approx i\<cdot>(udom_principal x) =
     udom_principal (ubasis_until (\<lambda>y. y \<le> i) x)"
 unfolding udom_approx_def
-apply (rule udom.basis_fun_principal)
+apply (rule udom.extension_principal)
 apply (erule udom_approx_mono)
 done
 
@@ -957,7 +957,7 @@
 lemma chain_udom_approx [simp]: "chain (\<lambda>i. udom_approx i)"
 unfolding udom_approx_def
 apply (rule chainI)
-apply (rule udom.basis_fun_mono)
+apply (rule udom.extension_mono)
 apply (erule udom_approx_mono)
 apply (erule udom_approx_mono)
 apply (rule udom.principal_mono)
diff -r 17bf4ddd0833 -r 51c866d1b53b src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Wed Dec 22 18:24:04 2010 -0800
@@ -121,11 +121,11 @@
 
 definition
   upper_unit :: "'a \<rightarrow> 'a upper_pd" where
-  "upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))"
+  "upper_unit = compact_basis.extension (\<lambda>a. upper_principal (PDUnit a))"
 
 definition
   upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
-  "upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u.
+  "upper_plus = upper_pd.extension (\<lambda>t. upper_pd.extension (\<lambda>u.
       upper_principal (PDPlus t u)))"
 
 abbreviation
@@ -143,13 +143,13 @@
 lemma upper_unit_Rep_compact_basis [simp]:
   "{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)"
 unfolding upper_unit_def
-by (simp add: compact_basis.basis_fun_principal PDUnit_upper_mono)
+by (simp add: compact_basis.extension_principal PDUnit_upper_mono)
 
 lemma upper_plus_principal [simp]:
   "upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
 unfolding upper_plus_def
-by (simp add: upper_pd.basis_fun_principal
-    upper_pd.basis_fun_mono PDPlus_upper_mono)
+by (simp add: upper_pd.extension_principal
+    upper_pd.extension_mono PDPlus_upper_mono)
 
 interpretation upper_add: semilattice upper_add proof
   fix xs ys zs :: "'a upper_pd"
@@ -330,7 +330,7 @@
 
 definition
   upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
-  "upper_bind = upper_pd.basis_fun upper_bind_basis"
+  "upper_bind = upper_pd.extension upper_bind_basis"
 
 syntax
   "_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
@@ -342,7 +342,7 @@
 lemma upper_bind_principal [simp]:
   "upper_bind\<cdot>(upper_principal t) = upper_bind_basis t"
 unfolding upper_bind_def
-apply (rule upper_pd.basis_fun_principal)
+apply (rule upper_pd.extension_principal)
 apply (erule upper_bind_basis_mono)
 done