src/HOL/IMP/Abs_Int3.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61890 f6ded81f5690
child 63882 018998c00003
permissions -rw-r--r--
Lots of new material for multivariate analysis
nipkow@47613
     1
(* Author: Tobias Nipkow *)
nipkow@47613
     2
nipkow@47613
     3
theory Abs_Int3
nipkow@47613
     4
imports Abs_Int2_ivl
nipkow@47613
     5
begin
nipkow@47613
     6
nipkow@47613
     7
nipkow@47613
     8
subsection "Widening and Narrowing"
nipkow@47613
     9
nipkow@47613
    10
class widen =
nipkow@47613
    11
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
nipkow@47613
    12
nipkow@47613
    13
class narrow =
nipkow@47613
    14
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
nipkow@47613
    15
nipkow@52504
    16
class wn = widen + narrow + order +
nipkow@51359
    17
assumes widen1: "x \<le> x \<nabla> y"
nipkow@51359
    18
assumes widen2: "y \<le> x \<nabla> y"
nipkow@51359
    19
assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
nipkow@51359
    20
assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
nipkow@51711
    21
begin
nipkow@47613
    22
nipkow@51711
    23
lemma narrowid[simp]: "x \<triangle> x = x"
nipkow@51711
    24
by (metis eq_iff narrow1 narrow2)
nipkow@47613
    25
nipkow@51711
    26
end
nipkow@51711
    27
haftmann@52729
    28
lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,order_top})"
nipkow@51711
    29
by (metis eq_iff top_greatest widen2)
nipkow@47613
    30
nipkow@52504
    31
instantiation ivl :: wn
nipkow@47613
    32
begin
nipkow@47613
    33
nipkow@51359
    34
definition "widen_rep p1 p2 =
nipkow@51359
    35
  (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else
nipkow@51359
    36
   let (l1,h1) = p1; (l2,h2) = p2
nipkow@51359
    37
   in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))"
nipkow@51359
    38
nipkow@51359
    39
lift_definition widen_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is widen_rep
nipkow@51359
    40
by(auto simp: widen_rep_def eq_ivl_iff)
nipkow@47613
    41
nipkow@51359
    42
definition "narrow_rep p1 p2 =
nipkow@51359
    43
  (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
nipkow@51359
    44
   let (l1,h1) = p1; (l2,h2) = p2
nipkow@51359
    45
   in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))"
nipkow@51359
    46
nipkow@51359
    47
lift_definition narrow_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is narrow_rep
nipkow@51359
    48
by(auto simp: narrow_rep_def eq_ivl_iff)
nipkow@47613
    49
nipkow@47613
    50
instance
nipkow@51359
    51
proof
nipkow@51711
    52
qed (transfer, auto simp: widen_rep_def narrow_rep_def le_iff_subset \<gamma>_rep_def subset_eq is_empty_rep_def empty_rep_def eq_ivl_def split: if_splits extended.splits)+
nipkow@47613
    53
nipkow@47613
    54
end
nipkow@47613
    55
haftmann@52729
    56
instantiation st :: ("{order_top,wn}")wn
nipkow@47613
    57
begin
nipkow@47613
    58
nipkow@51711
    59
lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)"
nipkow@51711
    60
by(auto simp: eq_st_def)
nipkow@47613
    61
nipkow@51711
    62
lift_definition narrow_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<triangle>)"
nipkow@51711
    63
by(auto simp: eq_st_def)
nipkow@47613
    64
nipkow@47613
    65
instance
nipkow@61179
    66
proof (standard, goal_cases)
nipkow@61179
    67
  case 1 thus ?case by transfer (simp add: less_eq_st_rep_iff widen1)
nipkow@47613
    68
next
nipkow@61179
    69
  case 2 thus ?case by transfer (simp add: less_eq_st_rep_iff widen2)
nipkow@47613
    70
next
nipkow@61179
    71
  case 3 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow1)
nipkow@47613
    72
next
nipkow@61179
    73
  case 4 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow2)
nipkow@47613
    74
qed
nipkow@47613
    75
nipkow@47613
    76
end
nipkow@47613
    77
nipkow@47613
    78
nipkow@52504
    79
instantiation option :: (wn)wn
nipkow@47613
    80
begin
nipkow@47613
    81
nipkow@47613
    82
fun widen_option where
nipkow@47613
    83
"None \<nabla> x = x" |
nipkow@47613
    84
"x \<nabla> None = x" |
nipkow@47613
    85
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)"
nipkow@47613
    86
nipkow@47613
    87
fun narrow_option where
nipkow@47613
    88
"None \<triangle> x = None" |
nipkow@47613
    89
"x \<triangle> None = None" |
nipkow@47613
    90
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
nipkow@47613
    91
nipkow@47613
    92
instance
nipkow@61179
    93
proof (standard, goal_cases)
nipkow@61179
    94
  case (1 x y) thus ?case
nipkow@47613
    95
    by(induct x y rule: widen_option.induct)(simp_all add: widen1)
