author  oheimb 
Thu, 01 Feb 2001 20:53:13 +0100  
changeset 11026  a50365d21144 
parent 10613  78b1d6c3ee9c 
child 11070  cc421547e744 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/TypeRel.thy 
2 
ID: $Id$ 

3 
Author: David von Oheimb 

4 
Copyright 1999 Technische Universitaet Muenchen 

5 

6 
The relations between Java types 

7 
*) 

8 

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

9 
theory TypeRel = Decl: 
8011  10 

11 
consts 

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

12 
subcls1 :: "'c prog => (cname \<times> cname) set" (* subclass *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

13 
widen :: "'c prog => (ty \<times> ty ) set" (* widening *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

14 
cast :: "'c prog => (cname \<times> cname) set" (* casting *) 
8011  15 

16 
syntax 

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

17 
subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

18 
subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

19 
widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

20 
cast :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70) 
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

21 

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

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

23 
subcls1 :: "'c prog => [cname, cname] => bool" ("_  _ <=C1 _" [71,71,71] 70) 
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

24 
subcls :: "'c prog => [cname, cname] => bool" ("_  _ <=C _" [71,71,71] 70) 
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

25 
widen :: "'c prog => [ty , ty ] => bool" ("_  _ <= _" [71,71,71] 70) 
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

26 
cast :: "'c prog => [cname, cname] => bool" ("_  _ <=? _" [71,71,71] 70) 
8011  27 

28 
translations 

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

29 
"G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

30 
"G\<turnstile>C \<preceq>C D" == "(C,D) \<in> (subcls1 G)^*" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

31 
"G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

32 
"G\<turnstile>C \<preceq>? D" == "(C,D) \<in> cast G" 
8011  33 

34 
defs 

35 

36 
(* direct subclass, cf. 8.1.3 *) 

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

37 
subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class G C=Some c \<and> fst c=D)}" 
8011  38 

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

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

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

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

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

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

44 

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

45 
lemma subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

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

49 

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

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

51 
"subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

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

55 

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

56 
lemma finite_subcls1: "finite (subcls1 G)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

57 
apply(subst subcls1_def2) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

59 
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

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

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

62 

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

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

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

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

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

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

68 

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

69 
lemma subcls_is_class2 [rule_format (no_asm)]: "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

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

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

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

75 

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

76 
consts class_rec ::"'c prog \<times> cname \<Rightarrow> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

77 
'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

78 
recdef class_rec "same_fst (\<lambda>G. wf ((subcls1 G)^1)) (\<lambda>G. (subcls1 G)^1)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

79 
"class_rec (G,C) = (\<lambda>t f. case class G C of None \<Rightarrow> arbitrary 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

80 
 Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^1) then 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

81 
f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

84 
apply (auto intro: subcls1I) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

86 

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

87 
lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

88 
class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)"; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

89 
apply (rule class_rec_tc [THEN class_rec.simps 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

90 
[THEN trans [THEN fun_cong [THEN fun_cong]]]]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

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

94 

8011  95 
consts 
96 

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

97 
method :: "'c prog \<times> cname => ( sig \<leadsto> cname \<times> ty \<times> 'c)" (* ###curry *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

98 
field :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty )" (* ###curry *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

101 
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *) 

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

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

103 
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

104 

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

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

106 
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

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

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

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

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

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

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

113 

8011  114 

115 
(* list of fields of a class, including inherited and hidden ones *) 

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

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

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

118 

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

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

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

121 
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

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

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

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

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

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

127 

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

128 

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

129 
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

130 

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

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

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

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

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

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

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

137 

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

138 

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

139 
inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

140 
i.e. sort of syntactic subtyping *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

141 
refl [intro!, simp]: "G\<turnstile> T \<preceq> T" (* identity conv., cf. 5.1.1 *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

142 
subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

143 
null [intro!]: "G\<turnstile> NT \<preceq> RefT R" 
8011  144 

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

145 
inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

146 
(* left out casts on primitve types *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

147 
widen: "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

148 
subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

149 

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

150 
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

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

152 
apply (erule widen.elims) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

155 

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

156 
lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

157 
apply (ind_cases "G\<turnstile>S\<preceq>T") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

160 

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

161 
lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

162 
apply (ind_cases "G\<turnstile>S\<preceq>T") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

165 

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

166 
lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

167 
apply (ind_cases "G\<turnstile>S\<preceq>T") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

170 

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

171 
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

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

173 
apply (ind_cases "G\<turnstile>S\<preceq>T") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

175 
done 
8011  176 

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

177 
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

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

179 
apply (ind_cases "G\<turnstile>S\<preceq>T") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

180 
apply (auto elim: widen.subcls) 
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_trans [rule_format (no_asm)]: "G\<turnstile>S\<preceq>U ==> \<forall>T. G\<turnstile>U\<preceq>T > G\<turnstile>S\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

184 
apply (erule widen.induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

186 
apply (frule widen_Class) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

187 
apply (frule_tac [2] widen_RefT) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

189 
apply(erule (1) rtrancl_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

191 

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

192 
ML {* InductAttrib.print_global_rules(the_context()) *} 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

193 
ML {* set show_tags *} 
8011  194 

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

195 
(*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

197 
assume "G\<turnstile>S\<preceq>U" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

198 
thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

199 
proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

201 
fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'". 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

202 
(* fix T' show "PROP ?P T T".*) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

205 
fix T assume "G\<turnstile>Class D\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

206 
then obtain E where "T = Class E" by (blast dest: widen_Class) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

207 
from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

210 
fix RT assume "G\<turnstile>RefT R\<preceq>RT" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

211 
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

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

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

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

215 
*) 
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 
theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

219 
assume "G\<turnstile>S\<preceq>U" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

220 
thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

221 
proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

223 
fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'". 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

224 
(* fix T' show "PROP ?P T T".*) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

227 
fix T assume "G\<turnstile>Class D\<preceq>T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

228 
then obtain E where "T = Class E" by (blast dest: widen_Class) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

229 
from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

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

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

232 
fix RT assume "G\<turnstile>RefT R\<preceq>RT" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10613
diff
changeset

233 
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

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

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

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

237 

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

238 

8011  239 

240 
end 