(* Title: HOL/MicroJava/BV/BVLightSpec.thy
ID: $Id$
Author: Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
header {* Specification of the LBV *}
theory LBVSpec = Step :
types
certificate = "state_type option list"
class_certificate = "sig \\<Rightarrow> certificate"
prog_certificate = "cname \\<Rightarrow> class_certificate"
constdefs
wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
"wtl_inst i G rT s s' cert max_pc pc \\<equiv> app (i,G,rT,s) \\<and>
(let s'' = the (step (i,G,s)) in
(\\<forall> pc' \\<in> (succs i pc). pc' < max_pc \\<and>
((pc' \\<noteq> pc+1) \\<longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> s'' <=s the (cert!pc'))) \\<and>
(if (pc+1) \\<in> (succs i pc) then
s' = s''
else
cert ! (pc+1) = Some s'))"
lemma [simp]:
"succs i pc = {pc+1} \\<Longrightarrow>
wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> pc+1 < max_pc \\<and> (s' = the (step (i,G,s))))"
by (unfold wtl_inst_def, auto)
lemma [simp]:
"succs i pc = {} \\<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> cert!(pc+1) = Some s')"
by (unfold wtl_inst_def, auto)
constdefs
wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
"wtl_inst_option i G rT s0 s1 cert max_pc pc \\<equiv>
(case cert!pc of
None \\<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
| Some s0' \\<Rightarrow> (G \\<turnstile> s0 <=s s0') \\<and>
wtl_inst i G rT s0' s1 cert max_pc pc)"
consts
wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
primrec
"wtl_inst_list [] G rT s0 s2 cert max_pc pc = (s0 = s2)"
"wtl_inst_list (instr#is) G rT s0 s2 cert max_pc pc =
(\\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \\<and>
wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))"
constdefs
wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \\<Rightarrow> bool"
"wtl_method G C pTs rT mxl ins cert \\<equiv>
let max_pc = length ins
in
0 < max_pc \\<and>
(\\<exists>s2. wtl_inst_list ins G rT
([],(Some(Class C))#((map Some pTs))@(replicate mxl None))
s2 cert max_pc 0)"
wtl_jvm_prog :: "[jvm_prog,prog_certificate] \\<Rightarrow> bool"
"wtl_jvm_prog G cert \\<equiv>
wf_prog (\\<lambda>G C (sig,rT,maxl,b).
wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
text {* \medskip *}
lemma rev_eq: "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z"
by auto
lemma wtl_inst_unique:
"wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow>
wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i")
by (unfold wtl_inst_def, auto)
lemma wtl_inst_option_unique:
"\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc;
wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'"
by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def)
lemma wtl_inst_list_unique:
"\\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \\<longrightarrow>
wtl_inst_list is G rT s0 s1' cert max_pc pc \\<longrightarrow> s1=s1'" (is "?P is")
proof (induct "?P" "is")
case Nil
show "?P []" by simp
case Cons
show "?P (a # list)"
proof intro
fix s0 fix pc
let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc"
let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc"
assume a: "?l (a#list) s0 s1 pc"
assume b: "?l (a#list) s0 s1' pc"
with a
obtain s s' where "?o s0 s" "?o s0 s'"
and l: "?l list s s1 (Suc pc)"
and l': "?l list s' s1' (Suc pc)" by auto
have "s=s'" by(rule wtl_inst_option_unique)
with l l' Cons
show "s1 = s1'" by blast
qed
qed
lemma wtl_partial:
"\\<forall> pc' pc s.
wtl_inst_list is G rT s s' cert mpc pc \\<longrightarrow> \
pc' < length is \\<longrightarrow> \
(\\<exists> a b s1. a @ b = is \\<and> length a = pc' \\<and> \
wtl_inst_list a G rT s s1 cert mpc pc \\<and> \
wtl_inst_list b G rT s1 s' cert mpc (pc+length a))" (is "?P is")
proof (induct "?P" "is")
case Nil
show "?P []" by auto
case Cons
show "?P (a#list)"
proof (intro allI impI)
fix pc' pc s
assume length: "pc' < length (a # list)"
assume wtl: "wtl_inst_list (a # list) G rT s s' cert mpc pc"
show "\\<exists> a' b s1.
a' @ b = a#list \\<and> length a' = pc' \\<and> \
wtl_inst_list a' G rT s s1 cert mpc pc \\<and> \
wtl_inst_list b G rT s1 s' cert mpc (pc+length a')"
(is "\\<exists> a b s1. ?E a b s1")
proof (cases "pc'")
case 0
with wtl
have "?E [] (a#list) s" by simp
thus ?thesis by blast
next
case Suc
with wtl
obtain s0 where wtlSuc: "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)"
and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc" by auto
from Cons
obtain a' b s1'
where "a' @ b = list" "length a' = nat"
and w:"wtl_inst_list a' G rT s0 s1' cert mpc (Suc pc)"
and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')"
proof (elim allE impE)
from length Suc show "nat < length list" by simp
from wtlSuc show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" .
qed (elim exE conjE, auto)
with Suc wtlOpt
have "?E (a#a') b s1'" by (auto simp del: split_paired_Ex)
thus ?thesis by blast
qed
qed
qed
lemma "wtl_append1":
"\\<lbrakk>wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0;
wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)\\<rbrakk> \\<Longrightarrow>
wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0"
proof -
assume w:
"wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0"
"wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)"
have
"\\<forall> pc s0.
wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\<longrightarrow>
wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\<longrightarrow>
wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x")
proof (induct "?P" "x")
case Nil
show "?P []" by simp
next
case Cons
show "?P (a#list)"
proof intro
fix pc s0
assume y:
"wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))"
assume al:
"wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc"
from this
obtain s' where
a: "wtl_inst_option a G rT s0 s' cert (Suc pc + length (list@y)) pc" and
l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)" by auto
with y Cons
have "wtl_inst_list (list @ y) G rT s' s2 cert (Suc pc + length (list @ y)) (Suc pc)"
by (elim allE impE) (assumption, simp+)
with a
show "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc"
by (auto simp del: split_paired_Ex)
qed
qed
with w
show ?thesis
proof (elim allE impE)
from w show "wtl_inst_list x G rT s0 s1 cert (0+length (x @ y)) 0" by simp
qed simp+
qed
lemma wtl_cons_appendl:
"\\<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))\\<rbrakk> \\<Longrightarrow>
wtl_inst_list (a@i#b) G rT s0 s3 cert (length (a@i#b)) 0"
proof -
assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
assume "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))"
hence "wtl_inst_list (i#b) G rT s1 s3 cert (length (a@i#b)) (length a)"
by (auto simp del: split_paired_Ex)
with a
show ?thesis by (rule wtl_append1)
qed
lemma "wtl_append":
"\\<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))\\<rbrakk> \\<Longrightarrow>
wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"
proof -
assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
assume i: "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
assume b: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))"
have "\\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \\<longrightarrow>
wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \\<longrightarrow>
wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \\<longrightarrow>
wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc" (is "?P a")
proof (induct "?P" "a")
case Nil
show "?P []" by (simp del: split_paired_Ex)
case Cons
show "?P (a#list)" (is "\\<forall>s0 pc. ?x s0 pc \\<longrightarrow> ?y s0 pc \\<longrightarrow> ?z s0 pc \\<longrightarrow> ?p s0 pc")
proof intro
fix s0 pc
assume y: "?y s0 pc"
assume z: "?z s0 pc"
assume "?x s0 pc"
from this
obtain s0' where opt: "wtl_inst_option a G rT s0 s0' cert (pc + length ((a # list) @ i # b)) pc"
and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)"
by (auto simp del: split_paired_Ex)
with y z Cons
have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)"
proof (elim allE impE)
from list show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" .
qed auto
with opt
show "?p s0 pc"
by (auto simp del: split_paired_Ex)
qed
qed
with a i b
show ?thesis
proof (elim allE impE)
from a show "wtl_inst_list a G rT s0 s1 cert (0+length (a@i#b)) 0" by simp
qed auto
qed
end