author  wenzelm 
Thu, 11 Feb 2010 00:45:02 +0100  
changeset 35102  cc7a0b9f938c 
parent 31166  a90fe83f58ea 
child 35416  d8d7d1b785af 
permissions  rwrr 
11376  1 
(* Title: HOL/NanoJava/TypeRel.thy 
2 
ID: $Id$ 

3 
Author: David von Oheimb 

4 
Copyright 2001 Technische Universitaet Muenchen 

5 
*) 

6 

7 
header "Type relations" 

8 

16417  9 
theory TypeRel imports Decl begin 
11376  10 

11 
consts 

11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11376
diff
changeset

12 
subcls1 :: "(cname \<times> cname) set" {* subclass *} 
11376  13 

35102  14 
abbreviation 
15 
subcls1_syntax :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70) 

16 
where "C <=C1 D == (C,D) \<in> subcls1" 

17 
abbreviation 

18 
subcls_syntax :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70) 

19 
where "C <=C D == (C,D) \<in> subcls1^*" 

11376  20 

35102  21 
notation (xsymbols) 
22 
subcls1_syntax ("_ \<prec>C1 _" [71,71] 70) and 

23 
subcls_syntax ("_ \<preceq>C _" [71,71] 70) 

11376  24 

25 
consts 

14134  26 
method :: "cname => (mname \<rightharpoonup> methd)" 
27 
field :: "cname => (fname \<rightharpoonup> ty)" 

11376  28 

29 

11565  30 
subsection "Declarations and properties not used in the meta theory" 
11376  31 

11565  32 
text{* Direct subclass relation *} 
11376  33 
defs 
34 
subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}" 

11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11376
diff
changeset

35 

11565  36 
text{* Widening, viz. method invocation conversion *} 
23755  37 
inductive 
38 
widen :: "ty => ty => bool" ("_ \<preceq> _" [71,71] 70) 

39 
where 

40 
refl [intro!, simp]: "T \<preceq> T" 

41 
 subcls: "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D" 

42 
 null [intro!]: "NT \<preceq> R" 

11376  43 

44 
lemma subcls1D: 

45 
"C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)" 

46 
apply (unfold subcls1_def) 

47 
apply auto 

48 
done 

49 

50 
lemma subcls1I: "\<lbrakk>class C = Some m; super m = D; C \<noteq> Object\<rbrakk> \<Longrightarrow> C\<prec>C1D" 

51 
apply (unfold subcls1_def) 

52 
apply auto 

53 
done 

54 

55 
lemma subcls1_def2: 

14952
47455995693d
removal of xsymbol syntax <Sigma> for dependent products
paulson
parents:
14171
diff
changeset

56 
"subcls1 = 
47455995693d
removal of xsymbol syntax <Sigma> for dependent products
paulson
parents:
14171
diff
changeset

57 
(SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})" 
11376  58 
apply (unfold subcls1_def is_class_def) 
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
28524
diff
changeset

59 
apply (auto split:split_if_asm) 
11376  60 
done 
61 

62 
lemma finite_subcls1: "finite subcls1" 

63 
apply(subst subcls1_def2) 

64 
apply(rule finite_SigmaI [OF finite_is_class]) 

65 
apply(rule_tac B = "{super (the (class C))}" in finite_subset) 

66 
apply auto 

67 
done 

68 

69 
constdefs 

70 

71 
ws_prog :: "bool" 

72 
"ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow> 

73 
is_class (super c) \<and> (super c,C)\<notin>subcls1^+" 

74 

75 
lemma ws_progD: "\<lbrakk>class C = Some c; C\<noteq>Object; ws_prog\<rbrakk> \<Longrightarrow> 

76 
is_class (super c) \<and> (super c,C)\<notin>subcls1^+" 

77 
apply (unfold ws_prog_def class_def) 

78 
apply (drule_tac map_of_SomeD) 

79 
apply auto 

80 
done 

81 

82 
lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^1 \<inter> subcls1^+ = {}" 

83 
by (fast dest: subcls1D ws_progD) 

84 

13867  85 
(* irrefl_tranclI in Transitive_Closure.thy is more general *) 
11376  86 
lemma irrefl_tranclI': "r^1 Int r^+ = {} ==> !x. (x, x) ~: r^+" 
13867  87 
by(blast elim: tranclE dest: trancl_into_rtrancl) 
88 

11376  89 

90 
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI'] 

91 

92 
lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y" 

93 
apply (rule irrefl_trancl_rD) 

94 
apply (rule subcls1_irrefl_lemma2) 

95 
apply auto 

96 
done 

97 

98 
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard] 

99 

100 
lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)" 

101 
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic) 

102 

103 

14134  104 
consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<rightharpoonup> 'b)" 
11376  105 

11626  106 
recdef (permissive) class_rec "subcls1\<inverse>" 
28524  107 
"class_rec C = (\<lambda>f. case class C of None \<Rightarrow> undefined 
11376  108 
 Some m \<Rightarrow> if wf (subcls1\<inverse>) 
109 
then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m) 

28524  110 
else undefined)" 
11376  111 
(hints intro: subcls1I) 
112 

113 
lemma class_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> 

114 
class_rec C f = (if C = Object then empty else class_rec (super m) f) ++ 

115 
map_of (f m)"; 

116 
apply (drule wf_subcls1) 

117 
apply (rule class_rec.simps [THEN trans [THEN fun_cong]]) 

118 
apply assumption 

119 
apply simp 

120 
done 

121 

11565  122 
{* Methods of a class, with inheritance and hiding *} 
11376  123 
defs method_def: "method C \<equiv> class_rec C methods" 
124 

125 
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> 

126 
method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)" 

127 
apply (unfold method_def) 

128 
apply (erule (1) class_rec [THEN trans]); 

129 
apply simp 

130 
done 

131 

132 

11565  133 
{* Fields of a class, with inheritance and hiding *} 
12264
9c356e2da72f
renamed "fields" to "flds" (avoid clash with new "fields" operation);
wenzelm
parents:
11626
diff
changeset

134 
defs field_def: "field C \<equiv> class_rec C flds" 
11376  135 

12264
9c356e2da72f
renamed "fields" to "flds" (avoid clash with new "fields" operation);
wenzelm
parents:
11626
diff
changeset

136 
lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow> 
9c356e2da72f
renamed "fields" to "flds" (avoid clash with new "fields" operation);
wenzelm
parents:
11626
diff
changeset

137 
field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)" 
11376  138 
apply (unfold field_def) 
139 
apply (erule (1) class_rec [THEN trans]); 

140 
apply simp 

141 
done 

142 

143 
end 