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