rename INF to INFM

--- a/src/HOL/SizeChange/Correctness.thy	Tue Jul 01 03:14:00 2008 +0200
+++ b/src/HOL/SizeChange/Correctness.thy	Tue Jul 01 06:21:28 2008 +0200
@@ -45,7 +45,7 @@
 proof (rule classical)
   assume "\<not>(\<exists>x. \<exists>\<^sub>\<infinity>i. f i = x)"
   hence "\<forall>x. \<exists>j. \<forall>i>j. f i \<noteq> x"
-    unfolding INF_nat by blast
+    unfolding INFM_nat by blast
   with choice
   have "\<exists>j. \<forall>x. \<forall>i>(j x). f i \<noteq> x" .
   then obtain j where 
@@ -854,14 +854,14 @@
     by (fold is_thread_def) simp
 
   show "\<exists>\<^sub>\<infinity>l. descat p \<theta> l"
-    unfolding INF_nat
+    unfolding INFM_nat
   proof
     fix i 
     
     let ?k = "section_of s i"
     from fdths obtain j
       where "?k < j" "is_desc_fthread \<theta> p (s j) (s (Suc j))"
-      unfolding INF_nat by auto
+      unfolding INFM_nat by auto
     then obtain l where "s j \<le> l" and desc: "descat p \<theta> l"
       unfolding is_desc_fthread_def
       by auto
@@ -908,7 +908,7 @@
 
   moreover
   from A have "\<exists>\<^sub>\<infinity>i. (\<exists>x. Q x i)" ..
-  hence "?Qs ?w" by (rule INF_mono) (auto intro:someI)
+  hence "?Qs ?w" by (rule INFM_mono) (auto intro:someI)
   ultimately
   show "?Ps ?w \<and> ?Qs ?w" ..
 qed
@@ -936,7 +936,7 @@
 
 lemma INF_drop_prefix:
   "(\<exists>\<^sub>\<infinity>i::nat. i > n \<and> P i) = (\<exists>\<^sub>\<infinity>i. P i)"
-  apply (auto simp:INF_nat)
+  apply (auto simp:INFM_nat)
   apply (drule_tac x = "max m n" in spec)
   apply (elim exE conjE)
   apply (rule_tac x = "na" in exI)
@@ -982,14 +982,14 @@
     qed
 
     show "\<exists>\<^sub>\<infinity>i. descat (contract s p) ?c\<theta> i"
-      unfolding INF_nat 
+      unfolding INFM_nat 
     proof 
       fix i
 
       let ?K = "section_of s (max (s (Suc i)) n)"
       from `\<exists>\<^sub>\<infinity>i. descat p \<theta> i` obtain j
 	  where "s (Suc ?K) < j" "descat p \<theta> j"
-	unfolding INF_nat by blast
+	unfolding INFM_nat by blast
       
       let ?L = "section_of s j"
       {
@@ -1069,7 +1069,7 @@
   from fr ths_spec have ths_spec2:
       "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
       "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
-    by (auto intro:INF_mono)
+    by (auto intro:INFM_mono)
   
   have p1: "\<And>i. i > n \<Longrightarrow> is_fthread ?j\<theta> p (s i) (s (Suc i))"
     by (rule connect_threads) (auto simp:connected ths_spec2)
@@ -1079,7 +1079,7 @@
     unfolding INF_drop_prefix .
   
   hence p2: "\<exists>\<^sub>\<infinity>i. is_desc_fthread ?j\<theta> p (s i) (s (Suc i))"
-    apply (rule INF_mono)
+    apply (rule INFM_mono)
     apply (rule connect_dthreads)
     by (auto simp:connected)
   
@@ -1099,8 +1099,8 @@
   unfolding is_desc_thread_def 
   apply (auto)
   apply (rule_tac x="Suc n" in exI, auto)
-  apply (rule INF_mono[where P="\<lambda>i. n < i"])
-  apply (simp only:INF_nat)
+  apply (rule INFM_mono[where P="\<lambda>i. n < i"])
+  apply (simp only:INFM_nat)
   by (auto simp add: th)
 qed
 
@@ -1314,16 +1314,16 @@
     obtain p where inf_visit: "\<exists>\<^sub>\<infinity>i. \<theta> i = p" by auto
 
     then obtain i where "n < i" "\<theta> i = p" 
-      by (auto simp:INF_nat)
+      by (auto simp:INFM_nat)
 
     from desc
     have "\<exists>\<^sub>\<infinity>i. descat ?cp \<theta> i"
       unfolding is_desc_thread_def by auto
     then obtain j 
       where "i < j" and "descat ?cp \<theta> j"
-      unfolding INF_nat by auto
+      unfolding INFM_nat by auto
     from inf_visit obtain k where "j < k" "\<theta> k = p"
-      by (auto simp:INF_nat)
+      by (auto simp:INFM_nat)
 
     from `i < j` `j < k` `n < i` thr 
       fin_from_inf[of n \<theta> ?cp]

--- a/src/HOL/SizeChange/Interpretation.thy	Tue Jul 01 03:14:00 2008 +0200
+++ b/src/HOL/SizeChange/Interpretation.thy	Tue Jul 01 06:21:28 2008 +0200
@@ -172,7 +172,7 @@
   from less 
   obtain k' where "n + k < k'"
 	and "s (Suc k') < s k'"
-	unfolding INF_nat by auto
+	unfolding INFM_nat by auto
   
   with decr[of "n + k" k'] min
   have "s (Suc k') < ?min" by auto
@@ -388,11 +388,11 @@
 		by (rule ird a)+
 	qed
   qed
-  moreover have "\<exists>\<^sub>\<infinity>i. ?seq (Suc i) < ?seq i" unfolding INF_nat
+  moreover have "\<exists>\<^sub>\<infinity>i. ?seq (Suc i) < ?seq i" unfolding INFM_nat
   proof 
 	fix i 
 	from inf obtain j where "i < j" and d: "descat ?p th j"
-	  unfolding INF_nat by auto
+	  unfolding INFM_nat by auto
 	let ?q1 = "th j" and ?q2 = "th (Suc j)"
 	from d have "dsc (Gs j) ?q1 ?q2" by auto