nipkow@47613
    96
next
nipkow@61179
    97
  case (2 x y) thus ?case
nipkow@47613
    98
    by(induct x y rule: widen_option.induct)(simp_all add: widen2)
nipkow@47613
    99
next
nipkow@61179
   100
  case (3 x y) thus ?case
nipkow@47613
   101
    by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
nipkow@47613
   102
next
nipkow@61179
   103
  case (4 y x) thus ?case
nipkow@47613
   104
    by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
nipkow@47613
   105
qed
nipkow@47613
   106
nipkow@47613
   107
end
nipkow@47613
   108
nipkow@52019
   109
definition map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom"
nipkow@52019
   110
where
nipkow@52019
   111
"map2_acom f C1 C2 = annotate (\<lambda>p. f (anno C1 p) (anno C2 p)) (strip C1)"
nipkow@52019
   112
nipkow@52504
   113
nipkow@49548
   114
instantiation acom :: (widen)widen
nipkow@49548
   115
begin
nipkow@49548
   116
definition "widen_acom = map2_acom (op \<nabla>)"
nipkow@49548
   117
instance ..
nipkow@49548
   118
end
nipkow@49548
   119
nipkow@49548
   120
instantiation acom :: (narrow)narrow
nipkow@49548
   121
begin
nipkow@49548
   122
definition "narrow_acom = map2_acom (op \<triangle>)"
nipkow@49548
   123
instance ..
nipkow@49548
   124
end
nipkow@49548
   125
nipkow@47613
   126
lemma strip_map2_acom[simp]:
nipkow@47613
   127
 "strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1"
nipkow@52019
   128
by(simp add: map2_acom_def)
nipkow@52019
   129
(*by(induct f C1 C2 rule: map2_acom.induct) simp_all*)
nipkow@47613
   130
nipkow@47613
   131
lemma strip_widen_acom[simp]:
nipkow@47613
   132
  "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1"
nipkow@49548
   133
by(simp add: widen_acom_def)
nipkow@47613
   134
nipkow@47613
   135
lemma strip_narrow_acom[simp]:
nipkow@47613
   136
  "strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1"
nipkow@49548
   137
by(simp add: narrow_acom_def)
nipkow@47613
   138
nipkow@52504
   139
lemma narrow1_acom: "C2 \<le> C1 \<Longrightarrow> C2 \<le> C1 \<triangle> (C2::'a::wn acom)"
nipkow@52019
   140
by(simp add: narrow_acom_def narrow1 map2_acom_def less_eq_acom_def size_annos)
nipkow@47613
   141
nipkow@52504
   142
lemma narrow2_acom: "C2 \<le> C1 \<Longrightarrow> C1 \<triangle> (C2::'a::wn acom) \<le> C1"
nipkow@52019
   143
by(simp add: narrow_acom_def narrow2 map2_acom_def less_eq_acom_def size_annos)
nipkow@47613
   144
nipkow@47613
   145
nipkow@52019
   146
subsubsection "Pre-fixpoint computation"
nipkow@47613
   147
nipkow@51359
   148
definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option"
nipkow@51359
   149
where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)"
nipkow@47613
   150
nipkow@51359
   151
definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option"
nipkow@51385
   152
where "iter_narrow f = while_option (\<lambda>x. x \<triangle> f x < x) (\<lambda>x. x \<triangle> f x)"
nipkow@47613
   153
nipkow@51359
   154
definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
nipkow@49548
   155
where "pfp_wn f x =
nipkow@49576
   156
  (case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)"
nipkow@47613
   157
nipkow@47613
   158
nipkow@51359
   159
lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p"
nipkow@47613
   160
by(auto simp add: iter_widen_def dest: while_option_stop)
nipkow@47613
   161
nipkow@47613
   162
lemma iter_widen_inv:
nipkow@47613
   163
assumes "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" and "P x"
nipkow@47613
   164
and "iter_widen f x = Some y" shows "P y"
nipkow@47613
   165
using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]]
nipkow@47613
   166
by (blast intro: assms(1-3))
nipkow@47613
   167
nipkow@47613
   168
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
nipkow@47613
   169
assumes "\<forall>C. strip (f C) = strip C" and "while_option P f C = Some C'"
nipkow@47613
   170
shows "strip C' = strip C"
nipkow@47613
   171
using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
nipkow@47613
   172
by (metis assms(1))
nipkow@47613
   173
nipkow@51359
   174
lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom"
nipkow@47613
   175
assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
nipkow@47613
   176
shows "strip C' = strip C"
nipkow@47613
   177
proof-
nipkow@47613
   178
  have "\<forall>C. strip(C \<nabla> f C) = strip C"
nipkow@47613
   179
    by (metis assms(1) strip_map2_acom widen_acom_def)
nipkow@47613
   180
  from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def)
nipkow@47613
   181
qed
nipkow@47613
   182
nipkow@47613
   183
lemma iter_narrow_pfp:
nipkow@52504
   184
