# HG changeset patch
# User nipkow
# Date 1368420637 -7200
# Node ID ae755fd6c8835752cddb9532f8c2a02db7f778cf
# Parent  4517ceb545c13b7c94262a3266ad876f4fd4d41f
tuned names

diff -r 4517ceb545c1 -r ae755fd6c883 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Sun May 12 20:58:01 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Mon May 13 06:50:37 2013 +0200
@@ -278,7 +278,7 @@
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and constrain_plus' = constrain_plus_ivl and constrain_less' = constrain_less_ivl
-defines AI_ivl' is AI_wn
+defines AI_wn_ivl is AI_wn
 ..
 
 
@@ -288,7 +288,7 @@
 definition "step_down_ivl n = ((\<lambda>C. C \<triangle> step_ivl \<top> C)^^n)"
 
 text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
-the loop took to execute. In contrast, @{const AI_ivl'} converges in a
+the loop took to execute. In contrast, @{const AI_wn_ivl} converges in a
 constant number of steps: *}
 
 value "show_acom (step_up_ivl 1 (bot test3_ivl))"
@@ -303,14 +303,14 @@
 value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
 value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
 value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
-value "show_acom_opt (AI_ivl' test3_ivl)"
+value "show_acom_opt (AI_wn_ivl test3_ivl)"
 
 
 text{* Now all the analyses terminate: *}
 
-value "show_acom_opt (AI_ivl' test4_ivl)"
-value "show_acom_opt (AI_ivl' test5_ivl)"
-value "show_acom_opt (AI_ivl' test6_ivl)"
+value "show_acom_opt (AI_wn_ivl test4_ivl)"
+value "show_acom_opt (AI_wn_ivl test5_ivl)"
+value "show_acom_opt (AI_wn_ivl test6_ivl)"
 
 
 subsubsection "Generic Termination Proof"
@@ -543,7 +543,7 @@
          split: prod.split extended.splits if_splits)
 
 definition n_ivl :: "ivl \<Rightarrow> nat" where
-"n_ivl ivl = 3 - m_ivl ivl"
+"n_ivl iv = 3 - m_ivl iv"
 
 lemma n_ivl_narrow:
   "x \<triangle> y < x \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
@@ -578,15 +578,15 @@
 done
 
 lemma iter_narrow_step_ivl_termination:
-  "top_on_acom C0 (- vars C0) \<Longrightarrow> step_ivl \<top> C0 \<le> C0 \<Longrightarrow>
-  \<exists>C. iter_narrow (step_ivl \<top>) C0 = Some C"
-apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. strip C0 = strip C \<and> top_on_acom C (-vars C)"])
+  "top_on_acom C (- vars C) \<Longrightarrow> step_ivl \<top> C \<le> C \<Longrightarrow>
+  \<exists>C'. iter_narrow (step_ivl \<top>) C = Some C'"
+apply(rule iter_narrow_termination[where n = "n_c" and P = "%C'. strip C = strip C' \<and> top_on_acom C' (-vars C')"])
 apply(auto simp: top_on_step'[simplified comp_def vars_acom_def]
         mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow)
 done
 
-theorem AI_ivl'_termination:
-  "\<exists>C. AI_ivl' c = Some C"
+theorem AI_wn_ivl_termination:
+  "\<exists>C. AI_wn_ivl c = Some C"
 apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
            split: option.split)
 apply(rule iter_narrow_step_ivl_termination)