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