author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44042  2ff2a54d0fb5 
child 47394  a360406f1fcb 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/State.thy 
2 
Author: David von Oheimb 

3 
Copyright 1999 Technische Universitaet Muenchen 

11070  4 
*) 
8011  5 

12911  6 
header {* \isaheader{Program State} *} 
8011  7 

32356
e11cd88e6ade
temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents:
30235
diff
changeset

8 
theory State 
e11cd88e6ade
temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents:
30235
diff
changeset

9 
imports TypeRel Value 
e11cd88e6ade
temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents:
30235
diff
changeset

10 
begin 
8011  11 

42463  12 
type_synonym 
24783  13 
fields' = "(vname \<times> cname \<rightharpoonup> val)"  "field name, defining class, value" 
8011  14 

42463  15 
type_synonym 
24783  16 
obj = "cname \<times> fields'"  "class instance with class name and fields" 
8011  17 

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

18 
definition obj_ty :: "obj => ty" where 
10042  19 
"obj_ty obj == Class (fst obj)" 
8011  20 

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

21 
definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where 
12517  22 
"init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))" 
32356
e11cd88e6ade
temporary adjustment to dubious state of eta expansion in recfun_codegen
haftmann
parents:
30235
diff
changeset

23 

42463  24 
type_synonym aheap = "loc \<rightharpoonup> obj"  {* "@{text heap}" used in a translation below *} 
25 
type_synonym locals = "vname \<rightharpoonup> val"  "simple state, i.e. variable contents" 

8011  26 

42463  27 
type_synonym state = "aheap \<times> locals"  "heap, local parameter including This" 
28 
type_synonym xstate = "val option \<times> state"  "state including exception information" 

12517  29 

35102  30 
abbreviation (input) 
31 
heap :: "state => aheap" 

32 
where "heap == fst" 

33 

34 
abbreviation (input) 

35 
locals :: "state => locals" 

36 
where "locals == snd" 

37 

38 
abbreviation "Norm s == (None, s)" 

8011  39 

35102  40 
abbreviation (input) 
41 
abrupt :: "xstate \<Rightarrow> val option" 

42 
where "abrupt == fst" 

43 

44 
abbreviation (input) 

45 
store :: "xstate \<Rightarrow> state" 

46 
where "store == snd" 

47 

48 
abbreviation 

49 
lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj" 

50 
where "lookup_obj s a' == the (heap s (the_Addr a'))" 

13672  51 

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

52 
definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where 
13672  53 
"raise_if b x xo \<equiv> if b \<and> (xo = None) then Some (Addr (XcptRef x)) else xo" 
8011  54 

44042  55 
text {* Make @{text new_Addr} completely specified (at least for the code generator) *} 
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

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

57 
definition new_Addr :: "aheap => loc \<times> val option" where 
13672  58 
"new_Addr h \<equiv> SOME (a,x). (h a = None \<and> x = None)  x = Some (Addr (XcptRef OutOfMemory))" 
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

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

60 
consts nat_to_loc' :: "nat => loc'" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

61 
code_datatype nat_to_loc' 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

62 
definition new_Addr :: "aheap => loc \<times> val option" where 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

63 
"new_Addr h \<equiv> 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

64 
if \<exists>n. h (Loc (nat_to_loc' n)) = None 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

65 
then (Loc (nat_to_loc' (LEAST n. h (Loc (nat_to_loc' n)) = None)), None) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

66 
else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))" 
8011  67 

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

68 
definition np :: "val => val option => val option" where 
10042  69 
"np v == raise_if (v = Null) NullPointer" 
8011  70 

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

71 
definition c_hupd :: "aheap => xstate => xstate" where 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

72 
"c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))" 
8011  73 

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

74 
definition cast_ok :: "'c prog => cname => aheap => val => bool" where 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

75 
"cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

76 

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

77 
lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

78 
apply (unfold obj_ty_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

79 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

81 

13672  82 

83 
lemma new_AddrD: "new_Addr hp = (ref, xcp) \<Longrightarrow> 

84 
hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))" 

85 
apply (drule sym) 

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

86 
apply (unfold new_Addr_def) 
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

87 
apply (simp split: split_if_asm) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

