src/HOL/MicroJava/J/WellForm.ML
changeset 10042 7164dc0d24d8
parent 9758 88366d7332ff
child 10138 412a3ced6efd
     1.1 --- a/src/HOL/MicroJava/J/WellForm.ML	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/WellForm.ML	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -5,22 +5,22 @@
     1.4  *)
     1.5  
     1.6  val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
     1.7 - "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wf_cdecl wf_mb G (C,c)" (K [
     1.8 + "!!X. [|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)" (K [
     1.9  	Asm_full_simp_tac 1,
    1.10  	fast_tac (set_cs addDs [get_in_set]) 1]);
    1.11  
    1.12  val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
    1.13 -	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
    1.14 +	"!!X. wf_prog wf_mb G ==> class G Object = Some (None, [], [])" (K [
    1.15  	safe_tac set_cs,
    1.16  	dtac in_set_get 1,
    1.17  	 Auto_tac]);
    1.18  Addsimps [class_Object];
    1.19  
    1.20  val is_class_Object = prove_goalw thy [is_class_def] 
    1.21 -	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
    1.22 +	"!!X. wf_prog wf_mb G ==> is_class G Object" (K [Asm_simp_tac 1]);
    1.23  Addsimps [is_class_Object];
    1.24  
    1.25 -Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
    1.26 +Goal "[|G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G|] ==> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
    1.27  by( forward_tac [r_into_trancl] 1);
    1.28  by( dtac subcls1D 1);
    1.29  by( strip_tac1 1);
    1.30 @@ -31,26 +31,26 @@
    1.31  qed "subcls1_wfD";
    1.32  
    1.33  val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] 
    1.34 -"\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
    1.35 +"!!X. [|wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object|] ==> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
    1.36  	pair_tac "r" 1,
    1.37  	asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
    1.38  
    1.39 -Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+";
    1.40 +Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> \\<not>(D,C)\\<in>(subcls1 G)^+";
    1.41  by(etac tranclE 1);
    1.42  by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
    1.43  qed "subcls_asym";
    1.44  
    1.45 -val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
    1.46 +val subcls_irrefl = prove_goal thy "!!X. [|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D" (K [
    1.47  	etac trancl_trans_induct 1,
    1.48  	 fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
    1.49  	fast_tac (HOL_cs addDs [subcls_asym]) 1]);
    1.50  
    1.51  val acyclic_subcls1 = prove_goalw thy [acyclic_def] 
    1.52 -	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> acyclic (subcls1 G)" (K [
    1.53 +	"!!X. wf_prog wf_mb G ==> acyclic (subcls1 G)" (K [
    1.54  	strip_tac1 1,
    1.55  	fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
    1.56  
    1.57 -val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
    1.58 +val wf_subcls1 = prove_goal thy "!!X. wf_prog wf_mb G ==> wf ((subcls1 G)^-1)" (K [
    1.59  	rtac finite_acyclic_wf 1,
    1.60  	 stac finite_converse 1,
    1.61  	 rtac finite_subcls1 1,
    1.62 @@ -58,7 +58,7 @@
    1.63  	etac acyclic_subcls1 1]);
    1.64  
    1.65  val major::prems = goal thy
    1.66 -  "\\<lbrakk>wf_prog wf_mb G; \\<And>C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
    1.67 +  "[|wf_prog wf_mb G; !!C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C";
    1.68  by(cut_facts_tac [major RS wf_subcls1] 1);
    1.69  by(dtac wf_trancl 1);
    1.70  by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
    1.71 @@ -67,10 +67,10 @@
    1.72  by(Auto_tac);
    1.73  qed "subcls_induct";
    1.74  
    1.75 -val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wf_mb G; P Object; \
    1.76 -\\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
    1.77 -\   wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
    1.78 -\ \\<rbrakk> \\<Longrightarrow> P C";
    1.79 +val prems = goal thy "[|is_class G C; wf_prog wf_mb G; P Object; \
    1.80 +\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
    1.81 +\   wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
    1.82 +\ |] ==> P C";
    1.83  by( cut_facts_tac prems 1);
    1.84  by( rtac impE 1);
    1.85  by(   atac 2);
    1.86 @@ -95,18 +95,18 @@
    1.87  by( etac subcls1I 1);
    1.88  qed "subcls1_induct";
    1.89  
    1.90 -Goal "\\<lbrakk>wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) \\<longrightarrow> is_class G D\\<rbrakk> \\<Longrightarrow> method (G,C) = \
    1.91 -\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
    1.92 -\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
    1.93 +Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) --> is_class G D|] ==> method (G,C) = \
    1.94 +\ (case class G C of None => empty | Some (sc,fs,ms) => \
    1.95 +\ (case sc of None => empty | Some D => method (G,D)) \\<oplus> \
    1.96  \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
    1.97  by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
    1.98  by( asm_simp_tac (simpset() addsplits[option.split]) 1);
    1.99  auto();
   1.100  qed "method_rec_lemma";
   1.101  
   1.102 -Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
   1.103 -\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
   1.104 -\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
   1.105 +Goal "wf_prog wf_mb G ==> method (G,C) = \
   1.106 +\ (case class G C of None => empty | Some (sc,fs,ms) => \
   1.107 +\ (case sc of None => empty | Some D => method (G,D)) \\<oplus> \
   1.108  \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
   1.109  by(rtac method_rec_lemma 1);
   1.110  by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def] 
   1.111 @@ -119,16 +119,16 @@
   1.112  by( Asm_full_simp_tac 1);
   1.113  qed "method_rec";
   1.114  
   1.115 -Goal "\\<lbrakk>wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C \\<longrightarrow> is_class G C\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
   1.116 +Goal "[|wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C --> is_class G C|] ==> fields (G,C) = \
   1.117  \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
   1.118 -\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
   1.119 +\ (case sc of None => [] | Some D => fields (G,D))";
   1.120  by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
   1.121  by( asm_simp_tac (simpset() addsplits[option.split]) 1);
   1.122  qed "fields_rec_lemma";
   1.123  
   1.124 -Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
   1.125 +Goal "[|class G C = Some (sc,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
   1.126  \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
   1.127 -\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
   1.128 +\ (case sc of None => [] | Some D => fields (G,D))";
   1.129  by(rtac fields_rec_lemma 1);
   1.130  by(   asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
   1.131  ba  1;
   1.132 @@ -142,16 +142,16 @@
   1.133  by( Asm_full_simp_tac 1);
   1.134  qed "fields_rec";
   1.135  
   1.136 -val method_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> method (G,Object) = empty"
   1.137 +val method_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> method (G,Object) = empty"
   1.138  	(K [stac method_rec 1,Auto_tac]);
   1.139 -val fields_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> fields (G,Object) = []"(K [
   1.140 +val fields_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> fields (G,Object) = []"(K [
   1.141  	stac fields_rec 1,Auto_tac]);
   1.142  Addsimps [method_Object, fields_Object];
   1.143  val field_Object = prove_goalw thy [field_def]
   1.144 - "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
   1.145 + "!!X. wf_prog wf_mb G ==> field (G,Object) = empty" (K [Asm_simp_tac 1]);
   1.146  Addsimps [field_Object];
   1.147  
   1.148 -Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<preceq>C Object";
   1.149 +Goal "[|is_class G C; wf_prog wf_mb G|] ==> G\\<turnstile>C\\<preceq>C Object";
   1.150  by(etac subcls1_induct 1);
   1.151  by(  atac 1);
   1.152  by( Fast_tac 1);
   1.153 @@ -160,18 +160,18 @@
   1.154  qed "subcls_C_Object";
   1.155  
   1.156  val is_type_rTI = prove_goalw thy [wf_mhead_def]
   1.157 -	"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
   1.158 +	"!!sig. wf_mhead G sig rT ==> is_type G rT"
   1.159  	(K [split_all_tac 1, Auto_tac]);
   1.160  
   1.161 -Goal "\\<lbrakk>(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   1.162 -\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))";
   1.163 +Goal "[|(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G|] ==> \
   1.164 +\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
   1.165  by(etac trancl_trans_induct 1);
   1.166  by( safe_tac (HOL_cs addSDs [subcls1D]));
   1.167  by(stac fields_rec 1);
   1.168  by(  Auto_tac);
   1.169  qed_spec_mp "fields_mono";
   1.170  
   1.171 -Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   1.172 +Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
   1.173  \ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
   1.174  by( etac subcls1_induct 1);
   1.175  by(   atac 1);
   1.176 @@ -193,7 +193,7 @@
   1.177  by( Asm_full_simp_tac 1);
   1.178  qed "widen_fields_defpl'";
   1.179  
   1.180 -Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
   1.181 +Goal "[|is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))|] ==> \
   1.182  \ G\\<turnstile>C\\<preceq>C fd";
   1.183  by( datac widen_fields_defpl' 1 1);
   1.184  (*###################*)
   1.185 @@ -202,7 +202,7 @@
   1.186  qed "widen_fields_defpl";
   1.187  
   1.188  
   1.189 -Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
   1.190 +Goal "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))";
   1.191  by( etac subcls1_induct 1);
   1.192  by(   atac 1);
   1.193  by(  safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
   1.194 @@ -226,7 +226,7 @@
   1.195  qed "unique_fields";
   1.196  
   1.197  Goal
   1.198 -"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
   1.199 +"[|wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft|] ==> \
   1.200  \                          map_of (fields (G,C')) f = Some ft";
   1.201  by( dtac rtranclD 1);
   1.202  by( Auto_tac);
   1.203 @@ -240,17 +240,17 @@
   1.204  
   1.205  
   1.206  val cfs_fields_lemma = prove_goalw thy [field_def] 
   1.207 -"\\<And>X. field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
   1.208 +"!!X. field (G,C) fn = Some (fd, fT) ==> map_of(fields (G,C)) (fn, fd) = Some fT"
   1.209  (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
   1.210  
   1.211 -val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
   1.212 -\  G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
   1.213 +val widen_cfs_fields = prove_goal thy "!!X. [|field (G,C) fn = Some (fd, fT);\
   1.214 +\  G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G|] ==> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
   1.215  fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
   1.216  bind_thm ("widen_cfs_fields",widen_cfs_fields);
   1.217  
   1.218  
   1.219 -Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
   1.220 -\  \\<longrightarrow> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
   1.221 +Goal "wf_prog wf_mb G ==> method (G,C) sig = Some (md,mh,m)\
   1.222 +\  --> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
   1.223  by( case_tac "is_class G C" 1);
   1.224  by(  forw_inst_tac [("C","C")] method_rec 2);
   1.225  by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
   1.226 @@ -264,7 +264,7 @@
   1.227  by( Asm_full_simp_tac 1);
   1.228  by( dtac override_SomeD 1);
   1.229  by( etac disjE 1);
   1.230 -by(  thin_tac "?P \\<longrightarrow> ?Q" 1);
   1.231 +by(  thin_tac "?P --> ?Q" 1);
   1.232  by(  Clarify_tac 2);
   1.233  by(  rtac rtrancl_trans 2);
   1.234  by(   atac 3);
   1.235 @@ -277,8 +277,8 @@
   1.236  by( Asm_full_simp_tac 1);
   1.237  qed_spec_mp "method_wf_mdecl";
   1.238  
   1.239 -Goal "\\<lbrakk>G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   1.240 -\  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
   1.241 +Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
   1.242 +\  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->\
   1.243  \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
   1.244  by( dtac rtranclD 1);
   1.245  by( etac disjE 1);
   1.246 @@ -312,15 +312,15 @@
   1.247  
   1.248  
   1.249  Goal
   1.250 - "\\<lbrakk> G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
   1.251 -\    method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
   1.252 -\ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
   1.253 + "[| G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
   1.254 +\    method (G,D) sig = Some (md, rT, b) |] \
   1.255 +\ ==> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
   1.256  by(auto_tac (claset() addDs [subcls_widen_methd,method_wf_mdecl],
   1.257               simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
   1.258  qed "subtype_widen_methd";
   1.259  
   1.260  
   1.261 -Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
   1.262 +Goal "wf_prog wf_mb G ==> \\<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
   1.263  by( case_tac "is_class G C" 1);
   1.264  by(  forw_inst_tac [("C","C")] method_rec 2);
   1.265  by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
   1.266 @@ -341,7 +341,7 @@
   1.267  qed_spec_mp "method_in_md";
   1.268  
   1.269  
   1.270 -Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
   1.271 +Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
   1.272  \ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
   1.273  by( etac subcls1_induct 1);
   1.274  by(   atac 1);