src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy

proper syntax;

(* Author: Tobias Nipkow *)

theory Abs_Int_den2
imports Abs_Int_den1_ivl
begin

context preord
begin

definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"

lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)

lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
by(simp add: mono_def)

declare le_trans[trans]

end


subsection "Widening and Narrowing"

text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
a trivial widening step. We generalise this idea and complement it with
narrowing, a process to regain precision.

Class @{text WN} makes some assumptions about the widening and narrowing
operators. The assumptions serve two purposes. Together with a further
assumption that certain chains become stationary, they permit to prove
termination of the fixed point iteration, which we do not --- we limit the
number of iterations as before. The second purpose of the narrowing
assumptions is to prove that the narrowing iteration keeps on producing
post-fixed points and that it goes down. However, this requires the function
being iterated to be monotone. Unfortunately, abstract interpretation with
widening is not monotone. Hence the (recursive) abstract interpretation of a
loop body that again contains a loop may result in a non-monotone
function. Therefore our narrowing iteration needs to check at every step
that a post-fixed point is maintained, and we cannot prove that the precision
increases. *}

class WN = SL_top +
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
assumes widen: "y \<sqsubseteq> x \<nabla> y"
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
begin

fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
"iter_up f 0 x = Top" |
"iter_up f (Suc n) x =
  (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"

lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
apply (induction n arbitrary: x)
 apply (simp)
apply (simp add: Let_def)
done

fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
"iter_down f 0 x = x" |
"iter_down f (Suc n) x =
  (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"

lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
apply (induction n arbitrary: x)
 apply (simp)
apply (simp add: Let_def)
done

definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
"iter' m n f x =
  (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"

lemma iter'_pfp_above:
shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
and "x0 \<sqsubseteq> iter' m n f x0"
using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
by(auto simp add: iter'_def Let_def)

text{* This is how narrowing works on monotone functions: you just iterate. *}

abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"

text{* Narrowing always yields a post-fixed point: *}

lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
defines "x n == iter_down_mono f n x0"
shows "f(x n) \<sqsubseteq> x n"
proof (induction n)
  case 0 show ?case by (simp add: x_def assms(2))
next
  case (Suc n)
  have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
  also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
  also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
  also have "\<dots> = x(Suc n)" by(simp add: x_def)
  finally show ?case .
qed

text{* Narrowing can only increase precision: *}

lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
defines "x n == iter_down_mono f n x0"
shows "x n \<sqsubseteq> x0"
proof (induction n)
  case 0 show ?case by(simp add: x_def)
next
  case (Suc n)
  have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
  also have "\<dots> \<sqsubseteq> x n" unfolding x_def
    by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
  also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
  finally show ?case .
qed


end


instantiation ivl :: WN
begin

definition "widen_ivl ivl1 ivl2 =
  ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
     case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
       I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
         (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"

definition "narrow_ivl ivl1 ivl2 =
  ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
     case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
       I (if l1 = None then l2 else l1)
         (if h1 = None then h2 else h1))"

instance
proof qed
  (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)

end

instantiation astate :: (WN) WN
begin

definition "widen_astate F1 F2 =
  FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"

definition "narrow_astate F1 F2 =
  FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"

instance
proof
  case goal1 thus ?case
    by(simp add: widen_astate_def le_astate_def lookup_def widen)
next
  case goal2 thus ?case
    by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
next
  case goal3 thus ?case
    by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
qed

end

instantiation up :: (WN) WN
begin

fun widen_up where
"widen_up bot x = x" |
"widen_up x bot = x" |
"widen_up (Up x) (Up y) = Up(x \<nabla> y)"

fun narrow_up where
"narrow_up bot x = bot" |
"narrow_up x bot = bot" |
"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"

instance
proof
  case goal1 show ?case
    by(induct x y rule: widen_up.induct) (simp_all add: widen)
next
  case goal2 thus ?case
    by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
next
  case goal3 thus ?case
    by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
qed

end

global_interpretation
  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
defines afilter_ivl' = afilter
and bfilter_ivl' = bfilter
and AI_ivl' = AI
and aval_ivl' = aval'
proof qed (auto simp: iter'_pfp_above)

value "list_up(AI_ivl' test3_ivl Top)"
value "list_up(AI_ivl' test4_ivl Top)"
value "list_up(AI_ivl' test5_ivl Top)"

end