# HG changeset patch
# User ballarin
# Date 1504208883 -7200
# Node ID e5b1d4d55bf623897da7425cb3e9b0625a883c64
# Parent  2db3fe23fdaff76cfafc7d59d9a1c1eb03936f16
Avoid \mu and \nu as constant syntax, use LFP and GFP instead.

diff -r 2db3fe23fdaf -r e5b1d4d55bf6 src/HOL/Algebra/Complete_Lattice.thy
--- a/src/HOL/Algebra/Complete_Lattice.thy	Thu Aug 31 21:48:01 2017 +0200
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Thu Aug 31 21:48:03 2017 +0200
@@ -375,23 +375,23 @@
 subsubsection \<open>Least fixed points\<close>
 
 lemma LFP_closed [intro, simp]:
-  "\<mu> f \<in> carrier L"
-  by (metis (lifting) LFP_def inf_closed mem_Collect_eq subsetI)
+  "LFP f \<in> carrier L"
+  by (metis (lifting) LEAST_FP_def inf_closed mem_Collect_eq subsetI)
 
 lemma LFP_lowerbound: 
   assumes "x \<in> carrier L" "f x \<sqsubseteq> x" 
-  shows "\<mu> f \<sqsubseteq> x"
-  by (auto intro:inf_lower assms simp add:LFP_def)
+  shows "LFP f \<sqsubseteq> x"
+  by (auto intro:inf_lower assms simp add:LEAST_FP_def)
 
 lemma LFP_greatest: 
   assumes "x \<in> carrier L" 
           "(\<And>u. \<lbrakk> u \<in> carrier L; f u \<sqsubseteq> u \<rbrakk> \<Longrightarrow> x \<sqsubseteq> u)"
-  shows "x \<sqsubseteq> \<mu> f"
-  by (auto simp add:LFP_def intro:inf_greatest assms)
+  shows "x \<sqsubseteq> LFP f"
+  by (auto simp add:LEAST_FP_def intro:inf_greatest assms)
 
 lemma LFP_lemma2: 
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
-  shows "f (\<mu> f) \<sqsubseteq> \<mu> f"
+  shows "f (LFP f) \<sqsubseteq> LFP f"
   using assms
   apply (auto simp add:Pi_def)
   apply (rule LFP_greatest)
