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