File Eval.ML

open Eval;

bind_thms ("arbitrary3_rews", map 
(fn s => prove_goalw thy [arbitrary3_def] s (K[Simp_tac 1]))
["arbitrary3 (In1l x) = In1 arbitrary","arbitrary3 (In1r x) = In1 Unit",
 "arbitrary3 (In2  x) = In2 arbitrary","arbitrary3 (In3  x) = In3 arbitrary"]);
Addsimps (thms "arbitrary3_rews");


section "throwing and catching";

Goalw [throw_def] 
 "throw a' x = xcpt_if True (Some (XcptLoc (the_Addr a'))) (np a' x)";
b y Simp_tac 1;
qed "throw_def2";

Goalw [catch_def] "¬G,Norm s\<turnstile>catch tn";
b y Simp_tac 1;
qed "catch_Norm";
Addsimps [catch_Norm];

Goalw [catch_def] "G,(Some (XcptLoc a), s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C";
b y Simp_tac 1;
qed "catch_XcptLoc";
Addsimps[catch_XcptLoc];

Goalw [new_xcpt_var_def] 
  "new_xcpt_var vn (x,s) = Norm (lupd(EName vn\<mapsto>Addr (the_XcptLoc (the x))) s)";
b y Simp_tac 1;
qed "new_xcpt_var_def2";
Addsimps[new_xcpt_var_def2];


section "assign";

qed_goalw "assign_Norm_Norm" thy [assign_def,Let_def] 
	"\<And>X. f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'" (K [Asm_simp_tac 1]);
qed_goalw "assign_Norm_Some" thy [assign_def,Let_def] 
	"\<And>s.\<lbrakk>fst (f v (Norm s)) = Some y\<rbrakk> \<Longrightarrow> assign f v (Norm s) = (Some y,s)" 
	(K [auto_tac (claset(), simpset() addsimps [split_beta])]);
qed_goalw "assign_Some" thy [assign_def,Let_def] 
	"assign f v (Some x,s) = (Some x,s)" 
	(K [auto_tac (claset(), simpset() addsimps [split_beta])]);
Addsimps[assign_Norm_Norm, assign_Norm_Some, assign_Some];

Goal "assign (\<lambda>v. supd (f v)) v (x, s) = (x, if x = None then f v s else s)";
b y Auto_tac;
qed "assign_supd";
Addsimps[assign_supd];

Goal "assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) = \
\ (raise_if (b s v) xcpt x, if x=None \<and> ¬b s v then f v s else s)";
b y case_tac "x = None" 1;
b y  Auto_tac;
qed "assign_raise_if";
Addsimps[assign_raise_if];


section "fits";

qed_goalw "fits_Null" thy [fits_def] "G,s\<turnstile>Null fits T" (K [
	Simp_tac 1]);
Addsimps [fits_Null];

qed_goalw "fits_Addr_RefT" thy [fits_def]
  "G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t" (K [Auto_tac]);
Addsimps [fits_Addr_RefT];

Goalw [fits_def] "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or> \
\ (\<exists>t. T = RefT t) \<and> a' = Null \<or> \
\ (\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and>  G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T";
b y case_tac "\<exists>pt. T = PrimT pt" 1;
b y  ALLGOALS Asm_full_simp_tac;
b y dtac (non_PrimT RS iffD1) 1;
b y case_tac "a' = Null" 1;
b y  ALLGOALS Asm_full_simp_tac;
qed "fitsD";


section "memory allocation";

Goalw [new_Addr_def] "new_Addr h = Some a \<Longrightarrow> h a = None";
b y Auto_tac;
b y dtac (split_paired_All RS iffD2) 1;
b y fast_tac (claset() addIs [selectI2]) 1;
qed "new_AddrD";

Goalw [enough_mem_def] 
  "\<And>a. \<lbrakk>new_Addr h = Some a; enough_mem\<rbrakk> \<Longrightarrow> still_free h a";
b y Fast_tac 1;
qed "enough_memD";


section "variables";

