isabelle: src/HOL/MicroJava/J/JTypeSafe.thy@cc421547e744 (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;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	96	length pTs' = length pns; nodups pns;
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 (unfold wf_java_prog_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	122	apply( drule max_spec2mheads)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	123	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	124	apply( drule (2) non_np_objD')
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( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	127	apply( frule (1) hext_objD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	128	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	129	apply( drule (3) Call_lemma)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	130	apply( clarsimp simp add: wf_java_mdecl_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	131	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	132	apply( drule spec, erule impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	133	apply( erule_tac [2] notE impE, tactic "assume_tac 2")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	134	apply( rule conformsI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	135	apply( erule conforms_heapD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	136	apply( rule lconf_ext)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	137	apply( force elim!: Call_lemma2)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	138	apply( erule conf_hext, erule (1) conf_obj_AddrI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	139	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	140	apply( erule conjE)
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( drule spec, erule (1) impE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	143	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	144	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	145	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	146	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	147	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	148	apply( rule_tac [2] impI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	149	apply( erule_tac [2] notE impE, tactic "assume_tac 2")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	150	apply( frule_tac [2] conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	151	apply( tactic "assume_tac 4")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	152	apply( tactic "assume_tac 2")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	153	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	154	apply( fast elim!: widen_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	155	apply( erule conforms_hext)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	156	apply( erule (1) hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	157	apply( erule conforms_heapD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	158	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	159
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	160	declare split_if [split del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	161	declare fun_upd_apply [simp del]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	162	declare fun_upd_same [simp]
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	163	ML{*
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	164	val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	165	(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	166	*}
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	167	ML{*
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	168	Unify.search_bound := 40;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	169	Unify.trace_bound := 40
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	170	*}
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	171	theorem eval_evals_exec_type_sound:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	172	"wf_java_prog G ==>
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	173	(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	174	(\<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	175	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	176	(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	177	(\<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	178	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	179	(G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) -->
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	180	(\<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	181	h\<le>\|h' \<and> (h',l')::\<preceq>(G,lT)))"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	182	apply( rule eval_evals_exec_induct)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	183	apply( unfold c_hupd_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	184
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	185	(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	186	apply( simp_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	187	apply( tactic "ALLGOALS strip_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	188	apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *})
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	189	apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	190	apply( unfold wf_java_prog_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	191
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	192	(* Level 7 *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	193
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	194	(* 15 NewC *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	195	apply( drule new_AddrD)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	196	apply( erule disjE)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	197	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	198	apply( simp (no_asm_simp))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	199	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	200	apply( rule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	201	apply( force elim!: NewC_conforms)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	202	apply( rule conf_obj_AddrI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	203	apply( rule_tac [2] rtrancl_refl)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	204	apply( simp (no_asm))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	205
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	206	(* for Cast *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	207	defer 1
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	208
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	209	(* 14 Lit *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	210	apply( erule conf_litval)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	211
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	212	(* 13 BinOp *)
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 (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	215	apply( rule conjI, erule (1) hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	216	apply( erule conjI)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	217	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	218	apply( drule eval_no_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	219	apply( simp split add: binop.split)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	220
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	221	(* 12 LAcc *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	222	apply( fast elim: conforms_localD [THEN lconfD])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	223
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	224	(* for FAss *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	225	apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	226
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	227	(* for if *)
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
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	232	(* 11+1 if *)
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
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	238	(* 10 Expr *)
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
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	242	(* 9 ??? *)
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
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	245	(* 8 Cast *)
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
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	252	(* 7 LAss *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	253	apply (fold fun_upd_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	254	apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) 1 *})
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	255	apply( blast intro: conforms_upd_local conf_widen)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	256
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	257	(* 6 FAcc *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	258	apply( fast elim!: FAcc_type_sound)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	259
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	260	(* 5 While *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	261	prefer 5
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	262	apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	263	apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	264	apply(force elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	265
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	266	apply (tactic "forward_hyp_tac")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	267
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	268	(* 4 Cons *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	269	prefer 3
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	270	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	271
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	272	(* 3 ;; *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	273	prefer 3
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	274	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	275
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	276	(* 2 FAss *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	277	apply( case_tac "x2 = None")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	278	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	279	apply( simp (no_asm_simp))
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	280	apply( fast intro: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	281	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	282	apply( drule eval_no_xcpt)
11070 cc421547e744 improved document (added headers etc) oheimb parents: 11026 diff changeset	283	apply( erule FAss_type_sound, rule HOL.refl, assumption+)
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	284
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	285	apply( tactic prune_params_tac)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	286	(* Level 52 *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	287
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	288	(* 1 Call *)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	289	apply( case_tac "x")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	290	prefer 2
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	291	apply( clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	292	apply( drule exec_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	293	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	294	apply( drule_tac eval_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	295	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	296	apply( fast elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	297	apply( clarify)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	298	apply( drule evals_no_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	299	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	300	apply( case_tac "a' = Null")
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	301	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	302	apply( drule exec_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	303	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	304	apply( drule eval_xcpt)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	305	apply( simp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	306	apply( fast elim: hext_trans)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	307	apply( drule (1) ty_expr_is_type)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	308	apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	309	apply(unfold is_class_def)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	310	apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	311	apply(rule Call_type_sound [unfolded wf_java_prog_def]);
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	312	prefer 11
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	313	apply blast
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	314	apply (simp (no_asm_simp))+
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	315	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	316	ML{*
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	317	Unify.search_bound := 20;
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	318	Unify.trace_bound := 20
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	319	*}
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	lemma eval_type_sound: "!!E s s'.
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	322	[\| 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	323	==> 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	324	apply( simp (no_asm_simp) only: split_tupled_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	325	apply (drule eval_evals_exec_type_sound
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	326	[THEN conjunct1, THEN mp, THEN spec, THEN mp])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	327	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	328	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	329
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	330	lemma exec_type_sound: "!!E s s'.
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	331	[\| 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	332	==> s'::\<preceq>E"
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	333	apply( simp (no_asm_simp) only: split_tupled_all)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	334	apply (drule eval_evals_exec_type_sound
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	335	[THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	336	apply auto
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	337	done
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	338
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	339	theorem all_methods_understood:
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	340	"[\|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	341	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	342	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	343	apply( drule (4) eval_type_sound)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	344	apply(clarsimp)
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 8011 diff changeset	345	apply(unfold wf_java_prog_def)
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	oheimb
	Mon, 05 Feb 2001 20:14:15 +0100
changeset 11070	cc421547e744
parent 11026	a50365d21144
child 11644	3dfde687f0d7
permissions	-rw-r--r--