author huffman Tue, 01 Jul 2008 06:21:28 +0200 changeset 27417 6cc897e2468a parent 27416 07e04ab0177a child 27418 564117b58d73
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 @@

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"
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)
by (auto simp:connected)

@@ -1099,8 +1099,8 @@
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)
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"
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
```