Goalw [fvar_def] "fvar C stat fn a' s = \
\ ((the (snd (the (globs (snd s) (if stat then Stat C else (Heap (the_Addr a'))))) \
\ (Inl (fn,C))),(\<lambda>v. supd (upd_gobj (if stat then Stat C else \
\ (Heap (the_Addr a'))) (Inl (fn,C)) v))),xupd (if stat then id else np a') s)";
b y simp_tac (simpset() addsimps [Let_def,split_beta]) 1;
qed "fvar_def2";

Goalw [avar_def] "avar G i' a' s = \
\((the(snd(snd(the_Arr(globs (snd s)(Heap(the_Addr a'))))) (Inr(the_Intg i'))),\
\(\<lambda>v (x,s').(raise_if(¬G,s'\<turnstile>v fits(fst(the_Arr(globs (snd s)(Heap(the_Addr a'))))))ArrStore x,\
\ upd_gobj (Heap (the_Addr a')) (Inr (the_Intg i')) v s'))), \
\ xupd (raise_if (¬(#0\<le>(the_Intg i') \<and> \
\(the_Intg i')<fst(snd((the_Arr(globs (snd s) (Heap (the_Addr a')))))))) IndOutBound\
\ \<circ> np a') s)";
b y simp_tac (simpset() addsimps [Let_def,split_beta]) 1;
qed "avar_def2";


section "target";

Goalw [target_def] 
"target IntVir s a' t = obj_class (lookup_obj s a')";
b y Simp_tac 1;
qed "target_IntVir";

Goalw [target_def] "m \<noteq> IntVir \<Longrightarrow> target m s a' t = the_Class (RefT t)";
b y Asm_simp_tac 1;
qed "target_notIntVir";

Goalw [target_def] "target Static s a' t = the_Class (RefT t)";
b y Simp_tac 1;
qed "target_Static";

Goalw [target_def] "target SuperM s a' t = the_Class (RefT t)";
b y Simp_tac 1;
qed "target_SuperM";

Addsimps[target_IntVir, target_Static, target_SuperM];


section "init_lvars";

Goalw [init_lvars_def] "init_lvars G C sig mode a' pvs (x,s) = \
\ set_lvars (init_vals(table_of (fst (snd (snd( the (cmethd G C sig))))))(fst (snd (fst (snd (the (cmethd G C sig)))))[\<mapsto>]pvs) (+)¬mode=Static ?\<mapsto>a') \
\ (if mode = Static then x else np a' x, s)";
b y simp_tac (simpset() addsimps [Let_def,split_beta]) 1;
qed "init_lvars_def2";


section "body";

Goalw [body_def, Let_def]
"body G C sig = (\<lambda> (D, _, _, c, ee). Body D c ee) (the (cmethd G C sig))";
b y rtac refl 1;
qed "body_def2";


section "improved induction rule";

