src/HOL/MicroJava/BV/LBVComplete.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23467 d1b97708d5eb
child 27681 8cedebf55539
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/BV/LBVComplete.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein
     4     Copyright   2000 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* \isaheader{Completeness of the LBV} *}
     8 
     9 theory LBVComplete
    10 imports LBVSpec Typing_Framework
    11 begin
    12 
    13 constdefs
    14   is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" 
    15   "is_target step phi pc' \<equiv>
    16      \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
    17 
    18   make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate"
    19   "make_cert step phi B \<equiv> 
    20      map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
    21 
    22 lemma [code]:
    23   "is_target step phi pc' =
    24   list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
    25 by (force simp: list_ex_iff is_target_def mem_iff)
    26 
    27 
    28 locale (open) lbvc = lbv + 
    29   fixes phi :: "'a list" ("\<phi>")
    30   fixes c   :: "'a list" 
    31   defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>"
    32 
    33   assumes mono: "mono r step (length \<phi>) A"
    34   assumes pres: "pres_type step (length \<phi>) A" 
    35   assumes phi:  "\<forall>pc < length \<phi>. \<phi>!pc \<in> A \<and> \<phi>!pc \<noteq> \<top>"
    36   assumes bounded: "bounded step (length \<phi>)"
    37 
    38   assumes B_neq_T: "\<bottom> \<noteq> \<top>" 
    39 
    40 
    41 lemma (in lbvc) cert: "cert_ok c (length \<phi>) \<top> \<bottom> A"
    42 proof (unfold cert_ok_def, intro strip conjI)  
    43   note [simp] = make_cert_def cert_def nth_append 
    44 
    45   show "c!length \<phi> = \<bottom>" by simp
    46 
    47   fix pc assume pc: "pc < length \<phi>" 
    48   from pc phi B_A show "c!pc \<in> A" by simp
    49   from pc phi B_neq_T show "c!pc \<noteq> \<top>" by simp
    50 qed
    51 
    52 lemmas [simp del] = split_paired_Ex
    53 
    54 
    55 lemma (in lbvc) cert_target [intro?]:
    56   "\<lbrakk> (pc',s') \<in> set (step pc (\<phi>!pc));
    57       pc' \<noteq> pc+1; pc < length \<phi>; pc' < length \<phi> \<rbrakk>
    58   \<Longrightarrow> c!pc' = \<phi>!pc'"
    59   by (auto simp add: cert_def make_cert_def nth_append is_target_def)
    60 
    61 
    62 lemma (in lbvc) cert_approx [intro?]:
    63   "\<lbrakk> pc < length \<phi>; c!pc \<noteq> \<bottom> \<rbrakk>
    64   \<Longrightarrow> c!pc = \<phi>!pc"
    65   by (auto simp add: cert_def make_cert_def nth_append)
    66 
    67 
    68 lemma (in lbv) le_top [simp, intro]:
    69   "x <=_r \<top>"
    70   by (insert top) simp
    71   
    72 
    73 lemma (in lbv) merge_mono:
    74   assumes less:  "ss2 <=|r| ss1"
    75   assumes x:     "x \<in> A"
    76   assumes ss1:   "snd`set ss1 \<subseteq> A"
    77   assumes ss2:   "snd`set ss2 \<subseteq> A"
    78   shows "merge c pc ss2 x <=_r merge c pc ss1 x" (is "?s2 <=_r ?s1")
    79 proof-
    80   have "?s1 = \<top> \<Longrightarrow> ?thesis" by simp
    81   moreover {
    82     assume merge: "?s1 \<noteq> T" 
    83     from x ss1 have "?s1 =
    84       (if \<forall>(pc', s')\<in>set ss1. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
    85       then (map snd [(p', t') \<leftarrow> ss1 . p'=pc+1]) ++_f x
    86       else \<top>)" 
    87       by (rule merge_def)  
    88     with merge obtain
    89       app: "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' <=_r c!pc'" 
    90            (is "?app ss1") and
    91       sum: "(map snd [(p',t') \<leftarrow> ss1 . p' = pc+1] ++_f x) = ?s1" 
    92            (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
    93       by (simp split: split_if_asm)
    94     from app less 
    95     have "?app ss2" by (blast dest: trans_r lesub_step_typeD)
    96     moreover {
    97       from ss1 have map1: "set (?map ss1) \<subseteq> A" by auto
    98       with x have "?sum ss1 \<in> A" by (auto intro!: plusplus_closed semilat)
    99       with sum have "?s1 \<in> A" by simp
   100       moreover    
   101       have mapD: "\<And>x ss. x \<in> set (?map ss) \<Longrightarrow> \<exists>p. (p,x) \<in> set ss \<and> p=pc+1" by auto
   102       from x map1 
   103       have "\<forall>x \<in> set (?map ss1). x <=_r ?sum ss1"
   104         by clarify (rule pp_ub1)
   105       with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp
   106       with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1"
   107         by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r)
   108       moreover 
   109       from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2)
   110       with sum have "x <=_r ?s1" by simp
   111       moreover 
   112       from ss2 have "set (?map ss2) \<subseteq> A" by auto
   113       ultimately
   114       have "?sum ss2 <=_r ?s1" using x by - (rule pp_lub)
   115     }
   116     moreover
   117     from x ss2 have 
   118       "?s2 =
   119       (if \<forall>(pc', s')\<in>set ss2. pc' \<noteq> pc + 1 \<longrightarrow> s' <=_r c!pc'
   120       then map snd [(p', t') \<leftarrow> ss2 . p' = pc + 1] ++_f x
   121       else \<top>)" 
   122       by (rule merge_def)
   123     ultimately have ?thesis by simp
   124   }
   125   ultimately show ?thesis by (cases "?s1 = \<top>") auto
   126 qed
   127 
   128 
   129 lemma (in lbvc) wti_mono:
   130   assumes less: "s2 <=_r s1"
   131   assumes pc:   "pc < length \<phi>" 
   132   assumes s1:   "s1 \<in> A"
   133   assumes s2:   "s2 \<in> A"
   134   shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'")
   135 proof -
   136   from mono pc s2 less have "step pc s2 <=|r| step pc s1" by (rule monoD)
   137   moreover
   138   from cert B_A pc have "c!Suc pc \<in> A" by (rule cert_okD3)
   139   moreover 
   140   from pres s1 pc
   141   have "snd`set (step pc s1) \<subseteq> A" by (rule pres_typeD2)
   142   moreover
   143   from pres s2 pc
   144   have "snd`set (step pc s2) \<subseteq> A" by (rule pres_typeD2)
   145   ultimately
   146   show ?thesis by (simp add: wti merge_mono)
   147 qed 
   148 
   149 lemma (in lbvc) wtc_mono:
   150   assumes less: "s2 <=_r s1"
   151   assumes pc:   "pc < length \<phi>" 
   152   assumes s1:   "s1 \<in> A"
   153   assumes s2:   "s2 \<in> A"
   154   shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'")
   155 proof (cases "c!pc = \<bottom>")
   156   case True 
   157   moreover from less pc s1 s2 have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono)
   158   ultimately show ?thesis by (simp add: wtc)
   159 next
   160   case False
   161   have "?s1' = \<top> \<Longrightarrow> ?thesis" by simp
   162   moreover {
   163     assume "?s1' \<noteq> \<top>" 
   164     with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm)
   165     with less have "s2 <=_r c!pc" ..
   166     with False c have ?thesis by (simp add: wtc)
   167   }
   168   ultimately show ?thesis by (cases "?s1' = \<top>") auto
   169 qed
   170 
   171 
   172 lemma (in lbv) top_le_conv [simp]:
   173   "\<top> <=_r x = (x = \<top>)"
   174   by (insert semilat) (simp add: top top_le_conv) 
   175 
   176 lemma (in lbv) neq_top [simp, elim]:
   177   "\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>"
   178   by (cases "x = T") auto
   179 
   180 
   181 lemma (in lbvc) stable_wti:
   182   assumes stable:  "stable r step \<phi> pc"
   183   assumes pc:      "pc < length \<phi>"
   184   shows "wti c pc (\<phi>!pc) \<noteq> \<top>"
   185 proof -
   186   let ?step = "step pc (\<phi>!pc)"
   187   from stable 
   188   have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)
   189   
   190   from cert B_A pc 
   191   have cert_suc: "c!Suc pc \<in> A" by (rule cert_okD3)
   192   moreover  
   193   from phi pc have "\<phi>!pc \<in> A" by simp
   194   from pres this pc 
   195   have stepA: "snd`set ?step \<subseteq> A" by (rule pres_typeD2) 
   196   ultimately
   197   have "merge c pc ?step (c!Suc pc) =
   198     (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
   199     then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
   200     else \<top>)" by (rule merge_def)
   201   moreover {
   202     fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
   203     with less have "s' <=_r \<phi>!pc'" by auto
   204     also 
   205     from bounded pc s' have "pc' < length \<phi>" by (rule boundedD)
   206     with s' suc_pc pc have "c!pc' = \<phi>!pc'" ..
   207     hence "\<phi>!pc' = c!pc'" ..
   208     finally have "s' <=_r c!pc'" .
   209   } hence "\<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" by auto
   210   moreover
   211   from pc have "Suc pc = length \<phi> \<or> Suc pc < length \<phi>" by auto
   212   hence "map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc \<noteq> \<top>" 
   213          (is "?map ++_f _ \<noteq> _")
   214   proof (rule disjE)
   215     assume pc': "Suc pc = length \<phi>"
   216     with cert have "c!Suc pc = \<bottom>" by (simp add: cert_okD2)
   217     moreover 
   218     from pc' bounded pc 
   219     have "\<forall>(p',t')\<in>set ?step. p'\<noteq>pc+1" by clarify (drule boundedD, auto)
   220     hence "[(p',t') \<leftarrow> ?step.p'=pc+1] = []" by (blast intro: filter_False) 
   221     hence "?map = []" by simp
   222     ultimately show ?thesis by (simp add: B_neq_T)  
   223   next
   224     assume pc': "Suc pc < length \<phi>"
   225     from pc' phi have "\<phi>!Suc pc \<in> A" by simp
   226     moreover note cert_suc
   227     moreover from stepA 
   228     have "set ?map \<subseteq> A" by auto
   229     moreover
   230     have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto
   231     with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto
   232     moreover
   233     from pc' have "c!Suc pc <=_r \<phi>!Suc pc" 
   234       by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx)
   235     ultimately
   236     have "?map ++_f c!Suc pc <=_r \<phi>!Suc pc" by (rule pp_lub)
   237     moreover
   238     from pc' phi have "\<phi>!Suc pc \<noteq> \<top>" by simp
   239     ultimately
   240     show ?thesis by auto
   241   qed
   242   ultimately
   243   have "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by simp
   244   thus ?thesis by (simp add: wti)  
   245 qed
   246 
   247 lemma (in lbvc) wti_less:
   248   assumes stable:  "stable r step \<phi> pc"
   249   assumes suc_pc:   "Suc pc < length \<phi>"
   250   shows "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wti <=_r _")
   251 proof -
   252   let ?step = "step pc (\<phi>!pc)"
   253 
   254   from stable 
   255   have less: "\<forall>(q,s')\<in>set ?step. s' <=_r \<phi>!q" by (simp add: stable_def)
   256    
   257   from suc_pc have pc: "pc < length \<phi>" by simp
   258   with cert B_A have cert_suc: "c!Suc pc \<in> A" by (rule cert_okD3)
   259   moreover  
   260   from phi pc have "\<phi>!pc \<in> A" by simp
   261   with pres pc have stepA: "snd`set ?step \<subseteq> A" by - (rule pres_typeD2)
   262   moreover
   263   from stable pc have "?wti \<noteq> \<top>" by (rule stable_wti)
   264   hence "merge c pc ?step (c!Suc pc) \<noteq> \<top>" by (simp add: wti)
   265   ultimately
   266   have "merge c pc ?step (c!Suc pc) =
   267     map snd [(p',t')\<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s) 
   268   hence "?wti = \<dots>" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
   269   also {
   270     from suc_pc phi have "\<phi>!Suc pc \<in> A" by simp
   271     moreover note cert_suc
   272     moreover from stepA have "set ?map \<subseteq> A" by auto
   273     moreover
   274     have "\<And>s. s \<in> set ?map \<Longrightarrow> \<exists>t. (Suc pc, t) \<in> set ?step" by auto
   275     with less have "\<forall>s' \<in> set ?map. s' <=_r \<phi>!Suc pc" by auto
   276     moreover
   277     from suc_pc have "c!Suc pc <=_r \<phi>!Suc pc"
   278       by (cases "c!Suc pc = \<bottom>") (auto dest: cert_approx)
   279     ultimately
   280     have "?sum <=_r \<phi>!Suc pc" by (rule pp_lub)
   281   }
   282   finally show ?thesis .
   283 qed
   284 
   285 lemma (in lbvc) stable_wtc:
   286   assumes stable:  "stable r step phi pc"
   287   assumes pc:      "pc < length \<phi>"
   288   shows "wtc c pc (\<phi>!pc) \<noteq> \<top>"
   289 proof -
   290   from stable pc have wti: "wti c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wti)
   291   show ?thesis
   292   proof (cases "c!pc = \<bottom>")
   293     case True with wti show ?thesis by (simp add: wtc)
   294   next
   295     case False
   296     with pc have "c!pc = \<phi>!pc" ..    
   297     with False wti show ?thesis by (simp add: wtc)
   298   qed
   299 qed
   300 
   301 lemma (in lbvc) wtc_less:
   302   assumes stable: "stable r step \<phi> pc"
   303   assumes suc_pc: "Suc pc < length \<phi>"
   304   shows "wtc c pc (\<phi>!pc) <=_r \<phi>!Suc pc" (is "?wtc <=_r _")
   305 proof (cases "c!pc = \<bottom>")
   306   case True
   307   moreover from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc"
   308     by (rule wti_less)
   309   ultimately show ?thesis by (simp add: wtc)
   310 next
   311   case False
   312   from suc_pc have pc: "pc < length \<phi>" by simp
   313   with stable have "?wtc \<noteq> \<top>" by (rule stable_wtc)
   314   with False have "?wtc = wti c pc (c!pc)" 
   315     by (unfold wtc) (simp split: split_if_asm)
   316   also from pc False have "c!pc = \<phi>!pc" .. 
   317   finally have "?wtc = wti c pc (\<phi>!pc)" .
   318   also from stable suc_pc have "wti c pc (\<phi>!pc) <=_r \<phi>!Suc pc" by (rule wti_less)
   319   finally show ?thesis .
   320 qed
   321 
   322 
   323 lemma (in lbvc) wt_step_wtl_lemma:
   324   assumes wt_step: "wt_step r \<top> step \<phi>"
   325   shows "\<And>pc s. pc+length ls = length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow>
   326                 wtl ls c pc s \<noteq> \<top>"
   327   (is "\<And>pc s. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?wtl ls pc s \<noteq> _")
   328 proof (induct ls)
   329   fix pc s assume "s\<noteq>\<top>" thus "?wtl [] pc s \<noteq> \<top>" by simp
   330 next
   331   fix pc s i ls
   332   assume "\<And>pc s. pc+length ls=length \<phi> \<Longrightarrow> s <=_r \<phi>!pc \<Longrightarrow> s \<in> A \<Longrightarrow> s\<noteq>\<top> \<Longrightarrow> 
   333                   ?wtl ls pc s \<noteq> \<top>"
   334   moreover
   335   assume pc_l: "pc + length (i#ls) = length \<phi>"
   336   hence suc_pc_l: "Suc pc + length ls = length \<phi>" by simp
   337   ultimately
   338   have IH: "\<And>s. s <=_r \<phi>!Suc pc \<Longrightarrow> s \<in> A \<Longrightarrow> s \<noteq> \<top> \<Longrightarrow> ?wtl ls (Suc pc) s \<noteq> \<top>" .
   339 
   340   from pc_l obtain pc: "pc < length \<phi>" by simp
   341   with wt_step have stable: "stable r step \<phi> pc" by (simp add: wt_step_def)
   342   from this pc have wt_phi: "wtc c pc (\<phi>!pc) \<noteq> \<top>" by (rule stable_wtc)
   343   assume s_phi: "s <=_r \<phi>!pc"
   344   from phi pc have phi_pc: "\<phi>!pc \<in> A" by simp
   345   assume s: "s \<in> A"
   346   with s_phi pc phi_pc have wt_s_phi: "wtc c pc s <=_r wtc c pc (\<phi>!pc)" by (rule wtc_mono)
   347   with wt_phi have wt_s: "wtc c pc s \<noteq> \<top>" by simp
   348   moreover
   349   assume s': "s \<noteq> \<top>" 
   350   ultimately
   351   have "ls = [] \<Longrightarrow> ?wtl (i#ls) pc s \<noteq> \<top>" by simp
   352   moreover {
   353     assume "ls \<noteq> []" 
   354     with pc_l have suc_pc: "Suc pc < length \<phi>" by (auto simp add: neq_Nil_conv)
   355     with stable have "wtc c pc (phi!pc) <=_r \<phi>!Suc pc" by (rule wtc_less)
   356     with wt_s_phi have "wtc c pc s <=_r \<phi>!Suc pc" by (rule trans_r)      
   357     moreover
   358     from cert suc_pc have "c!pc \<in> A" "c!(pc+1) \<in> A" 
   359       by (auto simp add: cert_ok_def)
   360     from pres this s pc have "wtc c pc s \<in> A" by (rule wtc_pres)
   361     ultimately
   362     have "?wtl ls (Suc pc) (wtc c pc s) \<noteq> \<top>" using IH wt_s by blast
   363     with s' wt_s have "?wtl (i#ls) pc s \<noteq> \<top>" by simp
   364   }
   365   ultimately show "?wtl (i#ls) pc s \<noteq> \<top>" by (cases ls) blast+
   366 qed
   367 
   368   
   369 theorem (in lbvc) wtl_complete:
   370   assumes wt: "wt_step r \<top> step \<phi>"
   371     and s: "s <=_r \<phi>!0" "s \<in> A" "s \<noteq> \<top>"
   372     and len: "length ins = length phi"
   373   shows "wtl ins c 0 s \<noteq> \<top>"
   374 proof -
   375   from len have "0+length ins = length phi" by simp
   376   from wt this s show ?thesis by (rule wt_step_wtl_lemma)
   377 qed
   378 
   379 end