src/HOL/MicroJava/J/WellType.thy
author oheimb
Thu Feb 01 20:53:13 2001 +0100 (2001-02-01)
changeset 11026 a50365d21144
parent 10763 08e1610c1dcb
child 11070 cc421547e744
permissions -rw-r--r--
converted to Isar, simplifying recursion on class hierarchy
nipkow@8011
     1
(*  Title:      HOL/MicroJava/J/WellType.thy
nipkow@8011
     2
    ID:         $Id$
nipkow@8011
     3
    Author:     David von Oheimb
nipkow@8011
     4
    Copyright   1999 Technische Universitaet Muenchen
nipkow@8011
     5
nipkow@8011
     6
Well-typedness of Java programs
nipkow@8011
     7
nipkow@8011
     8
the formulation of well-typedness of method calls given below (as well as
nipkow@8011
     9
the Java Specification 1.0) is a little too restrictive: Is does not allow
nipkow@8011
    10
methods of class Object to be called upon references of interface type.
nipkow@8011
    11
nipkow@8011
    12
simplifications:
nipkow@8011
    13
* the type rules include all static checks on expressions and statements, e.g.
nipkow@8011
    14
  definedness of names (of parameters, locals, fields, methods)
nipkow@8011
    15
nipkow@8011
    16
*)
nipkow@8011
    17
oheimb@11026
    18
theory WellType = Term + WellForm:
nipkow@8011
    19
nipkow@8011
    20
types	lenv (* local variables, including method parameters and This *)
oheimb@11026
    21
	= "vname \<leadsto> ty"
nipkow@8011
    22
        'c env
oheimb@11026
    23
	= "'c prog \<times> lenv"
nipkow@8011
    24
nipkow@8011
    25
syntax
kleing@10061
    26
  prg    :: "'c env => 'c prog"
oheimb@11026
    27
  localT :: "'c env => (vname \<leadsto> ty)"
nipkow@8011
    28
nipkow@8011
    29
translations	
kleing@10061
    30
  "prg"    => "fst"
kleing@10061
    31
  "localT" => "snd"
nipkow@8011
    32
nipkow@8011
    33
consts
oheimb@11026
    34
  more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