@@ -401,21 +401,21 @@
 
 lemma LFP_lemma3: 
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
-  shows "\<mu> f \<sqsubseteq> f (\<mu> f)"
+  shows "LFP f \<sqsubseteq> f (LFP f)"
   using assms
   apply (auto simp add:Pi_def)
   apply (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
 done
 
 lemma LFP_weak_unfold: 
-  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<mu> f .= f (\<mu> f)"
+  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f .= f (LFP f)"
   by (auto intro: LFP_lemma2 LFP_lemma3 funcset_mem)
 
 lemma LFP_fixed_point [intro]:
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
-  shows "\<mu> f \<in> fps L f"
+  shows "LFP f \<in> fps L f"
 proof -
-  have "f (\<mu> f) \<in> carrier L"
+  have "f (LFP f) \<in> carrier L"
     using assms(2) by blast
   with assms show ?thesis
     by (simp add: LFP_weak_unfold fps_def local.sym)
@@ -423,18 +423,18 @@
 
 lemma LFP_least_fixed_point:
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"
-  shows "\<mu> f \<sqsubseteq> x"
+  shows "LFP f \<sqsubseteq> x"
   using assms by (force intro: LFP_lowerbound simp add: fps_def)
   
 lemma LFP_idem: 
   assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"
-  shows "\<mu> f .= (f \<bottom>)"
+  shows "LFP f .= (f \<bottom>)"
 proof (rule weak_le_antisym)
   from assms(1) show fb: "f \<bottom> \<in> carrier L"
     by (rule funcset_mem, simp)
-  from assms show mf: "\<mu> f \<in> carrier L"
+  from assms show mf: "LFP f \<in> carrier L"
     by blast
-  show "\<mu> f \<sqsubseteq> f \<bottom>"
+  show "LFP f \<sqsubseteq> f \<bottom>"
   proof -
     have "f (f \<bottom>) .= f \<bottom>"
       by (auto simp add: fps_def fb assms(3) idempotent)
@@ -443,13 +443,13 @@
     ultimately show ?thesis
       by (auto intro: LFP_lowerbound simp add: fb)
   qed
-  show "f \<bottom> \<sqsubseteq> \<mu> f"
+  show "f \<bottom> \<sqsubseteq> LFP f"
   proof -
-    have "f \<bottom> \<sqsubseteq> f (\<mu> f)"
+    have "f \<bottom> \<sqsubseteq> f (LFP f)"
       by (auto intro: use_iso1[of _ f] simp add: assms)
-    moreover have "... .= \<mu> f"
+    moreover have "... .= LFP f"
       using assms(1) assms(2) fps_def by force
-    moreover from assms(1) have "f (\<mu> f) \<in> carrier L"
+    moreover from assms(1) have "f (LFP f) \<in> carrier L"
       by (auto)
     ultimately show ?thesis
       using fb by blast
@@ -460,23 +460,23 @@
 subsubsection \<open>Greatest fixed points\<close>
   
 lemma GFP_closed [intro, simp]:
-  "\<nu> f \<in> carrier L"
-  by (auto intro:sup_closed simp add:GFP_def)
+  "GFP f \<in> carrier L"
+  by (auto intro:sup_closed simp add:GREATEST_FP_def)
   
 lemma GFP_upperbound:
   assumes "x \<in> carrier L" "x \<sqsubseteq> f x"
-  shows "x \<sqsubseteq> \<nu> f"
-  by (auto intro:sup_upper assms simp add:GFP_def)
+  shows "x \<sqsubseteq> GFP f"
+  by (auto intro:sup_upper assms simp add:GREATEST_FP_def)
 
 lemma GFP_least: 
   assumes "x \<in> carrier L" 
           "(\<And>u. \<lbrakk> u \<in> carrier L; u \<sqsubseteq> f u \<rbrakk> \<Longrightarrow> u \<sqsubseteq> x)"
-  shows "\<nu> f \<sqsubseteq> x"
-  by (auto simp add:GFP_def intro:sup_least assms)
+  shows "GFP f \<sqsubseteq> x"
+  by (auto simp add:GREATEST_FP_def intro:sup_least assms)
 
 lemma GFP_lemma2:
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
-  shows "\<nu> f \<sqsubseteq> f (\<nu> f)"
+  shows "GFP f \<sqsubseteq> f (GFP f)"
   using assms
   apply (auto simp add:Pi_def)
   apply (rule GFP_least)
@@ -486,19 +486,19 @@
 
 lemma GFP_lemma3:
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
-  shows "f (\<nu> f) \<sqsubseteq> \<nu> f"
+  shows "f (GFP f) \<sqsubseteq> GFP f"
   by (metis GFP_closed GFP_lemma2 GFP_upperbound assms funcset_mem use_iso2)
   
 lemma GFP_weak_unfold: 
-  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<nu> f .= f (\<nu> f)"
+  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> GFP f .= f (GFP f)"
   by (auto intro: GFP_lemma2 GFP_lemma3 funcset_mem)
 
 lemma (in weak_complete_lattice) GFP_fixed_point [intro]:
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
-  shows "\<nu> f \<in> fps L f"
+  shows "GFP f \<in> fps L f"
   using assms
 proof -
-  have "f (\<nu> f) \<in> carrier L"
+  have "f (GFP f) \<in> carrier L"
     using assms(2) by blast
   with assms show ?thesis
     by (simp add: GFP_weak_unfold fps_def local.sym)
@@ -506,19 +506,19 @@
 
 lemma GFP_greatest_fixed_point:
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L" "x \<in> fps L f"
-  shows "x \<sqsubseteq> \<nu> f"
+  shows "x \<sqsubseteq> GFP f"
   using assms 
   by (rule_tac GFP_upperbound, auto simp add: fps_def, meson PiE local.sym weak_refl)
     
 lemma GFP_idem: 
   assumes "f \<in> carrier L \<rightarrow> carrier L" "Mono f" "Idem f"
-  shows "\<nu> f .= (f \<top>)"
+  shows "GFP f .= (f \<top>)"
 proof (rule weak_le_antisym)
   from assms(1) show fb: "f \<top> \<in> carrier L"
     by (rule funcset_mem, simp)
-  from assms show mf: "\<nu> f \<in> carrier L"
+  from assms show mf: "GFP f \<in> carrier L"
     by blast
-  show "f \<top> \<sqsubseteq> \<nu> f"
+  show "f \<top> \<sqsubseteq> GFP f"
   proof -
     have "f (f \<top>) .= f \<top>"
       by (auto simp add: fps_def fb assms(3) idempotent)
@@ -527,13 +527,13 @@
     ultimately show ?thesis
       by (rule_tac GFP_upperbound, simp_all add: fb local.sym)
   qed
-  show "\<nu> f \<sqsubseteq> f \<top>"
+  show "GFP f \<sqsubseteq> f \<top>"
   proof -
-    have "\<nu> f \<sqsubseteq> f (\<nu> f)"
+    have "GFP f \<sqsubseteq> f (GFP f)"
       by (simp add: GFP_lemma2 assms(1) assms(2))
     moreover have "... \<sqsubseteq> f \<top>"
       by (auto intro: use_iso1[of _ f] simp add: assms)
-    moreover from assms(1) have "f (\<nu> f) \<in> carrier L"
+    moreover from assms(1) have "f (GFP f) \<in> carrier L"
       by (auto)
     ultimately show ?thesis
       using fb local.le_trans by blast
@@ -635,27 +635,27 @@
 begin
 
 lemma LFP_unfold: 
-  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<mu> f = f (\<mu> f)"
+  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f = f (LFP f)"
   using eq_is_equal weak.LFP_weak_unfold by auto
 
 lemma LFP_const:
-  "t \<in> carrier L \<Longrightarrow> \<mu> (\<lambda> x. t) = t"
+  "t \<in> carrier L \<Longrightarrow> LFP (\<lambda> x. t) = t"
   by (simp add: local.le_antisym weak.LFP_greatest weak.LFP_lowerbound)
 
 lemma LFP_id:
-  "\<mu> id = \<bottom>"
+  "LFP id = \<bottom>"
   by (simp add: local.le_antisym weak.LFP_lowerbound)
 
 lemma GFP_unfold:
-  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> \<nu> f = f (\<nu> f)"
+  "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> GFP f = f (GFP f)"
   using eq_is_equal weak.GFP_weak_unfold by auto
 
 lemma GFP_const:
-  "t \<in> carrier L \<Longrightarrow> \<nu> (\<lambda> x. t) = t"
+  "t \<in> carrier L \<Longrightarrow> GFP (\<lambda> x. t) = t"
   by (simp add: local.le_antisym weak.GFP_least weak.GFP_upperbound)
 
 lemma GFP_id:
-  "\<nu> id = \<top>"
+  "GFP id = \<top>"
   using weak.GFP_upperbound by auto
 
 end
@@ -834,11 +834,11 @@
 
       let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"
 
-      show "is_lub ?L'' (\<mu>\<^bsub>?L'\<^esub> f) A"
+      show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"
       proof (rule least_UpperI, simp_all)
         fix x
         assume "x \<in> Upper ?L'' A"
-        hence "\<mu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
+        hence "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
           apply (rule_tac L'.LFP_lowerbound)
           apply (auto simp add: Upper_def)
           apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)          
@@ -846,14 +846,14 @@
           apply (auto)
           apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))
         done
