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 \ 's step_type \  nipkow@11298  16  's list \ nat set \ 's list \ nat set"  kleing@13006  17  propa :: "'s binop \ (nat \ 's) list \ 's list \ nat set \ '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 \ {})  kleing@12516  29  (%(ss,w). let p = SOME p. p \ 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 \ 's step_type \ 's list \ nat set"  kleing@12516  35 "unstables r step ss == {p. p < size ss \ \stable r step ss p}"  kleing@10496  36 kleing@13006  37  kildall :: "'s ord \ 's binop \ 's step_type \ 's list \ '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 \ (nat \ 's) list \ 's list \ '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  "\ss. \p < length ss; ss \ list n A; \(p,t)\set ps. p t\A \ \  nipkow@23281  51  (merges f ps ss)!p = map snd [(p',t') \ ps. p'=p] ++_f ss!p"  nipkow@13074  52  (is "\ss. \_; _; ?steptype ps\ \ ?P ss ps")  kleing@12516  53 proof (induct ps)  kleing@12516  54  show "\ss. ?P ss []" by simp  kleing@12516  55 kleing@12516  56  fix ss p' ps'  kleing@12516  57  assume ss: "ss \ 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: "aA" and ps': "?steptype ps'"  wenzelm@23467  62  by (cases p') auto  nipkow@13074  63  assume "\ss. p< length ss \ ss \ list n A \ ?steptype ps' \ ?P ss ps'"  wenzelm@23467  64  from this [OF _ _ ps'] have IH: "\ss. ss \ list n A \ p < length ss \ ?P ss ps'" .  kleing@12516  65 nipkow@13074  66  from ss ab  kleing@12516  67  have "ss[a := b +_f ss!a] \ 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  "\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 "\xs. xs \ list n A \ (\(p,x) \ set ps. p x\A)  nipkow@13074  87  \ merges f ps xs \ 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  "\ xs \ list n A; \(p,x) \ set ps. p x\A \  kleing@13006  97  \ merges f ps xs \ 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  "\xs. xs \ list n A \ (\(p,x)\set ps. p x \ A) \ 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  "\ xs \ list n A; \(p,x)\set ps. p x \ A \  kleing@13006  116  \ 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  "(\xs. xs \ list n A \ (\(p,x)\set ps. p x\A) \  kleing@12516  122  (merges f ps xs = xs) = (\(p,x)\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 \ set ys <= A \ xs <=[r] ys \ p < size xs \  nipkow@13074  155  x <=_r ys!p \ x\A \ 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 "\(p,t)\set ps. t <=_r ts!p \ t \ A \ 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  "\qs. \set ts <= A; \(p,t)\set ps. t <=_r ts!p \ t \ A \ p< size ts \ \  kleing@13006  169  set qs <= set ps \  kleing@13006  170  (\ss. set ss <= A \ ss <=[r] ts \ 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  "\ss w. (\(q,t)\set qs. q < size ss) \  kleing@12516  194  propa f qs ss w =  kleing@12516  195  (merges f qs ss, {q. \t. (q,t)\set qs \ t +_f ss!q \ 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 "\pres_type step n A; bounded step n;  kleing@12516  211  ss \ list n A; p \ w; \q\w. q < n;  kleing@12516  212  \q. q < n \ q \ w \ stable r step ss q; q < n;  kleing@12516  213  \s'. (q,s') \ set (step p (ss ! p)) \ s' +_f ss ! q = ss ! q;  kleing@13006  214  q \ w \ q = p \  kleing@13006  215  \ stable r step (merges f (step p (ss!p)) ss) q"  kleing@10496  216  apply (unfold stable_def)  kleing@12516  217  apply (subgoal_tac "\s'. (q,s') \ set (step p (ss!p)) \ 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 = "\x. (a, b) \ 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 \ 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  "\ mono r step n A; bounded step n;  nipkow@13074  289  \(p',s') \ set (step p (ss!p)). s' \ A; ss \ list n A; ts \ list n A; p < n;  nipkow@13074  290  ss <=[r] ts; \p. p < n \ stable r step ts p \  kleing@13066  291  \ 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 "\ ss \ list n A; \(q,t)\set qs. q t\A; p\w \ \  kleing@12516  318  ss <[r] merges f qs ss \  kleing@12516  319  merges f qs ss = ss \ {q. \t. (q,t)\set qs \ t +_f ss!q \ 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 "\q t. \((q, t) \ set qs \ t +_f ss ! q \ 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 "\ acc r ; pres_type step n A; mono r step n A;  kleing@12516  339  bounded step n; \p\w0. p < n; ss0 \ list n A;  kleing@12516  340  \p w0 \ stable r step ss0 p \ \  kleing@12516  341  iter f step ss0 w0 = (ss',w')  nipkow@11175  342  \  kleing@12516  343  ss' \ list n A \ stables r step ss' \ ss0 <=[r] ss' \  kleing@12516  344  (\ts\list n A. ss0 <=[r] ts \ stables r step ts \ 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 \ list n A \ (\p w \ stable r step ss p) \ ss0 <=[r] ss \  kleing@12516  349  (\ts\list n A. ss0 <=[r] ts \ stables r step ts \ ss <=[r] ts) \  nipkow@11175  350  (\p\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 \ w) \ w")  nipkow@11175  361  prefer 2; apply (fast intro: someI)  kleing@12516  362 apply(subgoal_tac "\(q,t) \ set (step (SOME p. p \ w) (ss ! (SOME p. p \ w))). q < length ss \ t \ 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 \ w) \ w")  nipkow@11175  412  prefer 2; apply (fast intro: someI)  kleing@12516  413 apply(subgoal_tac "\(q,t) \ set (step (SOME p. p \ w) (ss ! (SOME p. p \ w))). q < length ss \ t \ 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 "\ acc r; pres_type step n A; mono r step n A;  kleing@12516  440  bounded step n; ss0 \ list n A \ \  kleing@12516  441  kildall r f step ss0 \ list n A \  kleing@12516  442  stables r step (kildall r f step ss0) \  kleing@12516  443  ss0 <=[r] kildall r f step ss0 \  kleing@12516  444  (\ts\list n A. ss0 <=[r] ts \ stables r step ts \  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 "\ acc r; top r T; pres_type step n A; bounded step n; mono r step n A \  kleing@13006  457  \ 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 \ 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