Goal "(\<lambda>(u,ua) ub uc ud ue. P (u, ua) ub uc (ud, ue)) xs = \
\     (\<lambda>       ub uc ud ue. P xs      ub uc (ud, ue))";
b y pair_tac "xs" 1;
b y Simp_tac 1;
qed "Call_pair_eq_lemma";
val triv = "\
\ \<And>s xc t . P (Some xc,s) t          (arbitrary3 t) (Some xc,s); \
\ \<And>s.       P (Norm    s) (In1r Skip) (In1 Unit) (Norm s); \
\ \<And>s.       P (Norm    s) (In3 []  ) (In3 []) (Norm s); ";
val simple1 = "\
\ \<And>e es s0 x1 s1 x2 s2 v vs. \
\ \<lbrakk>G\<turnstile>Norm s0  \<midarrow>e -\<succ> v \<rightarrow> (x1, s1);  P  (Norm s0) (In1l e) (In1 v)  (x1, s1); \
\  G\<turnstile>(x1, s1) \<midarrow>es\<doteq>\<succ>vs\<rightarrow> (x2, s2);  P (x1,  s1) (In3 es) (In3 vs) (x2, s2)\<rbrakk>\<Longrightarrow>\
\  P (Norm s0) (In3 (e#es)) (In3 (v#vs)) (x2,s2); \
\ \
\ \<And>vn s. P (Norm s) (In2 (LVar vn)) (In2 (lvar vn s)) (Norm s); \
\ \<And>T e v s0 x1 s1. \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> (x1,s1); P (Norm s0) (In1l e) (In1 v) (x1,s1)\<rbrakk> \<Longrightarrow> \
\     P (Norm s0) (In1l (Cast T e)) (In1 v) (xupd (raise_if (¬ (G,s1\<turnstile>v fits T)) ClassCast) (x1,s1)); \
\ \<And>T e v s0 x1 s1. \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> (x1,s1); P (Norm s0) (In1l e) (In1 v) (x1,s1)\<rbrakk> \<Longrightarrow> \
\     P (Norm s0) (In1l (e InstOf T)) (In1 (Bool (v\<noteq>Null \<and> G,s1\<turnstile>v fits RefT T))) (x1,s1); ";
val simple2 = "\
\ \<And>v  s. P (Norm s) (In1l (Lit v)) (In1 v) (Norm s); \
\ \<And>v  s. P (Norm s) (In1l Super) (In1 (val_this s)) (Norm s); \
\ \<And>f v va s0 x1 s1. \
\ \<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> (x1,s1); P (Norm s0) (In2 va) (In2 (v,f)) (x1,s1)\<rbrakk> \<Longrightarrow> \
\  P (Norm s0) (In1l (Acc va)) (In1 v) (x1,s1); \
\     \
\ \<And>e v s0 s1. \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1; P (Norm s0) (In1l e) (In1 v) s1\<rbrakk>  \<Longrightarrow> \
\                   P (Norm s0) (In1r (Expr e)) (In1 Unit) s1; \
\ \<And>c1 c2 s0 s1 s2. \<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; P (Norm s0) (In1r c1) (In1 Unit) s1; \
\                    G\<turnstile>    s1 \<midarrow>c2\<rightarrow> s2; P       s1  (In1r c2) (In1 Unit) s2\<rbrakk>\<Longrightarrow>\
\                  P (Norm s0) (In1r (c1;; c2)) (In1 Unit) s2; ";
val body = "\
\ \<And>C sig v s0 s1. \
\  \<lbrakk>G\<turnstile>Norm s0 \<midarrow>     body G C sig  -\<succ>v\<rightarrow> s1;\
\   P(Norm s0)(In1l(body G C sig))(In1 v)s1\<rbrakk>\
\   \<Longrightarrow> P (Norm s0) (In1l (Methd C sig)) (In1 v) s1; \
\ \<And>C sig v s0 s1 s2 s3 D c e. \<lbrakk>\
\ G\<turnstile>Norm s0 \<midarrow>init D\<rightarrow> s1; P (Norm s0) (In1r (init D)) (In1 Unit) s1;\
\ G\<turnstile>     s1 \<midarrow>c     \<rightarrow> s2; P       s1  (In1r  c      ) (In1 Unit) s2;\
\ G\<turnstile>     s2 \<midarrow>e -\<succ>v \<rightarrow> s3; P       s2  (In1l  e      ) (In1    v) s3\<rbrakk>\<Longrightarrow>\
\                           P (Norm s0) (In1l (Body D c e)) (In1 v) s3; ";
val cond = "\
\ \<And>e0 e1 e2 b v s0 s1 s2.  \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1; P (Norm s0) (In1l e0) (In1 b) s1; \
\                       G\<turnstile>      s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2; \
\                       P       s1  (In1l (if the_Bool b then e1 else e2)) (In1 v)  s2\<rbrakk> \<Longrightarrow> \
\                       P (Norm s0) (In1l (e0 ? e1 : e2)) (In1 v) s2; \
\ \<And>c1 c2 e v s0 s1 s2.  \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1; P (Norm s0) (In1l e) (In1 v) s1; \
\                 G\<turnstile>     s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow>        s2; \
\                 P s1  (In1r (if the_Bool v then c1 else c2)) (In1 Unit) s2\<rbrakk>  \<Longrightarrow> \
\                 P (Norm s0) (In1r (If(e) c1 Else c2)) (In1 Unit) s2; ";
val loop = "\
\ \<And>c e b s0 s1 s2 s3. \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1; P (Norm s0) (In1l e) (In1 b) s1;\
\ if the_Bool b then ((G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> P s1 (In1r c) (In1 Unit) s2) \<and>\
\            G\<turnstile>s2 \<midarrow>While(e) c\<rightarrow> s3 \<and> P s2 (In1r (While(e) c)) (In1 Unit) s3)\
\ else s3 = s1\<rbrakk> \<Longrightarrow>\
\              P (Norm s0) (In1r (While(e) c)) (In1 Unit) s3; ";
val xcpt = "\
\ \<And>c1 c2 x1 s0 s1 s2. \<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1);   \
\          P (Norm s0) (In1r c1) (In1 Unit) (x1, s1); \
\                G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;  \
\         P (Norm s1) (In1r c2) (In1 Unit) s2\<rbrakk> \<Longrightarrow> \
\ P (Norm s0) (In1r (c1 Finally c2)) (In1 Unit) (xupd (xcpt_if (x1 \<noteq> None) x1) s2); \
\ \<And>a' e s0 s1. \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; P (Norm s0) (In1l e) (In1 a') s1\<rbrakk> \<Longrightarrow> \
\ P (Norm s0) (In1r (Throw e)) (In1 Unit) (xupd (throw a') s1); ";
val new = "\
\ \<And>C a s0 s1 s2. \<lbrakk>G\<turnstile>Norm s0       \<midarrow>init C\<rightarrow>         s1; \
\                 P (Norm s0) (In1r (init C)) (In1 Unit) s1; \
\                  G\<turnstile>s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow> \
\           P (Norm s0) (In1l (NewC C)) (In1 (Addr a)) s2; \
\ \<And>T a e i' s0 s1 x2 s2 s3. \
\\<lbrakk>G\<turnstile>Norm s0  \<midarrow>init_comp_ty T\<rightarrow> s1;\
\ P(Norm s0) (In1r (init_comp_ty T)) (In1 Unit)  s1;\
\ G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> (x2,s2); P s1 (In1l e) (In1 i') (x2,s2); \
\ G\<turnstile>xupd (check_neg i') (x2,s2) \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>\
\ P (Norm s0) (In1l (New T[e])) (In1 (Addr a)) s3; ";
val init = "\
\ \<And>s0 C x1 s1 x2 s2 s3 sc si fs ms ini. \
\ \<lbrakk>the (class G C) = (sc,si,fs,ms,ini); \
\  if inited C (globs s0) then s3 = Norm s0 else \
\   ((G\<turnstile>Norm (init_class_obj G C s0) \
\       \<midarrow>(if C = Object then Skip else init sc)\<rightarrow> (x1,s1) \<and> \
\    P(Norm (init_class_obj G C s0)) \
\         (In1r (if C = Object then Skip else init sc)) (In1 Unit) (x1,s1)) \<and> \
\    (G\<turnstile>(set_lvars empty (x1,s1)) \<midarrow>ini\<rightarrow> (x2,s2) \<and> \
\     P (set_lvars empty (x1,s1)) (In1r ini) (In1 Unit) (x2,s2)) \<and> \
\    s3 = restore_lvars (x1,s1) (x2,s2))\<rbrakk> \<Longrightarrow> \
\ P (Norm s0) (In1r (init C)) (In1 Unit) s3; ";
val ass = "\
\ \<And>e w f v va x s0 x1 s1 x2 s2. \
\       \<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> (x1,s1) ; P (Norm s0) (In2 va) (In2 (w,f)) (x1,s1);\
\        G\<turnstile>(x1,s1) \<midarrow>e-\<succ>v\<rightarrow> (x2,s2); P (x1,s1) (In1l e) (In1 v) (x2,s2)\<rbrakk> \<Longrightarrow> \
\  P (Norm s0) (In1l (Ass va e)) (In1 v) (assign f v (x2,s2)); ";
val try = "\
\ \<And>c1 c2 s0 x1 s1 x2 s2 s s3 tn vn. \
\ \<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1); P (Norm s0) (In1r c1) (In1 Unit) (x1,s1); \
\  G\<turnstile>(x1,s1) \<midarrow>sxalloc\<rightarrow> (x2,s2);\
\  if G,(x2,s2)\<turnstile>catch tn then (G\<turnstile>new_xcpt_var vn (x2,s2) \<midarrow>c2\<rightarrow> s3 \<and> \
\     P (new_xcpt_var vn (x2,s2)) (In1r c2) (In1 Unit) s3) else s3=(x2,s2)\<rbrakk> \<Longrightarrow>\
\  P (Norm s0) (In1r (Try c1 Catch(tn vn) c2)) (In1 Unit) s3; ";
val afvar = "\
\ \<And>T a e fn s0 x1 s1 x2 s2 C st stat v s2'. \
\ \<lbrakk>G\<turnstile>Norm s0 \<midarrow>init C\<rightarrow> (x1,s1); P (Norm s0) (In1r (init C)) (In1 Unit) (x1, s1);   \
\  G\<turnstile>(x1,s1) \<midarrow>e-\<succ>a\<rightarrow> (x2,s2); P (x1,s1) (In1l e) (In1 a) (x2,s2); (v,s2') = fvar C stat fn a (x2,s2)\<rbrakk> \<Longrightarrow> \
\  P (Norm s0) (In2 ({C,stat}e..fn)) (In2 v) s2';\
\ \<And>e1 e2 a i s0 x1 s1 x2 s2 T cs v s2'. \
\ \<lbrakk>G\<turnstile>Norm s0  \<midarrow>e1-\<succ>a\<rightarrow> (x1,s1); P (Norm s0) (In1l e1) (In1 a) (x1,s1); \
\   G\<turnstile> (x1,s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2,s2); P (x1,s1)   (In1l e2) (In1 i) (x2,s2); \
\  (v,s2') = avar G i a (x2,s2)\<rbrakk> \<Longrightarrow> \
\  P (Norm s0) (In2 (e1.[e2])) (In2 v) s2'; ";
val call = "\
\ \<And>a' e t cT mode mn pTs ps v pvs s0 x1 s1 x2 s2 x3 s3. \
\   \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> a' \<rightarrow> (x1, s1); P (Norm s0) (In1l e)  (In1 a')  (x1,s1); \
\    G\<turnstile>(x1,s1) \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2, s2); P (x1, s1) (In3 ps) (In3 pvs) (x2,s2); \
\  G\<turnstile>init_lvars G (target mode s2 a' cT) (mn,pTs) mode a' pvs (x2,s2) \
\        \<midarrow>Methd (target mode s2 a' cT) (mn, pTs)     -\<succ>v\<rightarrow> (x3,s3); \
\  P(init_lvars G (target mode s2 a' cT) (mn,pTs) mode a' pvs (x2,s2)) \
\  (In1l (Methd     (target mode s2 a' cT) (mn, pTs))) (In1 v) (x3,s3)\<rbrakk> \<Longrightarrow> \
\   P (Norm s0) (In1l ({t,cT,mode}e..mn({pTs}ps))) (In1 v) (restore_lvars (x2,s2) (x3, s3))";
val prems = goal thy ("\<lbrakk> "^triv^simple1^simple2^body^cond^loop^xcpt^new^
  init^ass^try^afvar^call^" \<rbrakk> \<Longrightarrow> (G\<turnstile>s \<midarrow>e\<succ>\<rightarrow> (v,s') \<longrightarrow> P s e v s')");