-        thus " \<mu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
+        thus " LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
           by (simp)
       next
         fix x
         assume xA: "x \<in> A"
-        show "x \<sqsubseteq>\<^bsub>L\<^esub> \<mu>\<^bsub>?L'\<^esub> f"
+        show "x \<sqsubseteq>\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
         proof -
-          have "\<mu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
+          have "LFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
             by blast
           thus ?thesis
             by (simp, meson AL L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed L.sup_upper xA subsetCE)
@@ -862,13 +862,13 @@
         show "A \<subseteq> fps L f"
           by (simp add: A)
       next
-        show "\<mu>\<^bsub>?L'\<^esub> f \<in> fps L f"
+        show "LFP\<^bsub>?L'\<^esub> f \<in> fps L f"
         proof (auto simp add: fps_def)
-          have "\<mu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
+          have "LFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
             by (rule L'.LFP_closed)
-          thus c:"\<mu>\<^bsub>?L'\<^esub> f \<in> carrier L"
+          thus c:"LFP\<^bsub>?L'\<^esub> f \<in> carrier L"
              by (auto simp add: at_least_at_most_def)
-          have "\<mu>\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (\<mu>\<^bsub>?L'\<^esub> f)"
+          have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"
           proof (rule "L'.LFP_weak_unfold", simp_all)
             show "f \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
               apply (auto simp add: Pi_def at_least_at_most_def)
@@ -882,7 +882,7 @@
               apply (meson L.at_least_at_most_closed subsetCE)
             done
           qed
-          thus "f (\<mu>\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> \<mu>\<^bsub>?L'\<^esub> f"
+          thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
             by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
         qed
       qed
@@ -933,24 +933,24 @@
 
       let ?L'' = "L\<lparr> carrier := fps L f \<rparr>"
 
-      show "is_glb ?L'' (\<nu>\<^bsub>?L'\<^esub> f) A"
+      show "is_glb ?L'' (GFP\<^bsub>?L'\<^esub> f) A"
       proof (rule greatest_LowerI, simp_all)
         fix x
         assume "x \<in> Lower ?L'' A"
-        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
+        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
           apply (rule_tac L'.GFP_upperbound)
           apply (auto simp add: Lower_def)
           apply (meson A AL L.at_least_at_most_member L.bottom_lower L.weak_complete_lattice_axioms fps_carrier subsetCE weak_complete_lattice.inf_greatest)
           apply (simp add: funcset_carrier' L.sym assms(2) fps_def)          
         done
-        thus "x \<sqsubseteq>\<^bsub>L\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
+        thus "x \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
           by (simp)
       next
         fix x
         assume xA: "x \<in> A"
-        show "\<nu>\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
+        show "GFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
         proof -
-          have "\<nu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
+          have "GFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
             by blast
           thus ?thesis
             by (simp, meson AL L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.inf_lower L.le_trans subsetCE xA)     
@@ -959,13 +959,13 @@
         show "A \<subseteq> fps L f"
           by (simp add: A)
       next
-        show "\<nu>\<^bsub>?L'\<^esub> f \<in> fps L f"
+        show "GFP\<^bsub>?L'\<^esub> f \<in> fps L f"
         proof (auto simp add: fps_def)
-          have "\<nu>\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
+          have "GFP\<^bsub>?L'\<^esub> f \<in> carrier ?L'"
             by (rule L'.GFP_closed)
-          thus c:"\<nu>\<^bsub>?L'\<^esub> f \<in> carrier L"
+          thus c:"GFP\<^bsub>?L'\<^esub> f \<in> carrier L"
              by (auto simp add: at_least_at_most_def)
-          have "\<nu>\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (\<nu>\<^bsub>?L'\<^esub> f)"
+          have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"
           proof (rule "L'.GFP_weak_unfold", simp_all)
             show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
               apply (auto simp add: Pi_def at_least_at_most_def)
@@ -979,7 +979,7 @@
               using L.at_least_at_most_closed apply (blast intro: funcset_carrier')
             done
           qed
-          thus "f (\<nu>\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> \<nu>\<^bsub>?L'\<^esub> f"
+          thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
             by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym) 
         qed
       qed
@@ -989,7 +989,7 @@
 
 theorem Knaster_Tarski_top:
   assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"
-  shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> \<nu>\<^bsub>L\<^esub> f"
+  shows "\<top>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"
 proof -
   interpret L: weak_complete_lattice L
     by (simp add: assms)
@@ -997,15 +997,15 @@
     by (rule Knaster_Tarski, simp_all add: assms)
   show ?thesis
   proof (rule L.weak_le_antisym, simp_all)
-    show "\<top>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> \<nu>\<^bsub>L\<^esub> f"
+    show "\<top>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>L\<^esub> f"
       by (rule L.GFP_greatest_fixed_point, simp_all add: assms L'.top_closed[simplified])
-    show "\<nu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
+    show "GFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
     proof -
-      have "\<nu>\<^bsub>L\<^esub> f \<in> fps L f"
+      have "GFP\<^bsub>L\<^esub> f \<in> fps L f"
         by (rule L.GFP_fixed_point, simp_all add: assms)
-      hence "\<nu>\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
+      hence "GFP\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
         by simp
-      hence "\<nu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
+      hence "GFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<top>\<^bsub>fpl L f\<^esub>"
         by (rule L'.top_higher)
       thus ?thesis
         by simp
@@ -1022,7 +1022,7 @@
 
 theorem Knaster_Tarski_bottom:
   assumes "weak_complete_lattice L" "isotone L L f" "f \<in> carrier L \<rightarrow> carrier L"
-  shows "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> \<mu>\<^bsub>L\<^esub> f"
+  shows "\<bottom>\<^bsub>fpl L f\<^esub> .=\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"
 proof -
   interpret L: weak_complete_lattice L
     by (simp add: assms)
@@ -1030,15 +1030,15 @@
     by (rule Knaster_Tarski, simp_all add: assms)
   show ?thesis
   proof (rule L.weak_le_antisym, simp_all)
-    show "\<mu>\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<bottom>\<^bsub>fpl L f\<^esub>"
+    show "LFP\<^bsub>L\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> \<bottom>\<^bsub>fpl L f\<^esub>"
       by (rule L.LFP_least_fixed_point, simp_all add: assms L'.bottom_closed[simplified])
-    show "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> \<mu>\<^bsub>L\<^esub> f"
+    show "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> LFP\<^bsub>L\<^esub> f"
     proof -
-      have "\<mu>\<^bsub>L\<^esub> f \<in> fps L f"
+      have "LFP\<^bsub>L\<^esub> f \<in> fps L f"
         by (rule L.LFP_fixed_point, simp_all add: assms)
-      hence "\<mu>\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
+      hence "LFP\<^bsub>L\<^esub> f \<in> carrier (fpl L f)"
         by simp
-      hence "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>fpl L f\<^esub> \<mu>\<^bsub>L\<^esub> f"
+      hence "\<bottom>\<^bsub>fpl L f\<^esub> \<sqsubseteq>\<^bsub>fpl L f\<^esub> LFP\<^bsub>L\<^esub> f"
         by (rule L'.bottom_lower)
       thus ?thesis
         by simp
diff -r 2db3fe23fdaf -r e5b1d4d55bf6 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Thu Aug 31 21:48:01 2017 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Thu Aug 31 21:48:03 2017 +0200
@@ -51,12 +51,12 @@
   where "x \<sqinter>\<^bsub>L\<^esub> y = \<Sqinter>\<^bsub>L\<^esub>{x, y}"
 
 definition
-  LFP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<mu>\<index>") where
-  "LFP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    --\<open>least fixed point\<close>
+  LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where
+  "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    --\<open>least fixed point\<close>
 
 definition
-  GFP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("\<nu>\<index>") where
-  "GFP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    --\<open>greatest fixed point\<close>
+  GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where
+  "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    --\<open>greatest fixed point\<close>
 
 
 subsection \<open>Dual operators\<close>
@@ -86,12 +86,12 @@
   by (simp add: top_def bottom_def)
 
 lemma LFP_dual [simp]:
-  "LFP (inv_gorder L) f = GFP L f"
-  by (simp add:LFP_def GFP_def)
+  "LEAST_FP (inv_gorder L) f = GREATEST_FP L f"
+  by (simp add:LEAST_FP_def GREATEST_FP_def)
 
 lemma GFP_dual [simp]:
-  "GFP (inv_gorder L) f = LFP L f"
-  by (simp add:LFP_def GFP_def)
+  "GREATEST_FP (inv_gorder L) f = LEAST_FP L f"
+  by (simp add:LEAST_FP_def GREATEST_FP_def)
 
 
 subsection \<open>Lattices\<close>