src/HOL/IMP/Abs_Int2.thy
changeset 51359 00b45c7e831f
parent 51037 0a6d84c41dbf
child 51389 8a9f0503b1c0
equal deleted inserted replaced
51358:0c376ef98559 51359:00b45c7e831f
     2 
     2 
     3 theory Abs_Int2
     3 theory Abs_Int2
     4 imports Abs_Int1
     4 imports Abs_Int1
     5 begin
     5 begin
     6 
     6 
     7 instantiation prod :: (preord,preord) preord
     7 instantiation prod :: (order,order) order
     8 begin
     8 begin
     9 
     9 
    10 definition "le_prod p1 p2 = (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
    10 definition "less_eq_prod p1 p2 = (fst p1 \<le> fst p2 \<and> snd p1 \<le> snd p2)"
       
    11 definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
    11 
    12 
    12 instance
    13 instance
    13 proof
    14 proof
    14   case goal1 show ?case by(simp add: le_prod_def)
    15   case goal1 show ?case by(rule less_prod_def)
    15 next
    16 next
    16   case goal2 thus ?case unfolding le_prod_def by(metis le_trans)
    17   case goal2 show ?case by(simp add: less_eq_prod_def)
       
    18 next
       
    19   case goal3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
       
    20 next
       
    21   case goal4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
    17 qed
    22 qed
    18 
    23 
    19 end
    24 end
    20 
    25 
    21 
    26 
    22 subsection "Backward Analysis of Expressions"
    27 subsection "Backward Analysis of Expressions"
    23 
    28 
    24 class lattice = semilattice + bot +
    29 class lattice = semilattice + bot +
    25 fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
    30 fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
    26 assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    31 assumes meet_le1 [simp]: "x \<sqinter> y \<le> x"
    27 and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    32 and meet_le2 [simp]: "x \<sqinter> y \<le> y"
    28 and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    33 and meet_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
    29 begin
    34 begin
    30 
    35 
    31 lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
    36 lemma mono_meet: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> x \<sqinter> y \<le> x' \<sqinter> y'"
    32 by (metis meet_greatest meet_le1 meet_le2 le_trans)
    37 by (metis meet_greatest meet_le1 meet_le2 order_trans)
    33 
    38 
    34 end
    39 end
    35 
    40 
    36 locale Val_abs1_gamma =
    41 locale Val_abs1_gamma =
    37   Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set" +
    42   Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::lattice \<Rightarrow> val set" +
    81 
    86 
    82 fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
    87 fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
    83 "afilter (N n) a S = (if test_num' n a then S else None)" |
    88 "afilter (N n) a S = (if test_num' n a then S else None)" |
    84 "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
    89 "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
    85   let a' = fun S x \<sqinter> a in
    90   let a' = fun S x \<sqinter> a in
    86   if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
    91   if a' = \<bottom> then None else Some(update S x a'))" |
    87 "afilter (Plus e1 e2) a S =
    92 "afilter (Plus e1 e2) a S =
    88  (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    93  (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    89   in afilter e1 a1 (afilter e2 a2 S))"
    94   in afilter e1 a1 (afilter e2 a2 S))"
    90 
    95 
    91 text{* The test for @{const bot} in the @{const V}-case is important: @{const
    96 text{* The test for @{const bot} in the @{const V}-case is important: @{const
   108   (let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
   113   (let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
   109    in afilter e1 a1 (afilter e2 a2 S))"
   114    in afilter e1 a1 (afilter e2 a2 S))"
   110 
   115 
   111 lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
   116 lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
   112 by(induction e arbitrary: a S)
   117 by(induction e arbitrary: a S)
   113   (auto simp: Let_def update_def L_st_def
   118   (auto simp: Let_def L_st_def split: option.splits prod.split)
   114            split: option.splits prod.split)
       
   115 
   119 
   116 lemma afilter_sound: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
   120 lemma afilter_sound: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
   117   s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
   121   s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
   118 proof(induction e arbitrary: a S)
   122 proof(induction e arbitrary: a S)
   119   case N thus ?case by simp (metis test_num')
   123   case N thus ?case by simp (metis test_num')
   187     by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
   191     by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
   188 next
   192 next
   189   case Seq thus ?case by auto
   193   case Seq thus ?case by auto
   190 next
   194 next
   191   case (If b _ C1 _ C2)
   195   case (If b _ C1 _ C2)
   192   hence 0: "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
   196   hence 0: "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
   193     by(simp, metis post_in_L join_ge1 join_ge2)
   197     by(simp, metis post_in_L join_ge1 join_ge2)
   194   have "vars b \<subseteq> X" using If.prems by simp
   198   have "vars b \<subseteq> X" using If.prems by simp
   195   note vars = `S \<in> L X` `vars b \<subseteq> X`
   199   note vars = `S \<in> L X` `vars b \<subseteq> X`
   196   show ?case using If 0
   200   show ?case using If 0
   197     by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
   201     by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
   202     by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
   206     by (auto simp: mono_gamma_o bfilter_sound[OF vars] bfilter_in_L[OF vars])
   203 qed
   207 qed
   204 
   208 
   205 lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
   209 lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
   206 proof(induction C arbitrary: S)
   210 proof(induction C arbitrary: S)
   207   case Assign thus ?case by(simp add: L_option_def L_st_def update_def split: option.splits)
   211   case Assign thus ?case by(auto simp add: L_option_def L_st_def split: option.splits)
   208 qed (auto simp add: bfilter_in_L)
   212 qed (auto simp add: bfilter_in_L)
   209 
   213 
   210 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
   214 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
   211 proof(simp add: CS_def AI_def)
   215 proof(simp add: CS_def AI_def)
   212   assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
   216   assume 1: "pfp (step' (Top(vars c))) (bot c) = Some C"
   213   have "C \<in> L(vars c)"
   217   have "C \<in> L(vars c)"
   214     by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
   218     by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
   215       (erule step'_in_L[OF _ top_in_L])
   219       (erule step'_in_L[OF _ Top_in_L])
   216   have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
   220   have pfp': "step' (Top(vars c)) C \<le> C" by(rule pfp_pfp[OF 1])
   217   have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   221   have 2: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   218   proof(rule order_trans)
   222   proof(rule order_trans)
   219     show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
   223     show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (Top(vars c)) C)"
   220       by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
   224       by(rule step_step'[OF `C \<in> L(vars c)` Top_in_L])
   221     show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
   225     show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
   222       by(rule mono_gamma_c[OF pfp'])
   226       by(rule mono_gamma_c[OF pfp'])
   223   qed
   227   qed
   224   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
   228   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
   225   have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
   229   have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
   226     by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
   230     by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
   227   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
   231   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
   228 qed
   232 qed
   229 
   233 
   230 end
   234 end
   231 
   235 
   232 
   236 
   233 subsubsection "Monotonicity"
   237 subsubsection "Monotonicity"
   234 
   238 
   235 locale Abs_Int1_mono = Abs_Int1 +
   239 locale Abs_Int1_mono = Abs_Int1 +
   236 assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
   240 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
   237 and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
   241 and mono_filter_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
   238   filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
   242   filter_plus' r a1 a2 \<le> filter_plus' r' b1 b2"
   239 and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
   243 and mono_filter_less': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow>
   240   filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
   244   filter_less' bv a1 a2 \<le> filter_less' bv b1 b2"
   241 begin
   245 begin
   242 
   246 
   243 lemma mono_aval':
   247 lemma mono_aval':
   244   "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
   248   "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<le> aval' e S2"
   245 by(induction e) (auto simp: le_st_def mono_plus' L_st_def)
   249 by(induction e) (auto simp: less_eq_st_def mono_plus' L_st_def)
   246 
   250 
   247 lemma mono_aval'':
   251 lemma mono_aval'':
   248   "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<sqsubseteq> aval'' e S2"
   252   "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
   249 apply(cases S1)
   253 apply(cases S1)
   250  apply simp
   254  apply simp
   251 apply(cases S2)
   255 apply(cases S2)
   252  apply simp
   256  apply simp
   253 by (simp add: mono_aval')
   257 by (simp add: mono_aval')
   254 
   258 
   255 lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
   259 lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
   256   r1 \<sqsubseteq> r2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> afilter e r1 S1 \<sqsubseteq> afilter e r2 S2"
   260   r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> afilter e r1 S1 \<le> afilter e r2 S2"
   257 apply(induction e arbitrary: r1 r2 S1 S2)
   261 apply(induction e arbitrary: r1 r2 S1 S2)
   258 apply(auto simp: test_num' Let_def mono_meet split: option.splits prod.splits)
   262 apply(auto simp: test_num' Let_def mono_meet split: option.splits prod.splits)
   259 apply (metis mono_gamma subsetD)
   263 apply (metis mono_gamma subsetD)
   260 apply(drule (2) mono_fun_L)
   264 apply(drule (2) mono_fun_L)
   261 apply (metis mono_meet le_trans)
   265 apply (metis mono_meet le_bot)
   262 apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)
   266 apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
   263 done
   267 done
   264 
   268 
   265 lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
   269 lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
   266   S1 \<sqsubseteq> S2 \<Longrightarrow> bfilter b bv S1 \<sqsubseteq> bfilter b bv S2"
   270   S1 \<le> S2 \<Longrightarrow> bfilter b bv S1 \<le> bfilter b bv S2"
   267 apply(induction b arbitrary: bv S1 S2)
   271 apply(induction b arbitrary: bv S1 S2)
   268 apply(simp)
   272 apply(simp)
   269 apply(simp)
   273 apply(simp)
   270 apply simp
   274 apply simp
   271 apply(metis join_least le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] bfilter_in_L)
   275 apply(metis join_least order_trans[OF _ join_ge1] order_trans[OF _ join_ge2] bfilter_in_L)
   272 apply (simp split: prod.splits)
   276 apply (simp split: prod.splits)
   273 apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)
   277 apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
   274 done
   278 done
   275 
   279 
   276 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   280 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   277   S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
   281   S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
   278 apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
   282 apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
   279 apply (auto simp: Let_def mono_bfilter mono_aval' mono_post
   283 apply (auto simp: Let_def mono_bfilter mono_aval' mono_post
   280   le_join_disj le_join_disj[OF  post_in_L post_in_L] bfilter_in_L
   284   le_join_disj le_join_disj[OF  post_in_L post_in_L] bfilter_in_L
   281             split: option.split)
   285             split: option.split)
   282 done
   286 done
   283 
   287 
   284 lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   288 lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   285   C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top X) C1 \<sqsubseteq> step' (top X) C2"
   289   C1 \<le> C2 \<Longrightarrow> step' (Top X) C1 \<le> step' (Top X) C2"
   286 by (metis top_in_L mono_step' preord_class.le_refl)
   290 by (metis Top_in_L mono_step' order_refl)
   287 
   291 
   288 end
   292 end
   289 
   293 
   290 end
   294 end