author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12925  99131847fb93 
child 13462  56610e2ba220 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/Basis.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 

6 
*) 

7 
header {* Definitions extending HOL as logical basis of Bali *} 

8 

9 
theory Basis = Main: 

10 

11 
ML_setup {* 

12 
Unify.search_bound := 40; 

13 
Unify.trace_bound := 40; 

14 
*} 

15 
(*print_depth 100;*) 

16 
(*Syntax.ambiguity_level := 1;*) 

17 

18 
section "misc" 

19 

20 
declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *) 

21 

22 
(* ###TO HOL/???.ML?? *) 

23 
ML {* 

24 
fun make_simproc name pat pred thm = Simplifier.mk_simproc name 

25 
[Thm.read_cterm (Thm.sign_of_thm thm) (pat, HOLogic.typeT)] 

26 
(K (K (fn s => if pred s then None else Some (standard (mk_meta_eq thm))))) 

27 
*} 

28 

29 
declare split_if_asm [split] option.split [split] option.split_asm [split] 

30 
ML {* 

31 
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) 

32 
*} 

33 
declare if_weak_cong [cong del] option.weak_case_cong [cong del] 

34 
declare length_Suc_conv [iff]; 

35 

36 
(*###to be phased out *) 

37 
ML {* 

38 
bind_thm ("make_imp", rearrange_prems [1,0] mp) 

39 
*} 

40 

41 
lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}" 

42 
apply auto 

43 
done 

44 

45 
lemma subset_insertD: 

46 
"A <= insert x B ==> A <= B & x ~: A  (EX B'. A = insert x B' & B' <= B)" 

47 
apply (case_tac "x:A") 

48 
apply (rule disjI2) 

49 
apply (rule_tac x = "A{x}" in exI) 

50 
apply fast+ 

51 
done 

52 

53 
syntax 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

54 
"3" :: nat ("3") 
12854  55 
"4" :: nat ("4") 
56 
translations 

57 
"3" == "Suc 2" 

58 
"4" == "Suc 3" 

59 

60 
(*unused*) 

61 
lemma range_bool_domain: "range f = {f True, f False}" 

62 
apply auto 

63 
apply (case_tac "xa") 

64 
apply auto 

65 
done 

66 

67 
(* context (theory "Transitive_Closure") *) 

68 
lemma irrefl_tranclI': "r^1 Int r^+ = {} ==> !x. (x, x) ~: r^+" 

69 
apply (rule allI) 

70 
apply (erule irrefl_tranclI) 

71 
done 

72 

73 
lemma trancl_rtrancl_trancl: 

74 
"\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+" 

75 
by (auto dest: tranclD rtrancl_trans rtrancl_into_trancl2) 

76 

77 
lemma rtrancl_into_trancl3: 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

78 
"\<lbrakk>(a,b)\<in>r^*; a\<noteq>b\<rbrakk> \<Longrightarrow> (a,b)\<in>r^+" 
12854  79 
apply (drule rtranclD) 
80 
apply auto 

81 
done 

82 

83 
lemma rtrancl_into_rtrancl2: 

84 
"\<lbrakk> (a, b) \<in> r; (b, c) \<in> r^* \<rbrakk> \<Longrightarrow> (a, c) \<in> r^*" 

85 
by (auto intro: r_into_rtrancl rtrancl_trans) 

86 

87 
lemma triangle_lemma: 

88 
"\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk> 

89 
\<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*" 

90 
proof  

91 
note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1] 

92 
note converse_rtranclE = converse_rtranclE [consumes 1] 

93 
assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c" 

94 
assume "(a,x)\<in>r\<^sup>*" 

95 
then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*" 

96 
proof (induct rule: converse_rtrancl_induct) 

97 
assume "(x,y)\<in>r\<^sup>*" 

98 
then show ?thesis 

99 
by blast 

100 
next 

101 
fix a v 

102 
assume a_v_r: "(a, v) \<in> r" and 

103 
v_x_rt: "(v, x) \<in> r\<^sup>*" and 

104 
a_y_rt: "(a, y) \<in> r\<^sup>*" and 

105 
hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*" 

106 
from a_y_rt 

107 
show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*" 

108 
proof (cases rule: converse_rtranclE) 

109 
assume "a=y" 

110 
with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*" 

111 
by (auto intro: r_into_rtrancl rtrancl_trans) 

112 
then show ?thesis 

113 
by blast 

114 
next 

115 
fix w 

116 
assume a_w_r: "(a, w) \<in> r" and 

117 
w_y_rt: "(w, y) \<in> r\<^sup>*" 

118 
from a_v_r a_w_r unique 

119 
have "v=w" 

120 
by auto 

121 
with w_y_rt hyp 

122 
show ?thesis 

