# HG changeset patch
# User nipkow
# Date 1325431973 -3600
# Node ID e81411bfa7efd6cccf497f432651655c15876a12
# Parent  d7eb081cf220ebda3193dcf709932efe0432f033
tuned argument order

diff -r d7eb081cf220 -r e81411bfa7ef src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Sun Jan 01 09:27:48 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sun Jan 01 16:32:53 2012 +0100
@@ -106,7 +106,7 @@
   have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
-  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
+  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
@@ -114,7 +114,7 @@
       show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
     qed
   qed
-  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
+  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c c'"
     by (blast intro: mono_gamma_c order_trans)
 qed
 
diff -r d7eb081cf220 -r e81411bfa7ef src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Sun Jan 01 09:27:48 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Sun Jan 01 16:32:53 2012 +0100
@@ -357,7 +357,7 @@
   have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
-  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
+  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
@@ -365,7 +365,7 @@
       show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
     qed
   qed
-  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
+  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c c'"
     by (blast intro: mono_gamma_c order_trans)
 qed
 
diff -r d7eb081cf220 -r e81411bfa7ef src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Sun Jan 01 09:27:48 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Sun Jan 01 16:32:53 2012 +0100
@@ -219,7 +219,7 @@
   have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c"
     by(simp add: strip_lpfpc[OF _ 1])
-  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
+  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
@@ -227,7 +227,7 @@
       show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
     qed
   qed
-  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
+  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c c'"
     by (blast intro: mono_gamma_c order_trans)
 qed
 
diff -r d7eb081cf220 -r e81411bfa7ef src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Sun Jan 01 09:27:48 2012 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Sun Jan 01 16:32:53 2012 +0100
@@ -193,7 +193,7 @@
   from pfp_WN_pfp[OF allI[OF strip_step'] mono_step' 1]
   have 2: "step' \<top> c' \<sqsubseteq> c'" .
   have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_WN[OF _ 1])
-  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' \<top> c')"
+  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')"
     proof(rule step_preserves_le[OF _ _ 3])
@@ -201,7 +201,7 @@
       show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2])
     qed
   qed
-  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c c'"
+  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c c'"
     by (blast intro: mono_gamma_c order_trans)
 qed
 
diff -r d7eb081cf220 -r e81411bfa7ef src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Sun Jan 01 09:27:48 2012 +0100
+++ b/src/HOL/IMP/Collecting.thy	Sun Jan 01 16:32:53 2012 +0100
@@ -171,7 +171,7 @@
   {S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
 
 definition CS :: "state set \<Rightarrow> com \<Rightarrow> state set acom" where
-"CS S c = lfp c (step S)"
+"CS S c = lfp (step S) c"
 
 lemma mono_step_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step S x \<le> step T y"
 proof(induction x y arbitrary: S T rule: less_eq_acom.induct)
@@ -190,7 +190,7 @@
 lemma strip_step: "strip(step S c) = strip c"
 by (induction c arbitrary: S) auto
 
-lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
+lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)"
 apply(rule lfp_unfold[OF _  mono_step])
 apply(simp add: strip_step)
 done
diff -r d7eb081cf220 -r e81411bfa7ef src/HOL/IMP/Complete_Lattice_ix.thy
--- a/src/HOL/IMP/Complete_Lattice_ix.thy	Sun Jan 01 09:27:48 2012 +0100
+++ b/src/HOL/IMP/Complete_Lattice_ix.thy	Sun Jan 01 16:32:53 2012 +0100
@@ -23,29 +23,29 @@
 and Glb_in_L: "A \<subseteq> L i \<Longrightarrow> Glb i A : L i"
 begin
 
-definition lfp :: "'i \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
-"lfp i f = Glb i {a : L i. f a \<le> a}"
+definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'i \<Rightarrow> 'a" where
+"lfp f i = Glb i {a : L i. f a \<le> a}"
 
-lemma index_lfp: "lfp i f : L i"
+lemma index_lfp: "lfp f i : L i"
 by(auto simp: lfp_def intro: Glb_in_L)
 
 lemma lfp_lowerbound:
-  "\<lbrakk> a : L i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp i f \<le> a"
+  "\<lbrakk> a : L i;  f a \<le> a \<rbrakk> \<Longrightarrow> lfp f i \<le> a"
 by (auto simp add: lfp_def intro: Glb_lower)
 
 lemma lfp_greatest:
-  "\<lbrakk> a : L i;  \<And>u. \<lbrakk> u : L i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp i f"
+  "\<lbrakk> a : L i;  \<And>u. \<lbrakk> u : L i; f u \<le> u\<rbrakk> \<Longrightarrow> a \<le> u \<rbrakk> \<Longrightarrow> a \<le> lfp f i"
 by (auto simp add: lfp_def intro: Glb_greatest)
 
 lemma lfp_unfold: assumes "\<And>x i. f x : L i \<longleftrightarrow> x : L i"
-and mono: "mono f" shows "lfp i f = f (lfp i f)"
+and mono: "mono f" shows "lfp f i = f (lfp f i)"
 proof-
   note assms(1)[simp] index_lfp[simp]
-  have 1: "f (lfp i f) \<le> lfp i f"
+  have 1: "f (lfp f i) \<le> lfp f i"
     apply(rule lfp_greatest)
     apply simp
     by (blast intro: lfp_lowerbound monoD[OF mono] order_trans)
-  have "lfp i f \<le> f (lfp i f)"
+  have "lfp f i \<le> f (lfp f i)"
     by (fastforce intro: 1 monoD[OF mono] lfp_lowerbound)
   with 1 show ?thesis by(blast intro: order_antisym)
 qed