# HG changeset patch
# User huffman
# Date 1290891312 28800
# Node ID 6023808b38d4b04a81661a8986ba30c897816a6a
# Parent  3af9b0df3521b3c18e7cd34586f4339cdbd608f5
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo

diff -r 3af9b0df3521 -r 6023808b38d4 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Sat Nov 27 12:38:02 2010 -0800
+++ b/src/HOLCF/Cfun.thy	Sat Nov 27 12:55:12 2010 -0800
@@ -264,7 +264,7 @@
 lemma contlub_LAM:
   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
     \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
-apply (simp add: thelub_cfun)
+apply (simp add: lub_cfun)
 apply (simp add: Abs_cfun_inverse2)
 apply (simp add: thelub_fun ch2ch_lambda)
 done
diff -r 3af9b0df3521 -r 6023808b38d4 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Sat Nov 27 12:38:02 2010 -0800
+++ b/src/HOLCF/Pcpodef.thy	Sat Nov 27 12:55:12 2010 -0800
@@ -91,7 +91,7 @@
  apply (rule type_definition.Rep [OF type])
 done
 
-theorem typedef_lub:
+theorem typedef_is_lub:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs A"
     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
@@ -107,7 +107,7 @@
     by (rule typedef_is_lubI [OF below])
 qed
 
-lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
+lemmas typedef_lub = typedef_is_lub [THEN thelubI, standard]
 
 theorem typedef_cpo:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
@@ -118,7 +118,7 @@
 proof
   fix S::"nat \<Rightarrow> 'b" assume "chain S"
   hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
-    by (rule typedef_lub [OF type below adm])
+    by (rule typedef_is_lub [OF type below adm])
   thus "\<exists>x. range S <<| x" ..
 qed
 
@@ -133,7 +133,7 @@
     and adm: "adm (\<lambda>x. x \<in> A)"
   shows "cont Rep"
  apply (rule contI)
- apply (simp only: typedef_thelub [OF type below adm])
+ apply (simp only: typedef_lub [OF type below adm])
  apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
  apply (rule cpo_lubI)
  apply (erule ch2ch_Rep [OF below])
diff -r 3af9b0df3521 -r 6023808b38d4 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Sat Nov 27 12:38:02 2010 -0800
+++ b/src/HOLCF/Tools/pcpodef.ML	Sat Nov 27 12:55:12 2010 -0800
@@ -9,7 +9,7 @@
 sig
   type cpo_info =
     { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
-      lub: thm, thelub: thm, compact: thm }
+      is_lub: thm, lub: thm, compact: thm }
   type pcpo_info =
     { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
       Rep_defined: thm, Abs_defined: thm }
@@ -45,7 +45,7 @@
 
 type cpo_info =
   { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
-    lub: thm, thelub: thm, compact: thm }
+    is_lub: thm, lub: thm, compact: thm }
 
 type pcpo_info =
   { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm,
@@ -94,8 +94,8 @@
     fun make thm = Drule.zero_var_indexes (thm OF cpo_thms');
     val cont_Rep = make @{thm typedef_cont_Rep};
     val cont_Abs = make @{thm typedef_cont_Abs};
+    val is_lub = make @{thm typedef_is_lub};
     val lub = make @{thm typedef_lub};
-    val thelub = make @{thm typedef_thelub};
     val compact = make @{thm typedef_compact};
     val (_, thy) =
       thy
@@ -104,13 +104,13 @@
         ([((Binding.prefix_name "adm_"      name, admissible'), []),
           ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
           ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
+          ((Binding.prefix_name "is_lub_"   name, is_lub     ), []),
           ((Binding.prefix_name "lub_"      name, lub        ), []),
-          ((Binding.prefix_name "thelub_"   name, thelub     ), []),
           ((Binding.prefix_name "compact_"  name, compact    ), [])])
       ||> Sign.parent_path;
     val cpo_info : cpo_info =
       { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
-        cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
+        cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact };
   in
     (cpo_info, thy)
   end;