--- 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
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Aug 11 14:52:39 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Aug 11 14:52:52 2000 +0200
@@ -9,28 +9,28 @@
theory LBVCorrect = BVSpec + LBVSpec:
constdefs
-fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
-"fits_partial phi pc is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow>
- wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \\<longrightarrow>
- wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \\<longrightarrow>
- ((cert!(pc+length a) = None \\<longrightarrow> phi!(pc+length a) = s1) \\<and>
- (\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
+fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \<Rightarrow> bool"
+"fits_partial phi pc is G rT s0 s2 cert \<equiv> (\<forall> a b i s1. (a@(i#b) = is) \<longrightarrow>
+ wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \<longrightarrow>
+ wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \<longrightarrow>
+ ((cert!(pc+length a) = None \<longrightarrow> phi!(pc+length a) = s1) \<and>
+ (\<forall> t. cert!(pc+length a) = Some t \<longrightarrow> phi!(pc+length a) = t)))"
-fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
-"fits phi is G rT s0 s2 cert \\<equiv> fits_partial phi 0 is G rT s0 s2 cert"
+fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \<Rightarrow> bool"
+"fits phi is G rT s0 s2 cert \<equiv> fits_partial phi 0 is G rT s0 s2 cert"
lemma fitsD:
-"fits phi is G rT s0 s2 cert \\<Longrightarrow>
- (a@(i#b) = is) \\<Longrightarrow>
- wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \\<Longrightarrow>
- wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \\<Longrightarrow>
- ((cert!(0+length a) = None \\<longrightarrow> phi!(0+length a) = s1) \\<and>
- (\\<forall> t. cert!(0+length a) = Some t \\<longrightarrow> phi!(0+length a) = t))"
+"fits phi is G rT s0 s2 cert \<Longrightarrow>
+ (a@(i#b) = is) \<Longrightarrow>
+ wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \<Longrightarrow>
+ wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \<Longrightarrow>
+ ((cert!(0+length a) = None \<longrightarrow> phi!(0+length a) = s1) \<and>
+ (\<forall> t. cert!(0+length a) = Some t \<longrightarrow> phi!(0+length a) = t))"
by (unfold fits_def fits_partial_def) blast
-lemma exists_list: "\\<exists>l. n < length l" (is "?Q n")
+lemma exists_list: "\<exists>l. n < length l" (is "?Q n")
proof (induct "n")
- fix n; assume "?Q n"
+ fix n assume "?Q n"
thus "?Q (Suc n)"
proof elim
fix l assume "n < length (l::'a list)"
@@ -40,12 +40,12 @@
qed auto
lemma exists_phi:
-"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow>
- \\<exists> phi. fits phi is G rT s0 s2 cert \\<and> length is < length phi"
+"wtl_inst_list is G rT s0 s2 cert (length is) 0 \<Longrightarrow>
+ \<exists> phi. fits phi is G rT s0 s2 cert \<and> length is < length phi"
proof -
assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0"
- have "\\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc
- \\<longrightarrow> (\\<exists> phi. pc + length is < length phi \\<and> fits_partial phi pc is G rT s0 s2 cert)"
+ have "\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc
+ \<longrightarrow> (\<exists> phi. pc + length is < length phi \<and> fits_partial phi pc is G rT s0 s2 cert)"
(is "?P is")
proof (induct "?P" "is")
case Nil
@@ -69,10 +69,10 @@
by blast
let "?A phi pc x s1'" =
- "(cert ! (pc + length (x::instr list)) = None \\<longrightarrow> phi ! (pc + length x) = s1') \\<and>
- (\\<forall>t. cert ! (pc + length x) = Some t \\<longrightarrow> phi ! (pc + length x) = t)"
+ "(cert ! (pc + length (x::instr list)) = None \<longrightarrow> phi ! (pc + length x) = s1') \<and>
+ (\<forall>t. cert ! (pc + length x) = Some t \<longrightarrow> phi ! (pc + length x) = t)"
- show "\\<exists>phi. pc + length (a # list) < length phi \\<and>
+ show "\<exists>phi. pc + length (a # list) < length phi \<and>
fits_partial phi pc (a # list) G rT s0 s2 cert"
proof (cases "cert!pc")
case None
@@ -148,156 +148,156 @@
lemma fits_lemma1:
-"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow>
- \\<forall> pc t. pc < length is \\<longrightarrow> (cert ! pc) = Some t \\<longrightarrow> (phi ! pc) = t";
-proof intro;
- fix pc t;
- assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0";
- assume fits: "fits phi is G rT s0 s3 cert";
- assume pc: "pc < length is";
- assume cert: "cert ! pc = Some t";
- from pc;
- have "is \\<noteq> []"; by auto;
- hence cons: "\\<exists>i y. is = i#y"; by (simp add: neq_Nil_conv);
- from wtl pc;
- have "\\<exists>a b s1. a@b = is \\<and> length a = pc \\<and>
- wtl_inst_list a G rT s0 s1 cert (length is) 0 \\<and>
+"\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\<rbrakk> \<Longrightarrow>
+ \<forall> pc t. pc < length is \<longrightarrow> (cert ! pc) = Some t \<longrightarrow> (phi ! pc) = t"
+proof intro
+ fix pc t
+ assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0"
+ assume fits: "fits phi is G rT s0 s3 cert"
+ assume pc: "pc < length is"
+ assume cert: "cert ! pc = Some t"
+ from pc
+ have "is \<noteq> []" by auto
+ hence cons: "\<exists>i y. is = i#y" by (simp add: neq_Nil_conv)
+ from wtl pc
+ have "\<exists>a b s1. a@b = is \<and> length a = pc \<and>
+ wtl_inst_list a G rT s0 s1 cert (length is) 0 \<and>
wtl_inst_list b G rT s1 s3 cert (length is) (0+length a)"
- (is "\\<exists>a b s1. ?A a b \\<and> ?L a \\<and> ?W1 a s1 \\<and> ?W2 a b s1");
- by (rule wtl_partial [rulify]);
- with cons;
- show "phi ! pc = t";
- proof (elim exE conjE);
- fix a b s1 i y;
- assume * :"?A a b" "?L a" "?W1 a s1" "?W2 a b s1" "is = i#y";
- with pc;
- have "b \\<noteq> []"; by auto;
- hence "\\<exists>b' bs. b = b'#bs"; by (simp add: neq_Nil_conv);
- thus ?thesis;
- proof (elim exE);
- fix b' bs; assume Cons: "b=b'#bs";
- with * fits cert;
- show ?thesis;
- proof (unfold fits_def fits_partial_def, elim allE impE);
- from * Cons; show "a@b'#bs=is"; by simp;
- qed simp+;
- qed;
- qed;
-qed;
+ (is "\<exists>a b s1. ?A a b \<and> ?L a \<and> ?W1 a s1 \<and> ?W2 a b s1")
+ by (rule wtl_partial [rulify])
+ with cons
+ show "phi ! pc = t"
+ proof (elim exE conjE)
+ fix a b s1 i y
+ assume * :"?A a b" "?L a" "?W1 a s1" "?W2 a b s1" "is = i#y"
+ with pc
+ have "b \<noteq> []" by auto
+ hence "\<exists>b' bs. b = b'#bs" by (simp add: neq_Nil_conv)
+ thus ?thesis
+ proof (elim exE)
+ fix b' bs assume Cons: "b=b'#bs"
+ with * fits cert
+ show ?thesis
+ proof (unfold fits_def fits_partial_def, elim allE impE)
+ from * Cons show "a@b'#bs=is" by simp
+ qed simp+
+ qed
+ qed
+qed
lemma fits_lemma2:
-"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
+"\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a);
fits phi (a@i#b) G rT s0 s3 cert; cert!(length a) = None;
- wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk>
- \\<Longrightarrow> phi!(length a) = s1";
-proof (unfold fits_def fits_partial_def, elim allE impE);
-qed (auto simp del: split_paired_Ex);
+ wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\<rbrakk>
+ \<Longrightarrow> phi!(length a) = s1"
+proof (unfold fits_def fits_partial_def, elim allE impE)
+qed (auto simp del: split_paired_Ex)
lemma wtl_suc_pc:
-"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
+"\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0;
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a);
wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a));
- fits phi (a@i#b) G rT s0 s3 cert \\<rbrakk> \\<Longrightarrow>
- b \\<noteq> [] \\<longrightarrow> G \\<turnstile> s2 <=s (phi ! (Suc (length a)))";
-proof;
- assume f: "fits phi (a@i#b) G rT s0 s3 cert";
+ fits phi (a@i#b) G rT s0 s3 cert \<rbrakk> \<Longrightarrow>
+ b \<noteq> [] \<longrightarrow> G \<turnstile> s2 <=s (phi ! (Suc (length a)))"
+proof
+ assume f: "fits phi (a@i#b) G rT s0 s3 cert"
assume "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
"wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
- and w: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))";
- hence a: "wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"; by (rule wtl_append);
- assume "b \\<noteq> []"
+ and w: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"
+ hence a: "wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0" by (rule wtl_append)
+ assume "b \<noteq> []"
from this
- obtain b' bs where Cons: "b = b' # bs"; by (simp add: neq_Nil_conv) (elim exE, rule that);
- hence "(a@[i]) @ b' # bs = a @ i # b"; by simp;
+ obtain b' bs where Cons: "b = b' # bs" by (simp add: neq_Nil_conv) (elim exE, rule that)
+ hence "(a@[i]) @ b' # bs = a @ i # b" by simp
with f
- show "G \\<turnstile> s2 <=s phi ! Suc (length a)";
- proof (rule fitsD [elimify]);
- from Cons w;
- show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))";
- by simp;
- from a;
- show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0"; by simp;
+ show "G \<turnstile> s2 <=s phi ! Suc (length a)"
+ proof (rule fitsD [elimify])
+ from Cons w
+ show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))"
+ by simp
+ from a
+ show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0" by simp
assume cert:
- "(cert ! (0 + length (a @ [i])) = None \\<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \\<and>
- (\\<forall>t. cert ! (0 + length (a @ [i])) = Some t \\<longrightarrow> phi ! (0 + length (a @ [i])) = t)";
- show ?thesis;
- proof (cases "cert ! Suc (length a)");
- assume "cert ! Suc (length a) = None";
- with cert;
- have "s2 = phi ! Suc (length a)"; by simp;
- thus ?thesis; by simp;
- next;
- fix t; assume "cert ! Suc (length a) = Some t";
- with cert;
- have "phi ! Suc (length a) = t"; by (simp del: split_paired_All);
- with cert Cons w;
- show ?thesis; by (auto simp add: wtl_inst_option_def)
+ "(cert ! (0 + length (a @ [i])) = None \<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \<and>
+ (\<forall>t. cert ! (0 + length (a @ [i])) = Some t \<longrightarrow> phi ! (0 + length (a @ [i])) = t)"
+ show ?thesis
+ proof (cases "cert ! Suc (length a)")
+ assume "cert ! Suc (length a) = None"
+ with cert
+ have "s2 = phi ! Suc (length a)" by simp
+ thus ?thesis by simp
+ next
+ fix t assume "cert ! Suc (length a) = Some t"
+ with cert
+ have "phi ! Suc (length a) = t" by (simp del: split_paired_All)
+ with cert Cons w
+ show ?thesis by (auto simp add: wtl_inst_option_def)
qed
qed
qed
lemma wtl_lemma:
-"\\<lbrakk>wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0;
+"\<lbrakk>wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0;
wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1);
wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1));
- fits phi (i1@i#i2) G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow>
- wt_instr i G rT phi (length (i1@i#i2)) (length i1)" (concl is "?P i");
-proof -;
- assume w1: "wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0" (is ?w1);
- assume wo: "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)";
- assume w2: "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))";
- assume f: "fits phi (i1@i#i2) G rT s0 s3 cert";
+ fits phi (i1@i#i2) G rT s0 s3 cert\<rbrakk> \<Longrightarrow>
+ wt_instr i G rT phi (length (i1@i#i2)) (length i1)" (concl is "?P i")
+proof -
+ assume w1: "wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0" (is ?w1)
+ assume wo: "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)"
+ assume w2: "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))"
+ assume f: "fits phi (i1@i#i2) G rT s0 s3 cert"
- from w1 wo w2;
- have wtl: "wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length (i1@i#i2)) 0";
- by (rule wtl_cons_appendl);
+ from w1 wo w2
+ have wtl: "wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length (i1@i#i2)) 0"
+ by (rule wtl_cons_appendl)
- with f;
- have c1: "\\<forall>t. cert ! (length i1) = Some t \\<longrightarrow> phi ! (length i1) = t";
- by intro (rule fits_lemma1 [rulify], auto);
+ with f
+ have c1: "\<forall>t. cert ! (length i1) = Some t \<longrightarrow> phi ! (length i1) = t"
+ by intro (rule fits_lemma1 [rulify], auto)
- from w1 wo w2 f;
- have c2: "cert ! (length i1) = None \\<Longrightarrow> phi ! (length i1) = s1";
- by - (rule fits_lemma2);
+ from w1 wo w2 f
+ have c2: "cert ! (length i1) = None \<Longrightarrow> phi ! (length i1) = s1"
+ by - (rule fits_lemma2)
- from wtl f;
- have c3: "\\<forall>pc t. pc < length(i1@i#i2) \\<longrightarrow> cert ! pc = Some t \\<longrightarrow> phi ! pc = t";
- by (rule fits_lemma1);
+ from wtl f
+ have c3: "\<forall>pc t. pc < length(i1@i#i2) \<longrightarrow> cert ! pc = Some t \<longrightarrow> phi ! pc = t"
+ by (rule fits_lemma1)
- from w1 wo w2 f;
- have suc: "i2 \\<noteq> [] \\<Longrightarrow> G \\<turnstile> s2 <=s phi ! Suc (length i1)";
- by (rule wtl_suc_pc [rulify]);
+ from w1 wo w2 f
+ have suc: "i2 \<noteq> [] \<Longrightarrow> G \<turnstile> s2 <=s phi ! Suc (length i1)"
+ by (rule wtl_suc_pc [rulify])
with wo
- show ?thesis;
+ show ?thesis
by (auto simp add: c1 c2 c3 wt_instr_def wtl_inst_def wtl_inst_option_def split: option.split_asm)
qed
lemma wtl_fits_wt:
-"\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\\<rbrakk>
- \\<Longrightarrow> \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
-proof intro;
- assume fits: "fits phi is G rT s0 s3 cert";
+"\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; fits phi is G rT s0 s3 cert\<rbrakk>
+ \<Longrightarrow> \<forall>pc. pc < length is \<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc"
+proof intro
+ assume fits: "fits phi is G rT s0 s3 cert"
- fix pc;
+ fix pc
assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0"
- and pc: "pc < length is";
+ and pc: "pc < length is"
from this
obtain i1 i2' s1 where
l: "i1 @ i2' = is" "length i1 = pc" and
w1: "wtl_inst_list i1 G rT s0 s1 cert (length is) 0" and
- w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)";
- by (rule wtl_partial [rulify, elimify]) (elim, rule that);
+ w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)"
+ by (rule wtl_partial [rulify, elimify]) (elim, rule that)
- from l pc;
- have "i2' \\<noteq> []"; by auto;
+ from l pc
+ have "i2' \<noteq> []" by auto
from this
obtain i i2 where c: "i2' = i#i2"
@@ -324,27 +324,27 @@
qed
lemma wtl_inst_list_correct:
-"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow>
- \\<exists> phi. \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
-proof -;
- assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
+"wtl_inst_list is G rT s0 s2 cert (length is) 0 \<Longrightarrow>
+ \<exists> phi. \<forall>pc. pc < length is \<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc"
+proof -
+ assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0"
from this
- obtain phi where "fits phi is G rT s0 s2 cert";
+ obtain phi where "fits phi is G rT s0 s2 cert"
by (rule exists_phi [elimify]) blast
with wtl
show ?thesis
- by (rule wtl_fits_wt [elimify]) blast;
+ by (rule wtl_fits_wt [elimify]) blast
qed
lemma fits_first:
-"\\<lbrakk>is \\<noteq> [];wtl_inst_list is G rT s0 s2 cert (length is) 0;
- fits phi is G rT s0 s2 cert\\<rbrakk> \\<Longrightarrow> G \\<turnstile> s0 <=s phi ! 0";
-proof -;
- assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
- assume fits: "fits phi is G rT s0 s2 cert";
- assume "is \\<noteq> []"
+"\<lbrakk>is \<noteq> [];wtl_inst_list is G rT s0 s2 cert (length is) 0;
+ fits phi is G rT s0 s2 cert\<rbrakk> \<Longrightarrow> G \<turnstile> s0 <=s phi ! 0"
+proof -
+ assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0"
+ assume fits: "fits phi is G rT s0 s2 cert"
+ assume "is \<noteq> []"
from this
obtain y ys where cons: "is = y#ys"
@@ -360,8 +360,8 @@
by simp
assume cert:
- "(cert ! (0 + length []) = None \\<longrightarrow> phi ! (0 + length []) = s0) \\<and>
- (\\<forall>t. cert ! (0 + length []) = Some t \\<longrightarrow> phi ! (0 + length []) = t)"
+ "(cert ! (0 + length []) = None \<longrightarrow> phi ! (0 + length []) = s0) \<and>
+ (\<forall>t. cert ! (0 + length []) = Some t \<longrightarrow> phi ! (0 + length []) = t)"
show ?thesis
proof (cases "cert!0")
@@ -369,30 +369,30 @@
with cert
show ?thesis by simp
next
- fix t; assume "cert!0 = Some t"
+ fix t assume "cert!0 = Some t"
with cert
- have "phi!0 = t"; by (simp del: split_paired_All);
- with cert cons wtl;
- show ?thesis; by (auto simp add: wtl_inst_option_def);
+ have "phi!0 = t" by (simp del: split_paired_All)
+ with cert cons wtl
+ show ?thesis by (auto simp add: wtl_inst_option_def)
qed
qed simp
qed
lemma wtl_method_correct:
-"wtl_method G C pTs rT mxl ins cert \\<Longrightarrow> \\<exists> phi. wt_method G C pTs rT mxl ins phi"
+"wtl_method G C pTs rT mxl ins cert \<Longrightarrow> \<exists> phi. wt_method G C pTs rT mxl ins phi"
proof (unfold wtl_method_def, simp del: split_paired_Ex, elim exE conjE)
let "?s0" = "([], Some (Class C) # map Some pTs @ replicate mxl None)"
fix s2
- assume neqNil: "ins \\<noteq> []"
+ assume neqNil: "ins \<noteq> []"
assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0"
from this
- obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \\<and> length ins < length phi"
- by (rule exists_phi [elimify]) blast;
+ obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \<and> length ins < length phi"
+ by (rule exists_phi [elimify]) blast
with wtl
have allpc:
- "\\<forall>pc. pc < length ins \\<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
+ "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
by elim (rule wtl_fits_wt [elimify])
from neqNil wtl fits
@@ -404,58 +404,58 @@
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_correct:
-"wtl_jvm_prog G cert ==> \\<exists> Phi. wt_jvm_prog G Phi";
-proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI);
+"wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
+proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI)
- assume wtl_prog: "wtl_jvm_prog G cert";
- thus "ObjectC \\<in> set G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
+ assume wtl_prog: "wtl_jvm_prog G cert"
+ thus "ObjectC \<in> set G" by (simp add: wtl_jvm_prog_def wf_prog_def)
- from wtl_prog;
- show uniqueG: "unique G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
+ from wtl_prog
+ show uniqueG: "unique G" by (simp add: wtl_jvm_prog_def wf_prog_def)
- show "\\<exists>Phi. Ball (set G) (wf_cdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
- (is "\\<exists>Phi. ?Q Phi");
- proof (intro exI);
+ show "\<exists>Phi. Ball (set G) (wf_cdecl (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
+ (is "\<exists>Phi. ?Q Phi")
+ proof (intro exI)
let "?Phi" =
- "\\<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\
- \\<epsilon> phi. wt_method G C (snd sig) rT 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 \\<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \\<in> set bb";
- with wtl_prog;
- show "wf_mdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT 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 "\\<forall>(sig,rT,mb)\\<in>set bb. wf_mhead G sig rT \\<and>
- (\\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
- "unique bb";
- with 1 uniqueG;
- show "(\\<lambda>(sig,rT,mb).
- wf_mhead G sig rT \\<and>
- (\\<lambda>(maxl,b).
+ "\<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\
+ \<epsilon> phi. wt_method G C (snd sig) rT 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 \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb"
+ with wtl_prog
+ show "wf_mdecl (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT 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 "\<forall>(sig,rT,mb)\<in>set bb. wf_mhead G sig rT \<and>
+ (\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
+ "unique bb"
+ with 1 uniqueG
+ show "(\<lambda>(sig,rT,mb).
+ wf_mhead G sig rT \<and>
+ (\<lambda>(maxl,b).
wt_method G a (snd sig) rT maxl b
- ((\\<lambda>(C,x,y,mdecls).
- (\\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
- (\\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \\<in> set mdecls \\<and> sg = sig))
- (\\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \\<in> set G \\<and> Cl = a))) mb) m";
+ ((\<lambda>(C,x,y,mdecls).
+ (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
+ (\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
+ (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
by - (drule bspec, assumption,
- clarsimp elim: wtl_method_correct [elimify],
- clarsimp intro: selectI simp add: unique_epsilon);
- qed;
- qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def);
- qed;
-qed;
+ clarsimp dest!: wtl_method_correct,
+ clarsimp intro!: selectI simp add: unique_epsilon)
+ qed
+ qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
+ qed
+qed
-end;
+end
--- a/src/HOL/MicroJava/BV/Step.thy Fri Aug 11 14:52:39 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy Fri Aug 11 14:52:52 2000 +0200
@@ -12,7 +12,7 @@
text "Effect of instruction on the state type"
consts
-step :: "instr \\<times> jvm_prog \\<times> state_type \\<Rightarrow> state_type option"
+step :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type option"
recdef step "{}"
"step (Load idx, G, (ST, LT)) = Some (the (LT ! idx) # ST, LT)"
@@ -41,22 +41,22 @@
text "Conditions under which step is applicable"
consts
-app :: "instr \\<times> jvm_prog \\<times> ty \\<times> state_type \\<Rightarrow> bool"
+app :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
recdef app "{}"
-"app (Load idx, G, rT, s) = (idx < length (snd s) \\<and> (snd s) ! idx \\<noteq> None)"
+"app (Load idx, G, rT, s) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> None)"
"app (Store idx, G, rT, (ts#ST, LT)) = (idx < length LT)"
"app (Bipush i, G, rT, s) = True"
"app (Aconst_null, G, rT, s) = True"
-"app (Getfield F C, G, rT, (oT#ST, LT)) = (is_class G C \\<and>
- field (G,C) F \\<noteq> None \\<and>
- fst (the (field (G,C) F)) = C \\<and>
- G \\<turnstile> oT \\<preceq> (Class C))"
-"app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \\<and>
- field (G,C) F \\<noteq> None \\<and>
- fst (the (field (G,C) F)) = C \\<and>
- G \\<turnstile> oT \\<preceq> (Class C) \\<and>
- G \\<turnstile> vT \\<preceq> (snd (the (field (G,C) F))))"
+"app (Getfield F C, G, rT, (oT#ST, LT)) = (is_class G C \<and>
+ field (G,C) F \<noteq> None \<and>
+ fst (the (field (G,C) F)) = C \<and>
+ G \<turnstile> oT \<preceq> (Class C))"
+"app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \<and>
+ field (G,C) F \<noteq> None \<and>
+ fst (the (field (G,C) F)) = C \<and>
+ G \<turnstile> oT \<preceq> (Class C) \<and>
+ G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))"
"app (New C, G, rT, s) = (is_class G C)"
"app (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)"
"app (Pop, G, rT, (ts#ST,LT)) = True"
@@ -66,19 +66,19 @@
"app (Swap, G, rT, (ts1#ts2#ST,LT)) = True"
"app (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT))
= True"
-"app (Ifcmpeq b, G, rT, (ts1#ts2#ST,LT)) = ((\\<exists> p. ts1 = PrimT p \\<and> ts1 = PrimT p) \\<or>
- (\\<exists>r r'. ts1 = RefT r \\<and> ts2 = RefT r'))"
+"app (Ifcmpeq b, G, rT, (ts1#ts2#ST,LT)) = ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or>
+ (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r'))"
"app (Goto b, G, rT, s) = True"
-"app (Return, G, rT, (T#ST,LT)) = (G \\<turnstile> T \\<preceq> rT)"
+"app (Return, G, rT, (T#ST,LT)) = (G \<turnstile> T \<preceq> rT)"
app_invoke:
-"app (Invoke C mn fpTs, G, rT, s) = (length fpTs < length (fst s) \\<and>
+"app (Invoke C mn fpTs, G, rT, s) = (length fpTs < length (fst s) \<and>
(let
apTs = rev (take (length fpTs) (fst s));
X = hd (drop (length fpTs) (fst s))
in
- G \\<turnstile> X \\<preceq> Class C \\<and>
- (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
- method (G,C) (mn,fpTs) \\<noteq> None
+ G \<turnstile> X \<preceq> Class C \<and>
+ (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
+ method (G,C) (mn,fpTs) \<noteq> None
))"
"app (i,G,rT,s) = False"
@@ -87,7 +87,7 @@
text {* \isa{p_count} of successor instructions *}
consts
-succs :: "instr \\<Rightarrow> p_count \\<Rightarrow> p_count set"
+succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set"
primrec
"succs (Load idx) pc = {pc+1}"
@@ -110,25 +110,25 @@
"succs (Invoke C mn fpTs) pc = {pc+1}"
-lemma 1: "2 < length a \\<Longrightarrow> (\\<exists>l l' l'' ls. a = l#l'#l''#ls)"
+lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
proof (cases a)
fix x xs assume "a = x#xs" "2 < length a"
thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
qed auto
-lemma 2: "\\<not>(2 < length a) \\<Longrightarrow> a = [] \\<or> (\\<exists> l. a = [l]) \\<or> (\\<exists> l l'. a = [l,l'])"
+lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
proof -;
- assume "\\<not>(2 < length a)"
+ assume "\<not>(2 < length a)"
hence "length a < (Suc 2)" by simp
- hence * : "length a = 0 \\<or> length a = 1 \\<or> length a = 2" by (auto simp add: less_Suc_eq)
+ hence * : "length a = 0 \<or> length a = 1 \<or> length a = 2" by (auto simp add: less_Suc_eq)
{
fix x
assume "length x = 1"
- hence "\\<exists> l. x = [l]" by - (cases x, auto)
+ hence "\<exists> l. x = [l]" by - (cases x, auto)
} note 0 = this
- have "length a = 2 \\<Longrightarrow> \\<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+ have "length a = 2 \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
with * show ?thesis by (auto dest: 0)
qed
@@ -139,56 +139,56 @@
*}
lemma appStore[simp]:
-"app (Store idx, G, rT, s) = (\\<exists> ts ST LT. s = (ts#ST,LT) \\<and> idx < length LT)"
+"app (Store idx, G, rT, s) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appGetField[simp]:
-"app (Getfield F C, G, rT, s) = (\\<exists> oT ST LT. s = (oT#ST, LT) \\<and> is_class G C \\<and>
- fst (the (field (G,C) F)) = C \\<and>
- field (G,C) F \\<noteq> None \\<and> G \\<turnstile> oT \\<preceq> (Class C))"
+"app (Getfield F C, G, rT, s) = (\<exists> oT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>
+ fst (the (field (G,C) F)) = C \<and>
+ field (G,C) F \<noteq> None \<and> G \<turnstile> oT \<preceq> (Class C))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appPutField[simp]:
-"app (Putfield F C, G, rT, s) = (\\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \\<and> is_class G C \\<and>
- field (G,C) F \\<noteq> None \\<and> fst (the (field (G,C) F)) = C \\<and>
- G \\<turnstile> oT \\<preceq> (Class C) \\<and>
- G \\<turnstile> vT \\<preceq> (snd (the (field (G,C) F))))"
+"app (Putfield F C, G, rT, s) = (\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and>
+ field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
+ G \<turnstile> oT \<preceq> (Class C) \<and>
+ G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appCheckcast[simp]:
-"app (Checkcast C, G, rT, s) = (\\<exists>rT ST LT. s = (RefT rT#ST,LT) \\<and> is_class G C)"
+"app (Checkcast C, G, rT, s) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C)"
by (cases s, cases "fst s", simp, cases "hd (fst s)", auto)
lemma appPop[simp]:
-"app (Pop, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))"
+"app (Pop, G, rT, s) = (\<exists>ts ST LT. s = (ts#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appDup[simp]:
-"app (Dup, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))"
+"app (Dup, G, rT, s) = (\<exists>ts ST LT. s = (ts#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appDup_x1[simp]:
-"app (Dup_x1, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
+"app (Dup_x1, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appDup_x2[simp]:
-"app (Dup_x2, G, rT, s) = (\\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"
+"app (Dup_x2, G, rT, s) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appSwap[simp]:
-"app (Swap, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
+"app (Swap, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appIAdd[simp]:
-"app (IAdd, G, rT, s) = (\\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s")
+"app (IAdd, G, rT, s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s")
proof (cases s)
case Pair
have "?app (a,b) = ?P (a,b)"
@@ -218,44 +218,49 @@
lemma appIfcmpeq[simp]:
-"app (Ifcmpeq b, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \\<and>
- ((\\<exists> p. ts1 = PrimT p \\<and> ts1 = PrimT p) \\<or>
- (\\<exists>r r'. ts1 = RefT r \\<and> ts2 = RefT r')))"
+"app (Ifcmpeq b, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and>
+ ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or>
+ (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appReturn[simp]:
-"app (Return, G, rT, s) = (\\<exists>T ST LT. s = (T#ST,LT) \\<and> (G \\<turnstile> T \\<preceq> rT))"
+"app (Return, G, rT, s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))"
by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
lemma appInvoke[simp]:
-"app (Invoke C mn fpTs, G, rT, s) = (\\<exists>apTs X ST LT.
- s = ((rev apTs) @ (X # ST), LT) \\<and>
- length apTs = length fpTs \\<and>
- G \\<turnstile> X \\<preceq> Class C \\<and>
- (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
- method (G,C) (mn,fpTs) \\<noteq> None)" (is "?app s = ?P s")
+"app (Invoke C mn fpTs, G, rT, s) = (\<exists>apTs X ST LT.
+ s = ((rev apTs) @ (X # ST), LT) \<and>
+ length apTs = length fpTs \<and>
+ G \<turnstile> X \<preceq> Class C \<and>
+ (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
+ method (G,C) (mn,fpTs) \<noteq> None)" (is "?app s = ?P s")
proof (cases s)
case Pair
- have "?app (a,b) \\<Longrightarrow> ?P (a,b)"
+ have "?app (a,b) \<Longrightarrow> ?P (a,b)"
proof -
assume app: "?app (a,b)"
- hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \\<and> length fpTs < length a"
- (is "?a \\<and> ?l") by auto
- hence "?a \\<and> 0 < length (drop (length fpTs) a)" (is "?a \\<and> ?l") by auto
- hence "?a \\<and> ?l \\<and> length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def)
- hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> 0 < length ST" by blast
- hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> ST \\<noteq> []" by blast
- hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> (\\<exists>X ST'. ST = X#ST')" by (simp add: neq_Nil_conv)
- hence "\\<exists>apTs X ST. a = rev apTs @ X # ST \\<and> length apTs = length fpTs" by blast
+ hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> length fpTs < length a"
+ (is "?a \<and> ?l") by auto
+ hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") by auto
+ hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def)
+ hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" by blast
+ hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" by blast
+ hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> (\<exists>X ST'. ST = X#ST')" by (simp add: neq_Nil_conv)
+ hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" by blast
with app
show ?thesis by auto blast
qed
- with Pair have "?app s \\<Longrightarrow> ?P s" by simp
+ with Pair have "?app s \<Longrightarrow> ?P s" by simp
thus ?thesis by auto
qed
lemmas [simp del] = app_invoke
+
+lemma app_step_some:
+ "\<lbrakk>app (i,G,rT,s); succs i pc \<noteq> {}\<rbrakk> \<Longrightarrow> step (i,G,s) \<noteq> None";
+ by (cases s, cases i, auto)
+
end
--- a/src/HOL/MicroJava/BV/StepMono.thy Fri Aug 11 14:52:39 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy Fri Aug 11 14:52:52 2000 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/MicroJava/BV/Step.thy
+(* Title: HOL/MicroJava/BV/StepMono.thy
ID: $Id$
Author: Gerwin Klein
Copyright 2000 Technische Universitaet Muenchen
@@ -11,39 +11,31 @@
lemmas [trans] = sup_state_trans sup_loc_trans widen_trans
-ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}
-ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}
-
-
-lemma app_step_some:
-"\\<lbrakk>app (i,G,rT,s); succs i pc \\<noteq> {} \\<rbrakk> \\<Longrightarrow> step (i,G,s) \\<noteq> None";
-by (cases s, cases i, auto)
-
lemma sup_state_length:
-"G \\<turnstile> s2 <=s s1 \\<Longrightarrow> length (fst s2) = length (fst s1) \\<and> length (snd s2) = length (snd s1)"
+"G \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd)
-lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)"
+lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
proof
- show "xb = PrimT p \\<Longrightarrow> G \\<turnstile> xb \\<preceq> PrimT p" by blast
+ show "xb = PrimT p \<Longrightarrow> G \<turnstile> xb \<preceq> PrimT p" by blast
- show "G\\<turnstile> xb \\<preceq> PrimT p \\<Longrightarrow> xb = PrimT p"
+ show "G\<turnstile> xb \<preceq> PrimT p \<Longrightarrow> xb = PrimT p"
proof (cases xb)
fix prim
- assume "xb = PrimT prim" "G\\<turnstile>xb\\<preceq>PrimT p"
+ assume "xb = PrimT prim" "G\<turnstile>xb\<preceq>PrimT p"
thus ?thesis by simp
next
fix ref
- assume "G\\<turnstile>xb\\<preceq>PrimT p" "xb = RefT ref"
+ assume "G\<turnstile>xb\<preceq>PrimT p" "xb = RefT ref"
thus ?thesis by simp (rule widen_RefT [elimify], auto)
qed
qed
lemma sup_loc_some [rulify]:
-"\\<forall> y n. (G \\<turnstile> b <=l y) \\<longrightarrow> n < length y \\<longrightarrow> y!n = Some t \\<longrightarrow> (\\<exists>t. b!n = Some t \\<and> (G \\<turnstile> (b!n) <=o (y!n)))" (is "?P b")
+"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Some t \<longrightarrow> (\<exists>t. b!n = Some t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
proof (induct "?P" b)
show "?P []" by simp
@@ -52,10 +44,10 @@
proof (clarsimp simp add: list_all2_Cons1 sup_loc_def)
fix z zs n
assume * :
- "G \\<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs"
+ "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs"
"n < Suc (length zs)" "(z # zs) ! n = Some t"
- show "(\\<exists>t. (a # list) ! n = Some t) \\<and> G \\<turnstile>(a # list) ! n <=o Some t"
+ show "(\<exists>t. (a # list) ! n = Some t) \<and> G \<turnstile>(a # list) ! n <=o Some t"
proof (cases n)
case 0
with * show ?thesis by (simp add: sup_ty_opt_some)
@@ -69,8 +61,8 @@
lemma all_widen_is_sup_loc:
-"\\<forall>b. length a = length b \\<longrightarrow> (\\<forall>x\\<in>set (zip a b). x \\<in> widen G) = (G \\<turnstile> (map Some a) <=l (map Some b))"
- (is "\\<forall>b. length a = length b \\<longrightarrow> ?Q a b" is "?P a")
+"\<forall>b. length a = length b \<longrightarrow> (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Some a) <=l (map Some b))"
+ (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
proof (induct "a")
show "?P []" by simp
@@ -87,7 +79,7 @@
lemma append_length_n [rulify]:
-"\\<forall>n. n \\<le> length x \\<longrightarrow> (\\<exists>a b. x = a@b \\<and> length a = n)" (is "?P x")
+"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
proof (induct "?P" "x")
show "?P []" by simp
@@ -96,22 +88,22 @@
show "?P (l#ls)"
proof (intro allI impI)
fix n
- assume l: "n \\<le> length (l # ls)"
+ assume l: "n \<le> length (l # ls)"
- show "\\<exists>a b. l # ls = a @ b \\<and> length a = n"
+ show "\<exists>a b. l # ls = a @ b \<and> length a = n"
proof (cases n)
assume "n=0" thus ?thesis by simp
next
fix "n'" assume s: "n = Suc n'"
with l
- have "n' \\<le> length ls" by simp
- hence "\\<exists>a b. ls = a @ b \\<and> length a = n'" by (rule Cons [rulify])
+ have "n' \<le> length ls" by simp
+ hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rulify])
thus ?thesis
proof elim
fix a b
assume "ls = a @ b" "length a = n'"
with s
- have "l # ls = (l#a) @ b \\<and> length (l#a) = n" by simp
+ have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
thus ?thesis by blast
qed
qed
@@ -121,23 +113,23 @@
lemma rev_append_cons:
-"\\<lbrakk>n < length x\\<rbrakk> \\<Longrightarrow> \\<exists>a b c. x = (rev a) @ b # c \\<and> length a = n"
+"\<lbrakk>n < length x\<rbrakk> \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
proof -
assume n: "n < length x"
- hence "n \\<le> length x" by simp
- hence "\\<exists>a b. x = a @ b \\<and> length a = n" by (rule append_length_n)
+ hence "n \<le> length x" by simp
+ hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
thus ?thesis
proof elim
fix r d assume x: "x = r@d" "length r = n"
with n
- have "\\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
+ have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
thus ?thesis
proof elim
fix b c
assume "d = b#c"
with x
- have "x = (rev (rev r)) @ b # c \\<and> length (rev r) = n" by simp
+ have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
thus ?thesis by blast
qed
qed
@@ -145,9 +137,9 @@
lemma app_mono:
-"\\<lbrakk>G \\<turnstile> s2 <=s s1; app (i, G, rT, s1)\\<rbrakk> \\<Longrightarrow> app (i, G, rT, s2)";
+"\<lbrakk>G \<turnstile> s2 <=s s1; app (i, G, rT, s1)\<rbrakk> \<Longrightarrow> app (i, G, rT, s2)";
proof -
- assume G: "G \\<turnstile> s2 <=s s1"
+ assume G: "G \<turnstile> s2 <=s s1"
assume app: "app (i, G, rT, s1)"
show ?thesis
@@ -158,7 +150,7 @@
have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length)
from G Load app
- have "G \\<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
+ have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
with G Load app l
show ?thesis by clarsimp (drule sup_loc_some, simp+)
@@ -191,22 +183,22 @@
where s1: "s1 = (vT # oT # ST, LT)" and
"field (G, cname) vname = Some (cname, b)"
"is_class G cname" and
- oT: "G\\<turnstile> oT\\<preceq> (Class cname)" and
- vT: "G\\<turnstile> vT\\<preceq> b"
+ oT: "G\<turnstile> oT\<preceq> (Class cname)" and
+ vT: "G\<turnstile> vT\<preceq> b"
by simp (elim exE conjE, simp, rule that)
moreover
from s1 G
obtain vT' oT' ST' LT'
where s2: "s2 = (vT' # oT' # ST', LT')" and
- oT': "G\\<turnstile> oT' \\<preceq> oT" and
- vT': "G\\<turnstile> vT' \\<preceq> vT"
+ oT': "G\<turnstile> oT' \<preceq> oT" and
+ vT': "G\<turnstile> vT' \<preceq> vT"
by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
moreover
from vT' vT
- have "G \\<turnstile> vT' \\<preceq> b" by (rule widen_trans)
+ have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
moreover
from oT' oT
- have "G\\<turnstile> oT' \\<preceq> (Class cname)" by (rule widen_trans)
+ have "G\<turnstile> oT' \<preceq> (Class cname)" by (rule widen_trans)
ultimately
show ?thesis
by (auto simp add: Putfield)
@@ -214,12 +206,12 @@
case Checkcast
with app G
show ?thesis
- by - (cases s2, auto intro: widen_RefT2 simp add: sup_state_Cons2)
+ by - (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2)
next
case Return
with app G
show ?thesis
- by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
+ by - (cases s2, auto simp add: sup_state_Cons2, rule widen_trans)
next
case Pop
with app G
@@ -266,9 +258,9 @@
obtain apTs X ST LT where
s1: "s1 = (rev apTs @ X # ST, LT)" and
l: "length apTs = length list" and
- C: "G \\<turnstile> X \\<preceq> Class cname" and
- w: "\\<forall>x \\<in> set (zip apTs list). x \\<in> widen G" and
- m: "method (G, cname) (mname, list) \\<noteq> None"
+ C: "G \<turnstile> X \<preceq> Class cname" and
+ w: "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
+ m: "method (G, cname) (mname, list) \<noteq> None"
by (simp del: not_None_eq, elim exE conjE) (rule that)
obtain apTs' X' ST' LT' where
@@ -278,7 +270,7 @@
from l s1 G
have "length list < length (fst s2)"
by (simp add: sup_state_length)
- hence "\\<exists>a b c. (fst s2) = rev a @ b # c \\<and> length a = length list"
+ hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
by (rule rev_append_cons [rulify])
thus ?thesis
by - (cases s2, elim exE conjE, simp, rule that)
@@ -289,26 +281,26 @@
from this s1 s2 G
obtain
- G': "G \\<turnstile> (apTs',LT') <=s (apTs,LT)" and
- X : "G \\<turnstile> X' \\<preceq> X" and "G \\<turnstile> (ST',LT') <=s (ST,LT)"
+ G': "G \<turnstile> (apTs',LT') <=s (apTs,LT)" and
+ X : "G \<turnstile> X' \<preceq> X" and "G \<turnstile> (ST',LT') <=s (ST,LT)"
by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1);
with C
- have C': "G \\<turnstile> X' \\<preceq> Class cname"
+ have C': "G \<turnstile> X' \<preceq> Class cname"
by - (rule widen_trans, auto)
from G'
- have "G \\<turnstile> map Some apTs' <=l map Some apTs"
+ have "G \<turnstile> map Some apTs' <=l map Some apTs"
by (simp add: sup_state_def)
also
from l w
- have "G \\<turnstile> map Some apTs <=l map Some list"
+ have "G \<turnstile> map Some apTs <=l map Some list"
by (simp add: all_widen_is_sup_loc)
finally
- have "G \\<turnstile> map Some apTs' <=l map Some list" .
+ have "G \<turnstile> map Some apTs' <=l map Some list" .
with l'
- have w': "\\<forall>x \\<in> set (zip apTs' list). x \\<in> widen G"
+ have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
by (simp add: all_widen_is_sup_loc)
from Invoke s2 l' w' C' m
@@ -319,14 +311,14 @@
lemma step_mono:
-"\\<lbrakk>succs i pc \\<noteq> {}; app (i,G,rT,s2); G \\<turnstile> s1 <=s s2\\<rbrakk> \\<Longrightarrow>
- G \\<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
+"\<lbrakk>succs i pc \<noteq> {}; app (i,G,rT,s2); G \<turnstile> s1 <=s s2\<rbrakk> \<Longrightarrow>
+ G \<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
proof (cases s1, cases s2)
fix a1 b1 a2 b2
assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
- assume succs: "succs i pc \\<noteq> {}"
+ assume succs: "succs i pc \<noteq> {}"
assume app2: "app (i,G,rT,s2)"
- assume G: "G \\<turnstile> s1 <=s s2"
+ assume G: "G \<turnstile> s1 <=s s2"
from G app2
have app1: "app (i,G,rT,s1)" by (rule app_mono)
@@ -334,9 +326,9 @@
from app1 app2 succs
obtain a1' b1' a2' b2'
where step: "step (i,G,s1) = Some (a1',b1')" "step (i,G,s2) = Some (a2',b2')";
- by (auto dest: app_step_some);
+ by (auto dest!: app_step_some);
- have "G \\<turnstile> (a1',b1') <=s (a2',b2')"
+ have "G \<turnstile> (a1',b1') <=s (a2',b2')"
proof (cases i)
case Load
@@ -349,10 +341,10 @@
y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp
from G s
- have "G \\<turnstile> b1 <=l b2" by (simp add: sup_state_def)
+ have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_def)
with y y'
- have "G \\<turnstile> y \\<preceq> y'"
+ have "G \<turnstile> y \<preceq> y'"
by - (drule sup_loc_some, simp+)
with Load G y y' s step app1 app2
@@ -411,17 +403,17 @@
have lr: "length a = length a'" by simp
from lr G s s1 s2
- have "G \\<turnstile> (ST, b1) <=s (ST', b2)"
+ have "G \<turnstile> (ST, b1) <=s (ST', b2)"
by (simp add: sup_state_append_fst sup_state_Cons1)
moreover
from Invoke G s step app1 app2
- have "b1 = b1' \\<and> b2 = b2'" by simp
+ have "b1 = b1' \<and> b2 = b2'" by simp
ultimately
- have "G \\<turnstile> (ST, b1') <=s (ST', b2')" by simp
+ have "G \<turnstile> (ST, b1') <=s (ST', b2')" by simp
with Invoke G s step app1 app2 s1 s2 l l'
show ?thesis