isabelle: src/HOL/MicroJava/J/JTypeSafe.thy@f6c1e7306c40 (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
11070 cc421547e744 improved document (added headers etc) oheimb parents: 11026 diff changeset	7	header "Type Safety Proof"
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	8
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	9	theory JTypeSafe = Eval + Conform:
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:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	14	"[\|h a = None; (h, l)::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C\|] ==>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	15	(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l)::\<preceq>(G, lT)"
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)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	18	apply( auto dest!: fields_is_type)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	19	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	20
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	21	lemma Cast_conf:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	22	"[\| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>Class C; G\<turnstile>C\<preceq>? D; cast_ok G D h v\|]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	23	==> G,h\<turnstile>v::\<preceq>Class D"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	24	apply (unfold cast_ok_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	25	apply( case_tac "v = Null")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	26	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	27	apply( drule widen_RefT)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	28	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	29	apply( drule (1) non_npD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	30	apply( auto intro!: conf_AddrI simp add: obj_ty_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	31	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	32
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	33	lemma FAcc_type_sound:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	34	"[\| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\<preceq>(G,lT);
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	35	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	36	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	37	apply( drule np_NoneD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	38	apply( erule conjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	39	apply( erule (1) notE impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	40	apply( drule non_np_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	41	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	42	apply( drule conforms_heapD [THEN hconfD])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	43	apply( assumption)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	44	apply( drule (2) widen_cfs_fields)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	45	apply( drule (1) oconf_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	46	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	47	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	48
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	49	lemma FAss_type_sound:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	50	"[\| 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	51	(G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	52	(G, lT)\<turnstile>aa::Class C;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	53	field (G,C) fn = Some (fd, ft); h''\<le>\|h';
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	54	x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>\|h;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	55	(h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None\|] ==>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	56	h''\<le>\|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	57	(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	58	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	59	apply( drule np_NoneD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	60	apply( erule conjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	61	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	62	apply( drule non_np_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	63	apply( assumption)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	64	apply( force)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	65	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	66	apply( simp (no_asm_use))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	67	apply( frule (1) hext_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	68	apply( erule exE)
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( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	71	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	72	apply( fast elim: hext_trans hext_upd_obj)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	73	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	74	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	75	apply( fast elim: conf_upd_obj [THEN iffD2])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	76
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	77	apply( rule conforms_upd_obj)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	78	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	79	apply( rule_tac [2] hextI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	80	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	81	apply( force)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	82	apply( rule oconf_hext)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	83	apply( erule_tac [2] hext_upd_obj)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	84	apply( drule (2) widen_cfs_fields)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	85	apply( rule oconf_obj [THEN iffD2])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	86	apply( simp (no_asm))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	87	apply( intro strip)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	88	apply( case_tac "(aaa, b) = (fn, fd)")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	89	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	90	apply( fast intro: conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	91	apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	92	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	93
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	94	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	95	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	96	length pTs' = length pns; distinct pns;
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	97	Ball (set lvars) (split (\<lambda>vn. is_type G))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	98	\|] ==> 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	99	apply (unfold wf_mhead_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	100	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	101	apply( rule lconf_ext_list)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	102	apply( rule Ball_set_table [THEN lconf_init_vars])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	103	apply( force)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	104	apply( assumption)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	105	apply( assumption)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	106	apply( erule (2) conf_list_gext_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	107	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	108
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	109	lemma Call_type_sound:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	110	"[\| wf_java_prog G; a' \<noteq> Null; (h, l)::\<preceq>(G, lT); class G C = Some y;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	111	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	112	list_all2 (conf G h) pvs pTsa;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	113	(md, rT, pns, lvars, blk, res) =
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	114	the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	115	\<forall>lT. (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	116	(G, lT)\<turnstile>blk\<surd> --> h\<le>\|xi \<and> (xi, xl)::\<preceq>(G, lT);
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	117	\<forall>lT. (xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	118	xi\<le>\|h' \<and> (h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	119	G,xh\<turnstile>a'::\<preceq> Class C \|] ==>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	120	xc\<le>\|h' \<and> (h', l)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	121	apply( drule max_spec2mheads)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	122	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	123	apply( drule (2) non_np_objD')
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	124	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	125	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	126	apply( frule (1) hext_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	127	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	128	apply( drule (3) Call_lemma)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	129	apply( clarsimp simp add: wf_java_mdecl_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	130	apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	131	apply( drule spec, erule impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	132	apply( erule_tac [2] notE impE, tactic "assume_tac 2")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	133	apply( rule conformsI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	134	apply( erule conforms_heapD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	135	apply( rule lconf_ext)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	136	apply( force elim!: Call_lemma2)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	137	apply( erule conf_hext, erule (1) conf_obj_AddrI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	138	apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	139	apply( erule conjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	140	apply( drule spec, erule (1) impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	141	apply( drule spec, erule (1) impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	142	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	143	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	144	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	145	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	146	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	147	apply( rule_tac [2] impI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	148	apply( erule_tac [2] notE impE, tactic "assume_tac 2")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	149	apply( frule_tac [2] conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	150	apply( tactic "assume_tac 4")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	151	apply( tactic "assume_tac 2")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	152	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	153	apply( fast elim!: widen_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	154	apply( erule conforms_hext)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	155	apply( erule (1) hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	156	apply( erule conforms_heapD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	157	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	158
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	159	declare split_if [split del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	160	declare fun_upd_apply [simp del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	161	declare fun_upd_same [simp]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	162	ML{*
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	163	val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	164	(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	165	*}
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	166	ML{*
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	167	Unify.search_bound := 40;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	168	Unify.trace_bound := 40
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	169	*}
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	170	theorem eval_evals_exec_type_sound:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	171	"wf_java_prog G ==>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	172	(G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	173	(\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	174	h\<le>\|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v ::\<preceq> T )))) \<and>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	175	(G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	176	(\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	177	h\<le>\|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	178	(G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	179	(\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	180	h\<le>\|h' \<and> (h',l')::\<preceq>(G,lT)))"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	181	apply( rule eval_evals_exec_induct)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	182	apply( unfold c_hupd_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	183
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	184	-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	185	apply( simp_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	186	apply( tactic "ALLGOALS strip_tac")
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	187	apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	188	THEN_ALL_NEW Full_simp_tac) *})
360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	189	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	190
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	191	-- "Level 7"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	192
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	193	-- "15 NewC"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	194	apply( drule new_AddrD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	195	apply( erule disjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	196	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	197	apply( simp (no_asm_simp))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	198	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	199	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	200	apply( force elim!: NewC_conforms)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	201	apply( rule conf_obj_AddrI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	202	apply( rule_tac [2] rtrancl_refl)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	203	apply( simp (no_asm))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	204
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	205	-- "for Cast"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	206	defer 1
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	207
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	208	-- "14 Lit"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	209	apply( erule conf_litval)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	210
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	211	-- "13 BinOp"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	212	apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	213	apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	214	apply( rule conjI, erule (1) hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	215	apply( erule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	216	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	217	apply( drule eval_no_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	218	apply( simp split add: binop.split)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	219
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	220	-- "12 LAcc"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	221	apply( fast elim: conforms_localD [THEN lconfD])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	222
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	223	-- "for FAss"
360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	224	apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	225	THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	226
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	227	-- "for if"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	228	apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	229
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	230	apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	231
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	232	-- "11+1 if"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	233	prefer 8
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	234	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	235	prefer 8
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	236	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	237
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	238	-- "10 Expr"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	239	prefer 6
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	240	apply( fast)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	241
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	242	-- "9 ???"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	243	apply( simp_all)
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	-- "8 Cast"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	246	prefer 8
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	247	apply (rule impI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	248	apply (drule raise_if_NoneD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	249	apply (clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	250	apply (fast elim: Cast_conf)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	251
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	252	-- "7 LAss"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	253	apply (fold fun_upd_def)
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	254	apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims")
360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	255	THEN_ALL_NEW Full_simp_tac) 1 *})
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	256	apply( blast intro: conforms_upd_local conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	257
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	258	-- "6 FAcc"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	259	apply( fast elim!: FAcc_type_sound)
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	-- "5 While"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	262	prefer 5
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	263	apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	264	apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	265	apply(force elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	266
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	267	apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	268
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	269	-- "4 Cons"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	270	prefer 3
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	271	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	272
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	273	-- "3 ;;"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	274	prefer 3
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	275	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	276
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	277	-- "2 FAss"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	278	apply( case_tac "x2 = None")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	279	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	280	apply( simp (no_asm_simp))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	281	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	282	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	283	apply( drule eval_no_xcpt)
11070 cc421547e744 improved document (added headers etc) oheimb parents: 11026 diff changeset	284	apply( erule FAss_type_sound, rule HOL.refl, assumption+)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	285
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	286	apply( tactic prune_params_tac)
12517 360e3215f029 exception merge, cleanup, tuned kleing parents: 11644 diff changeset	287	-- "Level 52"
11026 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	-- "1 Call"
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	290	apply( case_tac "x")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	291	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	292	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	293	apply( drule exec_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	294	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	295	apply( drule_tac eval_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	296	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	297	apply( fast elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	298	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	299	apply( drule evals_no_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	300	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	301	apply( case_tac "a' = Null")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	302	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	303	apply( drule exec_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	304	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	305	apply( drule eval_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	306	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	307	apply( fast elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	308	apply( drule (1) ty_expr_is_type)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	309	apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	310	apply(unfold is_class_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	311	apply(clarsimp)
11644 3dfde687f0d7 Removed some unfoldings of defs after declaring wf_java_prog as syntax streckem parents: 11070 diff changeset	312	apply(rule Call_type_sound);
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	313	prefer 11
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	314	apply blast
11644 3dfde687f0d7 Removed some unfoldings of defs after declaring wf_java_prog as syntax streckem parents: 11070 diff changeset	315	apply (simp (no_asm_simp))+
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	316	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	317	ML{*
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	318	Unify.search_bound := 20;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	319	Unify.trace_bound := 20
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	320	*}
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	321
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	322	lemma eval_type_sound: "!!E s s'.
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	323	[\| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); s::\<preceq>E; E\<turnstile>e::T \|]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	324	==> s'::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	325	apply( simp (no_asm_simp) only: split_tupled_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	326	apply (drule eval_evals_exec_type_sound
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	327	[THEN conjunct1, THEN mp, THEN spec, THEN mp])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	328	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	329	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	330
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	331	lemma exec_type_sound: "!!E s s'.
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	332	[\| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); s::\<preceq>E; E\<turnstile>s0\<surd> \|]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	333	==> s'::\<preceq>E"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	334	apply( simp (no_asm_simp) only: split_tupled_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	335	apply (drule eval_evals_exec_type_sound
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	336	[THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	337	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	338	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	339
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	340	theorem all_methods_understood:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	341	"[\|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	342	s::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None\|] ==>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	343	method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	344	apply( drule (4) eval_type_sound)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	345	apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	346	apply( frule widen_methd)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	347	apply( assumption)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	348	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	349	apply( fast)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	350	apply( drule non_npD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	351	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	352	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	353
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	354	declare split_beta [simp del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	355	declare fun_upd_apply [simp]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	356
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	357	end
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	358
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	359

author	nipkow
	Thu, 14 Feb 2002 12:06:07 +0100
changeset 12888	f6c1e7306c40
parent 12517	360e3215f029
child 12911	704713ca07ea
permissions	-rw-r--r--