# HG changeset patch # User kleing # Date 976021736 -3600 # Node ID fc0b575a2cf7ebac949a3986e5cb0c07c36ce928 # Parent 6d6cb845e841e9f07a629e3369bee8ab359747d3 BCV Integration diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Tue Dec 05 14:08:56 2000 +0100 @@ -10,9 +10,9 @@ theory BVSpec = Step: constdefs -wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool" -"wt_instr i G rT phi max_pc pc == - app i G rT (phi!pc) \ +wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool" +"wt_instr i G rT phi mxs max_pc pc == + app i G mxs rT (phi!pc) \ (\ pc' \ set (succs i pc). pc' < max_pc \ (G \ step i G (phi!pc) <=' phi!pc'))" wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" @@ -20,17 +20,17 @@ G \ Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" -wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool" -"wt_method G C pTs rT mxl ins phi == +wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool" +"wt_method G C pTs rT mxs mxl ins phi == let max_pc = length ins in 0 < max_pc \ wt_start G C pTs mxl phi \ - (\pc. pc wt_instr (ins ! pc) G rT phi max_pc pc)" + (\pc. pc wt_instr (ins ! pc) G rT phi mxs max_pc pc)" wt_jvm_prog :: "[jvm_prog,prog_type] => bool" "wt_jvm_prog G phi == - wf_prog (\G C (sig,rT,maxl,b). - wt_method G C (snd sig) rT maxl b (phi C sig)) G" + wf_prog (\G C (sig,rT,(maxs,maxl,b)). + wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G" @@ -39,21 +39,21 @@ by (unfold wt_jvm_prog_def, blast) lemma wt_jvm_prog_impl_wt_instr: -"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins |] - ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; +"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] + ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"; by (unfold wt_jvm_prog_def, drule method_wf_mdecl, simp, simp add: wf_mdecl_def wt_method_def) lemma wt_jvm_prog_impl_wt_start: -"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) |] ==> +"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 0 < (length ins) \ wt_start G C (snd sig) maxl (phi C sig)" by (unfold wt_jvm_prog_def, drule method_wf_mdecl, simp, simp add: wf_mdecl_def wt_method_def) -(* for most instructions wt_instr collapses: *) +text "for most instructions wt_instr collapses:" lemma -"succs i pc = [pc+1] ==> wt_instr i G rT phi max_pc pc = - (app i G rT (phi!pc) \ pc+1 < max_pc \ (G \ step i G (phi!pc) <=' phi!(pc+1)))" +"succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = + (app i G mxs rT (phi!pc) \ pc+1 < max_pc \ (G \ step i G (phi!pc) <=' phi!(pc+1)))" by (simp add: wt_instr_def) end diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Dec 05 14:08:56 2000 +0100 @@ -17,9 +17,9 @@ lemmas [simp del] = split_paired_All lemma wt_jvm_prog_impl_wt_instr_cor: - "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); + "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] - ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc" + ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" apply (unfold correct_state_def Let_def correct_frame_def) apply simp apply (blast intro: wt_jvm_prog_impl_wt_instr) @@ -27,9 +27,9 @@ lemma Load_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = Load idx; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -43,9 +43,9 @@ lemma Store_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = Store idx; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -64,9 +64,9 @@ lemma Bipush_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = Bipush i; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -92,9 +92,9 @@ lemma Aconst_null_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = Aconst_null; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -122,9 +122,9 @@ lemma Checkcast_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = Checkcast D; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -136,9 +136,9 @@ lemma Getfield_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = Getfield F D; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -158,9 +158,9 @@ lemma Putfield_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = Putfield F D; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -188,9 +188,9 @@ lemma New_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = New cl_idx; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -216,17 +216,17 @@ lemma Invoke_correct: "[| wt_jvm_prog G phi; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Invoke C' mn pTs; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" proof - assume wtprog: "wt_jvm_prog G phi" - assume method: "method (G,C) sig = Some (C,rT,maxl,ins)" + assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" assume ins: "ins ! pc = Invoke C' mn pTs" - assume wti: "wt_instr (ins!pc) G rT (phi C sig) (length ins) pc" + assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" assume approx: "G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\" @@ -278,7 +278,7 @@ a_stk': "approx_stk G hp stk' ST" and stk': "stk = opTs @ oX # stk'" and l_o: "length opTs = length apTs" - "length stk' = length ST" + "length stk' = length ST" by - (drule approx_stk_append_lemma, simp, elim, simp) from oX @@ -328,8 +328,8 @@ by simp with mC' wfprog - obtain D0 rT0 maxl0 ins0 where - mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxl0, ins0)" "G\rT0\rT" + obtain D0 rT0 maxs0 maxl0 ins0 where + mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\rT0\rT" by (auto dest: subtype_widen_methd intro: that) from X' D @@ -337,8 +337,8 @@ by simp with wfprog mX - obtain D'' rT' mxl' ins' where - mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxl', ins')" + obtain D'' rT' mxs' mxl' ins' where + mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" "G \ rT' \ rT0" by (auto dest: subtype_widen_methd intro: that) @@ -348,7 +348,7 @@ from mD wfprog obtain mD'': - "method (G, D'') (mn, pTs) = Some (D'', rT', mxl', ins')" + "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" "is_class G D''" by (auto dest: method_in_md) @@ -452,9 +452,9 @@ lemma Return_correct: "[| wt_jvm_prog G phi; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Return; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -473,9 +473,9 @@ lemma Goto_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Goto branch; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -487,9 +487,9 @@ lemma Ifcmpeq_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Ifcmpeq branch; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -500,9 +500,9 @@ lemma Pop_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Pop; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -513,9 +513,9 @@ lemma Dup_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Dup; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -528,9 +528,9 @@ lemma Dup_x1_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Dup_x1; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -543,9 +543,9 @@ lemma Dup_x2_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Dup_x2; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -558,9 +558,9 @@ lemma Swap_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = Swap; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -573,9 +573,9 @@ lemma IAdd_correct: "[| wf_prog wt G; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins ! pc = IAdd; - wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; + wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" @@ -590,7 +590,7 @@ lemma instr_correct: "[| wt_jvm_prog G phi; - method (G,C) sig = Some (C,rT,maxl,ins); + method (G,C) sig = Some (C,rT,maxs,maxl,ins); Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ |] ==> G,phi \JVM state'\" diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Tue Dec 05 14:08:56 2000 +0100 @@ -38,16 +38,16 @@ "correct_frames G hp phi rT0 sig0 (f#frs) = (let (stk,loc,C,sig,pc) = f in - (\ST LT rT maxl ins. + (\ST LT rT maxs maxl ins. phi C sig ! pc = Some (ST,LT) \ - method (G,C) sig = Some(C,rT,(maxl,ins)) \ + method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \ (\C' mn pTs k. pc = k+1 \ ins!k = (Invoke C' mn pTs) \ (mn,pTs) = sig0 \ (\apTs D ST' LT'. (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \ length apTs = length pTs \ - (\D' rT' maxl' ins'. - method (G,D) sig0 = Some(D',rT',(maxl',ins')) \ + (\D' rT' maxs' maxl' ins'. + method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins')) \ G \ rT0 \ rT') \ correct_frame G hp (tl ST, LT) maxl ins f \ correct_frames G hp phi rT sig frs))))" @@ -63,8 +63,8 @@ | (f#fs) => G\h hp\ \ (let (stk,loc,C,sig,pc) = f in - \rT maxl ins s. - method (G,C) sig = Some(C,rT,(maxl,ins)) \ + \rT maxs maxl ins s. + method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \ phi C sig ! pc = Some s \ correct_frame G hp s maxl ins f \ correct_frames G hp phi rT sig fs)) diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/DFA_Framework.thy --- a/src/HOL/MicroJava/BV/DFA_Framework.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/DFA_Framework.thy Tue Dec 05 14:08:56 2000 +0100 @@ -11,6 +11,8 @@ theory DFA_Framework = Listn: constdefs + bounded :: "(nat => nat list) => nat => bool" +"bounded succs n == !p (nat => 's => 's) diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/DFA_err.thy --- a/src/HOL/MicroJava/BV/DFA_err.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/DFA_err.thy Tue Dec 05 14:08:56 2000 +0100 @@ -25,9 +25,6 @@ (nat => 's err => 's err)" "err_step app step p == lift (%t. if app p t then OK (step p t) else Err)" -bounded :: "(nat => nat list) => nat => bool" -"bounded succs n == !p nat list) => bool" "non_empty succs == !p. succs p ~= []" diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/JType.thy --- a/src/HOL/MicroJava/BV/JType.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/JType.thy Tue Dec 05 14:08:56 2000 +0100 @@ -97,6 +97,59 @@ apply (auto dest: acyclic_impl_antisym_rtrancl antisymD) done +lemma wf_converse_subcls1_impl_acc_subtype: + "wf ((subcls1 G)^-1) ==> acc (subtype G)" +apply (unfold acc_def lesssub_def) +apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset) + apply blast +apply (drule wf_trancl) +apply (simp add: wf_eq_minimal) +apply clarify +apply (unfold lesub_def subtype_def) +apply (rename_tac M T) +apply (case_tac "EX C. Class C : M") + prefer 2 + apply (case_tac T) + apply (fastsimp simp add: PrimT_PrimT2) + apply simp + apply (subgoal_tac "ref_ty = NullT") + apply simp + apply (rule_tac x = NT in bexI) + apply (rule allI) + apply (rule impI, erule conjE) + apply (drule widen_RefT) + apply clarsimp + apply (case_tac t) + apply simp + apply simp + apply simp + apply (case_tac ref_ty) + apply simp + apply simp +apply (erule_tac x = "{C. Class C : M}" in allE) +apply auto +apply (rename_tac D) +apply (rule_tac x = "Class D" in bexI) + prefer 2 + apply assumption +apply clarify +apply (frule widen_RefT) +apply (erule exE) +apply (case_tac t) + apply simp +apply simp +apply (insert rtrancl_r_diff_Id [symmetric, standard, of "(subcls1 G)"]) +apply simp +apply (erule rtranclE) + apply blast +apply (drule rtrancl_converseI) +apply (subgoal_tac "((subcls1 G)-Id)^-1 = ((subcls1 G)^-1 - Id)") + prefer 2 + apply blast +apply simp +apply (blast intro: rtrancl_into_trancl2) +done + lemma closed_err_types: "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] ==> closed (err (types G)) (lift2 (sup G))" @@ -234,7 +287,8 @@ ML_setup {* bind_thm ("acyclic_subcls1", acyclic_subcls1) *} -theorem "wf_prog wf_mb G ==> err_semilat (esl G)" +theorem err_semilat_JType_esl: + "wf_prog wf_mb G ==> err_semilat (esl G)" by (frule acyclic_subcls1, frule univalent_subcls1, rule err_semilat_JType_esl_lemma) end diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/JVM.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/MicroJava/BV/JVM.thy Tue Dec 05 14:08:56 2000 +0100 @@ -0,0 +1,371 @@ +(* Title: HOL/BCV/JVM.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 2000 TUM + +A micro-JVM +*) + +header "JVM" + +theory JVM = Kildall + JType + Opt + Product + DFA_err + StepMono + BVSpec: + +types state = "state_type option err" + +constdefs + stk_esl :: "'c prog => nat => ty list esl" +"stk_esl S maxs == upto_esl maxs (JType.esl S)" + + reg_sl :: "'c prog => nat => ty err list sl" +"reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))" + + sl :: "'c prog => nat => nat => state sl" +"sl S maxs maxr == + Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))" + + states :: "'c prog => nat => nat => state set" +"states S maxs maxr == fst(sl S maxs maxr)" + + le :: "'c prog => nat => nat => state ord" +"le S maxs maxr == fst(snd(sl S maxs maxr))" + + sup :: "'c prog => nat => nat => state binop" +"sup S maxs maxr == snd(snd(sl S maxs maxr))" + + +constdefs + exec :: "jvm_prog \ nat \ ty \ instr list \ nat \ state \ state" + "exec G maxs rT bs == err_step (\pc. app (bs!pc) G maxs rT) (\pc. step (bs!pc) G)" + + kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list" + "kiljvm G maxs maxr rT bs == + kildall (sl G maxs maxr) (exec G maxs rT bs) (\pc. succs (bs!pc) pc)" + + +lemma JVM_states_unfold: + "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*> + list maxr (err(types S))))" + apply (unfold states_def JVM.sl_def Opt.esl_def Err.sl_def + stk_esl_def reg_sl_def Product.esl_def + Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) + by simp + + +lemma JVM_le_unfold: + "le S m n == + Err.le(Opt.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))" + apply (unfold JVM.le_def JVM.sl_def Opt.esl_def Err.sl_def + stk_esl_def reg_sl_def Product.esl_def + Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) + by simp + + +lemma Err_convert: + "Err.le (subtype G) a b = G \ a <=o b" + by (auto simp add: Err.le_def sup_ty_opt_def lift_top_def lesub_def subtype_def + split: err.split) + +lemma loc_convert: + "Listn.le (Err.le (subtype G)) a b = G \ a <=l b" + by (unfold Listn.le_def lesub_def sup_loc_def list_all2_def) + (simp add: Err_convert) + +lemma zip_map [rule_format]: + "\a. length a = length b --> zip (map f a) (map g b) = map (\(x,y). (f x, g y)) (zip a b)" + apply (induct b) + apply simp + apply clarsimp + apply (case_tac aa) + apply simp+ + done + +lemma stk_convert: + "Listn.le (subtype G) a b = G \ map OK a <=l map OK b" +proof + assume "Listn.le (subtype G) a b" + + hence le: "list_all2 (subtype G) a b" + by (unfold Listn.le_def lesub_def) + + { fix x' y' + assume "length a = length b" + "(x',y') \ set (zip (map OK a) (map OK b))" + then + obtain x y where OK: + "x' = OK x" "y' = OK y" "(x,y) \ set (zip a b)" + by (auto simp add: zip_map) + with le + have "subtype G x y" + by (simp add: list_all2_def Ball_def) + with OK + have "G \ x' <=o y'" + by (simp add: subtype_def) + } + + with le + show "G \ map OK a <=l map OK b" + by (auto simp add: sup_loc_def list_all2_def) +next + assume "G \ map OK a <=l map OK b" + + thus "Listn.le (subtype G) a b" + apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def) + apply (clarsimp simp add: zip_map subtype_def) + apply (drule bspec, assumption) + apply auto + done +qed + + +lemma state_conv: + "Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))) a b = G \ a <=s b" + by (unfold Product.le_def lesub_def sup_state_def) + (simp add: split_beta stk_convert loc_convert) + +lemma state_opt_conv: + "Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G)))) a b = G \ a <=' b" + by (unfold Opt.le_def lesub_def sup_state_opt_def lift_bottom_def) + (auto simp add: state_conv split: option.split) + +lemma JVM_le_convert: + "le G m n (OK t1) (OK t2) = G \ t1 <=' t2" + by (simp add: JVM_le_unfold Err.le_def lesub_def state_opt_conv) + +lemma JVM_le_Err_conv: + "le G m n = Err.le (sup_state_opt G)" + apply (simp add: expand_fun_eq) + apply (unfold Err.le_def JVM_le_unfold lesub_def) + apply (clarsimp split: err.splits) + apply (simp add: state_opt_conv) + done + +lemma special_ex_swap_lemma [iff]: + "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)" + by blast + +theorem exec_pres_type: + "[| wf_prog wf_mb S |] ==> + pres_type (exec S maxs rT bs) (size bs) (states S maxs maxr)" + apply (unfold pres_type_def list_def step_def JVM_states_unfold) + apply (clarify elim!: option_map_in_optionI lift_in_errI) + apply (simp add: exec_def err_step_def lift_def split: err.split) + apply (simp add: step_def option_map_def split: option.splits) + apply clarify + apply (case_tac "bs!p") + + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + defer + apply clarsimp + apply clarsimp + apply clarsimp + defer + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + defer + + apply (simp add: Un_subset_iff) + apply (drule method_wf_mdecl, assumption) + apply (simp add: wf_mdecl_def wf_mhead_def) + + apply (drule is_type_fields) + apply assumption + apply (subgoal_tac "((vname, cname), vT) \ set (fields (S, cname))") + apply assumption + apply (simp add: field_def) + apply (drule map_of_SomeD) + apply auto + done + +theorem exec_mono: + "wf_prog wf_mb G ==> + mono (JVM.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)" + apply (unfold mono_def) + apply clarify + apply (unfold lesub_def) + apply (case_tac t) + apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def) + apply (case_tac s) + apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def) + apply (simp add: JVM_le_convert exec_def err_step_def lift_def) + apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def) + apply (rule conjI) + apply clarify + apply (rule step_mono, assumption+) + apply (rule impI) + apply (erule contrapos_nn) + apply (rule app_mono, assumption+) + done + +theorem semilat_JVM_slI: + "[| wf_prog wf_mb G |] ==> semilat(sl G maxs maxr)" + apply (unfold JVM.sl_def stk_esl_def reg_sl_def) + apply (rule semilat_opt) + apply (rule err_semilat_Product_esl) + apply (rule err_semilat_upto_esl) + apply (rule err_semilat_JType_esl, assumption+) + apply (rule err_semilat_eslI) + apply (rule semilat_Listn_sl) + apply (rule err_semilat_JType_esl, assumption+) + done + +lemma sl_triple_conv: + "sl G maxs maxr == + (states G maxs maxr, le G maxs maxr, sup G maxs maxr)" + by (simp (no_asm) add: states_def JVM.le_def JVM.sup_def) + + +ML_setup {* bind_thm ("wf_subcls1", wf_subcls1); *} + +theorem is_bcv_kiljvm: + "[| wf_prog wf_mb G; bounded (\pc. succs (bs!pc) pc) (size bs) |] ==> + is_bcv (JVM.le G maxs maxr) Err (exec G maxs rT bs) (\pc. succs (bs!pc) pc) + (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)" + apply (unfold kiljvm_def sl_triple_conv) + apply (rule is_bcv_kildall) + apply (simp (no_asm) add: sl_triple_conv [symmetric]) + apply (force intro!: semilat_JVM_slI dest: wf_acyclic simp add: symmetric sl_triple_conv) + apply (simp (no_asm) add: JVM_le_unfold) + apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype + dest: wf_subcls1 wf_acyclic) + apply (simp add: JVM_le_unfold) + apply (erule exec_pres_type) + apply assumption + apply (erule exec_mono) + done + +theorem + "[| wf_prog wf_mb G; bounded (\pc. succs (bs!pc) pc) (size bs); + 0 < size bs; + r = kiljvm G maxs maxr rT bs + (OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))#(replicate (size bs-1) (OK None))); + \n < size bs. r!n \ Err; maxr = Suc (length pTs + mxl); + is_class G C; \x \ set pTs. is_type G x |] + ==> \phi. wt_method G C pTs rT maxs mxl bs phi" +proof - + let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) + #(replicate (size bs-1) (OK None))" + + assume wf: "wf_prog wf_mb G" + assume bounded: "bounded (\pc. succs (bs!pc) pc) (size bs)" + assume result: "r = kiljvm G maxs maxr rT bs ?start" + assume success: "\n < size bs. r!n \ Err" + assume instrs: "0 < size bs" + assume maxr: "maxr = Suc (length pTs + mxl)" + assume isclass: "is_class G C" + assume istype: "\x \ set pTs. is_type G x" + + { fix pc + have "succs (bs!pc) pc \ []" + by (cases "bs!pc") auto + } + + hence non_empty: "non_empty (\pc. succs (bs!pc) pc)" + by (unfold non_empty_def) blast + + from wf bounded + have bcv: + "is_bcv (le G maxs maxr) Err (exec G maxs rT bs) (\pc. succs (bs!pc) pc) + (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)" + by (rule is_bcv_kiljvm) + + { fix l x + have "set (replicate l x) \ {x}" + by (cases "0 < l") simp+ + } note subset_replicate = this + + from istype + have "set pTs \ types G" + by auto + + hence "OK `` set pTs \ err (types G)" + by auto + + with instrs maxr isclass + have "?start \ list (length bs) (states G maxs maxr)" + apply (unfold list_def JVM_states_unfold) + apply simp + apply (rule conjI) + apply (simp add: Un_subset_iff) + apply (rule_tac B = "{Err}" in subset_trans) + apply (simp add: subset_replicate) + apply simp + apply (rule_tac B = "{OK None}" in subset_trans) + apply (simp add: subset_replicate) + apply simp + done + + with bcv success result + have + "\ts\list (length bs) (states G maxs maxr). + ?start <=[le G maxs maxr] ts \ + welltyping (JVM.le G maxs maxr) Err (JVM.exec G maxs rT bs) (\pc. succs (bs ! pc) pc) ts" + by (unfold is_bcv_def) auto + + then obtain phi' where + l: "phi' \ list (length bs) (states G maxs maxr)" and + s: "?start <=[le G maxs maxr] phi'" and + w: "welltyping (le G maxs maxr) Err (exec G maxs rT bs) (\pc. succs (bs ! pc) pc) phi'" + by blast + + hence dynamic: + "dynamic_wt (sup_state_opt G) (exec G maxs rT bs) (\pc. succs (bs ! pc) pc) phi'" + by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv) + + from s + have le: "le G maxs maxr (?start ! 0) (phi'!0)" + by (drule_tac p=0 in le_listD) (simp add: lesub_def)+ + + from l + have l: "size phi' = size bs" + by simp + + with instrs w + have "phi' ! 0 \ Err" + by (unfold welltyping_def) simp + + with instrs l + have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0" + by clarsimp + + + from l bounded + have "bounded (\pc. succs (bs ! pc) pc) (length phi')" + by simp + + with dynamic non_empty + have "static_wt (sup_state_opt G) (\pc. app (bs!pc) G maxs rT) (\pc. step (bs!pc) G) + (\pc. succs (bs!pc) pc) (map ok_val phi')" + by (auto intro: dynamic_imp_static simp add: exec_def) + + with instrs l le bounded + have "wt_method G C pTs rT maxs mxl bs (map ok_val phi')" + apply (unfold wt_method_def static_wt_def) + apply simp + apply (rule conjI) + apply (unfold wt_start_def) + apply (rule JVM_le_convert [THEN iffD1]) + apply (simp (no_asm) add: phi0) + apply clarify + apply (erule allE, erule impE, assumption) + apply (elim conjE) + apply (clarsimp simp add: lesub_def wt_instr_def) + apply (unfold bounded_def) + apply blast + done + + thus ?thesis by blast +qed + +end diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/Kildall.thy --- a/src/HOL/MicroJava/BV/Kildall.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/Kildall.thy Tue Dec 05 14:08:56 2000 +0100 @@ -11,9 +11,6 @@ theory Kildall = DFA_Framework: constdefs - bounded :: "(nat => nat list) => nat => bool" -"bounded succs n == !p 's => 's) => nat => 's set => bool" "pres_type step n A == !s:A. !p prog_certificate" "make_Cert G Phi == \ C sig. - let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \ set G \ Cl = C; - (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \ set mdecls \ sg = sig + let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \ set G \ Cl = C; + (sig,rT,mxs,mxl,b) = SOME (sg,rT,mxs,mxl,b). (sg,rT,mxs,mxl,b) \ set mdecls \ sg = sig in make_cert b (Phi C sig)" @@ -83,19 +83,19 @@ lemma wtl_inst_mono: - "[| wtl_inst i G rT s1 cert mpc pc = OK s1'; fits ins cert phi; + "[| wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; pc < length ins; G \ s2 <=' s1; i = ins!pc |] ==> - \ s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = OK s2' \ (G \ s2' <=' s1')" + \ s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \ (G \ s2' <=' s1')" proof - assume pc: "pc < length ins" "i = ins!pc" - assume wtl: "wtl_inst i G rT s1 cert mpc pc = OK s1'" + assume wtl: "wtl_inst i G rT s1 cert mxs mpc pc = OK s1'" assume fits: "fits ins cert phi" assume G: "G \ s2 <=' s1" let "?step s" = "step i G s" from wtl G - have app: "app i G rT s2" by (auto simp add: wtl_inst_OK app_mono) + have app: "app i G mxs rT s2" by (auto simp add: wtl_inst_OK app_mono) from wtl G have step: "G \ ?step s2 <=' ?step s1" @@ -111,13 +111,13 @@ have "G\ ?step s2 <=' cert!pc'" . } note cert = this - have "\s2'. wtl_inst i G rT s2 cert mpc pc = OK s2' \ G \ s2' <=' s1'" + have "\s2'. wtl_inst i G rT s2 cert mxs mpc pc = OK s2' \ G \ s2' <=' s1'" proof (cases "pc+1 \ set (succs i pc)") case True with wtl have s1': "s1' = ?step s1" by (simp add: wtl_inst_OK) - have "wtl_inst i G rT s2 cert mpc pc = OK (?step s2) \ G \ ?step s2 <=' s1'" + have "wtl_inst i G rT s2 cert mxs mpc pc = OK (?step s2) \ G \ ?step s2 <=' s1'" (is "?wtl \ ?G") proof from True s1' @@ -134,7 +134,7 @@ have "s1' = cert ! Suc pc" by (simp add: wtl_inst_OK) with False app wtl - have "wtl_inst i G rT s2 cert mpc pc = OK s1' \ G \ s1' <=' s1'" + have "wtl_inst i G rT s2 cert mxs mpc pc = OK s1' \ G \ s1' <=' s1'" by (clarsimp intro!: cert simp add: wtl_inst_OK) thus ?thesis by blast @@ -145,11 +145,11 @@ lemma wtl_cert_mono: - "[| wtl_cert i G rT s1 cert mpc pc = OK s1'; fits ins cert phi; + "[| wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; pc < length ins; G \ s2 <=' s1; i = ins!pc |] ==> - \ s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = OK s2' \ (G \ s2' <=' s1')" + \ s2'. wtl_cert (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \ (G \ s2' <=' s1')" proof - - assume wtl: "wtl_cert i G rT s1 cert mpc pc = OK s1'" and + assume wtl: "wtl_cert i G rT s1 cert mxs mpc pc = OK s1'" and fits: "fits ins cert phi" "pc < length ins" "G \ s2 <=' s1" "i = ins!pc" @@ -167,11 +167,11 @@ by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits) from Some wtl - have "wtl_inst i G rT (Some a) cert mpc pc = OK s1'" + have "wtl_inst i G rT (Some a) cert mxs mpc pc = OK s1'" by (simp add: wtl_cert_def split: if_splits) with G fits - have "\ s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = OK s2' \ + have "\ s2'. wtl_inst (ins!pc) G rT (Some a) cert mxs mpc pc = OK s2' \ (G \ s2' <=' s1')" by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+) @@ -182,16 +182,16 @@ lemma wt_instr_imp_wtl_inst: - "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi; + "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi; pc < length ins; length ins = max_pc |] ==> - wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \ Err" + wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \ Err" proof - - assume wt: "wt_instr (ins!pc) G rT phi max_pc pc" + assume wt: "wt_instr (ins!pc) G rT phi mxs max_pc pc" assume fits: "fits ins cert phi" assume pc: "pc < length ins" "length ins = max_pc" from wt - have app: "app (ins!pc) G rT (phi!pc)" by (simp add: wt_instr_def) + have app: "app (ins!pc) G mxs rT (phi!pc)" by (simp add: wt_instr_def) from wt pc have pc': "!!pc'. pc' \ set (succs (ins!pc) pc) ==> pc' < length ins" @@ -210,13 +210,13 @@ qed lemma wt_less_wtl: - "[| wt_instr (ins!pc) G rT phi max_pc pc; - wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s; + "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; + wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s; fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> G \ s <=' phi ! Suc pc" proof - - assume wt: "wt_instr (ins!pc) G rT phi max_pc pc" - assume wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s" + assume wt: "wt_instr (ins!pc) G rT phi mxs max_pc pc" + assume wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s" assume fits: "fits ins cert phi" assume pc: "Suc pc < length ins" "length ins = max_pc" @@ -245,16 +245,16 @@ lemma wt_instr_imp_wtl_cert: - "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi; + "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi; pc < length ins; length ins = max_pc |] ==> - wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc \ Err" + wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc \ Err" proof - - assume "wt_instr (ins!pc) G rT phi max_pc pc" and + assume "wt_instr (ins!pc) G rT phi mxs max_pc pc" and fits: "fits ins cert phi" and pc: "pc < length ins" and "length ins = max_pc" - hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \ Err" + hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \ Err" by (rule wt_instr_imp_wtl_inst) hence "cert!pc = None ==> ?thesis" @@ -277,20 +277,20 @@ lemma wt_less_wtl_cert: - "[| wt_instr (ins!pc) G rT phi max_pc pc; - wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = OK s; + "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; + wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s; fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> G \ s <=' phi ! Suc pc" proof - - assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = OK s" + assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s" - assume wti: "wt_instr (ins!pc) G rT phi max_pc pc" + assume wti: "wt_instr (ins!pc) G rT phi mxs max_pc pc" "fits ins cert phi" "Suc pc < length ins" "length ins = max_pc" { assume "cert!pc = None" with wtl - have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s" + have "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s" by (simp add: wtl_cert_def) with wti have ?thesis @@ -303,7 +303,7 @@ have "cert!pc = phi!pc" by - (rule fitsD2, simp+) with c wtl - have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s" + have "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s" by (simp add: wtl_cert_def) with wti have ?thesis @@ -322,12 +322,12 @@ theorem wt_imp_wtl_inst_list: "\ pc. (\pc'. pc' < length all_ins --> - wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') --> + wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') --> fits all_ins cert phi --> (\l. pc = length l \ all_ins = l@ins) --> pc < length all_ins --> (\ s. (G \ s <=' (phi!pc)) --> - wtl_inst_list ins G rT cert (length all_ins) pc s \ Err)" + wtl_inst_list ins G rT cert mxs (length all_ins) pc s \ Err)" (is "\pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins" is "\pc. ?C pc ins" is "?P ins") proof (induct "?P" "ins") @@ -341,7 +341,7 @@ proof (intro allI impI, elim exE conjE) fix pc s l assume wt : "\pc'. pc' < length all_ins --> - wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'" + wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc'" assume fits: "fits all_ins cert phi" assume l : "pc < length all_ins" assume G : "G \ s <=' phi ! pc" @@ -350,10 +350,10 @@ by (simp add: nth_append) from l wt - have wti: "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast + have wti: "wt_instr (all_ins!pc) G rT phi mxs (length all_ins) pc" by blast with fits l - have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc \ Err" + have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert mxs (length all_ins) pc \ Err" by - (drule wt_instr_imp_wtl_cert, auto) from Cons @@ -361,7 +361,7 @@ with wt fits pc have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto - show "wtl_inst_list (i#ins') G rT cert (length all_ins) pc s \ Err" + show "wtl_inst_list (i#ins') G rT cert mxs (length all_ins) pc s \ Err" proof (cases "?len (Suc pc)") case False with pc @@ -375,13 +375,13 @@ from c wti fits l True obtain s'' where - "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = OK s''" + "wtl_cert (all_ins!pc) G rT (phi!pc) cert mxs (length all_ins) pc = OK s''" "G \ s'' <=' phi ! Suc pc" by clarsimp (drule wt_less_wtl_cert, auto) moreover from calculation fits G l obtain s' where - c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = OK s'" and + c': "wtl_cert (all_ins!pc) G rT s cert mxs (length all_ins) pc = OK s'" and "G \ s' <=' s''" by - (drule wtl_cert_mono, auto) ultimately @@ -389,7 +389,7 @@ by - (rule sup_state_opt_trans) with wtl - have "wtl_inst_list ins' G rT cert (length all_ins) (Suc pc) s' \ Err" + have "wtl_inst_list ins' G rT cert mxs (length all_ins) (Suc pc) s' \ Err" by auto with i c' @@ -400,17 +400,17 @@ lemma fits_imp_wtl_method_complete: - "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==> - wtl_method G C pTs rT mxl ins cert" + "[| wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi |] + ==> wtl_method G C pTs rT mxs mxl ins cert" by (simp add: wt_method_def wtl_method_def) (rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def) lemma wtl_method_complete: - "wt_method G C pTs rT mxl ins phi ==> - wtl_method G C pTs rT mxl ins (make_cert ins phi)" + "wt_method G C pTs rT mxs mxl ins phi + ==> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)" proof - - assume "wt_method G C pTs rT mxl ins phi" + assume "wt_method G C pTs rT mxs mxl ins phi" moreover have "fits ins (make_cert ins phi) phi" by (rule fits_make_cert) @@ -425,16 +425,16 @@ proof (unfold wt_jvm_prog_def) assume wfprog: - "wf_prog (\G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G" + "wf_prog (\G C (sig,rT,mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) G" thus ?thesis proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto) - fix a aa ab b ac ba ad ae bb + fix a aa ab b ac ba ad ae af bb assume 1 : "\(C,sc,fs,ms)\set G. Ball (set fs) (wf_fdecl G) \ unique fs \ (\(sig,rT,mb)\set ms. wf_mhead G sig rT \ - (\(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \ + (\(mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) mb) \ unique ms \ (case sc of None => C = Object | Some D => @@ -443,24 +443,24 @@ (\(sig,rT,b)\set ms. \D' rT' b'. method (G, D) sig = Some (D', rT', b') --> G\rT\rT'))" "(a, aa, ab, b) \ set G" - + assume uG : "unique G" - assume b : "((ac, ba), ad, ae, bb) \ set b" - + assume b : "((ac, ba), ad, ae, af, bb) \ set b" + from 1 - show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))" + show "wtl_method G a ba ad ae af bb (make_Cert G Phi a (ac, ba))" proof (rule bspec [elim_format], clarsimp) assume ub : "unique b" assume m: "\(sig,rT,mb)\set b. wf_mhead G sig rT \ - (\(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb" + (\(mxs,mxl,b). wt_method G a (snd sig) rT mxs mxl b (Phi a sig)) mb" from m b show ?thesis proof (rule bspec [elim_format], clarsimp) - assume "wt_method G a ba ad ae bb (Phi a (ac, ba))" + assume "wt_method G a ba ad ae af bb (Phi a (ac, ba))" with wfprog uG ub b 1 show ?thesis by - (rule wtl_method_complete [elim_format], assumption+, - simp add: make_Cert_def unique_epsilon) + simp add: make_Cert_def unique_epsilon unique_epsilon') qed qed qed diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/LBVCorrect.thy --- a/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Tue Dec 05 14:08:56 2000 +0100 @@ -11,48 +11,48 @@ lemmas [simp del] = split_paired_Ex split_paired_All constdefs -fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool" -"fits phi is G rT s0 cert == +fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,certificate] => bool" +"fits phi is G rT s0 maxs cert == (\pc s1. pc < length is --> - (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1 --> + (wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s0 = OK s1 --> (case cert!pc of None => phi!pc = s1 | Some t => phi!pc = Some t)))" constdefs -make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type" -"make_phi is G rT s0 cert == +make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,certificate] => method_type" +"make_phi is G rT s0 maxs cert == map (\pc. case cert!pc of - None => ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) + None => ok_val (wtl_inst_list (take pc is) G rT cert maxs (length is) 0 s0) | Some t => Some t) [0..length is(]" lemma fitsD_None: - "[|fits phi is G rT s0 cert; pc < length is; - wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1; + "[|fits phi is G rT s0 mxs cert; pc < length is; + wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s0 = OK s1; cert ! pc = None|] ==> phi!pc = s1" by (auto simp add: fits_def) lemma fitsD_Some: - "[|fits phi is G rT s0 cert; pc < length is; - wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1; + "[|fits phi is G rT s0 mxs cert; pc < length is; + wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s0 = OK s1; cert ! pc = Some t|] ==> phi!pc = Some t" by (auto simp add: fits_def) lemma make_phi_Some: "[| pc < length is; cert!pc = Some t |] ==> - make_phi is G rT s0 cert ! pc = Some t" + make_phi is G rT s0 mxs cert ! pc = Some t" by (simp add: make_phi_def) lemma make_phi_None: "[| pc < length is; cert!pc = None |] ==> - make_phi is G rT s0 cert ! pc = - ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)" + make_phi is G rT s0 mxs cert ! pc = + ok_val (wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s0)" by (simp add: make_phi_def) lemma exists_phi: - "\phi. fits phi is G rT s0 cert" + "\phi. fits phi is G rT s0 mxs cert" proof - - have "fits (make_phi is G rT s0 cert) is G rT s0 cert" + have "fits (make_phi is G rT s0 mxs cert) is G rT s0 mxs cert" by (auto simp add: fits_def make_phi_Some make_phi_None split: option.splits) @@ -61,17 +61,17 @@ qed lemma fits_lemma1: - "[| wtl_inst_list is G rT cert (length is) 0 s = OK s'; fits phi is G rT s cert |] + "[| wtl_inst_list is G rT cert mxs (length is) 0 s = OK s'; fits phi is G rT s mxs cert |] ==> \pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t" proof (intro strip) fix pc t - assume "wtl_inst_list is G rT cert (length is) 0 s = OK s'" + assume "wtl_inst_list is G rT cert mxs (length is) 0 s = OK s'" then obtain s'' where - "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s''" + "wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s''" by (blast dest: wtl_take) moreover - assume "fits phi is G rT s cert" + assume "fits phi is G rT s mxs cert" "pc < length is" "cert ! pc = Some t" ultimately @@ -80,26 +80,26 @@ lemma wtl_suc_pc: - "[| wtl_inst_list is G rT cert (length is) 0 s \ Err; - wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'; - wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''; - fits phi is G rT s cert; Suc pc < length is |] ==> + "[| wtl_inst_list is G rT cert mxs (length is) 0 s \ Err; + wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s'; + wtl_cert (is!pc) G rT s' cert mxs (length is) pc = OK s''; + fits phi is G rT s mxs cert; Suc pc < length is |] ==> G \ s'' <=' phi ! Suc pc" proof - - assume all: "wtl_inst_list is G rT cert (length is) 0 s \ Err" - assume fits: "fits phi is G rT s cert" + assume all: "wtl_inst_list is G rT cert mxs (length is) 0 s \ Err" + assume fits: "fits phi is G rT s mxs cert" - assume wtl: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and - wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''" and + assume wtl: "wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s'" and + wtc: "wtl_cert (is!pc) G rT s' cert mxs (length is) pc = OK s''" and pc: "Suc pc < length is" - hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = OK s''" + hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert mxs (length is) 0 s = OK s''" by (rule wtl_Suc) from all have app: - "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert (length is) 0 s \ Err" + "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert mxs (length is) 0 s \ Err" by simp from pc @@ -111,7 +111,7 @@ by (auto simp add: neq_Nil_conv simp del: length_drop) with app wts pc obtain x where - "wtl_cert l G rT s'' cert (length is) (Suc pc) = OK x" + "wtl_cert l G rT s'' cert mxs (length is) (Suc pc) = OK x" by (auto simp add: wtl_append min_def simp del: append_take_drop_id) hence c1: "!!t. cert!Suc pc = Some t ==> G \ s'' <=' cert!Suc pc" @@ -132,20 +132,20 @@ lemma wtl_fits_wt: - "[| wtl_inst_list is G rT cert (length is) 0 s \ Err; - fits phi is G rT s cert; pc < length is |] ==> - wt_instr (is!pc) G rT phi (length is) pc" + "[| wtl_inst_list is G rT cert mxs (length is) 0 s \ Err; + fits phi is G rT s mxs cert; pc < length is |] ==> + wt_instr (is!pc) G rT phi mxs (length is) pc" proof - - assume fits: "fits phi is G rT s cert" + assume fits: "fits phi is G rT s mxs cert" assume pc: "pc < length is" and - wtl: "wtl_inst_list is G rT cert (length is) 0 s \ Err" + wtl: "wtl_inst_list is G rT cert mxs (length is) 0 s \ Err" then obtain s' s'' where - w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and - c: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''" + w: "wtl_inst_list (take pc is) G rT cert mxs (length is) 0 s = OK s'" and + c: "wtl_cert (is!pc) G rT s' cert mxs (length is) pc = OK s''" by - (drule wtl_all, auto) from fits wtl pc @@ -158,7 +158,7 @@ by - (drule fitsD_None) from pc c cert_None cert_Some - have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = OK s''" + have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert mxs (length is) pc = OK s''" by (auto simp add: wtl_cert_def split: if_splits option.splits) { fix pc' @@ -219,16 +219,16 @@ lemma fits_first: - "[| 0 < length is; wtl_inst_list is G rT cert (length is) 0 s \ Err; - fits phi is G rT s cert |] ==> + "[| 0 < length is; wtl_inst_list is G rT cert mxs (length is) 0 s \ Err; + fits phi is G rT s mxs cert |] ==> G \ s <=' phi ! 0" proof - - assume wtl: "wtl_inst_list is G rT cert (length is) 0 s \ Err" - assume fits: "fits phi is G rT s cert" + assume wtl: "wtl_inst_list is G rT cert mxs (length is) 0 s \ Err" + assume fits: "fits phi is G rT s mxs cert" assume pc: "0 < length is" from wtl - have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = OK s" + have wt0: "wtl_inst_list (take 0 is) G rT cert mxs (length is) 0 s = OK s" by simp with fits pc @@ -244,7 +244,7 @@ by (simp add: neq_Nil_conv) (elim, rule that) with wtl obtain s' where - "wtl_cert x G rT s cert (length is) 0 = OK s'" + "wtl_cert x G rT s cert mxs (length is) 0 = OK s'" by simp (elim, rule that, simp) hence "!!t. cert!0 = Some t ==> G \ s <=' cert!0" @@ -257,18 +257,18 @@ lemma wtl_method_correct: -"wtl_method G C pTs rT mxl ins cert ==> \ phi. wt_method G C pTs rT mxl ins phi" +"wtl_method G C pTs rT mxs mxl ins cert ==> \ phi. wt_method G C pTs rT mxs mxl ins phi" proof (unfold wtl_method_def, simp only: Let_def, elim conjE) let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)" assume pc: "0 < length ins" - assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \ Err" + assume wtl: "wtl_inst_list ins G rT cert mxs (length ins) 0 ?s0 \ Err" - obtain phi where fits: "fits phi ins G rT ?s0 cert" + obtain phi where fits: "fits phi ins G rT ?s0 mxs cert" by (rule exists_phi [elim_format]) blast with wtl have allpc: - "\pc. pc < length ins --> wt_instr (ins ! pc) G rT phi (length ins) pc" + "\pc. pc < length ins --> wt_instr (ins ! pc) G rT phi mxs (length ins) pc" by (blast intro: wtl_fits_wt) from pc wtl fits @@ -290,40 +290,40 @@ from wtl_prog show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def) - show "\Phi. Ball (set G) (wf_cdecl (\G C (sig,rT,maxl,b). - wt_method G C (snd sig) rT maxl b (Phi C sig)) G)" + show "\Phi. Ball (set G) (wf_cdecl (\G C (sig,rT,maxs,maxl,b). + wt_method G C (snd sig) rT maxs maxl b (Phi C sig)) G)" (is "\Phi. ?Q Phi") proof (intro exI) let "?Phi" = "\ C sig. let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \ set G \ Cl = C; - (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \ set mdecls \ sg = sig - in SOME phi. wt_method G C (snd sig) rT maxl b phi" + (sig,rT,maxs,maxl,b) = SOME (sg,rT,maxs,maxl,b). (sg,rT,maxs,maxl,b) \ set mdecls \ sg = sig + in SOME phi. wt_method G C (snd sig) rT maxs maxl b phi" from wtl_prog show "?Q ?Phi" proof (unfold wf_cdecl_def, intro) fix x a b aa ba ab bb m assume 1: "x \ set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \ set bb" with wtl_prog - show "wf_mdecl (\G C (sig,rT,maxl,b). - wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m" + show "wf_mdecl (\G C (sig,rT,maxs,maxl,b). + wt_method G C (snd sig) rT maxs maxl b (?Phi C sig)) G a m" proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, elim conjE) apply_end (drule bspec, assumption, simp, elim conjE) assume "\(sig,rT,mb)\set bb. wf_mhead G sig rT \ - (\(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb" + (\(maxs,maxl,b). wtl_method G a (snd sig) rT maxs maxl b (cert a sig)) mb" "unique bb" with 1 uniqueG show "(\(sig,rT,mb). wf_mhead G sig rT \ - (\(maxl,b). - wt_method G a (snd sig) rT maxl b + (\(maxs,maxl,b). + wt_method G a (snd sig) rT maxs maxl b ((\(C,x,y,mdecls). - (\(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b)) - (SOME (sg,rT,maxl,b). (sg, rT, maxl, b) \ set mdecls \ sg = sig)) + (\(sig,rT,maxs,maxl,b). Eps (wt_method G C (snd sig) rT maxs maxl b)) + (SOME (sg,rT,maxs,maxl,b). (sg, rT, maxs, maxl, b) \ set mdecls \ sg = sig)) (SOME (Cl,x,y,mdecls). (Cl, x, y, mdecls) \ set G \ Cl = a))) mb) m" - by - (drule bspec, assumption, + by - (drule bspec, assumption, clarsimp dest!: wtl_method_correct, - clarsimp intro!: someI simp add: unique_epsilon) + clarsimp intro!: someI simp add: unique_epsilon unique_epsilon') qed qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def) qed diff -r 6d6cb845e841 -r fc0b575a2cf7 src/HOL/MicroJava/BV/LBVSpec.thy --- a/src/HOL/MicroJava/BV/LBVSpec.thy Tue Dec 05 14:08:22 2000 +0100 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Tue Dec 05 14:08:56 2000 +0100 @@ -21,52 +21,52 @@ "check_cert i G s cert pc max_pc == \pc' \ set (succs i pc). pc' < max_pc \ (pc' \ pc+1 --> G \ step i G s <=' cert!pc')" - wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] + wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count] => state_type option err" - "wtl_inst i G rT s cert max_pc pc == - if app i G rT s \ check_cert i G s cert pc max_pc then + "wtl_inst i G rT s cert maxs max_pc pc == + if app i G maxs rT s \ check_cert i G s cert pc max_pc then if pc+1 mem (succs i pc) then OK (step i G s) else OK (cert!(pc+1)) else Err"; constdefs - wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] + wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,p_count,p_count] => state_type option err" - "wtl_cert i G rT s cert max_pc pc == + "wtl_cert i G rT s cert maxs max_pc pc == case cert!pc of - None => wtl_inst i G rT s cert max_pc pc + None => wtl_inst i G rT s cert maxs max_pc pc | Some s' => if G \ s <=' (Some s') then - wtl_inst i G rT (Some s') cert max_pc pc + wtl_inst i G rT (Some s') cert maxs max_pc pc else Err" consts - wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count, + wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,p_count,p_count, state_type option] => state_type option err" primrec - "wtl_inst_list [] G rT cert max_pc pc s = OK s" - "wtl_inst_list (i#is) G rT cert max_pc pc s = - (let s' = wtl_cert i G rT s cert max_pc pc in - strict (wtl_inst_list is G rT cert max_pc (pc+1)) s')"; + "wtl_inst_list [] G rT cert maxs max_pc pc s = OK s" + "wtl_inst_list (i#is) G rT cert maxs max_pc pc s = + (let s' = wtl_cert i G rT s cert maxs max_pc pc in + strict (wtl_inst_list is G rT cert maxs max_pc (pc+1)) s')"; constdefs - wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] => bool" - "wtl_method G C pTs rT mxl ins cert == + wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,certificate] => bool" + "wtl_method G C pTs rT mxs mxl ins cert == let max_pc = length ins in 0 < max_pc \ - wtl_inst_list ins G rT cert max_pc 0 + wtl_inst_list ins G rT cert mxs max_pc 0 (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \ Err" wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool" "wtl_jvm_prog G cert == - wf_prog (\G C (sig,rT,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G" + wf_prog (\G C (sig,rT,maxs,maxl,b). wtl_method G C (snd sig) rT maxs maxl b (cert C sig)) G" lemma wtl_inst_OK: -"(wtl_inst i G rT s cert max_pc pc = OK s') = - (app i G rT s \ (\pc' \ set (succs i pc). - pc' < max_pc \ (pc' \ pc+1 --> G \ step i G s <=' cert!pc')) \ +"(wtl_inst i G rT s cert maxs max_pc pc = OK s') = + (app i G maxs rT s \ (\pc' \ set (succs i pc). + pc' < max_pc \ (pc' \ pc+1 --> G \ step i G s <=' cert!pc')) \ (if pc+1 \ set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))" by (auto simp add: wtl_inst_def check_cert_def set_mem_eq); @@ -75,15 +75,15 @@ by (cases x, auto) lemma wtl_Cons: - "wtl_inst_list (i#is) G rT cert max_pc pc s \ Err = - (\s'. wtl_cert i G rT s cert max_pc pc = OK s' \ - wtl_inst_list is G rT cert max_pc (pc+1) s' \ Err)" + "wtl_inst_list (i#is) G rT cert maxs max_pc pc s \ Err = + (\s'. wtl_cert i G rT s cert maxs max_pc pc = OK s' \ + wtl_inst_list is G rT cert maxs max_pc (pc+1) s' \ Err)" by (auto simp del: split_paired_Ex) lemma wtl_append: -"\ s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = OK s') = - (\s''. wtl_inst_list a G rT cert mpc pc s = OK s'' \