src/HOL/MicroJava/BV/SemilatAlg.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23464 bc2563c37b1a
child 27611 2c01c0bdb385
permissions -rw-r--r--
Name.uu, Name.aT;
kleing@13062
     1
(*  Title:      HOL/MicroJava/BV/SemilatAlg.thy
kleing@13062
     2
    ID:         $Id$
kleing@13062
     3
    Author:     Gerwin Klein
kleing@13062
     4
    Copyright   2002 Technische Universitaet Muenchen
kleing@13062
     5
*)
kleing@13062
     6
kleing@13062
     7
header {* \isaheader{More on Semilattices} *}
kleing@13062
     8
haftmann@16417
     9
theory SemilatAlg imports Typing_Framework Product begin
kleing@13062
    10
kleing@13062
    11
kleing@13066
    12
constdefs 
kleing@13066
    13
  lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
kleing@13066
    14
                    ("(_ /<=|_| _)" [50, 0, 51] 50)
kleing@13066
    15
  "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
kleing@13066
    16
kleing@13062
    17
consts
kleing@13062
    18
 "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
kleing@13062
    19
primrec
kleing@13062
    20
  "[] ++_f y = y"
kleing@13062
    21
  "(x#xs) ++_f y = xs ++_f (x +_f y)"
kleing@13062
    22
kleing@13062
    23
constdefs
kleing@13062
    24
 bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
kleing@13062
    25
"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  
kleing@13062
    26
kleing@13062
    27
 pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
kleing@13062
    28
"pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
kleing@13062
    29
kleing@13062
    30
 mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
kleing@13062
    31
"mono r step n A ==
kleing@13062
    32
 \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
kleing@13062
    33
kleing@13062
    34
kleing@13062
    35
lemma pres_typeD:
kleing@13062
    36
  "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
kleing@13062
    37
  by (unfold pres_type_def, blast)
kleing@13062
    38
kleing@13062
    39
lemma monoD:
kleing@13062
    40
  "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
kleing@13062
    41
  by (unfold mono_def, blast)
kleing@13062
    42
kleing@13062
    43
lemma boundedD: 
kleing@13062
    44
  "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n" 
kleing@13062
    45
  by (unfold bounded_def, blast)
kleing@13062
    46
kleing@13066
    47
lemma lesubstep_type_refl [simp, intro]:
kleing@13066
    48
  "(\<And>x. x <=_r x) \<Longrightarrow> x <=|r| x"
kleing@13066
    49
  by (unfold lesubstep_type_def) auto
kleing@13066
    50
kleing@13066
    51
lemma lesub_step_typeD:
kleing@13066
    52
  "a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
kleing@13066
    53
  by (unfold lesubstep_type_def) blast
kleing@13066
    54
kleing@13062
    55
kleing@13062
    56
lemma list_update_le_listI [rule_format]:
kleing@13062
    57
  "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
kleing@13062
    58
   x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow> 
kleing@13062
    59
   xs[p := x +_f xs!p] <=[r] ys"
kleing@13062
    60
  apply (unfold Listn.le_def lesub_def semilat_def)
kleing@13062
    61
  apply (simp add: list_all2_conv_all_nth nth_list_update)
kleing@13062
    62
  done
kleing@13062
    63
kleing@13062
    64
nipkow@13074
    65
lemma plusplus_closed: includes semilat shows
nipkow@13074
    66
  "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A"
kleing@13062
    67
proof (induct x)
kleing@13062
    68
  show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
kleing@13062
    69
  fix y x xs
nipkow@13074
    70
  assume y: "y \<in> A" and xs: "set (x#xs) \<subseteq> A"
nipkow@13074
    71
  assume IH: "\<And>y. \<lbrakk> set xs \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> xs ++_f y \<in> A"
wenzelm@23464
    72
  from xs obtain x: "x \<in> A" and xs': "set xs \<subseteq> A" by simp
kleing@13077
    73
  from x y have "(x +_f y) \<in> A" ..
wenzelm@23464
    74
  with xs' have "xs ++_f (x +_f y) \<in> A" by (rule IH)
kleing@13062
    75
  thus "(x#xs) ++_f y \<in> A" by simp
kleing@13062
    76
qed
kleing@13062
    77
nipkow@13074
    78
lemma (in semilat) pp_ub2:
nipkow@13074
    79
 "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
kleing@13062
    80
proof (induct x)
nipkow@13074
    81
  from semilat show "\<And>y. y <=_r [] ++_f y" by simp
kleing@13062
    82
  
kleing@13062
    83
  fix y a l
kleing@13062
    84
  assume y:  "y \<in> A"
kleing@13062
    85
  assume "set (a#l) \<subseteq> A"
nipkow@13074
    86
  then obtain a: "a \<in> A" and x: "set l \<subseteq> A" by simp
nipkow@13074
    87
  assume "\<And>y. \<lbrakk>set l \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r l ++_f y"
wenzelm@23464
    88
  hence IH: "\<And>y. y \<in> A \<Longrightarrow> y <=_r l ++_f y" using x .
kleing@13062
    89
kleing@13077
    90
  from a y have "y <=_r a +_f y" ..
kleing@13077
    91
  also from a y have "a +_f y \<in> A" ..
kleing@13062
    92
  hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)
nipkow@13074
    93
  finally have "y <=_r l ++_f (a +_f y)" .
kleing@13062
    94
  thus "y <=_r (a#l) ++_f y" by simp
kleing@13062
    95
