author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45970  b6d0cff57d96 
child 53374  a14d2a854c02 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/TypeRel.thy 
41589  2 
Author: David von Oheimb, Technische Universitaet Muenchen 
11070  3 
*) 
8011  4 

12911  5 
header {* \isaheader{Relations between Java Types} *} 
8011  6 

45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

7 
theory TypeRel 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

8 
imports Decl "~~/src/HOL/Library/Wfrec" 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

9 
begin 
8011  10 

22271  11 
 "direct subclass, cf. 8.1.3" 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

12 

1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

13 
inductive_set 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

14 
subcls1 :: "'c prog => (cname \<times> cname) set" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

15 
and subcls1' :: "'c prog => cname \<Rightarrow> cname => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70) 
22271  16 
for G :: "'c prog" 
17 
where 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

18 
"G \<turnstile> C \<prec>C1 D \<equiv> (C, D) \<in> subcls1 G" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

19 
 subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G \<turnstile> C \<prec>C1 D" 
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

20 

22271  21 
abbreviation 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

22 
subcls :: "'c prog => cname \<Rightarrow> cname => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70) 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

23 
where "G \<turnstile> C \<preceq>C D \<equiv> (C, D) \<in> (subcls1 G)^*" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

24 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

25 
lemma subcls1D: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

26 
"G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))" 
22271  27 
apply (erule subcls1.cases) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

28 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

29 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

30 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

31 
lemma subcls1_def2: 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

32 
"subcls1 P = 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

33 
(SIGMA C:{C. is_class P C}. {D. C\<noteq>Object \<and> fst (the (class P C))=D})" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

34 
by (auto simp add: is_class_def dest: subcls1D intro: subcls1I) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

35 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

36 
lemma finite_subcls1: "finite (subcls1 G)" 
23757  37 
apply(simp add: subcls1_def2 del: mem_Sigma_iff) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