assumes mono: "!!x1 x2::_::wn acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
nipkow@49576
   185
and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
nipkow@51359
   186
and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p"
nipkow@51359
   187
shows "P p \<and> f p \<le> p"
nipkow@47613
   188
proof-
nipkow@51359
   189
  let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0"
nipkow@49576
   190
  { fix p assume "?Q p"
nipkow@47613
   191
    note P = conjunct1[OF this] and 12 = conjunct2[OF this]
nipkow@47613
   192
    note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
nipkow@49576
   193
    let ?p' = "p \<triangle> f p"
nipkow@49576
   194
    have "?Q ?p'"
nipkow@47613
   195
    proof auto
nipkow@49576
   196
      show "P ?p'" by (blast intro: P Pinv)
nipkow@51711
   197
      have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2_acom[OF 1]])
nipkow@51711
   198
      also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1])
nipkow@51359
   199
      finally show "f ?p' \<le> ?p'" .
nipkow@51711
   200
      have "?p' \<le> p" by (rule narrow2_acom[OF 1])
nipkow@51359
   201
      also have "p \<le> p0" by(rule 2)
nipkow@51359
   202
      finally show "?p' \<le> p0" .
nipkow@47613
   203
    qed
nipkow@47613
   204
  }
nipkow@47613
   205
  thus ?thesis
nipkow@47613
   206
    using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]]
nipkow@47613
   207
    by (blast intro: assms(4,5) le_refl)
nipkow@47613
   208
qed
nipkow@47613
   209
nipkow@47613
   210
lemma pfp_wn_pfp:
nipkow@52504
   211
assumes mono: "!!x1 x2::_::wn acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
nipkow@49548
   212
and Pinv: "P x"  "!!x. P x \<Longrightarrow> P(f x)"
nipkow@49548
   213
  "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)"
nipkow@49548
   214
  "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
nipkow@51359
   215
and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p"
nipkow@47613
   216
proof-
nipkow@49576
   217
  from pfp_wn obtain p0
nipkow@49576
   218
    where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
nipkow@47613
   219
    by(auto simp: pfp_wn_def split: option.splits)
nipkow@49576
   220
  have "P p0" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(1-3))
nipkow@47613
   221
  thus ?thesis
nipkow@47613
   222
    by - (assumption |
nipkow@47613
   223
          rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+
nipkow@47613
   224
qed
nipkow@47613
   225
nipkow@47613
   226
lemma strip_pfp_wn:
nipkow@49548
   227
  "\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C"
nipkow@47613
   228
by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
nipkow@51390
   229
  (metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while)
nipkow@47613
   230
nipkow@47613
   231
nipkow@52504
   232
locale Abs_Int_wn = Abs_Int_inv_mono where \<gamma>=\<gamma>
nipkow@52504
   233
  for \<gamma> :: "'av::{wn,bounded_lattice} \<Rightarrow> val set"
nipkow@47613
   234
begin
nipkow@47613
   235
nipkow@47613
   236
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
nipkow@51711
   237
"AI_wn c = pfp_wn (step' \<top>) (bot c)"
nipkow@47613
   238
wenzelm@53015
   239
lemma AI_wn_correct: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c C"
nipkow@47613
   240
proof(simp add: CS_def AI_wn_def)
nipkow@51711
   241
  assume 1: "pfp_wn (step' \<top>) (bot c) = Some C"
nipkow@51711
   242
  have 2: "strip C = c \<and> step' \<top> C \<le> C"
nipkow@51711
   243
    by(rule pfp_wn_pfp[where x="bot c"]) (simp_all add: 1 mono_step'_top)
wenzelm@53015
   244
  have pfp: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C"
nipkow@50986
   245
  proof(rule order_trans)
wenzelm@53015
   246
    show "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le>  \<gamma>\<^sub>c (step' \<top> C)"
nipkow@51711
   247
      by(rule step_step')
wenzelm@53015
   248
    show "... \<le> \<gamma>\<^sub>c C"
nipkow@50986
   249
      by(rule mono_gamma_c[OF conjunct2[OF 2]])
nipkow@47613
   250
  qed
wenzelm@53015
   251
  have 3: "strip (\<gamma>\<^sub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
wenzelm@53015
   252
  have "lfp c (step (\<gamma>\<^sub>o \<top>)) \<le> \<gamma>\<^sub>c C"
wenzelm@53015
   253
    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^sub>o \<top>)", OF 3 pfp])
wenzelm@53015
   254
  thus "lfp c (step UNIV) \<le> \<gamma>\<^sub>c C" by simp
nipkow@47613
   255
qed
nipkow@47613
   256
nipkow@47613
   257
end
nipkow@47613
   258
haftmann@61890
   259
global_interpretation Abs_Int_wn
nipkow@51245
   260
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
nipkow@47613
   261
and test_num' = in_ivl
nipkow@51974
   262
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
haftmann@61671
   263
defines AI_wn_ivl = AI_wn
nipkow@47613
   264
..
nipkow@47613
   265
nipkow@47613
   266
nipkow@47613
   267
subsubsection "Tests"
nipkow@47613
   268
nipkow@51791
   269
definition "step_up_ivl n = ((\<lambda>C. C \<nabla> step_ivl \<top> C)^^n)"
nipkow@51791
   270
definition "step_down_ivl n = ((\<lambda>C. C \<triangle> step_ivl \<top> C)^^n)"
nipkow@47613
   271
nipkow@47613
   272
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
nipkow@51953
   273
the loop took to execute. In contrast, @{const AI_wn_ivl} converges in a
nipkow@47613
   274
constant number of steps: *}
nipkow@47613
   275
nipkow@47613
   276
value "show_acom (step_up_ivl 1 (bot test3_ivl))"
nipkow@47613
   277
value "show_acom (step_up_ivl 2 (bot test3_ivl))"
nipkow@47613
   278
value "show_acom (step_up_ivl 3 (bot test3_ivl))"
nipkow@47613
   279
value "show_acom (step_up_ivl 4 (bot test3_ivl))"
nipkow@47613
   280
value "show_acom (step_up_ivl 5 (bot test3_ivl))"
nipkow@49188
   281
value "show_acom (step_up_ivl 6 (bot test3_ivl))"
nipkow@49188
   282
value "show_acom (step_up_ivl 7 (bot test3_ivl))"
nipkow@49188
   283
value "show_acom (step_up_ivl 8 (bot test3_ivl))"
nipkow@49188
   284
value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))"
nipkow@49188
   285
