src/HOL/Bali/AxSound.thy
author wenzelm
Mon Jan 28 18:50:23 2002 +0100 (2002-01-28)
changeset 12857 a4386cc9b1c3
parent 12854 00d4a435777f
child 12859 f63315dfffd4
permissions -rw-r--r--
tuned header;
     1 (*  Title:      HOL/Bali/AxSound.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 header {* Soundness proof for Axiomatic semantics of Java expressions and 
     7           statements
     8        *}
     9 
    10 
    11 
    12 theory AxSound = AxSem:
    13 
    14 section "validity"
    15 
    16 consts
    17 
    18  triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
    19                                                 (   "_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
    20     ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
    21                                                 ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
    22 
    23 defs  triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
    24  \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) 
    25  \<longrightarrow> (\<forall>T C. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<longrightarrow>
    26  (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L))))"
    27 
    28 defs  ax_valids2_def:    "G,A|\<Turnstile>\<Colon>ts \<equiv>  \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)"
    29 
    30 lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} =  
    31  (\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow>  
    32   (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T C. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<longrightarrow>  
    33   Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))"
    34 apply (unfold triple_valid2_def)
    35 apply (simp (no_asm) add: split_paired_All)
    36 apply blast
    37 done
    38 
    39 lemma triple_valid2_eq [rule_format (no_asm)]: 
    40   "wf_prog G ==> triple_valid2 G = triple_valid G"
    41 apply (rule ext)
    42 apply (rule ext)
    43 apply (rule triple.induct)
    44 apply (simp (no_asm) add: triple_valid_def2 triple_valid2_def2)
    45 apply (rule iffI)
    46 apply  fast
    47 apply clarify
    48 apply (tactic "smp_tac 3 1")
    49 apply (case_tac "normal s")
    50 apply  clarsimp
    51 apply  (blast dest: evaln_eval eval_type_sound [THEN conjunct1])
    52 apply clarsimp
    53 done
    54 
    55 lemma ax_valids2_eq: "wf_prog G \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts = G,A|\<Turnstile>ts"
    56 apply (unfold ax_valids_def ax_valids2_def)
    57 apply (force simp add: triple_valid2_eq)
    58 done
    59 
    60 lemma triple_valid2_Suc [rule_format (no_asm)]: "G\<Turnstile>Suc n\<Colon>t \<longrightarrow> G\<Turnstile>n\<Colon>t"
    61 apply (induct_tac "t")
    62 apply (subst triple_valid2_def2)
    63 apply (subst triple_valid2_def2)
    64 apply (fast intro: evaln_nonstrict_Suc)
    65 done
    66 
    67 lemma Methd_triple_valid2_0: "G\<Turnstile>0\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
    68 apply (clarsimp elim!: evaln_elim_cases simp add: triple_valid2_def2)
    69 done
    70 
    71 lemma Methd_triple_valid2_SucI: 
    72 "\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk> 
    73   \<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
    74 apply (simp (no_asm_use) add: triple_valid2_def2)
    75 apply (intro strip, tactic "smp_tac 3 1", clarify)
    76 apply (erule wt_elim_cases, erule evaln_elim_cases)
    77 apply (unfold body_def Let_def)
    78 apply clarsimp
    79 apply blast
    80 done
    81 
    82 lemma triples_valid2_Suc: 
    83  "Ball ts (triple_valid2 G (Suc n)) \<Longrightarrow> Ball ts (triple_valid2 G n)"
    84 apply (fast intro: triple_valid2_Suc)
    85 done
    86 
    87 lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)";
    88 oops
    89 
    90 
    91 section "soundness"
    92 
    93 lemma Methd_sound: 
    94 "\<lbrakk>G,A\<union>  {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow> 
    95   G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
    96 apply (unfold ax_valids2_def mtriples_def)
    97 apply (rule allI)
    98 apply (induct_tac "n")
    99 apply  (clarify, tactic {* pair_tac "x" 1 *}, simp (no_asm))
   100 apply  (fast intro: Methd_triple_valid2_0)
   101 apply (clarify, tactic {* pair_tac "xa" 1 *}, simp (no_asm))
   102 apply (drule triples_valid2_Suc)
   103 apply (erule (1) notE impE)
   104 apply (drule_tac x = na in spec)
   105 apply (tactic {* auto_tac (claset() addSIs [thm "Methd_triple_valid2_SucI"],
   106    simpset() addsimps [ball_Un] addloop ("split_all_tac", split_all_tac)) *})
   107 done
   108 
   109 
   110 lemma valids2_inductI: "\<forall>s t n Y' s'. G\<turnstile>s\<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> t = c \<longrightarrow>    
   111   Ball A (triple_valid2 G n) \<longrightarrow> (\<forall>Y Z. P Y s Z \<longrightarrow>  
   112   (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T C. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<longrightarrow>  
   113   Q Y' s' Z \<and> s'\<Colon>\<preceq>(G, L)))) \<Longrightarrow>  
   114   G,A|\<Turnstile>\<Colon>{ {P} c\<succ> {Q}}"
   115 apply (simp (no_asm) add: ax_valids2_def triple_valid2_def2)
   116 apply clarsimp
   117 done
   118 
   119 ML_setup {*
   120 Delsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc]
   121 *}
   122 
   123 lemma Loop_sound: "\<lbrakk>G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'}};  
   124        G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}}\<rbrakk> \<Longrightarrow>  
   125        G,A|\<Turnstile>\<Colon>{ {P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}}"
   126 apply (rule valids2_inductI)
   127 apply ((rule allI)+, rule impI, tactic {* pair_tac "s" 1*}, tactic {* pair_tac "s'" 1*})
   128 apply (erule evaln.induct)
   129 apply  simp_all (* takes half a minute *)
   130 apply  clarify
   131 apply  (erule_tac V = "G,A|\<Turnstile>\<Colon>{ {?P'} .c. {?P}}" in thin_rl)
   132 apply  (simp_all (no_asm_use) add: ax_valids2_def triple_valid2_def2)
   133 apply  (tactic "smp_tac 1 1", tactic "smp_tac 3 1", force)
   134 apply clarify
   135 apply (rule wt_elim_cases, assumption)
   136 apply (tactic "smp_tac 1 1", tactic "smp_tac 1 1", tactic "smp_tac 3 1", 
   137        tactic "smp_tac 2 1", tactic "smp_tac 1 1")
   138 apply (erule impE,simp (no_asm),blast)
   139 apply (simp add: imp_conjL split_tupled_all split_paired_All)
   140 apply (case_tac "the_Bool b")
   141 apply  clarsimp
   142 apply  (case_tac "a")
   143 apply (simp_all)
   144 apply clarsimp
   145 apply  (erule_tac V = "c = l\<bullet> While(e) c \<longrightarrow> ?P" in thin_rl)
   146 apply (blast intro: conforms_absorb)
   147 apply blast+
   148 done
   149 
   150 declare subst_Bool_def2 [simp del]
   151 lemma all_empty: "(!x. P) = P"
   152 by simp
   153 lemma sound_valid2_lemma: 
   154 "\<lbrakk>\<forall>v n. Ball A (triple_valid2 G n) \<longrightarrow> P v n; Ball A (triple_valid2 G n)\<rbrakk>
   155  \<Longrightarrow>P v n"
   156 by blast
   157 ML {*
   158 val fullsimptac = full_simp_tac(simpset() delsimps [thm "all_empty"]);
   159 val sound_prepare_tac = EVERY'[REPEAT o thin_tac "?x \<in> ax_derivs G",
   160  full_simp_tac (simpset()addsimps[thm "ax_valids2_def",thm "triple_valid2_def2",
   161                                   thm "imp_conjL"] delsimps[thm "all_empty"]),
   162  Clarify_tac];
   163 val sound_elim_tac = EVERY'[eresolve_tac (thms "evaln_elim_cases"), 
   164         TRY o eresolve_tac (thms "wt_elim_cases"), fullsimptac, Clarify_tac];
   165 val sound_valid2_tac = REPEAT o FIRST'[smp_tac 1, 
   166                   datac (thm "sound_valid2_lemma") 1];
   167 val sound_forw_hyp_tac = 
   168  EVERY'[smp_tac 3 
   169           ORELSE' EVERY'[dtac spec,dtac spec, dtac spec,etac impE, Fast_tac] 
   170           ORELSE' EVERY'[dtac spec,dtac spec,etac impE, Fast_tac],
   171         fullsimptac, 
   172         smp_tac 2,TRY o smp_tac 1,
   173         TRY o EVERY'[etac impE, TRY o rtac impI, 
   174         atac ORELSE' (EVERY' [REPEAT o rtac exI,Blast_tac]),
   175         fullsimptac, Clarify_tac, TRY o smp_tac 1]]
   176 *}
   177 (* ### rtac conjI,rtac HOL.refl *)
   178 lemma Call_sound: 
   179 "\<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}};
   180   \<forall>a vs invC declC l. G,A|\<Turnstile>\<Colon>{ {(R a\<leftarrow>Vals vs \<and>.  
   181    (\<lambda>s. declC = invocation_declclass 
   182                     G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and>
   183          invC = invocation_class mode (store s) a statT \<and>
   184             l = locals (store s)) ;.  
   185    init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>.  
   186    (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}  
   187    Methd declC \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}}\<rbrakk> \<Longrightarrow>  
   188   G,A|\<Turnstile>\<Colon>{ {Normal P} {statT,mode}e\<cdot>mn({pTs}ps)-\<succ> {S}}"
   189 apply (tactic "EVERY'[sound_prepare_tac, sound_elim_tac, sound_valid2_tac] 1")
   190 apply (rename_tac x1 s1 x2 s2 ab bb v vs m pTsa statDeclC)
   191 apply (tactic "smp_tac 6 1")
   192 apply (tactic "sound_forw_hyp_tac 1")
   193 apply (tactic "sound_forw_hyp_tac 1")
   194 apply (drule max_spec2mheads)
   195 apply (drule evaln_eval, drule (3) eval_ts)
   196 apply (drule evaln_eval, frule (3) evals_ts)
   197 apply (drule spec,erule impE,rule exI, blast)
   198 (* apply (drule spec,drule spec,drule spec,erule impE,rule exI,blast) *)
   199 apply (case_tac "if static m then x2 else (np a') x2")
   200 defer 1
   201 apply  (rename_tac x, subgoal_tac "(Some x, s2)\<Colon>\<preceq>(G, L)" (* used two times *))
   202 prefer 2 
   203 apply   (force split add: split_if_asm)
   204 apply  (simp del: if_raise_if_None)
   205 apply  (tactic "smp_tac 2 1")
   206 apply (simp only: init_lvars_def2 invmode_Static_eq)
   207 apply (clarsimp simp del: resTy_mthd)
   208 apply  (drule spec,erule swap,erule conforms_set_locals [OF _ lconf_empty])
   209 apply clarsimp
   210 apply (drule Null_staticD)
   211 apply (drule eval_gext', drule (1) conf_gext, frule (3) DynT_propI)
   212 apply (erule impE) apply blast
   213 apply (subgoal_tac 
   214  "G\<turnstile>invmode (mhd (statDeclC,m)) e
   215      \<rightarrow>invocation_class (invmode m e) s2 a' statT\<preceq>statT")
   216 defer   apply simp
   217 apply (drule (3) DynT_mheadsD,simp,simp)
   218 apply (clarify, drule wf_mdeclD1, clarify)
   219 apply (frule ty_expr_is_type) apply simp
   220 apply (subgoal_tac "invmode (mhd (statDeclC,m)) e = IntVir \<longrightarrow> a' \<noteq> Null")
   221 defer   apply simp
   222 apply (frule (2) wt_MethdI)
   223 apply clarify
   224 apply (drule (2) conforms_init_lvars)
   225 apply   (simp) 
   226 apply   (assumption)+
   227 apply   simp
   228 apply   (assumption)+
   229 apply   (rule impI) apply simp
   230 apply   simp
   231 apply   simp
   232 apply   (rule Ball_weaken)
   233 apply     assumption
   234 apply     (force simp add: is_acc_type_def)
   235 apply (tactic "smp_tac 2 1")
   236 apply simp
   237 apply (tactic "smp_tac 1 1")
   238 apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl) 
   239 apply (erule impE)
   240 apply   (rule exI)+ 
   241 apply   (subgoal_tac "is_static dm = (static m)") 
   242 prefer 2  apply (simp add: member_is_static_simp)
   243 apply   (simp only: )
   244 apply   (simp only: sig.simps)
   245 apply (force dest!: evaln_eval eval_gext' elim: conforms_return 
   246              del: impCE simp add: init_lvars_def2)
   247 done
   248 
   249 lemma Init_sound: "\<lbrakk>wf_prog G; the (class G C) = c;  
   250       G,A|\<Turnstile>\<Colon>{ {Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}  
   251              .(if C = Object then Skip else Init (super c)). {Q}};  
   252   \<forall>l. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}  
   253             .init c. {set_lvars l .; R}}\<rbrakk> \<Longrightarrow>  
   254       G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}}"
   255 apply (tactic "EVERY'[sound_prepare_tac, sound_elim_tac,sound_valid2_tac] 1")
   256 apply (tactic {* instantiate_tac [("l24","\<lambda> n Y Z sa Y' s' L y a b aa ba ab bb. locals b")]*})
   257 apply (clarsimp simp add: split_paired_Ex)
   258 apply (drule spec, drule spec, drule spec, erule impE)
   259 apply  (erule_tac V = "All ?P" in thin_rl, fast)
   260 apply clarsimp
   261 apply (tactic "smp_tac 2 1", drule spec, erule impE, 
   262        erule (3) conforms_init_class_obj)
   263 apply (drule (1) wf_prog_cdecl)
   264 apply (erule impE, rule exI,erule_tac V = "All ?P" in thin_rl,
   265        force dest: wf_cdecl_supD split add: split_if simp add: is_acc_class_def)
   266 apply clarify
   267 apply (drule spec)
   268 apply (drule spec)
   269 apply (drule spec)
   270 apply  (erule impE)
   271 apply ( fast)
   272 apply (simp (no_asm_use) del: empty_def2)
   273 apply (tactic "smp_tac 2 1")
   274 apply (drule spec, erule impE, erule conforms_set_locals, rule lconf_empty)
   275 apply (erule impE,rule impI,rule exI, erule wf_cdecl_wt_init)
   276 apply clarsimp
   277 apply (erule (1) conforms_return, force dest: evaln_eval eval_gext')
   278 done
   279 
   280 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
   281 by fast
   282 
   283 lemma all4_conjunct2: 
   284   "\<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"
   285 by fast
   286 
   287 lemmas sound_lemmas = Init_sound Loop_sound Methd_sound
   288 
   289 lemma ax_sound2: "wf_prog G \<Longrightarrow> G,A|\<turnstile>ts \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts"
   290 apply (erule ax_derivs.induct)
   291 prefer 20 (* Call *)
   292 apply (erule (1) Call_sound) apply simp apply force apply force 
   293 
   294 apply (tactic {* TRYALL (eresolve_tac (thms "sound_lemmas") THEN_ALL_NEW 
   295     eresolve_tac [asm_rl, thm "all_conjunct2", thm "all4_conjunct2"]) *})
   296 
   297 apply(tactic "COND (has_fewer_prems(30+3)) (ALLGOALS sound_prepare_tac) no_tac")
   298 
   299                (*empty*)
   300 apply        fast (* insert *)
   301 apply       fast (* asm *)
   302 (*apply    fast *) (* cut *)
   303 apply     fast (* weaken *)
   304 apply    (tactic "smp_tac 3 1", clarify, tactic "smp_tac 1 1", frule evaln_eval,
   305 (* conseq *)case_tac"fst s",clarsimp simp add: eval_type_sound [THEN conjunct1],
   306 clarsimp)
   307 apply   (simp (no_asm_use) add: type_ok_def, drule evaln_eval,fast) (* hazard *)
   308 apply  force (* Abrupt *)
   309 
   310 (* 25 subgoals *)
   311 apply (tactic {* ALLGOALS sound_elim_tac *})(* LVar, Lit, Super, Nil, Skip,Do *)
   312 apply (tactic {* ALLGOALS (asm_simp_tac (noAll_simpset() 
   313                           delsimps [thm "all_empty"])) *})    (* Done *)
   314 (* for FVar *)
   315 apply (frule wf_ws_prog) 
   316 apply (frule ty_expr_is_type [THEN type_is_class, 
   317                               THEN accfield_declC_is_class])
   318 apply (simp,simp,simp) 
   319 apply (frule_tac [4] wt_init_comp_ty) (* for NewA*)
   320 apply (tactic "ALLGOALS sound_valid2_tac")
   321 apply (tactic "TRYALL sound_forw_hyp_tac") (* Cast, Inst, Acc, Expr *)
   322 apply (tactic {* TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1, 
   323   dtac spec], dtac conjunct2, smp_tac 1, 
   324   TRY o dres_inst_tac [("P","P'")] (thm "subst_Bool_the_BoolI")]) *})
   325 apply (frule_tac [14] x = x1 in conforms_NormI)  (* for Fin *)
   326 
   327 
   328 (* 15 subgoals *)
   329 (* FVar *)
   330 apply (tactic "sound_forw_hyp_tac 1")
   331 apply (clarsimp simp add: fvar_def2 Let_def split add: split_if_asm)
   332 
   333 (* AVar *)
   334 (*
   335 apply (drule spec, drule spec, erule impE, fast)
   336 apply (simp)
   337 apply (tactic "smp_tac 2 1")
   338 apply (tactic "smp_tac 1 1")
   339 apply (erule impE)
   340 apply (rule impI)
   341 apply (rule exI)+
   342 apply blast
   343 apply (clarsimp simp add: avar_def2)
   344 *)
   345 apply (tactic "sound_forw_hyp_tac 1")
   346 apply (clarsimp simp add: avar_def2)
   347 
   348 (* NewC *)
   349 apply (clarsimp simp add: is_acc_class_def)
   350 apply (erule (1) halloc_conforms, simp, simp)
   351 
   352 (* NewA *)
   353 apply (tactic "sound_forw_hyp_tac 1")
   354 apply (rule conjI,blast)
   355 apply (erule (1) halloc_conforms, simp, simp, simp add: is_acc_type_def)
   356 
   357 (* Ass *)
   358 apply (tactic "sound_forw_hyp_tac 1")
   359 apply (case_tac "aa")
   360 prefer 2
   361 apply  clarsimp
   362 apply (drule evaln_eval)+
   363 apply (frule (3) eval_ts)
   364 apply clarsimp
   365 apply (frule (3) evar_ts [THEN conjunct2])
   366 apply (frule wf_ws_prog)
   367 apply (drule (2) conf_widen)
   368 apply (drule_tac "s1.0" = b in eval_gext')
   369 apply (clarsimp simp add: assign_conforms_def)
   370 
   371 (* Cond *)
   372 
   373 apply (tactic "smp_tac 3 1") apply (tactic "smp_tac 2 1") 
   374 apply (tactic "smp_tac 1 1") apply (erule impE) 
   375 apply (rule impI,rule exI) 
   376 apply (rule_tac x = "if the_Bool b then T1 else T2" in exI)
   377 apply (force split add: split_if)
   378 apply assumption
   379 
   380 (* Body *)
   381 apply (tactic "sound_forw_hyp_tac 1")
   382 apply (rule conforms_absorb,assumption)
   383 
   384 (* Lab *)
   385 apply (tactic "sound_forw_hyp_tac 1")
   386 apply (rule conforms_absorb,assumption)
   387 
   388 (* If *)
   389 apply (tactic "sound_forw_hyp_tac 1")
   390 apply (tactic "sound_forw_hyp_tac 1")
   391 apply (force split add: split_if)
   392 
   393 (* Throw *)
   394 apply (drule evaln_eval, drule (3) eval_ts)
   395 apply clarsimp
   396 apply (drule (3) Throw_lemma)
   397 apply clarsimp
   398 
   399 (* Try *)
   400 apply (frule (1) sxalloc_type_sound)
   401 apply (erule sxalloc_elim_cases2)
   402 apply  (tactic "smp_tac 3 1")
   403 apply  (clarsimp split add: option.split_asm)
   404 apply (clarsimp split add: option.split_asm)
   405 apply (tactic "smp_tac 1 1")
   406 apply (simp only: split add: split_if_asm)
   407 prefer 2
   408 apply  (tactic "smp_tac 3 1", erule_tac V = "All ?P" in thin_rl, clarsimp)
   409 apply (drule spec, erule_tac V = "All ?P" in thin_rl, drule spec, drule spec, 
   410        erule impE, force)
   411 apply (frule (2) Try_lemma)
   412 apply clarsimp
   413 apply (fast elim!: conforms_deallocL)
   414 
   415 (* Fin *)
   416 apply (tactic "sound_forw_hyp_tac 1")
   417 apply (case_tac "x1", force)
   418 apply clarsimp
   419 apply (drule evaln_eval, drule (4) Fin_lemma)
   420 done
   421 
   422 
   423 
   424 declare subst_Bool_def2 [simp]
   425 
   426 theorem ax_sound: 
   427  "wf_prog G \<Longrightarrow> G,(A::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> G,A|\<Turnstile>ts"
   428 apply (subst ax_valids2_eq [symmetric])
   429 apply  assumption
   430 apply (erule (1) ax_sound2)
   431 done
   432 
   433 
   434 end