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