File AxSound.ML

open AxSound;

section "validity";

Goalw [triple_valid2_def] "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} = \
\(\<forall>Y s Z. P (Y,s) Z \<longrightarrow> (\<forall>w s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s')\<longrightarrow> \
\ (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T. (normal s \<longrightarrow> (G,L)\<turnstile>t\<Colon>T) \<longrightarrow> \
\ Q (res t w Y,s') Z \<and> s'\<Colon>\<preceq>(G,L)))))";
b y Simp_tac 1;
b y Blast_tac 1;
qed "triple_valid2_def2";

Goal "\<forall>s t n w s' Y Z. G\<turnstile>s\<midarrow>t\<succ>\<midarrow>n\<rightarrow>(w,s') \<longrightarrow> t=In1r c \<longrightarrow> \  
\ Ball A (triple_valid2 G n) \<longrightarrow> \
\ P (Y,s) Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T. (normal s \<longrightarrow> (G,L)\<turnstile>t\<Colon>T) \<longrightarrow> \
\ Q (Y,s') Z \<and> s'\<Colon>\<preceq>(G, L)))  \<Longrightarrow> G,A|\<Turnstile>\<Colon>{ {P} .c. {Q}}";
b y simp_tac (simpset() addsimps [ax_valids2_def,triple_valid2_def2]) 1;
b y Clarsimp_tac 1;
qed "valids2_inductI";

Goal "wf_prog G \<Longrightarrow> triple_valid2 G = triple_valid G";
b y rtac ext 1;
b y rtac ext 1;
b y rtac triple.induct 1;
b y simp_tac (simpset() addsimps [triple_valid_def2, triple_valid2_def2]) 1;
b y rtac iffI 1;
b y  Fast_tac 1;
b y Clarify_tac 1;
b y smp_tac 3 1;
b y (case_tac "normal s" THEN_ALL_NEW Clarsimp_tac) 1;
b y blast_tac (claset() addDs [evaln_eval, eval_type_sound RS conjunct1]) 1;
qed_spec_mp "triple_valid2_eq";

Goalw [ax_valids_def, ax_valids2_def] "wf_prog G \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts = G,A|\<Turnstile>ts";
b y force_tac (claset(), simpset() addsimps [triple_valid2_eq]) 1;
qed "ax_valids2_eq";

Goal "G\<Turnstile>Suc n\<Colon>t \<longrightarrow> G\<Turnstile>n\<Colon>t";
b y induct_tac "t" 1;
b y stac triple_valid2_def2 1;
b y stac triple_valid2_def2 1;
by (fast_tac (claset() addIs [evaln_nonstrict_Suc]) 1);
qed_spec_mp "triple_valid2_Suc";

Goal "G\<Turnstile>0\<Colon>{Normal P} Methd C sig-\<succ> {Q}";
by (clarsimp_tac (claset() addSEs evaln_elim_cases, 
	simpset() addsimps [triple_valid2_def2]) 1);
qed "Methd_triple_valid2_0";

Goal 
"\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk>\
\ \<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-\<succ> {Q}";
b y full_simp_tac (simpset() addsimps [triple_valid2_def2]) 1;
b y EVERY'[strip_tac, smp_tac 3, Clarify_tac] 1;
b y EVERY'[eresolve_tac wt_elim_cases, eresolve_tac evaln_elim_cases] 1;
b y rewrite_goals_tac [body_def, Let_def];
b y Clarsimp_tac 1;
b y Blast_tac 1;
qed "Methd_triple_valid2_SucI";

Goal "Ball ts (triple_valid2 G (Suc n)) \<Longrightarrow> Ball ts (triple_valid2 G n)";
by (fast_tac (claset() addIs [triple_valid2_Suc]) 1);
qed "triples_valid2_Suc";

(*Goalw [ax_valids_def] "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)";*)

Goalw [ax_valids2_def, mtriples_def] 
"\<lbrakk>G,A\<union>  {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>\
\ G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}";
b y rtac allI 1;
b y induct_tac "n" 1;
b y  ALLGOALS (EVERY'[Clarify_tac, pair_tac "xa", Simp_tac]);
b y  fast_tac (claset() addIs [Methd_triple_valid2_0]) 1;
b y dtac triples_valid2_Suc 1;
b y mp_tac 1;
b y dres_inst_tac [("x","na")] spec 1;
b y auto_tac (claset() addSIs [Methd_triple_valid2_SucI],
	simpset() addsimps[ball_Un] addloop ("split_all_tac", split_all_tac));
qed "Methd_sound";


Delsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];


