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