value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))"
nipkow@49188
   286
value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))"
nipkow@49188
   287
value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))"
nipkow@51953
   288
value "show_acom_opt (AI_wn_ivl test3_ivl)"
nipkow@47613
   289
nipkow@47613
   290
nipkow@47613
   291
text{* Now all the analyses terminate: *}
nipkow@47613
   292
nipkow@51953
   293
value "show_acom_opt (AI_wn_ivl test4_ivl)"
nipkow@51953
   294
value "show_acom_opt (AI_wn_ivl test5_ivl)"
nipkow@51953
   295
value "show_acom_opt (AI_wn_ivl test6_ivl)"
nipkow@47613
   296
nipkow@47613
   297
nipkow@47613
   298
subsubsection "Generic Termination Proof"
nipkow@47613
   299
nipkow@51722
   300
lemma top_on_opt_widen:
nipkow@51785
   301
  "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<nabla> o2 :: _ st option) X"
nipkow@51711
   302
apply(induct o1 o2 rule: widen_option.induct)
nipkow@51711
   303
apply (auto)
nipkow@51711
   304
by transfer simp
nipkow@51711
   305
nipkow@51722
   306
lemma top_on_opt_narrow:
nipkow@51785
   307
  "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<triangle> o2 :: _ st option) X"
nipkow@51711
   308
apply(induct o1 o2 rule: narrow_option.induct)
nipkow@51711
   309
apply (auto)
nipkow@51711
   310
by transfer simp
nipkow@51711
   311
nipkow@52019
   312
(* FIXME mk anno abbrv *)
nipkow@52019
   313
lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow>
nipkow@52019
   314
  annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))"
nipkow@52019
   315
by(simp add: map2_acom_def list_eq_iff_nth_eq size_annos anno_def[symmetric] size_annos_same[of C1 C2])
nipkow@52019
   316
nipkow@51711
   317
lemma top_on_acom_widen:
nipkow@51785
   318
  "\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk>
nipkow@51785
   319
  \<Longrightarrow> top_on_acom (C1 \<nabla> C2 :: _ st option acom) X"
nipkow@51711
   320
by(auto simp add: widen_acom_def top_on_acom_def)(metis top_on_opt_widen in_set_zipE)
nipkow@51711
   321
nipkow@51711
   322
lemma top_on_acom_narrow:
nipkow@51785
   323
  "\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk>
nipkow@51785
   324
  \<Longrightarrow> top_on_acom (C1 \<triangle> C2 :: _ st option acom) X"
nipkow@51711
   325
by(auto simp add: narrow_acom_def top_on_acom_def)(metis top_on_opt_narrow in_set_zipE)
nipkow@51711
   326
nipkow@51385
   327
text{* The assumptions for widening and narrowing differ because during
nipkow@51385
   328
narrowing we have the invariant @{prop"y \<le> x"} (where @{text y} is the next
nipkow@51385
   329
iterate), but during widening there is no such invariant, there we only have
nipkow@51385
   330
that not yet @{prop"y \<le> x"}. This complicates the termination proof for
nipkow@51385
   331
widening. *}
nipkow@51385
   332
nipkow@52504
   333
locale Measure_wn = Measure1 where m=m
haftmann@52729
   334
  for m :: "'av::{order_top,wn} \<Rightarrow> nat" +
nipkow@47613
   335
fixes n :: "'av \<Rightarrow> nat"
nipkow@51372
   336
assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
nipkow@51359
   337
assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
nipkow@51385
   338
assumes n_narrow: "y \<le> x \<Longrightarrow> x \<triangle> y < x \<Longrightarrow> n(x \<triangle> y) < n x"
nipkow@47613
   339
nipkow@47613
   340
begin
nipkow@47613
   341
nipkow@51711
   342
lemma m_s_anti_mono_rep: assumes "\<forall>x. S1 x \<le> S2 x"
nipkow@51711
   343
shows "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))"
nipkow@51711
   344
proof-
nipkow@51711
   345
  from assms have "\<forall>x. m(S1 x) \<ge> m(S2 x)" by (metis m_anti_mono)
nipkow@51711
   346
  thus "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))" by (metis setsum_mono)
nipkow@51372
   347
qed
nipkow@51372
   348
nipkow@51791
   349
lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s S1 X \<ge> m_s S2 X"
nipkow@51711
   350
unfolding m_s_def
nipkow@51711
   351
apply (transfer fixing: m)
nipkow@51711
   352
apply(simp add: less_eq_st_rep_iff eq_st_def m_s_anti_mono_rep)
nipkow@51711
   353
done
nipkow@51711
   354
nipkow@51711
   355
lemma m_s_widen_rep: assumes "finite X" "S1 = S2 on -X" "\<not> S2 x \<le> S1 x"
nipkow@51711
   356
  shows "(\<Sum>x\<in>X. m (S1 x \<nabla> S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
nipkow@51711
   357
proof-
nipkow@51711
   358
  have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S1 x \<nabla> S2 x)"
nipkow@52504
   359
    by (metis m_anti_mono wn_class.widen1)
nipkow@51711
   360
  have "x \<in> X" using assms(2,3)
nipkow@51711
   361
    by(auto simp add: Ball_def)
nipkow@51711
   362
  hence 2: "\<exists>x\<in>X. m(S1 x) > m(S1 x \<nabla> S2 x)"
nipkow@51711
   363
    using assms(3) m_widen by blast
nipkow@51711
   364
  from setsum_strict_mono_ex1[OF `finite X` 1 2]
nipkow@51711
   365
  show ?thesis .
nipkow@47613
   366
qed
nipkow@47613
   367
nipkow@51711
   368
lemma m_s_widen: "finite X \<Longrightarrow> fun S1 = fun S2 on -X ==>
nipkow@51791
   369
  ~ S2 \<le> S1 \<Longrightarrow> m_s (S1 \<nabla> S2) X < m_s S1 X"
nipkow@51711
   370
apply(auto simp add: less_st_def m_s_def)
nipkow@51711
   371
apply (transfer fixing: m)
nipkow@51711
   372
apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep)
nipkow@51711
   373
done
nipkow@51711
   374
nipkow@51785
   375
lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
nipkow@51791
   376
  o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X"
nipkow@51372
   377
proof(induction o1 o2 rule: less_eq_option.induct)
nipkow@51372
   378
  case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono)
nipkow@51372
   379
next
nipkow@51372
   380
  case 2 thus ?case
nipkow@51711
   381
    by(simp add: m_o_def le_SucI m_s_h split: option.splits)
nipkow@51372
   382
next
nipkow@51372
   383
  case 3 thus ?case by simp
nipkow@51372
   384
qed
nipkow@51372
   385
nipkow@51785
   386
lemma m_o_widen: "\<lbrakk> finite X; top_on_opt S1 (-X); top_on_opt S2 (-X); \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
nipkow@51791
   387
  m_o (S1 \<nabla> S2) X < m_o S1 X"
nipkow@51711
   388
by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
nipkow@47613
   389
nipkow@49547
   390
lemma m_c_widen:
nipkow@51785
   391
  "strip C1 = strip C2  \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2)
nipkow@51711
   392
   \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
nipkow@52019
   393
apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]listsum_setsum_nth)
nipkow@49547
   394
apply(subgoal_tac "length(annos C2) = length(annos C1)")
nipkow@51390
   395
 prefer 2 apply (simp add: size_annos_same2)
nipkow@49547
   396
apply (auto)
nipkow@49547
   397
apply(rule setsum_strict_mono_ex1)
nipkow@52019
   398
 apply(auto simp add: m_o_anti_mono vars_acom_def anno_def top_on_acom_def top_on_opt_widen widen1 less_eq_acom_def listrel_iff_nth)
nipkow@52019
   399
apply(rule_tac x=p in bexI)
nipkow@51711
   400
 apply (auto simp: vars_acom_def m_o_widen top_on_acom_def)
nipkow@49547
   401
done
nipkow@49547
   402
nipkow@49547
   403
wenzelm@53015
   404
definition n_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^sub>s") where
wenzelm@53015
   405
"n\<^sub>s S X = (\<Sum>x\<in>X. n(fun S x))"
nipkow@49547
   406
nipkow@51711
   407
lemma n_s_narrow_rep:
nipkow@51711
   408