qed
kleing@13062
    96
kleing@13062
    97
nipkow@13074
    98
lemma (in semilat) pp_ub1:
nipkow@13074
    99
shows "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
kleing@13062
   100
proof (induct ls)
kleing@13062
   101
  show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
nipkow@13074
   102
kleing@13062
   103
  fix y s ls
kleing@13062
   104
  assume "set (s#ls) \<subseteq> A"
kleing@13062
   105
  then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
kleing@13062
   106
  assume y: "y \<in> A" 
kleing@13062
   107
kleing@13062
   108
  assume 
nipkow@13074
   109
    "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
wenzelm@23464
   110
  hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" using ls .
kleing@13062
   111
kleing@13062
   112
  assume "x \<in> set (s#ls)"
kleing@13062
   113
  then obtain xls: "x = s \<or> x \<in> set ls" by simp
kleing@13062
   114
  moreover {
kleing@13062
   115
    assume xs: "x = s"
kleing@13077
   116
    from s y have "s <=_r s +_f y" ..
kleing@13077
   117
    also from s y have "s +_f y \<in> A" ..
nipkow@13074
   118
    with ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule pp_ub2)
nipkow@13074
   119
    finally have "s <=_r ls ++_f (s +_f y)" .
kleing@13062
   120
    with xs have "x <=_r ls ++_f (s +_f y)" by simp
kleing@13062
   121
  } 
kleing@13062
   122
  moreover {
kleing@13062
   123
    assume "x \<in> set ls"
kleing@13062
   124
    hence "\<And>y. y \<in> A \<Longrightarrow> x <=_r ls ++_f y" by (rule IH)
kleing@13077
   125
    moreover from s y have "s +_f y \<in> A" ..
nipkow@13074
   126
    ultimately have "x <=_r ls ++_f (s +_f y)" .
kleing@13062
   127
  }
kleing@13062
   128
  ultimately 
kleing@13062
   129
  have "x <=_r ls ++_f (s +_f y)" by blast
kleing@13062
   130
  thus "x <=_r (s#ls) ++_f y" by simp
kleing@13062
   131
qed
kleing@13062
   132
kleing@13062
   133
nipkow@13074
   134
lemma (in semilat) pp_lub:
wenzelm@23464
   135
  assumes z: "z \<in> A"
kleing@13069
   136
  shows 
kleing@13069
   137
  "\<And>y. y \<in> A \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> \<forall>x \<in> set xs. x <=_r z \<Longrightarrow> y <=_r z \<Longrightarrow> xs ++_f y <=_r z"
kleing@13069
   138
proof (induct xs)
kleing@13069
   139
  fix y assume "y <=_r z" thus "[] ++_f y <=_r z" by simp
kleing@13069
   140
next
kleing@13069
   141
  fix y l ls assume y: "y \<in> A" and "set (l#ls) \<subseteq> A"
kleing@13069
   142
  then obtain l: "l \<in> A" and ls: "set ls \<subseteq> A" by auto
kleing@13069
   143
  assume "\<forall>x \<in> set (l#ls). x <=_r z"
wenzelm@23464
   144
  then obtain lz: "l <=_r z" and lsz: "\<forall>x \<in> set ls. x <=_r z" by auto
wenzelm@23464
   145
  assume "y <=_r z" with lz have "l +_f y <=_r z" using l y z ..
kleing@13069
   146
  moreover
kleing@13077
   147
  from l y have "l +_f y \<in> A" ..
kleing@13069
   148
  moreover
kleing@13069
   149
  assume "\<And>y. y \<in> A \<Longrightarrow> set ls \<subseteq> A \<Longrightarrow> \<forall>x \<in> set ls. x <=_r z \<Longrightarrow> y <=_r z
kleing@13069
   150
          \<Longrightarrow> ls ++_f y <=_r z"
kleing@13069
   151
  ultimately
kleing@13077
   152
  have "ls ++_f (l +_f y) <=_r z" using ls lsz by -
kleing@13069
   153
  thus "(l#ls) ++_f y <=_r z" by simp
kleing@13069
   154
qed
kleing@13069
   155
kleing@13069
   156
nipkow@13074
   157
lemma ub1': includes semilat
nipkow@13074
   158
shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
nipkow@23281
   159
  \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" 
kleing@13062
   160
proof -
kleing@13062
   161
  let "b <=_r ?map ++_f y" = ?thesis
kleing@13062
   162
nipkow@13074
   163
  assume "y \<in> A"
kleing@13062
   164
  moreover
kleing@13062
   165
  assume "\<forall>(p,s) \<in> set S. s \<in> A"
kleing@13062
   166
  hence "set ?map \<subseteq> A" by auto
kleing@13062
   167
  moreover
kleing@13062
   168
  assume "(a,b) \<in> set S"
kleing@13062
   169
  hence "b \<in> set ?map" by (induct S, auto)
kleing@13062
   170
  ultimately
nipkow@13074
   171
  show ?thesis by - (rule pp_ub1)
kleing@13062
   172
qed
kleing@13062
   173
    
kleing@13062
   174
kleing@13062
   175
lemma plusplus_empty:  
kleing@13062
   176
  "\<forall>s'. (q, s') \<in> set S \<longrightarrow> s' +_f ss ! q = ss ! q \<Longrightarrow>
nipkow@23281
   177
   (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"
wenzelm@23464
   178
  by (induct S) auto 
kleing@13062
   179
kleing@13062
   180
end