123 
by blast 

124 
qed 

125 
qed 

126 
qed 

127 

128 

129 
lemma rtrancl_cases [consumes 1, case_names Refl Trancl]: 

130 
"\<lbrakk>(a,b)\<in>r\<^sup>*; a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 

131 
apply (erule rtranclE) 

132 
apply (auto dest: rtrancl_into_trancl1) 

133 
done 

134 

135 
(* ### To Transitive_Closure *) 

136 
theorems converse_rtrancl_induct 

137 
= converse_rtrancl_induct [consumes 1,case_names Id Step] 

138 

139 
theorems converse_trancl_induct 

140 
= converse_trancl_induct [consumes 1,case_names Single Step] 

141 

142 
(* context (theory "Set") *) 

143 
lemma Ball_weaken:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q" 

144 
by auto 

145 

146 
(* context (theory "Finite") *) 

147 
lemma finite_SetCompr2: "[ finite (Collect P); !y. P y > finite (range (f y)) ] ==> 

148 
finite {f y x x y. P y}" 

149 
apply (subgoal_tac "{f y x x y. P y} = UNION (Collect P) (%y. range (f y))") 

150 
prefer 2 apply fast 

151 
apply (erule ssubst) 

152 
apply (erule finite_UN_I) 

153 
apply fast 

154 
done 

155 

156 

157 
(* ### TO theory "List" *) 

158 
lemma list_all2_trans: "\<forall> a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow> 

159 
\<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3" 

160 
apply (induct_tac "xs1") 

161 
apply simp 

162 
apply (rule allI) 

163 
apply (induct_tac "xs2") 

164 
apply simp 

165 
apply (rule allI) 

166 
apply (induct_tac "xs3") 

167 
apply auto 

168 
done 

169 

170 

171 
section "pairs" 

172 

173 
lemma surjective_pairing5: "p = (fst p, fst (snd p), fst (snd (snd p)), fst (snd (snd (snd p))), 

174 
snd (snd (snd (snd p))))" 

175 
apply auto 

176 
done 

177 

178 
lemma fst_splitE [elim!]: 

179 
"[ fst s' = x'; !!x s. [ s' = (x,s); x = x' ] ==> Q ] ==> Q" 

180 
apply (cut_tac p = "s'" in surjective_pairing) 

181 
apply auto 

182 
done 

183 

184 
lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l > x : fst ` set l" 

185 
apply (induct_tac "l") 

186 
apply auto 

187 
done 

188 

189 

190 
section "quantifiers" 

191 

192 
(*###to be phased out *) 

193 
ML {* 

194 
fun noAll_simpset () = simpset() setmksimps 

195 
mksimps (filter (fn (x,_) => x<>"All") mksimps_pairs) 

196 
*} 

197 

198 
lemma All_Ex_refl_eq2 [simp]: 

199 
"(!x. (? b. x = f b & Q b) \<longrightarrow> P x) = (!b. Q b > P (f b))" 

200 
apply auto 

201 
done 

202 

203 
lemma ex_ex_miniscope1 [simp]: 

204 
"(EX w v. P w v & Q v) = (EX v. (EX w. P w v) & Q v)" 

205 
apply auto 

206 
done 

207 

208 
lemma ex_miniscope2 [simp]: 

209 
"(EX v. P v & Q & R v) = (Q & (EX v. P v & R v))" 

210 
apply auto 

211 
done 

212 

213 
lemma ex_reorder31: "(\<exists>z x y. P x y z) = (\<exists>x y z. P x y z)" 

214 
apply auto 

215 
done 

216 

217 
lemma All_Ex_refl_eq1 [simp]: "(!x. (? b. x = f b) > P x) = (!b. P (f b))" 

218 
apply auto 

219 
done 

220 

221 

222 
section "sums" 

223 

224 
hide const In0 In1 

225 

226 
syntax 

227 
fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80) 

228 
translations 

229 
"fun_sum" == "sum_case" 

230 

231 
consts the_Inl :: "'a + 'b \<Rightarrow> 'a" 

232 
the_Inr :: "'a + 'b \<Rightarrow> 'b" 

233 
primrec "the_Inl (Inl a) = a" 

234 
primrec "the_Inr (Inr b) = b" 

235 

236 
datatype ('a, 'b, 'c) sum3 = In1 'a  In2 'b  In3 'c 

237 

238 
consts the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a" 

239 
the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b" 

240 
the_In3 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c" 

241 
primrec "the_In1 (In1 a) = a" 

242 
primrec "the_In2 (In2 b) = b" 

243 
primrec "the_In3 (In3 c) = c" 

244 

245 
syntax 

246 
In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3" 

247 
In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3" 

248 
translations 

249 
"In1l e" == "In1 (Inl e)" 

250 
"In1r c" == "In1 (Inr c)" 

251 

252 
ML {* 

253 
fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[not_None_eq]) 

254 
(read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] 

255 
*} 

256 
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) 

257 

258 
translations 

12919  259 
"option"<= (type) "Datatype.option" 
12854  260 
"list" <= (type) "List.list" 
261 
"sum3" <= (type) "Basis.sum3" 

262 

263 

264 
section "quantifiers for option type" 

265 

266 
syntax 

267 
Oall :: "[pttrn, 'a option, bool] => bool" ("(3! _:_:/ _)" [0,0,10] 10) 

268 
Oex :: "[pttrn, 'a option, bool] => bool" ("(3? _:_:/ _)" [0,0,10] 10) 

269 

270 
syntax (symbols) 

271 
Oall :: "[pttrn, 'a option, bool] => bool" ("(3\<forall>_\<in>_:/ _)" [0,0,10] 10) 

272 
Oex :: "[pttrn, 'a option, bool] => bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10) 

273 

274 
translations 

275 
"! x:A: P" == "! x:o2s A. P" 

276 
"? x:A: P" == "? x:o2s A. P" 

277 

278 

279 
section "unique association lists" 

280 

281 
constdefs 

282 
unique :: "('a \<times> 'b) list \<Rightarrow> bool" 

12893  283 
"unique \<equiv> distinct \<circ> map fst" 
12854  284 

285 
lemma uniqueD [rule_format (no_asm)]: 

286 
"unique l> (!x y. (x,y):set l > (!x' y'. (x',y'):set l > x=x'> y=y'))" 

287 
apply (unfold unique_def o_def) 

288 
apply (induct_tac "l") 

289 
apply (auto dest: fst_in_set_lemma) 

290 
done 

291 

292 
lemma unique_Nil [simp]: "unique []" 

293 
apply (unfold unique_def) 

294 
apply (simp (no_asm)) 

295 
done 

296 

297 
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))" 

298 
apply (unfold unique_def) 

299 
apply (auto dest: fst_in_set_lemma) 

300 
done 

301 

302 
lemmas unique_ConsI = conjI [THEN unique_Cons [THEN iffD2], standard] 

303 

304 
lemma unique_single [simp]: "!!p. unique [p]" 

305 
apply auto 

306 
done 

307 

308 
lemma unique_ConsD: "unique (x#xs) ==> unique xs" 

309 
apply (simp add: unique_def) 

310 
done 

311 

312 
lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l > 

313 
(!(x,y):set l. !(x',y'):set l'. x' ~= x) > unique (l @ l')" 

314 
apply (induct_tac "l") 

315 
apply (auto dest: fst_in_set_lemma) 

316 
done 

317 

318 
lemma unique_map_inj [rule_format (no_asm)]: "unique l > inj f > unique (map (%(k,x). (f k, g k x)) l)" 

319 
apply (induct_tac "l") 

320 
apply (auto dest: fst_in_set_lemma simp add: inj_eq) 

321 
done 

322 

323 
lemma map_of_SomeI [rule_format (no_asm)]: "unique l > (k, x) : set l > map_of l k = Some x" 

324 
apply (induct_tac "l") 

325 
apply auto 

326 
done 

327 

328 

329 
section "list patterns" 

330 

331 
consts 

332 
lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b" 

333 
defs 

334 
lsplit_def: "lsplit == %f l. f (hd l) (tl l)" 

335 
(* list patterns  extends predefined type "pttrn" used in abstractions *) 

336 
syntax 

337 
"_lpttrn" :: "[pttrn,pttrn] => pttrn" ("_#/_" [901,900] 900) 

338 
translations 

339 
"%y#x#xs. b" == "lsplit (%y x#xs. b)" 

340 
"%x#xs . b" == "lsplit (%x xs . b)" 

341 

342 
lemma lsplit [simp]: "lsplit c (x#xs) = c x xs" 

343 
apply (unfold lsplit_def) 

344 
apply (simp (no_asm)) 

345 
done 

346 

347 
lemma lsplit2 [simp]: "lsplit P (x#xs) y z = P x xs y z" 

348 
apply (unfold lsplit_def) 

349 
apply simp 

350 
done 

351 

352 

353 
section "dummy pattern for quantifiers, let, etc." 

354 

355 
syntax 

356 
"@dummy_pat" :: pttrn ("'_") 

357 

358 
parse_translation {* 

359 
let fun dummy_pat_tr [] = Free ("_",dummyT) 

360 
 dummy_pat_tr ts = raise TERM ("dummy_pat_tr", ts); 

361 
in [("@dummy_pat", dummy_pat_tr)] 

362 
end 

363 
*} 

364 

365 
end 