# HG changeset patch # User oheimb # Date 946904828 -3600 # Node ID 381716a86fcb9f81fe24a521631c123cfcfc2c49 # Parent 1c8de414b45db523f3de59992bca97276004a969 removed inj_eq from the default simpset again diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/Conform.ML --- a/src/HOL/MicroJava/J/Conform.ML Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/Conform.ML Mon Jan 03 14:07:08 2000 +0100 @@ -75,7 +75,7 @@ ALLGOALS Asm_simp_tac]) RS mp; val conf_widen = prove_goalw thy [conf_def] -"\\G. wf_prog wtm G \\ G,h\\x\\\\T \\ G\\T\\T' \\ G,h\\x\\\\T'" (K [ +"\\G. wf_prog wf_mb G \\ G,h\\x\\\\T \\ G\\T\\T' \\ G,h\\x\\\\T'" (K [ rtac val_.induct 1, ALLGOALS Simp_tac, ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp; @@ -120,7 +120,7 @@ \ (\\a C' fs. a' = Addr a \\ h a = Some (C',fs) \\ G\\Class C'\\Class C)" (K[fast_tac (HOL_cs addDs [non_npD]) 1]); -Goal "a' \\ Null \\ wf_prog wtm G \\ G,h\\a'\\\\RefT t \\\ +Goal "a' \\ Null \\ wf_prog wf_mb G \\ G,h\\a'\\\\RefT t \\\ \ (\\C. t = ClassT C \\ C \\ Object) \\ \ \ (\\a C fs. a' = Addr a \\ h a = Some (C,fs) \\ G\\Class C\\RefT t)"; by (rtac impI 1); @@ -134,7 +134,7 @@ by (Fast_tac 1); qed_spec_mp "non_np_objD'"; -Goal "wf_prog wtm G \\ \\Ts Ts'. list_all2 (conf G h) vs Ts \\ list_all2 (\\T T'. G\\T\\T') Ts Ts' \\ list_all2 (conf G h) vs Ts'"; +Goal "wf_prog wf_mb G \\ \\Ts Ts'. list_all2 (conf G h) vs Ts \\ list_all2 (\\T T'. G\\T\\T') Ts Ts' \\ list_all2 (conf G h) vs Ts'"; by( induct_tac "vs" 1); by( ALLGOALS Clarsimp_tac); by( ALLGOALS (forward_tac [list_all2_lengthD RS sym])); diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/Conform.thy Mon Jan 03 14:07:08 2000 +0100 @@ -26,7 +26,7 @@ hconf :: "'c prog \\ aheap \\ bool" ("_\\h _\\" [51,51] 50) "G\\h h\\ \\ \\a obj. h a = Some obj \\ G,h\\obj\\" - conforms :: "state \\ javam env \\ bool" ("_\\\\_" [51,51] 50) + conforms :: "state \\ java_mb env \\ bool" ("_\\\\_" [51,51] 50) "s\\\\E \\ prg E\\h heap s\\ \\ prg E,heap s\\locals s[\\\\]localT E" end diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/Eval.thy Mon Jan 03 14:07:08 2000 +0100 @@ -10,15 +10,15 @@ Eval = State + consts - eval :: "javam prog \\ (xstate \\ expr \\ val \\ xstate) set" - evals :: "javam prog \\ (xstate \\ expr list \\ val list \\ xstate) set" - exec :: "javam prog \\ (xstate \\ stmt \\ xstate) set" + eval :: "java_mb prog \\ (xstate \\ expr \\ val \\ xstate) set" + evals :: "java_mb prog \\ (xstate \\ expr list \\ val list \\ xstate) set" + exec :: "java_mb prog \\ (xstate \\ stmt \\ xstate) set" syntax - eval :: "[javam prog,xstate,expr,val,xstate] \\ bool "("_\\_ -_\\_\\ _"[51,82,82,82,82]81) - evals:: "[javam prog,xstate,expr list, + eval :: "[java_mb prog,xstate,expr,val,xstate] \\ bool "("_\\_ -_\\_\\ _"[51,82,82,82,82]81) + evals:: "[java_mb prog,xstate,expr list, val list,xstate] \\ bool "("_\\_ -_[\\]_\\ _"[51,82,51,51,82]81) - exec :: "[javam prog,xstate,stmt, xstate] \\ bool "("_\\_ -_\\ _" [51,82,82, 82]81) + exec :: "[java_mb prog,xstate,stmt, xstate] \\ bool "("_\\_ -_\\ _" [51,82,82, 82]81) translations "G\\s -e \\ v\\ (x,s')" == "(s, e, v, _args x s') \\ eval G" diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/JBasis.ML --- a/src/HOL/MicroJava/J/JBasis.ML Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/JBasis.ML Mon Jan 03 14:07:08 2000 +0100 @@ -67,6 +67,10 @@ rotate_tac ~1,asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])]; +Goal "{y. x = Some y} \\ {the x}"; +by Auto_tac; +qed "some_subset_the"; + fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1, asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])]; @@ -114,7 +118,7 @@ Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"; by (induct_tac "l" 1); -by (auto_tac (claset() addDs [fst_in_set_lemma],simpset())); +by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq])); qed_spec_mp "unique_map_inj"; Goal "\\l. unique l \\ unique (map (split (\\k. Pair (k, C))) l)"; diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/JTypeSafe.ML --- a/src/HOL/MicroJava/J/JTypeSafe.ML Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML Mon Jan 03 14:07:08 2000 +0100 @@ -8,7 +8,7 @@ Addsimps [split_beta]; -Goal "\\h a = None; (h, l)\\\\(G, lT); wf_prog wtm G; is_class G C\\ \\ \ +Goal "\\h a = None; (h, l)\\\\(G, lT); wf_prog wf_mb G; is_class G C\\ \\ \ \ (h(a\\(C,(init_vars (fields (G,C))))), l)\\\\(G, lT)"; by( etac conforms_upd_obj 1); by( rewtac oconf_def); @@ -16,7 +16,7 @@ qed "NewC_conforms"; Goalw [cast_ok_def] - "\\ wf_prog wtm G; G,h\\v\\\\Tb; G\\Tb\\? T'; cast_ok G T' h v\\ \ + "\\ wf_prog wf_mb G; G,h\\v\\\\Tb; G\\Tb\\? T'; cast_ok G T' h v\\ \ \ \\ G,h\\v\\\\T'"; by( case_tac1 "v = Null" 1); by( Asm_full_simp_tac 1); @@ -44,7 +44,7 @@ by Auto_tac; qed "Cast_conf"; -Goal "\\ wf_prog wtm G; field (G,C) fn = Some (fd, ft); (h,l)\\\\(G,lT); \ +Goal "\\ wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\\\(G,lT); \ \ x' = None \\ G,h\\a'\\\\Class C; np a' x' = None \\ \\ \ \ G,h\\the (snd (the (h (the_Addr a'))) (fn, fd))\\\\ft"; by( dtac np_NoneD 1); @@ -60,10 +60,10 @@ by( dtac oconf_objD 1); by( atac 1); by Auto_tac; -val FAcc_type_sound = result(); +qed "FAcc_type_sound"; Goal - "\\ wf_prog wtm G; a = the_Addr a'; (c, fs) = the (h a); \ + "\\ wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \ \ (G, lT)\\v\\T'; G\\T'\\ft; \ \ (G, lT)\\aa\\Class C; \ \ field (G,C) fn = Some (fd, ft); h''\\|h'; \ @@ -105,9 +105,9 @@ by( Asm_full_simp_tac 1); by( fast_tac (HOL_cs addIs [conf_widen]) 1); by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1); -val FAss_type_sound = result(); +qed "FAss_type_sound"; -Goalw [wf_mhead_def] "\\ wf_prog wtm G; list_all2 (conf G h) pvs pTs; \ +Goalw [wf_mhead_def] "\\ wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \ \ list_all2 (\\T T'. G\\T\\T') pTs pTs'; wf_mhead G (mn,pTs') rT; \ \ length pTs' = length pns; nodups pns; \ \ Ball (set lvars) (split (\\vn. is_type G)) \ @@ -145,7 +145,7 @@ by( EVERY'[forward_tac [hext_objD], atac] 1); by( Clarsimp_tac 1); by( EVERY'[dtac Call_lemma, atac, atac] 1); -by( clarsimp_tac (claset(),simpset() addsimps [wt_java_mdecl_def])1); +by( clarsimp_tac (claset(),simpset() addsimps [wf_java_mdecl_def])1); by( thin_tac "method ?sig ?x = ?y" 1); by( EVERY'[dtac spec, etac impE] 1); by( mp_tac 2); diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/TypeRel.ML --- a/src/HOL/MicroJava/J/TypeRel.ML Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/TypeRel.ML Mon Jan 03 14:07:08 2000 +0100 @@ -14,12 +14,6 @@ \ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})" (K [Auto_tac]); -context Option.thy; -Goal "{y. x = Some y} \\ {the x}"; -by Auto_tac; -val some_subset_the = result(); -context thy; - Goal "finite (subcls1 G)"; by(stac subcls1_def2 1); by( rtac finite_SigmaI 1); @@ -38,21 +32,11 @@ auto_tac (claset() addDs lemmata, simpset())]); -(*#### patch for Isabelle98-1*) -val major::prems = goal Trancl.thy - "\\ (x,y) \\ r^+; \ -\ \\x y. (x,y) \\ r \\ P x y; \ -\ \\x y z. \\ (x,y) \\ r^+; P x y; (y,z) \\ r^+; P y z \\ \\ P x z \ -\ \\ \\ P x y"; -by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1); -qed "trancl_trans_induct"; - -Goalw [is_class_def] "G\\C\\C D \\ is_class G C"; +Goalw [is_class_def] "(C,D) \\ (subcls1 G)^+ \\ is_class G C"; by(etac trancl_trans_induct 1); by (auto_tac (HOL_cs addSDs [subcls1D],simpset())); qed "subcls_is_class"; - (* A particular thm about wf; looks like it is an odd instance of something more general *) @@ -66,7 +50,7 @@ by (Fast_tac 1); by(rewrite_goals_tac [wf_def]); by(Blast_tac 1); -val wf_rel_lemma = result(); +qed "wf_rel_lemma"; (* Proving the termination conditions *) @@ -74,7 +58,7 @@ goalw thy [subcls1_rel_def] "wf subcls1_rel"; by(rtac (wf_rel_lemma RS wf_subset) 1); by(Force_tac 1); -val wf_subcls1_rel = result(); +qed "wf_subcls1_rel"; val method_TC = prove_goalw_cterm [subcls1_rel_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs))))) @@ -111,21 +95,19 @@ val widen_Class_NullT = prove_typerel "G\\Class C\\RefT NullT \\ R" [prove_widen_lemma "G\\S\\T \\ S=Class C \\ T=RefT NullT \\ R"]; -val widen_Class_Class = prove_typerel "G\\Class C\\Class cm \\ C=cm | G\\C\\C cm" -[ prove_widen_lemma "G\\S\\T \\ S = Class C \\ T = Class cm \\ C=cm | G\\C\\C cm"]; +val widen_Class_Class = prove_typerel "G\\Class C\\Class cm \\ G\\C\\C cm" +[ prove_widen_lemma "G\\S\\T \\ S = Class C \\ T = Class cm \\ G\\C\\C cm"]; -Goal "\\G\\S\\U; \\C. is_class G C \\ G\\Class C\\Class Object;\ -\\\C. G\\Object\\C C \\ False \\ \\ \\T. G\\U\\T \\ G\\S\\T"; +Goal "G\\S\\U \\ \\T. G\\U\\T \\ G\\S\\T"; by( etac widen.induct 1); by Safe_tac; by( ALLGOALS (forward_tac [widen_Class, widen_RefT])); by Safe_tac; by( rtac widen.null 2); -by( forward_tac [widen_Class_Class] 1); -by Safe_tac; -by( ALLGOALS(EVERY'[etac thin_rl,etac thin_rl, - fast_tac (claset() addIs [widen.subcls,trancl_trans])])); -qed_spec_mp "widen_trans_lemma"; +by(dtac widen_Class_Class 1); +by(rtac widen.subcls 1); +by(eatac rtrancl_trans 1 1); +qed_spec_mp "widen_trans"; val prove_cast_lemma = prove_typerel_lemma [] cast.elim; diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/TypeRel.thy Mon Jan 03 14:07:08 2000 +0100 @@ -21,7 +21,7 @@ translations "G\\C \\C1 D" == "(C,D) \\ subcls1 G" - "G\\C \\C D" == "(C,D) \\ (subcls1 G)^+" + "G\\C \\C D" == "(C,D) \\ (subcls1 G)^*" "G\\S \\ T" == "(S,T) \\ widen G" "G\\S \\? T" == "(S,T) \\ cast G" diff -r 1c8de414b45d -r 381716a86fcb src/HOL/MicroJava/J/WellForm.ML --- a/src/HOL/MicroJava/J/WellForm.ML Thu Dec 23 19:59:50 1999 +0100 +++ b/src/HOL/MicroJava/J/WellForm.ML Mon Jan 03 14:07:08 2000 +0100 @@ -5,76 +5,63 @@ *) val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def] - "\\X. \\class G C = Some c; wf_prog wtm G\\ \\ wf_cdecl wtm G (C,c)" (K [ + "\\X. \\class G C = Some c; wf_prog wf_mb G\\ \\ wf_cdecl wf_mb G (C,c)" (K [ Asm_full_simp_tac 1, fast_tac (set_cs addDs [get_in_set]) 1]); val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def] - "\\X. wf_prog wtm G \\ class G Object = Some (None, [], [])" (K [ + "\\X. wf_prog wf_mb G \\ class G Object = Some (None, [], [])" (K [ safe_tac set_cs, dtac in_set_get 1, Auto_tac]); Addsimps [class_Object]; val is_class_Object = prove_goalw thy [is_class_def] - "\\X. wf_prog wtm G \\ is_class G Object" (K [Asm_simp_tac 1]); + "\\X. wf_prog wf_mb G \\ is_class G Object" (K [Asm_simp_tac 1]); Addsimps [is_class_Object]; -Goal "\\G\\C\\C1D; wf_prog wtm G\\ \\ D \\ C \\ \\ G\\D\\C C"; +Goal "\\G\\C\\C1D; wf_prog wf_mb G\\ \\ D \\ C \\ \\(D,C)\\(subcls1 G)^+"; by( forward_tac [r_into_trancl] 1); by( dtac subcls1D 1); by( strip_tac1 1); -by( dtac class_wf 1); -by( atac 1); +by( datac class_wf 1 1); by( rewtac wf_cdecl_def); -by( Clarsimp_tac 1); +by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] + delsimps [reflcl_trancl]) 1); qed "subcls1_wfD"; val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] -"\\X. \\wf_cdecl wtm G (C, sc, r); C \\ Object\\ \\ \\D. sc = Some D \\ is_class G D" (K [ +"\\X. \\wf_cdecl wf_mb G (C, sc, r); C \\ Object\\ \\ \\D. sc = Some D \\ is_class G D" (K [ pair_tac "r" 1, Asm_full_simp_tac 1, strip_tac1 1, option_case_tac 1, Fast_tac 1]); -local -val lemma = prove_goal thy "\\X. \\wf_prog wtm G; G\\C\\C D\\ \\ C=Object \\ R" (K [ - etac trancl_trans_induct 1, - atac 2, - rewtac subcls1_def, - Auto_tac]); -in -val subcls_Object = prove_goal thy "\\X. \\wf_prog wtm G; G\\Object\\C C\\ \\ R" (K [ - etac (lemma RS mp) 1, - Auto_tac]); -end; - -Goal "\\wf_prog wt G; G\\C\\C D\\ \\ \\ G\\D\\C C"; +Goal "\\wf_prog wf_mb G; (C,D)\\(subcls1 G)^+\\ \\ \\(D,C)\\(subcls1 G)^+"; by(etac tranclE 1); -by(ALLGOALS(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans]))); +by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans]))); qed "subcls_asym"; -val subcls_irrefl = prove_goal thy "\\X. \\wf_prog wtm G; G\\C\\C D\\ \\ C \\ D" (K [ +val subcls_irrefl = prove_goal thy "\\X. \\wf_prog wf_mb G; (C,D)\\(subcls1 G)^+\\ \\ C \\ D" (K [ etac trancl_trans_induct 1, fast_tac (HOL_cs addDs [subcls1_wfD]) 1, fast_tac (HOL_cs addDs [subcls_asym]) 1]); val acyclic_subcls1 = prove_goalw thy [acyclic_def] - "\\X. wf_prog wt G \\ acyclic (subcls1 G)" (K [ + "\\X. wf_prog wf_mb G \\ acyclic (subcls1 G)" (K [ strip_tac1 1, fast_tac (HOL_cs addDs [subcls_irrefl]) 1]); -val wf_subcls1 = prove_goal thy "\\X. wf_prog wtm G \\ wf ((subcls1 G)^-1)" (K [ +val wf_subcls1 = prove_goal thy "\\X. wf_prog wf_mb G \\ wf ((subcls1 G)^-1)" (K [ rtac finite_acyclic_wf 1, stac finite_converse 1, rtac finite_subcls1 1, stac acyclic_converse 1, etac acyclic_subcls1 1]); - val major::prems = goal thy - "\\wf_prog wt G; \\C. \\D. G\\C\\C D \\ P D \\