38 
apply(rule finite_SigmaI [OF finite_is_class]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

39 
apply(rule_tac B = "{fst (the (class G C))}" in finite_subset) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

40 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

41 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

42 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

43 
lemma subcls_is_class: "(C, D) \<in> (subcls1 G)^+ ==> is_class G C" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

44 
apply (unfold is_class_def) 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

45 
apply(erule trancl_trans_induct) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

46 
apply (auto dest!: subcls1D) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

47 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

48 

11266  49 
lemma subcls_is_class2 [rule_format (no_asm)]: 
50 
"G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

51 
apply (unfold is_class_def) 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

52 
apply (erule rtrancl_induct) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

53 
apply (drule_tac [2] subcls1D) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

54 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

55 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

56 

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

57 
definition class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow> 
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset

58 
(cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" where 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

59 
"class_rec G == wfrec ((subcls1 G)^1) 
13090
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

60 
(\<lambda>r C t f. case class G C of 
28524  61 
None \<Rightarrow> undefined 
13090
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

62 
 Some (D,fs,ms) \<Rightarrow> 
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

63 
f C fs ms (if C = Object then t else r D t f))" 
11284  64 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

65 
lemma class_rec_lemma: 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

66 
assumes wf: "wf ((subcls1 G)^1)" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

67 
and cls: "class G C = Some (D, fs, ms)" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

68 
shows "class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

69 
proof  
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

70 
from wf have step: "\<And>H a. wfrec ((subcls1 G)\<inverse>) H a = 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

71 
H (cut (wfrec ((subcls1 G)\<inverse>) H) ((subcls1 G)\<inverse>) a) a" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

72 
by (rule wfrec) 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

73 
have cut: "\<And>f. C \<noteq> Object \<Longrightarrow> cut f ((subcls1 G)\<inverse>) C D = f D" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

74 
by (rule cut_apply [where r="(subcls1 G)^1", simplified, OF subcls1I, OF cls]) 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

75 
from cls show ?thesis by (simp add: step cut class_rec_def) 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

76 
qed 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

77 

20970  78 
definition 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

79 
"wf_class G = wf ((subcls1 G)^1)" 
20970  80 

81 

44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

82 

322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

83 
text {* Code generator setup *} 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

84 

322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

85 
code_pred 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

86 
(modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

87 
subcls1p 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

88 
. 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

89 

b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

90 
declare subcls1_def [code_pred_def] 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

91 

44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

92 
code_pred 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

93 
(modes: i \<Rightarrow> i \<times> o \<Rightarrow> bool, i \<Rightarrow> i \<times> i \<Rightarrow> bool) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

94 
[inductify] 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

95 
subcls1 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

96 
. 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

97 

322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

98 
definition subcls' where "subcls' G = (subcls1p G)^**" 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

99 

44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

100 
code_pred 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

101 
(modes: i \<Rightarrow> i \<Rightarrow> i \<Rightarrow> bool, i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

102 
[inductify] 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

103 
subcls' 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

104 
. 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

105 

45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44035
diff
changeset

106 
lemma subcls_conv_subcls' [code_unfold]: 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

107 
"(subcls1 G)^* = {(C, D). subcls' G C D}" 
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

108 
by(simp add: subcls'_def subcls1_def rtrancl_def) 
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

109 

322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

110 
lemma class_rec_code [code]: 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

111 
"class_rec G C t f = 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

112 
(if wf_class G then 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

113 
(case class G C of 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

114 
None \<Rightarrow> class_rec G C t f 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

115 
 Some (D, fs, ms) \<Rightarrow> 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

116 
if C = Object then f Object fs ms t else f C fs ms (class_rec G D t f)) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

117 
else class_rec G C t f)" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

118 
apply(cases "wf_class G") 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

119 
apply(unfold class_rec_def wf_class_def) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

120 
apply(subst wfrec, assumption) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

121 
apply(cases "class G C") 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

122 
apply(simp add: wfrec) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

123 
apply clarsimp 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

124 
apply(rename_tac D fs ms) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

125 
apply(rule_tac f="f C fs ms" in arg_cong) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

126 
apply(clarsimp simp add: cut_def) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

127 
apply(blast intro: subcls1I) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

128 
apply simp 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

129 
done 
32461
eee4fa79398f
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
krauss
parents:
28562
diff
changeset

130 

44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

131 
lemma wf_class_code [code]: 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

132 
"wf_class G \<longleftrightarrow> (\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C)" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

133 
proof 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

134 
assume "wf_class G" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

135 
hence wf: "wf (((subcls1 G)^+)^1)" unfolding wf_class_def by(rule wf_converse_trancl) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

136 
hence acyc: "acyclic ((subcls1 G)^+)" by(auto dest: wf_acyclic) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

137 
show "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

138 
proof(safe) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

139 
fix C D fs ms 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

140 
assume "(C, D, fs, ms) \<in> set G" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

141 
and "C \<noteq> Object" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

142 
and subcls: "G \<turnstile> fst (the (class G C)) \<preceq>C C" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

143 
from `(C, D, fs, ms) \<in> set G` obtain D' fs' ms' 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

144 
where "class": "class G C = Some (D', fs', ms')" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

145 
unfolding class_def by(auto dest!: weak_map_of_SomeI) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

146 
hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` .. 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

147 
hence "(C, D') \<in> (subcls1 G)^+" .. 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

148 
also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

149 
with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

150 
finally show False using acyc by(auto simp add: acyclic_def) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

151 
qed 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

152 
next 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

153 
assume rhs[rule_format]: "\<forall>(C, rest) \<in> set G. C \<noteq> Object \<longrightarrow> \<not> G \<turnstile> fst (the (class G C)) \<preceq>C C" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

154 
have "acyclic (subcls1 G)" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

155 
proof(intro acyclicI strip notI) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

156 
fix C 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

157 
assume "(C, C) \<in> (subcls1 G)\<^sup>+" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

158 
thus False 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

159 
proof(cases) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

160 
case base 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

161 
then obtain rest where "class G C = Some (C, rest)" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

162 
and "C \<noteq> Object" by cases 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

163 
from `class G C = Some (C, rest)` have "(C, C, rest) \<in> set G" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

164 
unfolding class_def by(rule map_of_SomeD) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

165 
with `C \<noteq> Object` `class G C = Some (C, rest)` 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

166 
have "\<not> G \<turnstile> C \<preceq>C C" by(auto dest: rhs) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

167 
thus False by simp 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

168 
next 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

169 
case (step D) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

170 
from `G \<turnstile> D \<prec>C1 C` obtain rest where "class G D = Some (C, rest)" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

171 
and "D \<noteq> Object" by cases 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

172 
from `class G D = Some (C, rest)` have "(D, C, rest) \<in> set G" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

173 
unfolding class_def by(rule map_of_SomeD) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

174 
with `D \<noteq> Object` `class G D = Some (C, rest)` 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

175 
have "\<not> G \<turnstile> C \<preceq>C D" by(auto dest: rhs) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

176 
moreover from `(C, D) \<in> (subcls1 G)\<^sup>+` 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

177 
have "G \<turnstile> C \<preceq>C D" by(rule trancl_into_rtrancl) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

178 
ultimately show False by contradiction 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

179 
qed 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

180 
qed 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

181 
thus "wf_class G" unfolding wf_class_def 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

182 
by(rule finite_acyclic_wf_converse[OF finite_subcls1]) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

183 
qed 
32461
eee4fa79398f
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
krauss
parents:
28562
diff
changeset

184 

8011  185 
consts 
14134  186 
method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *) 
187 
field :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty )" (* ###curry *) 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

188 
fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *) 
8011  189 

12517  190 
 "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6" 
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

191 
defs method_def [code]: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts. 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

192 
ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

193 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

194 
lemma method_rec_lemma: "[class G C = Some (D,fs,ms); wf ((subcls1 G)^1)] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

195 
method (G,C) = (if C = Object then empty else method (G,D)) ++ 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

196 
map_of (map (\<lambda>(s,m). (s,(C,m))) ms)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

197 
apply (unfold method_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

198 
apply (simp split del: split_if) 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

199 
apply (erule (1) class_rec_lemma [THEN trans]) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

200 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

201 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

202 

8011  203 

12517  204 
 "list of fields of a class, including inherited and hidden ones" 
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

205 
defs fields_def [code]: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts. 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

206 
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

207 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32461
diff
changeset

208 
lemma fields_rec_lemma: "[class G C = Some (D,fs,ms); wf ((subcls1 G)^1)] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

209 
fields (G,C) = 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

210 
map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

211 
apply (unfold fields_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

212 
apply (simp split del: split_if) 
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
45231
diff
changeset

213 
apply (erule (1) class_rec_lemma [THEN trans]) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

214 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

215 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

216 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

217 

44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

218 
defs field_def [code]: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

219 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

220 
lemma field_fields: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

221 
"field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

222 
apply (unfold field_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

223 
apply (rule table_of_remap_SomeD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

224 
apply simp 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

225 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

226 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

227 

12517  228 
 "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping" 
23757  229 
inductive 
22271  230 
widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70) 
231 
for G :: "'c prog" 

232 
where 

12517  233 
refl [intro!, simp]: "G\<turnstile> T \<preceq> T"  "identity conv., cf. 5.1.1" 
22271  234 
 subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D" 
235 
 null [intro!]: "G\<turnstile> NT \<preceq> RefT R" 

8011  236 

44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

237 
code_pred widen . 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
44014
diff
changeset

238 

22597  239 
lemmas refl = HOL.refl 
240 

12517  241 
 "casting conversion, cf. 5.5 / 5.1.5" 
242 
 "left out casts on primitve types" 

23757  243 
inductive 
22271  244 
cast :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70) 
245 
for G :: "'c prog" 

246 
where 

14045  247 
widen: "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D" 
22271  248 
 subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

249 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

250 
lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

251 
apply (rule iffI) 
22271  252 
apply (erule widen.cases) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

253 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

254 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

255 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

256 
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t" 
23757  257 
apply (ind_cases "G\<turnstile>RefT R\<preceq>T") 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

258 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

259 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

260 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

261 
lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t" 
23757  262 
apply (ind_cases "G\<turnstile>S\<preceq>RefT R") 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

263 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

264 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

265 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

266 
lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D" 
23757  267 
apply (ind_cases "G\<turnstile>Class C\<preceq>T") 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

268 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

269 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

270 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

271 
lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

272 
apply (rule iffI) 
23757  273 
apply (ind_cases "G\<turnstile>Class C\<preceq>NT") 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

274 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

275 
done 
8011  276 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

277 
lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

278 
apply (rule iffI) 
23757  279 
apply (ind_cases "G\<turnstile>Class C \<preceq> Class D") 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

280 
apply (auto elim: widen.subcls) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

281 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

282 

14045  283 
lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D" 
23757  284 
by (ind_cases "G \<turnstile> T \<preceq> NT", auto) 
14045  285 

286 
lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False" 

287 
apply (rule iffI) 

22271  288 
apply (erule cast.cases) 
14045  289 
apply auto 
290 
done 

291 

292 
lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT" 

293 
apply (erule cast.cases) 

294 
apply simp apply (erule widen.cases) 

295 
apply auto 

296 
done 

297 

12517  298 
theorem widen_trans[trans]: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

299 
proof  
12517  300 
assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" 
11987  301 
proof induct 
12517  302 
case (refl T T') thus "G\<turnstile>T\<preceq>T'" . 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

303 
next 
11987  304 
case (subcls C D T) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

305 
then obtain E where "T = Class E" by (blast dest: widen_Class) 
22271  306 
with subcls show "G\<turnstile>Class C\<preceq>T" by auto 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

307 
next 
11987  308 
case (null R RT) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

309 
then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

310 
thus "G\<turnstile>NT\<preceq>RT" by auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

311 
qed 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

312 
qed 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

313 

8011  314 
end 