Goal "\<forall>s t n w s' Y Z. G\<turnstile>s\<midarrow>t\<succ>\<midarrow>n\<rightarrow>(w,s') \<longrightarrow> t=In1r c \<longrightarrow> \  
\ Ball A (triple_valid2 G n) \<longrightarrow> \
\ P (Y,s) Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T. (normal s \<longrightarrow> (G,L)\<turnstile>t\<Colon>T) \<longrightarrow> \
\ Q (Y,s') Z \<and> s'\<Colon>\<preceq>(G, L))) \<Longrightarrow> G,A|\<Turnstile>\<Colon>{ {P} .c. {Q}}";
b y simp_tac (simpset() addsimps [ax_valids2_def,triple_valid2_def2]) 1;
b y Clarsimp_tac 1;
qed "valids2_inductI";

Goal "\<lbrakk>G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'}}; \
\      G,A|\<Turnstile>\<Colon>{ {P'\<up>#Bool=True} .c. {P}}\<rbrakk> \<Longrightarrow> \
\      G,A|\<Turnstile>\<Colon>{ {P} .While(e) c. {P'\<up>#Bool=False}}";
b y rtac valids2_inductI 1;
b y EVERY'[REPEAT o rtac allI, rtac impI, pair_tac "s", pair_tac "s'"] 1;
b y (etac evaln.induct THEN_ALL_NEW Clarify_tac) 1;
(* 10 subgoals *)
b y ALLGOALS Full_simp_tac;
b y  ALLGOALS (full_simp_tac (simpset() addsimps [ax_valids2_def,triple_valid2_def2]));
b y  EVERY'[smp_tac 1,smp_tac 1,smp_tac 3,thin_All_tac,Full_simp_tac,Fast_tac]1;
(* 1 subgoal *)
b y EVERY'[etac conjE, resolve_tac wt_elim_cases, atac] 1;
b y EVERY'[smp_tac 1, smp_tac 1, smp_tac 3, smp_tac 2, smp_tac 1] 1;
b y EVERY'[etac impE, Simp_tac, etac exI] 1;
b y (case_tac "the_Bool b" THEN_ALL_NEW Clarsimp_tac) 1;
b y thin_tac "c = While(e) c \<longrightarrow> ?P" 1;
b y ALLGOALS Blast_tac;
qed "Loop_sound";

Delsimps[Bool_assn_def2];
val sound_prepare_tac = EVERY'[REPEAT o thin_tac "?x \<in> ax_derivs G",
 full_simp_tac (simpset()addsimps[ax_valids2_def,triple_valid2_def2,imp_conjL]),
 Clarify_tac, REPEAT o smp_tac 1];
val sound_elim_tac = EVERY'[eresolve_tac evaln_elim_cases, 
	TRY o eresolve_tac wt_elim_cases,Full_simp_tac,Clarify_tac];
val sound_forw_hyp_tac = EVERY'[smp_tac 3 ORELSE'
 EVERY'[dtac spec,dtac spec,dtac spec,etac impE, Fast_tac],
 Full_simp_tac, smp_tac 2,TRY o smp_tac 1,
 TRY o EVERY'[etac impE, TRY o rtac impI, atac ORELSE' etac exI, 
 Full_simp_tac, Clarify_tac, TRY o smp_tac 1]];

Goal "\<lbrakk>wf_prog G; G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q}}; \
\    G,A|\<Turnstile>\<Colon>{ {Q} ps\<doteq>\<succ> {\<lambda>Vals:pvs#Val:a#. \<lambda>s: let D = target mode s a cT \
\ in init_lvars G D (mn,pTs) mode a pvs .; R\<up>#DynT D\<up>#Lcls (locals s)}};\
\    \<forall>D. P1 D \<and> \
\  G,A|\<Turnstile>\<Colon>{ {R\<up>#DynT D \<and>. (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>D\<preceq>t)} Methd D (mn, pTs)-\<succ> \
\            {\<lambda>Val:v#Lcls:l#. set_lvars l .; S\<up>#Val v}}\<rbrakk> \<Longrightarrow> \
\ G,A|\<Turnstile>\<Colon>{ {Normal P} {t,cT,mode}e..mn({pTs}ps)-\<succ> {S}}";
b y sound_prepare_tac 1;
b y EVERY'[sound_elim_tac, rename_tac "x2 s2 ab bb v vs m pTsa pns rT"] 1;
b y sound_forw_hyp_tac 1;
b y sound_forw_hyp_tac 1;
b y dtac max_spec2mheads 1;
b y rewtac Let_def;
b y EVERY'[dtac evaln_eval, datac eval_ts 3] 1;
b y EVERY'[dtac evaln_eval, fatac evals_ts 3] 1;
b y REPEAT(EVERY'[dres_inst_tac [("x","target (invmode m e) s2 a' cT")]
	spec, dtac conjunct2, smp_tac 1] 1);
