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