# HG changeset patch # User nipkow # Date 1318403790 -7200 # Node ID d2eb07a1e01b71c4276b6c5ac537522e4d1b3e0f # Parent fc3bb3a42369dbad61debc5a23fb12adf867dbf5 separated monotonicity reasoning and defined narrowing with while_option diff -r fc3bb3a42369 -r d2eb07a1e01b src/HOL/IMP/Abs_Int0.thy --- a/src/HOL/IMP/Abs_Int0.thy Mon Oct 10 20:14:25 2011 +0200 +++ b/src/HOL/IMP/Abs_Int0.thy Wed Oct 12 09:16:30 2011 +0200 @@ -9,10 +9,7 @@ text{* Abstract interpretation over type @{text astate} instead of functions. *} -locale Abs_Int = Val_abs + -fixes pfp :: "('a st up acom \ 'a st up acom) \ 'a st up acom \ 'a st up acom" -assumes pfp: "\c. strip(f c) = strip c \ f(pfp f c) \ pfp f c" -and strip_pfp: "\c. strip(f c) = strip c \ strip(pfp f c) = strip c" +locale Abs_Int = Val_abs begin fun aval' :: "aexp \ 'a st \ 'a" where @@ -31,27 +28,15 @@ "step S ({Inv} WHILE b DO c {P}) = {S \ post c} WHILE b DO step Inv c {Inv}" +definition AI :: "com \ 'a st up acom option" where +"AI = lpfp\<^isub>c (step \)" + + lemma strip_step[simp]: "strip(step S c) = strip c" by(induct c arbitrary: S) (simp_all add: Let_def) -definition AI :: "com \ 'a st up acom" where -"AI c = pfp (step Top) (bot_acom c)" - -subsubsection "Monotonicity" - -lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" -by(induction e) (auto simp: le_st_def lookup_def mono_plus') - -lemma mono_update: "a \ a' \ S \ S' \ update S x a \ update S' x a'" -by(auto simp add: le_st_def lookup_def update_def) - -lemma step_mono: "S \ S' \ step S c \ step S' c" -apply(induction c arbitrary: S S') -apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split) -done - -subsubsection "Soundness" +text{* Soundness: *} lemma aval'_sound: "s <:f S \ aval a s <: aval' a S" by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def) @@ -92,10 +77,29 @@ by simp (metis `s <:up S` `S \ Inv` `Inv \ P` up_fun_in_rep_le) qed -lemma AI_sound: "(c,s) \ t \ t <:up post(AI c)" -by(fastforce simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp) +lemma AI_sound: "\ AI c = Some c'; (c,s) \ t \ \ t <:up post c'" +by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step) end +subsubsection "Monotonicity" + +locale Abs_Int_mono = Abs_Int + +assumes mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" +begin + +lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" +by(induction e) (auto simp: le_st_def lookup_def mono_plus') + +lemma mono_update: "a \ a' \ S \ S' \ update S x a \ update S' x a'" +by(auto simp add: le_st_def lookup_def update_def) + +lemma step_mono: "S \ S' \ step S c \ step S' c" +apply(induction c arbitrary: S S') +apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split) +done + end + +end diff -r fc3bb3a42369 -r d2eb07a1e01b src/HOL/IMP/Abs_Int0_const.thy --- a/src/HOL/IMP/Abs_Int0_const.thy Mon Oct 10 20:14:25 2011 +0200 +++ b/src/HOL/IMP/Abs_Int0_const.thy Wed Oct 12 09:16:30 2011 +0200 @@ -51,33 +51,25 @@ end -interpretation Rep rep_cval + +interpretation Val_abs rep_cval Const plus_cval proof case goal1 thus ?case by(cases a, cases b, simp, simp, cases b, simp, simp) next case goal2 show ?case by(simp add: Top_cval_def) -qed - -interpretation Val_abs rep_cval Const plus_cval -proof - case goal1 show ?case by simp next - case goal2 thus ?case - by(auto simp: plus_cval_cases split: cval.split) + case goal3 show ?case by simp next - case goal3 thus ?case + case goal4 thus ?case by(auto simp: plus_cval_cases split: cval.split) qed -text{* Could set the limit of the number of iterations to an arbitrarily -large number because all ascending chains in this semilattice are finite. *} - -interpretation Abs_Int rep_cval Const plus_cval "(iter 15)" +interpretation Abs_Int rep_cval Const plus_cval defines AI_const is AI and aval'_const is aval' and step_const is step -proof qed (auto simp: iter_pfp strip_iter) +proof qed text{* Straight line code: *} definition "test1_const = @@ -113,28 +105,20 @@ WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')" -text{* For readability: *} -translations "x" <= "CONST V x" -translations "x" <= "CONST N x" -translations "x" <= "CONST Const x" -translations "x < y" <= "CONST Less x y" -translations "x" <= "CONST B x" -translations "x" <= "CONST Up x" - value [code] "show_acom (((step_const \)^^0) (\\<^sub>c test1_const))" value [code] "show_acom (((step_const \)^^1) (\\<^sub>c test1_const))" value [code] "show_acom (((step_const \)^^2) (\\<^sub>c test1_const))" value [code] "show_acom (((step_const \)^^3) (\\<^sub>c test1_const))" -value [code] "show_acom (AI_const test1_const)" +value [code] "show_acom_opt (AI_const test1_const)" -value [code] "show_acom (AI_const test2_const)" -value [code] "show_acom (AI_const test3_const)" +value [code] "show_acom_opt (AI_const test2_const)" +value [code] "show_acom_opt (AI_const test3_const)" value [code] "show_acom (((step_const \)^^0) (\\<^sub>c test4_const))" value [code] "show_acom (((step_const \)^^1) (\\<^sub>c test4_const))" value [code] "show_acom (((step_const \)^^2) (\\<^sub>c test4_const))" value [code] "show_acom (((step_const \)^^3) (\\<^sub>c test4_const))" -value [code] "show_acom (AI_const test4_const)" +value [code] "show_acom_opt (AI_const test4_const)" value [code] "show_acom (((step_const \)^^0) (\\<^sub>c test5_const))" value [code] "show_acom (((step_const \)^^1) (\\<^sub>c test5_const))" @@ -142,9 +126,17 @@ value [code] "show_acom (((step_const \)^^3) (\\<^sub>c test5_const))" value [code] "show_acom (((step_const \)^^4) (\\<^sub>c test5_const))" value [code] "show_acom (((step_const \)^^5) (\\<^sub>c test5_const))" -value [code] "show_acom (AI_const test5_const)" +value [code] "show_acom_opt (AI_const test5_const)" + +value [code] "show_acom_opt (AI_const test6_const)" +value [code] "show_acom_opt (AI_const test7_const)" -value [code] "show_acom (AI_const test6_const)" -value [code] "show_acom (AI_const test7_const)" +text{* Monotonicity: *} + +interpretation Abs_Int_mono rep_cval Const plus_cval +proof + case goal1 thus ?case + by(auto simp: plus_cval_cases split: cval.split) +qed end diff -r fc3bb3a42369 -r d2eb07a1e01b src/HOL/IMP/Abs_Int0_fun.thy --- a/src/HOL/IMP/Abs_Int0_fun.thy Mon Oct 10 20:14:25 2011 +0200 +++ b/src/HOL/IMP/Abs_Int0_fun.thy Wed Oct 12 09:16:30 2011 +0200 @@ -4,6 +4,7 @@ theory Abs_Int0_fun imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step + "~~/src/HOL/Library/While_Combinator" begin subsection "Annotated Commands" @@ -155,15 +156,6 @@ end -definition Top_acom :: "com \ ('a::SL_top) acom" ("\\<^sub>c") where -"\\<^sub>c = anno \" - -lemma strip_Top_acom[simp]: "strip (\\<^sub>c c) = c" -by(simp add: Top_acom_def) - -lemma le_Top_acomp[simp]: "strip c' = c \ c' \ \\<^sub>c c" -by(induct c' arbitrary: c) (auto simp: Top_acom_def) - subsubsection "Lifting" @@ -216,23 +208,69 @@ lemma strip_bot_acom[simp]: "strip(\\<^sub>c c) = c" by(simp add: bot_acom_def) +lemma bot_acom[rule_format]: "strip c' = c \ \\<^sub>c c \ c'" +apply(induct c arbitrary: c') +apply (simp_all add: bot_acom_def) + apply(induct_tac c') + apply simp_all + apply(induct_tac c') + apply simp_all + apply(induct_tac c') + apply simp_all + apply(induct_tac c') + apply simp_all + apply(induct_tac c') + apply simp_all +done -subsection "Absract Interpretation" + +subsubsection "Post-fixed point iteration" -text{* The representation of abstract by a set of concrete values: *} +definition + pfp :: "(('a::preord) \ 'a) \ 'a \ 'a option" where +"pfp f = while_option (\x. \ f x \ x) f" + +lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \ x" +using while_option_stop[OF assms[simplified pfp_def]] by simp -locale Rep = -fixes rep :: "'a::SL_top \ 'b set" -assumes le_rep: "a \ b \ rep a \ rep b" -and rep_Top: "rep \ = UNIV" -begin +lemma pfp_least: +assumes mono: "\x y. x \ y \ f x \ f y" +and "f p \ p" and "x0 \ p" and "pfp f x0 = Some x" shows "x \ p" +proof- + { fix x assume "x \ p" + hence "f x \ f p" by(rule mono) + from this `f p \ p` have "f x \ p" by(rule le_trans) + } + thus "x \ p" using assms(2-) while_option_rule[where P = "%x. x \ p"] + unfolding pfp_def by blast +qed + +definition + lpfp\<^isub>c :: "(('a::SL_top)up acom \ 'a up acom) \ com \ 'a up acom option" where +"lpfp\<^isub>c f c = pfp f (\\<^sub>c c)" + +lemma lpfpc_pfp: "lpfp\<^isub>c f c0 = Some c \ f c \ c" +by(simp add: pfp_pfp lpfp\<^isub>c_def) -abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a" +lemma strip_pfp: +assumes "\x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" +using assms while_option_rule[where P = "%x. g x = g x0" and c = f] +unfolding pfp_def by metis + +lemma strip_lpfpc: assumes "\c. strip(f c) = strip c" and "lpfp\<^isub>c f c = Some c'" +shows "strip c' = c" +using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp\<^isub>c_def]] +by(metis strip_bot_acom) -lemma in_rep_Top[simp]: "x <: \" -by(simp add: rep_Top) +lemma lpfpc_least: +assumes mono: "\x y. x \ y \ f x \ f y" +and "strip p = c0" and "f p \ p" and lp: "lpfp\<^isub>c f c0 = Some c" shows "c \ p" +using pfp_least[OF _ _ bot_acom[OF `strip p = c0`] lp[simplified lpfp\<^isub>c_def]] + mono `f p \ p` +by blast -end + +subsection "Abstract Interpretation" definition rep_fun :: "('a \ 'b set) \ ('c \ 'a) \ ('c \ 'b)set" where "rep_fun rep F = {f. \x. f x \ rep(F x)}" @@ -243,72 +281,28 @@ text{* The interface for abstract values: *} -(* FIXME: separate Rep interface needed? *) -locale Val_abs = Rep rep for rep :: "'a::SL_top \ val set" + +locale Val_abs = +fixes rep :: "'a::SL_top \ val set" + assumes le_rep: "a \ b \ rep a \ rep b" + and rep_Top: "rep \ = UNIV" fixes num' :: "val \ 'a" and plus' :: "'a \ 'a \ 'a" -assumes rep_num': "n <: num' n" -and rep_plus': "n1 <: a1 \ n2 <: a2 \ n1+n2 <: plus' a1 a2" -and mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" - - -subsubsection "Post-fixed point iteration" - -fun iter :: "nat \ (('a::SL_top) acom \ 'a acom) \ 'a acom \ 'a acom" where -"iter 0 f c = \\<^sub>c (strip c)" | -"iter (Suc n) f c = (let fc = f c in if fc \ c then c else iter n f fc)" -(* code lemma?? *) - -lemma strip_iter: assumes "\c. strip(f c) = strip c" -shows "strip(iter n f c) = strip c" -apply (induction n arbitrary: c) - apply (metis iter.simps(1) strip_Top_acom) -apply (simp add:Let_def) -by (metis assms) - -lemma iter_pfp: assumes "\c. strip(f c) = strip c" -shows "f(iter n f c) \ iter n f c" -apply (induction n arbitrary: c) - apply(simp add: assms) -apply (simp add:Let_def) -done + assumes rep_num': "n : rep(num' n)" + and rep_plus': + "n1 : rep a1 \ n2 : rep a2 \ n1+n2 : rep(plus' a1 a2)" +begin -lemma iter_funpow: assumes "\c. strip(f c) = strip c" -shows "iter n f x \ \\<^sub>c (strip x) \ \k. iter n f x = (f^^k) x" -apply(induction n arbitrary: x) - apply simp -apply (auto simp: Let_def assms) - apply(metis funpow.simps(1) id_def) -by (metis assms funpow.simps(2) funpow_swap1 o_apply) - -text{* For monotone @{text f}, @{term "iter f n x0"} yields the least -post-fixed point above @{text x0}, unless it yields @{text Top}. *} +abbreviation in_rep (infix "<:" 50) + where "x <: a == x : rep a" -lemma iter_least_pfp: -assumes strip: "\c. strip(f c) = strip c" -and mono: "\x y. x \ y \ f x \ f y" -and not_top: "iter n f x0 \ \\<^sub>c (strip x0)" -and "f p \ p" and "x0 \ p" shows "iter n f x0 \ p" -proof- - obtain k where "iter n f x0 = (f^^k) x0" - using iter_funpow[OF strip not_top] by blast - moreover - { fix n have "(f^^n) x0 \ p" - proof(induction n) - case 0 show ?case by(simp add: `x0 \ p`) - next - case (Suc n) thus ?case - by (simp add: `x0 \ p`)(metis Suc `f p \ p` le_trans mono) - qed - } ultimately show ?thesis by simp -qed +lemma in_rep_Top[simp]: "x <: \" +by(simp add: rep_Top) + +end type_synonym 'a st = "(name \ 'a)" -locale Abs_Int_Fun = Val_abs + -fixes pfp :: "('a st up acom \ 'a st up acom) \ 'a st up acom \ 'a st up acom" -assumes pfp: "f(pfp f c) \ pfp f c" -and strip_pfp: "\c. strip(f c) = strip c \ strip(pfp f c) = strip c" +locale Abs_Int_Fun = Val_abs begin fun aval' :: "aexp \ 'a st \ 'a" where @@ -316,24 +310,26 @@ "aval' (V x) S = S x" | "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" -fun step :: "'a st up \ 'a st up acom \ 'a st up acom" where +fun step :: "'a st up \ 'a st up acom \ 'a st up acom" + where "step S (SKIP {P}) = (SKIP {S})" | "step S (x ::= e {P}) = x ::= e {case S of Bot \ Bot | Up S \ Up(S(x := aval' e S))}" | "step S (c1; c2) = step S c1; step (post c1) c2" | "step S (IF b THEN c1 ELSE c2 {P}) = - (let c1' = step S c1; c2' = step S c2 - in IF b THEN c1' ELSE c2' {post c1 \ post c2})" | + IF b THEN step S c1 ELSE step S c2 {post c1 \ post c2}" | "step S ({Inv} WHILE b DO c {P}) = {S \ post c} WHILE b DO (step Inv c) {Inv}" +definition AI :: "com \ 'a st up acom option" where +"AI = lpfp\<^isub>c (step \)" + + lemma strip_step[simp]: "strip(step S c) = strip c" by(induct c arbitrary: S) (simp_all add: Let_def) -definition AI :: "com \ 'a st up acom" where -"AI c = pfp (step \) (\\<^sub>c c)" - +text{*Lifting @{text "<:"} to other types: *} abbreviation fun_in_rep :: "state \ 'a st \ bool" (infix "<:f" 50) where "s <:f S == s \ rep_fun rep S" @@ -358,20 +354,7 @@ by(simp add: Top_up_def in_rep_Top_fun) -subsubsection "Monotonicity" - -lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" -by(induction e)(auto simp: le_fun_def mono_plus') - -lemma mono_update: "a \ a' \ S \ S' \ S(x := a) \ S'(x := a')" -by(simp add: le_fun_def) - -lemma step_mono: "S \ S' \ step S c \ step S' c" -apply(induction c arbitrary: S S') -apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split) -done - -subsubsection "Soundness" +text{* Soundness: *} lemma aval'_sound: "s <:f S \ aval a s <: aval' a S" by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def) @@ -380,7 +363,8 @@ by(simp add: rep_fun_def) lemma step_sound: - "step S c \ c \ (strip c,s) \ t \ s <:up S \ t <:up post c" + "\ step S c \ c; (strip c,s) \ t; s <:up S \ + \ t <:up post c" proof(induction c arbitrary: S s t) case SKIP thus ?case by simp (metis skipE up_fun_in_rep_le) @@ -412,8 +396,29 @@ by simp (metis `s <:up S` `S \ Inv` `Inv \ P` up_fun_in_rep_le) qed -lemma AI_sound: "(c,s) \ t \ t <:up post(AI c)" -by(auto simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp) +lemma AI_sound: + "\ AI c = Some c'; (c,s) \ t \ \ t <:up post c'" +by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step) + +end + + +subsubsection "Monotonicity" + +locale Abs_Int_Fun_mono = Abs_Int_Fun + +assumes mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" +begin + +lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" +by(induction e)(auto simp: le_fun_def mono_plus') + +lemma mono_update: "a \ a' \ S \ S' \ S(x := a) \ S'(x := a')" +by(simp add: le_fun_def) + +lemma step_mono: "S \ S' \ step S c \ step S' c" +apply(induction c arbitrary: S S') +apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split) +done end diff -r fc3bb3a42369 -r d2eb07a1e01b src/HOL/IMP/Abs_Int1.thy --- a/src/HOL/IMP/Abs_Int1.thy Mon Oct 10 20:14:25 2011 +0200 +++ b/src/HOL/IMP/Abs_Int1.thy Wed Oct 12 09:16:30 2011 +0200 @@ -30,10 +30,19 @@ and meet_le2 [simp]: "x \ y \ y" and meet_greatest: "x \ y \ x \ z \ x \ y \ z" assumes bot[simp]: "\ \ x" +begin -locale Rep1 = Rep rep for rep :: "'a::L_top_bot \ 'b set" + -assumes inter_rep_subset_rep_meet: "rep a1 \ rep a2 \ rep(a1 \ a2)" - -- "this means the meet is precise" +lemma mono_meet: "x \ x' \ y \ y' \ x \ y \ x' \ y'" +by (metis meet_greatest meet_le1 meet_le2 le_trans) + +end + + +locale Val_abs1_rep = + Val_abs rep num' plus' + for rep :: "'a::L_top_bot \ val set" and num' plus' + +assumes inter_rep_subset_rep_meet: + "rep a1 \ rep a2 \ rep(a1 \ a2)" and rep_Bot: "rep \ = {}" begin @@ -43,29 +52,19 @@ lemma rep_meet[simp]: "rep(a1 \ a2) = rep a1 \ rep a2" by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2) -lemma mono_meet: "x \ x' \ y \ y' \ x \ y \ x' \ y'" -by (metis meet_greatest meet_le1 meet_le2 le_trans) - end -locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep - for rep :: "'a::L_top_bot \ int set" and num' plus' + +locale Val_abs1 = Val_abs1_rep + fixes filter_plus' :: "'a \ 'a \ 'a \ 'a * 'a" and filter_less' :: "bool \ 'a \ 'a \ 'a * 'a" assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \ n1 <: a1 \ n2 <: a2 \ n1+n2 <: a \ n1 <: a1' \ n2 <: a2'" and filter_less': "filter_less' (n1 n1 <: a1 \ n2 <: a2 \ n1 <: a1' \ n2 <: a2'" -and mono_filter_plus': "a1 \ b1 \ a2 \ b2 \ r \ r' \ - filter_plus' r a1 a2 \ filter_plus' r' b1 b2" -and mono_filter_less': "a1 \ b1 \ a2 \ b2 \ - filter_less' bv a1 a2 \ filter_less' bv b1 b2" + -locale Abs_Int1 = Val_abs1 + -fixes pfp :: "('a st up acom \ 'a st up acom) \ 'a st up acom \ 'a st up acom" -assumes pfp: "\c. strip(f c) = strip c \ mono f \ f(pfp f c) \ pfp f c" -and strip_pfp: "\c. strip(f c) = strip c \ strip(pfp f c) = strip c" +locale Abs_Int1 = Val_abs1 begin lemma in_rep_join_UpI: "s <:up S1 | s <:up S2 \ s <:up S1 \ S2" @@ -78,7 +77,9 @@ "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" lemma aval'_sound: "s <:up S \ aval a s <: aval' a S" -by (induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def) +by(induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def) + +subsubsection "Backward analysis" fun afilter :: "aexp \ 'a \ 'a st up \ 'a st up" where "afilter (N n) a S = (if n <: a then S else Bot)" | @@ -141,7 +142,8 @@ qed -fun step :: "'a st up \ 'a st up acom \ 'a st up acom" where +fun step :: "'a st up \ 'a st up acom \ 'a st up acom" + where "step S (SKIP {P}) = (SKIP {S})" | "step S (x ::= e {P}) = x ::= e {case S of Bot \ Bot @@ -155,51 +157,13 @@ WHILE b DO step (bfilter b True Inv) c {bfilter b False Inv}" +definition AI :: "com \ 'a st up acom option" where +"AI = lpfp\<^isub>c (step \)" + lemma strip_step[simp]: "strip(step S c) = strip c" by(induct c arbitrary: S) (simp_all add: Let_def) -definition AI :: "com \ 'a st up acom" where -"AI c = pfp (step \) (\\<^sub>c c)" - - -subsubsection "Monotonicity" - -lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" -apply(cases S) - apply simp -apply(cases S') - apply simp -apply simp -by(induction e) (auto simp: le_st_def lookup_def mono_plus') - -lemma mono_afilter: "r \ r' \ S \ S' \ afilter e r S \ afilter e r' S'" -apply(induction e arbitrary: r r' S S') -apply(auto simp: Let_def split: up.splits prod.splits) -apply (metis le_rep subsetD) -apply(drule_tac x = "list" in mono_lookup) -apply (metis mono_meet le_trans) -apply (metis mono_meet mono_lookup mono_update le_trans) -apply(metis mono_aval' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv) -done - -lemma mono_bfilter: "S \ S' \ bfilter b r S \ bfilter b r S'" -apply(induction b arbitrary: r S S') -apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits) -apply(metis mono_aval' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv) -done - - -lemma post_le_post: "c \ c' \ post c \ post c'" -by (induction c c' rule: le_acom.induct) simp_all - -lemma mono_step: "S \ S' \ c \ c' \ step S c \ step S' c'" -apply(induction c c' arbitrary: S S' rule: le_acom.induct) -apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj - split: up.split) -done - - subsubsection "Soundness" lemma in_rep_update: "\ s <:f S; i <: a \ \ s(x := i) <:f update S x a" @@ -257,9 +221,59 @@ show ?case using `\ bval b t` by simp qed -lemma AI_sound: "(c,s) \ t \ t <:up post(AI c)" -by(fastforce simp: AI_def strip_pfp mono_def in_rep_Top_up - intro: step_sound pfp mono_step[OF le_refl]) +lemma AI_sound: "\ AI c = Some c'; (c,s) \ t \ \ t <:up post c'" +unfolding AI_def +by (metis in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step) +(* +by(metis step_sound[of "\" c' s t] strip_lpfp strip_step + lpfp_pfp mono_def mono_step[OF le_refl] in_rep_Top_up) +*) +end + + +subsubsection "Monotonicity" + +locale Abs_Int1_mono = Abs_Int1 + +assumes mono_plus': "a1 \ b1 \ a2 \ b2 \ plus' a1 a2 \ plus' b1 b2" +and mono_filter_plus': "a1 \ b1 \ a2 \ b2 \ r \ r' \ + filter_plus' r a1 a2 \ filter_plus' r' b1 b2" +and mono_filter_less': "a1 \ b1 \ a2 \ b2 \ + filter_less' bv a1 a2 \ filter_less' bv b1 b2" +begin + +lemma mono_aval': "S \ S' \ aval' e S \ aval' e S'" +apply(cases S) + apply simp +apply(cases S') + apply simp +apply simp +by(induction e) (auto simp: le_st_def lookup_def mono_plus') + +lemma mono_afilter: "r \ r' \ S \ S' \ afilter e r S \ afilter e r' S'" +apply(induction e arbitrary: r r' S S') +apply(auto simp: Let_def split: up.splits prod.splits) +apply (metis le_rep subsetD) +apply(drule_tac x = "list" in mono_lookup) +apply (metis mono_meet le_trans) +apply (metis mono_meet mono_lookup mono_update le_trans) +apply(metis mono_aval' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv) +done + +lemma mono_bfilter: "S \ S' \ bfilter b r S \