src/HOL/MicroJava/BV/Kildall.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23467 d1b97708d5eb
child 27611 2c01c0bdb385
permissions -rw-r--r--
Name.uu, Name.aT;
kleing@12516
     1
(*  Title:      HOL/MicroJava/BV/Kildall.thy
kleing@10496
     2
    ID:         $Id$
kleing@12516
     3
    Author:     Tobias Nipkow, Gerwin Klein
kleing@10496
     4
    Copyright   2000 TUM
kleing@10496
     5
kleing@10496
     6
Kildall's algorithm
kleing@10496
     7
*)
kleing@10496
     8
kleing@12911
     9
header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
kleing@10496
    10
haftmann@16417
    11
theory Kildall imports SemilatAlg While_Combinator begin
kleing@12516
    12
kleing@10496
    13
kleing@10496
    14
consts
kleing@12516
    15
 iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
nipkow@11298
    16
          's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"
kleing@13006
    17
 propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set"
kleing@10496
    18
kleing@10496
    19
primrec
kleing@12516
    20
"propa f []      ss w = (ss,w)"
kleing@12516
    21
"propa f (q'#qs) ss w = (let (q,t) = q';
kleing@12516
    22
                             u = t +_f ss!q;
kleing@12516
    23
                             w' = (if u = ss!q then w else insert q w)
kleing@12516
    24
                         in propa f qs (ss[q := u]) w')"
kleing@10496
    25
nipkow@11175
    26
defs iter_def:
kleing@12516
    27
"iter f step ss w ==
nipkow@11298
    28
 while (%(ss,w). w \<noteq> {})
kleing@12516
    29
       (%(ss,w). let p = SOME p. p \<in> w
kleing@12516
    30
                 in propa f (step p (ss!p)) ss (w-{p}))
nipkow@11298
    31
       (ss,w)"
kleing@10496
    32
kleing@10496
    33
constdefs
kleing@13006
    34
 unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set"
kleing@12516
    35
"unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}"
kleing@10496
    36
kleing@13006
    37
 kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list"
kleing@12516
    38
"kildall r f step ss == fst(iter f step ss (unstables r step ss))"
kleing@10496
    39
kleing@13006
    40
consts merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"
kleing@10496
    41
primrec
kleing@12516
    42
"merges f []      ss = ss"
kleing@12516
    43
"merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
kleing@10496
    44
kleing@10496
    45
nipkow@13074
    46
lemmas [simp] = Let_def semilat.le_iff_plus_unchanged [symmetric]
kleing@10496
    47
kleing@10496
    48
nipkow@13074
    49
lemma (in semilat) nth_merges:
nipkow@13074
    50
 "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