b y EVERY'[pair_tac "s", pair_tac "s'"] 1;
b y rtac impI 1;
b y etac eval.induct 1;
val ss = HOL_basic_ss addsimps [read_instantiate [("P","P") ]Call_pair_eq_lemma,
	fst_conv,snd_conv] addsimprocs [split_eta_proc];
b y ALLGOALS (asm_full_simp_tac ss);
val prems' = map (simplify ss) prems;
val tac = resolve_tac prems' THEN_ALL_NEW atac;
b y TRYALL tac;
b y resolve_tac prems' 1;
ba 1;
b y simp_tac ss 1;
qed "eval_induct";

Delsplits[split_if,split_if_asm,option.split,option.split_asm];
val halloc_elim_cases = map halloc.mk_cases [
	"G\<turnstile>(Some xc, s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'",
	"G\<turnstile>(Norm     s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"];

val sxalloc_elim_cases = map sxalloc.mk_cases [
 	"G\<turnstile> Norm              s  \<midarrow>sxalloc\<rightarrow> s'",
 	"G\<turnstile>(Some (XcptLoc a ),s) \<midarrow>sxalloc\<rightarrow> s'",
 	"G\<turnstile>(Some (StdXcpt xn),s) \<midarrow>sxalloc\<rightarrow> s'"];
