|
1 (* Title: HOL/MicroJava/J/WellType.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 Goalw [m_head_def] |
|
8 "\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wtm G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \ |
|
9 \\\<exists>md' rT' b'. cmethd (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT"; |
|
10 by( forward_tac [widen_Class_RefT] 1); |
|
11 by( etac exE 1); |
|
12 by( hyp_subst_tac 1); |
|
13 by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1); |
|
14 by( rewtac option_map_def); |
|
15 by( strip_tac1 1); |
|
16 by( split_all_tac 1); |
|
17 by( dtac widen_Class_Class 1); |
|
18 by( etac disjE 1); |
|
19 by( hyp_subst_tac 1); |
|
20 by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1); |
|
21 by( dtac subcls_widen_methd 1); |
|
22 by Auto_tac; |
|
23 qed "widen_methd"; |
|
24 |
|
25 |
|
26 Goal |
|
27 "\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \ |
|
28 \ \\<exists>T' rT' b. cmethd (G,T'') sig = Some (T',rT',b) \\<and> \ |
|
29 \ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wtm G T' (sig,rT',b)"; |
|
30 by( dtac widen_methd 1); |
|
31 by( atac 1); |
|
32 by( atac 1); |
|
33 by( Clarsimp_tac 1); |
|
34 by( dtac cmethd_wf_mdecl 1); |
|
35 by( atac 1); |
|
36 by( rewtac wf_mdecl_def); |
|
37 by Auto_tac; |
|
38 val Call_lemma = result(); |
|
39 |
|
40 |
|
41 val m_head_Object = prove_goalw thy [m_head_def] |
|
42 "\\<And>x. wf_prog wtm G \\<Longrightarrow> m_head G (ClassT Object) sig = None" (K [Asm_simp_tac 1]); |
|
43 |
|
44 Addsimps [m_head_Object]; |
|
45 |
|
46 val max_spec2appl_meths = prove_goalw thy [max_spec_def] |
|
47 "x \\<in> max_spec G rT sig \\<longrightarrow> x \\<in> appl_methds G rT sig" |
|
48 (fn _ => [Fast_tac 1]) RS mp; |
|
49 |
|
50 val appl_methsD = prove_goalw thy [appl_methds_def] |
|
51 "(mh,pTs')\\<in>appl_methds G rT (mn, pTs) \\<longrightarrow> \ |
|
52 \ m_head G rT (mn, pTs') = Some mh \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'" |
|
53 (K [Fast_tac 1]) RS mp; |
|
54 |
|
55 val is_type_typeof = prove_goal thy |
|
56 "(\\<forall>a. v \\<noteq> Addr a) \\<longrightarrow> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)" (K [ |
|
57 rtac val_.induct 1, |
|
58 Fast_tac 5, |
|
59 ALLGOALS Simp_tac]) RS mp; |
|
60 |
|
61 Addsimps [is_type_typeof]; |