oheimb@11026
    35
                (ty \<times> 'x) \<times> ty list => bool"
oheimb@11026
    36
  appl_methds :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
oheimb@11026
    37
  max_spec :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
nipkow@8011
    38
nipkow@8011
    39
defs
oheimb@11026
    40
  more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
oheimb@11026
    41
		                            list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
nipkow@8011
    42
  
nipkow@8011
    43
  (* applicable methods, cf. 15.11.2.1 *)
oheimb@11026
    44
  appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
oheimb@8105
    45
		                 {((Class md,rT),pTs') |md rT mb pTs'.
oheimb@11026
    46
		                  method (G,C)  (mn, pTs') = Some (md,rT,mb) \<and>
oheimb@11026
    47
		                  list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
nipkow@8011
    48
nipkow@8011
    49
  (* maximally specific methods, cf. 15.11.2.2 *)
oheimb@11026
    50
  max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
oheimb@11026
    51
                                       (\<forall>m'\<in>appl_methds G C sig.
oheimb@11026
    52
                                         more_spec G m' m --> m' = m)}"
oheimb@11026
    53
oheimb@11026
    54
lemma max_spec2appl_meths: 
oheimb@11026
    55
  "x \<in> max_spec G C sig ==> x \<in> appl_methds G C sig"
oheimb@11026
    56
apply (unfold max_spec_def)
oheimb@11026
    57
apply (fast)
oheimb@11026
    58
done
oheimb@11026
    59
oheimb@11026
    60
lemma appl_methsD: 
oheimb@11026
    61
"((md,rT),pTs')\<in>appl_methds G C (mn, pTs) ==>  
oheimb@11026
    62
  \<exists>D b. md = Class D \<and> method (G,C) (mn, pTs') = Some (D,rT,b)  
oheimb@11026
    63
  \<and> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
oheimb@11026
    64
apply (unfold appl_methds_def)
oheimb@11026
    65
apply (fast)
oheimb@11026
    66
done
oheimb@11026
    67
oheimb@11026
    68
lemmas max_spec2mheads = insertI1 [THEN [2] equalityD2 [THEN subsetD], 
oheimb@11026
    69
                         THEN max_spec2appl_meths, THEN appl_methsD]
oheimb@11026
    70
kleing@10061
    71
nipkow@8011
    72
consts
kleing@10042
    73
  typeof :: "(loc => ty option) => val => ty option"
nipkow@8011
    74
nipkow@8011
    75
primrec
nipkow@8011
    76
	"typeof dt  Unit    = Some (PrimT Void)"
nipkow@8011
    77
	"typeof dt  Null    = Some NT"
nipkow@8011
    78
	"typeof dt (Bool b) = Some (PrimT Boolean)"
nipkow@8011
    79
	"typeof dt (Intg i) = Some (PrimT Integer)"
nipkow@8011
    80
	"typeof dt (Addr a) = dt a"
nipkow@8011
    81
oheimb@11026
    82
lemma is_type_typeof [rule_format (no_asm), simp]: "(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"
oheimb@11026
    83
apply (rule val.induct)
oheimb@11026
    84
apply     auto
oheimb@11026
    85
done
oheimb@11026
    86
oheimb@11026
    87
lemma typeof_empty_is_type [rule_format (no_asm)]: 
oheimb@11026
    88
  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
oheimb@11026
    89
apply (rule val.induct)
oheimb@11026
    90
apply     auto
oheimb@11026
    91
done
oheimb@11026
    92
nipkow@8011
    93
types
oheimb@11026
    94
	java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
nipkow@8011
    95
	(* method body with parameter names, local variables, block, result expression *)
nipkow@8011
    96
nipkow@8011
    97
consts
oheimb@11026
    98
  ty_expr :: "java_mb env => (expr      \<times> ty     ) set"
oheimb@11026
    99
  ty_exprs:: "java_mb env => (expr list \<times> ty list) set"
kleing@10042
   100
  wt_stmt :: "java_mb env =>  stmt                 set"
nipkow@8011
   101
nipkow@8011
   102
syntax
oheimb@11026
   103
  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
oheimb@11026
   104
  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
oheimb@11026
   105
  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
nipkow@8011
   106
kleing@10061
   107
syntax (HTML)
kleing@10061
   108
  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
kleing@10061
   109
  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
kleing@10061
   110
  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
kleing@10061
   111
nipkow@8011
   112
nipkow@8011
   113
translations
oheimb@11026
   114
	"E\<turnstile>e :: T" == "(e,T) \<in> ty_expr  E"
oheimb@11026
   115
	"E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
oheimb@11026
   116
	"E\<turnstile>c \<surd>"    == "c     \<in> wt_stmt  E"
nipkow@8011
   117
  
oheimb@11026
   118
inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intros
nipkow@8011
   119
nipkow@8011
   120
(* well-typed expressions *)
nipkow@8011
   121
nipkow@8011
   122
  (* cf. 15.8 *)
oheimb@11026
   123
  NewC:	"[| is_class (prg E) C |] ==>
oheimb@11026
   124
         E\<turnstile>NewC C::Class C"
nipkow@8011
   125
nipkow@8011
   126
  (* cf. 15.15 *)
oheimb@11026
   127
  Cast:	"[| E\<turnstile>e::Class C; is_class (prg E) D;
oheimb@11026
   128
            prg E\<turnstile>C\<preceq>? D |] ==>
oheimb@11026
   129
         E\<turnstile>Cast D e::Class D"
nipkow@8011
   130
nipkow@8011
   131
  (* cf. 15.7.1 *)
oheimb@11026
   132
  Lit:	  "[| typeof (\<lambda>v. None) x = Some T |] ==>
oheimb@11026
   133
         E\<turnstile>Lit x::T"
nipkow@8011
   134
oheimb@9240
   135
  
nipkow@8011
   136
  (* cf. 15.13.1 *)
oheimb@11026
   137
  LAcc:	"[| localT E v = Some T; is_type (prg E) T |] ==>
oheimb@11026
   138
         E\<turnstile>LAcc v::T"
oheimb@9240
   139
oheimb@11026
   140
  BinOp:"[| E\<turnstile>e1::T;
oheimb@11026
   141
            E\<turnstile>e2::T;
kleing@10061
   142
            if bop = Eq then T' = PrimT Boolean
oheimb@11026
   143
                        else T' = T \<and> T = PrimT Integer|] ==>
oheimb@11026
   144
         E\<turnstile>BinOp bop e1 e2::T'"
oheimb@9240
   145
nipkow@8011
   146
  (* cf. 15.25, 15.25.1 *)
oheimb@11026
   147
  LAss: "[| E\<turnstile>LAcc v::T;
oheimb@11026
   148
	          E\<turnstile>e::T';
oheimb@11026
   149
            prg E\<turnstile>T'\<preceq>T |] ==>
oheimb@11026
   150
         E\<turnstile>v::=e::T'"
nipkow@8011
   151
nipkow@8011
   152
  (* cf. 15.10.1 *)
oheimb@11026
   153
  FAcc: "[| E\<turnstile>a::Class C; 
kleing@10061
   154
            field (prg E,C) fn = Some (fd,fT) |] ==>
oheimb@11026
   155
         E\<turnstile>{fd}a..fn::fT"
nipkow@8011
   156
nipkow@8011
   157
  (* cf. 15.25, 15.25.1 *)
oheimb@11026
   158
  FAss: "[| E\<turnstile>{fd}a..fn::T;
oheimb@11026
   159
            E\<turnstile>v        ::T';
oheimb@11026
   160
            prg E\<turnstile>T'\<preceq>T |] ==>
oheimb@11026
   161
         E\<turnstile>{fd}a..fn:=v::T'"
nipkow@8011
   162
nipkow@8011
   163
nipkow@8011
   164
  (* cf. 15.11.1, 15.11.2, 15.11.3 *)
oheimb@11026
   165
  Call: "[| E\<turnstile>a::Class C;
oheimb@11026
   166
            E\<turnstile>ps[::]pTs;
kleing@10061
   167
            max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
oheimb@11026
   168
         E\<turnstile>{C}a..mn({pTs'}ps)::rT"
nipkow@8011
   169
nipkow@8011
   170
(* well-typed expression lists *)
nipkow@8011
   171
nipkow@8011
   172
  (* cf. 15.11.??? *)
oheimb@11026
   173
  Nil: "E\<turnstile>[][::][]"
nipkow@8011
   174
nipkow@8011
   175
  (* cf. 15.11.??? *)
oheimb@11026
   176
  Cons:"[| E\<turnstile>e::T;
oheimb@11026
   177
           E\<turnstile>es[::]Ts |] ==>
oheimb@11026
   178
        E\<turnstile>e#es[::]T#Ts"
nipkow@8011
   179
nipkow@8011
   180
(* well-typed statements *)
nipkow@8011
   181
oheimb@11026
   182
  Skip:"E\<turnstile>Skip\<surd>"
nipkow@8011
   183
oheimb@11026
   184
  Expr:"[| E\<turnstile>e::T |] ==>
oheimb@11026
   185
        E\<turnstile>Expr e\<surd>"
nipkow@8011
   186
oheimb@11026
   187
  Comp:"[| E\<turnstile>s1\<surd>; 
oheimb@11026
   188
           E\<turnstile>s2\<surd> |] ==>
oheimb@11026
   189
        E\<turnstile>s1;; s2\<surd>"
nipkow@8011
   190
nipkow@8011
   191
  (* cf. 14.8 *)
oheimb@11026
   192
  Cond:"[| E\<turnstile>e::PrimT Boolean;
oheimb@11026
   193
           E\<turnstile>s1\<surd>;
oheimb@11026
   194
           E\<turnstile>s2\<surd> |] ==>
oheimb@11026
   195
         E\<turnstile>If(e) s1 Else s2\<surd>"
nipkow@8011
   196
nipkow@8011
   197
  (* cf. 14.10 *)
oheimb@11026
   198
  Loop:"[| E\<turnstile>e::PrimT Boolean;
oheimb@11026
   199
           E\<turnstile>s\<surd> |] ==>
