4 Copyright 2000 Technische Universitaet Muenchen |
4 Copyright 2000 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{Completeness of the LBV} *} |
7 header {* \isaheader{Completeness of the LBV} *} |
8 |
8 |
9 (* This theory is currently broken. The port to exceptions |
9 theory LBVComplete = LBVSpec + Typing_Framework: |
10 didn't make it into the Isabelle 2001 release. It is included for |
|
11 documentation only. See Isabelle 99-2 for a working copy of this |
|
12 theory. *) |
|
13 |
|
14 theory LBVComplete = BVSpec + LBVSpec + EffectMono: |
|
15 |
10 |
16 constdefs |
11 constdefs |
17 contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool" |
12 contains_targets :: "['s steptype, 's certificate, 's option list, nat, nat] \<Rightarrow> bool" |
18 "contains_targets ins cert phi pc == |
13 "contains_targets step cert phi pc n \<equiv> |
19 \<forall>pc' \<in> set (succs (ins!pc) pc). |
14 \<forall>(pc',s') \<in> set (step pc (OK (phi!pc))). pc' \<noteq> pc+1 \<and> pc' < n \<longrightarrow> cert!pc' = phi!pc'" |
20 pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'" |
15 |
21 |
16 fits :: "['s steptype, 's certificate, 's option list, nat] \<Rightarrow> bool" |
22 fits :: "[instr list, certificate, method_type] \<Rightarrow> bool" |
17 "fits step cert phi n \<equiv> \<forall>pc. pc < n \<longrightarrow> |
23 "fits ins cert phi == \<forall>pc. pc < length ins \<longrightarrow> |
18 contains_targets step cert phi pc n \<and> |
24 contains_targets ins cert phi pc \<and> |
19 (cert!pc = None \<or> cert!pc = phi!pc)" |
25 (cert!pc = None \<or> cert!pc = phi!pc)" |
20 |
26 |
21 is_target :: "['s steptype, 's option list, nat, nat] \<Rightarrow> bool" |
27 is_target :: "[instr list, p_count] \<Rightarrow> bool" |
22 "is_target step phi pc' n \<equiv> |
28 "is_target ins pc == |
23 \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < n \<and> (pc',s') \<in> set (step pc (OK (phi!pc)))" |
29 \<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')" |
24 |
30 |
25 make_cert :: "['s steptype, 's option list, nat] \<Rightarrow> 's certificate" |
31 |
26 "make_cert step phi n \<equiv> |
32 constdefs |
27 map (\<lambda>pc. if is_target step phi pc n then phi!pc else None) [0..n(]" |
33 make_cert :: "[instr list, method_type] \<Rightarrow> certificate" |
28 |
34 "make_cert ins phi == |
|
35 map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]" |
|
36 |
|
37 make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate" |
|
38 "make_Cert G Phi == \<lambda> C sig. let (C,rT,(maxs,maxl,b)) = the (method (G,C) sig) |
|
39 in make_cert b (Phi C sig)" |
|
40 |
29 |
41 lemmas [simp del] = split_paired_Ex |
30 lemmas [simp del] = split_paired_Ex |
42 |
31 |
43 lemma make_cert_target: |
32 lemma make_cert_target: |
44 "\<lbrakk> pc < length ins; is_target ins pc \<rbrakk> \<Longrightarrow> make_cert ins phi ! pc = phi!pc" |
33 "\<lbrakk> pc < n; is_target step phi pc n \<rbrakk> \<Longrightarrow> make_cert step phi n ! pc = phi!pc" |
45 by (simp add: make_cert_def) |
34 by (simp add: make_cert_def) |
46 |
35 |
47 lemma make_cert_approx: |
36 lemma make_cert_approx: |
48 "\<lbrakk> pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc \<rbrakk> \<Longrightarrow> |
37 "\<lbrakk> pc < n; make_cert step phi n ! pc \<noteq> phi!pc \<rbrakk> \<Longrightarrow> |
49 make_cert ins phi ! pc = None" |
38 make_cert step phi n ! pc = None" |
50 by (auto simp add: make_cert_def) |
39 by (auto simp add: make_cert_def) |
51 |
40 |
52 lemma make_cert_contains_targets: |
41 lemma make_cert_contains_targets: |
53 "pc < length ins \<Longrightarrow> contains_targets ins (make_cert ins phi) phi pc" |
42 "pc < n \<Longrightarrow> contains_targets step (make_cert step phi n) phi pc n" |
54 proof (unfold contains_targets_def, intro strip, elim conjE) |
43 proof (unfold contains_targets_def, clarify) |
55 fix pc' |
44 fix pc' s' |
56 assume "pc < length ins" |
45 assume "pc < n" |
57 "pc' \<in> set (succs (ins ! pc) pc)" |
46 "(pc',s') \<in> set (step pc (OK (phi ! pc)))" |
58 "pc' \<noteq> pc+1" and |
47 "pc' \<noteq> pc+1" and |
59 pc': "pc' < length ins" |
48 pc': "pc' < n" |
60 |
49 hence "is_target step phi pc' n" by (auto simp add: is_target_def) |
61 hence "is_target ins pc'" |
50 with pc' show "make_cert step phi n ! pc' = phi ! pc'" |
62 by (auto simp add: is_target_def) |
|
63 |
|
64 with pc' |
|
65 show "make_cert ins phi ! pc' = phi ! pc'" |
|
66 by (auto intro: make_cert_target) |
51 by (auto intro: make_cert_target) |
67 qed |
52 qed |
68 |
53 |
69 theorem fits_make_cert: |
54 theorem fits_make_cert: |
70 "fits ins (make_cert ins phi) phi" |
55 "fits step (make_cert step phi n) phi n" |
71 by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets) |
56 by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets) |
72 |
57 |
73 lemma fitsD: |
58 lemma fitsD: |
74 "\<lbrakk> fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); |
59 "\<lbrakk> fits step cert phi n; (pc',s') \<in> set (step pc (OK (phi ! pc))); |
75 pc' \<noteq> Suc pc; pc < length ins; pc' < length ins \<rbrakk> |
60 pc' \<noteq> Suc pc; pc < n; pc' < n \<rbrakk> |
76 \<Longrightarrow> cert!pc' = phi!pc'" |
61 \<Longrightarrow> cert!pc' = phi!pc'" |
77 by (clarsimp simp add: fits_def contains_targets_def) |
62 by (auto simp add: fits_def contains_targets_def) |
78 |
63 |
79 lemma fitsD2: |
64 lemma fitsD2: |
80 "\<lbrakk> fits ins cert phi; pc < length ins; cert!pc = Some s \<rbrakk> |
65 "\<lbrakk> fits step cert phi n; pc < n; cert!pc = Some s \<rbrakk> |
81 \<Longrightarrow> cert!pc = phi!pc" |
66 \<Longrightarrow> cert!pc = phi!pc" |
82 by (auto simp add: fits_def) |
67 by (auto simp add: fits_def) |
|
68 |
|
69 |
|
70 lemma merge_mono: |
|
71 assumes merge: "merge cert f r pc ss1 x = OK s1" |
|
72 assumes less: "ss2 <=|Err.le (Opt.le r)| ss1" |
|
73 shows "\<exists>s2. merge cert f r pc ss2 x = s2 \<and> s2 \<le>|r (OK s1)" |
|
74 proof- |
|
75 from merge |
|
76 obtain "\<forall>(pc',s')\<in>set ss1. pc' \<noteq> pc+1 \<longrightarrow> s' \<le>|r (OK (cert!pc'))" and |
|
77 "(map snd [(p',t')\<in>ss1 . p' = pc+1] ++|f x) = OK s1" |
|
78 sorry |
|
79 show ?thesis sorry |
|
80 qed |
|
81 |
|
82 |
|
83 lemma stable_wtl: |
|
84 assumes stable: "stable (Err.le (Opt.le r)) step (map OK phi) pc" |
|
85 assumes fits: "fits step cert phi n" |
|
86 assumes pc: "pc < length phi" |
|
87 shows "wtl_inst cert f r step pc (phi!pc) \<noteq> Err" |
|
88 proof - |
|
89 from pc have [simp]: "map OK phi ! pc = OK (phi!pc)" by simp |
|
90 from stable |
|
91 have "\<forall>(q,s')\<in>set (step pc (OK (phi!pc))). s' \<le>|r (map OK phi!q)" |
|
92 by (simp add: stable_def) |
|
93 |
|
94 |
|
95 |
|
96 |
|
97 lemma wtl_inst_mono: |
|
98 assumes wtl: "wtl_inst cert f r step pc s1 = OK s1'" |
|
99 assumes fits: "fits step cert phi n" |
|
100 assumes pc: "pc < n" |
|
101 assumes less: "OK s2 \<le>|r (OK s1)" |
|
102 shows "\<exists>s2'. wtl_inst cert f r step pc s2 = OK s2' \<and> OK s2' \<le>|r (OK s1')" |
|
103 apply (simp add: wtl_inst_def) |
|
104 |
83 |
105 |
84 lemma wtl_inst_mono: |
106 lemma wtl_inst_mono: |
85 "\<lbrakk> wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; |
107 "\<lbrakk> wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; |
86 pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow> |
108 pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow> |
87 \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')" |
109 \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')" |