src/HOL/IMP/Abs_Int3.thy
changeset 51036 e7b54119c436
parent 50995 3371f5ee4ace
child 51245 311fe56541ea
     1.1 --- a/src/HOL/IMP/Abs_Int3.thy	Mon Feb 11 11:38:16 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Tue Feb 12 11:54:29 2013 +0100
     1.3 @@ -358,24 +358,24 @@
     1.4  begin
     1.5  
     1.6  definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
     1.7 -"AI_wn c = pfp_wn (step' (top c)) (bot c)"
     1.8 +"AI_wn c = pfp_wn (step' (top(vars c))) (bot c)"
     1.9  
    1.10  lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    1.11  proof(simp add: CS_def AI_wn_def)
    1.12 -  assume 1: "pfp_wn (step' (top c)) (bot c) = Some C"
    1.13 -  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>c\<^esub> C \<sqsubseteq> C"
    1.14 +  assume 1: "pfp_wn (step' (top(vars c))) (bot c) = Some C"
    1.15 +  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<sqsubseteq> C"
    1.16      by(rule pfp_wn_pfp[where x="bot c"])
    1.17        (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
    1.18 -  have pfp: "step (\<gamma>\<^isub>o(top c)) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    1.19 +  have pfp: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    1.20    proof(rule order_trans)
    1.21 -    show "step (\<gamma>\<^isub>o (top c)) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top c) C)"
    1.22 +    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
    1.23        by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
    1.24      show "... \<le> \<gamma>\<^isub>c C"
    1.25        by(rule mono_gamma_c[OF conjunct2[OF 2]])
    1.26    qed
    1.27    have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
    1.28 -  have "lfp c (step (\<gamma>\<^isub>o (top c))) \<le> \<gamma>\<^isub>c C"
    1.29 -    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top c))", OF 3 pfp])
    1.30 +  have "lfp c (step (\<gamma>\<^isub>o (top(vars c)))) \<le> \<gamma>\<^isub>c C"
    1.31 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 pfp])
    1.32    thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
    1.33  qed
    1.34  
    1.35 @@ -396,9 +396,9 @@
    1.36  by(rule refl)
    1.37  
    1.38  definition "step_up_ivl n =
    1.39 -  ((\<lambda>C. C \<nabla> step_ivl (top(strip C)) C)^^n)"
    1.40 +  ((\<lambda>C. C \<nabla> step_ivl (top(vars(strip C))) C)^^n)"
    1.41  definition "step_down_ivl n =
    1.42 -  ((\<lambda>C. C \<triangle> step_ivl (top (strip C)) C)^^n)"
    1.43 +  ((\<lambda>C. C \<triangle> step_ivl (top(vars(strip C))) C)^^n)"
    1.44  
    1.45  text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
    1.46  the loop took to execute. In contrast, @{const AI_ivl'} converges in a
    1.47 @@ -416,14 +416,14 @@
    1.48  value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
    1.49  value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
    1.50  value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
    1.51 -value "show_acom (the(AI_ivl' test3_ivl))"
    1.52 +value "show_acom_opt (AI_ivl' test3_ivl)"
    1.53  
    1.54  
    1.55  text{* Now all the analyses terminate: *}
    1.56  
    1.57 -value "show_acom (the(AI_ivl' test4_ivl))"
    1.58 -value "show_acom (the(AI_ivl' test5_ivl))"
    1.59 -value "show_acom (the(AI_ivl' test6_ivl))"
    1.60 +value "show_acom_opt (AI_ivl' test4_ivl)"
    1.61 +value "show_acom_opt (AI_ivl' test5_ivl)"
    1.62 +value "show_acom_opt (AI_ivl' test6_ivl)"
    1.63  
    1.64  
    1.65  subsubsection "Generic Termination Proof"
    1.66 @@ -629,14 +629,14 @@
    1.67  
    1.68  
    1.69  lemma iter_winden_step_ivl_termination:
    1.70 -  "\<exists>C. iter_widen (step_ivl (top c)) (bot c) = Some C"
    1.71 +  "\<exists>C. iter_widen (step_ivl (top(vars c))) (bot c) = Some C"
    1.72  apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
    1.73  apply (simp_all add: step'_in_Lc m_c_widen)
    1.74  done
    1.75  
    1.76  lemma iter_narrow_step_ivl_termination:
    1.77 -  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top c) C0 \<sqsubseteq> C0 \<Longrightarrow>
    1.78 -  \<exists>C. iter_narrow (step_ivl (top c)) C0 = Some C"
    1.79 +  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top(vars c)) C0 \<sqsubseteq> C0 \<Longrightarrow>
    1.80 +  \<exists>C. iter_narrow (step_ivl (top(vars c))) C0 = Some C"
    1.81  apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
    1.82  apply (simp add: step'_in_Lc)
    1.83  apply (simp)
    1.84 @@ -654,7 +654,7 @@
    1.85  apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
    1.86             split: option.split)
    1.87  apply(rule iter_narrow_step_ivl_termination)
    1.88 -apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>c\<^esub>" and c=c, simplified])
    1.89 +apply(blast intro: iter_widen_inv[where f = "step' \<top>\<^bsub>vars c\<^esub>" and P = "%C. C \<in> Lc c"] bot_in_Lc Lc_widen step'_in_Lc[where S = "\<top>\<^bsub>vars c\<^esub>" and c=c, simplified])
    1.90  apply(erule iter_widen_pfp)
    1.91  done
    1.92