src/HOL/MicroJava/BV/LBVCorrect.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 (*
     2     ID:         $Id$
     3     Author:     Gerwin Klein
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* \isaheader{Correctness of the LBV} *}
     8 
     9 theory LBVCorrect = LBVSpec + Typing_Framework:
    10 
    11 locale (open) lbvs = lbv +
    12   fixes s0  :: 'a ("s\<^sub>0")
    13   fixes c   :: "'a list"
    14   fixes ins :: "'b list"
    15   fixes phi :: "'a list" ("\<phi>")
    16   defines phi_def:
    17   "\<phi> \<equiv> map (\<lambda>pc. if c!pc = \<bottom> then wtl (take pc ins) c 0 s0 else c!pc) 
    18        [0..<length ins]"
    19 
    20   assumes bounded: "bounded step (length ins)"
    21   assumes cert: "cert_ok c (length ins) \<top> \<bottom> A"
    22   assumes pres: "pres_type step (length ins) A"
    23 
    24 
    25 lemma (in lbvs) phi_None [intro?]:
    26   "\<lbrakk> pc < length ins; c!pc = \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = wtl (take pc ins) c 0 s0"
    27   by (simp add: phi_def)
    28 
    29 lemma (in lbvs) phi_Some [intro?]:
    30   "\<lbrakk> pc < length ins; c!pc \<noteq> \<bottom> \<rbrakk> \<Longrightarrow> \<phi> ! pc = c ! pc"
    31   by (simp add: phi_def)
    32 
    33 lemma (in lbvs) phi_len [simp]:
    34   "length \<phi> = length ins"
    35   by (simp add: phi_def)
    36 
    37 
    38 lemma (in lbvs) wtl_suc_pc:
    39   assumes all: "wtl ins c 0 s\<^sub>0 \<noteq> \<top>" 
    40   assumes pc:  "pc+1 < length ins"
    41   shows "wtl (take (pc+1) ins) c 0 s0 \<le>\<^sub>r \<phi>!(pc+1)"
    42 proof -
    43   from all pc
    44   have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all)
    45   with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)
    46 qed
    47 
    48 
    49 lemma (in lbvs) wtl_stable:
    50   assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>" 
    51   assumes s0:  "s0 \<in> A" 
    52   assumes pc:  "pc < length ins" 
    53   shows "stable r step \<phi> pc"
    54 proof (unfold stable_def, clarify)
    55   fix pc' s' assume step: "(pc',s') \<in> set (step pc (\<phi> ! pc))" 
    56                       (is "(pc',s') \<in> set (?step pc)")
    57   
    58   from bounded pc step have pc': "pc' < length ins" by (rule boundedD)
    59 
    60   have tkpc: "wtl (take pc ins) c 0 s0 \<noteq> \<top>" (is "?s1 \<noteq> _") by (rule wtl_take)
    61   have s2: "wtl (take (pc+1) ins) c 0 s0 \<noteq> \<top>" (is "?s2 \<noteq> _") by (rule wtl_take)
    62   
    63   from wtl pc have wt_s1: "wtc c pc ?s1 \<noteq> \<top>" by (rule wtl_all)
    64 
    65   have c_Some: "\<forall>pc t. pc < length ins \<longrightarrow> c!pc \<noteq> \<bottom> \<longrightarrow> \<phi>!pc = c!pc" 
    66     by (simp add: phi_def)
    67   have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..
    68 
    69   from wt_s1 pc c_None c_Some
    70   have inst: "wtc c pc ?s1  = wti c pc (\<phi>!pc)"
    71     by (simp add: wtc split: split_if_asm)
    72 
    73   have "?s1 \<in> A" by (rule wtl_pres) 
    74   with pc c_Some cert c_None
    75   have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)
    76   with pc pres
    77   have step_in_A: "snd`set (?step pc) \<subseteq> A" by (auto dest: pres_typeD2)
    78 
    79   show "s' <=_r \<phi>!pc'" 
    80   proof (cases "pc' = pc+1")
    81     case True
    82     with pc' cert
    83     have cert_in_A: "c!(pc+1) \<in> A" by (auto dest: cert_okD1)
    84     from True pc' have pc1: "pc+1 < length ins" by simp
    85     with tkpc have "?s2 = wtc c pc ?s1" by - (rule wtl_Suc)
    86     with inst 
    87     have merge: "?s2 = merge c pc (?step pc) (c!(pc+1))" by (simp add: wti)
    88     also    
    89     from s2 merge have "\<dots> \<noteq> \<top>" (is "?merge \<noteq> _") by simp
    90     with cert_in_A step_in_A
    91     have "?merge = (map snd [(p',t')\<in>?step pc. p'=pc+1] ++_f (c!(pc+1)))"
    92       by (rule merge_not_top_s) 
    93     finally
    94     have "s' <=_r ?s2" using step_in_A cert_in_A True step 
    95       by (auto intro: pp_ub1')
    96     also 
    97     from wtl pc1 have "?s2 <=_r \<phi>!(pc+1)" by (rule wtl_suc_pc)
    98     also note True [symmetric]
    99     finally show ?thesis by simp    
   100   next
   101     case False
   102     from wt_s1 inst
   103     have "merge c pc (?step pc) (c!(pc+1)) \<noteq> \<top>" by (simp add: wti)
   104     with step_in_A
   105     have "\<forall>(pc', s')\<in>set (?step pc). pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'" 
   106       by - (rule merge_not_top)
   107     with step False 
   108     have ok: "s' <=_r c!pc'" by blast
   109     moreover
   110     from ok
   111     have "c!pc' = \<bottom> \<Longrightarrow> s' = \<bottom>" by simp
   112     moreover
   113     from c_Some pc'
   114     have "c!pc' \<noteq> \<bottom> \<Longrightarrow> \<phi>!pc' = c!pc'" by auto
   115     ultimately
   116     show ?thesis by (cases "c!pc' = \<bottom>") auto 
   117   qed
   118 qed
   119 
   120   
   121 lemma (in lbvs) phi_not_top:
   122   assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
   123   assumes pc:  "pc < length ins"
   124   shows "\<phi>!pc \<noteq> \<top>"
   125 proof (cases "c!pc = \<bottom>")
   126   case False with pc
   127   have "\<phi>!pc = c!pc" ..
   128   also from cert pc have "\<dots> \<noteq> \<top>" by (rule cert_okD4)
   129   finally show ?thesis .
   130 next
   131   case True with pc
   132   have "\<phi>!pc = wtl (take pc ins) c 0 s0" ..
   133   also from wtl have "\<dots> \<noteq> \<top>" by (rule wtl_take)
   134   finally show ?thesis .
   135 qed
   136 
   137 lemma (in lbvs) phi_in_A:
   138   assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
   139   assumes s0:  "s0 \<in> A"
   140   shows "\<phi> \<in> list (length ins) A"
   141 proof -
   142   { fix x assume "x \<in> set \<phi>"
   143     then obtain xs ys where "\<phi> = xs @ x # ys" 
   144       by (auto simp add: in_set_conv_decomp)
   145     then obtain pc where pc: "pc < length \<phi>" and x: "\<phi>!pc = x"
   146       by (simp add: that [of "length xs"] nth_append)
   147     
   148     from wtl s0 pc 
   149     have "wtl (take pc ins) c 0 s0 \<in> A" by (auto intro!: wtl_pres)
   150     moreover
   151     from pc have "pc < length ins" by simp
   152     with cert have "c!pc \<in> A" ..
   153     ultimately
   154     have "\<phi>!pc \<in> A" using pc by (simp add: phi_def)
   155     hence "x \<in> A" using x by simp
   156   } 
   157   hence "set \<phi> \<subseteq> A" ..
   158   thus ?thesis by (unfold list_def) simp
   159 qed
   160 
   161 
   162 lemma (in lbvs) phi0:
   163   assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>"
   164   assumes 0:   "0 < length ins"
   165   shows "s0 <=_r \<phi>!0"
   166 proof (cases "c!0 = \<bottom>")
   167   case True
   168   with 0 have "\<phi>!0 = wtl (take 0 ins) c 0 s0" ..
   169   moreover have "wtl (take 0 ins) c 0 s0 = s0" by simp
   170   ultimately have "\<phi>!0 = s0" by simp
   171   thus ?thesis by simp
   172 next
   173   case False
   174   with 0 have "phi!0 = c!0" ..
   175   moreover 
   176   have "wtl (take 1 ins) c 0 s0 \<noteq> \<top>"  by (rule wtl_take)
   177   with 0 False 
   178   have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)
   179   ultimately
   180   show ?thesis by simp
   181 qed
   182 
   183 
   184 theorem (in lbvs) wtl_sound:
   185   assumes "wtl ins c 0 s0 \<noteq> \<top>" 
   186   assumes "s0 \<in> A" 
   187   shows "\<exists>ts. wt_step r \<top> step ts"
   188 proof -
   189   have "wt_step r \<top> step \<phi>"
   190   proof (unfold wt_step_def, intro strip conjI)
   191     fix pc assume "pc < length \<phi>"
   192     then obtain "pc < length ins" by simp
   193     show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
   194     show "stable r step \<phi> pc" by (rule wtl_stable)
   195   qed
   196   thus ?thesis ..
   197 qed
   198 
   199 
   200 theorem (in lbvs) wtl_sound_strong:
   201   assumes "wtl ins c 0 s0 \<noteq> \<top>" 
   202   assumes "s0 \<in> A" 
   203   assumes "0 < length ins"
   204   shows "\<exists>ts \<in> list (length ins) A. wt_step r \<top> step ts \<and> s0 <=_r ts!0"
   205 proof -
   206   have "\<phi> \<in> list (length ins) A" by (rule phi_in_A)
   207   moreover
   208   have "wt_step r \<top> step \<phi>"
   209   proof (unfold wt_step_def, intro strip conjI)
   210     fix pc assume "pc < length \<phi>"
   211     then obtain "pc < length ins" by simp
   212     show "\<phi>!pc \<noteq> \<top>" by (rule phi_not_top)
   213     show "stable r step \<phi> pc" by (rule wtl_stable)
   214   qed
   215   moreover
   216   have "s0 <=_r \<phi>!0" by (rule phi0)
   217   ultimately
   218   show ?thesis by fast
   219 qed
   220 
   221 end