# HG changeset patch # User wenzelm # Date 1007559130 -3600 # Node ID 23bd419144ebcbae4d25488a62c2c73affb292ba # Parent c845fec1ac946806fda1896793b09b01bc8b4e9f eliminated old use of intro/elim method; tuned; diff -r c845fec1ac94 -r 23bd419144eb src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Dec 05 13:16:34 2001 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Dec 05 14:32:10 2001 +0100 @@ -268,12 +268,12 @@ from step obtain ST' LT' where s': "phi C sig ! Suc pc = Some (ST', LT')" - by (simp add: step_def split_paired_Ex) (elim, rule that) + by (auto simp add: step_def split_paired_Ex) - from X + from X obtain T where X_Ref: "X = RefT T" - by - (drule widen_RefT2, erule exE, rule that) + by (blast dest: widen_RefT2) from s ins frame obtain @@ -289,8 +289,8 @@ a_stk': "approx_stk G hp stk' ST" and stk': "stk = opTs @ oX # stk'" and l_o: "length opTs = length apTs" - "length stk' = length ST" - by - (drule approx_stk_append, simp, elim, simp) + "length stk' = length ST" + by (auto dest: approx_stk_append) from oX have "\T'. typeof (option_map obj_ty \ hp) oX = Some T' \ G \ T' \ X" @@ -299,10 +299,8 @@ with X_Ref obtain T' where oX_Ref: "typeof (option_map obj_ty \ hp) oX = Some (RefT T')" - "G \ RefT T' \ X" - apply (elim, simp) - apply (frule widen_RefT2) - by (elim, simp) + "G \ RefT T' \ X" + by (auto dest: widen_RefT2) from stk' l_o l have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp @@ -330,7 +328,7 @@ with X_Ref obtain X' where X': "X = Class X'" - by - (drule widen_Class, elim, rule that) + by (blast dest: widen_Class) with X have X'_subcls: "G \ X' \C C'" @@ -339,7 +337,7 @@ with mC' wfprog obtain D0 rT0 maxs0 maxl0 ins0 where mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\rT0\rT" - by (auto dest: subtype_widen_methd intro: that) + by (fast dest: subtype_widen_methd) from X' D have D_subcls: "G \ D \C X'" @@ -349,7 +347,7 @@ obtain D'' rT' mxs' mxl' ins' where mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" "G \ rT' \ rT0" - by (auto dest: subtype_widen_methd intro: that) + by (fast dest: subtype_widen_methd) from mX mD have rT': "G \ rT' \ rT" @@ -357,7 +355,7 @@ from is_class X'_subcls D_subcls have is_class_D: "is_class G D" - by (auto dest: subcls_is_class2) + by (auto dest: subcls_is_class2) with mD wfprog obtain mD'': @@ -442,12 +440,11 @@ with state'_val heap_ok mD'' ins method phi_pc s X' l frames s' LT0 c_f c_f' is_class_C - have ?thesis - by (simp add: correct_state_def) (intro exI conjI, blast, assumption+) + have ?thesis by (simp add: correct_state_def) (intro exI conjI, blast) } with Null_ok oX_Ref - show "G,phi \JVM state'\" by - (cases oX, auto) + show "G,phi \JVM state'\" by (cases oX) auto qed lemmas [simp del] = map_append diff -r c845fec1ac94 -r 23bd419144eb src/HOL/MicroJava/BV/LBVCorrect.thy --- a/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Dec 05 13:16:34 2001 +0100 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Wed Dec 05 14:32:10 2001 +0100 @@ -241,18 +241,18 @@ moreover from pc obtain x xs where "is = x#xs" - by (simp add: neq_Nil_conv) (elim, rule that) + by (auto simp add: neq_Nil_conv) with wtl obtain s' where "wtl_cert x G rT s cert mxs (length is) 0 = OK s'" - by simp (elim, rule that, simp) + by auto hence "!!t. cert!0 = Some t ==> G \ s <=' cert!0" by (simp add: wtl_cert_def split: if_splits) ultimately show ?thesis - by - (cases "cert!0", auto) + by (cases "cert!0") auto qed diff -r c845fec1ac94 -r 23bd419144eb src/HOL/MicroJava/BV/StepMono.thy --- a/src/HOL/MicroJava/BV/StepMono.thy Wed Dec 05 13:16:34 2001 +0100 +++ b/src/HOL/MicroJava/BV/StepMono.thy Wed Dec 05 14:32:10 2001 +0100 @@ -14,52 +14,52 @@ lemma sup_loc_some [rule_format]: -"\ y n. (G \ b <=l y) --> n < length y --> y!n = OK t --> +"\ y n. (G \ b <=l y) --> n < length y --> y!n = OK t --> (\t. b!n = OK t \ (G \ (b!n) <=o (y!n)))" (is "?P b") proof (induct (open) ?P b) show "?P []" by simp case Cons - show "?P (a#list)" + show "?P (a#list)" proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def) fix z zs n - assume * : - "G \ a <=o z" "list_all2 (sup_ty_opt G) list zs" + assume * : + "G \ a <=o z" "list_all2 (sup_ty_opt G) list zs" "n < Suc (length list)" "(z # zs) ! n = OK t" - show "(\t. (a # list) ! n = OK t) \ G \(a # list) ! n <=o OK t" - proof (cases n) + show "(\t. (a # list) ! n = OK t) \ G \(a # list) ! n <=o OK t" + proof (cases n) case 0 with * show ?thesis by (simp add: sup_ty_opt_OK) next case Suc with Cons * - show ?thesis by (simp add: sup_loc_def Listn.le_def lesub_def) + show ?thesis by (simp add: sup_loc_def Listn.le_def lesub_def) qed - qed + qed qed - + lemma all_widen_is_sup_loc: -"\b. length a = length b --> - (\x\set (zip a b). x \ widen G) = (G \ (map OK a) <=l (map OK b))" +"\b. length a = length b --> + (\x\set (zip a b). x \ widen G) = (G \ (map OK a) <=l (map OK b))" (is "\b. length a = length b --> ?Q a b" is "?P a") proof (induct "a") show "?P []" by simp fix l ls assume Cons: "?P ls" - show "?P (l#ls)" + show "?P (l#ls)" proof (intro allI impI) - fix b - assume "length (l # ls) = length (b::ty list)" + fix b + assume "length (l # ls) = length (b::ty list)" with Cons show "?Q (l # ls) b" by - (cases b, auto) qed qed - + -lemma append_length_n [rule_format]: +lemma append_length_n [rule_format]: "\n. n \ length x --> (\a b. x = a@b \ length a = n)" (is "?P x") proof (induct (open) ?P x) show "?P []" by simp @@ -71,54 +71,38 @@ fix n assume l: "n \ length (l # ls)" - show "\a b. l # ls = a @ b \ length a = n" + show "\a b. l # ls = a @ b \ length a = n" proof (cases n) assume "n=0" thus ?thesis by simp next fix "n'" assume s: "n = Suc n'" - with l - have "n' \ length ls" by simp + with l + have "n' \ length ls" by simp hence "\a b. ls = a @ b \ length a = n'" by (rule Cons [rule_format]) - thus ?thesis - proof elim - fix a b - assume "ls = a @ b" "length a = n'" - with s - have "l # ls = (l#a) @ b \ length (l#a) = n" by simp - thus ?thesis by blast - qed + then obtain a b where "ls = a @ b" "length a = n'" by rules + with s have "l # ls = (l#a) @ b \ length (l#a) = n" by simp + thus ?thesis by blast qed qed qed - lemma rev_append_cons: "[|n < length x|] ==> \a b c. x = (rev a) @ b # c \ length a = n" proof - assume n: "n < length x" hence "n \ length x" by simp hence "\a b. x = a @ b \ length a = n" by (rule append_length_n) - thus ?thesis - proof elim - fix r d assume x: "x = r@d" "length r = n" - with n - have "\b c. d = b#c" by (simp add: neq_Nil_conv) - - thus ?thesis - proof elim - fix b c - assume "d = b#c" - with x - have "x = (rev (rev r)) @ b # c \ length (rev r) = n" by simp - thus ?thesis by blast - qed - qed + then obtain r d where x: "x = r@d" "length r = n" by rules + with n have "\b c. d = b#c" by (simp add: neq_Nil_conv) + then obtain b c where "d = b#c" by rules + with x have "x = (rev (rev r)) @ b # c \ length (rev r) = n" by simp + thus ?thesis by blast qed lemmas [iff] = not_Err_eq -lemma app_mono: +lemma app_mono: "[|G \ s <=' s'; app i G m rT s'|] ==> app i G m rT s" proof - @@ -129,19 +113,18 @@ have "app i G m rT (Some s2)" proof (cases (open) i) case Load - + from G Load app have "G \ snd s2 <=l snd s1" by (auto simp add: sup_state_conv) - - with G Load app - show ?thesis - by clarsimp (drule sup_loc_some, simp+) + + with G Load app + show ?thesis + by (auto dest: sup_loc_some) next case Store with G app show ?thesis - by - (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 - sup_loc_length sup_state_conv) + by (cases s2) (auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_conv) next case LitPush with G app @@ -154,14 +137,14 @@ case Getfield with app G show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans) + by (cases s2) (auto simp add: sup_state_Cons2, rule widen_trans) next case Putfield - - with app + + with app obtain vT oT ST LT b where s1: "s1 = (vT # oT # ST, LT)" and - "field (G, cname) vname = Some (cname, b)" + "field (G, cname) vname = Some (cname, b)" "is_class G cname" and oT: "G\ oT\ (Class cname)" and vT: "G\ vT\ b" @@ -172,7 +155,7 @@ where s2: "s2 = (vT' # oT' # ST', LT')" and oT': "G\ oT' \ oT" and vT': "G\ vT' \ vT" - by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that) + by (cases s2) (auto simp add: sup_state_Cons2) moreover from vT' vT have "G \ vT' \ b" by (rule widen_trans) @@ -185,58 +168,58 @@ next case Checkcast with app G - show ?thesis - by - (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2) + show ?thesis + by (cases s2) (auto intro!: widen_RefT2 simp add: sup_state_Cons2) next case Return with app G show ?thesis - by - (cases s2, auto simp add: sup_state_Cons2, rule widen_trans) + by (cases s2) (auto simp add: sup_state_Cons2, rule widen_trans) next case Pop with app G show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2) + by (cases s2) (auto simp add: sup_state_Cons2) next case Dup with app G show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2, + by (cases s2) (clarsimp simp add: sup_state_Cons2, auto dest: sup_state_length) next case Dup_x1 with app G show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2, + by (cases s2) (clarsimp simp add: sup_state_Cons2, auto dest: sup_state_length) next case Dup_x2 with app G show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2, + by (cases s2) (clarsimp simp add: sup_state_Cons2, auto dest: sup_state_length) next case Swap with app G show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2) + by (cases s2) (clarsimp simp add: sup_state_Cons2) next case IAdd with app G show ?thesis - by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT) + by (cases s2) (auto simp add: sup_state_Cons2 PrimT_PrimT) next - case Goto + case Goto with app show ?thesis by simp next case Ifcmpeq with app G show ?thesis - by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2) + by (cases s2) (auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2) next case Invoke - + with app obtain apTs X ST LT mD' rT' b' where s1: "s1 = (rev apTs @ X # ST, LT)" and @@ -245,40 +228,40 @@ C: "G \ X \ Class cname" and w: "\x \ set (zip apTs list). x \ widen G" and m: "method (G, cname) (mname, list) = Some (mD', rT', b')" - by (simp del: not_None_eq, elim exE conjE) (rule that) + by (simp del: not_None_eq) blast+ obtain apTs' X' ST' LT' where s2: "s2 = (rev apTs' @ X' # ST', LT')" and l': "length apTs' = length list" proof - - from l s1 G - have "length list < length (fst s2)" + from l s1 G + have "length list < length (fst s2)" by simp hence "\a b c. (fst s2) = rev a @ b # c \ length a = length list" by (rule rev_append_cons [rule_format]) thus ?thesis - by - (cases s2, elim exE conjE, simp, rule that) + by - (cases s2, elim exE conjE, simp, rule that) qed from l l' have "length (rev apTs') = length (rev apTs)" by simp - - from this s1 s2 G + + from this s1 s2 G obtain G': "G \ (apTs',LT') <=s (apTs,LT)" and X : "G \ X' \ X" and "G \ (ST',LT') <=s (ST,LT)" by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1) - + with C have C': "G \ X' \ Class cname" by - (rule widen_trans, auto) - + from G' have "G \ map OK apTs' <=l map OK apTs" by (simp add: sup_state_conv) also from l w - have "G \ map OK apTs <=l map OK list" + have "G \ map OK apTs <=l map OK list" by (simp add: all_widen_is_sup_loc) finally have "G \ map OK apTs' <=l map OK list" . @@ -294,33 +277,33 @@ } note this [simp] assume "G \ s <=' s'" "app i G m rT s'" - - thus ?thesis + + thus ?thesis by - (cases s, cases s', auto) qed - + lemmas [simp del] = split_paired_Ex lemmas [simp] = step_def lemma step_mono_Some: "[| app i G m rT (Some s2); G \ s1 <=s s2 |] ==> G \ the (step i G (Some s1)) <=s the (step i G (Some s2))" -proof (cases s1, cases s2) +proof (cases s1, cases s2) fix a1 b1 a2 b2 assume s: "s1 = (a1,b1)" "s2 = (a2,b2)" assume app2: "app i G m rT (Some s2)" assume G: "G \ s1 <=s s2" - hence "G \ Some s1 <=' Some s2" + hence "G \ Some s1 <=' Some s2" by simp from this app2 have app1: "app i G m rT (Some s1)" by (rule app_mono) - + have "step i G (Some s1) \ None \ step i G (Some s2) \ None" by simp - then + then obtain a1' b1' a2' b2' - where step: "step i G (Some s1) = Some (a1',b1')" + where step: "step i G (Some s1) = Some (a1',b1')" "step i G (Some s2) = Some (a2',b2')" by (auto simp del: step_def simp add: s) @@ -330,51 +313,51 @@ with s app1 obtain y where - y: "nat < length b1" "b1 ! nat = OK y" by clarsimp + y: "nat < length b1" "b1 ! nat = OK y" by auto from Load s app2 obtain y' where - y': "nat < length b2" "b2 ! nat = OK y'" by clarsimp + y': "nat < length b2" "b2 ! nat = OK y'" by auto - from G s + from G s have "G \ b1 <=l b2" by (simp add: sup_state_conv) with y y' - have "G \ y \ y'" - by - (drule sup_loc_some, simp+) - - with Load G y y' s step app1 app2 - show ?thesis by (clarsimp simp add: sup_state_conv) + have "G \ y \ y'" + by (auto dest: sup_loc_some) + + with Load G y y' s step app1 app2 + show ?thesis by (auto simp add: sup_state_conv) next case Store with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_conv sup_loc_update) + by (auto simp add: sup_state_conv sup_loc_update) next case LitPush with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case New with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case Getfield with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case Putfield with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case Checkcast with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case Invoke @@ -382,35 +365,35 @@ obtain a X ST where s1: "s1 = (a @ X # ST, b1)" and l: "length a = length list" - by (simp, elim exE conjE, simp) + by auto from Invoke s app2 obtain a' X' ST' where s2: "s2 = (a' @ X' # ST', b2)" and l': "length a' = length list" - by (simp, elim exE conjE, simp) + by auto from l l' have lr: "length a = length a'" by simp - - from lr G s s1 s2 + + from lr G s s1 s2 have "G \ (ST, b1) <=s (ST', b2)" by (simp add: sup_state_append_fst sup_state_Cons1) - + moreover - + from Invoke G s step app1 app2 have "b1 = b1' \ b2 = b2'" by simp - ultimately + ultimately have "G \ (ST, b1') <=s (ST', b2')" by simp with Invoke G s step app1 app2 s1 s2 l l' - show ?thesis - by (clarsimp simp add: sup_state_conv) + show ?thesis + by (auto simp add: sup_state_conv) next - case Return + case Return with G step show ?thesis by simp @@ -418,32 +401,32 @@ case Pop with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case Dup with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case Dup_x1 with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next + by (auto simp add: sup_state_Cons1) + next case Dup_x2 with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case Swap with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case IAdd with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) next case Goto with G s step app1 app2 @@ -452,11 +435,11 @@ case Ifcmpeq with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_Cons1) + by (auto simp add: sup_state_Cons1) qed with step - show ?thesis by auto + show ?thesis by auto qed lemma step_mono: