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 \ (nat \ 's) list \ 's list \ nat set \ '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 \ 's step_type \ 's list \ nat set \ 's list \ nat set" where  haftmann@35416  20  "iter f step ss w == while (%(ss,w). w \ {})  haftmann@33954  21  (%(ss,w). let p = SOME p. p \ 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 \ 's step_type \ 's list \ nat set" where  haftmann@33954  26 "unstables r step ss == {p. p < size ss \ \stable r step ss p}"  haftmann@33954  27 haftmann@35416  28 definition kildall :: "'s ord \ 's binop \ 's step_type \ 's list \ '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 \ (nat \ 's) list \ 's list \ '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  "\ss. \p < length ss; ss \ list n A; \(p,t)\set ps. p t\A \ \  haftmann@33954  41  (merges f ps ss)!p = map snd [(p',t') \ ps. p'=p] ++_f ss!p"  haftmann@33954  42  (is "\ss. \_; _; ?steptype ps\ \ ?P ss ps")  haftmann@33954  43 proof (induct ps)  haftmann@33954  44  show "\ss. ?P ss []" by simp  haftmann@33954  45 haftmann@33954  46  fix ss p' ps'  haftmann@33954  47  assume ss: "ss \ 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: "aA" and ps': "?steptype ps'"  haftmann@33954  52  by (cases p') auto  haftmann@33954  53  assume "\ss. p< length ss \ ss \ list n A \ ?steptype ps' \ ?P ss ps'"  haftmann@33954  54  from this [OF _ _ ps'] have IH: "\ss. ss \ list n A \ p < length ss \ ?P ss ps'" .  haftmann@33954  55 haftmann@33954  56  from ss ab  haftmann@33954  57  have "ss[a := b +_f ss!a] \ 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  "\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 "\xs. xs \ list n A \ (\(p,x) \ set ps. p x\A)  haftmann@33954  77  \ merges f ps xs \ 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  "\ xs \ list n A; \(p,x) \ set ps. p x\A \  haftmann@33954  87  \ merges f ps xs \ 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  "\xs. xs \ list n A \ (\(p,x)\set ps. p x \ A) \ 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  "\ xs \ list n A; \(p,x)\set ps. p x \ A \  haftmann@33954  106  \ 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  "(\xs. xs \ list n A \ (\(p,x)\set ps. p x\A) \  haftmann@33954  112  (merges f ps xs = xs) = (\(p,x)\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 \ set ys <= A \ xs <=[r] ys \ p < size xs \  haftmann@33954  145  x <=_r ys!p \ x\A \ 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 "\(p,t)\set ps. t <=_r ts!p \ t \ A \ 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  "\qs. \set ts <= A; \(p,t)\set ps. t <=_r ts!p \ t \ A \ p< size ts \ \  haftmann@33954  159  set qs <= set ps \  haftmann@33954  160  (\ss. set ss <= A \ ss <=[r] ts \ 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  "\ss w. (\(q,t)\set qs. q < size ss) \  haftmann@33954  184  propa f qs ss w =  haftmann@33954  185  (merges f qs ss, {q. \t. (q,t)\set qs \ t +_f ss!q \ 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 "\pres_type step n A; bounded step n;  haftmann@33954  201  ss \ list n A; p \ w; \q\w. q < n;  haftmann@33954  202  \q. q < n \ q \ w \ stable r step ss q; q < n;  haftmann@33954  203  \s'. (q,s') \ set (step p (ss ! p)) \ s' +_f ss ! q = ss ! q;  haftmann@33954  204  q \ w \ q = p \  haftmann@33954  205  \ stable r step (merges f (step p (ss!p)) ss) q"  haftmann@33954  206  apply (unfold stable_def)  haftmann@33954  207  apply (subgoal_tac "\s'. (q,s') \ set (step p (ss!p)) \ 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 = "\x. (a, b) \ 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 \ 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  "\ mono r step n A; bounded step n;  haftmann@33954  279  \(p',s') \ set (step p (ss!p)). s' \ A; ss \ list n A; ts \ list n A; p < n;  haftmann@33954  280  ss <=[r] ts; \p. p < n \ stable r step ts p \  haftmann@33954  281  \ 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 "\ ss \ list n A; \(q,t)\set qs. q t\A; p\w \ \  haftmann@33954  309  ss <[r] merges f qs ss \  haftmann@33954  310  merges f qs ss = ss \ {q. \t. (q,t)\set qs \ t +_f ss!q \ 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 "\q t. \((q, t) \ set qs \ t +_f ss ! q \ 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 "\ acc r ; pres_type step n A; mono r step n A;  haftmann@33954  334  bounded step n; \p\w0. p < n; ss0 \ list n A;  haftmann@33954  335  \p w0 \ stable r step ss0 p \ \  haftmann@33954  336  iter f step ss0 w0 = (ss',w')  haftmann@33954  337  \  haftmann@33954  338  ss' \ list n A \ stables r step ss' \ ss0 <=[r] ss' \  haftmann@33954  339  (\ts\list n A. ss0 <=[r] ts \ stables r step ts \ 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 \ list n A \ (\p w \ stable r step ss p) \ ss0 <=[r] ss \  haftmann@33954  347  (\ts\list n A. ss0 <=[r] ts \ stables r step ts \ ss <=[r] ts) \  haftmann@33954  348  (\p\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 \ w) \ w")  haftmann@33954  359  prefer 2; apply (fast intro: someI)  haftmann@33954  360 apply(subgoal_tac "\(q,t) \ set (step (SOME p. p \ w) (ss ! (SOME p. p \ w))). q < length ss \ t \ 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 \ w) \ w")  haftmann@33954  410  prefer 2; apply (fast intro: someI)  haftmann@33954  411 apply(subgoal_tac "\(q,t) \ set (step (SOME p. p \ w) (ss ! (SOME p. p \ w))). q < length ss \ t \ 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 "\ acc r; pres_type step n A; mono r step n A;  haftmann@33954  440  bounded step n; ss0 \ list n A \ \  haftmann@33954  441  kildall r f step ss0 \ list n A \  haftmann@33954  442  stables r step (kildall r f step ss0) \  haftmann@33954  443  ss0 <=[r] kildall r f step ss0 \  haftmann@33954  444  (\ts\list n A. ss0 <=[r] ts \ stables r step ts \  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 "\ acc r; top r T; pres_type step n A; bounded step n; mono r step n A \  haftmann@33954  462  \ 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 \ 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