# HG changeset patch
# User nipkow
# Date 1359128709 -3600
# Node ID 3371f5ee4aceb05136d7afefa27e248fe7837009
# Parent  aafd4270b4d4186a1be2f6bf69fdb75512c8291c
tuned

diff -r aafd4270b4d4 -r 3371f5ee4ace src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Fri Jan 25 16:45:09 2013 +0100
@@ -80,17 +80,17 @@
 value "show_acom (steps test1_const 1)"
 value "show_acom (steps test1_const 2)"
 value "show_acom (steps test1_const 3)"
-value "show_acom_opt (AI_const test1_const)"
+value "show_acom (the(AI_const test1_const))"
 
-value "show_acom_opt (AI_const test2_const)"
-value "show_acom_opt (AI_const test3_const)"
+value "show_acom (the(AI_const test2_const))"
+value "show_acom (the(AI_const test3_const))"
 
 value "show_acom (steps test4_const 0)"
 value "show_acom (steps test4_const 1)"
 value "show_acom (steps test4_const 2)"
 value "show_acom (steps test4_const 3)"
 value "show_acom (steps test4_const 4)"
-value "show_acom_opt (AI_const test4_const)"
+value "show_acom (the(AI_const test4_const))"
 
 value "show_acom (steps test5_const 0)"
 value "show_acom (steps test5_const 1)"
@@ -99,7 +99,7 @@
 value "show_acom (steps test5_const 4)"
 value "show_acom (steps test5_const 5)"
 value "show_acom (steps test5_const 6)"
-value "show_acom_opt (AI_const test5_const)"
+value "show_acom (the(AI_const test5_const))"
 
 value "show_acom (steps test6_const 0)"
 value "show_acom (steps test6_const 1)"
@@ -115,7 +115,7 @@
 value "show_acom (steps test6_const 11)"
 value "show_acom (steps test6_const 12)"
 value "show_acom (steps test6_const 13)"
-value "show_acom_opt (AI_const test6_const)"
+value "show_acom (the(AI_const test6_const))"
 
 
 text{* Monotonicity: *}
diff -r aafd4270b4d4 -r 3371f5ee4ace src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Jan 25 16:45:09 2013 +0100
@@ -121,7 +121,7 @@
 definition "test1_parity =
   ''x'' ::= N 1;
   WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
-value [code] "show_acom_opt (AI_parity test1_parity)"
+value [code] "show_acom (the(AI_parity test1_parity))"
 
 definition "test2_parity =
   ''x'' ::= N 1;
@@ -136,7 +136,7 @@
 value "show_acom (steps test2_parity 4)"
 value "show_acom (steps test2_parity 5)"
 value "show_acom (steps test2_parity 6)"
-value "show_acom_opt (AI_parity test2_parity)"
+value "show_acom (the(AI_parity test2_parity))"
 
 
 subsubsection "Termination"
diff -r aafd4270b4d4 -r 3371f5ee4ace src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Fri Jan 25 16:45:09 2013 +0100
@@ -55,11 +55,11 @@
 fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
 and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
 and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
-assumes test_num': "test_num' n a = (n : \<gamma> a)"
+assumes test_num': "test_num' i a = (i : \<gamma> a)"
 and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
-  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
-and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>
-  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
+  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma> a \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
+and filter_less': "filter_less' (i1<i2) a1 a2 = (b1,b2) \<Longrightarrow>
+  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
 
 
 locale Abs_Int1 =
@@ -80,13 +80,13 @@
 subsubsection "Backward analysis"
 
 fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
-"afilter (N n) a S = (if test_num' n a then S else None)" |
+"afilter (N i) a S = (if test_num' i a then S else None)" |
 "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
   let a' = fun S x \<sqinter> a in
   if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
 "afilter (Plus e1 e2) a S =
- (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
-  in afilter e1 a1 (afilter e2 a2 S))"
+ (let (a\<^isub>1',a\<^isub>2') = filter_plus' a (aval'' e1 S) (aval'' e2 S)
+  in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
 
 text{* The test for @{const bot} in the @{const V}-case is important: @{const
 bot} indicates that a variable has no possible values, i.e.\ that the current
@@ -105,8 +105,8 @@
   (if res then bfilter b1 True (bfilter b2 True S)
    else bfilter b1 False S \<squnion> bfilter b2 False S)" |
 "bfilter (Less e1 e2) res S =
-  (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
-   in afilter e1 res1 (afilter e2 res2 S))"
+  (let (a\<^isub>1',a\<^isub>2') = filter_less' res (aval'' e1 S) (aval'' e2 S)
+   in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
 
 lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
 by(induction e arbitrary: a S)
diff -r aafd4270b4d4 -r 3371f5ee4ace src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Jan 25 16:45:09 2013 +0100
@@ -248,25 +248,27 @@
 
 subsubsection "Tests"
 
-value "show_acom_opt (AI_ivl test1_ivl)"
+value "show_acom (the(AI_ivl test1_ivl))"
 
 text{* Better than @{text AI_const}: *}
-value "show_acom_opt (AI_ivl test3_const)"
-value "show_acom_opt (AI_ivl test4_const)"
-value "show_acom_opt (AI_ivl test6_const)"
+value "show_acom (the(AI_ivl test3_const))"
+value "show_acom (the(AI_ivl test4_const))"
+value "show_acom (the(AI_ivl test6_const))"
 
 definition "steps c i = (step_ivl(top c) ^^ i) (bot c)"
 
-value "show_acom_opt (AI_ivl test2_ivl)"
+value "test2_ivl"
+value "show_acom (the(AI_ivl test2_ivl))"
 value "show_acom (steps test2_ivl 0)"
 value "show_acom (steps test2_ivl 1)"
 value "show_acom (steps test2_ivl 2)"
 value "show_acom (steps test2_ivl 3)"
 
-text{* Fixed point reached in 2 steps.
+text{* Fixed point reached in 3 steps.
  Not so if the start value of x is known: *}
 
-value "show_acom_opt (AI_ivl test3_ivl)"
+value "test3_ivl"
+value "show_acom (the(AI_ivl test3_ivl))"
 value "show_acom (steps test3_ivl 0)"
 value "show_acom (steps test3_ivl 1)"
 value "show_acom (steps test3_ivl 2)"
@@ -279,12 +281,15 @@
 the actual execution terminates, the analysis may not. The value of y keeps
 decreasing as the analysis is iterated, no matter how long: *}
 
+value "test4_ivl"
 value "show_acom (steps test4_ivl 50)"
 
 text{* Relationships between variables are NOT captured: *}
-value "show_acom_opt (AI_ivl test5_ivl)"
+value "test5_ivl"
+value "show_acom (the(AI_ivl test5_ivl))"
 
 text{* Again, the analysis would not terminate: *}
+value "test6_ivl"
 value "show_acom (steps test6_ivl 50)"
 
 end
diff -r aafd4270b4d4 -r 3371f5ee4ace src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Fri Jan 25 16:45:09 2013 +0100
@@ -416,14 +416,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 (the(AI_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 (the(AI_ivl' test4_ivl))"
+value "show_acom (the(AI_ivl' test5_ivl))"
+value "show_acom (the(AI_ivl' test6_ivl))"
 
 
 subsubsection "Generic Termination Proof"
diff -r aafd4270b4d4 -r 3371f5ee4ace src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Sun Jan 20 15:34:27 2013 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Fri Jan 25 16:45:09 2013 +0100
@@ -109,7 +109,6 @@
 value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
 
 definition "show_acom = map_acom (Option.map show_st)"
-definition "show_acom_opt = Option.map show_acom"
 
 definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"