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