isabelle: src/HOL/MicroJava/J/JTypeSafe.thy@f9f3006a5579 (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
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	5	section \<open>Type Safety Proof\<close>
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
58263 6c907aad90ba ported MicroJava to new datatypes blanchet parents: 57492 diff changeset	25	apply (rename_tac ref_ty, case_tac "ref_ty")
14045 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)
57492 74bf65a1910a Hypsubst preserves equality hypotheses Thomas Sewell <thomas.sewell@nicta.com.au> parents: 54742 diff changeset	96	apply( case_tac "(ab, b) = (fn, fd)")
11026 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;
61424 c3658c18b7bc prod_case as canonical name for product type eliminator haftmann parents: 61361 diff changeset	107	Ball (set lvars) (case_prod (\<lambda>vn. is_type G))
11026 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)
59807 22bc39064290 prefer local fixes; wenzelm parents: 59802 diff changeset	140	apply( erule_tac V = "method sig x = y" for sig x y in thin_rl)
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	141	apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac @{context} 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)
59807 22bc39064290 prefer local fixes; wenzelm parents: 59802 diff changeset	147	apply( erule_tac V = "E\<turnstile>blk\<surd>" for E blk in thin_rl)
13672 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)
59807 22bc39064290 prefer local fixes; wenzelm parents: 59802 diff changeset	153	apply( erule_tac V = "E\<turnstile>res::rT" for E rT in thin_rl)
11026 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)
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	159	apply( erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	160	apply( frule_tac [2] conf_widen)
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	161	apply( tactic "assume_tac @{context} 4")
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	162	apply( tactic "assume_tac @{context} 2")
11026 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
62390 842917225d56 more canonical names nipkow parents: 62042 diff changeset	174	declare if_split [split del]
11026 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
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	179	ML\<open>
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	180	fun forward_hyp_tac ctxt =
60754 02924903a6fd prefer tactics with explicit context; wenzelm parents: 59826 diff changeset	181	ALLGOALS (TRY o (EVERY' [dresolve_tac ctxt [spec], mp_tac ctxt,
02924903a6fd prefer tactics with explicit context; wenzelm parents: 59826 diff changeset	182	(mp_tac ctxt ORELSE' (dresolve_tac ctxt [spec] THEN' mp_tac ctxt)),
02924903a6fd prefer tactics with explicit context; wenzelm parents: 59826 diff changeset	183	REPEAT o (eresolve_tac ctxt [conjE])]))
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	184	\<close>
24178 4ff1dc2aa18d turned Unify flags into configuration options (global only); wenzelm parents: 23894 diff changeset	185
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	186
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	187	theorem eval_evals_exec_type_sound:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	188	"wf_java_prog G ==>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	189	(G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) -->
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	190	(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T -->
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	191	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	192	(G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	193	(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	194	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	195	(G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) -->
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	196	(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> -->
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	197	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	198	apply( rule eval_evals_exec_induct)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	199	apply( unfold c_hupd_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	200
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	201	\<comment> "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	202	apply( simp_all)
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58963 diff changeset	203	apply( tactic "ALLGOALS (REPEAT o resolve_tac @{context} [impI, allI])")
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	204	apply( tactic \<open>ALLGOALS (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	205	THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context})))\<close>)
60754 02924903a6fd prefer tactics with explicit context; wenzelm parents: 59826 diff changeset	206	apply(tactic "ALLGOALS (EVERY' [REPEAT o (eresolve_tac @{context} [conjE]), REPEAT o hyp_subst_tac @{context}])")
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	207
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	208	\<comment> "Level 7"
6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	209	\<comment> "15 NewC"
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	210	apply (drule sym)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	211	apply( drule new_AddrD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	212	apply( erule disjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	213	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	214	apply( simp (no_asm_simp))
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	215	apply (rule conforms_xcpt_change, assumption)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	216	apply (simp (no_asm_simp) add: xconf_def)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	217	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	218	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	219	apply( force elim!: NewC_conforms)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	220	apply( rule conf_obj_AddrI)
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: 32367 diff changeset	221	apply( rule_tac [2] rtrancl.rtrancl_refl)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	222	apply( simp (no_asm))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	223
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	224	\<comment> "for Cast"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	225	defer 1
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	226
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	227	\<comment> "14 Lit"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	228	apply( erule conf_litval)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	229
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	230	\<comment> "13 BinOp"
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	231	apply (tactic "forward_hyp_tac @{context}")
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	232	apply (tactic "forward_hyp_tac @{context}")
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	233	apply( rule conjI, erule (1) hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	234	apply( erule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	235	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	236	apply( drule eval_no_xcpt)
63648 f9f3006a5579 "split add" -> "split" nipkow parents: 62390 diff changeset	237	apply( simp split: binop.split)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	238
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	239	\<comment> "12 LAcc"
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	240	apply simp
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	241	apply( fast elim: conforms_localD [THEN lconfD])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	242
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	243	\<comment> "for FAss"
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	244	apply( tactic \<open>EVERY'[eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	245	THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (eresolve_tac @{context} [conjE]), hyp_subst_tac @{context}] 3\<close>)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	246
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	247	\<comment> "for if"
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	248	apply( tactic \<open>(Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	249	(asm_full_simp_tac @{context})) 7\<close>)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	250
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	251	apply (tactic "forward_hyp_tac @{context}")
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	252
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	253	\<comment> "11+1 if"
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)
22271 51a80e238b29 Adapted to new inductive definition package. berghofe parents: 16417 diff changeset	256	prefer 7
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	257	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	258
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	259	\<comment> "10 Expr"
22271 51a80e238b29 Adapted to new inductive definition package. berghofe parents: 16417 diff changeset	260	prefer 6
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	261	apply( fast)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	262
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	263	\<comment> "9 ???"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	264	apply( simp_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	265
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	266	\<comment> "8 Cast"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	267	prefer 8
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	268	apply (rule conjI)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	269	apply (fast intro: conforms_xcpt_change xconf_raise_if)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	270
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	271	apply clarify
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	272	apply (drule raise_if_NoneD)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	273	apply (clarsimp)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	274	apply (rule Cast_conf)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	275	apply assumption+
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	276
14045 a34d89ce6097 Introduced distinction wf_prog vs. ws_prog streckem parents: 14025 diff changeset	277
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	278	\<comment> "7 LAss"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	279	apply (fold fun_upd_def)
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	280	apply( tactic \<open>(eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
8b5f00202e1a isabelle update_cartouches; wenzelm parents: 60754 diff changeset	281	THEN_ALL_NEW (full_simp_tac @{context})) 1\<close>)
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	282	apply (intro strip)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	283	apply (case_tac E)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	284	apply (simp)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	285	apply( blast intro: conforms_upd_local conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	286
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	287	\<comment> "6 FAcc"
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	288	apply (rule conjI)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	289	apply (simp add: np_def)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	290	apply (fast intro: conforms_xcpt_change xconf_raise_if)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	291	apply( fast elim!: FAcc_type_sound)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	292
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	293	\<comment> "5 While"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	294	prefer 5
59807 22bc39064290 prefer local fixes; wenzelm parents: 59802 diff changeset	295	apply(erule_tac V = "a \<longrightarrow> b" for a b in thin_rl)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	296	apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	297	apply(force elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	298
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	299	apply (tactic "forward_hyp_tac @{context}")
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	300
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	301	\<comment> "4 Cond"
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	302	prefer 4
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	303	apply (case_tac "the_Bool v")
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	304	apply simp
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	305	apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	306	apply simp
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	307	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	308
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	309	\<comment> "3 ;;"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	310	prefer 3
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	311	apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	312
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	313
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	314	\<comment> "2 FAss"
22271 51a80e238b29 Adapted to new inductive definition package. berghofe parents: 16417 diff changeset	315	apply (subgoal_tac "(np a' x1, aa, ba) ::\<preceq> (G, lT)")
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	316	prefer 2
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	317	apply (simp add: np_def)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	318	apply (fast intro: conforms_xcpt_change xconf_raise_if)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	319	apply( case_tac "x2")
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	320	\<comment> "x2 = None"
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	321	apply (simp)
58963 26bf09b95dda proper context for assume_tac (atac remains as fall-back without context); wenzelm parents: 58886 diff changeset	322	apply (tactic "forward_hyp_tac @{context}", clarify)
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	323	apply( drule eval_no_xcpt)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	324	apply( erule FAss_type_sound, rule HOL.refl, assumption+)
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	325	\<comment> "x2 = Some a"
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	326	apply ( simp (no_asm_simp))
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	327	apply( fast intro: hext_trans)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	328
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	329
54742 7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; wenzelm parents: 51798 diff changeset	330	apply( tactic "prune_params_tac @{context}")
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	331	\<comment> "Level 52"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	332
62042 6c6ccf573479 isabelle update_cartouches -c -t; wenzelm parents: 61424 diff changeset	333	\<comment> "1 Call"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	334	apply( case_tac "x")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	335	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	336	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	337	apply( drule exec_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( drule_tac eval_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	340	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	341	apply( fast elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	342	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	343	apply( drule evals_no_xcpt)
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( case_tac "a' = Null")
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 exec_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	348	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	349	apply( drule eval_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	350	apply( simp)
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	351	apply (rule conjI)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	352	apply( fast elim: hext_trans)
14045 a34d89ce6097 Introduced distinction wf_prog vs. ws_prog streckem parents: 14025 diff changeset	353	apply (rule conforms_xcpt_change, assumption)
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog streckem parents: 14025 diff changeset	354	apply (simp (no_asm_simp) add: xconf_def)
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	355	apply(clarsimp)
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	356
b95d12325b51 Added compiler streckem parents: 12951 diff changeset	357	apply( drule ty_expr_is_type, simp)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	358	apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	359	apply(unfold is_class_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	360	apply(clarsimp)
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	361
58860 fee7cfa69c50 eliminated spurious semicolons; wenzelm parents: 58263 diff changeset	362	apply(rule Call_type_sound)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	363	prefer 11
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	364	apply blast
11644 3dfde687f0d7 Removed some unfoldings of defs after declaring wf_java_prog as syntax streckem parents: 11070 diff changeset	365	apply (simp (no_asm_simp))+
13672 b95d12325b51 Added compiler streckem parents: 12951 diff changeset	366
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	367	done
24178 4ff1dc2aa18d turned Unify flags into configuration options (global only); wenzelm parents: 23894 diff changeset	368
14142 0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	369
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	370	lemma eval_type_sound: "!!E s s'.
14142 0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	371	[\| 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	372	==> (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	373	apply (simp (no_asm_simp) only: split_tupled_all)
0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	374	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	375	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	376	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	377
14142 0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	378
14045 a34d89ce6097 Introduced distinction wf_prog vs. ws_prog streckem parents: 14025 diff changeset	379	lemma evals_type_sound: "!!E s s'.
14142 0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	380	[\| 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	381	==> (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	382	apply (simp (no_asm_simp) only: split_tupled_all)
0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	383	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	384	apply auto
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog streckem parents: 14025 diff changeset	385	done
a34d89ce6097 Introduced distinction wf_prog vs. ws_prog streckem parents: 14025 diff changeset	386
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	387	lemma exec_type_sound: "!!E s s'.
14142 0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	388	\<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	389	\<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	390	apply( simp (no_asm_simp) only: split_tupled_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	391	apply (drule eval_evals_exec_type_sound
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	392	[THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	393	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	394	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	395
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	396	theorem all_methods_understood:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	397	"[\|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	398	(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	399	method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
14142 0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	400	apply (frule eval_type_sound, assumption+)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	401	apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	402	apply( frule widen_methd)
14142 0b04f6587e67 Changed lemmas .._type_sound streckem parents: 14045 diff changeset	403	apply assumption
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	404	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	405	apply( fast)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	406	apply( drule non_npD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	407	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	408	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	409
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	410	declare split_beta [simp del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	411	declare fun_upd_apply [simp]
14045 a34d89ce6097 Introduced distinction wf_prog vs. ws_prog streckem parents: 14025 diff changeset	412	declare wf_prog_ws_prog [simp del]
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	413
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	414	end
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	415

author	nipkow
	Wed, 10 Aug 2016 09:33:54 +0200
changeset 63648	f9f3006a5579
parent 62390	842917225d56
child 67443	3abf6a722518
permissions	-rw-r--r--