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