isabelle: src/HOL/MicroJava/J/JTypeSafe.thy@9a26c0d7a47a (annotated)

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

author	wenzelm
	Tue, 10 Jun 2008 16:43:16 +0200
changeset 27118	9a26c0d7a47a
parent 27098	d89fb4ee7280
child 27215	b43785a81e01
permissions	-rw-r--r--