src/HOL/IMP/Abs_Int2.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45127 d2eb07a1e01b
child 45623 f682f3f7b726
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Abs_Int2
     4 imports Abs_Int1_ivl
     5 begin
     6 
     7 
     8 subsection "Widening and Narrowing"
     9 
    10 class WN = SL_top +
    11 fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
    12 assumes widen1: "x \<sqsubseteq> x \<nabla> y"
    13 assumes widen2: "y \<sqsubseteq> x \<nabla> y"
    14 fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
    15 assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
    16 assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
    17 
    18 
    19 instantiation ivl :: WN
    20 begin
    21 
    22 definition "widen_ivl ivl1 ivl2 =
    23   ((*if is_empty ivl1 then ivl2 else
    24    if is_empty ivl2 then ivl1 else*)
    25      case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
    26        I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
    27          (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
    28 
    29 definition "narrow_ivl ivl1 ivl2 =
    30   ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
    31      case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
    32        I (if l1 = None then l2 else l1)
    33          (if h1 = None then h2 else h1))"
    34 
    35 instance
    36 proof qed
    37   (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
    38 
    39 end
    40 
    41 instantiation st :: (WN)WN
    42 begin
    43 
    44 definition "widen_st F1 F2 =
    45   FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
    46 
    47 definition "narrow_st F1 F2 =
    48   FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
    49 
    50 instance
    51 proof
    52   case goal1 thus ?case
    53     by(simp add: widen_st_def le_st_def lookup_def widen1)
    54 next
    55   case goal2 thus ?case
    56     by(simp add: widen_st_def le_st_def lookup_def widen2)
    57 next
    58   case goal3 thus ?case
    59     by(auto simp: narrow_st_def le_st_def lookup_def narrow1)
    60 next
    61   case goal4 thus ?case
    62     by(auto simp: narrow_st_def le_st_def lookup_def narrow2)
    63 qed
    64 
    65 end
    66 
    67 instantiation up :: (WN)WN
    68 begin
    69 
    70 fun widen_up where
    71 "widen_up Bot x = x" |
    72 "widen_up x Bot = x" |
    73 "widen_up (Up x) (Up y) = Up(x \<nabla> y)"
    74 
    75 fun narrow_up where
    76 "narrow_up Bot x = Bot" |
    77 "narrow_up x Bot = Bot" |
    78 "narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
    79 
    80 instance
    81 proof
    82   case goal1 show ?case
    83     by(induct x y rule: widen_up.induct) (simp_all add: widen1)
    84 next
    85   case goal2 show ?case
    86     by(induct x y rule: widen_up.induct) (simp_all add: widen2)
    87 next
    88   case goal3 thus ?case
    89     by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
    90 next
    91   case goal4 thus ?case
    92     by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
    93 qed
    94 
    95 end
    96 
    97 fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
    98 "map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
    99 "map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
   100 "map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" |
   101 "map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) =
   102   (IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" |
   103 "map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) =
   104   ({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})"
   105 
   106 abbreviation widen_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<nabla>\<^sub>c" 65)
   107 where "widen_acom == map2_acom (op \<nabla>)"
   108 
   109 abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65)
   110 where "narrow_acom == map2_acom (op \<triangle>)"
   111 
   112 lemma widen1_acom: "strip c = strip c' \<Longrightarrow> c \<sqsubseteq> c \<nabla>\<^sub>c c'"
   113 by(induct c c' rule: le_acom.induct)(simp_all add: widen1)
   114 
   115 lemma widen2_acom: "strip c = strip c' \<Longrightarrow> c' \<sqsubseteq> c \<nabla>\<^sub>c c'"
   116 by(induct c c' rule: le_acom.induct)(simp_all add: widen2)
   117 
   118 lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y"
   119 by(induct y x rule: le_acom.induct) (simp_all add: narrow1)
   120 
   121 lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
   122 by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
   123 
   124 
   125 subsubsection "Post-fixed point computation"
   126 
   127 definition
   128   prefp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
   129 "prefp f = while_option (\<lambda>x. \<not> x \<sqsubseteq> f x) f"
   130 
   131 definition
   132   pfp_WN :: "(('a::WN)up acom \<Rightarrow> 'a up acom) \<Rightarrow> com \<Rightarrow> 'a up acom option"
   133 where "pfp_WN f c = (case lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c of None \<Rightarrow> None
   134                      | Some c' \<Rightarrow> prefp (\<lambda>c. c \<triangle>\<^sub>c f c) c')"
   135 
   136 lemma strip_map2_acom:
   137  "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
   138 by(induct f c1 c2 rule: map2_acom.induct) simp_all
   139 
   140 lemma lpfp_step_up_pfp:
   141  "\<lbrakk> \<forall>c. strip(f c) = strip c;  lpfp\<^isub>c (\<lambda>c. c \<nabla>\<^sub>c f c) c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
   142 by (metis (no_types) assms lpfpc_pfp le_trans widen2_acom)
   143 
   144 lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0" 
   145 and "prefp (\<lambda>c. c \<triangle>\<^sub>c f c) x0 = Some x"
   146 shows "f x \<sqsubseteq> x \<and> x \<sqsubseteq> x0" (is "?P x")
   147 proof-
   148   { fix x assume "?P x"
   149     note 1 = conjunct1[OF this] and 2 = conjunct2[OF this]
   150     let ?x' = "x \<triangle>\<^sub>c f x"
   151     have "?P ?x'"
   152     proof
   153       have "f ?x' \<sqsubseteq> f x"  by(rule monoD[OF `mono f` narrow2_acom[OF 1]])
   154       also have "\<dots> \<sqsubseteq> ?x'" by(rule narrow1_acom[OF 1])
   155       finally show "f ?x' \<sqsubseteq> ?x'" .
   156       have "?x' \<sqsubseteq> x" by (rule narrow2_acom[OF 1])
   157       also have "x \<sqsubseteq> x0" by(rule 2)
   158       finally show "?x' \<sqsubseteq> x0" .
   159     qed
   160   }
   161   with while_option_rule[where P = ?P, OF _ assms(3)[simplified prefp_def]]
   162     assms(2) le_refl
   163   show ?thesis by blast
   164 qed
   165 
   166 
   167 lemma pfp_WN_pfp:
   168   "\<lbrakk> \<forall>c. strip (f c) = strip c;  mono f;  pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
   169 unfolding pfp_WN_def
   170 by (auto dest: iter_down_pfp lpfp_step_up_pfp split: option.splits)
   171 
   172 lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
   173 assumes "\<forall>c. strip (f c) = strip c" and "while_option P f c = Some c'"
   174 shows "strip c' = strip c"
   175 using while_option_rule[where P = "\<lambda>c'. strip c' = strip c", OF _ assms(2)]
   176 by (metis assms(1))
   177 
   178 lemma strip_pfp_WN:
   179   "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_WN f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
   180 apply(auto simp add: pfp_WN_def prefp_def split: option.splits)
   181 by (metis (no_types) strip_lpfpc strip_map2_acom strip_while)
   182 
   183 locale Abs_Int2 = Abs_Int1_mono rep for rep :: "'a::{WN,L_top_bot} \<Rightarrow> val set"
   184 begin
   185 
   186 definition AI_WN :: "com \<Rightarrow> 'a st up acom option" where
   187 "AI_WN = pfp_WN (step \<top>)"
   188 
   189 lemma AI_sound: "\<lbrakk> AI_WN c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
   190 unfolding AI_WN_def
   191 by(metis step_sound[of "\<top>" c' s t] strip_pfp_WN strip_step
   192   pfp_WN_pfp mono_def mono_step[OF le_refl] in_rep_Top_up)
   193 
   194 end
   195 
   196 interpretation
   197   Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl rep_ivl
   198 defines AI_ivl' is AI_WN
   199 proof qed
   200 
   201 value [code] "show_acom_opt (AI_ivl test3_ivl)"
   202 value [code] "show_acom_opt (AI_ivl' test3_ivl)"
   203 
   204 definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
   205 definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
   206 
   207 value [code] "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))"
   208 value [code] "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))"
   209 value [code] "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))"
   210 value [code] "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))"
   211 value [code] "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))"
   212 value [code] "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
   213 value [code] "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
   214 value [code] "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))"
   215 
   216 value [code] "show_acom_opt (AI_ivl' test4_ivl)"
   217 value [code] "show_acom_opt (AI_ivl' test5_ivl)"
   218 value [code] "show_acom_opt (AI_ivl' test6_ivl)"
   219 
   220 end