isabelle: src/HOL/MicroJava/J/JTypeSafe.thy@532e0ac5a66d (annotated)

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}]
51686 532e0ac5a66d added ML antiquotation @{theory_context}; wenzelm parents: 51304 diff changeset	203	THEN_ALL_NEW (full_simp_tac (simpset_of @{theory_context 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

author	wenzelm
	Wed, 10 Apr 2013 17:02:47 +0200
changeset 51686	532e0ac5a66d
parent 51304	0e71a248cacb
child 51717	9e7d1c139569
permissions	-rw-r--r--