--- a/src/HOL/IsaMakefile Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/IsaMakefile Thu Feb 01 20:53:13 2001 +0100
@@ -87,7 +87,7 @@
Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy \
- Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
+ Product_Type_lemmas.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \
SetInterval.thy String.thy Sum_Type.ML Sum_Type.thy \
@@ -96,7 +96,8 @@
Tools/datatype_rep_proofs.ML Tools/induct_attrib.ML Tools/induct_method.ML \
Tools/inductive_package.ML Tools/meson.ML Tools/numeral_syntax.ML \
Tools/primrec_package.ML Tools/recdef_package.ML \
- Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
+ Tools/record_package.ML Tools/split_rule.ML \
+ Tools/svc_funcs.ML Tools/typedef_package.ML \
Transitive_Closure.thy Transitive_Closure_lemmas.ML Wellfounded_Recursion.ML \
Wellfounded_Recursion.thy Wellfounded_Relations.ML \
Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
@@ -420,15 +421,11 @@
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML MicroJava/Digest.thy \
- MicroJava/J/Conform.ML MicroJava/J/Conform.thy \
- MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \
- MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \
- MicroJava/J/Decl.thy MicroJava/J/Decl.ML MicroJava/J/State.ML \
- MicroJava/J/State.thy MicroJava/J/Term.thy \
- MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \
- MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML MicroJava/J/Value.thy \
- MicroJava/J/WellType.ML MicroJava/J/WellType.thy \
- MicroJava/J/Example.ML MicroJava/J/Example.thy \
+ MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
+ MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \
+ MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \
+ MicroJava/J/WellForm.thy MicroJava/J/Value.thy \
+ MicroJava/J/WellType.thy MicroJava/J/Example.thy \
MicroJava/JVM/JVMExec.thy MicroJava/JVM/JVMInstructions.thy\
MicroJava/JVM/JVMState.thy MicroJava/JVM/JVMExecInstr.thy\
MicroJava/BV/BVSpec.thy MicroJava/BV/Step.thy\
--- a/src/HOL/MicroJava/BV/BVSpec.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Feb 01 20:53:13 2001 +0100
@@ -12,30 +12,30 @@
constdefs
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool"
"wt_instr i G rT phi mxs max_pc pc ==
- app i G mxs rT (phi!pc) \\<and>
- (\\<forall> pc' \\<in> set (succs i pc). pc' < max_pc \\<and> (G \\<turnstile> step i G (phi!pc) <=' phi!pc'))"
+ app i G mxs rT (phi!pc) \<and>
+ (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
"wt_start G C pTs mxl phi ==
- G \\<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
+ G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool"
"wt_method G C pTs rT mxs mxl ins phi ==
let max_pc = length ins
in
- 0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and>
- (\\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
+ 0 < max_pc \<and> wt_start G C pTs mxl phi \<and>
+ (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
"wt_jvm_prog G phi ==
- wf_prog (\\<lambda>G C (sig,rT,(maxs,maxl,b)).
+ wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)).
wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G"
lemma wt_jvm_progD:
-"wt_jvm_prog G phi ==> (\\<exists>wt. wf_prog wt G)"
+"wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr:
@@ -48,54 +48,17 @@
lemma wt_jvm_prog_impl_wt_start:
"[| wt_jvm_prog G phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==>
- 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)"
+ 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
text {* for most instructions wt\_instr collapses: *}
lemma
"succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc =
- (app i G mxs rT (phi!pc) \\<and> pc+1 < max_pc \\<and> (G \\<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
+ (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
by (simp add: wt_instr_def)
-(* ### move to WellForm *)
-
-lemma methd:
- "[| wf_prog wf_mb G; (C,S,fs,mdecls) \\<in> set G; (sig,rT,code) \\<in> set mdecls |]
- ==> method (G,C) sig = Some(C,rT,code) \\<and> is_class G C"
-proof -
- assume wf: "wf_prog wf_mb G"
- assume C: "(C,S,fs,mdecls) \\<in> set G"
-
- assume m: "(sig,rT,code) \\<in> set mdecls"
- moreover
- from wf
- have "class G Object = Some (arbitrary, [], [])"
- by simp
- moreover
- from wf C
- have c: "class G C = Some (S,fs,mdecls)"
- by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
- ultimately
- have O: "C \\<noteq> Object"
- by auto
-
- from wf C
- have "unique mdecls"
- by (unfold wf_prog_def wf_cdecl_def) auto
-
- hence "unique (map (\\<lambda>(s,m). (s,C,m)) mdecls)"
- by - (induct mdecls, auto)
-
- with m
- have "map_of (map (\\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
- by (force intro: map_of_SomeI)
-
- with wf C m c O
- show ?thesis
- by (auto simp add: is_class_def dest: method_rec [of _ _ C])
-qed
end
--- a/src/HOL/MicroJava/J/Conform.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,236 +0,0 @@
-(* Title: HOL/MicroJava/J/Conform.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-section "hext";
-
-Goalw [hext_def]
-" \\<forall>a C fs . h a = Some (C,fs) --> \
-\ (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'";
-by Auto_tac;
-qed "hextI";
-
-Goalw [hext_def] "[|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')";
-by (Force_tac 1);
-qed "hext_objD";
-
-Goal "h\\<le>|h";
-by (rtac hextI 1);
-by (Fast_tac 1);
-qed "hext_refl";
-
-Goal "h a = None ==> h\\<le>|h(a\\<mapsto>x)";
-by (rtac hextI 1);
-by Auto_tac;
-qed "hext_new";
-
-Goal "[|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''";
-by (rtac hextI 1);
-by (fast_tac (HOL_cs addDs [hext_objD]) 1);
-qed "hext_trans";
-
-Addsimps [hext_refl, hext_new];
-
-Goal "h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))";
-by (rtac hextI 1);
-by Auto_tac;
-qed "hext_upd_obj";
-
-
-section "conf";
-
-Goalw [conf_def] "G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T";
-by (Simp_tac 1);
-qed "conf_Null";
-Addsimps [conf_Null];
-
-Goalw [conf_def] "typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T";
-by (rtac val_.induct 1);
-by Auto_tac;
-qed_spec_mp "conf_litval";
-Addsimps[conf_litval];
-
-Goalw [conf_def] "[|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T";
-by (Asm_full_simp_tac 1);
-qed "conf_AddrI";
-
-Goalw [conf_def] "[|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D";
-by (Asm_full_simp_tac 1);
-qed "conf_obj_AddrI";
-
-Goalw [conf_def] "is_type G T --> G,h\\<turnstile>default_val T::\\<preceq>T";
-by (res_inst_tac [("y","T")] ty.exhaust 1);
-by (etac ssubst 1);
-by (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
-by (auto_tac (claset(), simpset() addsimps [widen.null]));
-qed_spec_mp "defval_conf";
-
-Goalw [conf_def]
-"h a = Some (C,fs) ==> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)";
-by (rtac val_.induct 1);
-by Auto_tac;
-qed "conf_upd_obj";
-
-Goalw [conf_def] "wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'";
-by (rtac val_.induct 1);
-by (auto_tac (claset() addIs [widen_trans], simpset()));
-qed_spec_mp "conf_widen";
-
-Goalw [conf_def] "h\\<le>|h' ==> G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T";
-by (rtac val_.induct 1);
-by (auto_tac (claset() addDs [hext_objD], simpset()));
-qed_spec_mp "conf_hext";
-
-Goalw [conf_def] "[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a";
-by Auto_tac;
-qed "new_locD";
-
-Goalw [conf_def]
- "G,h\\<turnstile>a'::\\<preceq>RefT T --> a' = Null | \
-\ (\\<exists>a obj T'. a' = Addr a \\<and> h a = Some obj \\<and> obj_ty obj = T' \\<and> G\\<turnstile>T'\\<preceq>RefT T)";
-by(induct_tac "a'" 1);
-by(Auto_tac);
-qed_spec_mp "conf_RefTD";
-
-Goal "G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null";
-by (dtac conf_RefTD 1);
-by Auto_tac;
-qed "conf_NullTD";
-
-Goal "[|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
-\ \\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t";
-by (dtac conf_RefTD 1);
-by Auto_tac;
-qed "non_npD";
-
-Goal "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
-\ (\\<exists>a C' fs. a' = Addr a \\<and> h a = Some (C',fs) \\<and> G\\<turnstile>C'\\<preceq>C C)";
-by (fast_tac (claset() addDs [non_npD]) 1);
-qed "non_np_objD";
-
-Goal "a' \\<noteq> Null ==> wf_prog wf_mb G ==> G,h\\<turnstile>a'::\\<preceq>RefT t -->\
-\ (\\<forall>C. t = ClassT C --> C \\<noteq> Object) --> \
-\ (\\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t)";
-by(res_inst_tac [("y","t")] ref_ty.exhaust 1);
- by (fast_tac (claset() addDs [conf_NullTD]) 1);
-by (fast_tac (claset() addDs [non_np_objD]) 1);
-qed_spec_mp "non_np_objD'";
-
-Goal "wf_prog wf_mb G ==> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' --> list_all2 (conf G h) vs Ts'";
-by(induct_tac "vs" 1);
- by(ALLGOALS Clarsimp_tac);
-by(forward_tac [list_all2_lengthD RS sym] 1);
-by(full_simp_tac (simpset()addsimps[length_Suc_conv]) 1);
-by(Safe_tac);
-by(forward_tac [list_all2_lengthD RS sym] 1);
-by(full_simp_tac (simpset()addsimps[length_Suc_conv]) 1);
-by(Clarify_tac 1);
-by(fast_tac (claset() addEs [conf_widen]) 1);
-qed_spec_mp "conf_list_gext_widen";
-
-
-section "lconf";
-
-Goalw[lconf_def] "[| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T";
-by (Force_tac 1);
-qed "lconfD";
-
-Goalw [lconf_def] "[| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L";
-by (fast_tac (claset() addEs [conf_hext]) 1);
-qed "lconf_hext";
-AddEs [lconf_hext];
-
-Goalw [lconf_def] "!!X. [| G,h\\<turnstile>l[::\\<preceq>]lT; \
-\ G,h\\<turnstile>v::\\<preceq>T; lT va = Some T |] ==> G,h\\<turnstile>l(va\\<mapsto>v)[::\\<preceq>]lT";
-by Auto_tac;
-qed "lconf_upd";
-
-Goal "\\<forall>x. P x --> R (dv x) x ==> (\\<forall>x. map_of fs f = Some x --> P x) --> \
-\ (\\<forall>T. map_of fs f = Some T --> \
-\ (\\<exists>v. map_of (map (\\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \\<and> R v T))";
-by( induct_tac "fs" 1);
-by Auto_tac;
-qed_spec_mp "lconf_init_vars_lemma";
-
-Goalw [lconf_def, init_vars_def]
-"\\<forall>n. \\<forall>T. map_of fs n = Some T --> is_type G T ==> G,h\\<turnstile>init_vars fs[::\\<preceq>]map_of fs";
-by Auto_tac;
-by( rtac lconf_init_vars_lemma 1);
-by( atac 3);
-by( strip_tac 1);
-by( etac defval_conf 1);
-by Auto_tac;
-qed "lconf_init_vars";
-AddSIs [lconf_init_vars];
-
-Goalw [lconf_def] "[|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)";
-by Auto_tac;
-qed "lconf_ext";
-
-Goalw [lconf_def] "G,h\\<turnstile>l[::\\<preceq>]L ==> \\<forall>vs Ts. nodups vns --> length Ts = length vns --> list_all2 (\\<lambda>v T. G,h\\<turnstile>v::\\<preceq>T) vs Ts --> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[::\\<preceq>]L(vns[\\<mapsto>]Ts)";
-by( induct_tac "vns" 1);
-by( ALLGOALS Clarsimp_tac);
-by( forward_tac [list_all2_lengthD] 1);
-by( auto_tac (claset(), simpset() addsimps [length_Suc_conv]));
-qed_spec_mp "lconf_ext_list";
-
-
-section "oconf";
-
-Goalw [oconf_def] "G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>";
-by (Fast_tac 1);
-qed "oconf_hext";
-
-Goalw [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
-\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T))";
-by Auto_tac;
-qed "oconf_obj";
-bind_thm ("oconf_objD", oconf_obj RS iffD1 RS spec RS spec RS mp);
-
-
-section "hconf";
-
-Goalw [hconf_def] "[|G\\<turnstile>h h\\<surd>; h a = Some obj|] ==> G,h\\<turnstile>obj\\<surd>";
-by (Fast_tac 1);
-qed "hconfD";
-
-Goalw [hconf_def] "\\<forall>a obj. h a=Some obj --> G,h\\<turnstile>obj\\<surd> ==> G\\<turnstile>h h\\<surd>";
-by (Fast_tac 1);
-qed "hconfI";
-
-
-section "conforms";
-
-Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>";
-by (Asm_full_simp_tac 1);
-qed "conforms_heapD";
-
-Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT";
-by (Asm_full_simp_tac 1);
-qed "conforms_localD";
-
-Goalw [conforms_def] "[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)";
-by Auto_tac;
-qed "conformsI";
-
-Goal "[|(h,l)::\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> |] ==> (h',l)::\\<preceq>(G,lT)";
-by( fast_tac (HOL_cs addDs [conforms_localD]
- addSEs [conformsI, lconf_hext]) 1);
-qed "conforms_hext";
-
-Goal "[|(h,l)::\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)|] ==> (h(a\\<mapsto>obj),l)::\\<preceq>(G, lT)";
-by( rtac conforms_hext 1);
-by Auto_tac;
-by( rtac hconfI 1);
-by( dtac conforms_heapD 1);
-by( (auto_tac (HOL_cs addEs [oconf_hext] addDs [hconfD],
- simpset()delsimps[split_paired_All])));
-qed "conforms_upd_obj";
-
-Goalw [conforms_def]
-"[|(h, l)::\\<preceq>(G, lT); G,h\\<turnstile>v::\\<preceq>T; lT va = Some T|] ==> \
-\ (h, l(va\\<mapsto>v))::\\<preceq>(G, lT)";
-by( auto_tac (claset() addEs [lconf_upd], simpset()));
-qed "conforms_upd_local";
--- a/src/HOL/MicroJava/J/Conform.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Thu Feb 01 20:53:13 2001 +0100
@@ -6,30 +6,30 @@
Conformity relations for type safety of Java
*)
-Conform = State + WellType +
+theory Conform = State + WellType:
-types 'c env_ = "'c prog \\<times> (vname \\<leadsto> ty)" (* same as env of WellType.thy *)
+types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)" (* same as env of WellType.thy *)
constdefs
- hext :: "aheap => aheap => bool" ("_ \\<le>| _" [51,51] 50)
- "h\\<le>|h' == \\<forall>a C fs. h a = Some(C,fs) --> (\\<exists>fs'. h' a = Some(C,fs'))"
+ hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50)
+ "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
- conf :: "'c prog => aheap => val => ty => bool" ("_,_ \\<turnstile> _ ::\\<preceq> _" [51,51,51,51] 50)
- "G,h\\<turnstile>v::\\<preceq>T == \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
+ conf :: "'c prog => aheap => val => ty => bool" ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
+ "G,h\<turnstile>v::\<preceq>T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
- lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
- ("_,_ \\<turnstile> _ [::\\<preceq>] _" [51,51,51,51] 50)
- "G,h\\<turnstile>vs[::\\<preceq>]Ts == \\<forall>n T. Ts n = Some T --> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T)"
+ lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
+ ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
+ "G,h\<turnstile>vs[::\<preceq>]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h\<turnstile>v::\<preceq>T)"
- oconf :: "'c prog => aheap => obj => bool" ("_,_ \\<turnstile> _ \\<surd>" [51,51,51] 50)
- "G,h\\<turnstile>obj\\<surd> == G,h\\<turnstile>snd obj[::\\<preceq>]map_of (fields (G,fst obj))"
+ oconf :: "'c prog => aheap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
+ "G,h\<turnstile>obj\<surd> == G,h\<turnstile>snd obj[::\<preceq>]map_of (fields (G,fst obj))"
- hconf :: "'c prog => aheap => bool" ("_ \\<turnstile>h _ \\<surd>" [51,51] 50)
- "G\\<turnstile>h h\\<surd> == \\<forall>a obj. h a = Some obj --> G,h\\<turnstile>obj\\<surd>"
+ hconf :: "'c prog => aheap => bool" ("_ \<turnstile>h _ \<surd>" [51,51] 50)
+ "G\<turnstile>h h\<surd> == \<forall>a obj. h a = Some obj --> G,h\<turnstile>obj\<surd>"
- conforms :: "state => java_mb env_ => bool" ("_ ::\\<preceq> _" [51,51] 50)
- "s::\\<preceq>E == prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[::\\<preceq>]localT E"
+ conforms :: "state => java_mb env_ => bool" ("_ ::\<preceq> _" [51,51] 50)
+ "s::\<preceq>E == prg E\<turnstile>h heap s\<surd> \<and> prg E,heap s\<turnstile>locals s[::\<preceq>]localT E"
syntax (HTML)
@@ -39,7 +39,7 @@
conf :: "'c prog => aheap => val => ty => bool"
("_,_ |- _ ::<= _" [51,51,51,51] 50)
- lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
+ lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
("_,_ |- _ [::<=] _" [51,51,51,51] 50)
oconf :: "'c prog => aheap => obj => bool"
@@ -51,4 +51,257 @@
conforms :: "state => java_mb env_ => bool"
("_ ::<= _" [51,51] 50)
+
+section "hext"
+
+lemma hextI:
+" \<forall>a C fs . h a = Some (C,fs) -->
+ (\<exists>fs'. h' a = Some (C,fs')) ==> h\<le>|h'"
+apply (unfold hext_def)
+apply auto
+done
+
+lemma hext_objD: "[|h\<le>|h'; h a = Some (C,fs) |] ==> \<exists>fs'. h' a = Some (C,fs')"
+apply (unfold hext_def)
+apply (force)
+done
+
+lemma hext_refl [simp]: "h\<le>|h"
+apply (rule hextI)
+apply (fast)
+done
+
+lemma hext_new [simp]: "h a = None ==> h\<le>|h(a\<mapsto>x)"
+apply (rule hextI)
+apply auto
+done
+
+lemma hext_trans: "[|h\<le>|h'; h'\<le>|h''|] ==> h\<le>|h''"
+apply (rule hextI)
+apply (fast dest: hext_objD)
+done
+
+lemma hext_upd_obj: "h a = Some (C,fs) ==> h\<le>|h(a\<mapsto>(C,fs'))"
+apply (rule hextI)
+apply auto
+done
+
+
+section "conf"
+
+lemma conf_Null [simp]: "G,h\<turnstile>Null::\<preceq>T = G\<turnstile>RefT NullT\<preceq>T"
+apply (unfold conf_def)
+apply (simp (no_asm))
+done
+
+lemma conf_litval [rule_format (no_asm), simp]:
+ "typeof (\<lambda>v. None) v = Some T --> G,h\<turnstile>v::\<preceq>T"
+apply (unfold conf_def)
+apply (rule val.induct)
+apply auto
+done
+
+lemma conf_AddrI: "[|h a = Some obj; G\<turnstile>obj_ty obj\<preceq>T|] ==> G,h\<turnstile>Addr a::\<preceq>T"
+apply (unfold conf_def)
+apply (simp)
+done
+
+lemma conf_obj_AddrI: "[|h a = Some (C,fs); G\<turnstile>C\<preceq>C D|] ==> G,h\<turnstile>Addr a::\<preceq> Class D"
+apply (unfold conf_def)
+apply (simp)
+done
+
+lemma defval_conf [rule_format (no_asm)]: "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
+apply (unfold conf_def)
+apply (rule_tac "y" = "T" in ty.exhaust)
+apply (erule ssubst)
+apply (rule_tac "y" = "prim_ty" in prim_ty.exhaust)
+apply (auto simp add: widen.null)
+done
+
+lemma conf_upd_obj:
+"h a = Some (C,fs) ==> (G,h(a\<mapsto>(C,fs'))\<turnstile>x::\<preceq>T) = (G,h\<turnstile>x::\<preceq>T)"
+apply (unfold conf_def)
+apply (rule val.induct)
+apply auto
+done
+
+lemma conf_widen [rule_format (no_asm)]: "wf_prog wf_mb G ==> G,h\<turnstile>x::\<preceq>T --> G\<turnstile>T\<preceq>T' --> G,h\<turnstile>x::\<preceq>T'"
+apply (unfold conf_def)
+apply (rule val.induct)
+apply (auto intro: widen_trans)
+done
+
+lemma conf_hext [rule_format (no_asm)]: "h\<le>|h' ==> G,h\<turnstile>v::\<preceq>T --> G,h'\<turnstile>v::\<preceq>T"
+apply (unfold conf_def)
+apply (rule val.induct)
+apply (auto dest: hext_objD)
+done
+
+lemma new_locD: "[|h a = None; G,h\<turnstile>Addr t::\<preceq>T|] ==> t\<noteq>a"
+apply (unfold conf_def)
+apply auto
+done
+
+lemma conf_RefTD [rule_format (no_asm)]:
+ "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null |
+ (\<exists>a obj T'. a' = Addr a \<and> h a = Some obj \<and> obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
+apply (unfold conf_def)
+apply(induct_tac "a'")
+apply(auto)
+done
+
+lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null"
+apply (drule conf_RefTD)
+apply auto
+done
+
+lemma non_npD: "[|a' \<noteq> Null; G,h\<turnstile>a'::\<preceq>RefT t|] ==>
+ \<exists>a C fs. a' = Addr a \<and> h a = Some (C,fs) \<and> G\<turnstile>Class C\<preceq>RefT t"
+apply (drule conf_RefTD)
+apply auto
+done
+
+lemma non_np_objD: "!!G. [|a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; C \<noteq> Object|] ==>
+ (\<exists>a C' fs. a' = Addr a \<and> h a = Some (C',fs) \<and> G\<turnstile>C'\<preceq>C C)"
+apply (fast dest: non_npD)
+done
+
+lemma non_np_objD' [rule_format (no_asm)]: "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t -->
+ (\<forall>C. t = ClassT C --> C \<noteq> Object) -->
+ (\<exists>a C fs. a' = Addr a \<and> h a = Some (C,fs) \<and> G\<turnstile>Class C\<preceq>RefT t)"
+apply(rule_tac "y" = "t" in ref_ty.exhaust)
+ apply (fast dest: conf_NullTD)
+apply (fast dest: non_np_objD)
+done
+
+lemma conf_list_gext_widen [rule_format (no_asm)]: "wf_prog wf_mb G ==> \<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts' --> list_all2 (conf G h) vs Ts'"
+apply(induct_tac "vs")
+ apply(clarsimp)
+apply(clarsimp)
+apply(frule list_all2_lengthD [THEN sym])
+apply(simp (no_asm_use) add: length_Suc_conv)
+apply(safe)
+apply(frule list_all2_lengthD [THEN sym])
+apply(simp (no_asm_use) add: length_Suc_conv)
+apply(clarify)
+apply(fast elim: conf_widen)
+done
+
+
+section "lconf"
+
+lemma lconfD: "[| G,h\<turnstile>vs[::\<preceq>]Ts; Ts n = Some T |] ==> G,h\<turnstile>(the (vs n))::\<preceq>T"
+apply (unfold lconf_def)
+apply (force)
+done
+
+lemma lconf_hext [elim]: "[| G,h\<turnstile>l[::\<preceq>]L; h\<le>|h' |] ==> G,h'\<turnstile>l[::\<preceq>]L"
+apply (unfold lconf_def)
+apply (fast elim: conf_hext)
+done
+
+lemma lconf_upd: "!!X. [| G,h\<turnstile>l[::\<preceq>]lT;
+ G,h\<turnstile>v::\<preceq>T; lT va = Some T |] ==> G,h\<turnstile>l(va\<mapsto>v)[::\<preceq>]lT"
+apply (unfold lconf_def)
+apply auto
+done
+
+lemma lconf_init_vars_lemma [rule_format (no_asm)]: "\<forall>x. P x --> R (dv x) x ==> (\<forall>x. map_of fs f = Some x --> P x) -->
+ (\<forall>T. map_of fs f = Some T -->
+ (\<exists>v. map_of (map (\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \<and> R v T))"
+apply( induct_tac "fs")
+apply auto
+done
+
+lemma lconf_init_vars [intro!]:
+"\<forall>n. \<forall>T. map_of fs n = Some T --> is_type G T ==> G,h\<turnstile>init_vars fs[::\<preceq>]map_of fs"
+apply (unfold lconf_def init_vars_def)
+apply auto
+apply( rule lconf_init_vars_lemma)
+apply( erule_tac [3] asm_rl)
+apply( intro strip)
+apply( erule defval_conf)
+apply auto
+done
+
+lemma lconf_ext: "[|G,s\<turnstile>l[::\<preceq>]L; G,s\<turnstile>v::\<preceq>T|] ==> G,s\<turnstile>l(vn\<mapsto>v)[::\<preceq>]L(vn\<mapsto>T)"
+apply (unfold lconf_def)
+apply auto
+done
+
+lemma lconf_ext_list [rule_format (no_asm)]: "G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. nodups vns --> length Ts = length vns --> list_all2 (\<lambda>v T. G,h\<turnstile>v::\<preceq>T) vs Ts --> G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)"
+apply (unfold lconf_def)
+apply( induct_tac "vns")
+apply( clarsimp)
+apply( clarsimp)
+apply( frule list_all2_lengthD)
+apply( auto simp add: length_Suc_conv)
+done
+
+
+section "oconf"
+
+lemma oconf_hext: "G,h\<turnstile>obj\<surd> ==> h\<le>|h' ==> G,h'\<turnstile>obj\<surd>"
+apply (unfold oconf_def)
+apply (fast)
+done
+
+lemma oconf_obj: "G,h\<turnstile>(C,fs)\<surd> =
+ (\<forall>T f. map_of(fields (G,C)) f = Some T --> (\<exists>v. fs f = Some v \<and> G,h\<turnstile>v::\<preceq>T))"
+apply (unfold oconf_def lconf_def)
+apply auto
+done
+
+lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]
+
+
+section "hconf"
+
+lemma hconfD: "[|G\<turnstile>h h\<surd>; h a = Some obj|] ==> G,h\<turnstile>obj\<surd>"
+apply (unfold hconf_def)
+apply (fast)
+done
+
+lemma hconfI: "\<forall>a obj. h a=Some obj --> G,h\<turnstile>obj\<surd> ==> G\<turnstile>h h\<surd>"
+apply (unfold hconf_def)
+apply (fast)
+done
+
+
+section "conforms"
+
+lemma conforms_heapD: "(h, l)::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
+apply (unfold conforms_def)
+apply (simp)
+done
+
+lemma conforms_localD: "(h, l)::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT"
+apply (unfold conforms_def)
+apply (simp)
+done
+
+lemma conformsI: "[|G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT|] ==> (h, l)::\<preceq>(G, lT)"
+apply (unfold conforms_def)
+apply auto
+done
+
+lemma conforms_hext: "[|(h,l)::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] ==> (h',l)::\<preceq>(G,lT)"
+apply( fast dest: conforms_localD elim!: conformsI lconf_hext)
+done
+
+lemma conforms_upd_obj: "[|(h,l)::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] ==> (h(a\<mapsto>obj),l)::\<preceq>(G, lT)"
+apply( rule conforms_hext)
+apply auto
+apply( rule hconfI)
+apply( drule conforms_heapD)
+apply( tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
+done
+
+lemma conforms_upd_local:
+"[|(h, l)::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] ==> (h, l(va\<mapsto>v))::\<preceq>(G, lT)"
+apply (unfold conforms_def)
+apply( auto elim: lconf_upd)
+done
+
end
--- a/src/HOL/MicroJava/J/Decl.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(* Title: HOL/MicroJava/J/Decl.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-Goalw [is_class_def, class_def] "finite {C. is_class G C}";
-by (fold_goals_tac [dom_def]);
-by (rtac finite_dom_map_of 1);
-qed "finite_is_class";
-
--- a/src/HOL/MicroJava/J/Decl.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Thu Feb 01 20:53:13 2001 +0100
@@ -6,52 +6,58 @@
Class declarations and programs
*)
-Decl = Type +
+theory Decl = Type:
types fdecl (* field declaration, cf. 8.3 (, 9.3) *)
- = "vname \\<times> ty"
+ = "vname \<times> ty"
types sig (* signature of a method, cf. 8.4.2 *)
- = "mname \\<times> ty list"
+ = "mname \<times> ty list"
'c mdecl (* method declaration in a class *)
- = "sig \\<times> ty \\<times> 'c"
+ = "sig \<times> ty \<times> 'c"
types 'c class (* class *)
- = "cname \\<times> fdecl list \\<times> 'c mdecl list"
+ = "cname \<times> fdecl list \<times> 'c mdecl list"
(* superclass, fields, methods*)
'c cdecl (* class declaration, cf. 8.1 *)
- = "cname \\<times> 'c class"
+ = "cname \<times> 'c class"
consts
Object :: cname (* name of root class *)
- ObjectC :: 'c cdecl (* decl of root class *)
+ ObjectC :: "'c cdecl" (* decl of root class *)
defs
- ObjectC_def "ObjectC == (Object, (arbitrary, [], []))"
+ ObjectC_def: "ObjectC == (Object, (arbitrary, [], []))"
types 'c prog = "'c cdecl list"
translations
- "fdecl" <= (type) "vname \\<times> ty"
- "sig" <= (type) "mname \\<times> ty list"
- "mdecl c" <= (type) "sig \\<times> ty \\<times> c"
- "class c" <= (type) "cname \\<times> fdecl list \\<times> (c mdecl) list"
- "cdecl c" <= (type) "cname \\<times> (c class)"
+ "fdecl" <= (type) "vname \<times> ty"
+ "sig" <= (type) "mname \<times> ty list"
+ "mdecl c" <= (type) "sig \<times> ty \<times> c"
+ "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
+ "cdecl c" <= (type) "cname \<times> (c class)"
"prog c" <= (type) "(c cdecl) list"
constdefs
- class :: "'c prog => (cname \\<leadsto> 'c class)"
- "class \\<equiv> map_of"
+ class :: "'c prog => (cname \<leadsto> 'c class)"
+ "class \<equiv> map_of"
is_class :: "'c prog => cname => bool"
- "is_class G C \\<equiv> class G C \\<noteq> None"
+ "is_class G C \<equiv> class G C \<noteq> None"
+
+lemma finite_is_class: "finite {C. is_class G C}"
+apply (unfold is_class_def class_def)
+apply (fold dom_def)
+apply (rule finite_dom_map_of)
+done
consts
--- a/src/HOL/MicroJava/J/Eval.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-(* Title: HOL/MicroJava/J/Eval.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-val eval_evals_exec_induct = complete_split_rule eval_evals_exec.induct;
-
-Goal "[|new_Addr (heap s) = (a,x); \
-\ s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
-\ G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
-by (Asm_simp_tac 1);
-br eval_evals_exec.NewC 1;
-by Auto_tac;
-qed "NewCI";
-
-Goal "!!s s'. (G\\<turnstile>(x,s) -e \\<succ> v -> (x',s') --> x'=None --> x=None) \\<and> \
-\ (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x'=None --> x=None) \\<and> \
-\ (G\\<turnstile>(x,s) -c -> (x',s') --> x'=None --> x=None)";
-by(split_all_tac 1);
-by(rtac eval_evals_exec_induct 1);
-by(rewtac c_hupd_def);
-by(ALLGOALS Asm_full_simp_tac);
-qed "eval_evals_exec_no_xcpt";
-
-Goal "G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None";
-by (dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1);
-by (Fast_tac 1);
-qed "eval_no_xcpt";
-
-Goal "G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None";
-by (dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1);
-by (Fast_tac 1);
-qed "evals_no_xcpt";
-
-Goal
-"!!s s'. (G\\<turnstile>(x,s) -e \\<succ> v -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
-\ (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
-\ (G\\<turnstile>(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)";
-by (split_all_tac 1);
-by (rtac eval_evals_exec_induct 1);
-by (rewtac c_hupd_def);
-by (ALLGOALS Asm_full_simp_tac);
-qed "eval_evals_exec_xcpt";
-
-Goal "G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and> s'=s";
-by (dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1);
-by (Fast_tac 1);
-qed "eval_xcpt";
-
-Goal "G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and> s'=s";
-by (dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1);
-by (Fast_tac 1);
-qed "exec_xcpt";
\ No newline at end of file
--- a/src/HOL/MicroJava/J/Eval.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Thu Feb 01 20:53:13 2001 +0100
@@ -7,20 +7,21 @@
execution of Java expressions and statements
*)
-Eval = State + WellType +
+theory Eval = State + WellType:
+
consts
- eval :: "java_mb prog => (xstate \\<times> expr \\<times> val \\<times> xstate) set"
- evals :: "java_mb prog => (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
- exec :: "java_mb prog => (xstate \\<times> stmt \\<times> xstate) set"
+ eval :: "java_mb prog => (xstate \<times> expr \<times> val \<times> xstate) set"
+ evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
+ exec :: "java_mb prog => (xstate \<times> stmt \<times> xstate) set"
syntax
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
- ("_ \\<turnstile> _ -_\\<succ>_-> _" [51,82,60,82,82] 81)
+ ("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
evals:: "[java_mb prog,xstate,expr list,
val list,xstate] => bool "
- ("_ \\<turnstile> _ -_[\\<succ>]_-> _" [51,82,60,51,82] 81)
+ ("_ \<turnstile> _ -_[\<succ>]_-> _" [51,82,60,51,82] 81)
exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
- ("_ \\<turnstile> _ -_-> _" [51,82,60,82] 81)
+ ("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
syntax (HTML)
eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
@@ -33,112 +34,159 @@
translations
- "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval G"
- "G\\<turnstile>s -e \\<succ> v-> s' " == "(s, e, v, s') \\<in> eval G"
- "G\\<turnstile>s -e[\\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
- "G\\<turnstile>s -e[\\<succ>]v-> s' " == "(s, e, v, s') \\<in> evals G"
- "G\\<turnstile>s -c -> (x,s')" <= "(s, c, x, s') \\<in> exec G"
- "G\\<turnstile>s -c -> s' " == "(s, c, s') \\<in> exec G"
+ "G\<turnstile>s -e \<succ> v-> (x,s')" <= "(s, e, v, x, s') \<in> eval G"
+ "G\<turnstile>s -e \<succ> v-> s' " == "(s, e, v, s') \<in> eval G"
+ "G\<turnstile>s -e[\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \<in> evals G"
+ "G\<turnstile>s -e[\<succ>]v-> s' " == "(s, e, v, s') \<in> evals G"
+ "G\<turnstile>s -c -> (x,s')" <= "(s, c, x, s') \<in> exec G"
+ "G\<turnstile>s -c -> s' " == "(s, c, s') \<in> exec G"
-inductive "eval G" "evals G" "exec G" intrs
+inductive "eval G" "evals G" "exec G" intros
(* evaluation of expressions *)
(* cf. 15.5 *)
- XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
+ XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)"
(* cf. 15.8.1 *)
- NewC "[| h = heap s; (a,x) = new_Addr h;
- h'= h(a\\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
- G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
+ NewC: "[| h = heap s; (a,x) = new_Addr h;
+ h'= h(a\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
+ G\<turnstile>Norm s -NewC C\<succ>Addr a-> c_hupd h' (x,s)"
(* cf. 15.15 *)
- Cast "[| G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
- x2 = raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
- G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
+ Cast: "[| G\<turnstile>Norm s0 -e\<succ>v-> (x1,s1);
+ x2 = raise_if (\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
+ G\<turnstile>Norm s0 -Cast C e\<succ>v-> (x2,s1)"
(* cf. 15.7.1 *)
- Lit "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
+ Lit: "G\<turnstile>Norm s -Lit v\<succ>v-> Norm s"
- BinOp "[| G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
- G\\<turnstile>s1 -e2\\<succ>v2-> s2;
+ BinOp:"[| G\<turnstile>Norm s -e1\<succ>v1-> s1;
+ G\<turnstile>s1 -e2\<succ>v2-> s2;
v = (case bop of Eq => Bool (v1 = v2)
| Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
- G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
+ G\<turnstile>Norm s -BinOp bop e1 e2\<succ>v-> s2"
(* cf. 15.13.1, 15.2 *)
- LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
+ LAcc: "G\<turnstile>Norm s -LAcc v\<succ>the (locals s v)-> Norm s"
(* cf. 15.25.1 *)
- LAss "[| G\\<turnstile>Norm s -e\\<succ>v-> (x,(h,l));
- l' = (if x = None then l(va\\<mapsto>v) else l) |] ==>
- G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
+ LAss: "[| G\<turnstile>Norm s -e\<succ>v-> (x,(h,l));
+ l' = (if x = None then l(va\<mapsto>v) else l) |] ==>
+ G\<turnstile>Norm s -va::=e\<succ>v-> (x,(h,l'))"
(* cf. 15.10.1, 15.2 *)
- FAcc "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1);
+ FAcc: "[| G\<turnstile>Norm s0 -e\<succ>a'-> (x1,s1);
v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
- G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
+ G\<turnstile>Norm s0 -{T}e..fn\<succ>v-> (np a' x1,s1)"
(* cf. 15.25.1 *)
- FAss "[| G\\<turnstile> Norm s0 -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
- G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
+ FAss: "[| G\<turnstile> Norm s0 -e1\<succ>a'-> (x1,s1); a = the_Addr a';
+ G\<turnstile>(np a' x1,s1) -e2\<succ>v -> (x2,s2);
h = heap s2; (c,fs) = the (h a);
- h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v)))) |] ==>
- G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
+ h' = h(a\<mapsto>(c,(fs((fn,T)\<mapsto>v)))) |] ==>
+ G\<turnstile>Norm s0 -{T}e1..fn:=e2\<succ>v-> c_hupd h' (x2,s2)"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
- Call "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
- G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
+ Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
+ G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
(md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
- G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
- G\\<turnstile> s3 -res\\<succ>v -> (x4,s4) |] ==>
- G\\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
+ G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
+ G\<turnstile> s3 -res\<succ>v -> (x4,s4) |] ==>
+ G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(heap s4,l))"
(* evaluation of expression lists *)
(* cf. 15.5 *)
- XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
+ XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
(* cf. 15.11.??? *)
- Nil "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
+ Nil: "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
(* cf. 15.6.4 *)
- Cons "[| G\\<turnstile>Norm s0 -e \\<succ> v -> s1;
- G\\<turnstile> s1 -es[\\<succ>]vs-> s2 |] ==>
- G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
+ Cons: "[| G\<turnstile>Norm s0 -e \<succ> v -> s1;
+ G\<turnstile> s1 -es[\<succ>]vs-> s2 |] ==>
+ G\<turnstile>Norm s0 -e#es[\<succ>]v#vs-> s2"
(* execution of statements *)
(* cf. 14.1 *)
- XcptS "G\\<turnstile>(Some xc,s) -c-> (Some xc,s)"
+ XcptS:"G\<turnstile>(Some xc,s) -c-> (Some xc,s)"
(* cf. 14.5 *)
- Skip "G\\<turnstile>Norm s -Skip-> Norm s"
+ Skip: "G\<turnstile>Norm s -Skip-> Norm s"
(* cf. 14.7 *)
- Expr "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==>
- G\\<turnstile>Norm s0 -Expr e-> s1"
+ Expr: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1 |] ==>
+ G\<turnstile>Norm s0 -Expr e-> s1"
(* cf. 14.2 *)
- Comp "[| G\\<turnstile>Norm s0 -c1-> s1;
- G\\<turnstile> s1 -c2-> s2|] ==>
- G\\<turnstile>Norm s0 -c1;; c2-> s2"
+ Comp: "[| G\<turnstile>Norm s0 -c1-> s1;
+ G\<turnstile> s1 -c2-> s2|] ==>
+ G\<turnstile>Norm s0 -c1;; c2-> s2"
(* cf. 14.8.2 *)
- Cond "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1;
- G\\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
- G\\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
+ Cond: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1;
+ G\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
+ G\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
(* cf. 14.10, 14.10.1 *)
- LoopF "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; \\<not>the_Bool v |] ==>
- G\\<turnstile>Norm s0 -While(e) c-> s1"
- LoopT "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; the_Bool v;
- G\\<turnstile>s1 -c-> s2; G\\<turnstile>s2 -While(e) c-> s3 |] ==>
- G\\<turnstile>Norm s0 -While(e) c-> s3"
+ LoopF:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; \<not>the_Bool v |] ==>
+ G\<turnstile>Norm s0 -While(e) c-> s1"
+ LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; the_Bool v;
+ G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
+ G\<turnstile>Norm s0 -While(e) c-> s3"
+
+lemmas eval_evals_exec_induct = eval_evals_exec.induct [complete_split]
+
+lemma NewCI: "[|new_Addr (heap s) = (a,x);
+ s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>
+ G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'"
+apply (simp (no_asm_simp))
+apply (rule eval_evals_exec.NewC)
+apply auto
+done
+
+lemma eval_evals_exec_no_xcpt:
+ "!!s s'. (G\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x'=None --> x=None) \<and>
+ (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x'=None --> x=None) \<and>
+ (G\<turnstile>(x,s) -c -> (x',s') --> x'=None --> x=None)"
+apply(simp (no_asm_simp) only: split_tupled_all)
+apply(rule eval_evals_exec_induct)
+apply(unfold c_hupd_def)
+apply(simp_all)
+done
-monos
- if_def2
+lemma eval_no_xcpt: "G\<turnstile>(x,s) -e\<succ>v-> (None,s') ==> x=None"
+apply (drule eval_evals_exec_no_xcpt [THEN conjunct1, THEN mp])
+apply (fast)
+done
+
+lemma evals_no_xcpt: "G\<turnstile>(x,s) -e[\<succ>]v-> (None,s') ==> x=None"
+apply (drule eval_evals_exec_no_xcpt [THEN conjunct2, THEN conjunct1, THEN mp])
+apply (fast)
+done
-end
+lemma eval_evals_exec_xcpt:
+"!!s s'. (G\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>
+ (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>
+ (G\<turnstile>(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s)"
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply (rule eval_evals_exec_induct)
+apply (unfold c_hupd_def)
+apply (simp_all)
+done
+
+lemma eval_xcpt: "G\<turnstile>(Some xc,s) -e\<succ>v-> (x',s') ==> x'=Some xc \<and> s'=s"
+apply (drule eval_evals_exec_xcpt [THEN conjunct1, THEN mp])
+apply (fast)
+done
+
+lemma exec_xcpt: "G\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \<and> s'=s"
+apply (drule eval_evals_exec_xcpt [THEN conjunct2, THEN conjunct2, THEN mp])
+apply (fast)
+done
+
+end
\ No newline at end of file
--- a/src/HOL/MicroJava/J/Example.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-
-Addsimps [inj_cnam_, inj_vnam_];
-Addsimps [Base_not_Object,Ext_not_Object];
-Addsimps [Base_not_Object RS not_sym,Ext_not_Object RS not_sym];
-
-bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps")));
-Goal "map_of ((aa,bb)#ps) aa = Some bb";
-by (Simp_tac 1);
-qed "map_of_Cons1";
-Goal "aa\\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa";
-by (Asm_simp_tac 1);
-qed "map_of_Cons2";
-Delsimps[map_of_Cons]; (* sic! *)
-Addsimps[map_of_Cons1, map_of_Cons2];
-
-Goalw [ObjectC_def,class_def] "class tprg Object = Some (arbitrary, [], [])";
-by (Simp_tac 1);
-qed "class_tprg_Object";
-
-Goalw [ObjectC_def, BaseC_def, ExtC_def, class_def]
-"class tprg Base = Some (Object, \
- \ [(vee, PrimT Boolean)], \
- \ [((foo, [Class Base]), Class Base, foo_Base)])";
-by (Simp_tac 1);
-qed "class_tprg_Base";
-
-Goalw [ObjectC_def, BaseC_def, ExtC_def, class_def]
-"class tprg Ext = Some (Base, \
- \ [(vee, PrimT Integer)], \
- \ [((foo, [Class Base]), Class Ext, foo_Ext)])";
-by (Simp_tac 1);
-qed "class_tprg_Ext";
-
-Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
-
-Goal "(Object,C) \\<in> (subcls1 tprg)^+ ==> R";
-by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
-qed "not_Object_subcls";
-AddSEs [not_Object_subcls];
-
-Goal "tprg\\<turnstile>Object\\<preceq>C C ==> C = Object";
-be rtrancl_induct 1;
-by Auto_tac;
-bd subcls1D 1;
-by Auto_tac;
-qed "subcls_ObjectD";
-AddSDs[subcls_ObjectD];
-
-Goal "(Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
-by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
-qed "not_Base_subcls_Ext";
-AddSEs [not_Base_subcls_Ext];
-
-Goalw [ObjectC_def, BaseC_def, ExtC_def, class_def]
-"class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
-by (auto_tac (claset(),simpset()addsplits[split_if_asm]addsimps[map_of_Cons]));
-qed "class_tprgD";
-
-Goal "(C,C) \\<in> (subcls1 tprg)^+ ==> R";
-by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
-by (ftac class_tprgD 1);
-by (auto_tac (claset() addSDs [],simpset()));
-bd (thm"rtranclD") 1;
-by Auto_tac;
-qed "not_class_subcls_class";
-AddSEs [not_class_subcls_class];
-
-goalw thy [ObjectC_def, BaseC_def, ExtC_def] "unique tprg";
-by (Simp_tac 1);
-qed "unique_classes";
-
-bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);
-
-Goal "tprg\\<turnstile>Ext\\<preceq>C Base";
-br subcls_direct 1;
-by Auto_tac;
-qed "Ext_subcls_Base";
-Addsimps [Ext_subcls_Base];
-
-Goal "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
-br widen.subcls 1;
-by (Simp_tac 1);
-qed "Ext_widen_Base";
-Addsimps [Ext_widen_Base];
-
-AddSIs ty_expr_ty_exprs_wt_stmt.intrs;
-
-
-Goal "acyclic (subcls1 tprg)";
-br acyclicI 1;
-by Safe_tac ;
-qed "acyclic_subcls1_";
-
-val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse);
-
-
-val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma);
-
-Goal "fields (tprg, Object) = []";
-by (stac fields_rec_ 1);
-by Auto_tac;
-qed "fields_Object";
-Addsimps [fields_Object];
-
-Addsimps [is_class_def];
-
-Goal "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]";
-by (stac fields_rec_ 1);
-by Auto_tac;
-qed "fields_Base";
-Addsimps [fields_Base];
-
-Goal "fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @\
- \ fields (tprg, Base)";
-br trans 1;
-br fields_rec_ 1;
-by Auto_tac;
-qed "fields_Ext";
-Addsimps [fields_Ext];
-
-val method_rec_ = wf_subcls1_ RS method_rec_lemma;
-
-Goal "method (tprg,Object) = map_of []";
-by (stac method_rec_ 1);
-by Auto_tac;
-qed "method_Object";
-Addsimps [method_Object];
-
-Goal "method (tprg, Base) = map_of \
-\ [((foo, [Class Base]), Base, (Class Base, foo_Base))]";
-br trans 1;
-br method_rec_ 1;
-by Auto_tac;
-qed "method_Base";
-Addsimps [method_Base];
-
-Goal "method (tprg, Ext) = (method (tprg, Base) ++ map_of \
-\ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])";
-br trans 1;
-br method_rec_ 1;
-by Auto_tac;
-qed "method_Ext";
-Addsimps [method_Ext];
-
-Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Base_def]
-"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))";
-by Auto_tac;
-qed "wf_foo_Base";
-
-Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Ext_def]
-"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))";
-by Auto_tac;
-br ty_expr_ty_exprs_wt_stmt.Cast 1;
-by (Simp_tac 2);
-br cast.subcls 2;
-by (rewtac field_def);
-by Auto_tac;
-qed "wf_foo_Ext";
-
-Goalw [wf_cdecl_def, wf_fdecl_def, ObjectC_def]
-"wf_cdecl wf_java_mdecl tprg ObjectC";
-by (Simp_tac 1);
-qed "wf_ObjectC";
-
-Goalw [wf_cdecl_def, wf_fdecl_def, BaseC_def]
-"wf_cdecl wf_java_mdecl tprg BaseC";
-by (Simp_tac 1);
-by (fold_goals_tac [BaseC_def]);
-br (wf_foo_Base RS conjI) 1;
-by Auto_tac;
-qed "wf_BaseC";
-
-Goalw [wf_cdecl_def, wf_fdecl_def, ExtC_def]
-"wf_cdecl wf_java_mdecl tprg ExtC";
-by (Simp_tac 1);
-by (fold_goals_tac [ExtC_def]);
-br (wf_foo_Ext RS conjI) 1;
-by Auto_tac;
-bd (thm"rtranclD") 1;
-by Auto_tac;
-qed "wf_ExtC";
-
-Goalw [wf_prog_def,Let_def]
-"wf_prog wf_java_mdecl tprg";
-by(simp_tac (simpset() addsimps [wf_ObjectC,wf_BaseC,wf_ExtC,unique_classes])1);
-qed "wf_tprg";
-
-Goalw [appl_methds_def]
-"appl_methds tprg Base (foo, [NT]) = \
-\ {((Class Base, Class Base), [Class Base])}";
-by (Simp_tac 1);
-by (subgoal_tac "tprg\\<turnstile>NT\\<preceq> Class Base" 1);
-by (auto_tac (claset(), simpset() addsimps [map_of_Cons,foo_Base_def]));
-qed "appl_methds_foo_Base";
-
-Goalw [max_spec_def] "max_spec tprg Base (foo, [NT]) = \
-\ {((Class Base, Class Base), [Class Base])}";
-by (auto_tac (claset(), simpset() addsimps [appl_methds_foo_Base]));
-qed "max_spec_foo_Base";
-
-fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
-Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\
-\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
-(* ?pTs' = [Class Base] *)
-by t; (* ;; *)
-by t; (* Expr *)
-by t; (* LAss *)
-by t; (* LAcc *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-by t; (* NewC *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-by t; (* Expr *)
-by t; (* Call *)
-by t; (* LAcc *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-by t; (* Cons *)
-by t; (* Lit *)
-by (Simp_tac 1);
-by t; (* Nil *)
-by (Simp_tac 1);
-br max_spec_foo_Base 1;
-qed "wt_test";
-
-fun e thm = resolve_tac (NewCI::eval_evals_exec.intrs) 1 thm;
-
-Delsplits[split_if];
-Addsimps[init_vars_def,c_hupd_def,cast_ok_def];
-Goalw [test_def]
-" [|new_Addr (heap (snd s0)) = (a, None)|] ==> \
-\ tprg\\<turnstile>s0 -test-> ?s";
-(* ?s = s3 *)
-by e; (* ;; *)
-by e; (* Expr *)
-by e; (* LAss *)
-by e; (* NewC *)
-by (Force_tac 1);
-by (Force_tac 1);
-by (Simp_tac 1);
-be thin_rl 1;
-by e; (* Expr *)
-by e; (* Call *)
-by e; (* LAcc *)
-by (Force_tac 1);
-by e; (* Cons *)
-by e; (* Lit *)
-by e; (* Nil *)
-by (Simp_tac 1);
-by (force_tac (claset(), simpset() addsimps [foo_Ext_def]) 1);
-by (Simp_tac 1);
-by e; (* Expr *)
-by e; (* FAss *)
-by e;(* Cast *)
-by e;(* LAcc *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by e;(* XcptE *)
-by (Simp_tac 1);
-by (EVERY'[rtac (surjective_pairing RS sym RSN (2,trans)), stac Pair_eq,
- Force_tac] 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by e; (* XcptE *)
-bind_thm ("exec_test", simplify (simpset()) (result()));
--- a/src/HOL/MicroJava/J/Example.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Thu Feb 01 20:53:13 2001 +0100
@@ -28,7 +28,7 @@
}
*)
-Example = Eval +
+theory Example = Eval:
datatype cnam_ = Base_ | Ext_
datatype vnam_ = vee_ | x_ | e_
@@ -38,18 +38,23 @@
cnam_ :: "cnam_ => cname"
vnam_ :: "vnam_ => vnam"
-rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
+axioms (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
+
+ inj_cnam_: "(cnam_ x = cnam_ y) = (x = y)"
+ inj_vnam_: "(vnam_ x = vnam_ y) = (x = y)"
- inj_cnam_ "(cnam_ x = cnam_ y) = (x = y)"
- inj_vnam_ "(vnam_ x = vnam_ y) = (x = y)"
+ surj_cnam_: "\<exists>m. n = cnam_ m"
+ surj_vnam_: "\<exists>m. n = vnam_ m"
- surj_cnam_ "\\<exists>m. n = cnam_ m"
- surj_vnam_ "\\<exists>m. n = vnam_ m"
+declare inj_cnam_ [simp] inj_vnam_ [simp]
syntax
- Base, Ext :: cname
- vee, x, e :: vname
+ Base :: cname
+ Ext :: cname
+ vee :: vname
+ x :: vname
+ e :: vname
translations
@@ -59,51 +64,323 @@
"x" == "VName (vnam_ x_)"
"e" == "VName (vnam_ e_)"
-rules
- Base_not_Object "Base \\<noteq> Object"
- Ext_not_Object "Ext \\<noteq> Object"
+axioms
+
+ Base_not_Object: "Base \<noteq> Object"
+ Ext_not_Object: "Ext \<noteq> Object"
+
+declare Base_not_Object [simp] Ext_not_Object [simp]
+declare Base_not_Object [THEN not_sym, simp]
+declare Ext_not_Object [THEN not_sym, simp]
consts
- foo_Base :: java_mb
- foo_Ext :: java_mb
- BaseC, ExtC :: java_mb cdecl
- test :: stmt
- foo :: mname
- a,b :: loc
+ foo_Base:: java_mb
+ foo_Ext :: java_mb
+ BaseC :: "java_mb cdecl"
+ ExtC :: "java_mb cdecl"
+ test :: stmt
+ foo :: mname
+ a :: loc
+ b :: loc
defs
- foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
- BaseC_def "BaseC == (Base, (Object,
+ foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
+ BaseC_def:"BaseC == (Base, (Object,
[(vee, PrimT Boolean)],
[((foo,[Class Base]),Class Base,foo_Base)]))"
- foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
+ foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
(LAcc x)..vee:=Lit (Intg #1)),
Lit Null)"
- ExtC_def "ExtC == (Ext, (Base ,
+ ExtC_def: "ExtC == (Ext, (Base ,
[(vee, PrimT Integer)],
[((foo,[Class Base]),Class Ext,foo_Ext)]))"
- test_def "test == Expr(e::=NewC Ext);;
+ test_def:"test == Expr(e::=NewC Ext);;
Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
syntax
- NP :: xcpt
- tprg :: java_mb prog
- obj1, obj2 :: obj
- s0,s1,s2,s3,s4:: state
+ NP :: xcpt
+ tprg ::"java_mb prog"
+ obj1 :: obj
+ obj2 :: obj
+ s0 :: state
+ s1 :: state
+ s2 :: state
+ s3 :: state
+ s4 :: state
translations
"NP" == "NullPointer"
"tprg" == "[ObjectC, BaseC, ExtC]"
- "obj1" <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
- ((vee, Ext )\\<mapsto>Intg #0))"
+ "obj1" <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
+ ((vee, Ext )\<mapsto>Intg #0))"
"s0" == " Norm (empty, empty)"
- "s1" == " Norm (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
- "s2" == " Norm (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
- "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
+ "s1" == " Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+ "s2" == " Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+ "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+
+
+ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
+lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"
+apply (simp (no_asm))
+done
+lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa"
+apply (simp (no_asm_simp))
+done
+declare map_of_Cons [simp del]; (* sic! *)
+
+lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])"
+apply (unfold ObjectC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_Base [simp]:
+"class tprg Base = Some (Object,
+ [(vee, PrimT Boolean)],
+ [((foo, [Class Base]), Class Base, foo_Base)])"
+apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_Ext [simp]:
+"class tprg Ext = Some (Base,
+ [(vee, PrimT Integer)],
+ [((foo, [Class Base]), Class Ext, foo_Ext)])"
+apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma not_Object_subcls [elim!]: "(Object,C) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+done
+
+lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
+apply (erule rtrancl_induct)
+apply auto
+apply (drule subcls1D)
+apply auto
+done
+
+lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+done
+
+lemma class_tprgD:
+"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext"
+apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (auto split add: split_if_asm simp add: map_of_Cons)
+done
+
+lemma not_class_subcls_class [elim!]: "(C,C) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+apply (frule class_tprgD)
+apply (auto dest!:)
+apply (drule rtranclD)
+apply auto
+done
+
+lemma unique_classes: "unique tprg"
+apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def)
+done
+
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
+
+lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
+apply (rule subcls_direct)
+apply auto
+done
+
+lemma Ext_widen_Base [simp]: "tprg\<turnstile>Class Ext\<preceq> Class Base"
+apply (rule widen.subcls)
+apply (simp (no_asm))
+done
+
+declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
+
+lemma acyclic_subcls1_: "acyclic (subcls1 tprg)"
+apply (rule acyclicI)
+apply safe
+done
+
+lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]]
+
+lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]
+
+lemma fields_Object [simp]: "fields (tprg, Object) = []"
+apply (subst fields_rec_)
+apply auto
+done
+
+declare is_class_def [simp]
+
+lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
+apply (subst fields_rec_)
+apply auto
+done
+
+lemma fields_Ext [simp]:
+ "fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
+apply (rule trans)
+apply (rule fields_rec_)
+apply auto
+done
+
+lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma]
+
+lemma method_Object [simp]: "method (tprg,Object) = map_of []"
+apply (subst method_rec_)
+apply auto
+done
+
+lemma method_Base [simp]: "method (tprg, Base) = map_of
+ [((foo, [Class Base]), Base, (Class Base, foo_Base))]"
+apply (rule trans)
+apply (rule method_rec_)
+apply auto
+done
+
+lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of
+ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
+apply (rule trans)
+apply (rule method_rec_)
+apply auto
+done
+
+lemma wf_foo_Base:
+"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))"
+apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Base_def)
+apply auto
+done
+
+lemma wf_foo_Ext:
+"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))"
+apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Ext_def)
+apply auto
+apply (rule ty_expr_ty_exprs_wt_stmt.Cast)
+prefer 2
+apply (simp)
+apply (rule_tac [2] cast.subcls)
+apply (unfold field_def)
+apply auto
+done
+
+lemma wf_ObjectC:
+"wf_cdecl wf_java_mdecl tprg ObjectC"
+apply (unfold wf_cdecl_def wf_fdecl_def ObjectC_def)
+apply (simp (no_asm))
+done
+
+lemma wf_BaseC:
+"wf_cdecl wf_java_mdecl tprg BaseC"
+apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def)
+apply (simp (no_asm))
+apply (fold BaseC_def)
+apply (rule wf_foo_Base [THEN conjI])
+apply auto
+done
+
+lemma wf_ExtC:
+"wf_cdecl wf_java_mdecl tprg ExtC"
+apply (unfold wf_cdecl_def wf_fdecl_def ExtC_def)
+apply (simp (no_asm))
+apply (fold ExtC_def)
+apply (rule wf_foo_Ext [THEN conjI])
+apply auto
+apply (drule rtranclD)
+apply auto
+done
+
+lemma wf_tprg:
+"wf_prog wf_java_mdecl tprg"
+apply (unfold wf_prog_def Let_def)
+apply(simp add: wf_ObjectC wf_BaseC wf_ExtC unique_classes)
+done
+
+lemma appl_methds_foo_Base:
+"appl_methds tprg Base (foo, [NT]) =
+ {((Class Base, Class Base), [Class Base])}"
+apply (unfold appl_methds_def)
+apply (simp (no_asm))
+apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
+apply (auto simp add: map_of_Cons foo_Base_def)
+done
+
+lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) =
+ {((Class Base, Class Base), [Class Base])}"
+apply (unfold max_spec_def)
+apply (auto simp add: appl_methds_foo_Base)
+done
+
+ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
+lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>
+ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
+apply (tactic t) (* ;; *)
+apply (tactic t) (* Expr *)
+apply (tactic t) (* LAss *)
+apply (tactic t) (* LAcc *)
+apply (simp (no_asm))
+apply (simp (no_asm))
+apply (tactic t) (* NewC *)
+apply (simp (no_asm))
+apply (simp (no_asm))
+apply (tactic t) (* Expr *)
+apply (tactic t) (* Call *)
+apply (tactic t) (* LAcc *)
+apply (simp (no_asm))
+apply (simp (no_asm))
+apply (tactic t) (* Cons *)
+apply (tactic t) (* Lit *)
+apply (simp (no_asm))
+apply (tactic t) (* Nil *)
+apply (simp (no_asm))
+apply (rule max_spec_foo_Base)
+done
+
+ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *}
+
+declare split_if [split del]
+declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
+lemma exec_test:
+" [|new_Addr (heap (snd s0)) = (a, None)|] ==>
+ tprg\<turnstile>s0 -test-> ?s"
+apply (unfold test_def)
+(* ?s = s3 *)
+apply (tactic e) (* ;; *)
+apply (tactic e) (* Expr *)
+apply (tactic e) (* LAss *)
+apply (tactic e) (* NewC *)
+apply force
+apply force
+apply (simp (no_asm))
+apply (erule thin_rl)
+apply (tactic e) (* Expr *)
+apply (tactic e) (* Call *)
+apply (tactic e) (* LAcc *)
+apply force
+apply (tactic e) (* Cons *)
+apply (tactic e) (* Lit *)
+apply (tactic e) (* Nil *)
+apply (simp (no_asm))
+apply (force simp add: foo_Ext_def)
+apply (simp (no_asm))
+apply (tactic e) (* Expr *)
+apply (tactic e) (* FAss *)
+apply (tactic e) (* Cast *)
+apply (tactic e) (* LAcc *)
+apply (simp (no_asm))
+apply (simp (no_asm))
+apply (simp (no_asm))
+apply (tactic e) (* XcptE *)
+apply (simp (no_asm))
+apply (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
+apply (simp (no_asm))
+apply (simp (no_asm))
+apply (tactic e) (* XcptE *)
+done
+
end
--- a/src/HOL/MicroJava/J/JBasis.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: HOL/MicroJava/J/JBasis.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 TU Muenchen
-*)
-
-(*###TO Product_Type*)
-Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
-by (rtac refl 1);
-qed "select_split";
-
-Addsimps [Let_def];
-
-bind_thm ("if_def2", read_instantiate [("P","\\<lambda>x. x")] split_if);
-
-(* ### To HOL.ML *)
-Goal "[| ?!x. P x; P y |] ==> Eps P = y";
-by (rtac some_equality 1);
-by (atac 1);
-by (etac ex1E 1);
-by (etac all_dupE 1);
-by (fast_tac HOL_cs 1);
-qed "ex1_some_eq_trivial";
-
-
-section "unique";
-
-Goal "(x, y) : set xys --> x : fst ` set xys";
-by (induct_tac "xys" 1);
-by Auto_tac;
-qed_spec_mp "fst_in_set_lemma";
-
-Goalw [unique_def] "unique []";
-by (Simp_tac 1);
-qed "unique_Nil";
-
-Goalw [unique_def] "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))";
-by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
-qed "unique_Cons";
-
-Addsimps [unique_Nil,unique_Cons];
-
-Goal "unique l' ==> unique l --> \
-\ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')";
-by (induct_tac "l" 1);
-by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
-qed_spec_mp "unique_append";
-
-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()addsimps[inj_eq]));
-qed_spec_mp "unique_map_inj";
-
-(* More about Maps *)
-
-(*###Addsimps [fun_upd_same, fun_upd_other];*)
-
-Goal "unique l --> (k, x) : set l --> map_of l k = Some x";
-by (induct_tac "l" 1);
-by Auto_tac;
-qed_spec_mp "map_of_SomeI";
-
-Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)";
-by(induct_tac "l" 1);
-by(ALLGOALS Simp_tac);
-by Safe_tac;
-by Auto_tac;
-bind_thm("Ball_set_table",result() RS mp);
-
-Goal "map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
-\map_of t (k, k') = Some x";
-by (induct_tac "t" 1);
-by Auto_tac;
-qed_spec_mp "table_of_remap_SomeD";
-
-(* ### To Map.ML *)
-Goal "map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "map_of_map";
--- a/src/HOL/MicroJava/J/JBasis.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Thu Feb 01 20:53:13 2001 +0100
@@ -6,11 +6,69 @@
Some auxiliary definitions.
*)
-JBasis = Main +
+theory JBasis = Main:
+lemmas [simp] = Let_def
+
+section "unique"
+
constdefs
unique :: "('a \\<times> 'b) list => bool"
"unique == nodups \\<circ> map fst"
+
+lemma fst_in_set_lemma [rule_format (no_asm)]:
+ "(x, y) : set xys --> x : fst ` set xys"
+apply (induct_tac "xys")
+apply auto
+done
+
+lemma unique_Nil [simp]: "unique []"
+apply (unfold unique_def)
+apply (simp (no_asm))
+done
+
+lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
+apply (unfold unique_def)
+apply (auto dest: fst_in_set_lemma)
+done
+
+lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l -->
+ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
+apply (induct_tac "l")
+apply (auto dest: fst_in_set_lemma)
+done
+
+lemma unique_map_inj [rule_format (no_asm)]:
+ "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
+apply (induct_tac "l")
+apply (auto dest: fst_in_set_lemma simp add: inj_eq)
+done
+
+section "More about Maps"
+
+lemma map_of_SomeI [rule_format (no_asm)]:
+ "unique l --> (k, x) : set l --> map_of l k = Some x"
+apply (induct_tac "l")
+apply auto
+done
+
+lemma Ball_set_table_:
+ "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)"
+apply(induct_tac "l")
+apply(simp_all (no_asm))
+apply safe
+apply auto
+done
+lemmas Ball_set_table = Ball_set_table_ [THEN mp];
+
+lemma table_of_remap_SomeD [rule_format (no_asm)]:
+"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) -->
+ map_of t (k, k') = Some x"
+apply (induct_tac "t")
+apply auto
+done
+
end
+
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,330 +0,0 @@
-(* Title: HOL/MicroJava/J/JTypeSafe.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-
-Type safety proof
-*)
-
-
-
-Addsimps [split_beta];
-
-Goal "[|h a = None; (h, l)::\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> \
-\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)::\\<preceq>(G, lT)";
-by( etac conforms_upd_obj 1);
-by( rewtac oconf_def);
-by( auto_tac (claset() addSDs [fields_is_type], simpset()));
-qed "NewC_conforms";
-
-Goalw [cast_ok_def]
- "[| wf_prog wf_mb G; G,h\\<turnstile>v::\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v|] \
-\ ==> G,h\\<turnstile>v::\\<preceq>Class D";
-by( case_tac "v = Null" 1);
-by( Asm_full_simp_tac 1);
-by( dtac widen_RefT 1);
-by( Clarify_tac 1);
-by( datac non_npD 1 1);
-by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
-qed "Cast_conf";
-
-Goal "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\\<preceq>(G,lT); \
-\ x' = None --> G,h\\<turnstile>a'::\\<preceq> Class C; np a' x' = None |] ==> \
-\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\\<preceq>ft";
-by( dtac np_NoneD 1);
-by( etac conjE 1);
-by( mp_tac 1);
-by( dtac non_np_objD 1);
-by Auto_tac;
-by( dtac (conforms_heapD RS hconfD) 1);
-by( atac 1);
-by( datac widen_cfs_fields 2 1);
-by( datac oconf_objD 1 1);
-by Auto_tac;
-qed "FAcc_type_sound";
-
-Goal
- "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \
-\ (G, lT)\\<turnstile>v::T'; G\\<turnstile>T'\\<preceq>ft; \
-\ (G, lT)\\<turnstile>aa::Class C; \
-\ field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
-\ x' = None --> G,h'\\<turnstile>a'::\\<preceq> Class C; h'\\<le>|h; \
-\ (h, l)::\\<preceq>(G, lT); G,h\\<turnstile>x::\\<preceq>T'; np a' x' = None|] ==> \
-\ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and> \
-\ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)::\\<preceq>(G, lT) \\<and> \
-\ G,h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x))))\\<turnstile>x::\\<preceq>T'";
-by( dtac np_NoneD 1);
-by( etac conjE 1);
-by( Asm_full_simp_tac 1);
-by( dtac non_np_objD 1);
-by( atac 1);
-by( SELECT_GOAL Auto_tac 1);
-by( Clarify_tac 1);
-by( Full_simp_tac 1);
-by( EVERY [ftac hext_objD 1, atac 1]);
-by( etac exE 1);
-by( Asm_full_simp_tac 1);
-by( Clarify_tac 1);
-by( rtac conjI 1);
-by( fast_tac (HOL_cs addEs [hext_trans, hext_upd_obj]) 1);
-by( rtac conjI 1);
-by( fast_tac (HOL_cs addEs [conf_upd_obj RS iffD2]) 2);
-
-by( rtac conforms_upd_obj 1);
-by Auto_tac;
-by( rtac hextI 2);
-by( Force_tac 2);
-by( rtac oconf_hext 1);
-by( etac hext_upd_obj 2);
-by( dtac widen_cfs_fields 1);
-by( atac 1);
-by( atac 1);
-by( rtac (oconf_obj RS iffD2) 1);
-by( Simp_tac 1);
-by( strip_tac 1);
-by( case_tac "(aaa, b) = (fn, fd)" 1);
-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);
-qed "FAss_type_sound";
-
-Goalw [wf_mhead_def] "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \
- \ list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; \
-\ length pTs' = length pns; nodups pns; \
-\ Ball (set lvars) (split (\\<lambda>vn. is_type G)) \
-\ |] ==> G,h\\<turnstile>init_vars lvars(pns[\\<mapsto>]pvs)[::\\<preceq>]map_of lvars(pns[\\<mapsto>]pTs')";
-by( Clarsimp_tac 1);
-by( rtac lconf_ext_list 1);
-by( rtac (Ball_set_table RS lconf_init_vars) 1);
-by( Force_tac 1);
-by( atac 1);
-by( atac 1);
-by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
-qed "Call_lemma2";
-
-Goalw [wf_java_prog_def]
- "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); class G C = Some y; \
-\ max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
-\ list_all2 (conf G h) pvs pTsa;\
-\ (md, rT, pns, lvars, blk, res) = \
-\ the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
-\ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))::\\<preceq>(G, lT) --> \
-\ (G, lT)\\<turnstile>blk\\<surd> --> h\\<le>|xi \\<and> (xi, xl)::\\<preceq>(G, lT); \
-\ \\<forall>lT. (xi, xl)::\\<preceq>(G, lT) --> (\\<forall>T. (G, lT)\\<turnstile>res::T --> \
-\ xi\\<le>|h' \\<and> (h', xj)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>T)); \
-\ G,xh\\<turnstile>a'::\\<preceq> Class C |] ==> \
-\ xc\\<le>|h' \\<and> (h', l)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>rTa)";
-by( dtac max_spec2mheads 1);
-by( Clarify_tac 1);
-by( datac non_np_objD' 2 1);
-by( Clarsimp_tac 1);
-by( Clarsimp_tac 1);
-by( EVERY'[ftac hext_objD, atac] 1);
-by( Clarsimp_tac 1);
-by( datac Call_lemma 3 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);
-by( rtac conformsI 1);
-by( etac conforms_heapD 1);
-by( rtac lconf_ext 1);
-by( force_tac (claset() addSEs [Call_lemma2],simpset()) 1);
-by( EVERY'[etac conf_hext, etac conf_obj_AddrI, atac] 1);
-by( thin_tac "?E\\<turnstile>?blk\\<surd>" 1);
-by( etac conjE 1);
-by( EVERY'[dtac spec, mp_tac] 1);
-(*by( thin_tac "?E::\\<preceq>(G, pT')" 1);*)
-by( EVERY'[dtac spec, mp_tac] 1);
-by( thin_tac "?E\\<turnstile>res::?rT" 1);
-by( Clarify_tac 1);
-by( rtac conjI 1);
-by( fast_tac (HOL_cs addIs [hext_trans]) 1);
-by( rtac conjI 1);
-by( rtac impI 2);
-by( mp_tac 2);
-by( forward_tac [conf_widen] 2);
-by( atac 4);
-by( atac 2);
-by( fast_tac (HOL_cs addSEs [widen_trans]) 2);
-by( etac conforms_hext 1);
-by( etac hext_trans 1);
-by( atac 1);
-by( etac conforms_heapD 1);
-qed "Call_type_sound";
-
-
-
-Unify.search_bound := 40;
-Unify.trace_bound := 40;
-Delsplits[split_if];
-Delsimps[fun_upd_apply];
-Addsimps[fun_upd_same];
-val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
- (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
-Goal
-"wf_java_prog G ==> \
-\ (G\\<turnstile>(x,(h,l)) -e \\<succ>v -> (x', (h',l')) --> \
-\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (\\<forall>T . (G,lT)\\<turnstile>e :: T --> \
-\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT) \\<and> (x'=None --> G,h'\\<turnstile>v ::\\<preceq> T )))) \\<and> \
-\ (G\\<turnstile>(x,(h,l)) -es[\\<succ>]vs-> (x', (h',l')) --> \
-\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (\\<forall>Ts. (G,lT)\\<turnstile>es[::]Ts --> \
-\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT) \\<and> (x'=None --> list_all2 (\\<lambda>v T. G,h'\\<turnstile>v::\\<preceq>T) vs Ts)))) \\<and> \
-\ (G\\<turnstile>(x,(h,l)) -c -> (x', (h',l')) --> \
-\ (\\<forall>lT. (h ,l )::\\<preceq>(G,lT) --> (G,lT)\\<turnstile>c \\<surd> --> \
-\ h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT)))";
-by( rtac eval_evals_exec_induct 1);
-by( rewtac c_hupd_def);
-
-(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
-by( ALLGOALS Asm_full_simp_tac);
-by( ALLGOALS strip_tac);
-by( ALLGOALS (eresolve_tac ty_expr_ty_exprs_wt_stmt.elims
- THEN_ALL_NEW Full_simp_tac));
-by( ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac]));
-by( rewtac wf_java_prog_def);
-
-(* Level 7 *)
-
-(* 15 NewC *)
-by( dtac new_AddrD 1);
-by( etac disjE 1);
-by( Asm_simp_tac 2);
-by( Clarsimp_tac 1);
-by( rtac conjI 1);
-by( force_tac (claset() addSEs [NewC_conforms],simpset()) 1);
-by( rtac conf_obj_AddrI 1);
-by( rtac rtrancl_refl 2);
-by( Simp_tac 1);
-
-(* for Cast *)
-by( defer_tac 1);
-
-(* 14 Lit *)
-by( etac conf_litval 1);
-
-(* 13 BinOp *)
-by forward_hyp_tac;
-by forward_hyp_tac;
-by( EVERY'[rtac conjI, eatac hext_trans 1] 1);
-by( etac conjI 1);
-by( Clarsimp_tac 1);
-by( dtac eval_no_xcpt 1);
-by( asm_full_simp_tac (simpset() addsplits [binop.split]) 1);
-
-(* 12 LAcc *)
-by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);
-
-(* for FAss *)
-by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac,
- REPEAT o (etac conjE), hyp_subst_tac] 3);
-
-(* for if *)
-by( (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
-
-by forward_hyp_tac;
-
-(* 11+1 if *)
-by( fast_tac (HOL_cs addIs [hext_trans]) 8);
-by( fast_tac (HOL_cs addIs [hext_trans]) 8);
-
-(* 10 Expr *)
-by( Fast_tac 6);
-
-(* 9 ??? *)
-by( ALLGOALS Asm_full_simp_tac);
-
-(* 8 Cast *)
-by( EVERY'[rtac impI, dtac raise_if_NoneD, Clarsimp_tac,
- fast_tac (claset() addEs [Cast_conf])] 8);
-
-(* 7 LAss *)
-by( asm_simp_tac (simpset() addsplits [split_if]) 1);
-by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac] 1);
-by( blast_tac (claset() addIs [conforms_upd_local, conf_widen]) 1);
-
-(* 6 FAcc *)
-by( fast_tac (claset() addSEs [FAcc_type_sound]) 1);
-
-(* 5 While *)
-by(thin_tac "?a \\<longrightarrow> ?b" 5);
-by(datac ty_expr_ty_exprs_wt_stmt.Loop 1 5);
-by(force_tac (claset() addEs [hext_trans], simpset()) 5);
-
-by forward_hyp_tac;
-
-(* 4 Cons *)
-by( fast_tac (claset() addDs [evals_no_xcpt] addIs [conf_hext,hext_trans]) 3);
-
-(* 3 ;; *)
-by( fast_tac (claset() addIs [hext_trans]) 3);
-
-(* 2 FAss *)
-by( case_tac "x2 = None" 1);
-by( Asm_simp_tac 2);
-by( fast_tac (claset() addIs [hext_trans]) 2);
-by( Asm_full_simp_tac 1);
-by( dtac eval_no_xcpt 1);
-by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
-
-by prune_params_tac;
-(* Level 52 *)
-
-(* 1 Call *)
-by( case_tac "x" 1);
-by( Clarsimp_tac 2);
-by( dtac exec_xcpt 2);
-by( Asm_full_simp_tac 2);
-by( dtac eval_xcpt 2);
-by( Asm_full_simp_tac 2);
-by( fast_tac (HOL_cs addEs [hext_trans]) 2);
-by( Clarify_tac 1);
-by( dtac evals_no_xcpt 1);
-by( Asm_full_simp_tac 1);
-by( case_tac "a' = Null" 1);
-by( Asm_full_simp_tac 1);
-by( dtac exec_xcpt 1);
-by( Asm_full_simp_tac 1);
-by( dtac eval_xcpt 1);
-by( Asm_full_simp_tac 1);
-by( fast_tac (HOL_cs addEs [hext_trans]) 1);
-by( datac ty_expr_is_type 1 1);
-by(Clarsimp_tac 1);
-by(rewtac is_class_def);
-by(Clarsimp_tac 1);
-by( (rtac (rewrite_rule [wf_java_prog_def] Call_type_sound)
- THEN_ALL_NEW Asm_simp_tac) 1);
-qed "eval_evals_exec_type_sound";
-
-Goal "!!E s s'. \
-\ [| G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v -> (x',s'); s::\\<preceq>E; E\\<turnstile>e::T |] \
-\ ==> s'::\\<preceq>E \\<and> (x'=None --> G,heap s'\\<turnstile>v::\\<preceq>T)";
-by( split_all_tac 1);
-bd (eval_evals_exec_type_sound RS conjunct1 RS mp RS spec RS mp) 1;
-by Auto_tac;
-qed "eval_type_sound";
-
-Goal "!!E s s'. \
-\ [| G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -s0-> (x',s'); s::\\<preceq>E; E\\<turnstile>s0\\<surd> |] \
-\ ==> s'::\\<preceq>E";
-by( split_all_tac 1);
-bd (eval_evals_exec_type_sound RS conjunct2 RS conjunct2 RS mp RS spec RS mp) 1;
-by Auto_tac;
-qed "exec_type_sound";
-
-Goal "[|G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'-> Norm s'; a' \\<noteq> Null;\
-\ s::\\<preceq>E; E\\<turnstile>e::Class C; method (G,C) sig \\<noteq> None|] ==> \
-\ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
-by( datac eval_type_sound 4 1);
-by(Clarsimp_tac 1);
-by(rewtac wf_java_prog_def);
-by( forward_tac [widen_methd] 1);
-by( atac 1);
-by( Fast_tac 2);
-by( dtac non_npD 1);
-by Auto_tac;
-qed "all_methods_understood";
-
-Delsimps [split_beta];
-Addsimps[fun_upd_apply];
-
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Feb 01 20:53:13 2001 +0100
@@ -3,7 +3,357 @@
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
-Type Safety of Java
+Type Safety Proof for MicroJava
*)
-JTypeSafe = Eval + Conform
+theory JTypeSafe = Eval + Conform:
+
+declare split_beta [simp]
+
+lemma NewC_conforms:
+"[|h a = None; (h, l)::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==>
+ (h(a\<mapsto>(C,(init_vars (fields (G,C))))), l)::\<preceq>(G, lT)"
+apply( erule conforms_upd_obj)
+apply( unfold oconf_def)
+apply( auto dest!: fields_is_type)
+done
+
+lemma Cast_conf:
+ "[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>Class C; G\<turnstile>C\<preceq>? D; cast_ok G D h v|]
+ ==> G,h\<turnstile>v::\<preceq>Class D"
+apply (unfold cast_ok_def)
+apply( case_tac "v = Null")
+apply( simp)
+apply( drule widen_RefT)
+apply( clarify)
+apply( drule (1) non_npD)
+apply( auto intro!: conf_AddrI simp add: obj_ty_def)
+done
+
+lemma FAcc_type_sound:
+"[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\<preceq>(G,lT);
+ x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==>
+ G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft"
+apply( drule np_NoneD)
+apply( erule conjE)
+apply( erule (1) notE impE)
+apply( drule non_np_objD)
+apply auto
+apply( drule conforms_heapD [THEN hconfD])
+apply( assumption)
+apply( drule (2) widen_cfs_fields)
+apply( drule (1) oconf_objD)
+apply auto
+done
+
+lemma FAss_type_sound:
+ "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a);
+ (G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft;
+ (G, lT)\<turnstile>aa::Class C;
+ field (G,C) fn = Some (fd, ft); h''\<le>|h';
+ x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h;
+ (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==>
+ h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and>
+ (h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and>
+ G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'"
+apply( drule np_NoneD)
+apply( erule conjE)
+apply( simp)
+apply( drule non_np_objD)
+apply( assumption)
+apply( force)
+apply( clarify)
+apply( simp (no_asm_use))
+apply( frule (1) hext_objD)
+apply( erule exE)
+apply( simp)
+apply( clarify)
+apply( rule conjI)
+apply( fast elim: hext_trans hext_upd_obj)
+apply( rule conjI)
+prefer 2
+apply( fast elim: conf_upd_obj [THEN iffD2])
+
+apply( rule conforms_upd_obj)
+apply auto
+apply( rule_tac [2] hextI)
+prefer 2
+apply( force)
+apply( rule oconf_hext)
+apply( erule_tac [2] hext_upd_obj)
+apply( drule (2) widen_cfs_fields)
+apply( rule oconf_obj [THEN iffD2])
+apply( simp (no_asm))
+apply( intro strip)
+apply( case_tac "(aaa, b) = (fn, fd)")
+apply( simp)
+apply( fast intro: conf_widen)
+apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
+done
+
+lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;
+ list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;
+ length pTs' = length pns; nodups pns;
+ Ball (set lvars) (split (\<lambda>vn. is_type G))
+ |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
+apply (unfold wf_mhead_def)
+apply( clarsimp)
+apply( rule lconf_ext_list)
+apply( rule Ball_set_table [THEN lconf_init_vars])
+apply( force)
+apply( assumption)
+apply( assumption)
+apply( erule (2) conf_list_gext_widen)
+done
+
+lemma Call_type_sound:
+ "[| wf_java_prog G; a' \<noteq> Null; (h, l)::\<preceq>(G, lT); class G C = Some y;
+ max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h;
+ list_all2 (conf G h) pvs pTsa;
+ (md, rT, pns, lvars, blk, res) =
+ the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));
+ \<forall>lT. (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->
+ (G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xi, xl)::\<preceq>(G, lT);
+ \<forall>lT. (xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->
+ xi\<le>|h' \<and> (h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));
+ G,xh\<turnstile>a'::\<preceq> Class C |] ==>
+ xc\<le>|h' \<and> (h', l)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
+apply (unfold wf_java_prog_def)
+apply( drule max_spec2mheads)
+apply( clarify)
+apply( drule (2) non_np_objD')
+apply( clarsimp)
+apply( clarsimp)
+apply( frule (1) hext_objD)
+apply( clarsimp)
+apply( drule (3) Call_lemma)
+apply( clarsimp simp add: wf_java_mdecl_def)
+apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
+apply( drule spec, erule impE)
+apply( erule_tac [2] notE impE, tactic "assume_tac 2")
+apply( rule conformsI)
+apply( erule conforms_heapD)
+apply( rule lconf_ext)
+apply( force elim!: Call_lemma2)
+apply( erule conf_hext, erule (1) conf_obj_AddrI)
+apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
+apply( erule conjE)
+apply( drule spec, erule (1) impE)
+apply( drule spec, erule (1) impE)
+apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
+apply( clarify)
+apply( rule conjI)
+apply( fast intro: hext_trans)
+apply( rule conjI)
+apply( rule_tac [2] impI)
+apply( erule_tac [2] notE impE, tactic "assume_tac 2")
+apply( frule_tac [2] conf_widen)
+apply( tactic "assume_tac 4")
+apply( tactic "assume_tac 2")
+prefer 2
+apply( fast elim!: widen_trans)
+apply( erule conforms_hext)
+apply( erule (1) hext_trans)
+apply( erule conforms_heapD)
+done
+
+declare split_if [split del]
+declare fun_upd_apply [simp del]
+declare fun_upd_same [simp]
+ML{*
+val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
+ (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
+*}
+ML{*
+Unify.search_bound := 40;
+Unify.trace_bound := 40
+*}
+theorem eval_evals_exec_type_sound:
+"wf_java_prog G ==>
+ (G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) -->
+ (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T -->
+ h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v ::\<preceq> T )))) \<and>
+ (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->
+ (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->
+ h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and>
+ (G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) -->
+ (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> -->
+ h\<le>|h' \<and> (h',l')::\<preceq>(G,lT)))"
+apply( rule eval_evals_exec_induct)
+apply( unfold c_hupd_def)
+
+(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
+apply( simp_all)
+apply( tactic "ALLGOALS strip_tac")
+apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *})
+apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
+apply( unfold wf_java_prog_def)
+
+(* Level 7 *)
+
+(* 15 NewC *)
+apply( drule new_AddrD)
+apply( erule disjE)
+prefer 2
+apply( simp (no_asm_simp))
+apply( clarsimp)
+apply( rule conjI)
+apply( force elim!: NewC_conforms)
+apply( rule conf_obj_AddrI)
+apply( rule_tac [2] rtrancl_refl)
+apply( simp (no_asm))
+
+(* for Cast *)
+defer 1
+
+(* 14 Lit *)
+apply( erule conf_litval)
+
+(* 13 BinOp *)
+apply (tactic "forward_hyp_tac")
+apply (tactic "forward_hyp_tac")
+apply( rule conjI, erule (1) hext_trans)
+apply( erule conjI)
+apply( clarsimp)
+apply( drule eval_no_xcpt)
+apply( simp split add: binop.split)
+
+(* 12 LAcc *)
+apply( fast elim: conforms_localD [THEN lconfD])
+
+(* for FAss *)
+apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
+
+(* for if *)
+apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
+
+apply (tactic "forward_hyp_tac")
+
+(* 11+1 if *)
+prefer 8
+apply( fast intro: hext_trans)
+prefer 8
+apply( fast intro: hext_trans)
+
+(* 10 Expr *)
+prefer 6
+apply( fast)
+
+(* 9 ??? *)
+apply( simp_all)
+
+(* 8 Cast *)
+prefer 8
+apply (rule impI)
+apply (drule raise_if_NoneD)
+apply (clarsimp)
+apply (fast elim: Cast_conf)
+
+(* 7 LAss *)
+apply (fold fun_upd_def)
+apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) 1 *})
+apply( blast intro: conforms_upd_local conf_widen)
+
+(* 6 FAcc *)
+apply( fast elim!: FAcc_type_sound)
+
+(* 5 While *)
+prefer 5
+apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
+apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
+apply(force elim: hext_trans)
+
+apply (tactic "forward_hyp_tac")
+
+(* 4 Cons *)
+prefer 3
+apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
+
+(* 3 ;; *)
+prefer 3
+apply( fast intro: hext_trans)
+
+(* 2 FAss *)
+apply( case_tac "x2 = None")
+prefer 2
+apply( simp (no_asm_simp))
+apply( fast intro: hext_trans)
+apply( simp)
+apply( drule eval_no_xcpt)
+apply( erule FAss_type_sound, simp (no_asm) (*###rule refl*), assumption+)
+
+apply( tactic prune_params_tac)
+(* Level 52 *)
+
+(* 1 Call *)
+apply( case_tac "x")
+prefer 2
+apply( clarsimp)
+apply( drule exec_xcpt)
+apply( simp)
+apply( drule_tac eval_xcpt)
+apply( simp)
+apply( fast elim: hext_trans)
+apply( clarify)
+apply( drule evals_no_xcpt)
+apply( simp)
+apply( case_tac "a' = Null")
+apply( simp)
+apply( drule exec_xcpt)
+apply( simp)
+apply( drule eval_xcpt)
+apply( simp)
+apply( fast elim: hext_trans)
+apply( drule (1) ty_expr_is_type)
+apply(clarsimp)
+apply(unfold is_class_def)
+apply(clarsimp)
+apply(rule Call_type_sound [unfolded wf_java_prog_def]);
+prefer 11
+apply blast
+apply (simp (no_asm_simp))+
+done
+ML{*
+Unify.search_bound := 20;
+Unify.trace_bound := 20
+*}
+
+lemma eval_type_sound: "!!E s s'.
+ [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); s::\<preceq>E; E\<turnstile>e::T |]
+ ==> s'::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply (drule eval_evals_exec_type_sound
+ [THEN conjunct1, THEN mp, THEN spec, THEN mp])
+apply auto
+done
+
+lemma exec_type_sound: "!!E s s'.
+ [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); s::\<preceq>E; E\<turnstile>s0\<surd> |]
+ ==> s'::\<preceq>E"
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply (drule eval_evals_exec_type_sound
+ [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
+apply auto
+done
+
+theorem all_methods_understood:
+"[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null;
+ s::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>
+ method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
+apply( drule (4) eval_type_sound)
+apply(clarsimp)
+apply(unfold wf_java_prog_def)
+apply( frule widen_methd)
+apply( assumption)
+prefer 2
+apply( fast)
+apply( drule non_npD)
+apply auto
+done
+
+declare split_beta [simp del]
+declare fun_upd_apply [simp]
+
+end
+
+
--- a/src/HOL/MicroJava/J/State.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-(* Title: HOL/MicroJava/J/State.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-Goalw [obj_ty_def] "obj_ty (C,fs) = Class C";
-by (Simp_tac 1);
-qed "obj_ty_def2";
-Addsimps [obj_ty_def2];
-
-Goalw [new_Addr_def]
-"(a,x) = new_Addr h ==> h a = None \\<and> x = None | x = Some OutOfMemory";
-by(asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1);
-by(rtac someI 1);
-by(rtac disjI2 1);
-by(res_inst_tac [("r","snd (?a,Some OutOfMemory)")] trans 1);
-by Auto_tac;
-qed "new_AddrD";
-
-
-Goalw [raise_if_def] "raise_if True x y \\<noteq> None";
-by Auto_tac;
-qed "raise_if_True";
-
-Goalw [raise_if_def] "raise_if False x y = y";
-by Auto_tac;
-qed "raise_if_False";
-
-Goalw [raise_if_def] "raise_if c x (Some y) \\<noteq> None";
-by Auto_tac;
-qed "raise_if_Some";
-
-Goalw [raise_if_def] "raise_if c z (if x = None then Some y else x) \\<noteq> None";
-by(induct_tac "x" 1);
-by Auto_tac;
-qed "raise_if_Some2";
-
-Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2];
-
-Goalw [raise_if_def]
- "raise_if c x y = Some z \\<longrightarrow> c \\<and> Some z = Some x | y = Some z";
-by Auto_tac;
-qed_spec_mp "raise_if_SomeD";
-
-Goalw [raise_if_def] "raise_if c x y = None --> \\<not> c \\<and> y = None";
-by Auto_tac;
-qed_spec_mp "raise_if_NoneD";
-
-Goalw [np_def, raise_if_def] "np a' x' = None --> x' = None \\<and> a' \\<noteq> Null";
-by Auto_tac;
-qed_spec_mp "np_NoneD";
-
-Goalw [np_def, raise_if_def] "a' \\<noteq> Null --> np a' x' = x'";
-by Auto_tac;
-qed_spec_mp "np_None";
-
-Goalw [np_def, raise_if_def] "np a' (Some xc) = Some xc";
-by Auto_tac;
-qed "np_Some";
-
-Goalw [np_def, raise_if_def] "np Null None = Some NullPointer";
-by Auto_tac;
-qed "np_Null";
-
-Goalw [np_def, raise_if_def] "np (Addr a) None = None";
-by Auto_tac;
-qed "np_Addr";
-
-Addsimps[np_None, np_Some,np_Null,np_Addr];
-
-Goalw [raise_if_def] "(np Null (raise_if c xc None)) = \
-\ Some (if c then xc else NullPointer)";
-by (Simp_tac 1);
-qed "np_raise_if";
-Addsimps[np_raise_if];
-
-
-
-
-
--- a/src/HOL/MicroJava/J/State.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/State.thy Thu Feb 01 20:53:13 2001 +0100
@@ -6,34 +6,34 @@
State for evaluation of Java expressions and statements
*)
-State = TypeRel + Value +
+theory State = TypeRel + Value:
types fields_
- = "(vname \\<times> cname \\<leadsto> val)" (* field name, defining class, value *)
+ = "(vname \<times> cname \<leadsto> val)" (* field name, defining class, value *)
- obj = "cname \\<times> fields_" (* class instance with class name and fields *)
+ obj = "cname \<times> fields_" (* class instance with class name and fields *)
constdefs
obj_ty :: "obj => ty"
"obj_ty obj == Class (fst obj)"
- init_vars :: "('a \\<times> ty) list => ('a \\<leadsto> val)"
- "init_vars == map_of o map (\\<lambda>(n,T). (n,default_val T))"
+ init_vars :: "('a \<times> ty) list => ('a \<leadsto> val)"
+ "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
datatype xcpt (* exceptions *)
= NullPointer
| ClassCast
| OutOfMemory
-types aheap = "loc \\<leadsto> obj" (* "heap" used in a translation below *)
- locals = "vname \\<leadsto> val"
+types aheap = "loc \<leadsto> obj" (* "heap" used in a translation below *)
+ locals = "vname \<leadsto> val"
state (* simple state, i.e. variable contents *)
- = "aheap \\<times> locals"
+ = "aheap \<times> locals"
(* heap, local parameter including This *)
xstate (* state including exception information *)
- = "xcpt option \\<times> state"
+ = "xcpt option \<times> state"
syntax
heap :: "state => aheap"
@@ -47,19 +47,98 @@
constdefs
- new_Addr :: "aheap => loc \\<times> xcpt option"
- "new_Addr h == SOME (a,x). (h a = None \\<and> x = None) | x = Some OutOfMemory"
+ new_Addr :: "aheap => loc \<times> xcpt option"
+ "new_Addr h == SOME (a,x). (h a = None \<and> x = None) | x = Some OutOfMemory"
raise_if :: "bool => xcpt => xcpt option => xcpt option"
- "raise_if c x xo == if c \\<and> (xo = None) then Some x else xo"
+ "raise_if c x xo == if c \<and> (xo = None) then Some x else xo"
np :: "val => xcpt option => xcpt option"
"np v == raise_if (v = Null) NullPointer"
c_hupd :: "aheap => xstate => xstate"
- "c_hupd h'== \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
+ "c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
cast_ok :: "'c prog => cname => aheap => val => bool"
- "cast_ok G C h v == v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C"
+ "cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"
+
+lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C"
+apply (unfold obj_ty_def)
+apply (simp (no_asm))
+done
+
+lemma new_AddrD:
+"(a,x) = new_Addr h ==> h a = None \<and> x = None | x = Some OutOfMemory"
+apply (unfold new_Addr_def)
+apply(simp add: Pair_fst_snd_eq Eps_split)
+apply(rule someI)
+apply(rule disjI2)
+apply(rule_tac "r" = "snd (?a,Some OutOfMemory)" in trans)
+apply auto
+done
+
+
+lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma raise_if_False [simp]: "raise_if False x y = y"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma raise_if_Some [simp]: "raise_if c x (Some y) \<noteq> None"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma raise_if_Some2 [simp]: "raise_if c z (if x = None then Some y else x) \<noteq> None"
+apply (unfold raise_if_def)
+apply(induct_tac "x")
+apply auto
+done
+
+lemma raise_if_SomeD [rule_format (no_asm)]:
+ "raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some x | y = Some z"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma raise_if_NoneD [rule_format (no_asm)]: "raise_if c x y = None --> \<not> c \<and> y = None"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma np_NoneD [rule_format (no_asm)]: "np a' x' = None --> x' = None \<and> a' \<noteq> Null"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_None [rule_format (no_asm), simp]: "a' \<noteq> Null --> np a' x' = x'"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_Some [simp]: "np a' (Some xc) = Some xc"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_Null [simp]: "np Null None = Some NullPointer"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_Addr [simp]: "np (Addr a) None = None"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) =
+ Some (if c then xc else NullPointer)"
+apply (unfold raise_if_def)
+apply (simp (no_asm))
+done
end
--- a/src/HOL/MicroJava/J/Term.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Term.thy Thu Feb 01 20:53:13 2001 +0100
@@ -6,7 +6,7 @@
Java expressions and statements
*)
-Term = Value +
+theory Term = Value:
datatype binop = Eq | Add (* function codes for binary operation *)
@@ -21,7 +21,7 @@
| FAss cname expr vname
expr (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
| Call cname expr mname
- (ty list) (expr list) (* method call*) ("{_}_.._'( {_}_')"
+ "ty list" "expr list" (* method call*) ("{_}_.._'( {_}_')"
[10,90,99,10,10] 90)
datatype stmt
@@ -32,3 +32,4 @@
| Loop expr stmt ("While '(_') _" [80,79]70)
end
+
--- a/src/HOL/MicroJava/J/Type.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Thu Feb 01 20:53:13 2001 +0100
@@ -6,13 +6,14 @@
Java types
*)
-Type = JBasis +
+theory Type = JBasis:
-types cname (* class name *)
- vnam (* variable or field name *)
- mname (* method name *)
-
-arities cname, vnam, mname :: term
+typedecl cname (* class name *)
+typedecl vnam (* variable or field name *)
+typedecl mname (* method name *)
+arities cname :: "term"
+ vnam :: "term"
+ mname :: "term"
datatype vname (* names for This pointer and local/field variables *)
= This
--- a/src/HOL/MicroJava/J/TypeRel.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(* Title: HOL/MicroJava/J/TypeRel.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-Goalw [subcls1_def]
- "G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> C \\<noteq> Object \\<and> (\\<exists>fs ms. class G C = Some (D,fs,ms))";
-by Auto_tac;
-qed "subcls1D";
-Goalw [subcls1_def] "\\<lbrakk>class G C = Some (D,rest); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D";
-by Auto_tac;
-qed "subcls1I";
-
-Goalw [subcls1_def, is_class_def]
-"subcls1 G = (\\<Sigma>C\\<in>{C. is_class G C} . {D. C\\<noteq>Object \\<and> fst (the (class G C))=D})";
-by Auto_tac;
-qed "subcls1_def2";
-
-Goal "finite (subcls1 G)";
-by(stac subcls1_def2 1);
-by( rtac (finite_is_class RS finite_SigmaI) 1);
-by(res_inst_tac [("B","{fst (the (class G C))}")] finite_subset 1);
-by Auto_tac;
-qed "finite_subcls1";
-
-
-Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
-by(etac trancl_trans_induct 1);
-by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
-qed "subcls_is_class";
-
-Goalw [is_class_def] "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
-by (etac rtrancl_induct 1);
-by (dtac subcls1D 2);
-by Auto_tac;
-qed_spec_mp "subcls_is_class2";
-
-(* A particular thm about wf;
- looks like it is an odd instance of something more general
-*)
-Goalw [wf_def] "wf{((A,x),(B,y)) . A=B \\<and> wf(R(A)) \\<and> (x,y)\\<in>R(A)}";
-by(full_simp_tac (simpset() delcongs [imp_cong]) 1);
-by(strip_tac 1);
-by(rename_tac "A x" 1);
-by(case_tac "wf(R A)" 1);
-by (eres_inst_tac [("a","x")] wf_induct 1);
-by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
-by (Fast_tac 1);
-by(rewrite_goals_tac [wf_def]);
-by(Blast_tac 1);
-qed "wf_rel_lemma";
-
-
-(* Proving the termination conditions *)
-
-goalw thy [subcls1_rel_def] "wf subcls1_rel";
-by(rtac (wf_rel_lemma RS wf_subset) 1);
-by(Force_tac 1);
-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)))))
- (K [auto_tac (claset() addIs [subcls1I], simpset())]);
-
-val fields_TC = prove_goalw_cterm [subcls1_rel_def]
- (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (fields.tcs)))))
- (K [auto_tac (claset() addIs [subcls1I], simpset())]);
-
-Goalw [field_def]
-"field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT";
-by (rtac table_of_remap_SomeD 1);
-by (Asm_full_simp_tac 1);
-qed "field_fields";
-
-AddSIs [widen.refl,widen.null];
-Addsimps [widen.refl];
-
-Goal "(G\\<turnstile>PrimT pT\\<preceq>RefT rT) = False";
-br iffI 1;
-be widen.elim 1;
-by Auto_tac;
-qed "widen_PrimT_RefT";
-AddIffs [widen_PrimT_RefT];
-
-Goal "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)";
-by (etac widen.elim 1);
-by Auto_tac;
-qed "widen_RefT_lemma";
-Goal "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t";
-by (dtac widen_RefT_lemma 1);
-by Auto_tac;
-qed "widen_RefT";
-
-Goal "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)";
-by (etac widen.elim 1);
-by Auto_tac;
-qed "widen_RefT2_lemma";
-Goal "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t";
-by (dtac widen_RefT2_lemma 1);
-by Auto_tac;
-qed "widen_RefT2";
-
-Goal "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)";
-by (etac widen.elim 1);
-by Auto_tac;
-qed "widen_Class_lemma";
-Goal "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D";
-by (dtac widen_Class_lemma 1);
-by Auto_tac;
-qed "widen_Class";
-
-Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False";
-br iffI 1;
-be widen.elim 1;
-by(Auto_tac);
-qed "widen_Class_NullT";
-AddIffs [widen_Class_NullT];
-
-Goal "(G\\<turnstile>Class C\\<preceq> Class D) = (G\\<turnstile>C\\<preceq>C D)";
-br iffI 1;
-be widen.elim 1;
-by(Auto_tac);
-bes widen.intrs 1;
-qed "widen_Class_Class";
-AddIffs [widen_Class_Class];
-
-Goal "G\\<turnstile>S\\<preceq>U ==> \\<forall>T. G\\<turnstile>U\\<preceq>T --> G\\<turnstile>S\\<preceq>T";
-by( etac widen.induct 1);
-by Safe_tac;
-by( ALLGOALS (forward_tac [widen_Class, widen_RefT]));
-by Safe_tac;
-by(eatac rtrancl_trans 1 1);
-qed_spec_mp "widen_trans";
--- a/src/HOL/MicroJava/J/TypeRel.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Feb 01 20:53:13 2001 +0100
@@ -6,18 +6,18 @@
The relations between Java types
*)
-TypeRel = Decl +
+theory TypeRel = Decl:
consts
- subcls1 :: "'c prog => (cname \\<times> cname) set" (* subclass *)
- widen :: "'c prog => (ty \\<times> ty ) set" (* widening *)
- cast :: "'c prog => (cname \\<times> cname) set" (* casting *)
+ subcls1 :: "'c prog => (cname \<times> cname) set" (* subclass *)
+ widen :: "'c prog => (ty \<times> ty ) set" (* widening *)
+ cast :: "'c prog => (cname \<times> cname) set" (* casting *)
syntax
- subcls1 :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<prec>C1 _" [71,71,71] 70)
- subcls :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>C _" [71,71,71] 70)
- widen :: "'c prog => [ty , ty ] => bool" ("_ \\<turnstile> _ \\<preceq> _" [71,71,71] 70)
- cast :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>? _" [71,71,71] 70)
+ subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
+ subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
+ widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
+ cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
syntax (HTML)
subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
@@ -26,58 +26,215 @@
cast :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
translations
- "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
- "G\\<turnstile>C \\<preceq>C D" == "(C,D) \\<in> (subcls1 G)^*"
- "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G"
- "G\\<turnstile>C \\<preceq>? D" == "(C,D) \\<in> cast G"
+ "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
+ "G\<turnstile>C \<preceq>C D" == "(C,D) \<in> (subcls1 G)^*"
+ "G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G"
+ "G\<turnstile>C \<preceq>? D" == "(C,D) \<in> cast G"
defs
(* direct subclass, cf. 8.1.3 *)
- subcls1_def"subcls1 G \\<equiv> {(C,D). C\\<noteq>Object \\<and> (\\<exists>c. class G C=Some c \\<and> fst c=D)}"
+ subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class G C=Some c \<and> fst c=D)}"
+lemma subcls1D:
+ "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
+apply (unfold subcls1_def)
+apply auto
+done
+
+lemma subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
+apply (unfold subcls1_def)
+apply auto
+done
+
+lemma subcls1_def2:
+"subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
+apply (unfold subcls1_def is_class_def)
+apply auto
+done
+
+lemma finite_subcls1: "finite (subcls1 G)"
+apply(subst subcls1_def2)
+apply(rule finite_SigmaI [OF finite_is_class])
+apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
+apply auto
+done
+
+lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ ==> is_class G C"
+apply (unfold is_class_def)
+apply(erule trancl_trans_induct)
+apply (auto dest!: subcls1D)
+done
+
+lemma subcls_is_class2 [rule_format (no_asm)]: "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
+apply (unfold is_class_def)
+apply (erule rtrancl_induct)
+apply (drule_tac [2] subcls1D)
+apply auto
+done
+
+consts class_rec ::"'c prog \<times> cname \<Rightarrow>
+ 'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
+recdef class_rec "same_fst (\<lambda>G. wf ((subcls1 G)^-1)) (\<lambda>G. (subcls1 G)^-1)"
+ "class_rec (G,C) = (\<lambda>t f. case class G C of None \<Rightarrow> arbitrary
+ | Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^-1) then
+ f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)"
+recdef_tc class_rec_tc: class_rec
+ apply (unfold same_fst_def)
+ apply (auto intro: subcls1I)
+ done
+
+lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow>
+ class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)";
+ apply (rule class_rec_tc [THEN class_rec.simps
+ [THEN trans [THEN fun_cong [THEN fun_cong]]]])
+ apply (rule ext, rule ext)
+ apply auto
+ done
+
consts
- method :: "'c prog \\<times> cname => ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
- field :: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
- fields :: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times> ty) list"
-
-constdefs (* auxiliary relation for recursive definitions below *)
-
- subcls1_rel :: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
- "subcls1_rel == {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}"
+ method :: "'c prog \<times> cname => ( sig \<leadsto> cname \<times> ty \<times> 'c)" (* ###curry *)
+ field :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty )" (* ###curry *)
+ fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
-recdef method "subcls1_rel"
- "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
- | Some (D,fs,ms) => (if C = Object then empty else
- if is_class G D then method (G,D)
- else arbitrary) ++
- map_of (map (\\<lambda>(s, m ).
- (s,(C,m))) ms))
- else arbitrary)"
+defs method_def: "method \<equiv> \<lambda>(G,C). class_rec (G,C) empty (\<lambda>C fs ms ts.
+ ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
+
+lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
+ method (G,C) = (if C = Object then empty else method (G,D)) ++
+ map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
+apply (unfold method_def)
+apply (simp split del: split_if)
+apply (erule (1) class_rec_lemma [THEN trans]);
+apply auto
+done
+
(* list of fields of a class, including inherited and hidden ones *)
-recdef fields "subcls1_rel"
- "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
- | Some (D,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
- (if C = Object then [] else
- if is_class G D then fields (G,D)
- else arbitrary))
- else arbitrary)"
-defs
+defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec (G,C) [] (\<lambda>C fs ms ts.
+ map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
+
+lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
+ fields (G,C) =
+ map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
+apply (unfold fields_def)
+apply (simp split del: split_if)
+apply (erule (1) class_rec_lemma [THEN trans]);
+apply auto
+done
+
+
+defs field_def: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+
+lemma field_fields:
+"field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
+apply (unfold field_def)
+apply (rule table_of_remap_SomeD)
+apply simp
+done
+
+
+inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3
+ i.e. sort of syntactic subtyping *)
+ refl [intro!, simp]: "G\<turnstile> T \<preceq> T" (* identity conv., cf. 5.1.1 *)
+ subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
+ null [intro!]: "G\<turnstile> NT \<preceq> RefT R"
- field_def "field == map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *)
+ (* left out casts on primitve types *)
+ widen: "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
+ subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
+
+lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
+apply (rule iffI)
+apply (erule widen.elims)
+apply auto
+done
+
+lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply auto
+done
+
+lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply auto
+done
+
+lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply auto
+done
+
+lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
+apply (rule iffI)
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply auto
+done
-inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
- i.e. sort of syntactic subtyping *)
- refl "G\\<turnstile> T \\<preceq> T" (* identity conv., cf. 5.1.1 *)
- subcls "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>Class C \\<preceq> Class D"
- null "G\\<turnstile> NT \\<preceq> RefT R"
+lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
+apply (rule iffI)
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (auto elim: widen.subcls)
+done
+
+lemma widen_trans [rule_format (no_asm)]: "G\<turnstile>S\<preceq>U ==> \<forall>T. G\<turnstile>U\<preceq>T --> G\<turnstile>S\<preceq>T"
+apply (erule widen.induct)
+apply safe
+apply (frule widen_Class)
+apply (frule_tac [2] widen_RefT)
+apply safe
+apply(erule (1) rtrancl_trans)
+done
+
+ML {* InductAttrib.print_global_rules(the_context()) *}
+ML {* set show_tags *}
-inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
- (* left out casts on primitve types *)
- widen "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>C \\<preceq>? D"
- subcls "G\\<turnstile>D\\<preceq>C C ==> G\\<turnstile>C \\<preceq>? D"
+(*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
+proof -
+ assume "G\<turnstile>S\<preceq>U"
+ thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
+ proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1])
+ case refl
+ fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
+ (* fix T' show "PROP ?P T T".*)
+ next
+ case subcls
+ fix T assume "G\<turnstile>Class D\<preceq>T"
+ then obtain E where "T = Class E" by (blast dest: widen_Class)
+ from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
+ next
+ case null
+ fix RT assume "G\<turnstile>RefT R\<preceq>RT"
+ then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
+ thus "G\<turnstile>NT\<preceq>RT" by auto
+ qed
+qed
+*)
+
+theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
+proof -
+ assume "G\<turnstile>S\<preceq>U"
+ thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
+ proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *)
+ case refl
+ fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
+ (* fix T' show "PROP ?P T T".*)
+ next
+ case subcls
+ fix T assume "G\<turnstile>Class D\<preceq>T"
+ then obtain E where "T = Class E" by (blast dest: widen_Class)
+ from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
+ next
+ case null
+ fix RT assume "G\<turnstile>RefT R\<preceq>RT"
+ then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
+ thus "G\<turnstile>NT\<preceq>RT" by auto
+ qed
+qed
+
+
end
--- a/src/HOL/MicroJava/J/Value.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Value.thy Thu Feb 01 20:53:13 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/MicroJava/J/Term.thy
+(* Title: HOL/MicroJava/J/Value.thy
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
@@ -6,12 +6,12 @@
Java values
*)
-Value = Type +
+theory Value = Type:
-types loc (* locations, i.e. abstract references on objects *)
-arities loc :: term
+typedecl loc (* locations, i.e. abstract references on objects *)
+arities loc :: "term"
-datatype val_ (* name non 'val' because of clash with ML token *)
+datatype val
= Unit (* dummy result value of void methods *)
| Null (* null reference *)
| Bool bool (* Boolean value *)
@@ -19,9 +19,6 @@
of clash with HOL/Set.thy *)
| Addr loc (* addresses, i.e. locations of objects *)
-types val = val_
-translations "val" <= (type) "val_"
-
consts
the_Bool :: "val => bool"
the_Intg :: "val => int"
--- a/src/HOL/MicroJava/J/WellForm.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,349 +0,0 @@
-(* Title: HOL/MicroJava/J/WellForm.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-Goalw [wf_prog_def, class_def]
- "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)";
-by (Asm_full_simp_tac 1);
-by (fast_tac (set_cs addDs [map_of_SomeD]) 1);
-qed "class_wf";
-
-Goalw [wf_prog_def, ObjectC_def, class_def]
- "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])";
-by (auto_tac (claset() addIs [map_of_SomeI], simpset()));
-qed "class_Object";
-Addsimps [class_Object];
-
-Goalw [is_class_def] "wf_prog wf_mb G ==> is_class G Object";
-by (Asm_simp_tac 1);
-qed "is_class_Object";
-Addsimps [is_class_Object];
-
-Goal "[|G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G|] ==> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
-by( forward_tac [r_into_trancl] 1);
-by( dtac subcls1D 1);
-by(Clarify_tac 1);
-by( datac class_wf 1 1);
-by( rewtac wf_cdecl_def);
-by(force_tac (claset(), simpset() addsimps [thm"reflcl_trancl" RS sym]
- delsimps [thm"reflcl_trancl"]) 1);
-qed "subcls1_wfD";
-
-Goalw [wf_cdecl_def]
-"!!r. \\<lbrakk>wf_cdecl wf_mb G (C,D,r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> is_class G D";
-by (auto_tac (claset(), simpset() addsplits [option.split_asm]));
-qed "wf_cdecl_supD";
-
-Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> \\<not>(D,C)\\<in>(subcls1 G)^+";
-by(etac tranclE 1);
-by(TRYALL(fast_tac (claset() addSDs [subcls1_wfD] addIs [trancl_trans])));
-qed "subcls_asym";
-
-Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D";
-by (etac trancl_trans_induct 1);
-by (auto_tac (claset() addDs [subcls1_wfD,subcls_asym],simpset()));
-qed "subcls_irrefl";
-
-Goalw [acyclic_def] "wf_prog wf_mb G ==> acyclic (subcls1 G)";
-by (fast_tac (claset() addDs [subcls_irrefl]) 1);
-qed "acyclic_subcls1";
-
-Goal "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)";
-by (rtac finite_acyclic_wf 1);
-by ( stac finite_converse 1);
-by ( rtac finite_subcls1 1);
-by (stac acyclic_converse 1);
-by (etac acyclic_subcls1 1);
-qed "wf_subcls1";
-
-val major::prems = goal thy
- "[|wf_prog wf_mb G; !!C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C";
-by(cut_facts_tac [major RS wf_subcls1] 1);
-by(dtac wf_trancl 1);
-by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
-by(eres_inst_tac [("a","C")] wf_induct 1);
-by(resolve_tac prems 1);
-by(Auto_tac);
-qed "subcls_induct";
-
-val prems = goalw thy [is_class_def] "[|is_class G C; wf_prog wf_mb G; P Object; \
-\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \\<and> \
-\ wf_cdecl wf_mb G (C,D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
-\ |] ==> P C";
-by( cut_facts_tac prems 1);
-by( rtac impE 1);
-by( atac 2);
-by( atac 2);
-by( etac thin_rl 1);
-by( rtac subcls_induct 1);
-by( atac 1);
-by( rtac impI 1);
-by( case_tac "C = Object" 1);
-by( Fast_tac 1);
-by Safe_tac;
-by( ftac class_wf 1);
-by( atac 1);
-by( ftac wf_cdecl_supD 1);
-by( atac 1);
-
-by( subgoal_tac "G\\<turnstile>C\\<prec>C1a" 1);
-by( etac subcls1I 2);
-by( rtac (hd (tl (tl (tl prems)))) 1);
-by (rewtac is_class_def);
-by Auto_tac;
-qed "subcls1_induct";
-
-Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (D,fs,ms) \\<longrightarrow> C \\<noteq> Object --> is_class G D|] ==> method (G,C) = \
-\ (case class G C of None => arbitrary | Some (D,fs,ms) => \
-\ (if C = Object then empty else method (G,D)) ++ \
-\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
-by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
-by( asm_simp_tac (simpset() addsplits[option.split]) 1);
-by Auto_tac;
-qed "method_rec_lemma";
-
-Goal "wf_prog wf_mb G ==> method (G,C) = \
-\ (case class G C of None => arbitrary | Some (D,fs,ms) => \
-\ (if C = Object then empty else method (G,D)) ++ \
-\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
-by(rtac method_rec_lemma 1);
-by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
- addsplits [option.split]) 1);
-by( case_tac "C = Object" 1);
-by( Force_tac 1);
-by Safe_tac;
-by( datac class_wf 1 1);
-by( datac wf_cdecl_supD 1 1);
-by( Asm_full_simp_tac 1);
-qed "method_rec";
-
-Goal "[|wf ((subcls1 G)^-1); class G C = Some (D,fs,ms); C \\<noteq> Object \\<longrightarrow> is_class G D|] ==> fields (G,C) = \
-\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))";
-by(rtac trans 1);
-by(rtac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
-by( asm_simp_tac (simpset() addsplits[option.split]) 1);
-qed "fields_rec_lemma";
-
-Goal "[|class G C = Some (D,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
-\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))";
-by(rtac trans 1);
-by(rtac fields_rec_lemma 1);
-by( asm_simp_tac (simpset() addsimps [wf_subcls1]) 1);
-ba 1;
-br refl 2;
-by( datac class_wf 1 1);
-by(rtac impI 1);
-by( eatac wf_cdecl_supD 1 1);
-qed "fields_rec";
-
-Goal "wf_prog wf_mb G ==> method (G,Object) = empty";
-by(stac method_rec 1);
-by Auto_tac;
-qed "method_Object";
-
-Goal "wf_prog wf_mb G ==> fields (G,Object) = []";
-by(stac fields_rec 1);
-by Auto_tac;
-qed "fields_Object";
-
-Addsimps [method_Object, fields_Object];
-
-Goalw [field_def] "wf_prog wf_mb G ==> field (G,Object) = empty";
-by(Asm_simp_tac 1);
-qed "field_Object";
-Addsimps [field_Object];
-
-Goal "[|is_class G C; wf_prog wf_mb G|] ==> G\\<turnstile>C\\<preceq>C Object";
-by(etac subcls1_induct 1);
-by( atac 1);
-by( Fast_tac 1);
-by(auto_tac (HOL_cs addSDs [wf_cdecl_supD], simpset()));
-by(eatac rtrancl_into_rtrancl2 1 1);
-qed "subcls_C_Object";
-
-Goalw [wf_mhead_def] "wf_mhead G sig rT ==> is_type G rT";
-by Auto_tac;
-qed "is_type_rTI";
-
-Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
-\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
-by( etac subcls1_induct 1);
-by( atac 1);
-by( Asm_simp_tac 1);
-by( safe_tac HOL_cs);
-by( stac fields_rec 1);
-by( atac 1);
-by( atac 1);
-by( simp_tac (simpset() delsplits [split_if]) 1);
-by( rtac ballI 1);
-by( split_all_tac 1);
-by( Simp_tac 1);
-by( etac UnE 1);
-by( Force_tac 1);
-by( etac (r_into_rtrancl RS rtrancl_trans) 1);
-by Auto_tac;
-qed "widen_fields_defpl'";
-
-Goal "[|((fn,fd),fT) \\<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==> \
-\ G\\<turnstile>C\\<preceq>C fd";
-by( datac widen_fields_defpl' 1 1);
-by (Fast_tac 1);
-qed "widen_fields_defpl";
-
-Goal "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))";
-by( etac subcls1_induct 1);
-by( atac 1);
-by( safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
-by( Asm_simp_tac 1);
-by( dtac subcls1_wfD 1);
-by( atac 1);
-by( stac fields_rec 1);
-by Auto_tac;
-by( rotate_tac ~1 1);
-by( forward_tac [class_wf] 1);
-by Auto_tac;
-by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);
-by( etac unique_append 1);
-by( rtac unique_map_inj 1);
-by( Clarsimp_tac 1);
-by (rtac injI 1);
-by( Asm_full_simp_tac 1);
-by(auto_tac (claset() addSDs [widen_fields_defpl], simpset()));
-qed "unique_fields";
-
-Goal "[|wf_prog wf_mb G; (C',C)\\<in>(subcls1 G)^*|] ==> \
-\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
-by(etac converse_rtrancl_induct 1);
-by( safe_tac (HOL_cs addSDs [subcls1D]));
-by(stac fields_rec 1);
-by( Auto_tac);
-qed_spec_mp "fields_mono_lemma";
-
-Goal
-"\\<lbrakk>map_of (fields (G,C)) fn = Some f; G\\<turnstile>D\\<preceq>C C; is_class G D; wf_prog wf_mb G\\<rbrakk>\
-\ \\<Longrightarrow> map_of (fields (G,D)) fn = Some f";
-by (rtac map_of_SomeI 1);
-by (eatac unique_fields 1 1);
-by (eatac fields_mono_lemma 1 1);
-by (etac map_of_SomeD 1);
-qed "fields_mono";
-
-Goal
-"[|field (G,C) fn = Some (fd, fT); G\\<turnstile>D\\<preceq>C C; wf_prog wf_mb G|]==> \
-\ map_of (fields (G,D)) (fn, fd) = Some fT";
-by (dtac field_fields 1);
-by (dtac (thm"rtranclD") 1);
-by Safe_tac;
-by (ftac subcls_is_class 1);
-by (dtac trancl_into_rtrancl 1);
-by (fast_tac (HOL_cs addDs [fields_mono]) 1);
-qed "widen_cfs_fields";
-
-Goal "wf_prog wf_mb G ==> is_class G C \\<Longrightarrow> \
-\ method (G,C) sig = Some (md,mh,m)\
-\ --> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
-by( etac subcls1_induct 1);
-by( atac 1);
-by( Force_tac 1);
-by( forw_inst_tac [("C","C")] method_rec 1);
-by( Clarify_tac 1);
-by( rotate_tac ~1 1);
-by( Asm_full_simp_tac 1);
-by( dtac override_SomeD 1);
-by( etac disjE 1);
-by( thin_tac "?P --> ?Q" 1);
-by( Clarify_tac 2);
-by( rtac rtrancl_trans 2);
-by( atac 3);
-by( rtac r_into_rtrancl 2);
-by( fast_tac (HOL_cs addIs [subcls1I]) 2);
-by (rotate_tac ~1 1);
-by (ftac map_of_SomeD 1);
-by( rewtac wf_cdecl_def);
-by (Clarsimp_tac 1);
-qed_spec_mp "method_wf_mdecl";
-
-Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
-\ \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->\
-\ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
-by( dtac (thm"rtranclD") 1);
-by( etac disjE 1);
-by( Fast_tac 1);
-by( etac conjE 1);
-by( etac trancl_trans_induct 1);
-by( Clarify_tac 2);
-by( EVERY[smp_tac 3 2]);
-by( fast_tac (HOL_cs addEs [widen_trans]) 2);
-by( Clarify_tac 1);
-by( dtac subcls1D 1);
-by( Clarify_tac 1);
-by( stac method_rec 1);
-by( atac 1);
-by( rewtac override_def);
-by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
-by( case_tac "\\<exists>z. map_of(map (\\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z" 1);
-by( etac exE 1);
-by( asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 2);
-by( ALLGOALS (rotate_tac ~1 THEN' forward_tac[ssubst] THEN' (fn n=>atac(n+1))));
-by( ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex])));
-by( dtac class_wf 1);
-by( atac 1);
-by( split_all_tac 1);
-by( rewtac wf_cdecl_def);
-by( dtac map_of_SomeD 1);
-by Auto_tac;
-qed_spec_mp "subcls_widen_methd";
-
-Goal
- "[| G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
-\ method (G,D) sig = Some (md, rT, b) |] \
-\ ==> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
-by(auto_tac (claset() addDs [subcls_widen_methd,method_wf_mdecl],
- simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
-qed "subtype_widen_methd";
-
-Goal "wf_prog wf_mb G ==> is_class G C \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
-by (etac subcls1_induct 1);
- ba 1;
- by (Asm_full_simp_tac 1);
-by (stac method_rec 1);
- ba 1;
-by (Clarify_tac 1);
-by (eres_inst_tac [("x","Da")] allE 1);
-by (Clarsimp_tac 1);
- by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
- by (Clarify_tac 1);
- by (stac method_rec 1);
- ba 1;
- by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
-qed_spec_mp "method_in_md";
-
-Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
-\ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
-by( etac subcls1_induct 1);
-by( atac 1);
-by( Asm_simp_tac 1);
-by( stac fields_rec 1);
-by( Fast_tac 1);
-by( atac 1);
-by( Clarsimp_tac 1);
-by( Safe_tac);
-by( Force_tac 2);
-by( dtac class_wf 1);
-by( atac 1);
-by( rewtac wf_cdecl_def);
-by( Clarsimp_tac 1);
-by( EVERY[dtac bspec 1, atac 1]);
-by( rewtac wf_fdecl_def);
-by Auto_tac;
-qed_spec_mp "fields_is_type_lemma";
-
-Goal "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==> \
-\ is_type G f";
-by(dtac map_of_SomeD 1);
-by(datac fields_is_type_lemma 2 1);
-by(Auto_tac);
-qed "fields_is_type";
-
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Feb 01 20:53:13 2001 +0100
@@ -14,31 +14,410 @@
* for uniformity, Object is assumed to be declared like any other class
*)
-WellForm = TypeRel +
+theory WellForm = TypeRel:
-types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
+types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
constdefs
wf_fdecl :: "'c prog => fdecl => bool"
-"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
+"wf_fdecl G == \<lambda>(fn,ft). is_type G ft"
wf_mhead :: "'c prog => sig => ty => bool"
-"wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
+"wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT"
wf_mdecl :: "'c wf_mb => 'c wf_mb"
-"wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
+"wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)"
wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
"wf_cdecl wf_mb G ==
- \\<lambda>(C,(D,fs,ms)).
- (\\<forall>f\\<in>set fs. wf_fdecl G f) \\<and> unique fs \\<and>
- (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and>
- (C \\<noteq> Object \\<longrightarrow> is_class G D \\<and> \\<not>G\\<turnstile>D\\<preceq>C C \\<and>
- (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
- method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
+ \<lambda>(C,(D,fs,ms)).
+ (\<forall>f\<in>set fs. wf_fdecl G f) \<and> unique fs \<and>
+ (\<forall>m\<in>set ms. wf_mdecl wf_mb G C m) \<and> unique ms \<and>
+ (C \<noteq> Object \<longrightarrow> is_class G D \<and> \<not>G\<turnstile>D\<preceq>C C \<and>
+ (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
+ method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
wf_prog :: "'c wf_mb => 'c prog => bool"
"wf_prog wf_mb G ==
- let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
+ let cs = set G in ObjectC \<in> cs \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
+
+lemma class_wf:
+ "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)"
+apply (unfold wf_prog_def class_def)
+apply (simp)
+apply (fast dest: map_of_SomeD)
+done
+
+lemma class_Object [simp]:
+ "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
+apply (unfold wf_prog_def ObjectC_def class_def)
+apply (auto intro: map_of_SomeI)
+done
+
+lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object"
+apply (unfold is_class_def)
+apply (simp (no_asm_simp))
+done
+
+lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
+apply( frule r_into_trancl)
+apply( drule subcls1D)
+apply(clarify)
+apply( drule (1) class_wf)
+apply( unfold wf_cdecl_def)
+apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
+done
+
+lemma wf_cdecl_supD:
+"!!r. \<lbrakk>wf_cdecl wf_mb G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
+apply (unfold wf_cdecl_def)
+apply (auto split add: option.split_asm)
+done
+
+lemma subcls_asym: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
+apply(erule tranclE)
+apply(fast dest!: subcls1_wfD )
+apply(fast dest!: subcls1_wfD intro: trancl_trans)
+done
+
+lemma subcls_irrefl: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
+apply (erule trancl_trans_induct)
+apply (auto dest: subcls1_wfD subcls_asym)
+done
+
+lemma acyclic_subcls1: "wf_prog wf_mb G ==> acyclic (subcls1 G)"
+apply (unfold acyclic_def)
+apply (fast dest: subcls_irrefl)
+done
+
+lemma wf_subcls1: "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)"
+apply (rule finite_acyclic_wf)
+apply ( subst finite_converse)
+apply ( rule finite_subcls1)
+apply (subst acyclic_converse)
+apply (erule acyclic_subcls1)
+done
+
+lemma subcls_induct:
+"[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
+proof -
+ assume p: "PROP ?P"
+ assume ?A thus ?thesis apply -
+apply(drule wf_subcls1)
+apply(drule wf_trancl)
+apply(simp only: trancl_converse)
+apply(erule_tac a = C in wf_induct)
+apply(rule p)
+apply(auto)
+done
+qed
+
+lemma subcls1_induct:
+"[|is_class G C; wf_prog wf_mb G; P Object;
+ !!C D fs ms. [|C \<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \<and>
+ wf_cdecl wf_mb G (C,D,fs,ms) \<and> G\<turnstile>C\<prec>C1D \<and> is_class G D \<and> P D|] ==> P C
+ |] ==> P C"
+(is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _")
+proof -
+ assume p: "PROP ?P"
+ assume ?A ?B ?C thus ?thesis apply -
+apply(unfold is_class_def)
+apply( rule impE)
+prefer 2
+apply( assumption)
+prefer 2
+apply( assumption)
+apply( erule thin_rl)
+apply( rule subcls_induct)
+apply( assumption)
+apply( rule impI)
+apply( case_tac "C = Object")
+apply( fast)
+apply safe
+apply( frule (1) class_wf)
+apply( frule (1) wf_cdecl_supD)
+
+apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
+apply( erule_tac [2] subcls1I)
+apply( rule p)
+apply (unfold is_class_def)
+apply auto
+done
+qed
+
+lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma];
+
+lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
+
+lemma method_Object [simp]: "wf_prog wf_mb G ==> method (G,Object) = empty"
+apply(subst method_rec)
+apply auto
+done
+
+lemma fields_Object [simp]: "wf_prog wf_mb G ==> fields (G,Object) = []"
+apply(subst fields_rec)
+apply auto
+done
+
+lemma field_Object [simp]: "wf_prog wf_mb G ==> field (G,Object) = empty"
+apply (unfold field_def)
+apply(simp (no_asm_simp))
+done
+
+lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
+apply(erule subcls1_induct)
+apply( assumption)
+apply( fast)
+apply(auto dest!: wf_cdecl_supD)
+apply(erule (1) rtrancl_into_rtrancl2)
+done
+
+lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
+apply (unfold wf_mhead_def)
+apply auto
+done
+
+lemma widen_fields_defpl': "[|is_class G C; wf_prog wf_mb G|] ==>
+ \<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
+apply( erule subcls1_induct)
+apply( assumption)
+apply( simp (no_asm_simp))
+apply( tactic "safe_tac HOL_cs")
+apply( subst fields_rec)
+apply( assumption)
+apply( assumption)
+apply( simp (no_asm) split del: split_if)
+apply( rule ballI)
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply( simp (no_asm))
+apply( erule UnE)
+apply( force)
+apply( erule r_into_rtrancl [THEN rtrancl_trans])
+apply auto
+done
+
+lemma widen_fields_defpl: "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>
+ G\<turnstile>C\<preceq>C fd"
+apply( drule (1) widen_fields_defpl')
+apply (fast)
+done
+
+lemma unique_fields: "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
+apply( erule subcls1_induct)
+apply( assumption)
+apply( safe dest!: wf_cdecl_supD)
+apply( simp (no_asm_simp))
+apply( drule subcls1_wfD)
+apply( assumption)
+apply( subst fields_rec)
+apply auto
+apply( rotate_tac -1)
+apply( frule class_wf)
+apply auto
+apply( simp add: wf_cdecl_def)
+apply( erule unique_append)
+apply( rule unique_map_inj)
+apply( clarsimp)
+apply (rule injI)
+apply( simp)
+apply(auto dest!: widen_fields_defpl)
+done
+
+lemma fields_mono_lemma [rule_format (no_asm)]: "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>
+ x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
+apply(erule converse_rtrancl_induct)
+apply( safe dest!: subcls1D)
+apply(subst fields_rec)
+apply( auto)
+done
+
+lemma fields_mono:
+"\<lbrakk>map_of (fields (G,C)) fn = Some f; G\<turnstile>D\<preceq>C C; is_class G D; wf_prog wf_mb G\<rbrakk>
+ \<Longrightarrow> map_of (fields (G,D)) fn = Some f"
+apply (rule map_of_SomeI)
+apply (erule (1) unique_fields)
+apply (erule (1) fields_mono_lemma)
+apply (erule map_of_SomeD)
+done
+
+lemma widen_cfs_fields:
+"[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; wf_prog wf_mb G|]==>
+ map_of (fields (G,D)) (fn, fd) = Some fT"
+apply (drule field_fields)
+apply (drule rtranclD)
+apply safe
+apply (frule subcls_is_class)
+apply (drule trancl_into_rtrancl)
+apply (fast dest: fields_mono)
+done
+
+lemma method_wf_mdecl [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>
+ method (G,C) sig = Some (md,mh,m)
+ --> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
+apply( erule subcls1_induct)
+apply( assumption)
+apply( force)
+apply( clarify)
+apply( frule_tac C = C in method_rec)
+apply( assumption)
+apply( rotate_tac -1)
+apply( simp)
+apply( drule override_SomeD)
+apply( erule disjE)
+apply( erule_tac V = "?P --> ?Q" in thin_rl)
+apply (frule map_of_SomeD)
+apply (clarsimp simp add: wf_cdecl_def)
+apply( clarify)
+apply( rule rtrancl_trans)
+prefer 2
+apply( assumption)
+apply( rule r_into_rtrancl)
+apply( fast intro: subcls1I)
+done
+
+lemma subcls_widen_methd [rule_format (no_asm)]:
+ "[|G\<turnstile>T\<preceq>C T'; wf_prog wf_mb G|] ==>
+ \<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->
+ (\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \<and> G\<turnstile>rT'\<preceq>rT)"
+apply( drule rtranclD)
+apply( erule disjE)
+apply( fast)
+apply( erule conjE)
+apply( erule trancl_trans_induct)
+prefer 2
+apply( clarify)
+apply( drule spec, drule spec, drule spec, erule (1) impE)
+apply( fast elim: widen_trans)
+apply( clarify)
+apply( drule subcls1D)
+apply( clarify)
+apply( subst method_rec)
+apply( assumption)
+apply( unfold override_def)
+apply( simp (no_asm_simp) del: split_paired_Ex)
+apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
+apply( erule exE)
+apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
+prefer 2
+apply( rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
+apply( tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1")
+apply( simp_all (no_asm_simp) del: split_paired_Ex)
+apply( drule (1) class_wf)
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply( unfold wf_cdecl_def)
+apply( drule map_of_SomeD)
+apply auto
+done
+
+lemma subtype_widen_methd:
+ "[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;
+ method (G,D) sig = Some (md, rT, b) |]
+ ==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
+apply(auto dest: subcls_widen_methd method_wf_mdecl simp add: wf_mdecl_def wf_mhead_def split_def)
+done
+
+lemma method_in_md [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
+apply (erule (1) subcls1_induct)
+ apply (simp)
+apply (erule conjE)
+apply (subst method_rec)
+ apply (assumption)
+ apply (assumption)
+apply (clarify)
+apply (erule_tac "x" = "Da" in allE)
+apply (clarsimp)
+ apply (simp add: map_of_map)
+ apply (clarify)
+ apply (subst method_rec)
+ apply (assumption)
+ apply (assumption)
+ apply (simp add: override_def map_of_map split add: option.split)
+done
+
+lemma widen_methd:
+"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\<turnstile>T''\<preceq>C C|]
+ ==> \<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
+apply( drule subcls_widen_methd)
+apply auto
+done
+
+lemma Call_lemma:
+"[|method (G,C) sig = Some (md,rT,b); G\<turnstile>T''\<preceq>C C; wf_prog wf_mb G;
+ class G C = Some y|] ==> \<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \<and>
+ G\<turnstile>rT'\<preceq>rT \<and> G\<turnstile>T''\<preceq>C T' \<and> wf_mhead G sig rT' \<and> wf_mb G T' (sig,rT',b)"
+apply( drule (2) widen_methd)
+apply( clarify)
+apply( frule subcls_is_class2)
+apply (unfold is_class_def)
+apply (simp (no_asm_simp))
+apply( drule method_wf_mdecl)
+apply( unfold wf_mdecl_def)
+apply( unfold is_class_def)
+apply auto
+done
+
+
+lemma fields_is_type_lemma [rule_format (no_asm)]: "[|is_class G C; wf_prog wf_mb G|] ==>
+ \<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
+apply( erule (1) subcls1_induct)
+apply( simp (no_asm_simp))
+apply( subst fields_rec)
+apply( fast)
+apply( assumption)
+apply( clarsimp)
+apply( safe)
+prefer 2
+apply( force)
+apply( drule (1) class_wf)
+apply( unfold wf_cdecl_def)
+apply( clarsimp)
+apply( drule (1) bspec)
+apply( unfold wf_fdecl_def)
+apply auto
+done
+
+lemma fields_is_type: "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>
+ is_type G f"
+apply(drule map_of_SomeD)
+apply(drule (2) fields_is_type_lemma)
+apply(auto)
+done
+
+lemma methd:
+ "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
+ ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
+proof -
+ assume wf: "wf_prog wf_mb G"
+ assume C: "(C,S,fs,mdecls) \<in> set G"
+
+ assume m: "(sig,rT,code) \<in> set mdecls"
+ moreover
+ from wf
+ have "class G Object = Some (arbitrary, [], [])"
+ by simp
+ moreover
+ from wf C
+ have c: "class G C = Some (S,fs,mdecls)"
+ by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
+ ultimately
+ have O: "C \<noteq> Object"
+ by auto
+
+ from wf C
+ have "unique mdecls"
+ by (unfold wf_prog_def wf_cdecl_def) auto
+
+ hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)"
+ by - (induct mdecls, auto)
+
+ with m
+ have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
+ by (force intro: map_of_SomeI)
+
+ with wf C m c O
+ show ?thesis
+ by (auto simp add: is_class_def dest: method_rec)
+qed
end
--- a/src/HOL/MicroJava/J/WellType.ML Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(* Title: HOL/MicroJava/J/WellType.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-Goal
-"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C|]\
-\ ==> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
-by( dtac subcls_widen_methd 1);
-by Auto_tac;
-qed "widen_methd";
-
-
-Goal
-"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G; \
-\ class G C = Some y|] ==> \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
-\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
-by( datac widen_methd 2 1);
-by( Clarify_tac 1);
-by( ftac subcls_is_class2 1);
-by (rewtac is_class_def);
-by (Asm_simp_tac 1);
-by( dtac method_wf_mdecl 1);
-by( rewtac wf_mdecl_def);
-by( rewtac is_class_def);
-by Auto_tac;
-qed "Call_lemma";
-
-Goal "wf_prog wf_mb G ==> method (G,Object) sig = None";
-by (Asm_simp_tac 1);
-qed "method_Object";
-Addsimps [method_Object];
-
-Goalw [max_spec_def]
- "x \\<in> max_spec G C sig ==> x \\<in> appl_methds G C sig";
-by (Fast_tac 1);
-qed"max_spec2appl_meths";
-
-Goalw [appl_methds_def]
-"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) ==> \
-\ \\<exists>D b. md = Class D \\<and> method (G,C) (mn, pTs') = Some (D,rT,b) \
-\ \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'";
-by (Fast_tac 1);
-qed "appl_methsD";
-
-bind_thm ("max_spec2mheads", insertI1 RSN (2,(equalityD2 RS subsetD)) RS
- max_spec2appl_meths RS appl_methsD);
-
-Goal "(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)";
-by (rtac val_.induct 1);
-by (Fast_tac 5);
-by Auto_tac;
-qed_spec_mp "is_type_typeof";
-Addsimps [is_type_typeof];
-
-Goal "typeof (\\<lambda>a. None) v = Some T \\<longrightarrow> is_type G T";
-by (rtac val_.induct 1);
-by Auto_tac;
-qed_spec_mp "typeof_empty_is_type";
-
-Goal "wf_prog wf_mb G \\<Longrightarrow> ((G,L)\\<turnstile>e::T \\<longrightarrow> is_type G T) \\<and> \
-\ ((G,L)\\<turnstile>es[::]Ts \\<longrightarrow> Ball (set Ts) (is_type G)) \\<and> ((G,L)\\<turnstile>c \\<surd> \\<longrightarrow> True)";
-by (rtac ty_expr_ty_exprs_wt_stmt.induct 1);
-by Auto_tac;
-by ( etac typeof_empty_is_type 1);
-by ( asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
-by ( dtac field_fields 1);
-by ( datac fields_is_type 1 1);
-by ( Asm_simp_tac 1);
-ba 1;
-by (auto_tac (claset() addSDs [max_spec2mheads,method_wf_mdecl,is_type_rTI], simpset()addsimps[wf_mdecl_def]));
-qed "wt_is_type";
-
-bind_thm ("ty_expr_is_type", permute_prems 0 1 (wt_is_type RS conjunct1 RS mp));
--- a/src/HOL/MicroJava/J/WellType.thy Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Thu Feb 01 20:53:13 2001 +0100
@@ -15,41 +15,59 @@
*)
-WellType = Term + WellForm +
+theory WellType = Term + WellForm:
types lenv (* local variables, including method parameters and This *)
- = "vname \\<leadsto> ty"
+ = "vname \<leadsto> ty"
'c env
- = "'c prog \\<times> lenv"
+ = "'c prog \<times> lenv"
syntax
prg :: "'c env => 'c prog"
- localT :: "'c env => (vname \\<leadsto> ty)"
+ localT :: "'c env => (vname \<leadsto> ty)"
translations
"prg" => "fst"
"localT" => "snd"
consts
- more_spec :: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
- (ty \\<times> 'x) \\<times> ty list => bool"
- appl_methds :: "'c prog => cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
- max_spec :: "'c prog => cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
+ more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
+ (ty \<times> 'x) \<times> ty list => bool"
+ appl_methds :: "'c prog => cname => sig => ((ty \<times> ty) \<times> ty list) set"
+ max_spec :: "'c prog => cname => sig => ((ty \<times> ty) \<times> ty list) set"
defs
- more_spec_def "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
- list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
+ more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
+ list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
(* applicable methods, cf. 15.11.2.1 *)
- appl_methds_def "appl_methds G C == \\<lambda>(mn, pTs).
+ appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
{((Class md,rT),pTs') |md rT mb pTs'.
- method (G,C) (mn, pTs') = Some (md,rT,mb) \\<and>
- list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
+ method (G,C) (mn, pTs') = Some (md,rT,mb) \<and>
+ list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
(* maximally specific methods, cf. 15.11.2.2 *)
- max_spec_def "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and>
- (\\<forall>m'\\<in>appl_methds G C sig.
- more_spec G m' m --> m' = m)}"
+ max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and>
+ (\<forall>m'\<in>appl_methds G C sig.
+ more_spec G m' m --> m' = m)}"
+
+lemma max_spec2appl_meths:
+ "x \<in> max_spec G C sig ==> x \<in> appl_methds G C sig"
+apply (unfold max_spec_def)
+apply (fast)
+done
+
+lemma appl_methsD:
+"((md,rT),pTs')\<in>appl_methds G C (mn, pTs) ==>
+ \<exists>D b. md = Class D \<and> method (G,C) (mn, pTs') = Some (D,rT,b)
+ \<and> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
+apply (unfold appl_methds_def)
+apply (fast)
+done
+
+lemmas max_spec2mheads = insertI1 [THEN [2] equalityD2 [THEN subsetD],
+ THEN max_spec2appl_meths, THEN appl_methsD]
+
consts
typeof :: "(loc => ty option) => val => ty option"
@@ -61,19 +79,30 @@
"typeof dt (Intg i) = Some (PrimT Integer)"
"typeof dt (Addr a) = dt a"
+lemma is_type_typeof [rule_format (no_asm), simp]: "(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"
+apply (rule val.induct)
+apply auto
+done
+
+lemma typeof_empty_is_type [rule_format (no_asm)]:
+ "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
+apply (rule val.induct)
+apply auto
+done
+
types
- java_mb = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
+ java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
(* method body with parameter names, local variables, block, result expression *)
consts
- ty_expr :: "java_mb env => (expr \\<times> ty ) set"
- ty_exprs:: "java_mb env => (expr list \\<times> ty list) set"
+ ty_expr :: "java_mb env => (expr \<times> ty ) set"
+ ty_exprs:: "java_mb env => (expr list \<times> ty list) set"
wt_stmt :: "java_mb env => stmt set"
syntax
- ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ \\<turnstile> _ :: _" [51,51,51]50)
- ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \\<turnstile> _ [::] _" [51,51,51]50)
- wt_stmt :: "java_mb env => stmt => bool" ("_ \\<turnstile> _ \\<surd>" [51,51 ]50)
+ ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ \<turnstile> _ :: _" [51,51,51]50)
+ ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
+ wt_stmt :: "java_mb env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51,51 ]50)
syntax (HTML)
ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ |- _ :: _" [51,51,51]50)
@@ -82,107 +111,123 @@
translations
- "E\\<turnstile>e :: T" == "(e,T) \\<in> ty_expr E"
- "E\\<turnstile>e[::]T" == "(e,T) \\<in> ty_exprs E"
- "E\\<turnstile>c \\<surd>" == "c \\<in> wt_stmt E"
+ "E\<turnstile>e :: T" == "(e,T) \<in> ty_expr E"
+ "E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
+ "E\<turnstile>c \<surd>" == "c \<in> wt_stmt E"
-inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intrs
+inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intros
(* well-typed expressions *)
(* cf. 15.8 *)
- NewC "[| is_class (prg E) C |] ==>
- E\\<turnstile>NewC C::Class C"
+ NewC: "[| is_class (prg E) C |] ==>
+ E\<turnstile>NewC C::Class C"
(* cf. 15.15 *)
- Cast "[| E\\<turnstile>e::Class C; is_class (prg E) D;
- prg E\\<turnstile>C\\<preceq>? D |] ==>
- E\\<turnstile>Cast D e::Class D"
+ Cast: "[| E\<turnstile>e::Class C; is_class (prg E) D;
+ prg E\<turnstile>C\<preceq>? D |] ==>
+ E\<turnstile>Cast D e::Class D"
(* cf. 15.7.1 *)
- Lit "[| typeof (\\<lambda>v. None) x = Some T |] ==>
- E\\<turnstile>Lit x::T"
+ Lit: "[| typeof (\<lambda>v. None) x = Some T |] ==>
+ E\<turnstile>Lit x::T"
(* cf. 15.13.1 *)
- LAcc "[| localT E v = Some T; is_type (prg E) T |] ==>
- E\\<turnstile>LAcc v::T"
+ LAcc: "[| localT E v = Some T; is_type (prg E) T |] ==>
+ E\<turnstile>LAcc v::T"
- BinOp "[| E\\<turnstile>e1::T;
- E\\<turnstile>e2::T;
+ BinOp:"[| E\<turnstile>e1::T;
+ E\<turnstile>e2::T;
if bop = Eq then T' = PrimT Boolean
- else T' = T \\<and> T = PrimT Integer|] ==>
- E\\<turnstile>BinOp bop e1 e2::T'"
+ else T' = T \<and> T = PrimT Integer|] ==>
+ E\<turnstile>BinOp bop e1 e2::T'"
(* cf. 15.25, 15.25.1 *)
- LAss "[| E\\<turnstile>LAcc v::T;
- E\\<turnstile>e::T';
- prg E\\<turnstile>T'\\<preceq>T |] ==>
- E\\<turnstile>v::=e::T'"
+ LAss: "[| E\<turnstile>LAcc v::T;
+ E\<turnstile>e::T';
+ prg E\<turnstile>T'\<preceq>T |] ==>
+ E\<turnstile>v::=e::T'"
(* cf. 15.10.1 *)
- FAcc "[| E\\<turnstile>a::Class C;
+ FAcc: "[| E\<turnstile>a::Class C;
field (prg E,C) fn = Some (fd,fT) |] ==>
- E\\<turnstile>{fd}a..fn::fT"
+ E\<turnstile>{fd}a..fn::fT"
(* cf. 15.25, 15.25.1 *)
- FAss "[| E\\<turnstile>{fd}a..fn::T;
- E\\<turnstile>v ::T';
- prg E\\<turnstile>T'\\<preceq>T |] ==>
- E\\<turnstile>{fd}a..fn:=v::T'"
+ FAss: "[| E\<turnstile>{fd}a..fn::T;
+ E\<turnstile>v ::T';
+ prg E\<turnstile>T'\<preceq>T |] ==>
+ E\<turnstile>{fd}a..fn:=v::T'"
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
- Call "[| E\\<turnstile>a::Class C;
- E\\<turnstile>ps[::]pTs;
+ Call: "[| E\<turnstile>a::Class C;
+ E\<turnstile>ps[::]pTs;
max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
- E\\<turnstile>{C}a..mn({pTs'}ps)::rT"
+ E\<turnstile>{C}a..mn({pTs'}ps)::rT"
(* well-typed expression lists *)
(* cf. 15.11.??? *)
- Nil "E\\<turnstile>[][::][]"
+ Nil: "E\<turnstile>[][::][]"
(* cf. 15.11.??? *)
- Cons "[| E\\<turnstile>e::T;
- E\\<turnstile>es[::]Ts |] ==>
- E\\<turnstile>e#es[::]T#Ts"
+ Cons:"[| E\<turnstile>e::T;
+ E\<turnstile>es[::]Ts |] ==>
+ E\<turnstile>e#es[::]T#Ts"
(* well-typed statements *)
- Skip "E\\<turnstile>Skip\\<surd>"
+ Skip:"E\<turnstile>Skip\<surd>"
- Expr "[| E\\<turnstile>e::T |] ==>
- E\\<turnstile>Expr e\\<surd>"
+ Expr:"[| E\<turnstile>e::T |] ==>
+ E\<turnstile>Expr e\<surd>"
- Comp "[| E\\<turnstile>s1\\<surd>;
- E\\<turnstile>s2\\<surd> |] ==>
- E\\<turnstile>s1;; s2\\<surd>"
+ Comp:"[| E\<turnstile>s1\<surd>;
+ E\<turnstile>s2\<surd> |] ==>
+ E\<turnstile>s1;; s2\<surd>"
(* cf. 14.8 *)
- Cond "[| E\\<turnstile>e::PrimT Boolean;
- E\\<turnstile>s1\\<surd>;
- E\\<turnstile>s2\\<surd> |] ==>
- E\\<turnstile>If(e) s1 Else s2\\<surd>"
+ Cond:"[| E\<turnstile>e::PrimT Boolean;
+ E\<turnstile>s1\<surd>;
+ E\<turnstile>s2\<surd> |] ==>
+ E\<turnstile>If(e) s1 Else s2\<surd>"
(* cf. 14.10 *)
- Loop "[| E\\<turnstile>e::PrimT Boolean;
- E\\<turnstile>s\\<surd> |] ==>
- E\\<turnstile>While(e) s\\<surd>"
+ Loop:"[| E\<turnstile>e::PrimT Boolean;
+ E\<turnstile>s\<surd> |] ==>
+ E\<turnstile>While(e) s\<surd>"
constdefs
- wf_java_mdecl :: java_mb prog => cname => java_mb mdecl => bool
-"wf_java_mdecl G C == \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
- length pTs = length pns \\<and>
- nodups pns \\<and>
- unique lvars \\<and>
- (\\<forall>pn\\<in>set pns. map_of lvars pn = None) \\<and>
- (\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
- (let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
- E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res::T \\<and> G\\<turnstile>T\\<preceq>rT))"
+ wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
+"wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
+ length pTs = length pns \<and>
+ nodups pns \<and>
+ unique lvars \<and>
+ (\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
+ (\<forall>(vn,T)\<in>set lvars. is_type G T) &
+ (let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
+ E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
- wf_java_prog :: java_mb prog => bool
+ wf_java_prog :: "java_mb prog => bool"
"wf_java_prog G == wf_prog wf_java_mdecl G"
+
+lemma wt_is_type: "wf_prog wf_mb G \<Longrightarrow> ((G,L)\<turnstile>e::T \<longrightarrow> is_type G T) \<and>
+ ((G,L)\<turnstile>es[::]Ts \<longrightarrow> Ball (set Ts) (is_type G)) \<and> ((G,L)\<turnstile>c \<surd> \<longrightarrow> True)"
+apply (rule ty_expr_ty_exprs_wt_stmt.induct)
+apply auto
+apply ( erule typeof_empty_is_type)
+apply ( simp split add: split_if_asm)
+apply ( drule field_fields)
+apply ( drule (1) fields_is_type)
+apply ( simp (no_asm_simp))
+apply (assumption)
+apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI simp add: wf_mdecl_def)
+done
+
+lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, COMP swap_prems_rl]
+
end
--- a/src/HOL/MicroJava/ROOT.ML Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/ROOT.ML Thu Feb 01 20:53:13 2001 +0100
@@ -1,9 +1,6 @@
goals_limit := 1;
-Unify.search_bound := 40;
-Unify.trace_bound := 40;
-
add_path "J";
add_path "JVM";
add_path "BV";