diff -r e391c3de0f6b -r 7894c7dab132 src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Sun Jan 10 18:41:07 2010 +0100 +++ b/src/HOL/Bali/WellForm.thy Sun Jan 10 18:43:45 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Bali/WellForm.thy - ID: \$Id\$ Author: David von Oheimb and Norbert Schirmer *) @@ -1409,8 +1408,7 @@ from clsC ws show "methd G C sig = Some m \ G\(mdecl (sig,mthd m)) declared_in (declclass m)" - (is "PROP ?P C") - proof (induct ?P C rule: ws_class_induct') + proof (induct C rule: ws_class_induct') case Object assume "methd G Object sig = Some m" with wf show ?thesis @@ -1755,28 +1753,20 @@ lemma ballE': "\x\A. P x \ (x \ A \ Q) \ (P x \ Q) \ Q" by blast lemma subint_widen_imethds: - "\G\I\I J; wf_prog G; is_iface G J; jm \ imethds G J sig\ \ - \ im \ imethds G I sig. is_static im = is_static jm \ + assumes irel: "G\I\I J" + and wf: "wf_prog G" + and is_iface: "is_iface G J" + and jm: "jm \ imethds G J sig" + shows "\im \ imethds G I sig. is_static im = is_static jm \ accmodi im = accmodi jm \ G\resTy im\resTy jm" -proof - - assume irel: "G\I\I J" and - wf: "wf_prog G" and - is_iface: "is_iface G J" - from irel show "jm \ imethds G J sig \ ?thesis" - (is "PROP ?P I" is "PROP ?Prem J \ ?Concl I") - proof (induct ?P I rule: converse_rtrancl_induct) - case Id - assume "jm \ imethds G J sig" - then show "?Concl J" by (blast elim: bexI') + using irel jm +proof (induct rule: converse_rtrancl_induct) + case base + then show ?case by (blast elim: bexI') next - case Step - fix I SI - assume subint1_I_SI: "G\I \I1 SI" and - subint_SI_J: "G\SI \I J" and - hyp: "PROP ?P SI" and - jm: "jm \ imethds G J sig" - from subint1_I_SI + case (step I SI) + from `G\I \I1 SI` obtain i where ifI: "iface G I = Some i" and SI: "SI \ set (isuperIfs i)" @@ -1784,10 +1774,10 @@ let ?newMethods = "(Option.set \ table_of (map (\(sig, mh). (sig, I, mh)) (imethods i)))" - show "?Concl I" + show ?case proof (cases "?newMethods sig = {}") case True - with ifI SI hyp wf jm + with ifI SI step wf show "?thesis" by (auto simp add: imethds_rec) next @@ -1816,7 +1806,7 @@ wf_SI: "wf_idecl G (SI,si)" by (auto dest!: wf_idecl_supD is_acc_ifaceD dest: wf_prog_idecl) - from jm hyp + from step obtain sim::"qtname \ mhead" where sim: "sim \ imethds G SI sig" and eq_static_sim_jm: "is_static sim = is_static jm" and @@ -1841,7 +1831,6 @@ show ?thesis by auto qed - qed qed (* Tactical version *) @@ -1974,30 +1963,20 @@ from clsC ws show "\ m d. \methd G C sig = Some m; class G (declclass m) = Some d\ \ table_of (methods d) sig = Some (mthd m)" - (is "PROP ?P C") - proof (induct ?P C rule: ws_class_induct) + proof (induct rule: ws_class_induct) case Object - fix m d - assume "methd G Object sig = Some m" - "class G (declclass m) = Some d" with wf show "?thesis m d" by auto next - case Subcls - fix C c m d - assume hyp: "PROP ?P (super c)" - and m: "methd G C sig = Some m" - and declC: "class G (declclass m) = Some d" - and clsC: "class G C = Some c" - and nObj: "C \ Object" + case (Subcls C c) let ?newMethods = "table_of (map (\(s, m). (s, C, m)) (methods c)) sig" show "?thesis m d" proof (cases "?newMethods") case None - from None clsC nObj ws m declC - show "?thesis" by (auto simp add: methd_rec) (rule hyp) + from None ws Subcls + show "?thesis" by (auto simp add: methd_rec) (rule Subcls) next case Some - from Some clsC nObj ws m declC + from Some ws Subcls show "?thesis" by (auto simp add: methd_rec dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)