src/HOL/Bali/AxSound.thy
changeset 13337 f75dfc606ac7
parent 12937 0c4fd7529467
child 13384 a34e38154413
     1.1 --- a/src/HOL/Bali/AxSound.thy	Wed Jul 10 14:51:18 2002 +0200
     1.2 +++ b/src/HOL/Bali/AxSound.thy	Wed Jul 10 15:07:02 2002 +0200
     1.3 @@ -313,17 +313,18 @@
     1.4    "\<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"
     1.5  by fast
     1.6  
     1.7 +
     1.8  lemmas sound_lemmas = Init_sound Loop_sound Methd_sound
     1.9  
    1.10  lemma ax_sound2: "wf_prog G \<Longrightarrow> G,A|\<turnstile>ts \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts"
    1.11  apply (erule ax_derivs.induct)
    1.12 -prefer 20 (* Call *)
    1.13 +prefer 22 (* Call *)
    1.14  apply (erule (1) Call_sound) apply simp apply force apply force 
    1.15  
    1.16  apply (tactic {* TRYALL (eresolve_tac (thms "sound_lemmas") THEN_ALL_NEW 
    1.17      eresolve_tac [asm_rl, thm "all_conjunct2", thm "all4_conjunct2"]) *})
    1.18  
    1.19 -apply(tactic "COND (has_fewer_prems(30+3)) (ALLGOALS sound_prepare_tac) no_tac")
    1.20 +apply(tactic "COND (has_fewer_prems(30+9)) (ALLGOALS sound_prepare_tac) no_tac")
    1.21  
    1.22                 (*empty*)
    1.23  apply        fast (* insert *)
    1.24 @@ -336,7 +337,13 @@
    1.25  apply   (simp (no_asm_use) add: type_ok_def,fast)(* hazard *)
    1.26  apply  force (* Abrupt *)
    1.27  
    1.28 -(* 25 subgoals *)
    1.29 +prefer 28 apply (simp add: evaln_InsInitV)
    1.30 +prefer 28 apply (simp add: evaln_InsInitE)
    1.31 +prefer 28 apply (simp add: evaln_Callee)
    1.32 +prefer 28 apply (simp add: evaln_FinA)
    1.33 +
    1.34 +(* 27 subgoals *)
    1.35 +apply (tactic {* sound_elim_tac 1 *})
    1.36  apply (tactic {* ALLGOALS sound_elim_tac *})(* LVar, Lit, Super, Nil, Skip,Do *)
    1.37  apply (tactic {* ALLGOALS (asm_simp_tac (noAll_simpset() 
    1.38                            delsimps [thm "all_empty"])) *})    (* Done *)
    1.39 @@ -347,12 +354,11 @@
    1.40  apply (simp,simp,simp) 
    1.41  apply (frule_tac [4] wt_init_comp_ty) (* for NewA*)
    1.42  apply (tactic "ALLGOALS sound_valid2_tac")
    1.43 -apply (tactic "TRYALL sound_forw_hyp_tac") (* Cast, Inst, Acc, Expr *)
    1.44 +apply (tactic "TRYALL sound_forw_hyp_tac") (* UnOp, Cast, Inst, Acc, Expr *)
    1.45  apply (tactic {* TRYALL (EVERY'[dtac spec, TRY o EVERY'[rotate_tac ~1, 
    1.46    dtac spec], dtac conjunct2, smp_tac 1, 
    1.47    TRY o dres_inst_tac [("P","P'")] (thm "subst_Bool_the_BoolI")]) *})
    1.48 -apply (frule_tac [14] x = x1 in conforms_NormI)  (* for Fin *)
    1.49 -
    1.50 +apply (frule_tac [15] x = x1 in conforms_NormI)  (* for Fin *)
    1.51  
    1.52  (* 15 subgoals *)
    1.53  (* FVar *)
    1.54 @@ -383,6 +389,9 @@
    1.55  apply (rule conjI,blast)
    1.56  apply (erule (1) halloc_conforms, simp, simp, simp add: is_acc_type_def)
    1.57  
    1.58 +(* BinOp *)
    1.59 +apply (tactic "sound_forw_hyp_tac 1")
    1.60 +
    1.61  (* Ass *)
    1.62  apply (tactic "sound_forw_hyp_tac 1")
    1.63  apply (case_tac "aa")