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