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