author  berghofe 
Wed, 07 Feb 2007 17:44:07 +0100  
changeset 22271  51a80e238b29 
parent 20970  c2a342e548a9 
child 22597  284b2183d070 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/TypeRel.thy 
2 
ID: $Id$ 

3 
Author: David von Oheimb 

4 
Copyright 1999 Technische Universitaet Muenchen 

11070  5 
*) 
8011  6 

12911  7 
header {* \isaheader{Relations between Java Types} *} 
8011  8 

16417  9 
theory TypeRel imports Decl begin 
8011  10 

22271  11 
 "direct subclass, cf. 8.1.3" 
12 
inductive2 

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

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

16 
subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D" 

10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

17 

22271  18 
abbreviation 
19 
subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70) 

20 
where "G\<turnstile>C \<preceq>C D \<equiv> (subcls1 G)^** C D" 

8011  21 

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

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

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

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

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

27 

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

28 
lemma subcls1_def2: 
22271  29 
"subcls1 G = member2 
14952
47455995693d
removal of xsymbol syntax <Sigma> for dependent products
paulson
parents:
14171
diff
changeset

30 
(SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})" 
22271  31 
by (auto simp add: is_class_def expand_fun_eq dest: subcls1D intro: subcls1I) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

32 

22271  33 
lemma finite_subcls1: "finite (Collect2 (subcls1 G))" 
34 
apply(simp add: subcls1_def2) 

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

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

36 
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

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

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

39 

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

41 
apply (unfold is_class_def) 
22271  42 
apply(erule trancl_trans_induct') 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

45 

11266  46 
lemma subcls_is_class2 [rule_format (no_asm)]: 
47 
"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

48 
apply (unfold is_class_def) 
22271  49 
apply (erule rtrancl_induct') 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

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

53 

13090
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

54 
constdefs 
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

55 
class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow> 
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

56 
(cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" 
22271  57 
"class_rec G == wfrec (Collect2 ((subcls1 G)^1)) 
13090
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

58 
(\<lambda>r C t f. case class G C of 
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

59 
None \<Rightarrow> arbitrary 
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

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

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

22271  63 
lemma class_rec_lemma: "wfP ((subcls1 G)^1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow> 
13090
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

64 
class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)" 
22271  65 
by (simp add: class_rec_def wfrec [to_pred] 
66 
cut_apply [OF Collect2I [where P="(subcls1 G)^1"], OF conversepI, OF subcls1I]) 

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

67 

20970  68 
definition 
22271  69 
"wf_class G = wfP ((subcls1 G)^1)" 
20970  70 

71 
lemma class_rec_func [code func]: 

72 
"class_rec G C t f = (if wf_class G then 

73 
(case class G C 

74 
of None \<Rightarrow> arbitrary 

75 
 Some (D, fs, ms) \<Rightarrow> f C fs ms (if C = Object then t else class_rec G D t f)) 

76 
else class_rec G C t f)" 

77 
proof (cases "wf_class G") 

78 
case False then show ?thesis by auto 

79 
next 

80 
case True 

22271  81 
from `wf_class G` have wf: "wfP ((subcls1 G)^1)" 
20970  82 
unfolding wf_class_def . 
83 
show ?thesis 

84 
proof (cases "class G C") 

85 
case None 

86 
with wf show ?thesis 

22271  87 
by (simp add: class_rec_def wfrec [to_pred] 
88 
cut_apply [OF Collect2I [where P="(subcls1 G)^1"], OF conversepI, OF subcls1I]) 

20970  89 
next 
90 
case (Some x) show ?thesis 

91 
proof (cases x) 

92 
case (fields D fs ms) 

93 
then have is_some: "class G C = Some (D, fs, ms)" using Some by simp 

94 
note class_rec = class_rec_lemma [OF wf is_some] 

95 
show ?thesis unfolding class_rec by (simp add: is_some) 

96 
qed 

97 
qed 

98 
qed 

99 

8011  100 
consts 
101 

14134  102 
method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *) 
103 
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

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

12517  106 
 "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6" 
13090
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

107 
defs method_def: "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

108 
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

109 

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

111 
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

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

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

114 
apply (simp split del: split_if) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

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

118 

8011  119 

12517  120 
 "list of fields of a class, including inherited and hidden ones" 
13090
4fb7a2f2c1df
Improved definition of class_rec: no longer mixes algorithm and
berghofe
parents:
12911
diff
changeset

121 
defs fields_def: "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

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

123 

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

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

126 
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

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

128 
apply (simp split del: split_if) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

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

132 

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

133 

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

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

135 

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

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

137 
"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

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

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

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

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

142 

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

143 

12517  144 
 "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping" 
22271  145 
inductive2 
146 
widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70) 

147 
for G :: "'c prog" 

148 
where 

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

8011  152 

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

22271  155 
inductive2 
156 
cast :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70) 

157 
for G :: "'c prog" 

158 
where 

14045  159 
widen: "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D" 
22271  160 
 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

161 

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

162 
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

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

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

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

167 

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

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

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

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

172 

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

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

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

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

177 

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

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

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

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

182 

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

183 
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

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

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

187 
done 
8011  188 

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

189 
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

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

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

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

194 

14045  195 
lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D" 
22271  196 
by (ind_cases2 "G \<turnstile> T \<preceq> NT", auto) 
14045  197 

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

199 
apply (rule iffI) 

22271  200 
apply (erule cast.cases) 
14045  201 
apply auto 
202 
done 

203 

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

205 
apply (erule cast.cases) 

206 
apply simp apply (erule widen.cases) 

207 
apply auto 

208 
done 

209 

12517  210 
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

211 
proof  
12517  212 
assume "G\<turnstile>S\<preceq>U" thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" 
11987  213 
proof induct 
12517  214 
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

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

217 
then obtain E where "T = Class E" by (blast dest: widen_Class) 
22271  218 
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

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

221 
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

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

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

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

225 

8011  226 
end 