src/HOL/NanoJava/TypeRel.thy
changeset 11376 bf98ad1c22c6
child 11558 6539627881e8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Sat Jun 16 20:06:42 2001 +0200
     1.3 @@ -0,0 +1,145 @@
     1.4 +(*  Title:      HOL/NanoJava/TypeRel.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   2001 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +
    1.10 +header "Type relations"
    1.11 +
    1.12 +theory TypeRel = Decl:
    1.13 +
    1.14 +consts
    1.15 +  widen   :: "(ty    \<times> ty   ) set"  (* widening *)
    1.16 +  subcls1 :: "(cname \<times> cname) set"  (* subclass *)
    1.17 +
    1.18 +syntax (xsymbols)
    1.19 +  widen   :: "[ty   , ty   ] => bool" ("_ \<preceq> _"    [71,71] 70)
    1.20 +  subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _"  [71,71] 70)
    1.21 +  subcls  :: "[cname, cname] => bool" ("_ \<preceq>C _"   [71,71] 70)
    1.22 +syntax
    1.23 +  widen   :: "[ty   , ty   ] => bool" ("_ <= _"   [71,71] 70)
    1.24 +  subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
    1.25 +  subcls  :: "[cname, cname] => bool" ("_ <=C _"  [71,71] 70)
    1.26 +
    1.27 +translations
    1.28 +  "C \<prec>C1 D" == "(C,D) \<in> subcls1"
    1.29 +  "C \<preceq>C  D" == "(C,D) \<in> subcls1^*"
    1.30 +  "S \<preceq>   T" == "(S,T) \<in> widen"
    1.31 +
    1.32 +consts
    1.33 +  method :: "cname => (mname \<leadsto> methd)"
    1.34 +  field  :: "cname => (vnam  \<leadsto> ty)"
    1.35 +
    1.36 +
    1.37 +text {* The rest of this theory is not actually used. *}
    1.38 +
    1.39 +defs
    1.40 +  (* direct subclass relation *)
    1.41 + subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
    1.42 +  
    1.43 +inductive widen intros (*widening, viz. method invocation conversion,
    1.44 +			           i.e. sort of syntactic subtyping *)
    1.45 +  refl   [intro!, simp]:           "T \<preceq> T"
    1.46 +  subcls         : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
    1.47 +  null   [intro!]:                "NT \<preceq> R"
    1.48 +
    1.49 +lemma subcls1D: 
    1.50 +  "C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)"
    1.51 +apply (unfold subcls1_def)
    1.52 +apply auto
    1.53 +done
    1.54 +
    1.55 +lemma subcls1I: "\<lbrakk>class C = Some m; super m = D; C \<noteq> Object\<rbrakk> \<Longrightarrow> C\<prec>C1D"
    1.56 +apply (unfold subcls1_def)
    1.57 +apply auto
    1.58 +done
    1.59 +
    1.60 +lemma subcls1_def2: 
    1.61 +"subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
    1.62 +apply (unfold subcls1_def is_class_def)
    1.63 +apply auto
    1.64 +done
    1.65 +
    1.66 +lemma finite_subcls1: "finite subcls1"
    1.67 +apply(subst subcls1_def2)
    1.68 +apply(rule finite_SigmaI [OF finite_is_class])
    1.69 +apply(rule_tac B = "{super (the (class C))}" in finite_subset)
    1.70 +apply  auto
    1.71 +done
    1.72 +
    1.73 +constdefs
    1.74 +
    1.75 +  ws_prog  :: "bool"
    1.76 + "ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow> 
    1.77 +                              is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
    1.78 +
    1.79 +lemma ws_progD: "\<lbrakk>class C = Some c; C\<noteq>Object; ws_prog\<rbrakk> \<Longrightarrow>  
    1.80 +  is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
    1.81 +apply (unfold ws_prog_def class_def)
    1.82 +apply (drule_tac map_of_SomeD)
    1.83 +apply auto
    1.84 +done
    1.85 +
    1.86 +lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}"
    1.87 +by (fast dest: subcls1D ws_progD)
    1.88 +
    1.89 +(* context (theory "Transitive_Closure") *)
    1.90 +lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
    1.91 +apply (rule allI)
    1.92 +apply (erule irrefl_tranclI)
    1.93 +done
    1.94 +
    1.95 +lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
    1.96 +
    1.97 +lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y"
    1.98 +apply (rule irrefl_trancl_rD)
    1.99 +apply (rule subcls1_irrefl_lemma2)
   1.100 +apply auto
   1.101 +done
   1.102 +
   1.103 +lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
   1.104 +
   1.105 +lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)"
   1.106 +by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
   1.107 +
   1.108 +
   1.109 +consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
   1.110 +
   1.111 +recdef class_rec "subcls1\<inverse>"
   1.112 +      "class_rec C = (\<lambda>f. case class C of None   \<Rightarrow> arbitrary 
   1.113 +                                        | Some m \<Rightarrow> if wf (subcls1\<inverse>) 
   1.114 +       then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
   1.115 +       else arbitrary)"
   1.116 +(hints intro: subcls1I)
   1.117 +
   1.118 +lemma class_rec: "\<lbrakk>class C = Some m;  ws_prog\<rbrakk> \<Longrightarrow>
   1.119 + class_rec C f = (if C = Object then empty else class_rec (super m) f) ++ 
   1.120 +                 map_of (f m)";
   1.121 +apply (drule wf_subcls1)
   1.122 +apply (rule class_rec.simps [THEN trans [THEN fun_cong]])
   1.123 +apply  assumption
   1.124 +apply simp
   1.125 +done
   1.126 +
   1.127 +(* methods of a class, with inheritance and hiding *)
   1.128 +defs method_def: "method C \<equiv> class_rec C methods"
   1.129 +
   1.130 +lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
   1.131 +method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
   1.132 +apply (unfold method_def)
   1.133 +apply (erule (1) class_rec [THEN trans]);
   1.134 +apply simp
   1.135 +done
   1.136 +
   1.137 +
   1.138 +(* fields of a class, with inheritance and hiding *)
   1.139 +defs field_def: "field C \<equiv> class_rec C fields"
   1.140 +
   1.141 +lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
   1.142 +field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)"
   1.143 +apply (unfold field_def)
   1.144 +apply (erule (1) class_rec [THEN trans]);
   1.145 +apply simp
   1.146 +done
   1.147 +
   1.148 +end