b y Clarsimp_noAllAsm_tac 1;
b y smp_tac 3 1;
b y EVERY'[case_tac "if m then x2 else (np a') x2", defer_tac] 1;
b y  EVERY'[rename_tac "x", subgoal_tac "(Some x, s2)\<Colon>\<preceq>(G, L)"] 1; (* used two times *)
b y   force_tac(claset(),simpset()addsplits[split_if_asm]) 2;
b y  asm_full_simp_tac (simpset() delsimps [if_raise_if_None]) 1;
b y  smp_tac 2 1;
b y  clarsimp_tac (claset(),noAll_simpset() addsimps[init_lvars_def2]) 1;
b y  EVERY'[dtac spec, etac swap, etac (lconf_empty RSN (2,conforms_set_locals))] 1;
b y Clarsimp_noAllAsm_tac 1;
b y dtac Null_staticD 1;
b y EVERY'[dtac eval_gext', datac conf_gext 1, fatac DynT_propI 3] 1;
b y EVERY'[mp_tac, smp_tac 2] 1;
b y EVERY'[exhaust_cmethd_tac "the (cmethd G (target (invmode m e) s2 a' cT) (mn, pTs))", Clarsimp_noAllAsm_tac] 1;
b y EVERY'[datac DynT_mheadsD 4, rtac refl] 1;
b y EVERY'[Clarify_tac, dtac wf_mdeclD1, Clarify_tac] 1;
b y EVERY'[datac conforms_init_lvars 10, smp_tac 1, Clarsimp_noAllAsm_tac] 1;
b y EVERY'[thin_tac "?P \<longrightarrow> ?Q", thin_tac "?P \<longrightarrow> ?Q", etac impE,
           force_tac (claset() addSDs [wt_MethdI], simpset())] 1;
b y force_tac (claset() addSDs [evaln_eval,eval_gext'] 
	addEs[conforms_return] delrules [impCE],simpset()addsimps[init_lvars_def2]) 1;
qed "Call_sound";

Goal "\<lbrakk>wf_prog G; the (class G C) = (sc, si, fs, ms, ini); \
\ G,A|\<Turnstile>\<Colon>{ {Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))} \
\        .(if C = Object then Skip else init sc). {\<lambda>s: Q\<up>#Lcls (locals s)}}; \
\ G,A|\<Turnstile>\<Colon>{ {Q ;. set_lvars empty} .ini. {\<lambda>Lcls:l#. set_lvars l .; R}}\<rbrakk> \<Longrightarrow> \
\ G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C)} .init C. {R}}";
b y sound_prepare_tac 1;
b y sound_elim_tac 1;
b y clarsimp_tac (claset(), noAll_simpset() addsimps [split_paired_Ex]) 1;
b y EVERY'[dtac spec,dtac spec,dtac spec,etac impE, thin_All_tac, Fast_tac] 1;
b y Clarsimp_noAllAsm_tac 1;
b y EVERY'[smp_tac 2, dtac spec, etac impE, eatac conforms_init_class_obj 3] 1;
b y datac wf_prog_cdecl 1 1;
b y EVERY'[etac impE, thin_All_tac, force_tac (claset() addDs [wf_cdecl_supD], 
	noAll_simpset()addsplits[split_if])] 1;
b y EVERY'[dtac spec, dtac spec, dtac spec, etac impE, Fast_tac] 1;
b y EVERY'[full_simp_tac (simpset() delsimps [empty_def2]), Clarify_tac] 1;
b y smp_tac 2 1;
b y EVERY'[dtac spec, etac impE, etac conforms_set_locals, rtac lconf_empty] 1; 
b y EVERY'[etac impE, rtac impI, etac wf_cdecl_wt_init] 1;
b y Clarsimp_tac 1;
b y EVERY'[eatac conforms_return 1, 
   force_tac (claset() addDs [evaln_eval,eval_gext'],simpset())] 1;
qed "Init_sound";

Goal "wf_prog G \<Longrightarrow> G,A|\<turnstile>ts \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts";
b y etac ax_derivs.induct 1;
b y (TRYALL (eresolve_tac[Call_sound,Init_sound,Loop_sound,Methd_sound]
		THEN_ALL_NEW atac));
b y         COND (has_fewer_prems (30+1)) (ALLGOALS sound_prepare_tac) no_tac;
            (* empty,insert *)
b y       Fast_tac 1; (* asm *)
(*b y    Fast_tac 1;*) (* cut *)
b y     Fast_tac 1; (* weaken *)
b y    EVERY'[smp_tac 3, Clarify_tac, smp_tac 1,
	      case_tac "fst s" THEN_ALL_NEW Clarsimp_noAllAsm_tac,
	      ftac evaln_eval, datac (eval_type_sound RS conjunct1) 3, 
              Blast_tac, Blast_tac] 1; (* conseq *)
b y   EVERY'[full_simp_tac (simpset() addsimps [type_ok_def]),
		dtac evaln_eval, Fast_tac] 1; (* hazard *)
