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