--- a/src/HOL/MicroJava/BV/LBVComplete.thy Fri Aug 11 14:52:39 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Fri Aug 11 14:52:52 2000 +0200
@@ -10,61 +10,61 @@
constdefs
- is_approx :: "['a option list, 'a list] \\<Rightarrow> bool"
- "is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow>
- (a!n = None \\<or> a!n = Some (b!n)))"
+ is_approx :: "['a option list, 'a list] \<Rightarrow> bool"
+ "is_approx a b \<equiv> length a = length b \<and> (\<forall> n. n < length a \<longrightarrow>
+ (a!n = None \<or> a!n = Some (b!n)))"
- contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
- "contains_dead ins cert phi pc \\<equiv>
- Suc pc \\<notin> succs (ins!pc) pc \\<and> Suc pc < length phi \\<longrightarrow>
+ contains_dead :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
+ "contains_dead ins cert phi pc \<equiv>
+ Suc pc \<notin> succs (ins!pc) pc \<and> Suc pc < length phi \<longrightarrow>
cert ! (Suc pc) = Some (phi ! Suc pc)"
- contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
- "contains_targets ins cert phi pc \\<equiv> (
- \\<forall> pc' \\<in> succs (ins!pc) pc. pc' \\<noteq> Suc pc \\<and> pc' < length phi \\<longrightarrow>
+ contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
+ "contains_targets ins cert phi pc \<equiv> (
+ \<forall> pc' \<in> succs (ins!pc) pc. pc' \<noteq> Suc pc \<and> pc' < length phi \<longrightarrow>
cert!pc' = Some (phi!pc'))"
- fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
- "fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
- (\\<forall> pc. pc < length ins \\<longrightarrow>
- contains_dead ins cert phi pc \\<and>
+ fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
+ "fits ins cert phi \<equiv> is_approx cert phi \<and> length ins < length phi \<and>
+ (\<forall> pc. pc < length ins \<longrightarrow>
+ contains_dead ins cert phi pc \<and>
contains_targets ins cert phi pc)"
- is_target :: "[instr list, p_count] \\<Rightarrow> bool"
- "is_target ins pc \\<equiv> \\<exists> pc'. pc' < length ins \\<and> pc \\<in> succs (ins!pc') pc'"
+ is_target :: "[instr list, p_count] \<Rightarrow> bool"
+ "is_target ins pc \<equiv> \<exists> pc'. pc' < length ins \<and> pc \<in> succs (ins!pc') pc'"
- maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
- "maybe_dead ins pc \\<equiv> \\<exists> pc'. pc = pc'+1 \\<and> pc \\<notin> succs (ins!pc') pc'"
+ maybe_dead :: "[instr list, p_count] \<Rightarrow> bool"
+ "maybe_dead ins pc \<equiv> \<exists> pc'. pc = pc'+1 \<and> pc \<notin> succs (ins!pc') pc'"
- mdot :: "[instr list, p_count] \\<Rightarrow> bool"
- "mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc"
+ mdot :: "[instr list, p_count] \<Rightarrow> bool"
+ "mdot ins pc \<equiv> maybe_dead ins pc \<or> is_target ins pc"
consts
- option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list"
+ option_filter_n :: "['a list, nat \<Rightarrow> bool, nat] \<Rightarrow> 'a option list"
primrec
"option_filter_n [] P n = []"
"option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1)
else None # option_filter_n t P (n+1))"
constdefs
- option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list"
- "option_filter l P \\<equiv> option_filter_n l P 0"
+ option_filter :: "['a list, nat \<Rightarrow> bool] \<Rightarrow> 'a option list"
+ "option_filter l P \<equiv> option_filter_n l P 0"
- make_cert :: "[instr list, method_type] \\<Rightarrow> certificate"
- "make_cert ins phi \\<equiv> option_filter phi (mdot ins)"
+ make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
+ "make_cert ins phi \<equiv> option_filter phi (mdot ins)"
- make_Cert :: "[jvm_prog, prog_type] \\<Rightarrow> prog_certificate"
- "make_Cert G Phi \\<equiv> \\<lambda> C sig.
- let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
- let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in
+ make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
+ "make_Cert G Phi \<equiv> \<lambda> C sig.
+ let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C in
+ let (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig in
make_cert b (Phi C sig)"
lemmas [simp del] = split_paired_Ex
-lemma length_ofn [rulify]: "\\<forall>n. length (option_filter_n l P n) = length l"
+lemma length_ofn [rulify]: "\<forall>n. length (option_filter_n l P n) = length l"
by (induct l) auto
@@ -72,7 +72,7 @@
proof -
{
fix a n
- have "\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
+ have "\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
proof (induct a)
show "?P []" by (auto simp add: is_approx_def)
@@ -89,7 +89,7 @@
assume "m < length (option_filter_n (l # ls) P n)"
hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp
- show "option_filter_n (l # ls) P n ! m = None \\<or>
+ show "option_filter_n (l # ls) P n ! m = None \<or>
option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)"
proof (cases "m")
assume "m = 0"
@@ -102,7 +102,7 @@
from m Suc
show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn)
- assume "option_filter_n ls P (Suc n) ! m' = None \\<or>
+ assume "option_filter_n ls P (Suc n) ! m' = None \<or>
option_filter_n ls P (Suc n) ! m' = Some (ls ! m')"
with m Suc
show ?thesis by auto
@@ -117,12 +117,12 @@
qed
lemma option_filter_Some:
-"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)"
+"\<lbrakk>n < length l; P n\<rbrakk> \<Longrightarrow> option_filter l P ! n = Some (l!n)"
proof -
assume 1: "n < length l" "P n"
- have "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow> option_filter_n l P n' ! n = Some (l!n)"
+ have "\<forall>n n'. n < length l \<longrightarrow> P (n+n') \<longrightarrow> option_filter_n l P n' ! n = Some (l!n)"
(is "?P l")
proof (induct l)
show "?P []" by simp
@@ -154,13 +154,13 @@
by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def)
lemma option_filter_contains_targets:
-"pc < length ins \\<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc"
+"pc < length ins \<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc"
proof (unfold contains_targets_def, clarsimp)
fix pc'
assume "pc < length ins"
- "pc' \\<in> succs (ins ! pc) pc"
- "pc' \\<noteq> Suc pc" and
+ "pc' \<in> succs (ins ! pc) pc"
+ "pc' \<noteq> Suc pc" and
pc': "pc' < length phi"
hence "is_target ins pc'" by (auto simp add: is_target_def)
@@ -172,7 +172,7 @@
lemma fits_make_cert:
- "length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi"
+ "length ins < length phi \<Longrightarrow> fits ins (make_cert ins phi) phi"
proof -
assume l: "length ins < length phi"
@@ -194,25 +194,25 @@
qed
lemma fitsD:
-"\\<lbrakk>fits ins cert phi; pc' \\<in> succs (ins!pc) pc; pc' \\<noteq> Suc pc; pc < length ins; pc' < length ins\\<rbrakk>
- \\<Longrightarrow> cert!pc' = Some (phi!pc')"
+"\<lbrakk>fits ins cert phi; pc' \<in> succs (ins!pc) pc; pc' \<noteq> Suc pc; pc < length ins; pc' < length ins\<rbrakk>
+ \<Longrightarrow> cert!pc' = Some (phi!pc')"
by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
lemma fitsD2:
-"\\<lbrakk>fits ins cert phi; Suc pc \\<notin> succs (ins!pc) pc; pc < length ins\\<rbrakk>
- \\<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
+"\<lbrakk>fits ins cert phi; Suc pc \<notin> succs (ins!pc) pc; pc < length ins\<rbrakk>
+ \<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
lemma wtl_inst_mono:
-"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins;
- G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
- \\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
+"\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins;
+ G \<turnstile> s2 <=s s1; i = ins!pc\<rbrakk> \<Longrightarrow>
+ \<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
proof -
assume pc: "pc < length ins" "i = ins!pc"
assume wtl: "wtl_inst i G rT s1 s1' cert mpc pc"
assume fits: "fits ins cert phi"
- assume G: "G \\<turnstile> s2 <=s s1"
+ assume G: "G \<turnstile> s2 <=s s1"
let "?step s" = "step (i, G, s)"
@@ -220,40 +220,40 @@
have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono)
from wtl G
- have step: "succs i pc \\<noteq> {} \\<Longrightarrow> G \\<turnstile> the (?step s2) <=s the (?step s1)"
+ have step: "succs i pc \<noteq> {} \<Longrightarrow> G \<turnstile> the (?step s2) <=s the (?step s1)"
by - (drule step_mono, auto simp add: wtl_inst_def)
with app
- have some: "succs i pc \\<noteq> {} \\<Longrightarrow> ?step s2 \\<noteq> None" by (simp add: app_step_some)
+ have some: "succs i pc \<noteq> {} \<Longrightarrow> ?step s2 \<noteq> None" by (simp add: app_step_some)
{
fix pc'
- assume 0: "pc' \\<in> succs i pc" "pc' \\<noteq> pc+1"
- hence "succs i pc \\<noteq> {}" by auto
- hence "G \\<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
+ assume 0: "pc' \<in> succs i pc" "pc' \<noteq> pc+1"
+ hence "succs i pc \<noteq> {}" by auto
+ hence "G \<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
also
from wtl 0
- have "G \\<turnstile> the (?step s1) <=s the (cert!pc')"
+ have "G \<turnstile> the (?step s1) <=s the (cert!pc')"
by (auto simp add: wtl_inst_def)
finally
- have "G\\<turnstile> the (?step s2) <=s the (cert!pc')" .
+ have "G\<turnstile> the (?step s2) <=s the (cert!pc')" .
} note cert = this
- have "\\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \\<and> G \\<turnstile> s2' <=s s1'"
- proof (cases "pc+1 \\<in> succs i pc")
+ have "\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \<and> G \<turnstile> s2' <=s s1'"
+ proof (cases "pc+1 \<in> succs i pc")
case True
with wtl
have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def)
- have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \\<and> G \\<turnstile> (the (?step s2)) <=s s1'"
- (is "?wtl \\<and> ?G")
+ have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \<and> G \<turnstile> (the (?step s2)) <=s s1'"
+ (is "?wtl \<and> ?G")
proof
from True s1'
show ?G by (auto intro: step)
from True app wtl
show ?wtl
- by (clarsimp intro: cert simp add: wtl_inst_def)
+ by (clarsimp intro!: cert simp add: wtl_inst_def)
qed
thus ?thesis by blast
next
@@ -262,8 +262,8 @@
have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def)
with False app wtl
- have "wtl_inst i G rT s2 s1' cert mpc pc \\<and> G \\<turnstile> s1' <=s s1'"
- by (clarsimp intro: cert simp add: wtl_inst_def)
+ have "wtl_inst i G rT s2 s1' cert mpc pc \<and> G \<turnstile> s1' <=s s1'"
+ by (clarsimp intro!: cert simp add: wtl_inst_def)
thus ?thesis by blast
qed
@@ -273,76 +273,76 @@
lemma wtl_option_mono:
-"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi;
- pc < length ins; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
- \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
+"\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi;
+ pc < length ins; G \<turnstile> s2 <=s s1; i = ins!pc\<rbrakk> \<Longrightarrow>
+ \<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
proof -
assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and
fits: "fits ins cert phi" "pc < length ins"
- "G \\<turnstile> s2 <=s s1" "i = ins!pc"
+ "G \<turnstile> s2 <=s s1" "i = ins!pc"
show ?thesis
proof (cases "cert!pc")
case None
- with wtl fits;
- show ?thesis;
- by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+);
+ with wtl fits
+ show ?thesis
+ by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+)
next
case Some
- with wtl fits;
+ with wtl fits
- have G: "G \\<turnstile> s2 <=s a"
+ have G: "G \<turnstile> s2 <=s a"
by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+)
from Some wtl
- have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def)
+ have "wtl_inst i G rT a s1' cert mpc pc" by (simp add: wtl_inst_option_def)
with G fits
- have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
- by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+);
+ have "\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
+ by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+)
- with Some G;
- show ?thesis; by (simp add: wtl_inst_option_def);
+ with Some G
+ show ?thesis by (simp add: wtl_inst_option_def)
qed
qed
lemma wt_instr_imp_wtl_inst:
-"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
- pc < length ins; length ins = max_pc\\<rbrakk> \\<Longrightarrow>
- \\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
+"\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
+ pc < length ins; length ins = max_pc\<rbrakk> \<Longrightarrow>
+ \<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
proof -
assume wt: "wt_instr (ins!pc) G rT phi 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, rT, phi!pc)" by (simp add: wt_instr_def)
from wt pc
- have pc': "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> pc' < length ins"
+ have pc': "!!pc'. pc' \<in> succs (ins!pc) pc \<Longrightarrow> pc' < length ins"
by (simp add: wt_instr_def)
let ?s' = "the (step (ins!pc,G, phi!pc))"
from wt
- have G: "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> G \\<turnstile> ?s' <=s phi ! pc'"
+ have G: "!!pc'. pc' \<in> succs (ins!pc) pc \<Longrightarrow> G \<turnstile> ?s' <=s phi ! pc'"
by (simp add: wt_instr_def)
from wt fits pc
- have cert: "!!pc'. \\<lbrakk>pc' \\<in> succs (ins!pc) pc; pc' < max_pc; pc' \\<noteq> pc+1\\<rbrakk>
- \\<Longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> ?s' <=s the (cert!pc')"
+ have cert: "!!pc'. \<lbrakk>pc' \<in> succs (ins!pc) pc; pc' < max_pc; pc' \<noteq> pc+1\<rbrakk>
+ \<Longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> ?s' <=s the (cert!pc')"
by (auto dest: fitsD simp add: wt_instr_def)
show ?thesis
- proof (cases "pc+1 \\<in> succs (ins!pc) pc")
+ proof (cases "pc+1 \<in> succs (ins!pc) pc")
case True
- have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \\<and> G \\<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \\<and> ?G")
+ have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \<and> G \<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \<and> ?G")
proof
from True
- show "G \\<turnstile> ?s' <=s phi ! Suc pc" by (simp add: G)
+ show "G \<turnstile> ?s' <=s phi ! Suc pc" by (simp add: G)
from True fits app pc cert pc'
show "?wtl"
@@ -356,7 +356,7 @@
case False
with fits app pc cert pc'
- have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \\<and> G \\<turnstile> ?s'' <=s phi ! Suc pc"
+ have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \<and> G \<turnstile> ?s'' <=s phi ! Suc pc"
by (auto dest: fitsD2 simp add: wtl_inst_def)
thus ?thesis by blast
@@ -365,32 +365,32 @@
lemma wt_instr_imp_wtl_option:
-"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; max_pc = length ins\\<rbrakk> \\<Longrightarrow>
- \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
+"\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; max_pc = length ins\<rbrakk> \<Longrightarrow>
+ \<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
proof -
assume fits : "fits ins cert phi" "pc < length ins"
and "wt_instr (ins!pc) G rT phi max_pc pc"
- "max_pc = length ins";
+ "max_pc = length ins"
- hence * : "\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
- by - (rule wt_instr_imp_wtl_inst, simp+);
+ hence * : "\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \<and> G \<turnstile> s <=s phi ! Suc pc"
+ by - (rule wt_instr_imp_wtl_inst, simp+)
- show ?thesis;
- proof (cases "cert ! pc");
- case None;
- with *;
- show ?thesis; by (simp add: wtl_inst_option_def);
+ show ?thesis
+ proof (cases "cert ! pc")
+ case None
+ with *
+ show ?thesis by (simp add: wtl_inst_option_def)
- next;
- case Some;
+ next
+ case Some
- from fits;
- have "pc < length phi"; by (clarsimp simp add: fits_def);
- with fits Some;
- have "cert ! pc = Some (phi!pc)"; by (auto simp add: fits_def is_approx_def);
+ from fits
+ have "pc < length phi" by (clarsimp simp add: fits_def)
+ with fits Some
+ have "cert ! pc = Some (phi!pc)" by (auto simp add: fits_def is_approx_def)
- with *;
- show ?thesis; by (simp add: wtl_inst_option_def);
+ with *
+ show ?thesis by (simp add: wtl_inst_option_def)
qed
qed
@@ -401,13 +401,13 @@
*}
theorem wt_imp_wtl_inst_list:
-"\\<forall> pc. (\\<forall>pc'. pc' < length all_ins \\<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \\<longrightarrow>
- fits all_ins cert phi \\<longrightarrow>
- (\\<exists>l. pc = length l \\<and> all_ins = l@ins) \\<longrightarrow>
- pc < length all_ins \\<longrightarrow>
- (\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow>
- (\\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))"
-(is "\\<forall>pc. ?wt \\<longrightarrow> ?fits \\<longrightarrow> ?l pc ins \\<longrightarrow> ?len pc \\<longrightarrow> ?wtl pc ins" is "\\<forall>pc. ?C pc ins" is "?P ins")
+"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<longrightarrow>
+ fits all_ins cert phi \<longrightarrow>
+ (\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>
+ pc < length all_ins \<longrightarrow>
+ (\<forall> s. (G \<turnstile> s <=s (phi!pc)) \<longrightarrow>
+ (\<exists>s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))"
+(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins" is "\<forall>pc. ?C pc ins" is "?P ins")
proof (induct "?P" "ins")
case Nil
show "?P []" by simp
@@ -418,10 +418,10 @@
show "?P (i#ins')"
proof (intro allI impI, elim exE conjE)
fix pc s l
- assume wt : "\\<forall>pc'. pc' < length all_ins \\<longrightarrow>
+ assume wt : "\<forall>pc'. pc' < length all_ins \<longrightarrow>
wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
assume fits: "fits all_ins cert phi"
- assume G : "G \\<turnstile> s <=s phi ! pc"
+ assume G : "G \<turnstile> s <=s phi ! pc"
assume l : "pc < length all_ins"
assume pc : "all_ins = l@i#ins'" "pc = length l"
@@ -434,25 +434,25 @@
with fits l
obtain s1 where
"wtl_inst_option (all_ins!pc) G rT (phi!pc) s1 cert (length all_ins) pc" and
- s1: "G \\<turnstile> s1 <=s phi ! (Suc pc)"
+ s1: "G \<turnstile> s1 <=s phi ! (Suc pc)"
by - (drule wt_instr_imp_wtl_option, assumption+, simp, elim exE conjE, simp)
with fits l
obtain s2 where
o: "wtl_inst_option (all_ins!pc) G rT s s2 cert (length all_ins) pc"
- and "G \\<turnstile> s2 <=s s1"
+ and "G \<turnstile> s2 <=s s1"
by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that)
with s1
- have G': "G \\<turnstile> s2 <=s phi ! (Suc pc)"
+ have G': "G \<turnstile> s2 <=s phi ! (Suc pc)"
by - (rule sup_state_trans, auto)
from Cons
have "?C (Suc pc) ins'" by blast
with wt fits pc
- have IH: "?len (Suc pc) \\<longrightarrow> ?wtl (Suc pc) ins'" by auto
+ have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
- show "\\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc"
+ show "\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc"
proof (cases "?len (Suc pc)")
case False
with pc
@@ -475,70 +475,70 @@
lemma fits_imp_wtl_method_complete:
-"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
+"\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
- (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex);
+ (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex)
lemma wtl_method_complete:
-"\\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)";
-proof -;
- assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G";
+"\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)"
+proof -
+ assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G"
- hence "fits ins (make_cert ins phi) phi";
- by - (rule fits_make_cert, simp add: wt_method_def);
+ hence "fits ins (make_cert ins phi) phi"
+ by - (rule fits_make_cert, simp add: wt_method_def)
- with *;
- show ?thesis; by - (rule fits_imp_wtl_method_complete);
-qed;
+ with *
+ show ?thesis by - (rule fits_imp_wtl_method_complete)
+qed
lemma unique_set:
-"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
- by (induct "l") auto;
+"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
+ by (induct "l") auto
lemma unique_epsilon:
-"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
- by (auto simp add: unique_set);
+"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
+ by (auto simp add: unique_set)
-theorem wtl_complete: "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)";
-proof (simp only: wt_jvm_prog_def);
+theorem wtl_complete: "\<lbrakk>wt_jvm_prog G Phi\<rbrakk> \<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)"
+proof (simp only: wt_jvm_prog_def)
- assume wfprog: "wf_prog (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G";
+ assume wfprog: "wf_prog (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl 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;
- assume 1 : "\\<forall>(C,sc,fs,ms)\\<in>set G.
- Ball (set fs) (wf_fdecl G) \\<and>
- unique fs \\<and>
- (\\<forall>(sig,rT,mb)\\<in>set ms. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \\<and>
- unique ms \\<and>
- (case sc of None \\<Rightarrow> C = Object
- | Some D \\<Rightarrow>
- is_class G D \\<and>
- (D, C) \\<notin> (subcls1 G)^* \\<and>
- (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
- "(a, aa, ab, b) \\<in> set 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
+ assume 1 : "\<forall>(C,sc,fs,ms)\<in>set G.
+ Ball (set fs) (wf_fdecl G) \<and>
+ unique fs \<and>
+ (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and> (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
+ unique ms \<and>
+ (case sc of None \<Rightarrow> C = Object
+ | Some D \<Rightarrow>
+ is_class G D \<and>
+ (D, C) \<notin> (subcls1 G)^* \<and>
+ (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
+ "(a, aa, ab, b) \<in> set G"
- assume uG : "unique G";
- assume b : "((ac, ba), ad, ae, bb) \\<in> set b";
+ assume uG : "unique G"
+ assume b : "((ac, ba), ad, ae, bb) \<in> set b"
- from 1;
- show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))";
- proof (rule bspec [elimify], clarsimp);
- assume ub : "unique b";
- assume m: "\\<forall>(sig,rT,mb)\\<in>set b. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb";
- from m b;
- show ?thesis;
- proof (rule bspec [elimify], clarsimp);
- assume "wt_method G a ba ad ae bb (Phi a (ac, ba))";
- with wfprog uG ub b 1;
- show ?thesis;
- by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon);
- qed;
- qed;
- qed;
+ from 1
+ show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
+ proof (rule bspec [elimify], clarsimp)
+ assume ub : "unique b"
+ assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb"
+ from m b
+ show ?thesis
+ proof (rule bspec [elimify], clarsimp)
+ assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"
+ with wfprog uG ub b 1
+ show ?thesis
+ by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon)
+ qed
+ qed
+ qed
qed
lemmas [simp] = split_paired_Ex