src/HOL/MicroJava/J/JTypeSafe.thy
author wenzelm
Thu, 28 Feb 2013 13:24:51 +0100
changeset 51304 0e71a248cacb
parent 45133 2214ba5bdfff
child 51686 532e0ac5a66d
permissions -rw-r--r--
marginalized historic strip_tac;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/MicroJava/J/JTypeSafe.thy
41589
bbd861837ebc tuned headers;
wenzelm
parents: 39159
diff changeset
     2
    Author:     David von Oheimb, Technische Universitaet Muenchen
11070
cc421547e744 improved document (added headers etc)
oheimb
parents: 11026
diff changeset
     3
*)
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     4
12911
704713ca07ea new document
kleing
parents: 12888
diff changeset
     5
header {* \isaheader{Type Safety Proof} *}
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     6
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14142
diff changeset
     7
theory JTypeSafe imports Eval Conform begin
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
     8
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
     9
declare split_beta [simp]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    10
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    11
lemma NewC_conforms: 
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
    12
"[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==>  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
    13
  (x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    14
apply( erule conforms_upd_obj)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    15
apply(  unfold oconf_def)
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    16
apply(  auto dest!: fields_is_type simp add: wf_prog_ws_prog)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    17
done
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    18
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    19
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    20
lemma Cast_conf: 
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    21
 "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>CC; G\<turnstile>CC \<preceq>? Class D; cast_ok G D h v|]  
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    22
  ==> G,h\<turnstile>v::\<preceq>Class D"
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    23
apply (case_tac "CC")
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    24
apply simp
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    25
apply (case_tac "ref_ty")
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    26
apply (clarsimp simp add: conf_def)
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    27
apply simp
23757
087b0a241557 - Renamed inductive2 to inductive
berghofe
parents: 22271
diff changeset
    28
apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    29
apply (rule conf_widen, assumption+) apply (erule widen.subcls)
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    30
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    31
apply (unfold cast_ok_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    32
apply( case_tac "v = Null")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    33
apply(  simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    34
apply(  clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    35
apply( drule (1) non_npD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    36
apply( auto intro!: conf_AddrI simp add: obj_ty_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    37
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    38
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
    39
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    40
lemma FAcc_type_sound: 
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
    41
"[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT);  
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    42
  x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==>  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    43
  G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    44
apply( drule np_NoneD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    45
apply( erule conjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    46
apply( erule (1) notE impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    47
apply( drule non_np_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    48
apply   auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    49
apply( drule conforms_heapD [THEN hconfD])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    50
apply(  assumption)
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    51
apply (frule wf_prog_ws_prog)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    52
apply( drule (2) widen_cfs_fields)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    53
apply( drule (1) oconf_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    54
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    55
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    56
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    57
lemma FAss_type_sound: 
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    58
 "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a);  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    59
    (G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft;  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    60
    (G, lT)\<turnstile>aa::Class C;  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    61
    field (G,C) fn = Some (fd, ft); h''\<le>|h';  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    62
    x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h;  
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
    63
    Norm (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==>  
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    64
  h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and>   
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
    65
  Norm(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and>   
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    66
  G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    67
apply( drule np_NoneD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    68
apply( erule conjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    69
apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    70
apply( drule non_np_objD)
12951
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
    71
apply(  assumption)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    72
apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    73
apply( simp (no_asm_use))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    74
apply( frule (1) hext_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    75
apply( erule exE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    76
apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    77
apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    78
apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    79
apply(  fast elim: hext_trans hext_upd_obj)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    80
apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    81
prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    82
apply(  fast elim: conf_upd_obj [THEN iffD2])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    83
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    84
apply( rule conforms_upd_obj)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    85
apply   auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    86
apply(  rule_tac [2] hextI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    87
prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    88
apply(  force)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    89
apply( rule oconf_hext)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    90
apply(  erule_tac [2] hext_upd_obj)
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
    91
apply (frule wf_prog_ws_prog)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    92
apply( drule (2) widen_cfs_fields)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    93
apply( rule oconf_obj [THEN iffD2])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    94
apply( simp (no_asm))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    95
apply( intro strip)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    96
apply( case_tac "(aaa, b) = (fn, fd)")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    97
apply(  simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    98
apply(  fast intro: conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
    99
apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   100
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   101
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   102
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   103
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   104
lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   105
   list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;  
12888
f6c1e7306c40 nodups -> distinct
nipkow
parents: 12517
diff changeset
   106
  length pTs' = length pns; distinct pns;  
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   107
  Ball (set lvars) (split (\<lambda>vn. is_type G))  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   108
  |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   109
apply (unfold wf_mhead_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   110
apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   111
apply( rule lconf_ext_list)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   112
apply(    rule Ball_set_table [THEN lconf_init_vars])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   113
apply(    force)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   114
apply(   assumption)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   115
apply(  assumption)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   116
apply( erule (2) conf_list_gext_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   117
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   118
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   119
lemma Call_type_sound: 
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   120
 "[| wf_java_prog G; a' \<noteq> Null; Norm (h, l)::\<preceq>(G, lT); class G C = Some y;  
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   121
     max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h;  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   122
     list_all2 (conf G h) pvs pTsa; 
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   123
     (md, rT, pns, lvars, blk, res) =  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   124
               the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); 
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   125
  \<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   126
  (G, lT)\<turnstile>blk\<surd> -->  h\<le>|xi \<and>  (xcptb, xi, xl)::\<preceq>(G, lT);  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   127
  \<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   128
          xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   129
  G,xh\<turnstile>a'::\<preceq> Class C
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   130
  |] ==>  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   131
  xc\<le>|h' \<and> (x',(h', l))::\<preceq>(G, lT) \<and>  (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   132
apply( drule max_spec2mheads)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   133
apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   134
apply( drule (2) non_np_objD')
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   135
apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   136
apply( frule (1) hext_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   137
apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   138
apply( drule (3) Call_lemma)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   139
apply( clarsimp simp add: wf_java_mdecl_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   140
apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   141
apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac 2")
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   142
apply(  rule conformsI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   143
apply(   erule conforms_heapD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   144
apply(  rule lconf_ext)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   145
apply(   force elim!: Call_lemma2)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   146
apply(  erule conf_hext, erule (1) conf_obj_AddrI)
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   147
apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) 
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   148
apply (simp add: conforms_def)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   149
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   150
apply( erule conjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   151
apply( drule spec, erule (1) impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   152
apply( drule spec, erule (1) impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   153
apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   154
apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   155
apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   156
apply(  fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   157
apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   158
apply(  rule_tac [2] impI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   159
apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   160
apply(  frule_tac [2] conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   161
apply(    tactic "assume_tac 4")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   162
apply(   tactic "assume_tac 2")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   163
prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   164
apply(  fast elim!: widen_trans)
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   165
apply (rule conforms_xcpt_change)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   166
apply( rule conforms_hext) apply assumption
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   167
apply(  erule (1) hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   168
apply( erule conforms_heapD)
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   169
apply (simp add: conforms_def)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   170
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   171
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   172
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   173
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   174
declare split_if [split del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   175
declare fun_upd_apply [simp del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   176
declare fun_upd_same [simp]
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   177
declare wf_prog_ws_prog [simp]
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   178
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   179
ML{*
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   180
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   181
  (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   182
*}
24178
4ff1dc2aa18d turned Unify flags into configuration options (global only);
wenzelm
parents: 23894
diff changeset
   183
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   184
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   185
theorem eval_evals_exec_type_sound: 
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   186
"wf_java_prog G ==>  
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   187
  (G\<turnstile>(x,(h,l)) -e  \<succ>v  -> (x', (h',l')) -->  
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   188
      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e  :: T -->  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   189
      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v  ::\<preceq> T )))) \<and>  
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   190
  (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->  
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   191
      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   192
      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and>  
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   193
  (G\<turnstile>(x,(h,l)) -c       -> (x', (h',l')) -->  
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   194
      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) -->       (G,lT)\<turnstile>c  \<surd> -->  
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   195
      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT)))"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   196
apply( rule eval_evals_exec_induct)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   197
apply( unfold c_hupd_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   198
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   199
-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   200
apply( simp_all)
51304
0e71a248cacb marginalized historic strip_tac;
wenzelm
parents: 45133
diff changeset
   201
apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 33954
diff changeset
   202
apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 27215
diff changeset
   203
                 THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   204
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   205
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   206
-- "Level 7"
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   207
-- "15 NewC"
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   208
apply (drule sym)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   209
apply( drule new_AddrD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   210
apply( erule disjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   211
prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   212
apply(  simp (no_asm_simp))
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   213
apply (rule conforms_xcpt_change, assumption) 
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   214
apply (simp (no_asm_simp) add: xconf_def)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   215
apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   216
apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   217
apply(  force elim!: NewC_conforms)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   218
apply( rule conf_obj_AddrI)
33954
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 32367
diff changeset
   219
apply(  rule_tac [2] rtrancl.rtrancl_refl)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   220
apply( simp (no_asm))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   221
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   222
-- "for Cast"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   223
defer 1
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   224
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   225
-- "14 Lit"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   226
apply( erule conf_litval)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   227
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   228
-- "13 BinOp"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   229
apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   230
apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   231
apply( rule conjI, erule (1) hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   232
apply( erule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   233
apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   234
apply( drule eval_no_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   235
apply( simp split add: binop.split)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   236
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   237
-- "12 LAcc"
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   238
apply simp
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   239
apply( fast elim: conforms_localD [THEN lconfD])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   240
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   241
-- "for FAss"
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 33954
diff changeset
   242
apply( tactic {* EVERY'[eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 23757
diff changeset
   243
       THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   244
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   245
-- "for if"
45133
2214ba5bdfff modernized structure Induct_Tacs;
wenzelm
parents: 41589
diff changeset
   246
apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 23757
diff changeset
   247
  (asm_full_simp_tac @{simpset})) 7*})
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   248
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   249
apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   250
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   251
-- "11+1 if"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   252
prefer 7
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   253
apply(  fast intro: hext_trans)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   254
prefer 7
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   255
apply(  fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   256
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   257
-- "10 Expr"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   258
prefer 6
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   259
apply( fast)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   260
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   261
-- "9 ???"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   262
apply( simp_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   263
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   264
-- "8 Cast"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   265
prefer 8
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   266
apply (rule conjI)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   267
  apply (fast intro: conforms_xcpt_change xconf_raise_if)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   268
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   269
  apply clarify
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   270
  apply (drule raise_if_NoneD)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   271
  apply (clarsimp)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   272
  apply (rule Cast_conf)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   273
  apply assumption+
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   274
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   275
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   276
-- "7 LAss"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   277
apply (fold fun_upd_def)
39159
0dec18004e75 more antiquotations;
wenzelm
parents: 33954
diff changeset
   278
apply( tactic {* (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
23894
1a4167d761ac tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents: 23757
diff changeset
   279
                 THEN_ALL_NEW (full_simp_tac @{simpset})) 1 *})
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   280
apply (intro strip)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   281
apply (case_tac E)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   282
apply (simp)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   283
apply( blast intro: conforms_upd_local conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   284
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   285
-- "6 FAcc"
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   286
apply (rule conjI) 
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   287
  apply (simp add: np_def)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   288
  apply (fast intro: conforms_xcpt_change xconf_raise_if)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   289
apply( fast elim!: FAcc_type_sound)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   290
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   291
-- "5 While"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   292
prefer 5
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   293
apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   294
apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   295
apply(force elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   296
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   297
apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   298
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   299
-- "4 Cond"
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   300
prefer 4
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   301
apply (case_tac "the_Bool v")
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   302
apply simp
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   303
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   304
apply simp
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   305
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   306
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   307
-- "3 ;;"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   308
prefer 3
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   309
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   310
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   311
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   312
-- "2 FAss"
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 16417
diff changeset
   313
apply (subgoal_tac "(np a' x1, aa, ba) ::\<preceq> (G, lT)")
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   314
  prefer 2
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   315
  apply (simp add: np_def)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   316
  apply (fast intro: conforms_xcpt_change xconf_raise_if)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   317
apply( case_tac "x2")
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   318
  -- "x2 = None"
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   319
  apply (simp)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   320
  apply (tactic forward_hyp_tac, clarify)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   321
  apply( drule eval_no_xcpt)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   322
  apply( erule FAss_type_sound, rule HOL.refl, assumption+)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   323
  -- "x2 = Some a"
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   324
  apply (  simp (no_asm_simp))
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   325
  apply(  fast intro: hext_trans)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   326
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   327
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   328
apply( tactic prune_params_tac)
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   329
-- "Level 52"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   330
12517
360e3215f029 exception merge, cleanup, tuned
kleing
parents: 11644
diff changeset
   331
-- "1 Call"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   332
apply( case_tac "x")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   333
prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   334
apply(  clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   335
apply(  drule exec_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   336
apply(  simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   337
apply(  drule_tac eval_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   338
apply(  simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   339
apply(  fast elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   340
apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   341
apply( drule evals_no_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   342
apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   343
apply( case_tac "a' = Null")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   344
apply(  simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   345
apply(  drule exec_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   346
apply(  simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   347
apply(  drule eval_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   348
apply(  simp)
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   349
apply (rule conjI)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   350
  apply(  fast elim: hext_trans)
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   351
  apply (rule conforms_xcpt_change, assumption) 
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   352
  apply (simp (no_asm_simp) add: xconf_def)
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   353
apply(clarsimp)
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   354
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   355
apply( drule ty_expr_is_type, simp)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   356
apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   357
apply(unfold is_class_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   358
apply(clarsimp)
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   359
11644
3dfde687f0d7 Removed some unfoldings of defs after declaring wf_java_prog as syntax
streckem
parents: 11070
diff changeset
   360
apply(rule Call_type_sound);
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   361
prefer 11
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   362
apply blast
11644
3dfde687f0d7 Removed some unfoldings of defs after declaring wf_java_prog as syntax
streckem
parents: 11070
diff changeset
   363
apply (simp (no_asm_simp))+ 
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   364
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   365
done
24178
4ff1dc2aa18d turned Unify flags into configuration options (global only);
wenzelm
parents: 23894
diff changeset
   366
14142
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   367
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   368
lemma eval_type_sound: "!!E s s'.  
14142
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   369
  [| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]  
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   370
  ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T) \<and> heap s \<le>| heap s'"
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   371
apply (simp (no_asm_simp) only: split_tupled_all)
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   372
apply (drule eval_evals_exec_type_sound [THEN conjunct1, THEN mp, THEN spec, THEN mp])
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   373
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   374
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   375
14142
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   376
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   377
lemma evals_type_sound: "!!E s s'.  
14142
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   378
  [| wf_java_prog G; G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>es[::]Ts; G=prg E |]  
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   379
  ==> (x',s')::\<preceq>E \<and> (x'=None --> (list_all2 (\<lambda>v T. G,heap s'\<turnstile>v::\<preceq>T) vs Ts)) \<and> heap s \<le>| heap s'"
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   380
apply (simp (no_asm_simp) only: split_tupled_all)
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   381
apply (drule eval_evals_exec_type_sound [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp])
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   382
apply auto
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   383
done
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   384
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   385
lemma exec_type_sound: "!!E s s'.  
14142
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   386
  \<lbrakk> wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd>; G=prg E \<rbrakk>
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   387
  \<Longrightarrow> (x',s')::\<preceq>E \<and> heap s \<le>| heap s'"
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   388
apply( simp (no_asm_simp) only: split_tupled_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   389
apply (drule eval_evals_exec_type_sound 
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   390
             [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   391
apply   auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   392
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   393
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   394
theorem all_methods_understood: 
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   395
"[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; 
13672
b95d12325b51 Added compiler
streckem
parents: 12951
diff changeset
   396
          (x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>  
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   397
  method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
14142
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   398
apply (frule eval_type_sound, assumption+)
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   399
apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   400
apply( frule widen_methd)
14142
0b04f6587e67 Changed lemmas .._type_sound
streckem
parents: 14045
diff changeset
   401
apply assumption
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   402
prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   403
apply(  fast)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   404
apply( drule non_npD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   405
apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   406
done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   407
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   408
declare split_beta [simp del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   409
declare fun_upd_apply [simp]
14045
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog
streckem
parents: 14025
diff changeset
   410
declare wf_prog_ws_prog [simp del]
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   411
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   412
end
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 8011
diff changeset
   413