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