# HG changeset patch # User huffman # Date 1214886088 -7200 # Node ID 6cc897e2468a799100966a780cc88413374b8740 # Parent 07e04ab0177a82df5ae02754ce8f712c54c9e1ff rename INF to INFM diff -r 07e04ab0177a -r 6cc897e2468a src/HOL/SizeChange/Correctness.thy --- 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 "\(\x. \\<^sub>\i. f i = x)" hence "\x. \j. \i>j. f i \ x" - unfolding INF_nat by blast + unfolding INFM_nat by blast with choice have "\j. \x. \i>(j x). f i \ x" . then obtain j where @@ -854,14 +854,14 @@ by (fold is_thread_def) simp show "\\<^sub>\l. descat p \ 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 \ p (s j) (s (Suc j))" - unfolding INF_nat by auto + unfolding INFM_nat by auto then obtain l where "s j \ l" and desc: "descat p \ l" unfolding is_desc_fthread_def by auto @@ -908,7 +908,7 @@ moreover from A have "\\<^sub>\i. (\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 \ ?Qs ?w" .. qed @@ -936,7 +936,7 @@ lemma INF_drop_prefix: "(\\<^sub>\i::nat. i > n \ P i) = (\\<^sub>\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 "\\<^sub>\i. descat (contract s p) ?c\ i" - unfolding INF_nat + unfolding INFM_nat proof fix i let ?K = "section_of s (max (s (Suc i)) n)" from `\\<^sub>\i. descat p \ i` obtain j where "s (Suc ?K) < j" "descat p \ 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: "\i. i > n \ is_fthread (\s i) p (s i) (s (Suc i))" "\\<^sub>\i. is_desc_fthread (\s i) p (s i) (s (Suc i))" - by (auto intro:INF_mono) + by (auto intro:INFM_mono) have p1: "\i. i > n \ is_fthread ?j\ 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: "\\<^sub>\i. is_desc_fthread ?j\ 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="\i. n < i"]) - apply (simp only:INF_nat) + apply (rule INFM_mono[where P="\i. n < i"]) + apply (simp only:INFM_nat) by (auto simp add: th) qed @@ -1314,16 +1314,16 @@ obtain p where inf_visit: "\\<^sub>\i. \ i = p" by auto then obtain i where "n < i" "\ i = p" - by (auto simp:INF_nat) + by (auto simp:INFM_nat) from desc have "\\<^sub>\i. descat ?cp \ i" unfolding is_desc_thread_def by auto then obtain j where "i < j" and "descat ?cp \ j" - unfolding INF_nat by auto + unfolding INFM_nat by auto from inf_visit obtain k where "j < k" "\ 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 \ ?cp] diff -r 07e04ab0177a -r 6cc897e2468a src/HOL/SizeChange/Interpretation.thy --- 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 "\\<^sub>\i. ?seq (Suc i) < ?seq i" unfolding INF_nat + moreover have "\\<^sub>\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