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;
     1 (*  Title:      HOL/MicroJava/BV/Kildall.thy

     2     ID:         $Id$

     3     Author:     Tobias Nipkow, Gerwin Klein

     4     Copyright   2000 TUM

     5

     6 Kildall's algorithm

     7 *)

     8

     9 header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}

    10

    11 theory Kildall imports SemilatAlg While_Combinator begin

    12

    13

    14 consts

    15  iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>

    16           's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"

    17  propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set"

    18

    19 primrec

    20 "propa f []      ss w = (ss,w)"

    21 "propa f (q'#qs) ss w = (let (q,t) = q';

    22                              u = t +_f ss!q;

    23                              w' = (if u = ss!q then w else insert q w)

    24                          in propa f qs (ss[q := u]) w')"

    25

    26 defs iter_def:

    27 "iter f step ss w ==

    28  while (%(ss,w). w \<noteq> {})

    29        (%(ss,w). let p = SOME p. p \<in> w

    30                  in propa f (step p (ss!p)) ss (w-{p}))

    31        (ss,w)"

    32

    33 constdefs

    34  unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set"

    35 "unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}"

    36

    37  kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list"

    38 "kildall r f step ss == fst(iter f step ss (unstables r step ss))"

    39

    40 consts merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"

    41 primrec

    42 "merges f []      ss = ss"

    43 "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"

    44

    45

    46 lemmas [simp] = Let_def semilat.le_iff_plus_unchanged [symmetric]

    47

    48

    49 lemma (in semilat) nth_merges:

    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>

    51   (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"

    52   (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")

    53 proof (induct ps)

    54   show "\<And>ss. ?P ss []" by simp

    55

    56   fix ss p' ps'

    57   assume ss: "ss \<in> list n A"

    58   assume l:  "p < length ss"

    59   assume "?steptype (p'#ps')"

    60   then obtain a b where

    61     p': "p'=(a,b)" and ab: "a<n" "b\<in>A" and ps': "?steptype ps'"

    62     by (cases p') auto

    63   assume "\<And>ss. p< length ss \<Longrightarrow> ss \<in> list n A \<Longrightarrow> ?steptype ps' \<Longrightarrow> ?P ss ps'"

    64   from this [OF _ _ ps'] have IH: "\<And>ss. ss \<in> list n A \<Longrightarrow> p < length ss \<Longrightarrow> ?P ss ps'" .

    65

    66   from ss ab

    67   have "ss[a := b +_f ss!a] \<in> list n A" by (simp add: closedD)

    68   moreover

    69   from calculation l

    70   have "p < length (ss[a := b +_f ss!a])" by simp

    71   ultimately

    72   have "?P (ss[a := b +_f ss!a]) ps'" by (rule IH)

    73   with p' l

    74   show "?P ss (p'#ps')" by simp

    75 qed

    76

    77

    78 (** merges **)

    79

    80 lemma length_merges [rule_format, simp]:

    81   "\<forall>ss. size(merges f ps ss) = size ss"

    82   by (induct_tac ps, auto)

    83

    84

    85 lemma (in semilat) merges_preserves_type_lemma:

    86 shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)

    87           \<longrightarrow> merges f ps xs \<in> list n A"

    88 apply (insert closedI)

    89 apply (unfold closed_def)

    90 apply (induct_tac ps)

    91  apply simp

    92 apply clarsimp

    93 done

    94

    95 lemma (in semilat) merges_preserves_type [simp]:

    96  "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>

    97   \<Longrightarrow> merges f ps xs \<in> list n A"

    98 by (simp add: merges_preserves_type_lemma)

    99

   100 lemma (in semilat) merges_incr_lemma:

   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"

   102 apply (induct_tac ps)

   103  apply simp

   104 apply simp

   105 apply clarify

   106 apply (rule order_trans)

   107   apply simp

   108  apply (erule list_update_incr)

   109   apply simp

   110  apply simp

   111 apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])

   112 done

   113

   114 lemma (in semilat) merges_incr:

   115  "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk>

   116   \<Longrightarrow> xs <=[r] merges f ps xs"

   117   by (simp add: merges_incr_lemma)

   118

   119

   120 lemma (in semilat) merges_same_conv [rule_format]:

   121  "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow>

   122      (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"

   123   apply (induct_tac ps)

   124    apply simp

   125   apply clarsimp

   126   apply (rename_tac p x ps xs)

   127   apply (rule iffI)

   128    apply (rule context_conjI)

   129     apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")

   130      apply (drule_tac p = p in le_listD)

   131       apply simp

   132      apply simp

   133     apply (erule subst, rule merges_incr)

   134        apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])

   135       apply clarify

   136       apply (rule conjI)

   137        apply simp

   138        apply (blast dest: boundedD)

   139       apply blast

   140    apply clarify

   141    apply (erule allE)

   142    apply (erule impE)

   143     apply assumption

   144    apply (drule bspec)

   145     apply assumption

   146    apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])

   147    apply blast

   148   apply clarify

   149   apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])

   150   done

   151

   152

   153 lemma (in semilat) list_update_le_listI [rule_format]:

   154   "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>

   155    x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"

   156   apply(insert semilat)

   157   apply (unfold Listn.le_def lesub_def semilat_def)

   158   apply (simp add: list_all2_conv_all_nth nth_list_update)

   159   done

   160

   161 lemma (in semilat) merges_pres_le_ub:

   162   assumes "set ts <= A" and "set ss <= A"

   163     and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts"

   164   shows "merges f ps ss <=[r] ts"

   165 proof -

   166   { fix t ts ps

   167     have

   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>

   169     set qs <= set ps  \<longrightarrow>

   170     (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"

   171     apply (induct_tac qs)

   172      apply simp

   173     apply (simp (no_asm_simp))

   174     apply clarify

   175     apply (rotate_tac -2)

   176     apply simp

   177     apply (erule allE, erule impE, erule_tac [2] mp)

   178      apply (drule bspec, assumption)

   179      apply (simp add: closedD)

   180     apply (drule bspec, assumption)

   181     apply (simp add: list_update_le_listI)

   182     done

   183   } note this [dest]

   184

   185   from prems show ?thesis by blast

   186 qed

   187

   188

   189 (** propa **)

   190

   191

   192 lemma decomp_propa:

   193   "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow>

   194    propa f qs ss w =

   195    (merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)"

   196   apply (induct qs)

   197    apply simp

   198   apply (simp (no_asm))

   199   apply clarify

   200   apply simp

   201   apply (rule conjI)

   202    apply blast

   203   apply (simp add: nth_list_update)

   204   apply blast

   205   done

   206

   207 (** iter **)

   208

   209 lemma (in semilat) stable_pres_lemma:

   210 shows "\<lbrakk>pres_type step n A; bounded step n;

   211      ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n;

   212      \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n;

   213      \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q;

   214      q \<notin> w \<or> q = p \<rbrakk>

   215   \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"

   216   apply (unfold stable_def)

   217   apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")

   218    prefer 2

   219    apply clarify

   220    apply (erule pres_typeD)

   221     prefer 3 apply assumption

   222     apply (rule listE_nth_in)

   223      apply assumption

   224     apply simp

   225    apply simp

   226   apply simp

   227   apply clarify

   228   apply (subst nth_merges)

   229        apply simp

   230        apply (blast dest: boundedD)

   231       apply assumption

   232      apply clarify

   233      apply (rule conjI)

   234       apply (blast dest: boundedD)

   235      apply (erule pres_typeD)

   236        prefer 3 apply assumption

   237       apply simp

   238      apply simp

   239 apply(subgoal_tac "q < length ss")

   240 prefer 2 apply simp

   241   apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)

   242 apply assumption

   243   apply clarify

   244   apply (rule conjI)

   245    apply (blast dest: boundedD)

   246   apply (erule pres_typeD)

   247      prefer 3 apply assumption

   248     apply simp

   249    apply simp

   250   apply (drule_tac P = "\<lambda>x. (a, b) \<in> set (step q x)" in subst)

   251    apply assumption

   252

   253  apply (simp add: plusplus_empty)

   254  apply (cases "q \<in> w")

   255   apply simp

   256   apply (rule ub1')

   257      apply (rule semilat)

   258     apply clarify

   259     apply (rule pres_typeD)

   260        apply assumption

   261       prefer 3 apply assumption

   262      apply (blast intro: listE_nth_in dest: boundedD)

   263     apply (blast intro: pres_typeD dest: boundedD)

   264    apply (blast intro: listE_nth_in dest: boundedD)

   265   apply assumption

   266

   267  apply simp

   268  apply (erule allE, erule impE, assumption, erule impE, assumption)

   269  apply (rule order_trans)

   270    apply simp

   271   defer

   272  apply (rule pp_ub2)(*

   273     apply assumption*)

   274    apply simp

   275    apply clarify

   276    apply simp

   277    apply (rule pres_typeD)

   278       apply assumption

   279      prefer 3 apply assumption

   280     apply (blast intro: listE_nth_in dest: boundedD)

   281    apply (blast intro: pres_typeD dest: boundedD)

   282   apply (blast intro: listE_nth_in dest: boundedD)

   283  apply blast

   284  done

   285

   286

   287 lemma (in semilat) merges_bounded_lemma:

   288  "\<lbrakk> mono r step n A; bounded step n;

   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;

   290     ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk>

   291   \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"

   292   apply (unfold stable_def)

   293   apply (rule merges_pres_le_ub)

   294      apply simp

   295     apply simp

   296    prefer 2 apply assumption

   297

   298   apply clarsimp

   299   apply (drule boundedD, assumption+)

   300   apply (erule allE, erule impE, assumption)

   301   apply (drule bspec, assumption)

   302   apply simp

   303

   304   apply (drule monoD [of _ _ _ _ p "ss!p"  "ts!p"])

   305      apply assumption

   306     apply simp

   307    apply (simp add: le_listD)

   308

   309   apply (drule lesub_step_typeD, assumption)

   310   apply clarify

   311   apply (drule bspec, assumption)

   312   apply simp

   313   apply (blast intro: order_trans)

   314   done

   315

   316 lemma termination_lemma: includes semilat

   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>

   318       ss <[r] merges f qs ss \<or>

   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"

   320 apply(insert semilat)

   321   apply (unfold lesssub_def)

   322   apply (simp (no_asm_simp) add: merges_incr)

   323   apply (rule impI)

   324   apply (rule merges_same_conv [THEN iffD1, elim_format])

   325   apply assumption+

   326     defer

   327     apply (rule sym, assumption)

   328    defer apply simp

   329    apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")

   330    apply (blast intro!: psubsetI elim: equalityE)

   331    apply clarsimp

   332    apply (drule bspec, assumption)

   333    apply (drule bspec, assumption)

   334    apply clarsimp

   335   done

   336

   337 lemma iter_properties[rule_format]: includes semilat

   338 shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;

   339      bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;

   340      \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>

   341    iter f step ss0 w0 = (ss',w')

   342    \<longrightarrow>

   343    ss' \<in> list n A \<and> stables r step ss' \<and> ss0 <=[r] ss' \<and>

   344    (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"

   345 apply(insert semilat)

   346 apply (unfold iter_def stables_def)

   347 apply (rule_tac P = "%(ss,w).

   348  ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>

   349  (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and>

   350  (\<forall>p\<in>w. p < n)" and

   351  r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset"

   352        in while_rule)

   353

   354 -- "Invariant holds initially:"

   355 apply (simp add:stables_def)

   356

   357 -- "Invariant is preserved:"

   358 apply(simp add: stables_def split_paired_all)

   359 apply(rename_tac ss w)

   360 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")

   361  prefer 2; apply (fast intro: someI)

   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")

   363  prefer 2

   364  apply clarify

   365  apply (rule conjI)

   366   apply(clarsimp, blast dest!: boundedD)

   367  apply (erule pres_typeD)

   368   prefer 3

   369   apply assumption

   370   apply (erule listE_nth_in)

   371   apply simp

   372  apply simp

   373 apply (subst decomp_propa)

   374  apply fast

   375 apply simp

   376 apply (rule conjI)

   377  apply (rule merges_preserves_type)

   378  apply blast

   379  apply clarify

   380  apply (rule conjI)

   381   apply(clarsimp, fast dest!: boundedD)

   382  apply (erule pres_typeD)

   383   prefer 3

   384   apply assumption

   385   apply (erule listE_nth_in)

   386   apply blast

   387  apply blast

   388 apply (rule conjI)

   389  apply clarify

   390  apply (blast intro!: stable_pres_lemma)

   391 apply (rule conjI)

   392  apply (blast intro!: merges_incr intro: le_list_trans)

   393 apply (rule conjI)

   394  apply clarsimp

   395  apply (blast intro!: merges_bounded_lemma)

   396 apply (blast dest!: boundedD)

   397

   398

   399 -- "Postcondition holds upon termination:"

   400 apply(clarsimp simp add: stables_def split_paired_all)

   401

   402 -- "Well-foundedness of the termination relation:"

   403 apply (rule wf_lex_prod)

   404  apply (insert orderI [THEN acc_le_listI])

   405  apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])

   406 apply (rule wf_finite_psubset)

   407

   408 -- "Loop decreases along termination relation:"

   409 apply(simp add: stables_def split_paired_all)

   410 apply(rename_tac ss w)

   411 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")

   412  prefer 2; apply (fast intro: someI)

   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")

   414  prefer 2

   415  apply clarify

   416  apply (rule conjI)

   417   apply(clarsimp, blast dest!: boundedD)

   418  apply (erule pres_typeD)

   419   prefer 3

   420   apply assumption

   421   apply (erule listE_nth_in)

   422   apply blast

   423  apply blast

   424 apply (subst decomp_propa)

   425  apply blast

   426 apply clarify

   427 apply (simp del: listE_length

   428     add: lex_prod_def finite_psubset_def

   429          bounded_nat_set_is_finite)

   430 apply (rule termination_lemma)

   431 apply assumption+

   432 defer

   433 apply assumption

   434 apply clarsimp

   435 done

   436

   437

   438 lemma kildall_properties: includes semilat

   439 shows "\<lbrakk> acc r; pres_type step n A; mono r step n A;

   440      bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>

   441   kildall r f step ss0 \<in> list n A \<and>

   442   stables r step (kildall r f step ss0) \<and>

   443   ss0 <=[r] kildall r f step ss0 \<and>

   444   (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>

   445                  kildall r f step ss0 <=[r] ts)"

   446 apply (unfold kildall_def)

   447 apply(case_tac "iter f step ss0 (unstables r step ss0)")

   448 apply(simp)

   449 apply (rule iter_properties)

   450 apply (simp_all add: unstables_def stable_def)

   451 apply (rule semilat)

   452 done

   453

   454

   455 lemma is_bcv_kildall: includes semilat

   456 shows "\<lbrakk> acc r; top r T; pres_type step n A; bounded step n; mono r step n A \<rbrakk>

   457   \<Longrightarrow> is_bcv r T step n A (kildall r f step)"

   458 apply(unfold is_bcv_def wt_step_def)

   459 apply(insert semilat kildall_properties[of A])

   460 apply(simp add:stables_def)

   461 apply clarify

   462 apply(subgoal_tac "kildall r f step ss \<in> list n A")

   463  prefer 2 apply (simp(no_asm_simp))

   464 apply (rule iffI)

   465  apply (rule_tac x = "kildall r f step ss" in bexI)

   466   apply (rule conjI)

   467    apply (blast)

   468   apply (simp  (no_asm_simp))

   469  apply(assumption)

   470 apply clarify

   471 apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")

   472  apply simp

   473 apply (blast intro!: le_listD less_lengthI)

   474 done

   475

   476 end