assumes "finite X"  "S1 = S2 on -X"  "\<forall>x. S2 x \<le> S1 x"  "\<forall>x. S1 x \<triangle> S2 x \<le> S1 x"
nipkow@51711
   409
  "S1 x \<noteq> S1 x \<triangle> S2 x"
nipkow@51711
   410
shows "(\<Sum>x\<in>X. n (S1 x \<triangle> S2 x)) < (\<Sum>x\<in>X. n (S1 x))"
nipkow@47613
   411
proof-
nipkow@51711
   412
  have 1: "\<forall>x. n(S1 x \<triangle> S2 x) \<le> n(S1 x)"
nipkow@51711
   413
      by (metis assms(3) assms(4) eq_iff less_le_not_le n_narrow)
nipkow@51711
   414
  have "x \<in> X" by (metis Compl_iff assms(2) assms(5) narrowid)
nipkow@51711
   415
  hence 2: "\<exists>x\<in>X. n(S1 x \<triangle> S2 x) < n(S1 x)"
nipkow@51711
   416
    by (metis assms(3-5) eq_iff less_le_not_le n_narrow)
nipkow@51711
   417
  show ?thesis
nipkow@51711
   418
    apply(rule setsum_strict_mono_ex1[OF `finite X`]) using 1 2 by blast+
nipkow@47613
   419
qed
nipkow@47613
   420
nipkow@51711
   421
lemma n_s_narrow: "finite X \<Longrightarrow> fun S1 = fun S2 on -X \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1
wenzelm@53015
   422
  \<Longrightarrow> n\<^sub>s (S1 \<triangle> S2) X < n\<^sub>s S1 X"
nipkow@51711
   423
apply(auto simp add: less_st_def n_s_def)
nipkow@51711
   424
apply (transfer fixing: n)
nipkow@51711
   425
apply(auto simp add: less_eq_st_rep_iff eq_st_def fun_eq_iff n_s_narrow_rep)
nipkow@51711
   426
done
nipkow@47613
   427
wenzelm@53015
   428
definition n_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^sub>o") where
wenzelm@53015
   429
"n\<^sub>o opt X = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^sub>s S X + 1)"
nipkow@47613
   430
nipkow@47613
   431
lemma n_o_narrow:
nipkow@51785
   432
  "top_on_opt S1 (-X) \<Longrightarrow> top_on_opt S2 (-X) \<Longrightarrow> finite X
wenzelm@53015
   433
  \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^sub>o (S1 \<triangle> S2) X < n\<^sub>o S1 X"
nipkow@47613
   434
apply(induction S1 S2 rule: narrow_option.induct)
nipkow@51711
   435
apply(auto simp: n_o_def n_s_narrow)
nipkow@47613
   436
done
nipkow@47613
   437
nipkow@49576
   438
wenzelm@53015
   439
definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^sub>c") where
wenzelm@53015
   440
"n\<^sub>c C = listsum (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"
nipkow@47613
   441
nipkow@51385
   442
lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
nipkow@51385
   443
  (\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"
nipkow@51385
   444
by(metis (hide_lams, no_types) less_le_not_le le_iff_le_annos size_annos_same2)
nipkow@51385
   445
nipkow@51711
   446
lemma n_c_narrow: "strip C1 = strip C2
nipkow@51785
   447
  \<Longrightarrow> top_on_acom C1 (- vars C1) \<Longrightarrow> top_on_acom C2 (- vars C2)
wenzelm@53015
   448
  \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^sub>c (C1 \<triangle> C2) < n\<^sub>c C1"
nipkow@51792
   449
apply(auto simp: n_c_def narrow_acom_def listsum_setsum_nth)
nipkow@47613
   450
apply(subgoal_tac "length(annos C2) = length(annos C1)")
nipkow@47613
   451
prefer 2 apply (simp add: size_annos_same2)
nipkow@47613
   452
apply (auto)
nipkow@51385
   453
apply(simp add: less_annos_iff le_iff_le_annos)
nipkow@47613
   454
apply(rule setsum_strict_mono_ex1)
nipkow@51711
   455
apply (auto simp: vars_acom_def top_on_acom_def)
nipkow@51385
   456
apply (metis n_o_narrow nth_mem finite_cvars less_imp_le le_less order_refl)
nipkow@47613
   457
apply(rule_tac x=i in bexI)
nipkow@47613
   458
prefer 2 apply simp
nipkow@51711
   459
apply(rule n_o_narrow[where X = "vars(strip C2)"])
nipkow@51711
   460
apply (simp_all)
nipkow@47613
   461
done
nipkow@47613
   462
nipkow@47613
   463
end
nipkow@47613
   464
nipkow@47613
   465
nipkow@47613
   466
lemma iter_widen_termination:
nipkow@52504
   467
fixes m :: "'a::wn acom \<Rightarrow> nat"
nipkow@47613
   468
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
nipkow@47613
   469
and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
nipkow@51359
   470
and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
nipkow@47613
   471
and "P C" shows "EX C'. iter_widen f C = Some C'"
nipkow@49547
   472
proof(simp add: iter_widen_def,
nipkow@49547
   473
      rule measure_while_option_Some[where P = P and f=m])
nipkow@47613
   474
  show "P C" by(rule `P C`)
nipkow@47613
   475
next
nipkow@51359
   476
  fix C assume "P C" "\<not> f C \<le> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
nipkow@49547
   477
    by(simp add: P_f P_widen m_widen)
nipkow@47613
   478
qed
nipkow@49496
   479
nipkow@47613
   480
lemma iter_narrow_termination:
nipkow@52504
   481
fixes n :: "'a::wn acom \<Rightarrow> nat"
nipkow@47613
   482
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
nipkow@47613
   483
and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
nipkow@51359
   484
and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2"
nipkow@51385
   485
and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
nipkow@51359
   486
and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'"
nipkow@49547
   487
proof(simp add: iter_narrow_def,
nipkow@51359
   488
      rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<le> C"])
nipkow@51359
   489
  show "P C \<and> f C \<le> C" using init by blast
nipkow@47613
   490
next
nipkow@51385
   491
  fix C assume 1: "P C \<and> f C \<le> C" and 2: "C \<triangle> f C < C"
nipkow@47613
   492
  hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
nipkow@51359
   493
  moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C"
nipkow@51711
   494
    by (metis narrow1_acom narrow2_acom 1 mono order_trans)
nipkow@49547
   495
  moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f)
nipkow@51359
   496
  ultimately show "(P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<le> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C"
nipkow@49547
   497
    by blast
nipkow@47613
   498
qed
nipkow@47613
   499
nipkow@52504
   500
locale Abs_Int_wn_measure = Abs_Int_wn where \<gamma>=\<gamma> + Measure_wn where m=m
nipkow@52504
   501
  for \<gamma> :: "'av::{wn,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
nipkow@49547
   502
nipkow@47613
   503
nipkow@47613
   504
subsubsection "Termination: Intervals"
nipkow@47613
   505
nipkow@51359
   506
definition m_rep :: "eint2 \<Rightarrow> nat" where
nipkow@51359
   507
"m_rep p = (if is_empty_rep p then 3 else
nipkow@51359
   508
  let (l,h) = p in (case l of Minf \<Rightarrow> 0 | _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | _ \<Rightarrow> 1))"
nipkow@51359
   509
nipkow@51359
   510
lift_definition m_ivl :: "ivl \<Rightarrow> nat" is m_rep
nipkow@51359
   511
by(auto simp: m_rep_def eq_ivl_iff)
nipkow@47613
   512
nipkow@51924
   513
lemma m_ivl_nice: "m_ivl[l,h] = (if [l,h] = \<bottom> then 3 else
nipkow@51359
   514
   (if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))"
nipkow@51359
   515
unfolding bot_ivl_def
nipkow@51359
   516
by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split)
nipkow@47613
   517
nipkow@51359
   518
lemma m_ivl_height: "m_ivl iv \<le> 3"
nipkow@51359
   519
by transfer (simp add: m_rep_def split: prod.split extended.split)
nipkow@51359
   520
nipkow@51359
   521
lemma m_ivl_anti_mono: "y \<le> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
nipkow@51359
   522
by transfer
nipkow@51359
   523
   (auto simp: m_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
nipkow@51359
   524
         split: prod.split extended.splits if_splits)
nipkow@47613
   525
nipkow@47613
   526
lemma m_ivl_widen:
nipkow@51359
   527
  "~ y \<le> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
nipkow@51359
   528
by transfer
nipkow@51359
   529
   (auto simp: m_rep_def widen_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
nipkow@51359
   530
         split: prod.split extended.splits if_splits)
nipkow@47613
   531
nipkow@47613
   532
definition n_ivl :: "ivl \<Rightarrow> nat" where
nipkow@51953
   533
"n_ivl iv = 3 - m_ivl iv"
nipkow@47613
   534
nipkow@47613
   535
lemma n_ivl_narrow:
nipkow@51385
   536
  "x \<triangle> y < x \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
nipkow@51359
   537
unfolding n_ivl_def
nipkow@51385
   538
apply(subst (asm) less_le_not_le)
nipkow@51385
   539
apply transfer
nipkow@51385
   540
by(auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset
nipkow@51385
   541
         split: prod.splits if_splits extended.split)
nipkow@47613
   542
nipkow@47613
   543
haftmann@61890
   544
global_interpretation Abs_Int_wn_measure
nipkow@51245
   545
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
nipkow@47613
   546
and test_num' = in_ivl
nipkow@51974
   547
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
nipkow@51359
   548
and m = m_ivl and n = n_ivl and h = 3
nipkow@61179
   549
proof (standard, goal_cases)
nipkow@61179
   550
  case 2 thus ?case by(rule m_ivl_anti_mono)
nipkow@47613
   551
next
nipkow@61179
   552
  case 1 thus ?case by(rule m_ivl_height)
nipkow@47613
   553
