src/HOL/MicroJava/DFA/Semilat.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61994 133a8a888ae8
child 63258 576fb8068ba6
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/MicroJava/DFA/Semilat.thy
     2     Author:     Tobias Nipkow
     3     Copyright   2000 TUM
     4 *)
     5 
     6 chapter \<open>Bytecode Verifier \label{cha:bv}\<close>
     7 
     8 section \<open>Semilattices\<close>
     9 
    10 theory Semilat
    11 imports Main "~~/src/HOL/Library/While_Combinator"
    12 begin
    13 
    14 type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool"
    15 type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    16 type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop"
    17 
    18 definition lesub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    19   where "lesub x r y \<longleftrightarrow> r x y"
    20 
    21 definition lesssub :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool"
    22   where "lesssub x r y \<longleftrightarrow> lesub x r y \<and> x \<noteq> y"
    23 
    24 definition plussub :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c"
    25   where "plussub x f y = f x y"
    26 
    27 notation (ASCII)
    28   "lesub"  ("(_ /<='__ _)" [50, 1000, 51] 50) and
    29   "lesssub"  ("(_ /<'__ _)" [50, 1000, 51] 50) and
    30   "plussub"  ("(_ /+'__ _)" [65, 1000, 66] 65)
    31 
    32 notation
    33   "lesub"  ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
    34   "lesssub"  ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and
    35   "plussub"  ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65)
    36 
    37 (* allow \<sub> instead of \<bsub>..\<esub> *)
    38 abbreviation (input)
    39   lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50)
    40   where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y"
    41 
    42 abbreviation (input)
    43   lesssub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50)
    44   where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y"
    45 
    46 abbreviation (input)
    47   plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65)
    48   where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y"
    49 
    50 definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where
    51   "ord r \<equiv> \<lambda>x y. (x,y) \<in> r"
    52 
    53 definition order :: "'a ord \<Rightarrow> bool" where
    54   "order r \<equiv> (\<forall>x. x \<sqsubseteq>\<^sub>r x) \<and> (\<forall>x y. x \<sqsubseteq>\<^sub>r y \<and> y \<sqsubseteq>\<^sub>r x \<longrightarrow> x=y) \<and> (\<forall>x y z. x \<sqsubseteq>\<^sub>r y \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<sqsubseteq>\<^sub>r z)"
    55 
    56 definition top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool" where
    57   "top r T \<equiv> \<forall>x. x \<sqsubseteq>\<^sub>r T"
    58   
    59 definition acc :: "'a ord \<Rightarrow> bool" where
    60   "acc r \<equiv> wf {(y,x). x \<sqsubset>\<^sub>r y}"
    61 
    62 definition closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool" where
    63   "closed A f \<equiv> \<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^sub>f y \<in> A"
    64 
    65 definition semilat :: "'a sl \<Rightarrow> bool" where
    66   "semilat \<equiv> \<lambda>(A,r,f). order r \<and> closed A f \<and> 
    67                        (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and>
    68                        (\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and>
    69                        (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z)"
    70 
    71 definition is_ub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
    72   "is_ub r x y u \<equiv> (x,u)\<in>r \<and> (y,u)\<in>r"
    73 
    74 definition is_lub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
    75   "is_lub r x y u \<equiv> is_ub r x y u \<and> (\<forall>z. is_ub r x y z \<longrightarrow> (u,z)\<in>r)"
    76 
    77 definition some_lub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    78   "some_lub r x y \<equiv> SOME z. is_lub r x y z"
    79 
    80 locale Semilat =
    81   fixes A :: "'a set"
    82   fixes r :: "'a ord"
    83   fixes f :: "'a binop"
    84   assumes semilat: "semilat (A, r, f)"
    85 
    86 lemma order_refl [simp, intro]: "order r \<Longrightarrow> x \<sqsubseteq>\<^sub>r x"
    87   (*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*)
    88 
    89 lemma order_antisym: "\<lbrakk> order r; x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r x \<rbrakk> \<Longrightarrow> x = y"
    90   (*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*)
    91 
    92 lemma order_trans: "\<lbrakk> order r; x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r z \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r z"
    93   (*<*) by (unfold order_def) blast (*>*)
    94 
    95 lemma order_less_irrefl [intro, simp]: "order r \<Longrightarrow> \<not> x \<sqsubset>\<^sub>r x"
    96   (*<*) by (unfold order_def lesssub_def) blast (*>*)
    97 
    98 lemma order_less_trans: "\<lbrakk> order r; x \<sqsubset>\<^sub>r y; y \<sqsubset>\<^sub>r z \<rbrakk> \<Longrightarrow> x \<sqsubset>\<^sub>r z"
    99   (*<*) by (unfold order_def lesssub_def) blast (*>*)
   100 
   101 lemma topD [simp, intro]: "top r T \<Longrightarrow> x \<sqsubseteq>\<^sub>r T"
   102   (*<*) by (simp add: top_def) (*>*)
   103 
   104 lemma top_le_conv [simp]: "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T \<sqsubseteq>\<^sub>r x) = (x = T)"
   105   (*<*) by (blast intro: order_antisym) (*>*)
   106 
   107 lemma semilat_Def:
   108 "semilat(A,r,f) \<equiv> order r \<and> closed A f \<and> 
   109                  (\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and> 
   110                  (\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and> 
   111                  (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z)"
   112   (*<*) by (unfold semilat_def) clarsimp (*>*)
   113 
   114 lemma (in Semilat) orderI [simp, intro]: "order r"
   115   (*<*) using semilat by (simp add: semilat_Def) (*>*)
   116 
   117 lemma (in Semilat) closedI [simp, intro]: "closed A f"
   118   (*<*) using semilat by (simp add: semilat_Def) (*>*)
   119 
   120 lemma closedD: "\<lbrakk> closed A f; x\<in>A; y\<in>A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<in> A"
   121   (*<*) by (unfold closed_def) blast (*>*)
   122 
   123 lemma closed_UNIV [simp]: "closed UNIV f"
   124   (*<*) by (simp add: closed_def) (*>*)
   125 
   126 lemma (in Semilat) closed_f [simp, intro]: "\<lbrakk>x \<in> A; y \<in> A\<rbrakk>  \<Longrightarrow> x \<squnion>\<^sub>f y \<in> A"
   127   (*<*) by (simp add: closedD [OF closedI]) (*>*)
   128 
   129 lemma (in Semilat) refl_r [intro, simp]: "x \<sqsubseteq>\<^sub>r x" by simp
   130 
   131 lemma (in Semilat) antisym_r [intro?]: "\<lbrakk> x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r x \<rbrakk> \<Longrightarrow> x = y"
   132   (*<*) by (rule order_antisym) auto (*>*)
   133   
   134 lemma (in Semilat) trans_r [trans, intro?]: "\<lbrakk>x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r z\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r z"
   135   (*<*) by (auto intro: order_trans) (*>*)
   136   
   137 lemma (in Semilat) ub1 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y"
   138   (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
   139 
   140 lemma (in Semilat) ub2 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y"
   141   (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
   142 
   143 lemma (in Semilat) lub [simp, intro?]:
   144   "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z"
   145   (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
   146 
   147 lemma (in Semilat) plus_le_conv [simp]:
   148   "\<lbrakk> x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> (x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z) = (x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z)"
   149   (*<*) by (blast intro: ub1 ub2 lub order_trans) (*>*)
   150 
   151 lemma (in Semilat) le_iff_plus_unchanged: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (x \<squnion>\<^sub>f y = y)"
   152 (*<*)
   153 apply (rule iffI)
   154  apply (blast intro: antisym_r lub ub2)
   155 apply (erule subst)
   156 apply simp
   157 done
   158 (*>*)
   159 
   160 lemma (in Semilat) le_iff_plus_unchanged2: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (y \<squnion>\<^sub>f x = y)"
   161 (*<*)
   162 apply (rule iffI)
   163  apply (blast intro: order_antisym lub ub1)
   164 apply (erule subst)
   165 apply simp
   166 done 
   167 (*>*)
   168 
   169 
   170 lemma (in Semilat) plus_assoc [simp]:
   171   assumes a: "a \<in> A" and b: "b \<in> A" and c: "c \<in> A"
   172   shows "a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c) = a \<squnion>\<^sub>f b \<squnion>\<^sub>f c"
   173 (*<*)
   174 proof -
   175   from a b have ab: "a \<squnion>\<^sub>f b \<in> A" ..
   176   from this c have abc: "(a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c \<in> A" ..
   177   from b c have bc: "b \<squnion>\<^sub>f c \<in> A" ..
   178   from a this have abc': "a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c) \<in> A" ..
   179 
   180   show ?thesis
   181   proof    
   182     show "a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c) \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c"
   183     proof -
   184       from a b have "a \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f b" .. 
   185       also from ab c have "\<dots> \<sqsubseteq>\<^sub>r \<dots> \<squnion>\<^sub>f c" ..
   186       finally have "a<": "a \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" .
   187       from a b have "b \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f b" ..
   188       also from ab c have "\<dots> \<sqsubseteq>\<^sub>r \<dots> \<squnion>\<^sub>f c" ..
   189       finally have "b<": "b \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" .
   190       from ab c have "c<": "c \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" ..    
   191       from "b<" "c<" b c abc have "b \<squnion>\<^sub>f c \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" ..
   192       from "a<" this a bc abc show ?thesis ..
   193     qed
   194     show "(a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" 
   195     proof -
   196       from b c have "b \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f c" .. 
   197       also from a bc have "\<dots> \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f \<dots>" ..
   198       finally have "b<": "b \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" .
   199       from b c have "c \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f c" ..
   200       also from a bc have "\<dots> \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f \<dots>" ..
   201       finally have "c<": "c \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" .
   202       from a bc have "a<": "a \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" ..
   203       from "a<" "b<" a b abc' have "a \<squnion>\<^sub>f b \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" ..
   204       from this "c<" ab c abc' show ?thesis ..
   205     qed
   206   qed
   207 qed
   208 (*>*)
   209 
   210 lemma (in Semilat) plus_com_lemma:
   211   "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a \<squnion>\<^sub>f b \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f a"
   212 (*<*)
   213 proof -
   214   assume a: "a \<in> A" and b: "b \<in> A"  
   215   from b a have "a \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f a" .. 
   216   moreover from b a have "b \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f a" ..
   217   moreover note a b
   218   moreover from b a have "b \<squnion>\<^sub>f a \<in> A" ..
   219   ultimately show ?thesis ..
   220 qed
   221 (*>*)
   222 
   223 lemma (in Semilat) plus_commutative:
   224   "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a \<squnion>\<^sub>f b = b \<squnion>\<^sub>f a"
   225   (*<*) by(blast intro: order_antisym plus_com_lemma) (*>*)
   226 
   227 lemma is_lubD:
   228   "is_lub r x y u \<Longrightarrow> is_ub r x y u \<and> (\<forall>z. is_ub r x y z \<longrightarrow> (u,z) \<in> r)"
   229   (*<*) by (simp add: is_lub_def) (*>*)
   230 
   231 lemma is_ubI:
   232   "\<lbrakk> (x,u) \<in> r; (y,u) \<in> r \<rbrakk> \<Longrightarrow> is_ub r x y u"
   233   (*<*) by (simp add: is_ub_def) (*>*)
   234 
   235 lemma is_ubD:
   236   "is_ub r x y u \<Longrightarrow> (x,u) \<in> r \<and> (y,u) \<in> r"
   237   (*<*) by (simp add: is_ub_def) (*>*)
   238 
   239 
   240 lemma is_lub_bigger1 [iff]:  
   241   "is_lub (r^* ) x y y = ((x,y)\<in>r^* )"
   242 (*<*)
   243 apply (unfold is_lub_def is_ub_def)
   244 apply blast
   245 done
   246 (*>*)
   247 
   248 lemma is_lub_bigger2 [iff]:
   249   "is_lub (r^* ) x y x = ((y,x)\<in>r^* )"
   250 (*<*)
   251 apply (unfold is_lub_def is_ub_def)
   252 apply blast 
   253 done
   254 (*>*)
   255 
   256 lemma extend_lub:
   257   "\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) \<in> r \<rbrakk> 
   258   \<Longrightarrow> EX v. is_lub (r^* ) x' y v"
   259 (*<*)
   260 apply (unfold is_lub_def is_ub_def)
   261 apply (case_tac "(y,x) \<in> r^*")
   262  apply (case_tac "(y,x') \<in> r^*")
   263   apply blast
   264  apply (blast elim: converse_rtranclE dest: single_valuedD)
   265 apply (rule exI)
   266 apply (rule conjI)
   267  apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD)
   268 apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl 
   269              elim: converse_rtranclE dest: single_valuedD)
   270 done
   271 (*>*)
   272 
   273 lemma single_valued_has_lubs [rule_format]:
   274   "\<lbrakk> single_valued r; (x,u) \<in> r^* \<rbrakk> \<Longrightarrow> (\<forall>y. (y,u) \<in> r^* \<longrightarrow> 
   275   (EX z. is_lub (r^* ) x y z))"
   276 (*<*)
   277 apply (erule converse_rtrancl_induct)
   278  apply clarify
   279  apply (erule converse_rtrancl_induct)
   280   apply blast
   281  apply (blast intro: converse_rtrancl_into_rtrancl)
   282 apply (blast intro: extend_lub)
   283 done
   284 (*>*)
   285 
   286 lemma some_lub_conv:
   287   "\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u"
   288 (*<*)
   289 apply (unfold some_lub_def is_lub_def)
   290 apply (rule someI2)
   291  apply assumption
   292 apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl)
   293 done
   294 (*>*)
   295 
   296 lemma is_lub_some_lub:
   297   "\<lbrakk> single_valued r; acyclic r; (x,u)\<in>r^*; (y,u)\<in>r^* \<rbrakk> 
   298   \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"
   299   (*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
   300 
   301 subsection\<open>An executable lub-finder\<close>
   302 
   303 definition exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop" where
   304 "exec_lub r f x y \<equiv> while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y"
   305 
   306 lemma exec_lub_refl: "exec_lub r f T T = T"
   307 by (simp add: exec_lub_def while_unfold)
   308 
   309 lemma acyclic_single_valued_finite:
   310  "\<lbrakk>acyclic r; single_valued r; (x,y) \<in> r\<^sup>*\<rbrakk>
   311   \<Longrightarrow> finite (r \<inter> {a. (x, a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})"
   312 (*<*)
   313 apply(erule converse_rtrancl_induct)
   314  apply(rule_tac B = "{}" in finite_subset)
   315   apply(simp only:acyclic_def)
   316   apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl)
   317  apply simp
   318 apply(rename_tac x x')
   319 apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} =
   320                    insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})")
   321  apply simp
   322 apply(blast intro:converse_rtrancl_into_rtrancl
   323             elim:converse_rtranclE dest:single_valuedD)
   324 done
   325 (*>*)
   326 
   327 
   328 lemma exec_lub_conv:
   329   "\<lbrakk> acyclic r; \<forall>x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
   330   exec_lub r f x y = u"
   331 (*<*)
   332 apply(unfold exec_lub_def)
   333 apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and
   334                r = "(r \<inter> {(a,b). (y,a) \<in> r\<^sup>* \<and> (b,u) \<in> r\<^sup>*})^-1" in while_rule)
   335     apply(blast dest: is_lubD is_ubD)
   336    apply(erule conjE)
   337    apply(erule_tac z = u in converse_rtranclE)
   338     apply(blast dest: is_lubD is_ubD)
   339    apply(blast dest:rtrancl_into_rtrancl)
   340   apply(rename_tac s)
   341   apply(subgoal_tac "is_ub (r\<^sup>*) x y s")
   342    prefer 2 apply(simp add:is_ub_def)
   343   apply(subgoal_tac "(u, s) \<in> r\<^sup>*")
   344    prefer 2 apply(blast dest:is_lubD)
   345   apply(erule converse_rtranclE)
   346    apply blast
   347   apply(simp only:acyclic_def)
   348   apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl)
   349  apply(rule finite_acyclic_wf)
   350   apply simp
   351   apply(erule acyclic_single_valued_finite)
   352    apply(blast intro:single_valuedI)
   353   apply(simp add:is_lub_def is_ub_def)
   354  apply simp
   355  apply(erule acyclic_subset)
   356  apply blast
   357 apply simp
   358 apply(erule conjE)
   359 apply(erule_tac z = u in converse_rtranclE)
   360  apply(blast dest: is_lubD is_ubD)
   361 apply(blast dest:rtrancl_into_rtrancl)
   362 done
   363 (*>*)
   364 
   365 lemma is_lub_exec_lub:
   366   "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; \<forall>x y. (x,y) \<in> r \<longrightarrow> f x = y \<rbrakk>
   367   \<Longrightarrow> is_lub (r^* ) x y (exec_lub r f x y)"
   368   (*<*) by (fastforce dest: single_valued_has_lubs simp add: exec_lub_conv) (*>*)
   369 
   370 end