Eval.ML
Back to theory Eval
open Eval;
(*###*)
val split_beta2 = prove_goal Prod.thy "!!z. (%(x,y). P (x,y)) z = P z"
(K [split_all_tac 1, Simp_tac 1]);
qed_goal "split_eta3" Prod.thy "(%(x,y,z). f(x,y,z)) = f"
(K [rtac ext 1, split_all_tac 1, Simp_tac 1]);
val prems = goal thy "[| \
\ !!e xc s. P (Some xc,s) e arbitrary (Some xc,s); \
\ !!C a x s. new_Addr (heap s) = Some (a, x) ==> \
\ P (Norm s) (NewC C) (Addr a) (c_hupd[a|->init_Obj G C] (x, s)); \
\ !!T a e i' x x1 s0 s1. [|G|-Norm s0 -e:>i'-> (x1, s1); P (Norm s0) e i' (x1, s1); \
\ new_Addr (heap s1) = Some (a, x)|] \
\ ==> P (Norm s0) (New T[e]) (Addr a) (c_hupd[a|->init_Arr T (the_Intg i')] \
\(raise_if (the_Intg i' < $#0) NegArrSize (if x1 = None then x else x1), s1)); \
\ !!T e v x1 s0 s1. [|G|-Norm s0 -e:>v-> (x1, s1); P (Norm s0) e v (x1, s1)|] ==> \
\ P (Norm s0) (Cast T e) v (raise_if (~ (G,heap s1|-v fits T)) ClassCast x1,s1); \
\ !!v s. P (Norm s) (Lit v) v (Norm s); \
\ !!vn s. P (Norm s) (LAcc vn) (the (snd s vn)) (Norm s); \
\ !!e v vn x s0 s1. [|G|-Norm s0 -e:>v-> (x, s1); P (Norm s0) e v (x, s1)|] ==> \
\ P (Norm s0) (vn:=e) v (x, (if x = None then lupd[vn|->v] s1 else s1)); \
\ !!T a' e fn x1 s0 s1. [|G|-Norm s0 -e:>a'-> (x1,s1); P (Norm s0) e a' (x1,s1)|] ==> \
\ P (Norm s0) (e.{T}fn) (the (snd (the_Obj (heap s1 (the_Addr a'))) (fn, T))) \
\ ((np a') x1, s1); \
\ !!T a' c e1 e2 fn fs v x1 x2 s0 s1 s2. \
\ [|G|-Norm s0 -e1:>a'-> (x1, s1); P (Norm s0) e1 a' (x1, s1); \
\ G|-((np a') x1, s1) -e2:>v-> (x2, s2); P ((np a') x1, s1) e2 v (x2, s2); \
\ (c, fs) = the_Obj (heap s2 (the_Addr a'))|] ==> P (Norm s0) \
\ (e1.{T}fn:=e2) v (c_hupd[the_Addr a'|->Obj c (fs[(fn, T)|->v])] (x2, s2)); \
\ !!a' e1 e2 i' x2 s0 s1 s2. [|G|-Norm s0 -e1:>a'-> s1; P (Norm s0) e1 a' s1; \
\ G|-s1 -e2:>i'-> (x2, s2); P s1 e2 i' (x2, s2)|] ==> \
\ P (Norm s0) (AAcc e1 e2) (the (snd (the_Arr (heap s2 (the_Addr a'))) \
\ (the_Intg i'))) (raise_if (snd (the_Arr (heap s2 (the_Addr a'))) \
\ (the_Intg i') = None) IndOutBound (np a' x2), s2); \
\ !!T a' cs e1 e2 e3 i' v x3 s0 s1 s2 s3. \
\ [|G|-Norm s0 -e1:>a'-> s1; P (Norm s0) e1 a' s1; \
\ G|-s1 -e2:>i'-> s2 ; P s1 e2 i' s2; \
\ G|-s2 -e3:>v -> (x3, s3); P s2 e3 v (x3, s3); \
\ (T, cs) = the_Arr (heap s3 (the_Addr a'))|] ==> \
\ P (Norm s0) (e1[e2]:=e3) v (c_hupd[the_Addr a'|->Arr T (cs[the_Intg i'|->v])] \
\ (raise_if (~ G,heap s3|-v fits T) ArrStore \
\ (raise_if (cs (the_Intg i') = None) IndOutBound (np a' x3)), s3)); \
\ !!a' blk e h l lvars md mn p pT pn pv rT res v x2 x4 s0 s1 s3 s4. \
\ [|G|-Norm s0 -e:>a'-> s1 ; P (Norm s0) e a' s1; \
\ G|- s1 -p:>pv-> (x2, h, l); P s1 p pv (x2,h,l); \
\ (md, (pn, rT), lvars, blk, res) = \
\ the (cmethd G (fst (the_Obj (h (the_Addr a')))) (mn, pT)); \
\ G|-((np a') x2, h, init_vars lvars[This|->a'][pn|->pv]) -blk-> s3; \
\ Q ((np a') x2, h, init_vars lvars[This|->a'][pn|->pv]) blk s3; \
\ G|-s3 -res:>v-> (x4, s4); P s3 res v (x4, s4)|] ==> \
\ P (Norm s0) (e..mn{pT}(p)) v (x4, heap s4, l); \
\ !!c xc s. Q (Some xc,s) c (Some xc, s); \
\ !!a c x xn s0 s1. [|G|-Norm s0 -c-> (Some (SysXcpt xn), s1); \
\ Q (Norm s0) c (Some (SysXcpt xn), s1); \
\ new_Addr (heap s1) = Some (a, x)|] ==> \
\ Q (Norm s0) c (Some (XcptLoc a), hupd[a|->init_Obj G (SXcpt \
\ (if x = None then xn else OutOfMemory))] s1); \
\ !!s. Q (Norm s) Skip (Norm s); \
\ !!e v s0 s1. [|G|-Norm s0 -e:>v-> s1; P (Norm s0) e v s1|] ==> \
\ Q (Norm s0) (Expr e) s1; \
\ !!c1 c2 s0 s1 s2. [|G|-Norm s0 -c1-> s1; Q (Norm s0) c1 s1; \
\ G|- s1 -c2-> s2; Q s1 c2 s2|] ==> \
\ Q (Norm s0) (c1;; c2) s2; \
\ !!c1 c2 e v s0 s1 s2. [|G|-Norm s0 -e:>v-> s1; P (Norm s0) e v s1; \
\ G|- s1 -(if the_Bool v then c1 else c2)-> s2; \
\ Q s1 (if the_Bool v then c1 else c2) s2|] ==> \
\ Q (Norm s0) (If(e) c1 Else c2) s2; \
\ !!c e s0 s1. [|G|-Norm s0 -(If(e) (c;; While(e) c) Else Skip)-> s1; \
\ Q (Norm s0) (If(e) (c;; While(e) c) Else Skip) s1|] ==> \
\ Q (Norm s0) (While(e) c) s1; \
\ !!a' e x1 s0 s1. [|G|-Norm s0 -e:>a'-> (x1, s1); P (Norm s0) e a' (x1, s1)|] ==> \
\ Q (Norm s0) (Throw e) (if (np a') x1 = None then Some (XcptLoc (the_Addr a'))\
\ else (np a') x1, s1); \
\ !!a c1 c2 tn vn s0 s1 s2. [| \
\ G|-Norm s0 -c1-> (Some (XcptLoc a), s1); Q (Norm s0) c1 (Some (XcptLoc a), s1);\
\ G|-xcpt_ty s1 (XcptLoc a)<=:Class tn; \
\ G|-Norm (lupd[vn|->Addr a] s1) -c2-> s2; \
\ Q(Norm (lupd[vn|->Addr a] s1)) c2 s2|] ==> \
\ Q(Norm s0) (Try c1 Catch(tn vn) c2) s2; \
\ !!a c1 c2 tn vn x1 s0 s1. [|G|-Norm s0 -c1-> (x1, s1); Q (Norm s0) c1 (x1, s1); \
\ x1 = None | x1 = Some (XcptLoc a) & ~ G|-xcpt_ty s1 (XcptLoc a)<=:Class tn|] ==> \
\ Q (Norm s0) (Try c1 Catch(tn vn) c2) (x1, s1); \
\ !!c1 c2 x1 x2 s0 s1 s2. [|G|-Norm s0 -c1-> (x1, s1); Q (Norm s0) c1 (x1, s1); \
\ G|-Norm s1 -c2-> (x2, s2); Q (Norm s1) c2 (x2, s2)|] ==> \
\ Q (Norm s0) (c1 Finally c2) (if x1 ~= None & x2 = None then x1 else x2, s2) \
\ |] ==> (G|-s -e:>v-> s' --> P s e v s') & \
\ (G|-s -c -> s' --> Q s c s')";
b y pair_tac "s " 1 THEN pair_tac "y" 1;
b y pair_tac "s'" 1 THEN pair_tac "yb" 1;
b y rtac eval_exec.induct 1;
b y ALLGOALS (full_simp_tac (HOL_basic_ss addsimps [split_beta2,split_eta3])
THEN' (TRY o stac split_beta2));
(*####
goal Prod.thy "(%(y,z). P (x, y, z)) k";
b y simp_tac (HOL_basic_ss addsimps [split_beta2]) 1;
b y simp_tac (HOL_basic_ss addsimps [read_instantiate [("P","%k. P (x,k)")] split_beta2]) 1;
b y stac split_beta2 1;
*)
b y TRYALL (SELECT_GOAL (resolve_tac prems 1 THEN (ALLGOALS atac)));
b y dres_inst_tac [("P","%P. P c2 xba xca yca")] (split_beta2 RS subst) 1;
b y TRYALL (SELECT_GOAL (resolve_tac prems 1 THEN (ALLGOALS atac)));
val eval_exec_induct = result();
(*
G|-(x,(h,l)) -e:>v-> (x',(h',l'))) ==> l This = l' This"
G|-(x,(h,l)) -s -> (x',(h',l'))) ==> l This = l' This"
G|-s -e:>v-> s' --> G|-s -e:>v'-> s'' --> v' = v & s'' = s'"
G|-s -s0 -> s' --> G|-s -s0 -> s'' --> s'' = s'"
*)
val NewCI = prove_goal Eval.thy "!!X. [|new_Addr (heap s) = Some (a,None)|] ==>\
\ G|-Norm s -NewC C:>Addr a-> Norm (hupd[a|->init_Obj G C]s)" (K [
dtac eval_exec.NewC 1,
rewtac c_hupd_def,
Auto_tac]);
(*weak: middle case does not occur*)
val exec_SkipE = eval_exec.mk_cases stmt.distinct "G|-s -Skip-> t";
fun eval_induct_tac i = res_inst_tac [("Q2","%s c s'. True")]
(eval_exec_induct RS conjunct1 RS mp) i THEN atac (i+23);
fun exec_induct_tac i = res_inst_tac [("P2","%s e v s'. True")]
(eval_exec_induct RS conjunct2 RS mp) i THEN atac (i+23);
local
val exec_SkipD_lemma1 = prove_goal thy
"!!X. G|-s -c-> s' ==> fst s=None --> c=Skip --> fst s'= None" (K[
exec_induct_tac 1,
Auto_tac]);
val exec_SkipD_lemma2 = prove_goal thy "!!X. G|-Norm s -Skip-> (Some x',s') ==> R"
(K[dtac exec_SkipD_lemma1 1, Auto_tac]);
in
val exec_SkipD = prove_goal thy "!!X. G|-s -Skip-> s' ==> s' = s" (K [
etac exec_SkipE 1,
etac exec_SkipD_lemma2 2,
Auto_tac]);
end;
val eval_exec_no_xcpt = simplify (simpset()) (prove_goal thy
"!!s s'. (G|-s -e:>v-> s' --> fst s' = None --> fst s = None) & \
\ (G|-s -c -> s' --> fst s' = None --> fst s = None) " (K [
rtac eval_exec_induct 1,
rewtac c_hupd_def,
ALLGOALS Asm_full_simp_tac]));
val eval_no_xcpt = prove_goal thy "!!X. G|-(x,s) -e:>v-> (None,s') ==> x=None" (K [
dtac (eval_exec_no_xcpt RS conjunct1 RS mp) 1,
Auto_tac]);
(*unused*)
val exec_no_xcpt = prove_goal thy "!!X. G|-(x,s) -s0-> (None,s') ==> x=None" (K [
dtac (eval_exec_no_xcpt RS conjunct2 RS mp) 1,
Auto_tac]);
val eval_exec_xcpt = simplify (simpset()) (prove_goal thy
"!!X. (G|-s -e:>v-> s' --> fst s=Some xc --> fst s'=Some xc & snd s'=snd s) & \
\ (G|-s -c -> s' --> fst s=Some xc --> fst s'=Some xc & snd s'=snd s) " (K [
rtac eval_exec_induct 1,
rewtac c_hupd_def,
ALLGOALS Asm_full_simp_tac]));
val eval_xcpt = prove_goal thy
"!!X. G|-(Some xc,s) -e:>v-> (x',s') ==> x'=Some xc & s'=s" (K [
dtac (eval_exec_xcpt RS conjunct1 RS mp) 1,
Auto_tac]);
val exec_xcpt = prove_goal thy
"!!X. G|-(Some xc,s) -s0-> (x',s') ==> x'=Some xc & s'=s" (K [
dtac (eval_exec_xcpt RS conjunct2 RS mp) 1,
Auto_tac]);
AddSDs[eval_xcpt, exec_xcpt];
val try1_tac = force_tac (claset() addEs [eval_exec.Try1],simpset());
val try2_tac = force_tac (claset() addSDs[exec_SkipD]
addEs [eval_exec.Try2],simpset());
goal thy "!!s1 s2. [|G|-Norm s0 -c1-> (x1,s1); \
\ case x1 of None => (x1',s1') = (x1,s1) | Some xc => \
\ (case xc of XcptLoc a => (x1',s1') = (x1,s1) \
\ | SysXcpt xn => new_Addr (heap s1) = Some (a,x) & \
\ ((x1',s1') = (Some (XcptLoc a), \
\ hupd[a|->init_Obj G (SXcpt (if x = None then xn else OutOfMemory))] s1)));\
\ catch = (? a. x1'=Some (XcptLoc a) & G|-xcpt_ty s1' (XcptLoc a)<=:Class tn); \
\ G|-(if catch then None else x1', \
\ if catch then lupd[vn|->Addr (the_XcptLoc (the x1'))]s1' else s1') \
\ -(if catch then c2 else Skip)-> s2|] ==> \
\ G|-Norm s0 -(Try c1 Catch(tn vn) c2)-> s2";
b y asm_full_simp_tac (simpset()setloop(split_asm_tac[split_option_case_asm]))1;
b y try2_tac 1;
b y rotate_tac 1 1 THEN dtac sym 1;
b y asm_full_simp_tac HOL_basic_ss 1;
b y case_tac "catch" 1;
b y ALLGOALS (asm_full_simp_tac (simpset() setloop (K no_tac)));
b y ALLGOALS Clarify_tac;
b y ALLGOALS (asm_full_simp_tac (simpset() setloop
(split_asm_tac[split_xcpt_case_asm])));
b y try1_tac 1;
b y Asm_full_simp_tac 1;
b y dtac eval_exec.SXcpt 1;
b y Force_tac 1;
b y Simp_tac 1;
b y try1_tac 1;
b y dtac eval_exec.SXcpt 1;
b y Force_tac 1;
b y Simp_tac 1;
b y try1_tac 1;
b y try2_tac 1;
b y Clarify_tac 1;
b y dtac eval_exec.SXcpt 1;
b y Force_tac 1;
b y Simp_tac 1;
b y try2_tac 1;
qed "Try_intro";
Delsimps [update_def2];
Unify.search_bound := 30;
Unify.trace_bound := 30;
(*
claset_ref():=claset() delSWrapper "split_all_tac";
goal thy "!!X. wf_prog G ==> \
\ (G|-s -e:>v-> s' --> \
\ (!L. s ::<=:(G,L) --> (!T. (G,L)|-e ::T --> \
\ heap(snd s)<=|heap(snd s') & s'::<=:(G,L) & \
\ (fst s'=None --> G,heap(snd s')|-v::<=:T)))) \
\ & \
\ (G|-s -c -> s' --> \
\ (!L. s ::<=:(G,L) --> (G,L)|-c::<> --> \
\ heap(snd s)<=|heap(snd s') & s'::<=:(G,L)))";
b y rtac eval_exec_induct 1;
(* several simplifications, SXcptE, SXcptS, Skip *)
b y ALLGOALS (full_simp_tac (simpset() setloop (K no_tac)));
b y ALLGOALS Clarify_tac;
val forward_hyp_tac = EVERY' [dtac spec, mp_tac,
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)];
(* 20 SXcpt *)
b y forward_hyp_tac 12;
b y SELECT_GOAL (etac SXcpt_type_sound 1 THEN ALLGOALS Fast_tac) 12;
val typD_tac = EVERY' [eresolve_tac (ty_exprs_elim_cases@wt_stmts_elim_cases),
full_simp_tac (simpset()setloop(K no_tac)), Clarify_tac];
b y ALLGOALS typD_tac;
(* 19 Try2 *)
b y Fast_tac 18;
(* for LAss *)
b y typD_tac 6;
(* for FAss *)
b y typD_tac 8;
(* for AAss *)
b y typD_tac 10;
(* Level 10 *)
*)
goal thy "!!X. wf_prog G ==> \
\ (G|-(x,(h,l)) -e:>v-> (x',(h',l')) --> \
\ (!L. (x ,h ,l )::<=:(G,L) --> (!T. (G,L)|-e ::T --> \
\ h<=|h' & (x',h',l')::<=:(G,L) & (x'=None --> G,h'|-v::<=:T)))) \
\ & \
\ (G|-(x,(h,l)) -c -> (x',(h',l')) --> \
\ (!L. (x ,h ,l )::<=:(G,L) --> (G,L)|-c::<> --> \
\ h<=|h' & (x',h',l')::<=:(G,L)))";
b y rtac eval_exec.induct 1;
(* several simplifications, SXcptE, SXcptS, Skip *)
b y ALLGOALS (full_simp_tac (simpset() setloop split_all_tac));
b y ALLGOALS Clarify_tac;
val forward_hyp_tac = EVERY' [dtac spec, mp_tac,
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)];
(* 20 SXcpt *)
b y forward_hyp_tac 12;
b y SELECT_GOAL (etac SXcpt_type_sound 1 THEN ALLGOALS atac) 12;
val typD_tac = EVERY' [eresolve_tac (ty_exprs_elim_cases@wt_stmts_elim_cases),
full_simp_tac (simpset()setloop(K no_tac)), Clarify_tac];
b y ALLGOALS typD_tac;
(* 19 Try2 *)
b y Fast_tac 18;
(* for LAss *)
b y typD_tac 6;
(* for FAss *)
b y typD_tac 8;
(* for AAss *)
b y typD_tac 10;
(* Level 10 *)
(* 18 NewC *)
b y SELECT_GOAL (etac NewC_type_sound 1 THEN ALLGOALS atac) 1;
b y ALLGOALS (TRY o forward_hyp_tac);
(* 17 NewA *)
b y Full_simp_tac 1;
b y Clarify_tac 1;
b y SELECT_GOAL (etac NewA_type_sound 1 THEN ALLGOALS atac) 1;
b y SELECT_GOAL Auto_tac 1;
(* 16 Cast *)
b y Asm_simp_tac 1;
b y SELECT_GOAL (etac Cast_conf 1 THEN ALLGOALS atac) 1;
(* 15 Lit *)
b y etac conf_litval 1;
(* 14 LAcc *)
b y SELECT_GOAL (etac LAcc_conf 1 THEN ALLGOALS atac) 1;
(* 13 LAss *)
b y Asm_full_simp_tac 1;
b y Clarify_tac 1;
b y Asm_full_simp_tac 1;
b y SELECT_GOAL (etac LAss_conf 1 THEN ALLGOALS atac) 1;
(* 12 FAcc *)
b y Asm_full_simp_tac 1;
b y Clarify_tac 1;
b y Asm_full_simp_tac 1;
b y SELECT_GOAL (etac FAcc_conf 1 THEN ALLGOALS atac) 1;
(* 11 FAss *)
b y forward_hyp_tac 1;
b y case_tac "x2 = None" 1;
b y rotate_tac ~1 2 THEN Asm_full_simp_tac 2; (*###conditional rewrite on c_hupd*)
b y fast_tac (claset() delrules (map make_elim [non_np_ObjD, non_np_ArrD])) 2;
b y Asm_full_simp_tac 1;
b y Clarify_tac 1;
b y dtac eval_no_xcpt 1;
b y SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1;
(* 10 Expr *)
b y Fast_tac 4;
(* 9 ;; *)
b y Fast_tac 4;
(* 8 if *)
b y SELECT_GOAL Auto_tac 4;
(* 7 while *)
b y fast_tac (claset() addIs [wt_stmts.Cond, wt_stmts.Comp]
addEs [wt_stmts.Loop]) 4;
(* Level 40 *)
(* 6 AAcc *)
b y forward_hyp_tac 1;
b y rtac conjI 1;
b y fast_tac (claset() delrules (map make_elim [non_np_ObjD, non_np_ArrD])) 1;
b y optionE_tac "x2" 1;
b y Asm_full_simp_tac 2;
b y dtac eval_no_xcpt 1;
b y hyp_subst_tac 1;
b y Asm_full_simp_tac 1;
b y fast_tac (HOL_cs addEs [AAcc_conf]) 1;
(* 5 AAss *)
b y forward_hyp_tac 1;
b y forward_hyp_tac 1;
b y optionE_tac "x3" 1;
b y Asm_full_simp_tac 2;
b y Clarify_tac 2;
b y Asm_full_simp_tac 2;
b y fast_tac (claset() delrules (map make_elim [non_np_ObjD, non_np_ArrD]))2;
b y dtac eval_no_xcpt 1;
b y hyp_subst_tac 1;
b y dtac eval_no_xcpt 1;
b y Asm_full_simp_tac 1;
b y SELECT_GOAL (etac AAss_type_sound 1 THEN ALLGOALS atac) 1;
(* Level 61 *)
(* 4 Call *)
b y forward_hyp_tac 1;
b y optionE_tac "x2" 1;
b y Asm_full_simp_tac 2;
b y Fast_tac 2;
b y dtac eval_no_xcpt 1;
b y Clarify_tac 1;
b y Full_simp_tac 1;
b y case_tac "a' = Null" 1;
b y Asm_full_simp_tac 1;
b y Fast_tac 1;
b y SELECT_GOAL (etac Call_type_sound 1 THEN ALLGOALS atac) 1;
(* 3 Throw *)
b y Asm_full_simp_tac 1;
b y SELECT_GOAL (safe_tac (claset() delrules (map make_elim [non_np_ObjD, non_np_ArrD]))) 1;
b y SELECT_GOAL (etac Throw_conforms 1 THEN ALLGOALS atac) 1;
(* Level 75 *)
(* 2 Try1#### *)
b y EVERY' [dtac spec, etac impE] 1;
b y fast_tac (claset()addEs [deallocL_conforms]) 2;
b y rtac allocL_conforms 1;
b y etac conforms_NormI 1;
b y rtac non_np_conf 1;
b y etac conforms_XcptLocD 1 THEN Fast_tac 1;
b y Simp_tac 1;
b y Simp_tac 1;
(* 1 Fin *)
b y EVERY' [dtac spec, etac impE] 1;
b y etac conforms_NormI 1;
b y auto_tac (claset() addEs [conforms_xhext],simpset());
qed "eval_exec_type_sound";
Addsimps [update_def2];
qed_goal "eval_type_sound" thy
"!!s s'. [|E = (G,L); wf_prog G; G|-s -e:>v -> (x',s'); \
\ s::<=:E; E|-e::T|] ==> (x',s')::<=:E & (x'=None --> G,heap s'|-v::<=:T)" (K [
split_all_tac 1,
Simp_tac 1,
dtac (eval_exec_type_sound RS conjunct1 RS mp) 1,
atac 1,
Fast_tac 1]);
qed_goal "exec_type_sound" thy
"!!s s'. [|E = (G,L); wf_prog G; G|-s -s0-> s'; \
\ s::<=:E; E|-s0::<>|] ==> s'::<=:E" (K [
split_all_tac 1,
Simp_tac 1,
dtac (eval_exec_type_sound RS conjunct2 RS mp) 1,
atac 1,
Fast_tac 1]);
goal thy "!!X. [|E = (G,L); wf_prog G; G|-s -e:>a'-> Norm s'; a' ~= Null;\
\ s::<=:E; E|-e::RefT T; mheads G T sig ~= {}|] ==> \
\ cmethd G (fst (the_Obj (heap s' (the_Addr a')))) sig ~= None";
b y dtac eval_type_sound 1 THEN REPEAT(atac 1);
b y dtac (not_empty RS iffD1) 1;
b y rtac (not_None_eq RS iffD2) 1;
b y Clarify_tac 1;
b y forward_tac [widen_methd] 1;
b y atac 1;
b y Fast_tac 2;
b y dtac non_npD 1;
b y Auto_tac;
b y etac mheads_ArrayD 1 THEN REPEAT(atac 1);
qed "all_methods_understood";