src/HOL/MicroJava/J/WellType.thy
changeset 14045 a34d89ce6097
parent 13672 b95d12325b51
child 14134 0fdf5708c7a8
     1.1 --- a/src/HOL/MicroJava/J/WellType.thy	Mon May 26 11:42:41 2003 +0200
     1.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Mon May 26 18:36:15 2003 +0200
     1.3 @@ -108,19 +108,19 @@
     1.4  -- "local variables might include This, which is hidden anyway"
     1.5  
     1.6  consts
     1.7 -  ty_expr :: "(java_mb env \<times> expr      \<times> ty     ) set"
     1.8 -  ty_exprs:: "(java_mb env \<times> expr list \<times> ty list) set"
     1.9 -  wt_stmt :: "(java_mb env \<times> stmt               ) set"
    1.10 +  ty_expr :: "('c env \<times> expr      \<times> ty     ) set"
    1.11 +  ty_exprs:: "('c env \<times> expr list \<times> ty list) set"
    1.12 +  wt_stmt :: "('c env \<times> stmt               ) set"
    1.13  
    1.14  syntax (xsymbols)
    1.15 -  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
    1.16 -  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
    1.17 -  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
    1.18 +  ty_expr :: "'c env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
    1.19 +  ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
    1.20 +  wt_stmt :: "'c env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
    1.21  
    1.22  syntax
    1.23 -  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
    1.24 -  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
    1.25 -  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
    1.26 +  ty_expr :: "'c env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
    1.27 +  ty_exprs:: "'c env => [expr list, ty list] => bool" ("_ |- _ [::] _" [51,51,51]50)
    1.28 +  wt_stmt :: "'c env =>  stmt                => bool" ("_ |- _ [ok]"   [51,51   ]50)
    1.29  
    1.30  
    1.31  translations
    1.32 @@ -134,9 +134,9 @@
    1.33           E\<turnstile>NewC C::Class C"  -- "cf. 15.8"
    1.34  
    1.35    -- "cf. 15.15"
    1.36 -  Cast: "[| E\<turnstile>e::Class C; is_class (prg E) D;
    1.37 -            prg E\<turnstile>C\<preceq>? D |] ==>
    1.38 -         E\<turnstile>Cast D e::Class D"
    1.39 +  Cast: "[| E\<turnstile>e::C; is_class (prg E) D;
    1.40 +            prg E\<turnstile>C\<preceq>? Class D |] ==>
    1.41 +         E\<turnstile>Cast D e:: Class D"
    1.42  
    1.43    -- "cf. 15.7.1"
    1.44    Lit:    "[| typeof (\<lambda>v. None) x = Some T |] ==>
    1.45 @@ -213,7 +213,7 @@
    1.46  
    1.47  constdefs
    1.48  
    1.49 - wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
    1.50 + wf_java_mdecl :: "'c prog => cname => java_mb mdecl => bool"
    1.51  "wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
    1.52    length pTs = length pns \<and>
    1.53    distinct pns \<and>
    1.54 @@ -225,25 +225,22 @@
    1.55     E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
    1.56  
    1.57  syntax 
    1.58 - wf_java_prog :: "java_mb prog => bool"
    1.59 + wf_java_prog :: "'c prog => bool"
    1.60  translations
    1.61    "wf_java_prog" == "wf_prog wf_java_mdecl"
    1.62  
    1.63  lemma wf_java_prog_wf_java_mdecl: "\<lbrakk> 
    1.64    wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths \<rbrakk>
    1.65    \<Longrightarrow> wf_java_mdecl G C jmdcl"
    1.66 -apply (simp add: wf_prog_def) 
    1.67 -apply (simp add: wf_cdecl_def)
    1.68 +apply (simp only: wf_prog_def) 
    1.69  apply (erule conjE)+
    1.70  apply (drule bspec, assumption)
    1.71 -apply simp
    1.72 -apply (erule conjE)+
    1.73 -apply (drule bspec, assumption)
    1.74 -apply (simp add: wf_mdecl_def split_beta)
    1.75 +apply (simp add: wf_cdecl_mdecl_def split_beta)
    1.76  done
    1.77  
    1.78 -lemma wt_is_type: "(E\<turnstile>e::T \<longrightarrow> wf_prog wf_mb (prg E) \<longrightarrow> is_type (prg E) T) \<and>  
    1.79 -       (E\<turnstile>es[::]Ts \<longrightarrow> wf_prog wf_mb (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and> 
    1.80 +
    1.81 +lemma wt_is_type: "(E\<turnstile>e::T \<longrightarrow> ws_prog (prg E) \<longrightarrow> is_type (prg E) T) \<and>  
    1.82 +       (E\<turnstile>es[::]Ts \<longrightarrow> ws_prog (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and> 
    1.83         (E\<turnstile>c \<surd> \<longrightarrow> True)"
    1.84  apply (rule ty_expr_ty_exprs_wt_stmt.induct)
    1.85  apply auto
    1.86 @@ -253,10 +250,15 @@
    1.87  apply ( drule (1) fields_is_type)
    1.88  apply (  simp (no_asm_simp))
    1.89  apply  (assumption)
    1.90 -apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI 
    1.91 +apply (auto dest!: max_spec2mheads method_wf_mhead is_type_rTI 
    1.92              simp add: wf_mdecl_def)
    1.93  done
    1.94  
    1.95  lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, rule_format]
    1.96  
    1.97 +lemma expr_class_is_class: "
    1.98 +  \<lbrakk>ws_prog (prg E); E \<turnstile> e :: Class C\<rbrakk> \<Longrightarrow> is_class (prg E) C"
    1.99 +  by (frule ty_expr_is_type, assumption, simp)
   1.100 +
   1.101 +
   1.102  end