# HG changeset patch # User kleing # Date 965814780 -7200 # Node ID 1f99296758c2dcf621a4c456cfffc9adf7161102 # Parent 8d5221bf765b7e54e29c9b4e90768da37f59fdc9 tuned diff -r 8d5221bf765b -r 1f99296758c2 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Tue Aug 08 16:57:44 2000 +0200 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Wed Aug 09 11:53:00 2000 +0200 @@ -36,6 +36,8 @@ wf_prog (\\G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (phi C sig)) G" + + lemma wt_jvm_progD: "wt_jvm_prog G phi \\ (\\wt. wf_prog wt G)" by (unfold wt_jvm_prog_def, blast) diff -r 8d5221bf765b -r 1f99296758c2 src/HOL/MicroJava/BV/LBVComplete.thy --- a/src/HOL/MicroJava/BV/LBVComplete.thy Tue Aug 08 16:57:44 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy Wed Aug 09 11:53:00 2000 +0200 @@ -6,11 +6,7 @@ header {* Completeness of the LBV *} -theory LBVComplete = BVSpec + LBVSpec: - - -ML_setup {* bind_thm ("widen_RefT", widen_RefT) *} -ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *} +theory LBVComplete = BVSpec + LBVSpec + StepMono: constdefs @@ -66,52 +62,60 @@ make_cert b (Phi C sig)" -lemma length_ofn: "\\n. length (option_filter_n l P n) = length l" +lemmas [simp del] = split_paired_Ex + +lemma length_ofn [rulify]: "\\n. length (option_filter_n l P n) = length l" by (induct l) auto -lemma is_approx_option_filter_n: -"\\n. is_approx (option_filter_n a P n) a" (is "?P a") -proof (induct a) - show "?P []" by (auto simp add: is_approx_def) - fix l ls - assume Cons: "?P ls" - - show "?P (l#ls)" - proof (unfold is_approx_def, intro allI conjI impI) - fix n - show "length (option_filter_n (l # ls) P n) = length (l # ls)" - by (simp only: length_ofn) +lemma is_approx_option_filter: "is_approx (option_filter l P) l" +proof - + { + fix a n + have "\\n. is_approx (option_filter_n a P n) a" (is "?P a") + proof (induct a) + show "?P []" by (auto simp add: is_approx_def) + + fix l ls + assume Cons: "?P ls" - fix m - assume "m < length (option_filter_n (l # ls) P n)" - hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp - - show "option_filter_n (l # ls) P n ! m = None \\ - option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)" - proof (cases "m") - assume "m = 0" - with m show ?thesis by simp - next - fix m' assume Suc: "m = Suc m'" - from Cons - show ?thesis - proof (unfold is_approx_def, elim allE impE conjE) - from m Suc - show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn) - - assume "option_filter_n ls P (Suc n) ! m' = None \\ - option_filter_n ls P (Suc n) ! m' = Some (ls ! m')" - with m Suc - show ?thesis by auto + show "?P (l#ls)" + proof (unfold is_approx_def, intro allI conjI impI) + fix n + show "length (option_filter_n (l # ls) P n) = length (l # ls)" + by (simp only: length_ofn) + + fix m + assume "m < length (option_filter_n (l # ls) P n)" + hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp + + show "option_filter_n (l # ls) P n ! m = None \\ + option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)" + proof (cases "m") + assume "m = 0" + with m show ?thesis by simp + next + fix m' assume Suc: "m = Suc m'" + from Cons + show ?thesis + proof (unfold is_approx_def, elim allE impE conjE) + from m Suc + show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn) + + assume "option_filter_n ls P (Suc n) ! m' = None \\ + option_filter_n ls P (Suc n) ! m' = Some (ls ! m')" + with m Suc + show ?thesis by auto + qed + qed qed qed - qed + } + + thus ?thesis + by (auto simp add: option_filter_def) qed -lemma is_approx_option_filter: "is_approx (option_filter l P) l" - by (simp add: option_filter_def is_approx_option_filter_n) - lemma option_filter_Some: "\\n < length l; P n\\ \\ option_filter l P ! n = Some (l!n)" proof - @@ -200,11 +204,8 @@ by (clarsimp simp add: fits_def contains_dead_def contains_targets_def) - -lemmas [trans] = sup_state_trans - lemma wtl_inst_mono: -"\\wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; wf_prog wf_mb G; +"\\wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; G \\ s2 <=s s1; i = ins!pc\\ \\ \\ s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\ (G \\ s2' <=s s1')"; proof - @@ -270,6 +271,42 @@ with pc show ?thesis by simp qed + +lemma wtl_option_mono: +"\\wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; + pc < length ins; G \\ s2 <=s s1; i = ins!pc\\ \\ + \\ s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\ (G \\ s2' <=s s1')" +proof - + assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and + fits: "fits ins cert phi" "pc < length ins" + "G \\ s2 <=s s1" "i = ins!pc" + + show ?thesis + proof (cases "cert!pc") + case None + with wtl fits; + show ?thesis; + by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+); + next + case Some + with wtl fits; + + have G: "G \\ s2 <=s a" + by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+) + + from Some wtl + have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def) + + with G fits + have "\\ s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\ (G \\ s2' <=s s1')" + by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+); + + with Some G; + show ?thesis; by (simp add: wtl_inst_option_def); + qed +qed + + lemma wt_instr_imp_wtl_inst: "\\wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi; @@ -296,7 +333,7 @@ from wt fits pc have cert: "!!pc'. \\pc' \\ succs (ins!pc) pc; pc' < max_pc; pc' \\ pc+1\\ \\ cert!pc' \\ None \\ G \\ ?s' <=s the (cert!pc')" - by (auto dest: fitsD simp add: wt_instr_def simp del: split_paired_Ex) + by (auto dest: fitsD simp add: wt_instr_def) show ?thesis proof (cases "pc+1 \\ succs (ins!pc) pc") @@ -358,143 +395,87 @@ qed -lemma wtl_option_mono: -"\\wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; - wf_prog wf_mb G; G \\ s2 <=s s1; i = ins!pc\\ \\ - \\ s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\ (G \\ s2' <=s s1')" -proof - - assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and - fits: "fits ins cert phi" "pc < length ins" - "wf_prog wf_mb G" "G \\ s2 <=s s1" "i = ins!pc" - - show ?thesis - proof (cases "cert!pc") - case None - with wtl fits; - show ?thesis; - by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+); - next - case Some - with wtl fits; - - have G: "G \\ s2 <=s a" - by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+) - - from Some wtl - have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def) +text {* + \medskip + Main induction over the instruction list. +*} - with G fits - have "\\ s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\ (G \\ s2' <=s s1')" - by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+); - - with Some G; - show ?thesis; by (simp add: wtl_inst_option_def); - qed -qed - - -(* main induction over instruction list *) theorem wt_imp_wtl_inst_list: -"\\ pc. (\\pc'. pc' < length ins \\ wt_instr (ins ! pc') G rT phi (pc+length ins) (pc+pc')) \\ - wf_prog wf_mb G \\ - fits all_ins cert phi \\ (\\ l. pc = length l \\ all_ins=l@ins) \\ pc < length all_ins \\ +"\\ pc. (\\pc'. pc' < length all_ins \\ wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \\ + fits all_ins cert phi \\ + (\\l. pc = length l \\ all_ins = l@ins) \\ + pc < length all_ins \\ (\\ s. (G \\ s <=s (phi!pc)) \\ - (\\s'. wtl_inst_list ins G rT s s' cert (pc+length ins) pc))" -(is "\\pc. ?C pc ins" is "?P ins"); -proof (induct "?P" "ins"); - case Nil; - show "?P []"; by simp; -next; - case Cons; + (\\s'. wtl_inst_list ins G rT s s' cert (length all_ins) pc))" +(is "\\pc. ?wt \\ ?fits \\ ?l pc ins \\ ?len pc \\ ?wtl pc ins" is "\\pc. ?C pc ins" is "?P ins") +proof (induct "?P" "ins") + case Nil + show "?P []" by simp +next + fix i ins' + assume Cons: "?P ins'" - show "?P (a#list)"; - proof (intro allI impI, elim exE conjE); - fix pc s l; - assume 1: "wf_prog wf_mb G" "fits all_ins cert phi"; - assume 2: "pc < length all_ins" "G \\ s <=s phi ! pc" - "all_ins = l @ a # list" "pc = length l"; + show "?P (i#ins')" + proof (intro allI impI, elim exE conjE) + fix pc s l + assume wt : "\\pc'. pc' < length all_ins \\ + wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'" + assume fits: "fits all_ins cert phi" + assume G : "G \\ s <=s phi ! pc" + assume l : "pc < length all_ins" - from Cons; - have IH: "?C (Suc pc) list"; by blast; + assume pc : "all_ins = l@i#ins'" "pc = length l" + hence i : "all_ins ! pc = i" + by (simp add: nth_append) - assume 3: "\\pc'. pc' < length (a # list) \\ - wt_instr ((a # list) ! pc') G rT phi (pc + length (a # list)) (pc + pc')"; - hence 4: "\\pc'. pc' < length list \\ - wt_instr (list ! pc') G rT phi (Suc pc + length list) (Suc pc + pc')"; by auto; + from l wt + have "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast - from 2; - have 5: "a = all_ins ! pc"; by (simp add: nth_append); - - - show "\\s'. wtl_inst_list (a # list) G rT s s' cert (pc + length (a # list)) pc"; - proof (cases list); - case Nil; - - with 1 2 3 5; - have "\\s'. wtl_inst_option a G rT (phi ! pc) s' cert (Suc (length l)) pc"; - by - (rule wt_instr_imp_wtl_option [elimify], force+); + with fits l + obtain s1 where + "wtl_inst_option (all_ins!pc) G rT (phi!pc) s1 cert (length all_ins) pc" and + s1: "G \\ s1 <=s phi ! (Suc pc)" + by - (drule wt_instr_imp_wtl_option, assumption+, simp, elim exE conjE, simp) + + with fits l + obtain s2 where + o: "wtl_inst_option (all_ins!pc) G rT s s2 cert (length all_ins) pc" + and "G \\ s2 <=s s1" + by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that) - with Nil 1 2 5; - have "\\s'. wtl_inst_option a G rT s s' cert (Suc (length l)) pc"; - by elim (rule wtl_option_mono [elimify], force+); - - with Nil 2; - show ?thesis; by auto; - next; - fix i' ins'; - assume Cons2: "list = i' # ins'"; - - with IH 1 2 3; - have * : "\\ s. (G \\ s <=s (phi!(Suc pc))) \\ - (\\s'. wtl_inst_list list G rT s s' cert ((Suc pc)+length list) (Suc pc))"; - by (elim impE) force+; + with s1 + have G': "G \\ s2 <=s phi ! (Suc pc)" + by - (rule sup_state_trans, auto) - from 3; - have "wt_instr a G rT phi (pc + length (a # list)) pc"; by auto; - - with 1 2 5; - have "\\s1'. wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc \\ G \\ s1' <=s phi ! Suc pc"; - by - (rule wt_instr_imp_wtl_option [elimify], assumption+, simp+); - - hence "\\s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\ - (G \\ s1 <=s (phi ! (Suc pc)))" (* \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s))"; *) - proof elim; - fix s1'; - assume "wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc" and - a :"G \\ s1' <=s phi ! Suc pc"; - with 1 2 5; - have "\\s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\ - ((G \\ s1 <=s s1'))" (* \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s))"; *) - by - (rule wtl_option_mono [elimify], simp+); + from Cons + have "?C (Suc pc) ins'" by blast + with wt fits pc + have IH: "?len (Suc pc) \\ ?wtl (Suc pc) ins'" by auto - with a; - show ?thesis; - proof (elim, intro); - fix s1; - assume "G \\ s1 <=s s1'" "G \\ s1' <=s phi ! Suc pc"; - show "G \\ s1 <=s phi ! Suc pc"; by (rule sup_state_trans); - qed auto; - qed - - thus ?thesis - proof (elim exE conjE); - fix s1; - assume wto: "wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc"; - assume Gs1: "G \\ s1 <=s phi ! Suc pc" (* \\ (\\s. cert ! Suc pc = Some s \\ G \\ s1 <=s s)"; *) - - with * - have "\\s'. wtl_inst_list list G rT s1 s' cert ((Suc pc)+length list) (Suc pc)"; by blast - - with wto; - show ?thesis; by (auto simp del: split_paired_Ex); - qed + show "\\s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc" + proof (cases "?len (Suc pc)") + case False + with pc + have "ins' = []" by simp + with i o + show ?thesis by auto + next + case True + with IH + have "?wtl (Suc pc) ins'" by blast + with G' + obtain s' where + "wtl_inst_list ins' G rT s2 s' cert (length all_ins) (Suc pc)" + by - (elim allE impE, auto) + with i o + show ?thesis by auto qed qed qed - + lemma fits_imp_wtl_method_complete: -"\\wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\ \\ wtl_method G C pTs rT mxl ins cert"; +"\\wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\ \\ wtl_method G C pTs rT mxl ins cert" by (simp add: wt_method_def wtl_method_def del: split_paired_Ex) (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex); @@ -560,5 +541,6 @@ qed; qed +lemmas [simp] = split_paired_Ex end diff -r 8d5221bf765b -r 1f99296758c2 src/HOL/MicroJava/BV/Step.thy --- a/src/HOL/MicroJava/BV/Step.thy Tue Aug 08 16:57:44 2000 +0200 +++ b/src/HOL/MicroJava/BV/Step.thy Wed Aug 09 11:53:00 2000 +0200 @@ -10,7 +10,7 @@ theory Step = Convert : -(* effect of instruction on the state type *) +text "Effect of instruction on the state type" consts step :: "instr \\ jvm_prog \\ state_type \\ state_type option" @@ -39,7 +39,7 @@ "step (i,G,s) = None" -(* conditions under which step is applicable *) +text "Conditions under which step is applicable" consts app :: "instr \\ jvm_prog \\ ty \\ state_type \\ bool" @@ -84,7 +84,8 @@ "app (i,G,rT,s) = False" -(* p_count of successor instructions *) +text {* \isa{p_count} of successor instructions *} + consts succs :: "instr \\ p_count \\ p_count set" @@ -131,15 +132,21 @@ with * show ?thesis by (auto dest: 0) qed +text {* +\mdeskip +simp rules for \isa{app} without patterns, better suited for proofs +\medskip +*} + lemma appStore[simp]: -"app (Store idx, G, rT, s) = (\\ ts ST LT. s = (ts#ST,LT) \\ idx < length LT)" (is "?app s = ?P s") +"app (Store idx, G, rT, s) = (\\ ts ST LT. s = (ts#ST,LT) \\ idx < length LT)" by (cases s, cases "2 < length (fst s)", auto dest: 1 2) lemma appGetField[simp]: "app (Getfield F C, G, rT, s) = (\\ oT ST LT. s = (oT#ST, LT) \\ is_class G C \\ fst (the (field (G,C) F)) = C \\ - field (G,C) F \\ None \\ G \\ oT \\ (Class C))" (is "?app s = ?P s") + field (G,C) F \\ None \\ G \\ oT \\ (Class C))" by (cases s, cases "2 < length (fst s)", auto dest: 1 2) @@ -147,36 +154,36 @@ "app (Putfield F C, G, rT, s) = (\\ vT oT ST LT. s = (vT#oT#ST, LT) \\ is_class G C \\ field (G,C) F \\ None \\ fst (the (field (G,C) F)) = C \\ G \\ oT \\ (Class C) \\ - G \\ vT \\ (snd (the (field (G,C) F))))" (is "?app s = ?P s") + G \\ vT \\ (snd (the (field (G,C) F))))" by (cases s, cases "2 < length (fst s)", auto dest: 1 2) lemma appCheckcast[simp]: -"app (Checkcast C, G, rT, s) = (\\rT ST LT. s = (RefT rT#ST,LT) \\ is_class G C)" (is "?app s = ?P s") +"app (Checkcast C, G, rT, s) = (\\rT ST LT. s = (RefT rT#ST,LT) \\ is_class G C)" by (cases s, cases "fst s", simp, cases "hd (fst s)", auto) lemma appPop[simp]: -"app (Pop, G, rT, s) = (\\ts ST LT. s = (ts#ST,LT))" (is "?app s = ?P s") +"app (Pop, G, rT, s) = (\\ts ST LT. s = (ts#ST,LT))" by (cases s, cases "2 < length (fst s)", auto dest: 1 2) lemma appDup[simp]: -"app (Dup, G, rT, s) = (\\ts ST LT. s = (ts#ST,LT))" (is "?app s = ?P s") +"app (Dup, G, rT, s) = (\\ts ST LT. s = (ts#ST,LT))" by (cases s, cases "2 < length (fst s)", auto dest: 1 2) lemma appDup_x1[simp]: -"app (Dup_x1, G, rT, s) = (\\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" (is "?app s = ?P s") +"app (Dup_x1, G, rT, s) = (\\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" by (cases s, cases "2 < length (fst s)", auto dest: 1 2) lemma appDup_x2[simp]: -"app (Dup_x2, G, rT, s) = (\\ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"(is "?app s = ?P s") +"app (Dup_x2, G, rT, s) = (\\ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))" by (cases s, cases "2 < length (fst s)", auto dest: 1 2) lemma appSwap[simp]: -"app (Swap, G, rT, s) = (\\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" (is "?app s = ?P s") +"app (Swap, G, rT, s) = (\\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" by (cases s, cases "2 < length (fst s)", auto dest: 1 2) @@ -250,469 +257,5 @@ qed lemmas [simp del] = app_invoke -lemmas [trans] = sup_loc_trans - -ML_setup {* bind_thm ("widen_RefT", widen_RefT) *} -ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *} - - - -lemma app_step_some: -"\\app (i,G,rT,s); succs i pc \\ {} \\ \\ step (i,G,s) \\ None"; -by (cases s, cases i, auto) - -lemma sup_state_length: -"G \\ s2 <=s s1 \\ length (fst s2) = length (fst s1) \\ length (snd s2) = length (snd s1)" - by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd) - -lemma PrimT_PrimT: "(G \\ xb \\ PrimT p) = (xb = PrimT p)" -proof - show "xb = PrimT p \\ G \\ xb \\ PrimT p" by blast - - show "G\\ xb \\ PrimT p \\ xb = PrimT p" - proof (cases xb) - fix prim - assume "xb = PrimT prim" "G\\xb\\PrimT p" - thus ?thesis by simp - next - fix ref - assume "G\\xb\\PrimT p" "xb = RefT ref" - thus ?thesis by simp (rule widen_RefT [elimify], auto) - qed -qed - -lemma sup_loc_some [rulify]: -"\\ y n. (G \\ b <=l y) \\ n < length y \\ y!n = Some t \\ (\\t. b!n = Some t \\ (G \\ (b!n) <=o (y!n)))" (is "?P b") -proof (induct "?P" b) - show "?P []" by simp - - case Cons - show "?P (a#list)" - proof (clarsimp simp add: list_all2_Cons1 sup_loc_def) - fix z zs n - assume * : - "G \\ a <=o z" "list_all2 (sup_ty_opt G) list zs" - "n < Suc (length zs)" "(z # zs) ! n = Some t" - - show "(\\t. (a # list) ! n = Some t) \\ G \\(a # list) ! n <=o Some t" - proof (cases n) - case 0 - with * show ?thesis by (simp add: sup_ty_opt_some) - next - case Suc - with Cons * - show ?thesis by (simp add: sup_loc_def) - qed - qed -qed - - -lemma all_widen_is_sup_loc: -"\\b. length a = length b \\ (\\x\\set (zip a b). x \\ widen G) = (G \\ (map Some a) <=l (map Some 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)" - proof (intro allI impI) - 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: "\\n. n \\ length x \\ (\\a b. x = a@b \\ length a = n)" (is "?P x") -proof (induct "?P" "x") - show "?P []" by simp - - fix l ls assume Cons: "?P ls" - - show "?P (l#ls)" - proof (intro allI impI) - fix n - assume l: "n \\ length (l # ls)" - - 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 - hence "\\a b. ls = a @ b \\ length a = n'" by (rule Cons [rulify]) - 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 - 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 [rulify]) - 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 -qed - - -lemma app_mono: -"\\G \\ s2 <=s s1; app (i, G, rT, s1)\\ \\ app (i, G, rT, s2)"; -proof - - assume G: "G \\ s2 <=s s1" - assume app: "app (i, G, rT, s1)" - - show ?thesis - proof (cases i) - case Load - - from G - have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length) - - from G Load app - have "G \\ snd s2 <=l snd s1" by (auto simp add: sup_state_def) - - with G Load app l - show ?thesis by clarsimp (drule sup_loc_some, simp+) - next - case Store - with G app - show ?thesis - by - (cases s2, - auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def) - next - case Bipush - thus ?thesis by simp - next - case Aconst_null - thus ?thesis by simp - next - case New - with app - show ?thesis by simp - next - case Getfield - with app G - show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans) - next - case Putfield - - with app - obtain vT oT ST LT b - where s1: "s1 = (vT # oT # ST, LT)" and - "field (G, cname) vname = Some (cname, b)" - "is_class G cname" and - oT: "G\\ oT\\ (Class cname)" and - vT: "G\\ vT\\ b" - by simp (elim exE conjE, simp, rule that) - moreover - from s1 G - obtain vT' oT' ST' LT' - 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) - moreover - from vT' vT - have "G \\ vT' \\ b" by (rule widen_trans) - moreover - from oT' oT - have "G\\ oT' \\ (Class cname)" by (rule widen_trans) - ultimately - show ?thesis - by (auto simp add: Putfield) - next - case Checkcast - with app G - 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, clarsimp 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) - next - case Dup - with app G - show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2) - next - case Dup_x1 - with app G - show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2) - next - case Dup_x2 - with app G - show ?thesis - by - (cases s2, clarsimp simp add: sup_state_Cons2) - next - case Swap - with app G - show ?thesis - 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) - next - 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) - next - case Invoke - - with app - obtain apTs X ST LT where - s1: "s1 = (rev apTs @ X # ST, LT)" and - l: "length apTs = length list" and - C: "G \\ X \\ Class cname" and - w: "\\x \\ set (zip apTs list). x \\ widen G" and - m: "method (G, cname) (mname, list) \\ None" - by (simp del: not_None_eq, elim exE conjE) (rule that) - - 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)" - by (simp add: sup_state_length) - hence "\\a b c. (fst s2) = rev a @ b # c \\ length a = length list" - by (rule rev_append_cons [rulify]) - thus ?thesis - 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 - obtain - G': "G \\ (apTs',LT') <=s (apTs,LT)" - "G \\ X' \\ X" "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 Some apTs' <=l map Some apTs" - by (simp add: sup_state_def) - also - from l w - have "G \\ map Some apTs <=l map Some list" - by (simp add: all_widen_is_sup_loc) - finally - have "G \\ map Some apTs' <=l map Some list" . - - with l' - have w': "\\x \\ set (zip apTs' list). x \\ widen G" - by (simp add: all_widen_is_sup_loc) - - from Invoke s2 l' w' C' m - show ?thesis - by simp blast - qed -qed - - -lemma step_mono: -"\\succs i pc \\ {}; app (i,G,rT,s2); G \\ s1 <=s s2\\ \\ - G \\ the (step (i,G,s1)) <=s the (step (i,G,s2))" -proof (cases s1, cases s2) - fix a1 b1 a2 b2 - assume s: "s1 = (a1,b1)" "s2 = (a2,b2)" - assume succs: "succs i pc \\ {}" - assume app2: "app (i,G,rT,s2)" - assume G: "G \\ s1 <=s s2" - - from G app2 - have app1: "app (i,G,rT,s1)" by (rule app_mono) - - from app1 app2 succs - obtain a1' b1' a2' b2' - where step: "step (i,G,s1) = Some (a1',b1')" "step (i,G,s2) = Some (a2',b2')"; - by (auto dest: app_step_some); - - have "G \\ (a1',b1') <=s (a2',b2')" - proof (cases i) - case Load - - with s app1 - obtain y where - y: "nat < length b1" "b1 ! nat = Some y" by clarsimp - - from Load s app2 - obtain y' where - y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp - - from G s - have "G \\ b1 <=l b2" by (simp add: sup_state_def) - - 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_def) - next - case Store - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_def sup_loc_update) - next - case Bipush - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case New - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case Aconst_null - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case Getfield - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case Putfield - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case Checkcast - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case Invoke - - with s app1 - obtain a X ST where - s1: "s1 = (a @ X # ST, b1)" and - l: "length a = length list" - by (simp, elim exE conjE, simp) - - 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) - - from l l' - have lr: "length a = length a'" by simp - - 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 - - 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_def) - next - case Return - with succs have "False" by simp - thus ?thesis by blast - next - case Pop - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case Dup - with G s step app1 app2 - show ?thesis - by (clarsimp 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 - case Dup_x2 - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case Swap - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case IAdd - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - next - case Goto - with G s step app1 app2 - show ?thesis by simp - next - case Ifcmpeq - with G s step app1 app2 - show ?thesis - by (clarsimp simp add: sup_state_Cons1) - qed - - with step - show ?thesis by auto -qed - - end diff -r 8d5221bf765b -r 1f99296758c2 src/HOL/MicroJava/BV/StepMono.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/MicroJava/BV/StepMono.thy Wed Aug 09 11:53:00 2000 +0200 @@ -0,0 +1,480 @@ +(* Title: HOL/MicroJava/BV/Step.thy + ID: $Id$ + Author: Gerwin Klein + Copyright 2000 Technische Universitaet Muenchen +*) + +header {* Monotonicity of \isa{step} and \isa{app} *} + +theory StepMono = Step : + + +lemmas [trans] = sup_state_trans sup_loc_trans widen_trans + +ML_setup {* bind_thm ("widen_RefT", widen_RefT) *} +ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *} + + +lemma app_step_some: +"\\app (i,G,rT,s); succs i pc \\ {} \\ \\ step (i,G,s) \\ None"; +by (cases s, cases i, auto) + + +lemma sup_state_length: +"G \\ s2 <=s s1 \\ length (fst s2) = length (fst s1) \\ length (snd s2) = length (snd s1)" + by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd) + + +lemma PrimT_PrimT: "(G \\ xb \\ PrimT p) = (xb = PrimT p)" +proof + show "xb = PrimT p \\ G \\ xb \\ PrimT p" by blast + + show "G\\ xb \\ PrimT p \\ xb = PrimT p" + proof (cases xb) + fix prim + assume "xb = PrimT prim" "G\\xb\\PrimT p" + thus ?thesis by simp + next + fix ref + assume "G\\xb\\PrimT p" "xb = RefT ref" + thus ?thesis by simp (rule widen_RefT [elimify], auto) + qed +qed + + +lemma sup_loc_some [rulify]: +"\\ y n. (G \\ b <=l y) \\ n < length y \\ y!n = Some t \\ (\\t. b!n = Some t \\ (G \\ (b!n) <=o (y!n)))" (is "?P b") +proof (induct "?P" b) + show "?P []" by simp + + case Cons + show "?P (a#list)" + proof (clarsimp simp add: list_all2_Cons1 sup_loc_def) + fix z zs n + assume * : + "G \\ a <=o z" "list_all2 (sup_ty_opt G) list zs" + "n < Suc (length zs)" "(z # zs) ! n = Some t" + + show "(\\t. (a # list) ! n = Some t) \\ G \\(a # list) ! n <=o Some t" + proof (cases n) + case 0 + with * show ?thesis by (simp add: sup_ty_opt_some) + next + case Suc + with Cons * + show ?thesis by (simp add: sup_loc_def) + qed + qed +qed + + +lemma all_widen_is_sup_loc: +"\\b. length a = length b \\ (\\x\\set (zip a b). x \\ widen G) = (G \\ (map Some a) <=l (map Some 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)" + proof (intro allI impI) + 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 [rulify]: +"\\n. n \\ length x \\ (\\a b. x = a@b \\ length a = n)" (is "?P x") +proof (induct "?P" "x") + show "?P []" by simp + + fix l ls assume Cons: "?P ls" + + show "?P (l#ls)" + proof (intro allI impI) + fix n + assume l: "n \\ length (l # ls)" + + 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 + hence "\\a b. ls = a @ b \\ length a = n'" by (rule Cons [rulify]) + 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 + 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 +qed + + +lemma app_mono: +"\\G \\ s2 <=s s1; app (i, G, rT, s1)\\ \\ app (i, G, rT, s2)"; +proof - + assume G: "G \\ s2 <=s s1" + assume app: "app (i, G, rT, s1)" + + show ?thesis + proof (cases i) + case Load + + from G + have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length) + + from G Load app + have "G \\ snd s2 <=l snd s1" by (auto simp add: sup_state_def) + + with G Load app l + show ?thesis by clarsimp (drule sup_loc_some, simp+) + next + case Store + with G app + show ?thesis + by - (cases s2, + auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def) + next + case Bipush + thus ?thesis by simp + next + case Aconst_null + thus ?thesis by simp + next + case New + with app + show ?thesis by simp + next + case Getfield + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans) + next + case Putfield + + with app + obtain vT oT ST LT b + where s1: "s1 = (vT # oT # ST, LT)" and + "field (G, cname) vname = Some (cname, b)" + "is_class G cname" and + oT: "G\\ oT\\ (Class cname)" and + vT: "G\\ vT\\ b" + by simp (elim exE conjE, simp, rule that) + moreover + from s1 G + obtain vT' oT' ST' LT' + 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) + moreover + from vT' vT + have "G \\ vT' \\ b" by (rule widen_trans) + moreover + from oT' oT + have "G\\ oT' \\ (Class cname)" by (rule widen_trans) + ultimately + show ?thesis + by (auto simp add: Putfield) + next + case Checkcast + with app G + 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, clarsimp 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) + next + case Dup + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2) + next + case Dup_x1 + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2) + next + case Dup_x2 + with app G + show ?thesis + by - (cases s2, clarsimp simp add: sup_state_Cons2) + next + case Swap + with app G + show ?thesis + 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) + next + 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) + next + case Invoke + + with app + obtain apTs X ST LT where + s1: "s1 = (rev apTs @ X # ST, LT)" and + l: "length apTs = length list" and + C: "G \\ X \\ Class cname" and + w: "\\x \\ set (zip apTs list). x \\ widen G" and + m: "method (G, cname) (mname, list) \\ None" + by (simp del: not_None_eq, elim exE conjE) (rule that) + + 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)" + by (simp add: sup_state_length) + hence "\\a b c. (fst s2) = rev a @ b # c \\ length a = length list" + by (rule rev_append_cons [rulify]) + thus ?thesis + 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 + 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' \\