1.1 --- a/src/HOL/IMP/Abs_Int1_const.thy	Sun Jan 20 15:34:27 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy	Fri Jan 25 16:45:09 2013 +0100
     1.3 @@ -80,17 +80,17 @@
     1.4  value "show_acom (steps test1_const 1)"
     1.5  value "show_acom (steps test1_const 2)"
     1.6  value "show_acom (steps test1_const 3)"
     1.7 -value "show_acom_opt (AI_const test1_const)"
     1.8 +value "show_acom (the(AI_const test1_const))"
     1.9  
    1.10 -value "show_acom_opt (AI_const test2_const)"
    1.11 -value "show_acom_opt (AI_const test3_const)"
    1.12 +value "show_acom (the(AI_const test2_const))"
    1.13 +value "show_acom (the(AI_const test3_const))"
    1.14  
    1.15  value "show_acom (steps test4_const 0)"
    1.16  value "show_acom (steps test4_const 1)"
    1.17  value "show_acom (steps test4_const 2)"
    1.18  value "show_acom (steps test4_const 3)"
    1.19  value "show_acom (steps test4_const 4)"
    1.20 -value "show_acom_opt (AI_const test4_const)"
    1.21 +value "show_acom (the(AI_const test4_const))"
    1.22  
    1.23  value "show_acom (steps test5_const 0)"
    1.24  value "show_acom (steps test5_const 1)"
    1.25 @@ -99,7 +99,7 @@
    1.26  value "show_acom (steps test5_const 4)"
    1.27  value "show_acom (steps test5_const 5)"
    1.28  value "show_acom (steps test5_const 6)"
    1.29 -value "show_acom_opt (AI_const test5_const)"
    1.30 +value "show_acom (the(AI_const test5_const))"
    1.31  
    1.32  value "show_acom (steps test6_const 0)"
    1.33  value "show_acom (steps test6_const 1)"
    1.34 @@ -115,7 +115,7 @@
    1.35  value "show_acom (steps test6_const 11)"
    1.36  value "show_acom (steps test6_const 12)"
    1.37  value "show_acom (steps test6_const 13)"
    1.38 -value "show_acom_opt (AI_const test6_const)"
    1.39 +value "show_acom (the(AI_const test6_const))"
    1.40  
    1.41  
    1.42  text{* Monotonicity: *}

     2.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Sun Jan 20 15:34:27 2013 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Jan 25 16:45:09 2013 +0100
     2.3 @@ -121,7 +121,7 @@
     2.4  definition "test1_parity =
     2.5    ''x'' ::= N 1;
     2.6    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
     2.7 -value [code] "show_acom_opt (AI_parity test1_parity)"
     2.8 +value [code] "show_acom (the(AI_parity test1_parity))"
     2.9  
    2.10  definition "test2_parity =
    2.11    ''x'' ::= N 1;
    2.12 @@ -136,7 +136,7 @@
    2.13  value "show_acom (steps test2_parity 4)"
    2.14  value "show_acom (steps test2_parity 5)"
    2.15  value "show_acom (steps test2_parity 6)"
    2.16 -value "show_acom_opt (AI_parity test2_parity)"
    2.17 +value "show_acom (the(AI_parity test2_parity))"
    2.18  
    2.19  
    2.20  subsubsection "Termination"

     3.1 --- a/src/HOL/IMP/Abs_Int2.thy	Sun Jan 20 15:34:27 2013 +0100
     3.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Fri Jan 25 16:45:09 2013 +0100
     3.3 @@ -55,11 +55,11 @@
     3.4  fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
     3.5  and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
     3.6  and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
     3.7 -assumes test_num': "test_num' n a = (n : \<gamma> a)"
     3.8 +assumes test_num': "test_num' i a = (i : \<gamma> a)"
     3.9  and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
    3.10 -  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
    3.11 -and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>
    3.12 -  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
    3.13 +  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma> a \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
    3.14 +and filter_less': "filter_less' (i1<i2) a1 a2 = (b1,b2) \<Longrightarrow>
    3.15 +  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
    3.16  
    3.17  
    3.18  locale Abs_Int1 =
    3.19 @@ -80,13 +80,13 @@
    3.20  subsubsection "Backward analysis"
    3.21  
    3.22  fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
    3.23 -"afilter (N n) a S = (if test_num' n a then S else None)" |
    3.24 +"afilter (N i) a S = (if test_num' i a then S else None)" |
    3.25  "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
    3.26    let a' = fun S x \<sqinter> a in
    3.27    if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
    3.28  "afilter (Plus e1 e2) a S =
    3.29 - (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    3.30 -  in afilter e1 a1 (afilter e2 a2 S))"
    3.31 + (let (a\<^isub>1',a\<^isub>2') = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    3.32 +  in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
    3.33  
    3.34  text{* The test for @{const bot} in the @{const V}-case is important: @{const
    3.35  bot} indicates that a variable has no possible values, i.e.\ that the current
    3.36 @@ -105,8 +105,8 @@
    3.37    (if res then bfilter b1 True (bfilter b2 True S)
    3.38     else bfilter b1 False S \<squnion> bfilter b2 False S)" |
    3.39  "bfilter (Less e1 e2) res S =
    3.40 -  (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
    3.41 -   in afilter e1 res1 (afilter e2 res2 S))"
    3.42 +  (let (a\<^isub>1',a\<^isub>2') = filter_less' res (aval'' e1 S) (aval'' e2 S)
    3.43 +   in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
    3.44  
    3.45  lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
    3.46  by(induction e arbitrary: a S)

     4.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Sun Jan 20 15:34:27 2013 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Jan 25 16:45:09 2013 +0100
     4.3 @@ -248,25 +248,27 @@
     4.4  
     4.5  subsubsection "Tests"
     4.6  
     4.7 -value "show_acom_opt (AI_ivl test1_ivl)"
     4.8 +value "show_acom (the(AI_ivl test1_ivl))"
     4.9  
    4.10  text{* Better than @{text AI_const}: *}
    4.11 -value "show_acom_opt (AI_ivl test3_const)"
    4.12 -value "show_acom_opt (AI_ivl test4_const)"
    4.13 -value "show_acom_opt (AI_ivl test6_const)"
    4.14 +value "show_acom (the(AI_ivl test3_const))"
    4.15 +value "show_acom (the(AI_ivl test4_const))"
    4.16 +value "show_acom (the(AI_ivl test6_const))"
    4.17  
    4.18  definition "steps c i = (step_ivl(top c) ^^ i) (bot c)"
    4.19  
    4.20 -value "show_acom_opt (AI_ivl test2_ivl)"
    4.21 +value "test2_ivl"
    4.22 +value "show_acom (the(AI_ivl test2_ivl))"
    4.23  value "show_acom (steps test2_ivl 0)"
    4.24  value "show_acom (steps test2_ivl 1)"
    4.25  value "show_acom (steps test2_ivl 2)"
    4.26  value "show_acom (steps test2_ivl 3)"
    4.27  
    4.28 -text{* Fixed point reached in 2 steps.
    4.29 +text{* Fixed point reached in 3 steps.
    4.30   Not so if the start value of x is known: *}
    4.31  
    4.32 -value "show_acom_opt (AI_ivl test3_ivl)"
    4.33 +value "test3_ivl"
    4.34 +value "show_acom (the(AI_ivl test3_ivl))"
    4.35  value "show_acom (steps test3_ivl 0)"
    4.36  value "show_acom (steps test3_ivl 1)"
    4.37  value "show_acom (steps test3_ivl 2)"
    4.38 @@ -279,12 +281,15 @@
    4.39  the actual execution terminates, the analysis may not. The value of y keeps
    4.40  decreasing as the analysis is iterated, no matter how long: *}
    4.41  
    4.42 +value "test4_ivl"
    4.43  value "show_acom (steps test4_ivl 50)"
    4.44  
    4.45  text{* Relationships between variables are NOT captured: *}
    4.46 -value "show_acom_opt (AI_ivl test5_ivl)"
    4.47 +value "test5_ivl"
    4.48 +value "show_acom (the(AI_ivl test5_ivl))"
    4.49  
    4.50  text{* Again, the analysis would not terminate: *}
    4.51 +value "test6_ivl"
    4.52  value "show_acom (steps test6_ivl 50)"
    4.53  
    4.54  end

     5.1 --- a/src/HOL/IMP/Abs_Int3.thy	Sun Jan 20 15:34:27 2013 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Fri Jan 25 16:45:09 2013 +0100
     5.3 @@ -416,14 +416,14 @@
     5.4  value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
     5.5  value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
     5.6  value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
     5.7 -value "show_acom_opt (AI_ivl' test3_ivl)"
     5.8 +value "show_acom (the(AI_ivl' test3_ivl))"
     5.9  
    5.10  
    5.11  text{* Now all the analyses terminate: *}
    5.12  
    5.13 -value "show_acom_opt (AI_ivl' test4_ivl)"
    5.14 -value "show_acom_opt (AI_ivl' test5_ivl)"
    5.15 -value "show_acom_opt (AI_ivl' test6_ivl)"
    5.16 +value "show_acom (the(AI_ivl' test4_ivl))"
    5.17 +value "show_acom (the(AI_ivl' test5_ivl))"
    5.18 +value "show_acom (the(AI_ivl' test6_ivl))"
    5.19  
    5.20  
    5.21  subsubsection "Generic Termination Proof"

     6.1 --- a/src/HOL/IMP/Abs_State.thy	Sun Jan 20 15:34:27 2013 +0100
     6.2 +++ b/src/HOL/IMP/Abs_State.thy	Fri Jan 25 16:45:09 2013 +0100
     6.3 @@ -109,7 +109,6 @@
     6.4  value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
     6.5  
     6.6  definition "show_acom = map_acom (Option.map show_st)"
     6.7 -definition "show_acom_opt = Option.map show_acom"
     6.8  
     6.9  definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
    6.10