b y  Force_tac 1; (* Xcpt *)

(* 23 subgoals *)
b y ALLGOALS sound_elim_tac;
b y ALLGOALS (asm_simp_tac (noAll_simpset())); (* LVar, Lit, Super, Nil, Skip, ??? *)
b y clarsimp_tac (claset(), simpset() addsplits[option.split_asm]) 17;(* Done *)
b y EVERY'[ftac wf_ws_prog, fatac 
 (ty_expr_is_type RS type_is_class RS cfield_defpl_is_class) 3] 1;(* for FVar *)
b y ftac wt_init_comp_ty 4;(* for NewA*)
b y ALLGOALS sound_forw_hyp_tac; (* Cast, Inst, Acc, Expr *)
b y TRYALL (EVERY'[dtac spec, dtac conjunct2, smp_tac 1,
	dres_inst_tac [("P","P'")] Bool_assn_the_BoolI]);
b y forw_inst_tac [("x","x1")] conforms_NormI 13; (* for Fin *)
b y ALLGOALS (FIRST'[sound_forw_hyp_tac, (* Cons, Comp *)
		smp_tac 2(*for NewC*), K all_tac]);
(* 11 subgoals *)

(* FVar *)
b y clarsimp_tac(claset(),simpset()addsimps[fvar_def2]addsplits[split_if_asm])1;

(* AVar *)
b y clarsimp_tac(claset(),simpset()addsimps[avar_def2])1;

(* NewC *)
b y Asm_simp_tac 1;
b y (eatac halloc_conforms 2 THEN_ALL_NEW Asm_simp_tac) 1;

(* NewA *)
b y Asm_simp_tac 1;
b y (eatac halloc_conforms 1 THEN_ALL_NEW Asm_simp_tac) 1;

(* Ass *)
b y case_tac "aa" 1;
b y  Clarsimp_tac 2;
b y REPEAT (dtac evaln_eval 1);
b y fatac eval_ts 3 1;
b y Clarsimp_tac 1;
b y EVERY'[fatac (evar_ts RS conjunct2) 3] 1;
b y ftac wf_ws_prog 1;
b y datac conf_widen 2 1;
b y dres_inst_tac [("s1.0","b")] eval_gext' 1;
b y Clarsimp_tac 1;

(* Cond *)
b y EVERY'[etac impE, rtac impI, res_inst_tac [("x","if the_Bool b then T1 else T2")] exI, force_tac (claset(), simpset() addsplits [split_if])] 1;
b y atac 1;

(* Body *)
b y sound_forw_hyp_tac 1;

(* If *)
b y force_tac (claset(), simpset() addsplits [split_if]) 1;

(* Throw *)
b y EVERY'[dtac evaln_eval, datac eval_ts 3] 1;
b y Clarsimp_tac 1;
b y datac Throw_lemma 3 1;
b y Clarsimp_tac 1;

(* Try *)
b y fatac sxalloc_type_sound 1 1;
b y etac sxalloc_elim_cases2 1;
b y  smp_tac 3 1;
b y  clarsimp_tac (claset(), noAll_simpset() addsplits[option.split_asm]) 1;
b y clarsimp_tac (claset(), noAll_simpset()addsplits[option.split_asm]) 1;
b y smp_tac 1 1;
b y split_asm_tac [split_if_asm] 1;
b y  EVERY'[smp_tac 3, thin_All_tac, Clarsimp_tac] 2;
b y EVERY'[thin_All_tac, dtac spec,dtac spec,dtac spec, etac impE, Force_tac] 1;
b y fatac Try_lemma 2 1;
b y Clarsimp_tac 1;
b y fast_tac (claset()addSEs [conforms_deallocL]) 1;

(* Fin *)
b y EVERY'[dtac evaln_eval, datac Fin_lemma 3, Force_tac] 1;
qed "ax_sound2";
Addsimps[Bool_assn_def2];

Goal "wf_prog G \<Longrightarrow> G,A|\<turnstile>ts \<Longrightarrow> G,A|\<Turnstile>ts";
b y stac (ax_valids2_eq RS sym) 1;
b y  atac 1;
b y eatac ax_sound2 1 1;
qed "ax_sound";