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