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