1 (* Title: HOL/MicroJava/J/WellType.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 Goal |
|
8 "[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C|]\ |
|
9 \ ==> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT"; |
|
10 by( dtac subcls_widen_methd 1); |
|
11 by Auto_tac; |
|
12 qed "widen_methd"; |
|
13 |
|
14 |
|
15 Goal |
|
16 "[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G; \ |
|
17 \ class G C = Some y|] ==> \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \ |
|
18 \ 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)"; |
|
19 by( datac widen_methd 2 1); |
|
20 by( Clarify_tac 1); |
|
21 by( ftac subcls_is_class2 1); |
|
22 by (rewtac is_class_def); |
|
23 by (Asm_simp_tac 1); |
|
24 by( dtac method_wf_mdecl 1); |
|
25 by( rewtac wf_mdecl_def); |
|
26 by( rewtac is_class_def); |
|
27 by Auto_tac; |
|
28 qed "Call_lemma"; |
|
29 |
|
30 Goal "wf_prog wf_mb G ==> method (G,Object) sig = None"; |
|
31 by (Asm_simp_tac 1); |
|
32 qed "method_Object"; |
|
33 Addsimps [method_Object]; |
|
34 |
|
35 Goalw [max_spec_def] |
|
36 "x \\<in> max_spec G C sig ==> x \\<in> appl_methds G C sig"; |
|
37 by (Fast_tac 1); |
|
38 qed"max_spec2appl_meths"; |
|
39 |
|
40 Goalw [appl_methds_def] |
|
41 "((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) ==> \ |
|
42 \ \\<exists>D b. md = Class D \\<and> method (G,C) (mn, pTs') = Some (D,rT,b) \ |
|
43 \ \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"; |
|
44 by (Fast_tac 1); |
|
45 qed "appl_methsD"; |
|
46 |
|
47 bind_thm ("max_spec2mheads", insertI1 RSN (2,(equalityD2 RS subsetD)) RS |
|
48 max_spec2appl_meths RS appl_methsD); |
|
49 |
|
50 Goal "(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)"; |
|
51 by (rtac val_.induct 1); |
|
52 by (Fast_tac 5); |
|
53 by Auto_tac; |
|
54 qed_spec_mp "is_type_typeof"; |
|
55 Addsimps [is_type_typeof]; |
|
56 |
|
57 Goal "typeof (\\<lambda>a. None) v = Some T \\<longrightarrow> is_type G T"; |
|
58 by (rtac val_.induct 1); |
|
59 by Auto_tac; |
|
60 qed_spec_mp "typeof_empty_is_type"; |
|
61 |
|
62 Goal "wf_prog wf_mb G \\<Longrightarrow> ((G,L)\\<turnstile>e::T \\<longrightarrow> is_type G T) \\<and> \ |
|
63 \ ((G,L)\\<turnstile>es[::]Ts \\<longrightarrow> Ball (set Ts) (is_type G)) \\<and> ((G,L)\\<turnstile>c \\<surd> \\<longrightarrow> True)"; |
|
64 by (rtac ty_expr_ty_exprs_wt_stmt.induct 1); |
|
65 by Auto_tac; |
|
66 by ( etac typeof_empty_is_type 1); |
|
67 by ( asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1); |
|
68 by ( dtac field_fields 1); |
|
69 by ( datac fields_is_type 1 1); |
|
70 by ( Asm_simp_tac 1); |
|
71 ba 1; |
|
72 by (auto_tac (claset() addSDs [max_spec2mheads,method_wf_mdecl,is_type_rTI], simpset()addsimps[wf_mdecl_def])); |
|
73 qed "wt_is_type"; |
|
74 |
|
75 bind_thm ("ty_expr_is_type", permute_prems 0 1 (wt_is_type RS conjunct1 RS mp)); |
|