val sxalloc_cases = sxalloc.mk_cases "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'";
Goal "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'; \
\      \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P; \
\      \<And>a s. \<lbrakk>s' = (Some (XcptLoc a), s)\<rbrakk> \<Longrightarrow> P \
\     \<rbrakk> \<Longrightarrow> P";
b y cut_facts_tac (premises()) 1;
b y etac sxalloc_cases 1;
b y ALLGOALS (eresolve_tac (premises()));
qed "sxalloc_elim_cases2";

val eval_cases = eval.mk_cases "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'";

val cases1 = [
	"G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<rightarrow>  vs'",
	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<rightarrow> vs'"];
val cases2 = [
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c e)              \<succ>\<rightarrow> xs'"];
val cases3 = [
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1r (While(e) c)              \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<rightarrow> vs'"];
val cases4 = [
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In2  ({C,stat}e..fn)           \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l ({t,cT,mode}e..mn({pT}p)) \<succ>\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1r (init C)                  \<succ>\<rightarrow> xs'"];
val eval_elim_cases = map eval.mk_cases (cases1@cases2@cases3@cases4);

Addsplits[split_if,split_if_asm,option.split,option.split_asm];

Goal "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow> \
\ (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = In1 Unit) \
\ | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)";
b y etac eval_cases 1 THEN Auto_tac;
b y induct_tac "t" 1;
b y   induct_tac "a" 1;
b y    Auto_tac;
qed "eval_Inj_elim";

fun eval_fun nam inj rhs =
let
  val name = "eval_" ^ nam ^ "_eq"
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
  val () = qed_goal name thy (lhs ^ " = (" ^ rhs ^ ")") 
	(K [Auto_tac, ALLGOALS (ftac eval_Inj_elim) THEN Auto_tac])
  fun is_Inj (Const (inj,_) $ _) = true
    | is_Inj _                   = false
  fun pred (_ $ (Const ("Pair",_) $ _ $ 
      (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
in
  make_simproc name lhs pred (thm name)
end;

val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'";
val eval_var_proc  =eval_fun "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'";
val eval_exprs_proc=eval_fun "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'";
val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=In1 Unit \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";
Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];

bind_thms ("XcptIs", sum3_instantiate eval.Xcpt);
AddSIs (halloc.Xcpt::eval.Xcpt::XcptIs);

fun split_solve_tac s = EVERY' [pair_tac s, case_tac "x = None" THEN_ALL_NEW 
 (force_tac (claset() addSEs eval_elim_cases addSIs eval.intrs, simpset()))];
fun split_prover n s = qed_goal n thy s (fn prems => 
	[cut_facts_tac prems 1, split_solve_tac "s" 1]);
split_prover "LitI" "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s";
split_prover "CondI" "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2";
split_prover "SkipI" "G\<turnstile>s \<midarrow>Skip\<rightarrow> s";
split_prover "ExprI" "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'";
split_prover "CompI" "\<lbrakk>G\<turnstile>s \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<rightarrow> s2";
split_prover "IfI" "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2";
split_prover"MethdI" "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'";
AddSIs[SkipI];

Goal "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2; \
\      C = target mode (snd s2) a' cT;\
\      G\<turnstile>init_lvars G C (mn,pTs) mode a' pvs s2 \<midarrow>Methd C (mn,pTs)-\<succ> v\<rightarrow> s3;\
\      s3' = restore_lvars s2 s3\<rbrakk> \<Longrightarrow> \
\      G\<turnstile>Norm s0 \<midarrow>{t,cT,mode}e..mn({pTs}ps)-\<succ>v\<rightarrow> s3'";
b y (datac eval.Call 1 THEN_ALL_NEW (TRY o ares_tac [refl])) 1;
b y Asm_simp_tac 1;
qed "eval_Call";

Goal "\<lbrakk>if inited C (globs s0) then s3 = Norm s0 else \
\     G\<turnstile>Norm (init_class_obj G C s0) \
\        \<midarrow>(if C = Object then Skip else init (fst (the (class G C))))\<rightarrow> s1 \<and> \
\     G\<turnstile>set_lvars empty s1 \<midarrow>(snd (snd (snd (snd (the (class G C))))))\<rightarrow> s2 \<and>\
\     s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow> \
\ G\<turnstile>Norm s0 \<midarrow>init C\<rightarrow> s3";
b y rtac (surjective_pairing5 RS eval.Init) 1;
b y Auto_tac;
qed "eval_Init";

Goal "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>init C\<rightarrow> s";
b y pair_tac "s" 1;
b y case_tac "x" 1;
b y  Safe_tac;
b y rtac eval_Init 1;
b y   Auto_tac;
qed "init_done";

qed_goal "SkipD" thy "\<And>X. G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
	(K [etac eval_cases 1 THEN Auto_tac]);
AddSDs [SkipD];
Goal "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')";
b y Auto_tac;
qed "Skip_eq";
Addsimps[Skip_eq];

(*unused*)
Goal 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<longrightarrow> (\<forall>C. t=In1r (init C) \<longrightarrow> locals (snd s) = locals (snd s'))";
b y (rtac eval_induct THEN_ALL_NEW full_simp_tac (simpset() 
	delsplits[split_if_asm,option.split_asm])) 1;
b y Auto_tac;
qed_spec_mp "init_retains_locals";

Goal "\<And>s s'. G\<turnstile>s \<midarrow>e\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s";
b y etac eval_cases 1 THEN Auto_tac;
qed "eval_no_xcpt_lemma";

Goal "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s') = (x = None \<and> G\<turnstile>Norm s \<midarrow>e\<succ>\<rightarrow> (w,Norm s'))";
b y Auto_tac;
b y ALLGOALS (ftac eval_no_xcpt_lemma) THEN Auto_tac;
qed "eval_no_xcpt";

local
  fun is_None (Const ("Option.option.None",_)) = true
    | is_None _ = false
  fun pred (t as (_ $ (Const ("Pair",_) $
     (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
in
  val eval_no_xcpt_proc = 
  make_simproc "eval_no_xcpt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred eval_no_xcpt
end;
Addsimprocs [eval_no_xcpt_proc];

Goal"G\<turnstile>s \<midarrow>e\<succ>\<rightarrow> (v,s') \<Longrightarrow> fst s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 e";
b y etac eval_cases 1 THEN Auto_tac;
qed "eval_xcpt_lemma";

Goal "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s') = \
\ (s'=(Some xc,s) \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,(Some xc,s)))";
b y Auto_tac;
b y ALLGOALS (ftac eval_xcpt_lemma) THEN Auto_tac;
qed "eval_xcpt";

local
  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
    | is_Some _ = false
  fun pred (_ $ (Const ("Pair",_) $
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
       x))) $ _ ) = is_Some x
in
  val eval_xcpt_proc = 
  make_simproc "eval_xcpt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred eval_xcpt
end;
Addsimprocs [eval_xcpt_proc];


qed_goal "halloc_xcpt" thy 
"\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)" (K [
	eresolve_tac halloc_elim_cases 1, Auto_tac]);
AddSDs [halloc_xcpt];

(*
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
*)

Goal "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')";
b y pair_tac "s" 1;
b y case_tac "x" 1;
b y  ALLGOALS (clarsimp_tac (claset(), simpset() addsimprocs [eval_expr_proc]));
b y etac eval.Methd 1;
b y dtac eval_xcpt_lemma 1;
b y Force_tac 1;
qed "eval_Methd";


section "univalent";

fun unique_tac thm = EVERY' [Clarsimp_tac, dtac thm, atac, K Auto_tac];

Goal "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as";
b y split_all_tac 1;
b y etac halloc.induct 1;
b y  auto_tac (claset() addSEs halloc_elim_cases, simpset() delsplits[split_if,split_if_asm]);
b y   ALLGOALS (dtac (trans RS sym) THEN' etac sym);
b y   Auto_tac;
qed_spec_mp "unique_halloc";

Goalw [univalent_def] "univalent {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}";
b y unique_tac unique_halloc 1;
qed "univalent_halloc";

Goal "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'";
b y split_all_tac 1;
b y etac sxalloc.induct 1;
b y   auto_tac (claset() addSEs sxalloc_elim_cases, simpset() delsplits[split_if,split_if_asm]);
b y   ALLGOALS (datac unique_halloc 1);
b y   Auto_tac;
qed_spec_mp "unique_sxalloc";

Goalw [univalent_def] "univalent {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}";
b y blast_tac (claset() addDs [unique_sxalloc]) 1;
qed "univalent_sxalloc";

val triv_refls = map (fn s => read_instantiate_sg (sign_of HOL.thy)
                 [("psi",s)] asm_rl) ["?s = ?s \<and> ?t = ?t","?t = ?t"];
fun fail_if_triv_refl i = dresolve_tac triv_refls i THEN_ELSE (no_tac, all_tac);
val spec_mp = EVERY'[dtac spec,mp_tac,fail_if_triv_refl];
val simp = asm_full_simp_tac (simpset() setmksimps (mksimps [("op &", [conjunct1,conjunct2]),("True", [])]) setloop (K no_tac) delsimps [split_paired_All]);
fun SOLVE1 tac = fn i => fn st => (tac i THEN COND (has_fewer_prems (nprems_of st)) all_tac no_tac) st;
val cs = claset() delrules [allE]
      addbefore ("spec_mp",spec_mp) 
      addbefore ("sym_trans", datac (sym RS trans) 1)
      addaltern ("simp_tac", SOLVE1 (simp_tac (simpset() delsplits[split_if,split_if_asm])));
val fast = full_simp_tac (HOL_basic_ss addsimps [if_def2]) THEN' 
           fast_tac (cs delrules [conjI,zero_var_indexes (Pair_eq RS iffD2)] 
                        addaltern ("simp", CHANGED o Full_simp_tac));
Goal "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)";
b y pair_tac "ws" 1;
b y rtac eval_induct 1; 
b y ALLGOALS (EVERY'[Clarify_tac, rotate_tac ~1, eresolve_tac eval_elim_cases]);
(* 27 subgoals *)
b y ALLGOALS (fn i => if i <= 19 then fast i else REPEAT (mp_tac i));
b y        EVERY'[spec_mp, simp, datac unique_halloc 1,fast] 1; (*NewC*)
b y       EVERY'[spec_mp, simp, spec_mp, simp, etac thin_rl] 1;
b y       EVERY'[datac unique_halloc 1, fast] 1; (* NewA *)
b y      EVERY'[simp, fast] 1; (*Init*)
b y     EVERY'[spec_mp,simp,spec_mp,simp] 1; (* Ass *)
b y    EVERY'[spec_mp, simp, datac unique_sxalloc 1, Clarify_tac] 1;
b y    asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1;
b y    Blast_tac 1; (* Try *)
b y   EVERY'[spec_mp, simp, spec_mp] 1;
b y   EVERY'[Clarify_tac, dtac sym, Asm_full_simp_tac] 1; (* FVar *)
b y  EVERY'[spec_mp, simp, spec_mp] 1;
b y  EVERY'[Clarify_tac, dtac sym, Asm_full_simp_tac] 1; (* AVar *)
b y EVERY'[simp, Clarify_tac, simp,
           spec_mp, Clarify_tac, spec_mp, fast] 1; (* Call *)
qed_spec_mp "unique_eval";

(* unused *)
Goalw [univalent_def] 
 "univalent {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}";
b y unique_tac unique_eval 1;
qed "univalent_eval";