wneuper/isa: src/HOL/MicroJava/J/WellForm.ML@6fc37b5c5e98

     1 (*  Title:      HOL/MicroJava/J/WellForm.ML

     2     ID:         $Id$

     3     Author:     David von Oheimb

     4     Copyright   1999 Technische Universitaet Muenchen

     5 *)

     7 val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]

     8  "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> wf_cdecl wtm G (C,c)" (K [

     9 	Asm_full_simp_tac 1,

    10 	fast_tac (set_cs addDs [get_in_set]) 1]);

    12 val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]

    13 	"\\<And>X. wf_prog wtm G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [

    14 	safe_tac set_cs,

    15 	dtac in_set_get 1,

    16 	 Auto_tac]);

    17 Addsimps [class_Object];

    19 val is_class_Object = prove_goalw thy [is_class_def]

    20 	"\\<And>X. wf_prog wtm G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);

    21 Addsimps [is_class_Object];

    23 Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not>  G\\<turnstile>D\\<prec>C C";

    24 by( forward_tac [r_into_trancl] 1);

    25 by( dtac subcls1D 1);

    26 by( strip_tac1 1);

    27 by( dtac class_wf 1);

    28 by(  atac 1);

    29 by( rewtac wf_cdecl_def);

    30 by( Clarsimp_tac 1);

    31 qed "subcls1_wfD";

    33 val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def]

    34 "\\<And>X. \\<lbrakk>wf_cdecl wtm G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [

    35 	pair_tac "r" 1,

    36 	Asm_full_simp_tac 1,

    37 	strip_tac1 1,

    38 	option_case_tac 1,

    39 	Fast_tac 1]);

    41 local

    42 val lemma = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C=Object \\<longrightarrow> R" (K [

    43 	etac trancl_trans_induct 1,

    44 	 atac 2,

    45 	rewtac subcls1_def,

    46 	Auto_tac]);

    47 in

    48 val subcls_Object = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>Object\\<prec>C C\\<rbrakk> \\<Longrightarrow> R" (K [

    49 	etac (lemma RS mp) 1,

    50 	Auto_tac]);

    51 end;

    53 Goal "\\<lbrakk>wf_prog wt G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> \\<not>  G\\<turnstile>D\\<prec>C C";

    54 by(etac tranclE 1);

    55 by(ALLGOALS(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));

    56 qed "subcls_asym";

    58 val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [

    59 	etac trancl_trans_induct 1,

    60 	 fast_tac (HOL_cs addDs [subcls1_wfD]) 1,

    61 	fast_tac (HOL_cs addDs [subcls_asym]) 1]);

    63 val acyclic_subcls1 = prove_goalw thy [acyclic_def]

    64 	"\\<And>X. wf_prog wt G \\<Longrightarrow> acyclic (subcls1 G)" (K [

    65 	strip_tac1 1,

    66 	fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);

    68 val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [

    69 	rtac finite_acyclic_wf 1,

    70 	 stac finite_converse 1,

    71 	 rtac finite_subcls1 1,

    72 	stac acyclic_converse 1,

    73 	etac acyclic_subcls1 1]);

    76 val major::prems = goal thy

    77   "\\<lbrakk>wf_prog wt G; \\<And>C. \\<forall>D. G\\<turnstile>C\\<prec>C D \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";

    78 by(cut_facts_tac [major RS wf_subcls1] 1);

    79 by(dtac wf_trancl 1);

    80 by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);

    81 by(eres_inst_tac [("a","C")] wf_induct 1);

    82 by(resolve_tac prems 1);

    83 by(Auto_tac);

    84 qed "subcls_induct";

    86 val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wtm G; P Object; \

    87 \\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \

    88 \   wf_cdecl wtm G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\

    89 \ \\<rbrakk> \\<Longrightarrow> P C";

    90 by( cut_facts_tac prems 1);

    91 by( rtac impE 1);

    92 by(   atac 2);

    93 by(  atac 2);

    94 by( etac thin_rl 1);

    95 by( rtac subcls_induct 1);

    96 by(  atac 1);

    97 by( rtac impI 1);

    98 by( case_tac "C = Object" 1);

    99 by(  Fast_tac 1);

   100 by( ex_ftac is_classD 1);

   101 by( forward_tac [class_wf] 1);

   102 by(  atac 1);

   103 by( forward_tac [wf_cdecl_supD] 1);

   104 by(  atac 1);

   105 by( strip_tac1 1);

   106 by( rtac (hd (tl (tl (tl prems)))) 1);

   107 by(   atac 1);

   108 by(  atac 1);

   109 by( subgoal_tac "G\\<turnstile>C\\<prec>C1D" 1);

   110 by(  fast_tac (HOL_cs addIs [r_into_trancl]) 1);

   111 by( etac subcls1I 1);

   112 qed "subcls1_induct";

   114 Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) = \

   115 \ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \

   116 \ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \

   117 \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";

   118 by( stac (method_TC RS (wf_subcls1_rel RS (hd method.rules))) 1);

   119 by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]

   120 		addsplits [option.split]) 1);

   121 by( case_tac "C = Object" 1);

   122 by(  Asm_full_simp_tac 1);

   123 by( dtac class_wf 1);

   124 by(  atac 1);

   125 by( dtac wf_cdecl_supD 1);

   126 by(  atac 1);

   127 by( Asm_full_simp_tac 1);

   128 val method_rec = result();

   130 Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wtm G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \

   131 \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \

   132 \ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";

   133 by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.rules))) 1);

   134 by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);

   135 by( option_case_tac2 "sc" 1);

   136 by(  Asm_simp_tac 1);

   137 by( case_tac "C = Object" 1);

   138 by(  rotate_tac 2 1);

   139 by(  Asm_full_simp_tac 1);

   140 by( dtac class_wf 1);

   141 by(  atac 1);

   142 by( dtac wf_cdecl_supD 1);

   143 by(  atac 1);

   144 by( Asm_full_simp_tac 1);

   145 val fields_rec = result();

   147 val method_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> method (G,Object) = empty"

   148 	(K [stac method_rec 1,Auto_tac]);

   149 val fields_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> fields (G,Object) = []"(K [

   150 	stac fields_rec 1,Auto_tac]);

   151 Addsimps [method_Object, fields_Object];

   152 val field_Object = prove_goalw thy [field_def]

   153  "\\<And>X. wf_prog wtm G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);

   154 Addsimps [field_Object];

   156 val subcls_C_Object = prove_goal thy

   157 	"\\<And>X. \\<lbrakk>is_class G C; wf_prog wtm G \\<rbrakk> \\<Longrightarrow> C \\<noteq> Object \\<longrightarrow> G\\<turnstile>C\\<prec>C Object" (K [

   158 	etac subcls1_induct 1,

   159 	  atac 1,

   160 	 Fast_tac 1,

   161 	safe_tac (HOL_cs addSDs [wf_cdecl_supD] addss (simpset())),

   162 	 fast_tac (HOL_cs addIs [r_into_trancl]) 1,

   163 	rtac trancl_trans 1,

   164 	 atac 2,

   165 	rtac r_into_trancl 1,

   166 	rtac subcls1I 1,

   167 	ALLGOALS Asm_simp_tac]) RS mp;

   169 val is_type_rTI = prove_goalw thy [wf_mhead_def]

   170 	"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"

   171 	(K [split_all_tac 1, Auto_tac]);

   173 val widen_Class_Object = prove_goal thy

   174 	"\\<lbrakk>wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object" (fn prems => [

   175 	cut_facts_tac prems 1,

   176 	case_tac "C=Object" 1,

   177 	 hyp_subst_tac 1,

   178 	 Asm_simp_tac 1,

   179 	rtac widen.subcls 1,

   180 	fast_tac (HOL_cs addEs [subcls_C_Object]) 1]);

   182 val widen_trans = prove_goal thy "\\<lbrakk>wf_prog wtm G; G\\<turnstile>S\\<preceq>U; G\\<turnstile>U\\<preceq>T\\<rbrakk> \\<Longrightarrow> G\\<turnstile>S\\<preceq>T"

   183 (fn prems=> [cut_facts_tac prems 1,

   184 	fast_tac (HOL_cs addEs [widen_trans_lemma, widen_Class_Object,

   185 				subcls_Object]) 1]);

   187 val fields_mono = prove_goal thy

   188 "\\<And>X. \\<lbrakk>G\\<turnstile>C'\\<prec>C C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \

   189 \ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))" (K [

   190 	etac trancl_trans_induct 1,

   191 	 safe_tac (HOL_cs addSDs [subcls1D]),

   192 	stac fields_rec 1,

   193 	  Auto_tac]) RS mp;

   195 Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \

   196 \ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq>Class fd";

   197 by( etac subcls1_induct 1);

   198 by(   atac 1);

   199 by(  Asm_simp_tac 1);

   200 by( safe_tac HOL_cs);

   201 by( stac fields_rec 1);

   202 by(   atac 1);

   203 by(  atac 1);

   204 by( Simp_tac 1);

   205 by( rtac ballI 1);

   206 by( split_all_tac 1);

   207 by( Simp_tac 1);

   208 by( etac UnE 1);

   209 by(  dtac split_Pair_eq 1);

   210 by(  SELECT_GOAL (Auto_tac) 1);

   211 by( rtac widen_trans 1);

   212 by(   atac 1);

   213 by(  etac (r_into_trancl RS widen.subcls) 1);

   214 by( etac BallE 1);

   215 by(  contr_tac 1);

   216 by( Asm_full_simp_tac 1);

   217 val widen_fields_defpl' = result();

   219 Goal "\\<lbrakk>is_class G C; wf_prog wtm G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \

   220 \ G\\<turnstile>Class C\\<preceq>Class fd";

   221 by( dtac widen_fields_defpl' 1);

   222 by(  atac 1);

   223 (*###################*)

   224 by( dtac bspec 1);

   225 auto();

   226 val widen_fields_defpl = result();

   229 Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";

   230 by( etac subcls1_induct 1);

   231 by(   atac 1);

   232 by(  safe_tac (HOL_cs addSDs [wf_cdecl_supD]));

   233 by(  Asm_simp_tac 1);

   234 by( dtac subcls1_wfD 1);

   235 by(  atac 1);

   236 by( stac fields_rec 1);

   237 by   Auto_tac;

   238 by( rotate_tac ~1 1);

   239 by( ex_ftac is_classD 1);

   240 by( forward_tac [class_wf] 1);

   241 by  Auto_tac;

   242 by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);

   243 by( etac unique_append 1);

   244 by(  rtac unique_map_Pair 1);

   245 by(  Step_tac 1);

   246 by (EVERY1[dtac widen_fields_defpl, atac, atac]);

   247 by( Asm_full_simp_tac 1);

   248 by( dtac split_Pair_eq 1);

   249 by( fast_tac (HOL_cs addSDs [widen_Class_Class]) 1);

   250 val unique_fields = result();

   252 Goal

   253 "\\<lbrakk>wf_prog wtm G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \

   254 \                          map_of (fields (G,C')) f = Some ft";

   255 by( dtac widen_Class_Class 1);

   256 by( etac disjE 1);

   257 by(  Asm_simp_tac 1);

   258 by( rtac table_mono 1);

   259 by(   atac 3);

   260 by(  rtac unique_fields 1);

   261 by(   etac subcls_is_class 1);

   262 by(  atac 1);

   263 by( fast_tac (HOL_cs addEs [fields_mono]) 1);

   264 val widen_fields_mono = result();

   267 val cfs_fields_lemma = prove_goalw thy [field_def]

   268 "\\<And>X. field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"

   269 (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);

   271 val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\

   272 \  G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[

   273 fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);

   275 Goal "wf_prog wtm G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\

   276 \  \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wtm G md (sig,(mh,m))";

   277 by( case_tac "is_class G C" 1);

   278 by(  forw_inst_tac [("C","C")] method_rec 2);

   279 by(    asm_full_simp_tac (simpset() addsimps [is_class_def]

   280 	delsimps [not_None_eq]) 2);

   281 by( etac subcls1_induct 1);

   282 by(   atac 1);

   283 by(  Force_tac 1);

   284 by( forw_inst_tac [("C","C")] method_rec 1);

   285 by( strip_tac1 1);

   286 by( rotate_tac ~1 1);

   287 by( Asm_full_simp_tac 1);

   288 by( dtac override_SomeD 1);

   289 by( etac disjE 1);

   290 by(  thin_tac "?P \\<longrightarrow> ?Q" 1);

   291 by(  Clarify_tac 2);

   292 by(  rtac widen_trans 2);

   293 by(    atac 2);

   294 by(   atac 3);

   295 by(  rtac widen.subcls 2);

   296 by(  rtac r_into_trancl 2);

   297 by(  fast_tac (HOL_cs addIs [subcls1I]) 2);

   298 by( forward_tac [table_mapf_SomeD] 1);

   299 by( strip_tac1 1);

   300 by( Asm_full_simp_tac 1);

   301 by( rewtac wf_cdecl_def);

   302 by( Asm_full_simp_tac 1);

   303 val method_wf_mdecl = result() RS mp;

   305 Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wt G\\<rbrakk> \\<Longrightarrow> \

   306 \  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\

   307 \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";

   308 by( etac trancl_trans_induct 1);

   309 by(  strip_tac1 2);

   310 by(  EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);

   311 by(  fast_tac (HOL_cs addEs [widen_trans]) 2);

   312 by( strip_tac1 1);

   313 by( dtac subcls1D 1);

   314 by( strip_tac1 1);

   315 by( stac method_rec 1);

   316 by(  atac 1);

   317 by( rewtac override_def);

   318 by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);

   319 by( case_tac "\\<exists>z. map_of(map (\\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z" 1);

   320 by(  etac exE 1);

   321 by(  asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 2);

   322 by(  ALLGOALS (rotate_tac ~1 THEN' forward_tac[ssubst] THEN' (fn n=>atac(n+1))));

   323 by(  ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex])));

   324 by( dtac class_wf 1);

   325 by(  atac 1);

   326 by( split_all_tac 1);

   327 by( rewtac wf_cdecl_def);

   328 by( dtac table_mapf_Some2 1);

   329 by( Clarsimp_tac 1);

   330 by( dres_inst_tac [("xys1","ms")] get_in_set 1);

   331 by Auto_tac;

   332 qed_spec_mp "subcls_widen_methd";

   335 Goal

   336  "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wt G; \

   337 \    method (G,D) sig = Some (md, rT, b) \\<rbrakk> \

   338 \ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";

   339 by(auto_tac (claset() addSDs [widen_Class_Class]

   340                       addDs [subcls_widen_methd,method_wf_mdecl],

   341              simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));

   342 qed "subtype_widen_methd";

   345 Goal "wf_prog wt 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)";

   346 by( case_tac "is_class G C" 1);

   347 by(  forw_inst_tac [("C","C")] method_rec 2);

   348 by(    asm_full_simp_tac (simpset() addsimps [is_class_def]

   349 	delsimps [not_None_eq]) 2);

   350 by (etac subcls1_induct 1);

   351   ba 1;

   352  by (Asm_full_simp_tac 1);

   353 by (stac method_rec 1);

   354  ba 1;

   355 by (Clarify_tac 1);

   356 by (eres_inst_tac [("x","Da")] allE 1);

   357 by (Clarsimp_tac 1);

   358  by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);

   359  by (Clarify_tac 1);

   360  by (stac method_rec 1);

   361   ba 1;

   362  by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);

   363 qed_spec_mp "method_in_md";

   365 writeln"OK";

   367 Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \

   368 \ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";

   369 by( etac subcls1_induct 1);

   370 by(   atac 1);

   371 by(  Asm_simp_tac 1);

   372 by( strip_tac1 1);

   373 by( stac fields_rec 1);

   374 by(   atac 1);

   375 by(  atac 1);

   376 by( Asm_simp_tac 1);

   377 by( safe_tac set_cs);

   378 by(  Fast_tac 2);

   379 by( dtac class_wf 1);

   380 by(  atac 1);

   381 by( rewtac wf_cdecl_def);

   382 by( Asm_full_simp_tac 1);

   383 by( strip_tac1 1);

   384 by( EVERY[dtac bspec 1, atac 1]);

   385 by( rewtac wf_fdecl_def);

   386 by( split_all_tac 1);

   387 by( Asm_full_simp_tac 1);

   388 val is_type_fields = result() RS bspec;

author	nipkow
	Fri, 26 Nov 1999 08:46:59 +0100
changeset 8034	6fc37b5c5e98
parent 8011	d14c4e9e9c8e
child 8082	381716a86fcb
permissions	-rw-r--r--