# HG changeset patch # User wenzelm # Date 968004107 -7200 # Node ID e9fb6d44a4901d04cd38417f68f5a88503483c47 # Parent 71de955e8fc92621673b6e05528b8373682a59d8 tuned; diff -r 71de955e8fc9 -r e9fb6d44a490 doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Sun Sep 03 20:01:27 2000 +0200 +++ b/doc-src/IsarRef/conversion.tex Sun Sep 03 20:01:47 2000 +0200 @@ -21,7 +21,9 @@ % \texttt{} & & \\ \texttt{stac}~a~1 & & subst~a \\ \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\ - \texttt{split_all_tac} & \ll & clarify & \Text{(HOL)} \\ + \texttt{split_all_tac} & & simp~(no_asm_simp)~only: split_paired_all & \Text{(HOL)} \\ + & \approx & simp~only: split_tupled_all & \Text{(HOL)} \\ + & \ll & clarify & \Text{(HOL)} \\ \end{matharray} diff -r 71de955e8fc9 -r e9fb6d44a490 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Sep 03 20:01:27 2000 +0200 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Sep 03 20:01:47 2000 +0200 @@ -21,7 +21,7 @@ apply (unfold correct_state_def Let_def correct_frame_def) apply simp apply (blast intro: wt_jvm_prog_impl_wt_instr) -. +done lemma Load_correct: "\ wf_prog wt G; @@ -36,7 +36,7 @@ apply (rule approx_loc_imp_approx_val_sup) apply simp+ apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) -. +done lemma Store_correct: "\ wf_prog wt G; @@ -50,7 +50,7 @@ apply (rule conjI) apply (blast intro: approx_stk_imp_approx_stk_sup) apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup) -. +done lemma conf_Intg_Integer [iff]: @@ -65,10 +65,10 @@ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ -\ G,phi \JVM state'\"; +\ G,phi \JVM state'\" apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons) apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) -. +done lemma NT_subtype_conv: "G \ NT \ T = (T=NT \ (\C. T = Class C))" @@ -78,7 +78,7 @@ apply auto apply (case_tac R) apply auto - . + done note l = this show ?thesis @@ -92,12 +92,12 @@ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ -\ G,phi \JVM state'\"; +\ G,phi \JVM state'\" apply (clarsimp simp add: defs1 map_eq_Cons) apply (rule conjI) apply (force simp add: approx_val_Null NT_subtype_conv) apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) -. +done lemma Cast_conf2: @@ -110,7 +110,7 @@ apply (clarsimp simp add: conf_def obj_ty_def) apply (cases v) apply (auto intro: null rtrancl_trans) -. +done lemma Checkcast_correct: @@ -123,7 +123,7 @@ \ G,phi \JVM state'\" apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def) apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2) -. +done lemma Getfield_correct: @@ -133,7 +133,7 @@ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ -\ G,phi \JVM state'\"; +\ G,phi \JVM state'\" apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split) apply (frule conf_widen) apply assumption+ @@ -144,7 +144,7 @@ apply assumption+ apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def) apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) -. +done lemma Putfield_correct: "\ wf_prog wt G; @@ -153,7 +153,7 @@ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; G,phi \JVM (None, hp, (stk,loc,C,sig,pc)#frs)\ \ -\ G,phi \JVM state'\"; +\ G,phi \JVM state'\" apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split) apply (clarsimp simp add: approx_val_def) apply (frule conf_widen) @@ -162,11 +162,12 @@ apply assumption apply (drule conf_RefTD) apply clarsimp -apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup - approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup - hconf_imp_hconf_field_update - correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields) -. +apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap + approx_stk_imp_approx_stk_sup + approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup + hconf_imp_hconf_field_update + correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields) +done lemma collapse_paired_All: "(\x y. P(x,y)) = (\z. P z)" @@ -190,7 +191,7 @@ correct_init_obj simp add: NT_subtype_conv approx_val_def conf_def fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 split: option.split) -. +done (****** Method Invocation ******) @@ -442,14 +443,14 @@ \ G,phi \JVM state'\" apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm) apply (frule wt_jvm_prog_impl_wt_instr) -apply (tactic "EVERY1[atac, etac Suc_lessD]") +apply (assumption, erule Suc_lessD) apply (unfold wt_jvm_prog_def) -apply (tactic {* fast_tac (claset() - addDs [thm "subcls_widen_methd"] - addEs [rotate_prems 1 widen_trans] - addIs [conf_widen] - addss (simpset() addsimps [thm "approx_val_def",thm "append_eq_conv_conj", map_eq_Cons]@thms "defs1")) 1 *}) -. +apply (fastsimp + dest: subcls_widen_methd + elim: widen_trans [COMP swap_prems_rl] + intro: conf_widen + simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1) +done lemmas [simp] = map_append @@ -463,7 +464,7 @@ \ G,phi \JVM state'\" apply (clarsimp simp add: defs1) apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) -. +done lemma Ifcmpeq_correct: @@ -476,7 +477,7 @@ \ G,phi \JVM state'\" apply (clarsimp simp add: defs1) apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) -. +done lemma Pop_correct: "\ wf_prog wt G; @@ -488,7 +489,7 @@ \ G,phi \JVM state'\" apply (clarsimp simp add: defs1) apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) -. +done lemma Dup_correct: "\ wf_prog wt G; @@ -501,7 +502,7 @@ apply (clarsimp simp add: defs1 map_eq_Cons) apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup simp add: defs1 map_eq_Cons) -. +done lemma Dup_x1_correct: "\ wf_prog wt G; @@ -514,7 +515,7 @@ apply (clarsimp simp add: defs1 map_eq_Cons) apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup simp add: defs1 map_eq_Cons) -. +done lemma Dup_x2_correct: "\ wf_prog wt G; @@ -527,7 +528,7 @@ apply (clarsimp simp add: defs1 map_eq_Cons) apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup simp add: defs1 map_eq_Cons) -. +done lemma Swap_correct: "\ wf_prog wt G; @@ -540,7 +541,7 @@ apply (clarsimp simp add: defs1 map_eq_Cons) apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup simp add: defs1 map_eq_Cons) -. +done lemma IAdd_correct: "\ wf_prog wt G; @@ -552,7 +553,7 @@ \ G,phi \JVM state'\" apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def) apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup) -. +done (** instr correct **) @@ -575,7 +576,7 @@ Checkcast_correct Getfield_correct Putfield_correct New_correct Goto_correct Ifcmpeq_correct Pop_correct Dup_correct Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+ -. +done (** Main **) @@ -588,19 +589,19 @@ lemma BV_correct_1 [rulify]: "\state. \ wt_jvm_prog G phi; G,phi \JVM state\\ - \ exec (G,state) = Some state' \ G,phi \JVM state'\"; -apply (tactic "split_all_tac 1") + \ exec (G,state) = Some state' \ G,phi \JVM state'\" +apply (simp only: split_tupled_all) apply (rename_tac xp hp frs) apply (case_tac xp) apply (case_tac frs) apply simp - apply (tactic "split_all_tac 1") - apply (tactic "hyp_subst_tac 1") + apply (simp only: split_tupled_all) + apply hypsubst apply (frule correct_state_impl_Some_method) apply (force intro: instr_correct) apply (case_tac frs) -apply simp+ -. +apply simp_all +done lemma L0: @@ -613,7 +614,7 @@ apply (drule L0) apply assumption apply (fast intro: BV_correct_1) -. +done theorem BV_correct [rulify]: @@ -622,7 +623,7 @@ apply (erule rtrancl_induct) apply simp apply (auto intro: BV_correct_1) -. +done theorem BV_correct_initial: @@ -631,6 +632,6 @@ apply (drule BV_correct) apply assumption+ apply (simp add: correct_state_def correct_frame_def split_def split: option.splits) -. +done end