# Theory Abs_Int1

Up to index of Isabelle/HOL/HOL-IMP

theory Abs_Int1
imports Abs_State
`(* Author: Tobias Nipkow *)theory Abs_Int1imports Abs_Statebeginlemma le_iff_le_annos_zip: "C1 \<sqsubseteq> C2 <-> (∀ (a1,a2) ∈ set(zip (annos C1) (annos C2)). a1 \<sqsubseteq> a2) ∧ strip C1 = strip C2"by(induct C1 C2 rule: le_acom.induct) (auto simp: size_annos_same2)lemma le_iff_le_annos: "C1 \<sqsubseteq> C2 <->  strip C1 = strip C2 ∧ (∀ i<size(annos C1). annos C1 ! i \<sqsubseteq> annos C2 ! i)"by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)lemma mono_fun_L[simp]: "F ∈ L X ==> F \<sqsubseteq> G ==> x : X ==> fun F x \<sqsubseteq> fun G x"by(simp add: mono_fun L_st_def)lemma bot_in_L[simp]: "bot c ∈ L(vars c)"by(simp add: L_acom_def bot_def)lemma L_acom_simps[simp]: "SKIP {P} ∈ L X <-> P ∈ L X"  "(x ::= e {P}) ∈ L X <-> x : X ∧ vars e ⊆ X ∧ P ∈ L X"  "(C1;C2) ∈ L X <-> C1 ∈ L X ∧ C2 ∈ L X"  "(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) ∈ L X <->   vars b ⊆ X ∧ C1 ∈ L X ∧ C2 ∈ L X ∧ P1 ∈ L X ∧ P2 ∈ L X ∧ Q ∈ L X"  "({I} WHILE b DO {P} C {Q}) ∈ L X <->   I ∈ L X ∧ vars b ⊆ X ∧ P ∈ L X ∧ C ∈ L X ∧ Q ∈ L X"by(auto simp add: L_acom_def)lemma post_in_annos: "post C : set(annos C)"by(induction C) autolemma post_in_L[simp]: "C ∈ L X ==> post C ∈ L X"by(simp add: L_acom_def post_in_annos)subsection "Computable Abstract Interpretation"text{* Abstract interpretation over type @{text st} instead offunctions. *}context Gammabeginfun aval' :: "aexp => 'av st => 'av" where"aval' (N i) S = num' i" |"aval' (V x) S = fun S x" |"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"lemma aval'_sound: "s : γ⇣s S ==> vars a ⊆ dom S ==> aval a s : γ(aval' a S)"by (induction a) (auto simp: gamma_num' gamma_plus' γ_st_def)endtext{* The for-clause (here and elsewhere) only serves the purpose of fixingthe name of the type parameter @{typ 'av} which would otherwise be renamed to@{typ 'a}. *}locale Abs_Int = Gamma where γ=γ for γ :: "'av::semilattice => val set"beginfun step' :: "'av st option => 'av st option acom => 'av st option acom" where"step' S (SKIP {P}) = (SKIP {S})" |"step' S (x ::= e {P}) =  x ::= e {case S of None => None | Some S => Some(update S x (aval' e S))}" |"step' S (C1; C2) = step' S C1; step' (post C1) C2" |"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =  (IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2})" |"step' S ({I} WHILE b DO {P} C {Q}) =   {S \<squnion> post C} WHILE b DO {I} step' P C {I}"definition AI :: "com => 'av st option acom option" where"AI c = pfp (step' (top c)) (bot c)"lemma strip_step'[simp]: "strip(step' S C) = strip C"by(induct C arbitrary: S) (simp_all add: Let_def)text{* Soundness: *}lemma in_gamma_update:  "[| s : γ⇣s S; i : γ a |] ==> s(x := i) : γ⇣s(update S x a)"by(simp add: γ_st_def)lemma step_step': "C ∈ L X ==> S ∈ L X ==> step (γ⇣o S) (γ⇣c C) ≤ γ⇣c (step' S C)"proof(induction C arbitrary: S)  case SKIP thus ?case by autonext  case Assign thus ?case    by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)next  case Seq thus ?case by autonext  case (If b p1 C1 p2 C2 P)  hence "post C1 \<sqsubseteq> post C1 \<squnion> post C2 ∧ post C2 \<sqsubseteq> post C1 \<squnion> post C2"    by(simp, metis post_in_L join_ge1 join_ge2)  thus ?case using If by (auto simp: mono_gamma_o)next  case While thus ?case by (auto simp: mono_gamma_o)qedlemma step'_in_L[simp]:  "[| C ∈ L X; S ∈ L X |] ==> (step' S C) ∈ L X"proof(induction C arbitrary: S)  case Assign thus ?case    by(auto simp: L_st_def update_def split: option.splits)qed autolemma AI_sound: "AI c = Some C ==> CS c ≤ γ⇣c C"proof(simp add: CS_def AI_def)  assume 1: "pfp (step' (top c)) (bot c) = Some C"  have "C ∈ L(vars c)"    by(rule pfp_inv[where P = "%C. C ∈ L(vars c)", OF 1 _ bot_in_L])      (erule step'_in_L[OF _ top_in_L])  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])  have 2: "step (γ⇣o(top c)) (γ⇣c C) ≤ γ⇣c C"  proof(rule order_trans)    show "step (γ⇣o (top c)) (γ⇣c C) ≤  γ⇣c (step' (top c) C)"      by(rule step_step'[OF `C ∈ L(vars c)` top_in_L])    show "γ⇣c (step' (top c) C) ≤ γ⇣c C"      by(rule mono_gamma_c[OF pfp'])  qed  have 3: "strip (γ⇣c C) = c" by(simp add: strip_pfp[OF _ 1])  have "lfp c (step (γ⇣o(top c))) ≤ γ⇣c C"    by(rule lfp_lowerbound[simplified,where f="step (γ⇣o(top c))", OF 3 2])  thus "lfp c (step UNIV) ≤ γ⇣c C" by simpqedendsubsubsection "Monotonicity"lemma le_join_disj: "y ∈ L X ==> (z::_::semilatticeL) ∈ L X ==>  x \<sqsubseteq> y ∨ x \<sqsubseteq> z ==> x \<sqsubseteq> y \<squnion> z"by (metis join_ge1 join_ge2 preord_class.le_trans)locale Abs_Int_mono = Abs_Int +assumes mono_plus': "a1 \<sqsubseteq> b1 ==> a2 \<sqsubseteq> b2 ==> plus' a1 a2 \<sqsubseteq> plus' b1 b2"beginlemma mono_aval':  "S1 \<sqsubseteq> S2 ==> S1 ∈ L X ==> S2 ∈ L X ==> vars e ⊆ X ==> aval' e S1 \<sqsubseteq> aval' e S2"by(induction e) (auto simp: le_st_def mono_plus' L_st_def)theorem mono_step': "S1 ∈ L X ==> S2 ∈ L X ==> C1 ∈ L X ==> C2 ∈ L X ==>  S1 \<sqsubseteq> S2 ==> C1 \<sqsubseteq> C2 ==> step' S1 C1 \<sqsubseteq> step' S2 C2"apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)apply (auto simp: Let_def mono_aval' mono_post  le_join_disj le_join_disj[OF  post_in_L post_in_L]            split: option.split)donelemma mono_step'_top: "C ∈ L(vars c) ==> C' ∈ L(vars c) ==>  C \<sqsubseteq> C' ==> step' (top c) C \<sqsubseteq> step' (top c) C'"by (metis top_in_L mono_step' preord_class.le_refl)lemma pfp_bot_least:assumes "∀x∈L(vars c)∩{C. strip C = c}.∀y∈L(vars c)∩{C. strip C = c}.  x \<sqsubseteq> y --> f x \<sqsubseteq> f y"and "∀C. C ∈ L(vars c)∩{C. strip C = c} --> f C ∈ L(vars c)∩{C. strip C = c}"and "f C' \<sqsubseteq> C'" "strip C' = c" "C' ∈ L(vars c)" "pfp f (bot c) = Some C"shows "C \<sqsubseteq> C'"apply(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])by (simp_all add: assms(4,5) bot_least)lemma AI_least_pfp: assumes "AI c = Some C"and "step' (top c) C' \<sqsubseteq> C'" "strip C' = c" "C' ∈ L(vars c)"shows "C \<sqsubseteq> C'"apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])by (simp_all add: mono_step'_top)endsubsubsection "Termination"abbreviation sqless (infix "\<sqsubset>" 50) where"x \<sqsubset> y == x \<sqsubseteq> y ∧ ¬ y \<sqsubseteq> x"lemma pfp_termination:fixes x0 :: "'a::preord" and m :: "'a => nat"assumes mono: "!!x y. I x ==> I y ==> x \<sqsubseteq> y ==> f x \<sqsubseteq> f y"and m: "!!x y. I x ==> I y ==> x \<sqsubset> y ==> m x > m y"and I: "!!x y. I x ==> I(f x)" and "I x0" and "x0 \<sqsubseteq> f x0"shows "∃x. pfp f x0 = Some x"proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<sqsubseteq> f x"])  show "wf {(y,x). ((I x ∧ x \<sqsubseteq> f x) ∧ ¬ f x \<sqsubseteq> x) ∧ y = f x}"    by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)next  show "I x0 ∧ x0 \<sqsubseteq> f x0" using `I x0` `x0 \<sqsubseteq> f x0` by blastnext  fix x assume "I x ∧ x \<sqsubseteq> f x" thus "I(f x) ∧ f x \<sqsubseteq> f(f x)"    by (blast intro: I mono)qedlocale Measure1 =fixes m :: "'av::preord => nat"fixes h :: "nat"assumes m1: "x \<sqsubseteq> y ==> m x ≥ m y"assumes h: "m x ≤ h"begindefinition m_s :: "'av st => nat" ("m⇣s") where"m_s S = (∑ x ∈ dom S. m(fun S x))"lemma m_s_h: "x ∈ L X ==> finite X ==> m_s x ≤ h * card X"by(simp add: L_st_def m_s_def)  (metis nat_mult_commute of_nat_id setsum_bounded[OF h])lemma m_s1: "S1 \<sqsubseteq> S2 ==> m_s S1 ≥ m_s S2"proof(auto simp add: le_st_def m_s_def)  assume "∀x∈dom S2. fun S1 x \<sqsubseteq> fun S2 x"  hence "∀x∈dom S2. m(fun S1 x) ≥ m(fun S2 x)" by (metis m1)  thus "(∑x∈dom S2. m (fun S2 x)) ≤ (∑x∈dom S2. m (fun S1 x))"    by (metis setsum_mono)qeddefinition m_o :: "nat => 'av st option => nat" ("m⇣o") where"m_o d opt = (case opt of None => h*d+1 | Some S => m_s S)"lemma m_o_h: "ost ∈ L X ==> finite X ==> m_o (card X) ost ≤ (h*card X + 1)"by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h)lemma m_o1: "finite X ==> o1 ∈ L X ==> o2 ∈ L X ==>  o1 \<sqsubseteq> o2 ==> m_o (card X) o1 ≥ m_o (card X) o2"proof(induction o1 o2 rule: le_option.induct)  case 1 thus ?case by (simp add: m_o_def)(metis m_s1)next  case 2 thus ?case    by(simp add: L_option_def m_o_def le_SucI m_s_h split: option.splits)next  case 3 thus ?case by simpqeddefinition m_c :: "'av st option acom => nat" ("m⇣c") where"m_c C = (∑i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"lemma m_c_h: assumes "C ∈ L(vars(strip C))"shows "m_c C ≤ size(annos C) * (h * card(vars(strip C)) + 1)"proof-  let ?X = "vars(strip C)" let ?n = "card ?X" let ?a = "size(annos C)"  { fix i assume "i < ?a"    hence "annos C ! i ∈ L ?X" using assms by(simp add: L_acom_def)    note m_o_h[OF this finite_cvars]  } note 1 = this  have "m_c C = (∑i<?a. m_o ?n (annos C ! i))" by(simp add: m_c_def)  also have "… ≤ (∑i<?a. h * ?n + 1)"    apply(rule setsum_mono) using 1 by simp  also have "… = ?a * (h * ?n + 1)" by simp  finally show ?thesis .qedendlocale Measure = Measure1 +assumes m2: "x \<sqsubset> y ==> m x > m y"beginlemma m_s2: "finite(dom S1) ==> S1 \<sqsubset> S2 ==> m_s S1 > m_s S2"proof(auto simp add: le_st_def m_s_def)  assume "finite(dom S2)" and 0: "∀x∈dom S2. fun S1 x \<sqsubseteq> fun S2 x"  hence 1: "∀x∈dom S2. m(fun S1 x) ≥ m(fun S2 x)" by (metis m1)  fix x assume "x ∈ dom S2" "¬ fun S2 x \<sqsubseteq> fun S1 x"  hence 2: "∃x∈dom S2. m(fun S1 x) > m(fun S2 x)" using 0 m2 by blast  from setsum_strict_mono_ex1[OF `finite(dom S2)` 1 2]  show "(∑x∈dom S2. m (fun S2 x)) < (∑x∈dom S2. m (fun S1 x))" .qedlemma m_o2: "finite X ==> o1 ∈ L X ==> o2 ∈ L X ==>  o1 \<sqsubset> o2 ==> m_o (card X) o1 > m_o (card X) o2"proof(induction o1 o2 rule: le_option.induct)  case 1 thus ?case by (simp add: m_o_def L_st_def m_s2)next  case 2 thus ?case    by(auto simp add: m_o_def le_imp_less_Suc m_s_h)next  case 3 thus ?case by simpqedlemma m_c2: "C1 ∈ L(vars(strip C1)) ==> C2 ∈ L(vars(strip C2)) ==>  C1 \<sqsubset> C2 ==> m_c C1 > m_c C2"proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] L_acom_def)  let ?X = "vars(strip C2)"  let ?n = "card ?X"  assume V1: "∀a∈set(annos C1). a ∈ L ?X"    and V2: "∀a∈set(annos C2). a ∈ L ?X"    and strip_eq: "strip C1 = strip C2"    and 0: "∀i<size(annos C2). annos C1 ! i \<sqsubseteq> annos C2 ! i"  hence 1: "∀i<size(annos C2). m_o ?n (annos C1 ! i) ≥ m_o ?n (annos C2 ! i)"    by (auto simp: all_set_conv_all_nth)       (metis finite_cvars m_o1 size_annos_same2)  fix i assume "i < size(annos C2)" "¬ annos C2 ! i \<sqsubseteq> annos C1 ! i"  hence "m_o ?n (annos C1 ! i) > m_o ?n (annos C2 ! i)" (is "?P i")    by(metis m_o2[OF finite_cvars] V1 V2 nth_mem size_annos_same[OF strip_eq] 0)  hence 2: "∃i < size(annos C2). ?P i" using `i < size(annos C2)` by blast  show "(∑i<size(annos C2). m_o ?n (annos C2 ! i))         < (∑i<size(annos C2). m_o ?n (annos C1 ! i))"    apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)qedendlocale Abs_Int_measure =  Abs_Int_mono where γ=γ + Measure where m=m  for γ :: "'av::semilattice => val set" and m :: "'av => nat"beginlemma AI_Some_measure: "∃C. AI c = Some C"unfolding AI_defapply(rule pfp_termination[where I = "%C. strip C = c ∧ C ∈ L(vars c)"  and m="m_c"])apply(simp_all add: m_c2 mono_step'_top bot_least)doneendend`