next
nipkow@61179
   554
  case 3 thus ?case by(rule m_ivl_widen)
nipkow@47613
   555
next
nipkow@61179
   556
  case 4 from 4(2) show ?case by(rule n_ivl_narrow)
nipkow@49576
   557
  -- "note that the first assms is unnecessary for intervals"
nipkow@47613
   558
qed
nipkow@47613
   559
nipkow@47613
   560
lemma iter_winden_step_ivl_termination:
nipkow@51711
   561
  "\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C"
nipkow@51785
   562
apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on_acom C (- vars C)"])
nipkow@51711
   563
apply (auto simp add: m_c_widen top_on_bot top_on_step'[simplified comp_def vars_acom_def]
nipkow@51711
   564
  vars_acom_def top_on_acom_widen)
nipkow@47613
   565
done
nipkow@47613
   566
nipkow@47613
   567
lemma iter_narrow_step_ivl_termination:
nipkow@51953
   568
  "top_on_acom C (- vars C) \<Longrightarrow> step_ivl \<top> C \<le> C \<Longrightarrow>
nipkow@51953
   569
  \<exists>C'. iter_narrow (step_ivl \<top>) C = Some C'"
nipkow@51953
   570
apply(rule iter_narrow_termination[where n = "n_c" and P = "%C'. strip C = strip C' \<and> top_on_acom C' (-vars C')"])
nipkow@51711
   571
apply(auto simp: top_on_step'[simplified comp_def vars_acom_def]
nipkow@51711
   572
        mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow)
nipkow@47613
   573
done
nipkow@47613
   574
nipkow@51953
   575
theorem AI_wn_ivl_termination:
nipkow@51953
   576
  "\<exists>C. AI_wn_ivl c = Some C"
nipkow@47613
   577
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination
nipkow@47613
   578
           split: option.split)
nipkow@47613
   579
apply(rule iter_narrow_step_ivl_termination)
nipkow@51711
   580
apply(rule conjunct2)
nipkow@51785
   581
apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on_acom C (- vars C)"])
nipkow@51711
   582
apply(auto simp: top_on_acom_widen top_on_step'[simplified comp_def vars_acom_def]
nipkow@51711
   583
  iter_widen_pfp top_on_bot vars_acom_def)
nipkow@47613
   584
done
nipkow@47613
   585
nipkow@51390
   586
(*unused_thms Abs_Int_init - *)
nipkow@47613
   587
nipkow@49578
   588
subsubsection "Counterexamples"
nipkow@49578
   589
nipkow@51359
   590
text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening.
nipkow@51359
   591
It can already be lost after the first step: *}
nipkow@49578
   592
nipkow@52504
   593
lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"
nipkow@51359
   594
and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"
nipkow@55357
   595
nitpick[card = 3, expect = genuine, show_consts, timeout = 120]
nipkow@49578
   596
(*
nipkow@49578
   597
1 < 2 < 3,
nipkow@49578
   598
f x = 2,
nipkow@49578
   599
x widen y = 3 -- guarantees termination with top=3
nipkow@49578
   600
x = 1
nipkow@49578
   601
Now f is mono, x <= f x, not f x <= x
nipkow@49578
   602
but x widen f x = 3, f 3 = 2, but not 3 <= 2
nipkow@49578
   603
*)
nipkow@49578
   604
oops
nipkow@49578
   605
nipkow@49578
   606
text{* Widening terminates but may converge more slowly than Kleene iteration.
nipkow@49578
   607
In the following model, Kleene iteration goes from 0 to the least pfp
nipkow@49578
   608
in one step but widening takes 2 steps to reach a strictly larger pfp: *}
nipkow@52504
   609
lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y"
nipkow@51359
   610
and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"
nipkow@51359
   611
shows "f(x \<nabla> f x) \<le> x \<nabla> f x"
nipkow@55357
   612
nitpick[card = 4, expect = genuine, show_consts, timeout = 120]
nipkow@49578
   613
(*
nipkow@49578
   614
nipkow@49578
   615
   0 < 1 < 2 < 3
nipkow@49578
   616
f: 1   1   3   3
nipkow@49578
   617
nipkow@49578
   618
0 widen 1 = 2
nipkow@49578
   619
2 widen 3 = 3
nipkow@49578
   620
and x widen y arbitrary, eg 3, which guarantees termination
nipkow@49578
   621
nipkow@49578
   622
Kleene: f(f 0) = f 1 = 1 <= 1 = f 1
nipkow@49578
   623
nipkow@49578
   624
but
nipkow@49578
   625
nipkow@49578
   626
because not f 0 <= 0, we obtain 0 widen f 0 = 0 wide 1 = 2,
nipkow@49578
   627
which is again not a pfp: not f 2 = 3 <= 2
nipkow@49578
   628
Another widening step yields 2 widen f 2 = 2 widen 3 = 3
nipkow@49578
   629
*)
wenzelm@49892
   630
oops
nipkow@49578
   631
nipkow@47613
   632
end