author | haftmann |
Fri, 11 Jun 2010 17:14:02 +0200 | |
changeset 37407 | 61dd8c145da7 |
parent 35416 | d8d7d1b785af |
child 52866 | 438f578ef1d9 |
permissions | -rw-r--r-- |
13673 | 1 |
(* Title: HOL/MicroJava/Comp/TypeInf.thy |
2 |
Author: Martin Strecker |
|
3 |
*) |
|
4 |
||
5 |
(* Exact position in theory hierarchy still to be determined *) |
|
17778 | 6 |
theory TypeInf |
7 |
imports "../J/WellType" |
|
8 |
begin |
|
13673 | 9 |
|
10 |
||
11 |
||
12 |
(**********************************************************************) |
|
13 |
; |
|
14 |
||
15 |
(*** Inversion of typing rules -- to be moved into WellType.thy |
|
16 |
Also modify the wtpd_expr_\<dots> proofs in CorrComp.thy ***) |
|
17 |
||
18 |
lemma NewC_invers: "E\<turnstile>NewC C::T |
|
19 |
\<Longrightarrow> T = Class C \<and> is_class (prg E) C" |
|
20 |
by (erule ty_expr.cases, auto) |
|
21 |
||
22 |
lemma Cast_invers: "E\<turnstile>Cast D e::T |
|
14045 | 23 |
\<Longrightarrow> \<exists> C. T = Class D \<and> E\<turnstile>e::C \<and> is_class (prg E) D \<and> prg E\<turnstile>C\<preceq>? Class D" |
13673 | 24 |
by (erule ty_expr.cases, auto) |
25 |
||
26 |
lemma Lit_invers: "E\<turnstile>Lit x::T |
|
27 |
\<Longrightarrow> typeof (\<lambda>v. None) x = Some T" |
|
28 |
by (erule ty_expr.cases, auto) |
|
29 |
||
30 |
lemma LAcc_invers: "E\<turnstile>LAcc v::T |
|
31 |
\<Longrightarrow> localT E v = Some T \<and> is_type (prg E) T" |
|
32 |
by (erule ty_expr.cases, auto) |
|
33 |
||
34 |
lemma BinOp_invers: "E\<turnstile>BinOp bop e1 e2::T' |
|
35 |
\<Longrightarrow> \<exists> T. E\<turnstile>e1::T \<and> E\<turnstile>e2::T \<and> |
|
36 |
(if bop = Eq then T' = PrimT Boolean |
|
37 |
else T' = T \<and> T = PrimT Integer)" |
|
38 |
by (erule ty_expr.cases, auto) |
|
39 |
||
40 |
lemma LAss_invers: "E\<turnstile>v::=e::T' |
|
41 |
\<Longrightarrow> \<exists> T. v ~= This \<and> E\<turnstile>LAcc v::T \<and> E\<turnstile>e::T' \<and> prg E\<turnstile>T'\<preceq>T" |
|
42 |
by (erule ty_expr.cases, auto) |
|
43 |
||
44 |
lemma FAcc_invers: "E\<turnstile>{fd}a..fn::fT |
|
45 |
\<Longrightarrow> \<exists> C. E\<turnstile>a::Class C \<and> field (prg E,C) fn = Some (fd,fT)" |
|
46 |
by (erule ty_expr.cases, auto) |
|
47 |
||
48 |
lemma FAss_invers: "E\<turnstile>{fd}a..fn:=v::T' |
|
49 |
\<Longrightarrow> \<exists> T. E\<turnstile>{fd}a..fn::T \<and> E\<turnstile>v ::T' \<and> prg E\<turnstile>T'\<preceq>T" |
|
50 |
by (erule ty_expr.cases, auto) |
|
51 |
||
52 |
lemma Call_invers: "E\<turnstile>{C}a..mn({pTs'}ps)::rT |
|
53 |
\<Longrightarrow> \<exists> pTs md. |
|
54 |
E\<turnstile>a::Class C \<and> E\<turnstile>ps[::]pTs \<and> max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}" |
|
55 |
by (erule ty_expr.cases, auto) |
|
56 |
||
57 |
||
58 |
lemma Nil_invers: "E\<turnstile>[] [::] Ts \<Longrightarrow> Ts = []" |
|
59 |
by (erule ty_exprs.cases, auto) |
|
60 |
||
61 |
lemma Cons_invers: "E\<turnstile>e#es[::]Ts \<Longrightarrow> |
|
62 |
\<exists> T Ts'. Ts = T#Ts' \<and> E \<turnstile>e::T \<and> E \<turnstile>es[::]Ts'" |
|
63 |
by (erule ty_exprs.cases, auto) |
|
64 |
||
65 |
||
66 |
lemma Expr_invers: "E\<turnstile>Expr e\<surd> \<Longrightarrow> \<exists> T. E\<turnstile>e::T" |
|
67 |
by (erule wt_stmt.cases, auto) |
|
68 |
||
69 |
lemma Comp_invers: "E\<turnstile>s1;; s2\<surd> \<Longrightarrow> E\<turnstile>s1\<surd> \<and> E\<turnstile>s2\<surd>" |
|
70 |
by (erule wt_stmt.cases, auto) |
|
71 |
||
72 |
lemma Cond_invers: "E\<turnstile>If(e) s1 Else s2\<surd> |
|
73 |
\<Longrightarrow> E\<turnstile>e::PrimT Boolean \<and> E\<turnstile>s1\<surd> \<and> E\<turnstile>s2\<surd>" |
|
74 |
by (erule wt_stmt.cases, auto) |
|
75 |
||
76 |
lemma Loop_invers: "E\<turnstile>While(e) s\<surd> |
|
77 |
\<Longrightarrow> E\<turnstile>e::PrimT Boolean \<and> E\<turnstile>s\<surd>" |
|
78 |
by (erule wt_stmt.cases, auto) |
|
79 |
||
80 |
||
81 |
(**********************************************************************) |
|
82 |
||
83 |
||
84 |
declare split_paired_All [simp del] |
|
85 |
declare split_paired_Ex [simp del] |
|
86 |
||
87 |
(* Uniqueness of types property *) |
|
88 |
||
89 |
lemma uniqueness_of_types: " |
|
14045 | 90 |
(\<forall> (E\<Colon>'a prog \<times> (vname \<Rightarrow> ty option)) T1 T2. |
91 |
E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2) \<and> |
|
92 |
(\<forall> (E\<Colon>'a prog \<times> (vname \<Rightarrow> ty option)) Ts1 Ts2. |
|
93 |
E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)" |
|
13673 | 94 |
apply (rule expr.induct) |
95 |
||
96 |
(* NewC *) |
|
97 |
apply (intro strip) |
|
98 |
apply (erule ty_expr.cases) apply simp+ |
|
99 |
apply (erule ty_expr.cases) apply simp+ |
|
100 |
||
101 |
(* Cast *) |
|
102 |
apply (intro strip) |
|
103 |
apply (erule ty_expr.cases) apply simp+ |
|
104 |
apply (erule ty_expr.cases) apply simp+ |
|
105 |
||
106 |
(* Lit *) |
|
107 |
apply (intro strip) |
|
108 |
apply (erule ty_expr.cases) apply simp+ |
|
109 |
apply (erule ty_expr.cases) apply simp+ |
|
110 |
||
111 |
(* BinOp *) |
|
112 |
apply (intro strip) |
|
113 |
apply (case_tac binop) |
|
114 |
(* Eq *) |
|
115 |
apply (erule ty_expr.cases) apply simp+ |
|
116 |
apply (erule ty_expr.cases) apply simp+ |
|
117 |
(* Add *) |
|
118 |
apply (erule ty_expr.cases) apply simp+ |
|
119 |
apply (erule ty_expr.cases) apply simp+ |
|
120 |
||
121 |
(* LAcc *) |
|
122 |
apply (intro strip) |
|
123 |
apply (erule ty_expr.cases) apply simp+ |
|
124 |
apply (erule ty_expr.cases) apply simp+ |
|
125 |
||
126 |
(* LAss *) |
|
127 |
apply (intro strip) |
|
128 |
apply (erule ty_expr.cases) apply simp+ |
|
129 |
apply (erule ty_expr.cases) apply simp+ |
|
130 |
||
131 |
||
132 |
(* FAcc *) |
|
133 |
apply (intro strip) |
|
134 |
apply (drule FAcc_invers)+ apply (erule exE)+ |
|
135 |
apply (subgoal_tac "C = Ca", simp) apply blast |
|
136 |
||
137 |
||
138 |
(* FAss *) |
|
139 |
apply (intro strip) |
|
140 |
apply (drule FAss_invers)+ apply (erule exE)+ apply (erule conjE)+ |
|
141 |
apply (drule FAcc_invers)+ apply (erule exE)+ apply blast |
|
142 |
||
143 |
||
144 |
(* Call *) |
|
145 |
apply (intro strip) |
|
146 |
apply (drule Call_invers)+ apply (erule exE)+ apply (erule conjE)+ |
|
147 |
apply (subgoal_tac "pTs = pTsa", simp) apply blast |
|
148 |
||
149 |
(* expression lists *) |
|
150 |
apply (intro strip) |
|
151 |
apply (erule ty_exprs.cases)+ apply simp+ |
|
152 |
||
153 |
apply (intro strip) |
|
154 |
apply (erule ty_exprs.cases, simp) |
|
155 |
apply (erule ty_exprs.cases, simp) |
|
156 |
apply (subgoal_tac "e = ea", simp) apply simp |
|
157 |
done |
|
158 |
||
159 |
||
160 |
lemma uniqueness_of_types_expr [rule_format (no_asm)]: " |
|
161 |
(\<forall> E T1 T2. E\<turnstile>e :: T1 \<longrightarrow> E\<turnstile>e :: T2 \<longrightarrow> T1 = T2)" |
|
162 |
by (rule uniqueness_of_types [THEN conjunct1]) |
|
163 |
||
164 |
lemma uniqueness_of_types_exprs [rule_format (no_asm)]: " |
|
165 |
(\<forall> E Ts1 Ts2. E\<turnstile>es [::] Ts1 \<longrightarrow> E\<turnstile>es [::] Ts2 \<longrightarrow> Ts1 = Ts2)" |
|
166 |
by (rule uniqueness_of_types [THEN conjunct2]) |
|
167 |
||
168 |
||
169 |
||
170 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
17778
diff
changeset
|
171 |
definition inferred_tp :: "[java_mb env, expr] \<Rightarrow> ty" where |
13673 | 172 |
"inferred_tp E e == (SOME T. E\<turnstile>e :: T)" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
17778
diff
changeset
|
173 |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
17778
diff
changeset
|
174 |
definition inferred_tps :: "[java_mb env, expr list] \<Rightarrow> ty list" where |
13673 | 175 |
"inferred_tps E es == (SOME Ts. E\<turnstile>es [::] Ts)" |
176 |
||
177 |
(* get inferred type(s) for well-typed term *) |
|
178 |
lemma inferred_tp_wt: "E\<turnstile>e :: T \<Longrightarrow> (inferred_tp E e) = T" |
|
179 |
by (auto simp: inferred_tp_def intro: uniqueness_of_types_expr) |
|
180 |
||
181 |
lemma inferred_tps_wt: "E\<turnstile>es [::] Ts \<Longrightarrow> (inferred_tps E es) = Ts" |
|
182 |
by (auto simp: inferred_tps_def intro: uniqueness_of_types_exprs) |
|
183 |
||
184 |
||
185 |
end |
|
186 |