nipkow@23281
    51
  (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
nipkow@13074
    52
  (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
kleing@12516
    53
proof (induct ps)
kleing@12516
    54
  show "\<And>ss. ?P ss []" by simp
kleing@12516
    55
kleing@12516
    56
  fix ss p' ps'
kleing@12516
    57
  assume ss: "ss \<in> list n A"
kleing@12516
    58
  assume l:  "p < length ss"
kleing@12516
    59
  assume "?steptype (p'#ps')"
kleing@12516
    60
  then obtain a b where
wenzelm@23467
    61
    p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and ps': "?steptype ps'"
wenzelm@23467
    62
    by (cases p') auto
nipkow@13074
    63
  assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"
wenzelm@23467
    64
  from this [OF _ _ ps'] have IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .
kleing@12516
    65
nipkow@13074
    66
  from ss ab
kleing@12516
    67
  have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD)
kleing@12516
    68
  moreover
wenzelm@23467
    69
  from calculation l
kleing@12516
    70
  have "p < length (ss[a := b +_f ss!a])" by simp
kleing@12516
    71
  ultimately
kleing@12516
    72
  have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)
nipkow@13074
    73
  with p' l
kleing@12516
    74
  show "?P ss (p'#ps')" by simp
kleing@12516
    75
qed
kleing@12516
    76
kleing@12516
    77
kleing@10496
    78
(** merges **)
kleing@10496
    79
kleing@10496
    80
lemma length_merges [rule_format, simp]:
kleing@12516
    81
  "\<forall>ss. size(merges f ps ss) = size ss"
kleing@10496
    82
  by (induct_tac ps, auto)
kleing@10496
    83
kleing@12516
    84
nipkow@13074
    85
lemma (in semilat) merges_preserves_type_lemma:
nipkow@13074
    86
shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
nipkow@13074
    87
          \<longrightarrow> merges f ps xs \<in> list n A"
nipkow@13074
    88
apply (insert closedI)
nipkow@13074
    89
apply (unfold closed_def)
nipkow@13074
    90
apply (induct_tac ps)
nipkow@13074
    91
 apply simp
nipkow@13074
    92
apply clarsimp
nipkow@13074
    93
done
kleing@10496
    94
nipkow@13074
    95
lemma (in semilat) merges_preserves_type [simp]:
nipkow@13074
    96
 "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
kleing@13006
    97
  \<Longrightarrow> merges f ps xs \<in> list n A"
nipkow@13074
    98
by (simp add: merges_preserves_type_lemma)
nipkow@13074
    99
nipkow@13074
   100
lemma (in semilat) merges_incr_lemma:
nipkow@13074
   101
 "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
nipkow@13074
   102
apply (induct_tac ps)
nipkow@13074
   103
 apply simp
nipkow@13074
   104
apply simp
nipkow@13074
   105
apply clarify
nipkow@13074
   106
apply (rule order_trans)
kleing@10496
   107
  apply simp
nipkow@13074
   108
 apply (erule list_update_incr)
nipkow@13074
   109
  apply simp
nipkow@13074
   110
 apply simp
nipkow@13074
   111
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
nipkow@13074
   112
done
kleing@10496
   113
nipkow@13074
   114
lemma (in semilat) merges_incr:
nipkow@13074
   115
 "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
kleing@13006
   116
  \<Longrightarrow> xs <=[r] merges f ps xs"
kleing@12516
   117
  by (simp add: merges_incr_lemma)
kleing@12516
   118
kleing@12516
   119
nipkow@13074
   120
lemma (in semilat) merges_same_conv [rule_format]:
nipkow@13074
   121
 "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
kleing@12516
   122
     (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
kleing@10496
   123
  apply (induct_tac ps)
kleing@10496
   124
   apply simp
kleing@10496
   125
  apply clarsimp
kleing@12516
   126
  apply (rename_tac p x ps xs)
kleing@10496
   127
  apply (rule iffI)
kleing@10496
   128
   apply (rule context_conjI)
kleing@10496
   129
    apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
wenzelm@17537
   130
     apply (drule_tac p = p in le_listD)
wenzelm@17537
   131
      apply simp
wenzelm@17537
   132
     apply simp
kleing@10496
   133
    apply (erule subst, rule merges_incr)
kleing@10496
   134
       apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
kleing@12516
   135
      apply clarify
kleing@12516
   136
      apply (rule conjI)
kleing@12516
   137
       apply simp
kleing@12516
   138
       apply (blast dest: boundedD)
kleing@12516
   139
      apply blast
kleing@10496
   140
   apply clarify
kleing@10496
   141
   apply (erule allE)
kleing@10496
   142
   apply (erule impE)
kleing@10496
   143
    apply assumption
kleing@10496
   144
   apply (drule bspec)
kleing@10496
   145
    apply assumption
kleing@10496
   146
   apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
kleing@12516
   147
   apply blast
kleing@10496
   148
  apply clarify 
kleing@10496
   149
  apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
kleing@10496
   150
  done
kleing@10496
   151
kleing@10496
   152
nipkow@13074
   153
lemma (in semilat) list_update_le_listI [rule_format]:
kleing@13006
   154
  "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
nipkow@13074
   155
   x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"
nipkow@13074
   156
  apply(insert semilat)
kleing@10496
   157
  apply (unfold Listn.le_def lesub_def semilat_def)
kleing@10496
   158
  apply (simp add: list_all2_conv_all_nth nth_list_update)
kleing@10496
   159
  done
kleing@10496
   160
nipkow@13074
   161
lemma (in semilat) merges_pres_le_ub:
wenzelm@18372
   162
  assumes "set ts <= A" and "set ss <= A"
wenzelm@18372
   163
    and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts"
wenzelm@18372
   164
  shows "merges f ps ss <=[r] ts"
kleing@10496
   165
proof -
nipkow@13074
   166
  { fix t ts ps
kleing@10496
   167
    have
nipkow@13074
   168
    "\<And>qs. \<lbrakk>set ts <= A; \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p< size ts \<rbrakk> \<Longrightarrow>
kleing@13006
   169
    set qs <= set ps  \<longrightarrow> 
kleing@13006
   170
    (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
kleing@10496
   171
    apply (induct_tac qs)
kleing@10496
   172
     apply simp
kleing@10496
   173
    apply (simp (no_asm_simp))
kleing@10496
   174
    apply clarify
kleing@10496
   175
    apply (rotate_tac -2)
kleing@10496
   176
    apply simp
kleing@10496
   177
    apply (erule allE, erule impE, erule_tac [2] mp)
kleing@12516
   178
     apply (drule bspec, assumption)
kleing@12516
   179
     apply (simp add: closedD)
kleing@12516
   180
    apply (drule bspec, assumption)
kleing@10496
   181
    apply (simp add: list_update_le_listI)
kleing@12516
   182
    done 
kleing@10496
   183
  } note this [dest]
kleing@10496
   184
  
wenzelm@18372
   185
  from prems show ?thesis by blast
kleing@10496
   186
qed
kleing@10496
   187
kleing@10496
   188
kleing@12516
   189
(** propa **)
kleing@10496
   190
kleing@10496
   191
kleing@12516
   192
lemma decomp_propa:
kleing@13006
   193
  "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> 
kleing@12516
   194
   propa f qs ss w = 
kleing@12516
   195
   (merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)"
kleing@12516
   196
  apply (induct qs)
kleing@12516
   197
   apply simp   
kleing@10496
   198
  apply (simp (no_asm))
kleing@12516
   199
  apply clarify  
kleing@12516
   200
  apply simp
kleing@12516
   201
  apply (rule conjI) 
kleing@10496
   202
   apply blast
kleing@10496
   203
  apply (simp add: nth_list_update)
kleing@10496
   204
  apply blast
kleing@10496
   205
  done 
kleing@10496
   206
kleing@10496
   207
(** iter **)
kleing@10496
   208
nipkow@13074
   209
lemma (in semilat) stable_pres_lemma:
nipkow@13074
   210
shows "\<lbrakk>pres_type step n A; bounded step n; 
kleing@12516
   211
     ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
kleing@12516
   212
     \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
kleing@12516
   213
     \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q; 
kleing@13006
   214
     q \<notin> w \<or> q = p \<rbrakk> 
kleing@13006
   215
  \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
kleing@10496
   216
  apply (unfold stable_def)
kleing@12516
   217
  apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
kleing@12516
   218
   prefer 2
kleing@12516
   219
   apply clarify
kleing@12516
   220
   apply (erule pres_typeD)
kleing@12516
   221
    prefer 3 apply assumption
kleing@12516
   222
    apply (rule listE_nth_in)
kleing@12516
   223
     apply assumption
kleing@12516
   224
    apply simp
kleing@12516
   225
   apply simp
kleing@10496
   226
  apply simp
kleing@10496
   227
  apply clarify
nipkow@13074
   228
  apply (subst nth_merges)
kleing@12516
   229
       apply simp
kleing@12516
   230
       apply (blast dest: boundedD)
kleing@10496
   231
      apply assumption
kleing@12516
   232
     apply clarify
kleing@12516
   233
     apply (rule conjI)
kleing@12516
   234
      apply (blast dest: boundedD)
kleing@12516
   235
     apply (erule pres_typeD)
kleing@12516
   236
       prefer 3 apply assumption
kleing@12516
   237
      apply simp
nipkow@13074
   238
     apply simp
nipkow@13074
   239
apply(subgoal_tac "q < length ss")
nipkow@13074
   240
prefer 2 apply simp
nipkow@13074
   241
  apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
nipkow@13074
   242
apply assumption
kleing@12516
   243
  apply clarify
kleing@10496
   244
  apply (rule conjI)
kleing@12516
   245
   apply (blast dest: boundedD)
kleing@12516
   246
  apply (erule pres_typeD)
kleing@12516
   247
     prefer 3 apply assumption
kleing@12516
   248
    apply simp
kleing@12516
   249
   apply simp
kleing@12516
   250
  apply (drule_tac P = "\<lambda>x. (a, b) \<in> set (step q x)" in subst)
kleing@12516
   251
   apply assumption
kleing@12516
   252
kleing@12516
   253
 apply (simp add: plusplus_empty)
kleing@12516
   254
 apply (cases "q \<in> w")
kleing@12516
   255
  apply simp
kleing@12516
   256
  apply (rule ub1')
wenzelm@23467
   257
     apply (rule semilat)
kleing@12516
   258
    apply clarify
kleing@12516
   259
    apply (rule pres_typeD)
kleing@12516
   260
       apply assumption
kleing@12516
   261
      prefer 3 apply assumption
kleing@12516
   262
     apply (blast intro: listE_nth_in dest: boundedD)
kleing@12516
   263
    apply (blast intro: pres_typeD dest: boundedD)
kleing@12516
   264
   apply (blast intro: listE_nth_in dest: boundedD)
kleing@12516
   265
  apply assumption
kleing@10496
   266
kleing@12516
   267
 apply simp
kleing@12516
   268
 apply (erule allE, erule impE, assumption, erule impE, assumption)
kleing@12516
   269
 apply (rule order_trans)
kleing@12516
   270
   apply simp
kleing@12516
   271
  defer
nipkow@13074
   272
 apply (rule pp_ub2)(*
nipkow@13074
   273
    apply assumption*)
kleing@12516
   274
   apply simp
kleing@12516
   275
   apply clarify
kleing@12516
   276
   apply simp
kleing@12516
   277
   apply (rule pres_typeD)
kleing@12516
   278
      apply assumption
kleing@12516
   279
     prefer 3 apply assumption
kleing@12516
   280
    apply (blast intro: listE_nth_in dest: boundedD)
kleing@12516
   281
   apply (blast intro: pres_typeD dest: boundedD)
kleing@12516
   282
  apply (blast intro: listE_nth_in dest: boundedD)
kleing@12516
   283
 apply blast
kleing@12516
   284
 done
nipkow@13074
   285
nipkow@13074
   286
nipkow@13074
   287
lemma (in semilat) merges_bounded_lemma:
nipkow@13074
   288
 "\<lbrakk> mono r step n A; bounded step n; 
nipkow@13074
   289
    \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
nipkow@13074
   290
    ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
kleing@13066
   291
  \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts" 
kleing@10496
   292
  apply (unfold stable_def)
kleing@12516
   293
  apply (rule merges_pres_le_ub)
kleing@12516
   294
     apply simp
kleing@12516
   295
    apply simp
kleing@12516
   296
   prefer 2 apply assumption
kleing@12516
   297
kleing@12516
   298
  apply clarsimp
kleing@12516
   299
  apply (drule boundedD, assumption+)
kleing@12516
   300
  apply (erule allE, erule impE, assumption)
kleing@12516
   301
  apply (drule bspec, assumption)
kleing@12516
   302
  apply simp
kleing@12516
   303
kleing@12516
   304
  apply (drule monoD [of _ _ _ _ p "ss!p"  "ts!p"])
kleing@12516
   305
     apply assumption
kleing@12516
   306
    apply simp
kleing@12516
   307
   apply (simp add: le_listD)
kleing@12516
   308
  
kleing@13066
   309
  apply (drule lesub_step_typeD, assumption) 
kleing@12516
   310
  apply clarify
kleing@12516
   311
  apply (drule bspec, assumption)
kleing@12516
   312
  apply simp
kleing@12516
   313
  apply (blast intro: order_trans)
kleing@10496
   314
  done
kleing@10496
   315
nipkow@13074
   316
lemma termination_lemma: includes semilat
nipkow@13074
   317
shows "\<lbrakk> ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
kleing@12516
   318
      ss <[r] merges f qs ss \<or> 
kleing@12516
   319
  merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
nipkow@13074
   320
apply(insert semilat)
nipkow@11175
   321
  apply (unfold lesssub_def)
nipkow@11175
   322
  apply (simp (no_asm_simp) add: merges_incr)
kleing@10496
   323
  apply (rule impI)
nipkow@11175
   324
  apply (rule merges_same_conv [THEN iffD1, elim_format]) 
nipkow@11175
   325
  apply assumption+
nipkow@11175
   326
    defer
nipkow@11175
   327
    apply (rule sym, assumption)
kleing@12516
   328
   defer apply simp
kleing@12516
   329
   apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
nipkow@11175
   330
   apply (blast intro!: psubsetI elim: equalityE)
kleing@12516
   331
   apply clarsimp
kleing@12516
   332
   apply (drule bspec, assumption) 
kleing@12516
   333
   apply (drule bspec, assumption)
kleing@12516
   334
   apply clarsimp
kleing@12516
   335
  done 
kleing@10496
   336
nipkow@13074
   337
lemma iter_properties[rule_format]: includes semilat
nipkow@13074
   338
shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;
kleing@12516
   339
     bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
kleing@12516
   340
     \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
kleing@12516
   341
   iter f step ss0 w0 = (ss',w')
nipkow@11175
   342
   \<longrightarrow>
kleing@12516
   343
   ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>
kleing@12516
   344
   (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
nipkow@13074
   345
apply(insert semilat)
nipkow@11298
   346
apply (unfold iter_def stables_def)
nipkow@11175
   347
apply (rule_tac P = "%(ss,w).
kleing@12516
   348
 ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
kleing@12516
   349
 (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and>
nipkow@11175
   350
 (\<forall>p\<in>w. p < n)" and
nipkow@11175
   351
 r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset"
nipkow@11175
   352
       in while_rule)
nipkow@11175
   353
kleing@12516
   354
-- "Invariant holds initially:"
nipkow@13074
   355
apply (simp add:stables_def)
kleing@12516
   356
kleing@12516
   357
-- "Invariant is preserved:"
nipkow@11175
   358
apply(simp add: stables_def split_paired_all)
nipkow@11175
   359
apply(rename_tac ss w)
nipkow@11175
   360
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
nipkow@11175
   361
 prefer 2; apply (fast intro: someI)
kleing@12516
   362
apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
kleing@12516
   363
 prefer 2
kleing@12516
   364
 apply clarify
kleing@12516
   365
 apply (rule conjI)
kleing@12516
   366
  apply(clarsimp, blast dest!: boundedD)
kleing@12516
   367
 apply (erule pres_typeD)
kleing@12516
   368
  prefer 3
kleing@12516
   369
  apply assumption
kleing@12516
   370
  apply (erule listE_nth_in)
paulson@14365
   371
  apply simp
paulson@14365
   372
 apply simp
nipkow@11175
   373
apply (subst decomp_propa)
paulson@14365
   374
 apply fast
nipkow@11175
   375
apply simp
nipkow@11175
   376
apply (rule conjI)
nipkow@13074
   377
 apply (rule merges_preserves_type)
nipkow@13074
   378
 apply blast
kleing@12516
   379
 apply clarify
kleing@12516
   380
 apply (rule conjI)
paulson@14365
   381
  apply(clarsimp, fast dest!: boundedD)
kleing@12516
   382
 apply (erule pres_typeD)
kleing@12516
   383
  prefer 3
kleing@12516
   384
  apply assumption
kleing@12516
   385
  apply (erule listE_nth_in)
kleing@12516
   386
  apply blast
kleing@12516
   387
 apply blast
nipkow@13074
   388
apply (rule conjI)
nipkow@13074
   389
 apply clarify
nipkow@11175
   390
 apply (blast intro!: stable_pres_lemma)
nipkow@13074
   391
apply (rule conjI)
nipkow@11175
   392
 apply (blast intro!: merges_incr intro: le_list_trans)
nipkow@11175
   393
apply (rule conjI)
nipkow@11175
   394
 apply clarsimp
kleing@12516
   395
 apply (blast intro!: merges_bounded_lemma)
nipkow@11175
   396
apply (blast dest!: boundedD)
nipkow@11175
   397
nipkow@11175
   398
kleing@12516
   399
-- "Postcondition holds upon termination:"
nipkow@13074
   400
apply(clarsimp simp add: stables_def split_paired_all)
kleing@12516
   401
kleing@12516
   402
-- "Well-foundedness of the termination relation:"
nipkow@11175
   403
apply (rule wf_lex_prod)
nipkow@13074
   404
 apply (insert orderI [THEN acc_le_listI])
berghofe@22271
   405
 apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
kleing@12516
   406
apply (rule wf_finite_psubset) 
nipkow@11175
   407
kleing@12516
   408
-- "Loop decreases along termination relation:"
nipkow@11175
   409
apply(simp add: stables_def split_paired_all)
nipkow@11175
   410
apply(rename_tac ss w)
nipkow@11175
   411
apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
nipkow@11175
   412
 prefer 2; apply (fast intro: someI)
kleing@12516
   413
apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
kleing@12516
   414
 prefer 2
kleing@12516
   415
 apply clarify
kleing@12516
   416
 apply (rule conjI)
kleing@12516
   417
  apply(clarsimp, blast dest!: boundedD)
kleing@12516
   418
 apply (erule pres_typeD)
kleing@12516
   419
  prefer 3
kleing@12516
   420
  apply assumption
kleing@12516
   421
  apply (erule listE_nth_in)
kleing@12516
   422
  apply blast
kleing@12516
   423
 apply blast
nipkow@11175
   424
apply (subst decomp_propa)
kleing@12516
   425
 apply blast
nipkow@13074
   426
apply clarify
nipkow@11175
   427
apply (simp del: listE_length
kleing@12516
   428
    add: lex_prod_def finite_psubset_def 
nipkow@11175
   429
         bounded_nat_set_is_finite)
kleing@12516
   430
apply (rule termination_lemma)
kleing@12516
   431
apply assumption+
kleing@12516
   432
defer
kleing@12516
   433
apply assumption
kleing@12516
   434
apply clarsimp
nipkow@13074
   435
done
kleing@12516
   436
nipkow@11175
   437
nipkow@13074
   438
lemma kildall_properties: includes semilat
nipkow@13074
   439
shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;
kleing@12516
   440
     bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
kleing@12516
   441
  kildall r f step ss0 \<in> list n A \<and>
kleing@12516
   442
  stables r step (kildall r f step ss0) \<and>
kleing@12516
   443
  ss0 <=[r] kildall r f step ss0 \<and>
kleing@12516
   444
  (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
kleing@12516
   445
                 kildall r f step ss0 <=[r] ts)"
nipkow@11229
   446
apply (unfold kildall_def)
kleing@12516
   447
apply(case_tac "iter f step ss0 (unstables r step ss0)")
nipkow@11298
   448
apply(simp)
nipkow@11229
   449
apply (rule iter_properties)
wenzelm@23467
   450
apply (simp_all add: unstables_def stable_def)
wenzelm@23467
   451
apply (rule semilat)
wenzelm@23467
   452
done
nipkow@13074
   453
kleing@10496
   454
nipkow@13074
   455
lemma is_bcv_kildall: includes semilat
nipkow@13074
   456
shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>
kleing@13006
   457
  \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
nipkow@11299
   458
apply(unfold is_bcv_def wt_step_def)
nipkow@13074
   459
apply(insert semilat kildall_properties[of A])
nipkow@11229
   460
apply(simp add:stables_def)
nipkow@11229
   461
apply clarify
kleing@12516
   462
apply(subgoal_tac "kildall r f step ss \<in> list n A")
nipkow@11229
   463
 prefer 2 apply (simp(no_asm_simp))
nipkow@11229
   464
apply (rule iffI)
kleing@12516
   465
 apply (rule_tac x = "kildall r f step ss" in bexI) 
nipkow@11229
   466
  apply (rule conjI)
nipkow@13074
   467
   apply (blast)
nipkow@11229
   468
  apply (simp  (no_asm_simp))
nipkow@13074
   469
 apply(assumption)
nipkow@11229
   470
apply clarify
kleing@12516
   471
apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")
nipkow@11229
   472
 apply simp
nipkow@11229
   473
apply (blast intro!: le_listD less_lengthI)
nipkow@11229
   474
done
kleing@10496
   475
nipkow@14191
   476
end