author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45605  a89b4bc311a5 
child 55017  2df6ad1dbd66 
permissions  rwrr 
11376  1 
(* Title: HOL/NanoJava/TypeRel.thy 
41589  2 
Author: David von Oheimb, Technische Universitaet Muenchen 
11376  3 
*) 
4 

5 
header "Type relations" 

6 

44146  7 
theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin 
11376  8 

44375  9 
text{* Direct subclass relation *} 
10 

11 
definition subcls1 :: "(cname \<times> cname) set" 

12 
where 

13 
"subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}" 

11376  14 

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

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

18 
abbreviation 

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

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

11376  21 

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

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

11376  25 

26 

11565  27 
subsection "Declarations and properties not used in the meta theory" 
11376  28 

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

32 
where 

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

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

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

11376  36 

37 
lemma subcls1D: 

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

39 
apply (unfold subcls1_def) 

40 
apply auto 

41 
done 

42 

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

44 
apply (unfold subcls1_def) 

45 
apply auto 

46 
done 

47 

48 
lemma subcls1_def2: 

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

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

50 
(SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})" 
11376  51 
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

52 
apply (auto split:split_if_asm) 
11376  53 
done 
54 

55 
lemma finite_subcls1: "finite subcls1" 

56 
apply(subst subcls1_def2) 

57 
apply(rule finite_SigmaI [OF finite_is_class]) 

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

59 
apply auto 

60 
done 

61 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset

62 
definition ws_prog :: "bool" where 
11376  63 
"ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow> 
64 
is_class (super c) \<and> (super c,C)\<notin>subcls1^+" 

65 

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

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

68 
apply (unfold ws_prog_def class_def) 

69 
apply (drule_tac map_of_SomeD) 

70 
apply auto 

71 
done 

72 

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

74 
by (fast dest: subcls1D ws_progD) 

75 

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

11376  80 

81 
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI'] 

82 

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

84 
apply (rule irrefl_trancl_rD) 

85 
apply (rule subcls1_irrefl_lemma2) 

86 
apply auto 

87 
done 

88 

45605  89 
lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI] 
11376  90 

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

92 
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic) 

93 

44146  94 
definition class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<rightharpoonup> 'b)" 
95 
where 

96 
"class_rec \<equiv> wfrec (subcls1\<inverse>) (\<lambda>rec C f. 

97 
case class C of None \<Rightarrow> undefined 

98 
 Some m \<Rightarrow> (if C = Object then empty else rec (super m) f) ++ map_of (f m))" 

11376  99 

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

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

44146  102 
map_of (f m)" 
11376  103 
apply (drule wf_subcls1) 
44146  104 
apply (subst def_wfrec[OF class_rec_def], auto) 
105 
apply (subst cut_apply, auto intro: subcls1I) 

11376  106 
done 
107 

11565  108 
{* Methods of a class, with inheritance and hiding *} 
44375  109 
definition method :: "cname => (mname \<rightharpoonup> methd)" where 
110 
"method C \<equiv> class_rec C methods" 

11376  111 

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

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

114 
apply (unfold method_def) 

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

116 
apply simp 

117 
done 

118 

119 

11565  120 
{* Fields of a class, with inheritance and hiding *} 
44375  121 
definition field :: "cname => (fname \<rightharpoonup> ty)" where 
122 
"field C \<equiv> class_rec C flds" 

11376  123 

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

124 
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

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

128 
apply simp 

129 
done 

130 

131 
end 