src/HOL/IMP/Abs_Int2.thy
 changeset 51359 00b45c7e831f parent 51037 0a6d84c41dbf child 51389 8a9f0503b1c0
equal 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`