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>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<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)))))";
b y Simp_tac 1;
b y Blast_tac 1;
qed "triple_valid2_def2";

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";


Goal "\<forall>s t n Y' s'. G\<turnstile>s\<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> t = c \<longrightarrow> \  
\ Ball A (triple_valid2 G n) \<longrightarrow> (\<forall>Y Z. 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\<succ> {Q}}";
b y simp_tac (simpset() addsimps [ax_valids2_def,triple_valid2_def2]) 1;
b y Clarsimp_tac 1;
qed "valids2_inductI";

Delsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];

Goal "\<lbrakk>G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'}}; \
\      G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)} .c. {P}}\<rbrakk> \<Longrightarrow> \
\      G,A|\<Turnstile>\<Colon>{ {P} .While(e) c. {(P'\<leftarrow>=False)\<down>=\<bullet>}}";
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 
     simp_tac (simpset_of Term.thy delsplits[split_if,split_if_asm])) 1;
b y  ALLGOALS Clarify_tac;
b y  thin_tac "G,A|\<Turnstile>\<Colon>{ {?P'} .c. {?P}}" 1;
b y  ALLGOALS (full_simp_tac (simpset() addsimps [ax_valids2_def,triple_valid2_def2]));
b y  EVERY'[smp_tac 1, smp_tac 3, Force_tac] 1;
(* 1 subgoal *)
b y EVERY'[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" 1;
b y  Clarsimp_tac 1;
b y  thin_tac "c = While(e) c \<longrightarrow> ?P" 1;
b y  case_tac "a" 1;
b y   ALLGOALS (asm_full_simp_tac (simpset() addsimps [imp_conjL]));
b y   ALLGOALS Blast_tac;
qed "Loop_sound";


Delsimps[subst_Bool_def2];
Goal "(!x. P) = P";
b y Simp_tac 1;
qed "all_empty";
val fullsimptac = full_simp_tac(simpset() delsimps [all_empty])
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]
 delsimps[all_empty]),
 Clarify_tac];
val sound_elim_tac = EVERY'[eresolve_tac evaln_elim_cases, 
        TRY o eresolve_tac wt_elim_cases,fullsimptac,Clarify_tac];
Goal "\<lbrakk>\<forall>v n. Ball A (triple_valid2 G n) \<longrightarrow> P v n; Ball A (triple_valid2 G n)\<rbrakk>\
\ \<Longrightarrow> P v n";
b y smp_tac 2 1;
b y atac 1;
qed "sound_valid2_lemma";
val sound_valid2_tac = REPEAT o FIRST'[smp_tac 1, datac sound_valid2_lemma 1];
val sound_forw_hyp_tac = EVERY'[smp_tac 3 ORELSE'
 EVERY'[dtac spec,dtac spec,dtac spec,etac impE, Fast_tac],
 fullsimptac, smp_tac 2,TRY o smp_tac 1,
 TRY o EVERY'[etac impE, TRY o rtac impI, atac ORELSE' etac exI, 
 fullsimptac, Clarify_tac, TRY o smp_tac 1]];

Goal "\<lbrakk>wf_prog G; G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q}}; \<forall>a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>Val a} ps\<doteq>\<succ> {R a}}; \
\    \<forall>a vs D l. G,A|\<Turnstile>\<Colon>{ {(R a\<leftarrow>Vals vs \<and>. \
\              (\<lambda>s. D = target mode (snd s) a cT \<and> l = locals (snd s)) ;. \
\              init_lvars G D (mn,pTs) mode a vs) \<and>. \
\              (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>D\<preceq>t)} \
\              Methd D (mn,pTs)-\<succ> {set_lvars l .; S}}\<rbrakk> \<Longrightarrow> \
\ G,A|\<Turnstile>\<Colon>{ {Normal P} {t,cT,mode}e..mn({pTs}ps)-\<succ> {S}}";
b y EVERY'[sound_prepare_tac, sound_elim_tac, sound_valid2_tac,
           rename_tac "x1 s1 x2 s2 ab bb v vs m pTsa pns rT"] 1;
b y smp_tac 5 1;
b y sound_forw_hyp_tac 1;
b y sound_forw_hyp_tac 1;
b y dtac max_spec2mheads 1;
b y EVERY'[dtac evaln_eval, datac eval_ts 3] 1;
b y EVERY'[dtac evaln_eval, fatac evals_ts 3] 1;
b y EVERY'[dtac spec,dtac spec,dtac spec,etac impE,rtac exI,blast_tac HOL_cs] 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). {Q}}; \
\ \<forall>l. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty} \
\           .ini. {set_lvars l .; R}}\<rbrakk> \<Longrightarrow> \
\     G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C)} .init C. {R}}";
b y EVERY'[sound_prepare_tac, sound_elim_tac, sound_valid2_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 HOL_cs] 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 Clarify_tac 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 "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l";
b y Fast_tac 1;
qed "all_conjunct2";

Goal "\<forall>a vs D l. (P' a vs D l \<and> P a vs D l) \<Longrightarrow> \<forall>a vs D l. P a vs D l";
b y Fast_tac 1;
qed "all4_conjunct2";


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 eresolve_tac [asm_rl, all_conjunct2, all4_conjunct2]));
b y(*empty*)COND (has_fewer_prems (30+1)) (ALLGOALS sound_prepare_tac) no_tac;
b y        Fast_tac 1; (* 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, ftac evaln_eval,  (* conseq *)
    case_tac "fst s" THEN_ALL_NEW 
    clarsimp_tac (claset(), simpset()addsimps[eval_type_sound RS conjunct1])] 1;
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 (fn i => if i < 0 then defer_tac i else sound_elim_tac i);
                                     (* LVar, Lit, Super, Nil, Skip *)
b y  ALLGOALS (asm_simp_tac (noAll_simpset()delsimps[all_empty])); (* 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_valid2_tac;
b y TRYALL sound_forw_hyp_tac; (* Cast, Inst, Acc, Expr *)
b y TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1, dtac spec], 
                   dtac conjunct2, smp_tac 1,
                   TRY o dres_inst_tac [("P","P'")] subst_Bool_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,Let_def]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 (claset(), simpset() addsimps [assign_conforms_def]) 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'[dtac spec,thin_All_tac, 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[subst_Bool_def2];

Goal "wf_prog G \<Longrightarrow> G,(A::'a triple set)|\<turnstile>(ts::'a triple set) \<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";