oheimb@11026
   200
        E\<turnstile>While(e) s\<surd>"
nipkow@8011
   201
nipkow@8011
   202
constdefs
nipkow@8011
   203
oheimb@11026
   204
 wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
oheimb@11026
   205
"wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
oheimb@11026
   206
	length pTs = length pns \<and>
oheimb@11026
   207
	nodups pns \<and>
oheimb@11026
   208
	unique lvars \<and>
oheimb@11026
   209
	(\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
oheimb@11026
   210
	(\<forall>(vn,T)\<in>set lvars. is_type G T) &
oheimb@11026
   211
	(let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
oheimb@11026
   212
	 E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
nipkow@8011
   213
oheimb@11026
   214
 wf_java_prog :: "java_mb prog => bool"
kleing@10042
   215
"wf_java_prog G == wf_prog wf_java_mdecl G"
nipkow@8011
   216
oheimb@11026
   217
oheimb@11026
   218
lemma wt_is_type: "wf_prog wf_mb G \<Longrightarrow> ((G,L)\<turnstile>e::T \<longrightarrow> is_type G T) \<and>  
oheimb@11026
   219
       ((G,L)\<turnstile>es[::]Ts \<longrightarrow> Ball (set Ts) (is_type G)) \<and> ((G,L)\<turnstile>c \<surd> \<longrightarrow> True)"
oheimb@11026
   220
apply (rule ty_expr_ty_exprs_wt_stmt.induct)
oheimb@11026
   221
apply auto
oheimb@11026
   222
apply (   erule typeof_empty_is_type)
oheimb@11026
   223
apply (  simp split add: split_if_asm)
oheimb@11026
   224
apply ( drule field_fields)
oheimb@11026
   225
apply ( drule (1) fields_is_type)
oheimb@11026
   226
apply (  simp (no_asm_simp))
oheimb@11026
   227
apply  (assumption)
oheimb@11026
   228
apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI simp add: wf_mdecl_def)
oheimb@11026
   229
done
oheimb@11026
   230
oheimb@11026
   231
lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, COMP swap_prems_rl]
oheimb@11026
   232
nipkow@8011
   233
end