88 
apply (erule LeastI) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

90 

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

91 
lemma raise_if_True [simp]: "raise_if True x y \<noteq> None" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

92 
apply (unfold raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

95 

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

96 
lemma raise_if_False [simp]: "raise_if False x y = y" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

97 
apply (unfold raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

100 

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

101 
lemma raise_if_Some [simp]: "raise_if c x (Some y) \<noteq> None" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

102 
apply (unfold raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

105 

12517  106 
lemma raise_if_Some2 [simp]: 
107 
"raise_if c z (if x = None then Some y else x) \<noteq> None" 

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

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

109 
apply(induct_tac "x") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

112 

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

113 
lemma raise_if_SomeD [rule_format (no_asm)]: 
13672  114 
"raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some (Addr (XcptRef x))  y = Some z" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

115 
apply (unfold raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

118 

12517  119 
lemma raise_if_NoneD [rule_format (no_asm)]: 
120 
"raise_if c x y = None > \<not> c \<and> y = None" 

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

121 
apply (unfold raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

124 

12517  125 
lemma np_NoneD [rule_format (no_asm)]: 
126 
"np a' x' = None > x' = None \<and> a' \<noteq> Null" 

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

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

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

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

130 

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

131 
lemma np_None [rule_format (no_asm), simp]: "a' \<noteq> Null > np a' x' = x'" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

132 
apply (unfold np_def raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

135 

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

136 
lemma np_Some [simp]: "np a' (Some xc) = Some xc" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

137 
apply (unfold np_def raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

140 

13672  141 
lemma np_Null [simp]: "np Null None = Some (Addr (XcptRef NullPointer))" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

142 
apply (unfold np_def raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

145 

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

146 
lemma np_Addr [simp]: "np (Addr a) None = None" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

147 
apply (unfold np_def raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

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

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

150 

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

151 
lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) = 
13672  152 
Some (Addr (XcptRef (if c then xc else NullPointer)))" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

153 
apply (unfold raise_if_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

154 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10061
diff
changeset

155 
done 
8011  156 

14144  157 
lemma c_hupd_fst [simp]: "fst (c_hupd h (x, s)) = x" 
158 
by (simp add: c_hupd_def split_beta) 

159 

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

160 
text {* Naive implementation for @{term "new_Addr"} by exhaustive search *} 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

161 

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

162 
definition gen_new_Addr :: "aheap => nat \<Rightarrow> loc \<times> val option" where 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

163 
"gen_new_Addr h n \<equiv> 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

164 
if \<exists>a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

165 
then (Loc (nat_to_loc' (LEAST a. a \<ge> n \<and> h (Loc (nat_to_loc' a)) = None)), None) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

166 
else (Loc (nat_to_loc' 0), Some (Addr (XcptRef OutOfMemory)))" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

167 

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

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

169 
"new_Addr h = gen_new_Addr h 0" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

170 
by(simp only: new_Addr_def gen_new_Addr_def split: split_if) simp 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

171 

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

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

173 
"gen_new_Addr h n = (if h (Loc (nat_to_loc' n)) = None then (Loc (nat_to_loc' n), None) else gen_new_Addr h (Suc n))" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

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

175 
apply(rule impI) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

176 
apply(rule conjI) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

177 
apply safe[1] 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

178 
apply(auto intro: arg_cong[where f=nat_to_loc'] Least_equality)[1] 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

179 
apply(rule arg_cong[where f=nat_to_loc']) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

180 
apply(rule arg_cong[where f=Least]) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

181 
apply(rule ext) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

182 
apply(safe, simp_all)[1] 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

183 
apply(rename_tac "n'") 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

184 
apply(case_tac "n = n'", simp_all)[1] 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

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

186 
apply(subgoal_tac "a = n") 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

187 
apply(auto intro: Least_equality arg_cong[where f=nat_to_loc'])[1] 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

188 
apply(rule ccontr) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

189 
apply(erule_tac x="a" in allE) 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

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

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

192 

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

193 
instantiation loc' :: equal begin 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

194 
definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'" 
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

195 
instance proof qed(simp add: equal_loc'_def) 
8011  196 
end 
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
42463
diff
changeset

197 

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

198 
end 