author  blanchet 
Tue, 27 Oct 2009 17:53:19 +0100  
changeset 33557  107f3df799f6 
parent 33556  cba22e2999d5 
child 33571  3655e51f9958 
permissions  rwrr 
33192  1 
(* Title: HOL/Nitpick/Tools/nitpick_hol.ML 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 
Copyright 2008, 2009 

4 

5 
Auxiliary HOLrelated functions used by Nitpick. 

6 
*) 

7 

8 
signature NITPICK_HOL = 

9 
sig 

10 
type const_table = term list Symtab.table 

11 
type special_fun = (styp * int list * term list) * styp 

12 
type unrolled = styp * styp 

13 
type wf_cache = (styp * (bool * bool)) list 

14 

15 
type extended_context = { 

16 
thy: theory, 

17 
ctxt: Proof.context, 

18 
max_bisim_depth: int, 

19 
boxes: (typ option * bool option) list, 

20 
wfs: (styp option * bool option) list, 

21 
user_axioms: bool option, 

22 
debug: bool, 

23 
destroy_constrs: bool, 

24 
specialize: bool, 

25 
skolemize: bool, 

26 
star_linear_preds: bool, 

27 
uncurry: bool, 

28 
fast_descrs: bool, 

29 
tac_timeout: Time.time option, 

30 
evals: term list, 

31 
case_names: (string * int) list, 

32 
def_table: const_table, 

33 
nondef_table: const_table, 

34 
user_nondefs: term list, 

35 
simp_table: const_table Unsynchronized.ref, 

36 
psimp_table: const_table, 

37 
intro_table: const_table, 

38 
ground_thm_table: term list Inttab.table, 

39 
ersatz_table: (string * string) list, 

40 
skolems: (string * string list) list Unsynchronized.ref, 

41 
special_funs: special_fun list Unsynchronized.ref, 

42 
unrolled_preds: unrolled list Unsynchronized.ref, 

43 
wf_cache: wf_cache Unsynchronized.ref} 

44 

45 
val name_sep : string 

46 
val numeral_prefix : string 

47 
val skolem_prefix : string 

48 
val eval_prefix : string 

49 
val original_name : string > string 

50 
val unbox_type : typ > typ 

51 
val string_for_type : Proof.context > typ > string 

52 
val prefix_name : string > string > string 

53 
val short_name : string > string 

54 
val short_const_name : string > string 

55 
val shorten_const_names_in_term : term > term 

56 
val type_match : theory > typ * typ > bool 

57 
val const_match : theory > styp * styp > bool 

58 
val term_match : theory > term * term > bool 

59 
val is_TFree : typ > bool 

60 
val is_higher_order_type : typ > bool 

61 
val is_fun_type : typ > bool 

62 
val is_set_type : typ > bool 

63 
val is_pair_type : typ > bool 

64 
val is_lfp_iterator_type : typ > bool 

65 
val is_gfp_iterator_type : typ > bool 

66 
val is_fp_iterator_type : typ > bool 

67 
val is_boolean_type : typ > bool 

68 
val is_integer_type : typ > bool 

69 
val is_record_type : typ > bool 

70 
val is_number_type : theory > typ > bool 

71 
val const_for_iterator_type : typ > styp 

72 
val nth_range_type : int > typ > typ 

73 
val num_factors_in_type : typ > int 

74 
val num_binder_types : typ > int 

75 
val curried_binder_types : typ > typ list 

76 
val mk_flat_tuple : typ > term list > term 

77 
val dest_n_tuple : int > term > term list 

78 
val instantiate_type : theory > typ > typ > typ > typ 

79 
val is_codatatype : theory > typ > bool 

80 
val is_pure_typedef : theory > typ > bool 

81 
val is_univ_typedef : theory > typ > bool 

82 
val is_datatype : theory > typ > bool 

83 
val is_record_constr : styp > bool 

84 
val is_record_get : theory > styp > bool 

85 
val is_record_update : theory > styp > bool 

86 
val is_abs_fun : theory > styp > bool 

87 
val is_rep_fun : theory > styp > bool 

88 
val is_constr : theory > styp > bool 

89 
val is_sel : string > bool 

90 
val discr_for_constr : styp > styp 

91 
val num_sels_for_constr_type : typ > int 

92 
val nth_sel_name_for_constr_name : string > int > string 

93 
val nth_sel_for_constr : styp > int > styp 

94 
val boxed_nth_sel_for_constr : extended_context > styp > int > styp 

95 
val sel_no_from_name : string > int 

96 
val eta_expand : typ list > term > int > term 

97 
val extensionalize : term > term 

98 
val distinctness_formula : typ > term list > term 

99 
val register_frac_type : string > (string * string) list > theory > theory 

100 
val unregister_frac_type : string > theory > theory 

101 
val register_codatatype : typ > string > styp list > theory > theory 

102 
val unregister_codatatype : typ > theory > theory 

103 
val datatype_constrs : theory > typ > styp list 

104 
val boxed_datatype_constrs : extended_context > typ > styp list 

105 
val num_datatype_constrs : theory > typ > int 

106 
val constr_name_for_sel_like : string > string 

107 
val boxed_constr_for_sel : extended_context > styp > styp 

108 
val card_of_type : (typ * int) list > typ > int 

109 
val bounded_card_of_type : int > int > (typ * int) list > typ > int 

110 
val bounded_precise_card_of_type : 

111 
theory > int > int > (typ * int) list > typ > int 

112 
val is_finite_type : theory > typ > bool 

113 
val all_axioms_of : theory > term list * term list * term list 

114 
val arity_of_built_in_const : bool > styp > int option 

115 
val is_built_in_const : bool > styp > bool 

116 
val case_const_names : theory > (string * int) list 

117 
val const_def_table : Proof.context > term list > const_table 

118 
val const_nondef_table : term list > const_table 

119 
val const_simp_table : Proof.context > const_table 

120 
val const_psimp_table : Proof.context > const_table 

121 
val inductive_intro_table : Proof.context > const_table > const_table 

122 
val ground_theorem_table : theory > term list Inttab.table 

123 
val ersatz_table : theory > (string * string) list 

124 
val def_of_const : theory > const_table > styp > term option 

125 
val is_inductive_pred : extended_context > styp > bool 

126 
val is_constr_pattern_lhs : theory > term > bool 

127 
val is_constr_pattern_formula : theory > term > bool 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33232
diff
changeset

128 
val merge_type_vars_in_terms : term list > term list 
33192  129 
val ground_types_in_type : extended_context > typ > typ list 
130 
val ground_types_in_terms : extended_context > term list > typ list 

131 
val format_type : int list > int list > typ > typ 

132 
val format_term_type : 

133 
theory > const_table > (term option * int list) list > term > typ 

134 
val user_friendly_const : 

135 
extended_context > string * string > (term option * int list) list 

136 
> styp > term * typ 

137 
val assign_operator_for_const : styp > string 

138 
val preprocess_term : 

139 
extended_context > term > ((term list * term list) * (bool * bool)) * term 

140 
end; 

141 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

142 
structure Nitpick_HOL : NITPICK_HOL = 
33192  143 
struct 
144 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

145 
open Nitpick_Util 
33192  146 

147 
type const_table = term list Symtab.table 

148 
type special_fun = (styp * int list * term list) * styp 

149 
type unrolled = styp * styp 

150 
type wf_cache = (styp * (bool * bool)) list 

151 

152 
type extended_context = { 

153 
thy: theory, 

154 
ctxt: Proof.context, 

155 
max_bisim_depth: int, 

156 
boxes: (typ option * bool option) list, 

157 
wfs: (styp option * bool option) list, 

158 
user_axioms: bool option, 

159 
debug: bool, 

160 
destroy_constrs: bool, 

161 
specialize: bool, 

162 
skolemize: bool, 

163 
star_linear_preds: bool, 

164 
uncurry: bool, 

165 
fast_descrs: bool, 

166 
tac_timeout: Time.time option, 

167 
evals: term list, 

168 
case_names: (string * int) list, 

169 
def_table: const_table, 

170 
nondef_table: const_table, 

171 
user_nondefs: term list, 

172 
simp_table: const_table Unsynchronized.ref, 

173 
psimp_table: const_table, 

174 
intro_table: const_table, 

175 
ground_thm_table: term list Inttab.table, 

176 
ersatz_table: (string * string) list, 

177 
skolems: (string * string list) list Unsynchronized.ref, 

178 
special_funs: special_fun list Unsynchronized.ref, 

179 
unrolled_preds: unrolled list Unsynchronized.ref, 

180 
wf_cache: wf_cache Unsynchronized.ref} 

181 

182 
structure TheoryData = TheoryDataFun( 

183 
type T = {frac_types: (string * (string * string) list) list, 

184 
codatatypes: (string * (string * styp list)) list} 

185 
val empty = {frac_types = [], codatatypes = []} 

186 
val copy = I 

187 
val extend = I 

188 
fun merge _ ({frac_types = fs1, codatatypes = cs1}, 

189 
{frac_types = fs2, codatatypes = cs2}) = 

190 
{frac_types = AList.merge (op =) (op =) (fs1, fs2), 

191 
codatatypes = AList.merge (op =) (op =) (cs1, cs2)}) 

192 

193 
(* term * term > term *) 

194 
fun s_conj (t1, @{const True}) = t1 

195 
 s_conj (@{const True}, t2) = t2 

196 
 s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False} 

197 
else HOLogic.mk_conj (t1, t2) 

198 
fun s_disj (t1, @{const False}) = t1 

199 
 s_disj (@{const False}, t2) = t2 

200 
 s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True} 

201 
else HOLogic.mk_disj (t1, t2) 

202 
(* term > term > term *) 

203 
fun mk_exists v t = 

204 
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) 

205 

206 
(* term > term > term list *) 

207 
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) = 

208 
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t] 

209 
 strip_connective _ t = [t] 

210 
(* term > term list * term *) 

211 
fun strip_any_connective (t as (t0 $ t1 $ t2)) = 

212 
if t0 mem [@{const "op &"}, @{const "op "}] then 

213 
(strip_connective t0 t, t0) 

214 
else 

215 
([t], @{const Not}) 

216 
 strip_any_connective t = ([t], @{const Not}) 

217 
(* term > term list *) 

218 
val conjuncts = strip_connective @{const "op &"} 

219 
val disjuncts = strip_connective @{const "op "} 

220 

221 
val name_sep = "$" 

222 
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep 

223 
val sel_prefix = nitpick_prefix ^ "sel" 

224 
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep 

225 
val set_prefix = nitpick_prefix ^ "set" ^ name_sep 

226 
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep 

227 
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep 

228 
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep 

229 
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep 

230 
val base_prefix = nitpick_prefix ^ "base" ^ name_sep 

231 
val step_prefix = nitpick_prefix ^ "step" ^ name_sep 

232 
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep 

233 
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep 

234 
val skolem_prefix = nitpick_prefix ^ "sk" 

235 
val special_prefix = nitpick_prefix ^ "sp" 

236 
val uncurry_prefix = nitpick_prefix ^ "unc" 

237 
val eval_prefix = nitpick_prefix ^ "eval" 

238 
val bound_var_prefix = "b" 

239 
val cong_var_prefix = "c" 

240 
val iter_var_prefix = "i" 

241 
val val_var_prefix = nitpick_prefix ^ "v" 

242 
val arg_var_prefix = "x" 

243 

244 
(* int > string *) 

245 
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep 

246 
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep 

247 
(* int > int > string *) 

248 
fun skolem_prefix_for k j = 

249 
skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep 

250 
fun uncurry_prefix_for k j = 

251 
uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep 

252 

253 
(* string > string * string *) 

254 
val strip_first_name_sep = 

255 
Substring.full #> Substring.position name_sep ##> Substring.triml 1 

256 
#> pairself Substring.string 

257 
(* string > string *) 

258 
fun original_name s = 

259 
if String.isPrefix nitpick_prefix s then 

260 
case strip_first_name_sep s of (s1, "") => s1  (_, s2) => original_name s2 

261 
else 

262 
s 

263 
val after_name_sep = snd o strip_first_name_sep 

264 

265 
(* When you add constants to these lists, make sure to handle them in 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

266 
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as 
33192  267 
well. *) 
268 
val built_in_consts = 

269 
[(@{const_name all}, 1), 

270 
(@{const_name "=="}, 2), 

271 
(@{const_name "==>"}, 2), 

272 
(@{const_name Pure.conjunction}, 2), 

273 
(@{const_name Trueprop}, 1), 

274 
(@{const_name Not}, 1), 

275 
(@{const_name False}, 0), 

276 
(@{const_name True}, 0), 

277 
(@{const_name All}, 1), 

278 
(@{const_name Ex}, 1), 

279 
(@{const_name "op ="}, 2), 

280 
(@{const_name "op &"}, 2), 

281 
(@{const_name "op "}, 2), 

282 
(@{const_name "op >"}, 2), 

283 
(@{const_name If}, 3), 

284 
(@{const_name Let}, 2), 

285 
(@{const_name Unity}, 0), 

286 
(@{const_name Pair}, 2), 

287 
(@{const_name fst}, 1), 

288 
(@{const_name snd}, 1), 

289 
(@{const_name Id}, 0), 

290 
(@{const_name insert}, 2), 

291 
(@{const_name converse}, 1), 

292 
(@{const_name trancl}, 1), 

293 
(@{const_name rel_comp}, 2), 

294 
(@{const_name image}, 2), 

295 
(@{const_name Suc}, 0), 

296 
(@{const_name finite}, 1), 

297 
(@{const_name nat}, 0), 

298 
(@{const_name zero_nat_inst.zero_nat}, 0), 

299 
(@{const_name one_nat_inst.one_nat}, 0), 

300 
(@{const_name plus_nat_inst.plus_nat}, 0), 

301 
(@{const_name minus_nat_inst.minus_nat}, 0), 

302 
(@{const_name times_nat_inst.times_nat}, 0), 

303 
(@{const_name div_nat_inst.div_nat}, 0), 

304 
(@{const_name div_nat_inst.mod_nat}, 0), 

305 
(@{const_name ord_nat_inst.less_nat}, 2), 

306 
(@{const_name ord_nat_inst.less_eq_nat}, 2), 

307 
(@{const_name nat_gcd}, 0), 

308 
(@{const_name nat_lcm}, 0), 

309 
(@{const_name zero_int_inst.zero_int}, 0), 

310 
(@{const_name one_int_inst.one_int}, 0), 

311 
(@{const_name plus_int_inst.plus_int}, 0), 

312 
(@{const_name minus_int_inst.minus_int}, 0), 

313 
(@{const_name times_int_inst.times_int}, 0), 

314 
(@{const_name div_int_inst.div_int}, 0), 

315 
(@{const_name div_int_inst.mod_int}, 0), 

316 
(@{const_name uminus_int_inst.uminus_int}, 0), (* FIXME: needed? *) 

317 
(@{const_name ord_int_inst.less_int}, 2), 

318 
(@{const_name ord_int_inst.less_eq_int}, 2), 

319 
(@{const_name Tha}, 1), 

320 
(@{const_name Frac}, 0), 

321 
(@{const_name norm_frac}, 0)] 

322 
val built_in_descr_consts = 

323 
[(@{const_name The}, 1), 

324 
(@{const_name Eps}, 1)] 

325 
val built_in_typed_consts = 

326 
[((@{const_name of_nat}, nat_T > int_T), 0)] 

327 
val built_in_set_consts = 

328 
[(@{const_name lower_semilattice_fun_inst.inf_fun}, 2), 

329 
(@{const_name upper_semilattice_fun_inst.sup_fun}, 2), 

330 
(@{const_name minus_fun_inst.minus_fun}, 2), 

331 
(@{const_name ord_fun_inst.less_eq_fun}, 2)] 

332 

333 
(* typ > typ *) 

334 
fun unbox_type (Type (@{type_name fun_box}, Ts)) = 

335 
Type ("fun", map unbox_type Ts) 

336 
 unbox_type (Type (@{type_name pair_box}, Ts)) = 

337 
Type ("*", map unbox_type Ts) 

338 
 unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts) 

339 
 unbox_type T = T 

340 
(* Proof.context > typ > string *) 

341 
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type 

342 

343 
(* string > string > string *) 

344 
val prefix_name = Long_Name.qualify o Long_Name.base_name 

345 
(* string > string *) 

346 
fun short_name s = List.last (space_explode "." s) handle List.Empty => "" 

347 
(* string > term > term *) 

348 
val prefix_abs_vars = Term.map_abs_vars o prefix_name 

349 
(* term > term *) 

350 
val shorten_abs_vars = Term.map_abs_vars short_name 

351 
(* string > string *) 

352 
fun short_const_name s = 

353 
case space_explode name_sep s of 

354 
[_] => s > String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix 

355 
 ss => map short_name ss > space_implode "_" 

356 
(* term > term *) 

357 
val shorten_const_names_in_term = 

358 
map_aterms (fn Const (s, T) => Const (short_const_name s, T)  t => t) 

359 

360 
(* theory > typ * typ > bool *) 

361 
fun type_match thy (T1, T2) = 

362 
(Sign.typ_match thy (T2, T1) Vartab.empty; true) 

363 
handle Type.TYPE_MATCH => false 

364 
(* theory > styp * styp > bool *) 

365 
fun const_match thy ((s1, T1), (s2, T2)) = 

366 
s1 = s2 andalso type_match thy (T1, T2) 

367 
(* theory > term * term > bool *) 

368 
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2) 

369 
 term_match thy (Free (s1, T1), Free (s2, T2)) = 

370 
const_match thy ((short_name s1, T1), (short_name s2, T2)) 

371 
 term_match thy (t1, t2) = t1 aconv t2 

372 

373 
(* typ > bool *) 

374 
fun is_TFree (TFree _) = true 

375 
 is_TFree _ = false 

376 
fun is_higher_order_type (Type ("fun", _)) = true 

377 
 is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts 

378 
 is_higher_order_type _ = false 

379 
fun is_fun_type (Type ("fun", _)) = true 

380 
 is_fun_type _ = false 

381 
fun is_set_type (Type ("fun", [_, @{typ bool}])) = true 

382 
 is_set_type _ = false 

383 
fun is_pair_type (Type ("*", _)) = true 

384 
 is_pair_type _ = false 

385 
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s 

386 
 is_lfp_iterator_type _ = false 

387 
fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s 

388 
 is_gfp_iterator_type _ = false 

389 
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type 

390 
val is_boolean_type = equal prop_T orf equal bool_T 

391 
val is_integer_type = 

392 
member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type 

393 
val is_record_type = not o null o Record.dest_recTs 

394 
(* theory > typ > bool *) 

395 
fun is_frac_type thy (Type (s, [])) = 

396 
not (null (these (AList.lookup (op =) (#frac_types (TheoryData.get thy)) 

397 
s))) 

398 
 is_frac_type _ _ = false 

399 
fun is_number_type thy = is_integer_type orf is_frac_type thy 

400 

401 
(* bool > styp > typ *) 

402 
fun iterator_type_for_const gfp (s, T) = 

403 
Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s, 

404 
binder_types T) 

405 
(* typ > styp *) 

406 
fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts > bool_T) 

407 
 const_for_iterator_type T = 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

408 
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) 
33192  409 

410 
(* int > typ > typ * typ *) 

411 
fun strip_n_binders 0 T = ([], T) 

412 
 strip_n_binders n (Type ("fun", [T1, T2])) = 

413 
strip_n_binders (n  1) T2 >> cons T1 

414 
 strip_n_binders n (Type (@{type_name fun_box}, Ts)) = 

415 
strip_n_binders n (Type ("fun", Ts)) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

416 
 strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], []) 
33192  417 
(* typ > typ *) 
418 
val nth_range_type = snd oo strip_n_binders 

419 

420 
(* typ > int *) 

421 
fun num_factors_in_type (Type ("*", [T1, T2])) = 

422 
fold (Integer.add o num_factors_in_type) [T1, T2] 0 

423 
 num_factors_in_type _ = 1 

424 
fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2 

425 
 num_binder_types _ = 0 

426 
(* typ > typ list *) 

427 
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types 

428 
fun maybe_curried_binder_types T = 

429 
(if is_pair_type (body_type T) then binder_types else curried_binder_types) T 

430 

431 
(* typ > term list > term *) 

432 
fun mk_flat_tuple _ [t] = t 

433 
 mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) = 

434 
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

435 
 mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts) 
33192  436 
(* int > term > term list *) 
437 
fun dest_n_tuple 1 t = [t] 

438 
 dest_n_tuple n t = HOLogic.dest_prod t > dest_n_tuple (n  1) > op :: 

439 

440 
(* int > typ > typ list *) 

441 
fun dest_n_tuple_type 1 T = [T] 

442 
 dest_n_tuple_type n (Type (_, [T1, T2])) = 

443 
T1 :: dest_n_tuple_type (n  1) T2 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

444 
 dest_n_tuple_type _ T = 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

445 
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) 
33192  446 

447 
(* (typ * typ) list > typ > typ *) 

448 
fun typ_subst [] T = T 

449 
 typ_subst ps T = 

450 
let 

451 
(* typ > typ *) 

452 
fun subst T = 

453 
case AList.lookup (op =) ps T of 

454 
SOME T' => T' 

455 
 NONE => case T of Type (s, Ts) => Type (s, map subst Ts)  _ => T 

456 
in subst T end 

457 

458 
(* theory > typ > typ > typ > typ *) 

459 
fun instantiate_type thy T1 T1' T2 = 

460 
Same.commit (Envir.subst_type_same 

461 
(Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty)) 

462 
(Logic.varifyT T2) 

463 
handle Type.TYPE_MATCH => 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

464 
raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], []) 
33192  465 

466 
(* theory > typ > typ > styp *) 

467 
fun repair_constr_type thy body_T' T = 

468 
instantiate_type thy (body_type T) body_T' T 

469 

470 
(* string > (string * string) list > theory > theory *) 

471 
fun register_frac_type frac_s ersaetze thy = 

472 
let 

473 
val {frac_types, codatatypes} = TheoryData.get thy 

474 
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types 

475 
in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end 

476 
(* string > theory > theory *) 

477 
fun unregister_frac_type frac_s = register_frac_type frac_s [] 

478 

479 
(* typ > string > styp list > theory > theory *) 

480 
fun register_codatatype co_T case_name constr_xs thy = 

481 
let 

482 
val {frac_types, codatatypes} = TheoryData.get thy 

483 
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs 

484 
val (co_s, co_Ts) = dest_Type co_T 

485 
val _ = 

486 
if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then () 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

487 
else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], []) 
33192  488 
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs)) 
489 
codatatypes 

490 
in TheoryData.put {frac_types = frac_types, codatatypes = codatatypes} thy end 

491 
(* typ > theory > theory *) 

492 
fun unregister_codatatype co_T = register_codatatype co_T "" [] 

493 

494 
type typedef_info = 

495 
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, 

496 
set_def: thm option, prop_of_Rep: thm, set_name: string, 

497 
Rep_inverse: thm option} 

498 

499 
(* theory > string > typedef_info *) 

500 
fun typedef_info thy s = 

501 
if is_frac_type thy (Type (s, [])) then 

502 
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, 

503 
Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac}, 

504 
set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"} 

505 
> Logic.varify, 

506 
set_name = @{const_name Frac}, Rep_inverse = NONE} 

507 
else case Typedef.get_info thy s of 

508 
SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse, 

509 
...} => 

510 
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name, 

511 
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, 

512 
set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse} 

513 
 NONE => NONE 

514 

515 
(* string > bool *) 

516 
fun is_basic_datatype s = 

517 
s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit}, 

518 
@{type_name nat}, @{type_name int}] 

519 
(* theory > string > bool *) 

520 
val is_typedef = is_some oo typedef_info 

521 
val is_real_datatype = is_some oo Datatype.get_info 

522 
(* theory > typ > bool *) 

523 
fun is_codatatype thy (T as Type (s, _)) = 

524 
not (null (AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s 

525 
> Option.map snd > these)) 

526 
 is_codatatype _ _ = false 

527 
fun is_pure_typedef thy (T as Type (s, _)) = 

528 
is_typedef thy s andalso 

529 
not (is_real_datatype thy s orelse is_codatatype thy T 

530 
orelse is_record_type T orelse is_integer_type T) 

531 
 is_pure_typedef _ _ = false 

532 
fun is_univ_typedef thy (Type (s, _)) = 

533 
(case typedef_info thy s of 

534 
SOME {set_def, prop_of_Rep, ...} => 

535 
(case set_def of 

536 
SOME thm => 

537 
try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm 

538 
 NONE => 

539 
try (fst o dest_Const o snd o HOLogic.dest_mem 

540 
o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV} 

541 
 NONE => false) 

542 
 is_univ_typedef _ _ = false 

543 
fun is_datatype thy (T as Type (s, _)) = 

544 
(is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind}) 

545 
andalso not (is_basic_datatype s) 

546 
 is_datatype _ _ = false 

547 

548 
(* theory > typ > (string * typ) list * (string * typ) *) 

549 
fun all_record_fields thy T = 

550 
let val (recs, more) = Record.get_extT_fields thy T in 

551 
recs @ more :: all_record_fields thy (snd more) 

552 
end 

553 
handle TYPE _ => [] 

554 
(* styp > bool *) 

555 
fun is_record_constr (x as (s, T)) = 

556 
String.isSuffix Record.extN s andalso 

557 
let val dataT = body_type T in 

558 
is_record_type dataT andalso 

559 
s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN 

560 
end 

561 
(* theory > typ > int *) 

562 
val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields 

563 
(* theory > string > typ > int *) 

564 
fun no_of_record_field thy s T1 = 

565 
find_index (equal s o fst) (Record.get_extT_fields thy T1 > single > op @) 

566 
(* theory > styp > bool *) 

567 
fun is_record_get thy (s, Type ("fun", [T1, _])) = 

568 
exists (equal s o fst) (all_record_fields thy T1) 

569 
 is_record_get _ _ = false 

570 
fun is_record_update thy (s, T) = 

571 
String.isSuffix Record.updateN s andalso 

572 
exists (equal (unsuffix Record.updateN s) o fst) 

573 
(all_record_fields thy (body_type T)) 

574 
handle TYPE _ => false 

575 
fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) = 

576 
(case typedef_info thy s' of 

577 
SOME {Abs_name, ...} => s = Abs_name 

578 
 NONE => false) 

579 
 is_abs_fun _ _ = false 

580 
fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) = 

581 
(case typedef_info thy s' of 

582 
SOME {Rep_name, ...} => s = Rep_name 

583 
 NONE => false) 

584 
 is_rep_fun _ _ = false 

585 

586 
(* theory > styp > styp *) 

587 
fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) = 

588 
(case typedef_info thy s' of 

589 
SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1])) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

590 
 NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])) 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

591 
 mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]) 
33192  592 

593 
(* theory > styp > bool *) 

594 
fun is_coconstr thy (s, T) = 

595 
let 

596 
val {codatatypes, ...} = TheoryData.get thy 

597 
val co_T = body_type T 

598 
val co_s = dest_Type co_T > fst 

599 
in 

600 
exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T) 

601 
(AList.lookup (op =) codatatypes co_s > Option.map snd > these) 

602 
end 

603 
handle TYPE ("dest_Type", _, _) => false 

604 
fun is_constr_like thy (s, T) = 

605 
s mem [@{const_name FunBox}, @{const_name PairBox}] orelse 

606 
let val (x as (s, T)) = (s, unbox_type T) in 

607 
Refute.is_IDT_constructor thy x orelse is_record_constr x 

608 
orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) 

609 
orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}] 

610 
orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T) 

611 
orelse is_coconstr thy x 

612 
end 

613 
fun is_constr thy (x as (_, T)) = 

614 
is_constr_like thy x 

615 
andalso not (is_basic_datatype (fst (dest_Type (body_type T)))) 

616 
(* string > bool *) 

617 
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix 

618 
val is_sel_like_and_no_discr = 

619 
String.isPrefix sel_prefix 

620 
orf (member (op =) [@{const_name fst}, @{const_name snd}]) 

621 

622 
datatype boxability = 

623 
InConstr  InSel  InExpr  InPair  InFunLHS  InFunRHS1  InFunRHS2 

624 

625 
(* boxability > boxability *) 

626 
fun in_fun_lhs_for InConstr = InSel 

627 
 in_fun_lhs_for _ = InFunLHS 

628 
fun in_fun_rhs_for InConstr = InConstr 

629 
 in_fun_rhs_for InSel = InSel 

630 
 in_fun_rhs_for InFunRHS1 = InFunRHS2 

631 
 in_fun_rhs_for _ = InFunRHS1 

632 

633 
(* extended_context > boxability > typ > bool *) 

634 
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T = 

635 
case T of 

636 
Type ("fun", _) => 

637 
boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T)) 

638 
 Type ("*", Ts) => 

639 
boxy mem [InPair, InFunRHS1, InFunRHS2] 

640 
orelse (boxy mem [InExpr, InFunLHS] 

641 
andalso exists (is_boxing_worth_it ext_ctxt InPair) 

642 
(map (box_type ext_ctxt InPair) Ts)) 

643 
 _ => false 

644 
(* extended_context > boxability > string * typ list > string *) 

645 
and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) = 

646 
case triple_lookup (type_match thy) boxes (Type z) of 

647 
SOME (SOME box_me) => box_me 

648 
 _ => is_boxing_worth_it ext_ctxt boxy (Type z) 

649 
(* extended_context > boxability > typ > typ *) 

650 
and box_type ext_ctxt boxy T = 

651 
case T of 

652 
Type (z as ("fun", [T1, T2])) => 

653 
if not (boxy mem [InConstr, InSel]) 

654 
andalso should_box_type ext_ctxt boxy z then 

655 
Type (@{type_name fun_box}, 

656 
[box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2]) 

657 
else 

658 
box_type ext_ctxt (in_fun_lhs_for boxy) T1 

659 
> box_type ext_ctxt (in_fun_rhs_for boxy) T2 

660 
 Type (z as ("*", Ts)) => 

661 
if should_box_type ext_ctxt boxy z then 

662 
Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts) 

663 
else 

664 
Type ("*", map (box_type ext_ctxt 

665 
(if boxy mem [InConstr, InSel] then boxy 

666 
else InPair)) Ts) 

667 
 _ => T 

668 

669 
(* styp > styp *) 

670 
fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T > bool_T) 

671 

672 
(* typ > int *) 

673 
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T) 

674 
(* string > int > string *) 

675 
fun nth_sel_name_for_constr_name s n = 

676 
if s = @{const_name Pair} then 

677 
if n = 0 then @{const_name fst} else @{const_name snd} 

678 
else 

679 
sel_prefix_for n ^ s 

680 
(* styp > int > styp *) 

681 
fun nth_sel_for_constr x ~1 = discr_for_constr x 

682 
 nth_sel_for_constr (s, T) n = 

683 
(nth_sel_name_for_constr_name s n, 

684 
body_type T > nth (maybe_curried_binder_types T) n) 

685 
(* extended_context > styp > int > styp *) 

686 
fun boxed_nth_sel_for_constr ext_ctxt = 

687 
apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr 

688 

689 
(* string > int *) 

690 
fun sel_no_from_name s = 

691 
if String.isPrefix discr_prefix s then 

692 
~1 

693 
else if String.isPrefix sel_prefix s then 

694 
s > unprefix sel_prefix > Int.fromString > the 

695 
else if s = @{const_name snd} then 

696 
1 

697 
else 

698 
0 

699 

700 
(* typ list > term > int > term *) 

701 
fun eta_expand _ t 0 = t 

702 
 eta_expand Ts (Abs (s, T, t')) n = 

703 
Abs (s, T, eta_expand (T :: Ts) t' (n  1)) 

704 
 eta_expand Ts t n = 

705 
fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n)) 

706 
(List.take (binder_types (fastype_of1 (Ts, t)), n)) 

707 
(list_comb (incr_boundvars n t, map Bound (n  1 downto 0))) 

708 

709 
(* term > term *) 

710 
fun extensionalize t = 

711 
case t of 

712 
(t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1 

713 
 Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) => 

714 
let val v = Var ((s, maxidx_of_term t + 1), T) in 

715 
extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2))) 

716 
end 

717 
 _ => t 

718 

719 
(* typ > term list > term *) 

720 
fun distinctness_formula T = 

721 
all_distinct_unordered_pairs_of 

722 
#> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2)) 

723 
#> List.foldr (s_conj o swap) @{const True} 

724 

725 
(* typ > term *) 

726 
fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T) 

727 
fun suc_const T = Const (@{const_name Suc}, T > T) 

728 

729 
(* theory > typ > styp list *) 

730 
fun datatype_constrs thy (T as Type (s, Ts)) = 

731 
if is_datatype thy T then 

732 
case Datatype.get_info thy s of 

733 
SOME {index, descr, ...} => 

734 
let val (_, dtyps, constrs) = AList.lookup (op =) descr index > the in 

735 
map (fn (s', Us) => 

736 
(s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us > T)) 

737 
constrs 

738 
end 

739 
 NONE => 

740 
case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of 

741 
SOME (_, xs' as (_ :: _)) => 

742 
map (apsnd (repair_constr_type thy T)) xs' 

743 
 _ => 

744 
if is_record_type T then 

745 
let 

746 
val s' = unsuffix Record.ext_typeN s ^ Record.extN 

747 
val T' = (Record.get_extT_fields thy T 

748 
> apsnd single > uncurry append > map snd) > T 

749 
in [(s', T')] end 

750 
else case typedef_info thy s of 

751 
SOME {abs_type, rep_type, Abs_name, ...} => 

752 
[(Abs_name, instantiate_type thy abs_type T rep_type > T)] 

753 
 NONE => 

754 
if T = @{typ ind} then 

755 
[dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}] 

756 
else 

757 
[] 

758 
else 

759 
[] 

760 
 datatype_constrs _ _ = [] 

761 
(* extended_context > typ > styp list *) 

762 
fun boxed_datatype_constrs (ext_ctxt as {thy, ...}) = 

763 
map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs thy 

764 
(* theory > typ > int *) 

765 
val num_datatype_constrs = length oo datatype_constrs 

766 

767 
(* string > string *) 

768 
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair} 

769 
 constr_name_for_sel_like @{const_name snd} = @{const_name Pair} 

770 
 constr_name_for_sel_like s' = original_name s' 

771 
(* extended_context > styp > styp *) 

772 
fun boxed_constr_for_sel ext_ctxt (s', T') = 

773 
let val s = constr_name_for_sel_like s' in 

774 
AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s 

775 
> the > pair s 

776 
end 

777 
(* theory > styp > term *) 

778 
fun discr_term_for_constr thy (x as (s, T)) = 

779 
let val dataT = body_type T in 

780 
if s = @{const_name Suc} then 

781 
Abs (Name.uu, dataT, 

782 
@{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0)) 

783 
else if num_datatype_constrs thy dataT >= 2 then 

784 
Const (discr_for_constr x) 

785 
else 

786 
Abs (Name.uu, dataT, @{const True}) 

787 
end 

788 

789 
(* theory > styp > term > term *) 

790 
fun discriminate_value thy (x as (_, T)) t = 

791 
case strip_comb t of 

792 
(Const x', args) => 

793 
if x = x' then @{const True} 

794 
else if is_constr_like thy x' then @{const False} 

795 
else betapply (discr_term_for_constr thy x, t) 

796 
 _ => betapply (discr_term_for_constr thy x, t) 

797 

798 
(* styp > term > term *) 

799 
fun nth_arg_sel_term_for_constr (x as (s, T)) n = 

800 
let val (arg_Ts, dataT) = strip_type T in 

801 
if dataT = nat_T then 

802 
@{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"} 

803 
else if is_pair_type dataT then 

804 
Const (nth_sel_for_constr x n) 

805 
else 

806 
let 

807 
(* int > typ > int * term *) 

808 
fun aux m (Type ("*", [T1, T2])) = 

809 
let 

810 
val (m, t1) = aux m T1 

811 
val (m, t2) = aux m T2 

812 
in (m, HOLogic.mk_prod (t1, t2)) end 

813 
 aux m T = 

814 
(m + 1, Const (nth_sel_name_for_constr_name s m, dataT > T) 

815 
$ Bound 0) 

816 
val m = fold (Integer.add o num_factors_in_type) 

817 
(List.take (arg_Ts, n)) 0 

818 
in Abs ("x", dataT, aux m (nth arg_Ts n) > snd) end 

819 
end 

820 
(* theory > styp > term > int > typ > term *) 

821 
fun select_nth_constr_arg thy x t n res_T = 

822 
case strip_comb t of 

823 
(Const x', args) => 

824 
if x = x' then nth args n 

825 
else if is_constr_like thy x' then Const (@{const_name unknown}, res_T) 

826 
else betapply (nth_arg_sel_term_for_constr x n, t) 

827 
 _ => betapply (nth_arg_sel_term_for_constr x n, t) 

828 

829 
(* theory > styp > term list > term *) 

830 
fun construct_value _ x [] = Const x 

831 
 construct_value thy (x as (s, _)) args = 

832 
let val args = map Envir.eta_contract args in 

833 
case hd args of 

834 
Const (x' as (s', _)) $ t => 

835 
if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s 

836 
andalso forall (fn (n, t') => 

837 
select_nth_constr_arg thy x t n dummyT = t') 

838 
(index_seq 0 (length args) ~~ args) then 

839 
t 

840 
else 

841 
list_comb (Const x, args) 

842 
 _ => list_comb (Const x, args) 

843 
end 

844 

845 
(* theory > typ > term > term *) 

846 
fun constr_expand thy T t = 

847 
(case head_of t of 

848 
Const x => if is_constr_like thy x then t else raise SAME () 

849 
 _ => raise SAME ()) 

850 
handle SAME () => 

851 
let 

852 
val x' as (_, T') = 

853 
if is_pair_type T then 

854 
let val (T1, T2) = HOLogic.dest_prodT T in 

855 
(@{const_name Pair}, [T1, T2] > T) 

856 
end 

857 
else 

858 
datatype_constrs thy T > the_single 

859 
val arg_Ts = binder_types T' 

860 
in 

861 
list_comb (Const x', map2 (select_nth_constr_arg thy x' t) 

862 
(index_seq 0 (length arg_Ts)) arg_Ts) 

863 
end 

864 

865 
(* (typ * int) list > typ > int *) 

866 
fun card_of_type asgns (Type ("fun", [T1, T2])) = 

867 
reasonable_power (card_of_type asgns T2) (card_of_type asgns T1) 

868 
 card_of_type asgns (Type ("*", [T1, T2])) = 

869 
card_of_type asgns T1 * card_of_type asgns T2 

870 
 card_of_type _ (Type (@{type_name itself}, _)) = 1 

871 
 card_of_type _ @{typ prop} = 2 

872 
 card_of_type _ @{typ bool} = 2 

873 
 card_of_type _ @{typ unit} = 1 

874 
 card_of_type asgns T = 

875 
case AList.lookup (op =) asgns T of 

876 
SOME k => k 

877 
 NONE => if T = @{typ bisim_iterator} then 0 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

878 
else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) 
33192  879 
(* int > (typ * int) list > typ > int *) 
880 
fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) = 

881 
let 

882 
val k1 = bounded_card_of_type max default_card asgns T1 

883 
val k2 = bounded_card_of_type max default_card asgns T2 

884 
in 

885 
if k1 = max orelse k2 = max then max 

886 
else Int.min (max, reasonable_power k2 k1) 

887 
end 

888 
 bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) = 

889 
let 

890 
val k1 = bounded_card_of_type max default_card asgns T1 

891 
val k2 = bounded_card_of_type max default_card asgns T2 

892 
in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end 

893 
 bounded_card_of_type max default_card asgns T = 

894 
Int.min (max, if default_card = ~1 then 

895 
card_of_type asgns T 

896 
else 

897 
card_of_type asgns T 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

898 
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 
33192  899 
default_card) 
900 
(* theory > int > (typ * int) list > typ > int *) 

901 
fun bounded_precise_card_of_type thy max default_card asgns T = 

902 
let 

903 
(* typ list > typ > int *) 

904 
fun aux avoid T = 

905 
(if T mem avoid then 

906 
0 

907 
else case T of 

908 
Type ("fun", [T1, T2]) => 

909 
let 

910 
val k1 = aux avoid T1 

911 
val k2 = aux avoid T2 

912 
in 

913 
if k1 = 0 orelse k2 = 0 then 0 

914 
else if k1 >= max orelse k2 >= max then max 

915 
else Int.min (max, reasonable_power k2 k1) 

916 
end 

917 
 Type ("*", [T1, T2]) => 

918 
let 

919 
val k1 = aux avoid T1 

920 
val k2 = aux avoid T2 

921 
in 

922 
if k1 = 0 orelse k2 = 0 then 0 

923 
else if k1 >= max orelse k2 >= max then max 

924 
else Int.min (max, k1 * k2) 

925 
end 

926 
 Type (@{type_name itself}, _) => 1 

927 
 @{typ prop} => 2 

928 
 @{typ bool} => 2 

929 
 @{typ unit} => 1 

930 
 Type _ => 

931 
(case datatype_constrs thy T of 

932 
[] => if is_integer_type T then 0 else raise SAME () 

933 
 constrs => 

934 
let 

935 
val constr_cards = 

936 
datatype_constrs thy T 

937 
> map (Integer.prod o map (aux (T :: avoid)) o binder_types 

938 
o snd) 

939 
in 

940 
if exists (equal 0) constr_cards then 0 

941 
else Integer.sum constr_cards 

942 
end) 

943 
 _ => raise SAME ()) 

944 
handle SAME () => AList.lookup (op =) asgns T > the_default default_card 

945 
in Int.min (max, aux [] T) end 

946 

947 
(* theory > typ > bool *) 

948 
fun is_finite_type thy = not_equal 0 o bounded_precise_card_of_type thy 1 2 [] 

949 

950 
(* term > bool *) 

951 
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 

952 
 is_ground_term (Const _) = true 

953 
 is_ground_term _ = false 

954 

955 
(* term > word > word *) 

956 
fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2) 

957 
 hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0) 

958 
 hashw_term _ = 0w0 

959 
(* term > int *) 

960 
val hash_term = Word.toInt o hashw_term 

961 

962 
(* term list > (indexname * typ) list *) 

963 
fun special_bounds ts = 

964 
fold Term.add_vars ts [] > sort (TermOrd.fast_indexname_ord o pairself fst) 

965 

966 
(* indexname * typ > term > term *) 

967 
fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) 

968 

969 
(* term > bool *) 

970 
fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _) 

971 
$ Const (@{const_name TYPE}, _)) = true 

972 
 is_arity_type_axiom _ = false 

973 
(* theory > bool > term > bool *) 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

974 
fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) = 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

975 
is_typedef_axiom thy boring t2 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

976 
 is_typedef_axiom thy boring 
33192  977 
(@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _) 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

978 
$ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) = 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

979 
boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}] 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

980 
orelse is_frac_type thy (Type (s, []))) 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

981 
andalso is_typedef thy s 
33192  982 
 is_typedef_axiom _ _ _ = false 
983 

984 
(* Distinguishes between (1) constant definition axioms, (2) type arity and 

985 
typedef axioms, and (3) other axioms, and returns the pair ((1), (3)). 

986 
Typedef axioms are uninteresting to Nitpick, because it can retrieve them 

987 
using "typedef_info". *) 

988 
(* theory > (string * term) list > string list > term list * term list *) 

989 
fun partition_axioms_by_definitionality thy axioms def_names = 

990 
let 

991 
val axioms = sort (fast_string_ord o pairself fst) axioms 

992 
val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms 

993 
val nondefs = 

994 
OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms 

995 
> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd) 

996 
in pairself (map snd) (defs, nondefs) end 

997 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

998 
(* Ideally we would check against "Complex_Main", not "Refute", but any theory 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

999 
will do as long as it contains all the "axioms" and "axiomatization" 
33192  1000 
commands. *) 
1001 
(* theory > bool *) 

1002 
fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute}) 

1003 

1004 
(* term > bool *) 

1005 
val is_plain_definition = 

1006 
let 

1007 
(* term > bool *) 

1008 
fun do_lhs t1 = 

1009 
case strip_comb t1 of 

1010 
(Const _, args) => forall is_Var args 

1011 
andalso not (has_duplicates (op =) args) 

1012 
 _ => false 

1013 
fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1 

1014 
 do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) = 

1015 
do_lhs t1 

1016 
 do_eq _ = false 

1017 
in do_eq end 

1018 

1019 
(* theory > term list * term list * term list *) 

1020 
fun all_axioms_of thy = 

1021 
let 

1022 
(* theory list > term list *) 

1023 
val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of) 

1024 
val specs = Defs.all_specifications_of (Theory.defs_of thy) 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1025 
val def_names = specs > maps snd > filter #is_def > map #name 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1026 
> OrdList.make fast_string_ord 
33192  1027 
val thys = thy :: Theory.ancestors_of thy 
1028 
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys 

1029 
val built_in_axioms = axioms_of_thys built_in_thys 

1030 
val user_axioms = axioms_of_thys user_thys 

1031 
val (built_in_defs, built_in_nondefs) = 

1032 
partition_axioms_by_definitionality thy built_in_axioms def_names 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1033 
> filter (is_typedef_axiom thy false) 
33192  1034 
val (user_defs, user_nondefs) = 
1035 
partition_axioms_by_definitionality thy user_axioms def_names 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1036 
val (built_in_nondefs, user_nondefs) = 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1037 
List.partition (is_typedef_axiom thy false) user_nondefs 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1038 
>> append built_in_nondefs 
33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33232
diff
changeset

1039 
val defs = (thy > PureThy.all_thms_of 
33192  1040 
> filter (equal Thm.definitionK o Thm.get_kind o snd) 
1041 
> map (prop_of o snd) > filter is_plain_definition) @ 

1042 
user_defs @ built_in_defs 

1043 
in (defs, built_in_nondefs, user_nondefs) end 

1044 

1045 
(* bool > styp > int option *) 

1046 
fun arity_of_built_in_const fast_descrs (s, T) = 

1047 
if s = @{const_name If} then 

1048 
if nth_range_type 3 T = @{typ bool} then NONE else SOME 3 

1049 
else case AList.lookup (op =) 

1050 
(built_in_consts 

1051 
> fast_descrs ? append built_in_descr_consts) s of 

1052 
SOME n => SOME n 

1053 
 NONE => 

1054 
case AList.lookup (op =) built_in_typed_consts (s, T) of 

1055 
SOME n => SOME n 

1056 
 NONE => 

1057 
if is_fun_type T andalso is_set_type (domain_type T) then 

1058 
AList.lookup (op =) built_in_set_consts s 

1059 
else 

1060 
NONE 

1061 
(* bool > styp > bool *) 

1062 
val is_built_in_const = is_some oo arity_of_built_in_const 

1063 

1064 
(* This function is designed to work for both real definition axioms and 

1065 
simplification rules (equational specifications). *) 

1066 
(* term > term *) 

1067 
fun term_under_def t = 

1068 
case t of 

1069 
@{const "==>"} $ _ $ t2 => term_under_def t2 

1070 
 Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1 

1071 
 @{const Trueprop} $ t1 => term_under_def t1 

1072 
 Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1 

1073 
 Abs (_, _, t') => term_under_def t' 

1074 
 t1 $ _ => term_under_def t1 

1075 
 _ => t 

1076 

1077 
(* Here we crucially rely on "Refute.specialize_type" performing a preorder 

1078 
traversal of the term, without which the wrong occurrence of a constant could 

1079 
be matched in the face of overloading. *) 

1080 
(* theory > bool > const_table > styp > term list *) 

1081 
fun def_props_for_const thy fast_descrs table (x as (s, _)) = 

1082 
if is_built_in_const fast_descrs x then 

1083 
[] 

1084 
else 

1085 
these (Symtab.lookup table s) 

1086 
> map_filter (try (Refute.specialize_type thy x)) 

1087 
> filter (equal (Const x) o term_under_def) 

1088 

1089 
(* term > term *) 

1090 
fun normalized_rhs_of thy t = 

1091 
let 

1092 
(* term > term *) 

1093 
fun aux (v as Var _) t = lambda v t 

1094 
 aux (c as Const (@{const_name TYPE}, T)) t = lambda c t 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

1095 
 aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) 
33192  1096 
val (lhs, rhs) = 
1097 
case t of 

1098 
Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2) 

1099 
 @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) => 

1100 
(t1, t2) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

1101 
 _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t]) 
33192  1102 
val args = strip_comb lhs > snd 
1103 
in fold_rev aux args rhs end 

1104 

1105 
(* theory > const_table > styp > term option *) 

1106 
fun def_of_const thy table (x as (s, _)) = 

1107 
if is_built_in_const false x orelse original_name s <> s then 

1108 
NONE 

1109 
else 

1110 
x > def_props_for_const thy false table > List.last 

1111 
> normalized_rhs_of thy > prefix_abs_vars s > SOME 

1112 
handle List.Empty => NONE 

1113 

1114 
datatype fixpoint_kind = Lfp  Gfp  NoFp 

1115 

1116 
(* term > fixpoint_kind *) 

1117 
fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t 

1118 
 fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp 

1119 
 fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp 

1120 
 fixpoint_kind_of_rhs _ = NoFp 

1121 

1122 
(* theory > const_table > term > bool *) 

1123 
fun is_mutually_inductive_pred_def thy table t = 

1124 
let 

1125 
(* term > bool *) 

1126 
fun is_good_arg (Bound _) = true 

1127 
 is_good_arg (Const (s, _)) = 

1128 
s mem [@{const_name True}, @{const_name False}, @{const_name undefined}] 

1129 
 is_good_arg _ = false 

1130 
in 

1131 
case t > strip_abs_body > strip_comb of 

1132 
(Const x, ts as (_ :: _)) => 

1133 
(case def_of_const thy table x of 

1134 
SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts 

1135 
 NONE => false) 

1136 
 _ => false 

1137 
end 

1138 
(* theory > const_table > term > term *) 

1139 
fun unfold_mutually_inductive_preds thy table = 

1140 
map_aterms (fn t as Const x => 

1141 
(case def_of_const thy table x of 

1142 
SOME t' => 

1143 
let val t' = Envir.eta_contract t' in 

1144 
if is_mutually_inductive_pred_def thy table t' then t' 

1145 
else t 

1146 
end 

1147 
 NONE => t) 

1148 
 t => t) 

1149 

1150 
(* term > string * term *) 

1151 
fun pair_for_prop t = 

1152 
case term_under_def t of 

1153 
Const (s, _) => (s, t) 

1154 
 Free _ => raise NOT_SUPPORTED "local definitions" 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

1155 
 t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) 
33192  1156 

1157 
(* (Proof.context > term list) > Proof.context > const_table *) 

1158 
fun table_for get ctxt = 

1159 
get ctxt > map pair_for_prop > AList.group (op =) > Symtab.make 

1160 

1161 
(* theory > (string * int) list *) 

1162 
fun case_const_names thy = 

1163 
Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) => 

1164 
if is_basic_datatype dtype_s then 

1165 
I 

1166 
else 

1167 
cons (case_name, AList.lookup (op =) descr index 

1168 
> the > #3 > length)) 

1169 
(Datatype.get_all thy) [] @ 

1170 
map (apsnd length o snd) (#codatatypes (TheoryData.get thy)) 

1171 

1172 
(* Proof.context > term list > const_table *) 

1173 
fun const_def_table ctxt ts = 

1174 
table_for (map prop_of o Nitpick_Defs.get) ctxt 

1175 
> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) 

1176 
(map pair_for_prop ts) 

1177 
(* term list > const_table *) 

1178 
fun const_nondef_table ts = 

1179 
fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] 

1180 
> AList.group (op =) > Symtab.make 

1181 
(* Proof.context > const_table *) 

1182 
val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) 

1183 
val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) 

1184 
(* Proof.context > const_table > const_table *) 

1185 
fun inductive_intro_table ctxt def_table = 

1186 
table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) 

1187 
def_table o prop_of) 

1188 
o Nitpick_Intros.get) ctxt 

1189 
(* theory > term list Inttab.table *) 

1190 
fun ground_theorem_table thy = 

1191 
fold ((fn @{const Trueprop} $ t1 => 

1192 
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) 

1193 
 _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty 

1194 

1195 
val basic_ersatz_table = 

1196 
[(@{const_name prod_case}, @{const_name split}), 

1197 
(@{const_name card}, @{const_name card'}), 

1198 
(@{const_name setsum}, @{const_name setsum'}), 

1199 
(@{const_name fold_graph}, @{const_name fold_graph'}), 

1200 
(@{const_name wf}, @{const_name wf'}), 

1201 
(@{const_name wf_wfrec}, @{const_name wf_wfrec'}), 

1202 
(@{const_name wfrec}, @{const_name wfrec'})] 

1203 

1204 
(* theory > (string * string) list *) 

1205 
fun ersatz_table thy = 

1206 
fold (append o snd) (#frac_types (TheoryData.get thy)) basic_ersatz_table 

1207 

1208 
(* const_table Unsynchronized.ref > string > term list > unit *) 

1209 
fun add_simps simp_table s eqs = 

1210 
Unsynchronized.change simp_table 

1211 
(Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s))) 

1212 

1213 
(* Similar to "Refute.specialize_type" but returns all matches rather than only 

1214 
the first (preorder) match. *) 

1215 
(* theory > styp > term > term list *) 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1216 
fun multi_specialize_type thy slack (x as (s, T)) t = 
33192  1217 
let 
1218 
(* term > (typ * term) list > (typ * term) list *) 

1219 
fun aux (Const (s', T')) ys = 

1220 
if s = s' then 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1221 
ys > (if AList.defined (op =) ys T' then 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1222 
I 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1223 
else 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1224 
cons (T', Refute.monomorphic_term 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1225 
(Sign.typ_match thy (T', T) Vartab.empty) t) 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1226 
handle Type.TYPE_MATCH => I 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1227 
 Refute.REFUTE _ => 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1228 
if slack then 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1229 
I 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1230 
else 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1231 
raise NOT_SUPPORTED ("too much polymorphism in \ 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1232 
\axiom involving " ^ quote s)) 
33192  1233 
else 
1234 
ys 

1235 
 aux _ ys = ys 

1236 
in map snd (fold_aterms aux t []) end 

1237 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1238 
(* theory > bool > const_table > styp > term list *) 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1239 
fun nondef_props_for_const thy slack table (x as (s, _)) = 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

1240 
these (Symtab.lookup table s) > maps (multi_specialize_type thy slack x) 
33192  1241 

1242 
(* theory > styp list > term list *) 

1243 
fun optimized_typedef_axioms thy (abs_s, abs_Ts) = 

1244 
let val abs_T = Type (abs_s, abs_Ts) in 

1245 
if is_univ_typedef thy abs_T then 

1246 
[] 

1247 
else case typedef_info thy abs_s of 

1248 
SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name, 

1249 
...} => 

1250 
let 

1251 
val rep_T = instantiate_type thy abs_type abs_T rep_type 

1252 
val rep_t = Const (Rep_name, abs_T > rep_T) 

1253 
val set_t = Const (set_name, rep_T > bool_T) 

1254 
val set_t' = 

1255 
prop_of_Rep > HOLogic.dest_Trueprop 

1256 
> Refute.specialize_type thy (dest_Const rep_t) 

1257 
> HOLogic.dest_mem > snd 

1258 
in 

1259 
[HOLogic.all_const abs_T 

1260 
$ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))] 

1261 
> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t')) 

1262 
> map HOLogic.mk_Trueprop 

1263 
end 

1264 
 NONE => [] 

1265 
end 

1266 
(* theory > styp > term *) 

1267 
fun inverse_axiom_for_rep_fun thy (x as (_, T)) = 

1268 
typedef_info thy (fst (dest_Type (domain_type T))) 

1269 
> the > #Rep_inverse > the > prop_of > Refute.specialize_type thy x 

1270 

1271 
(* theory > int * styp > term *) 

1272 
fun constr_case_body thy (j, (x as (_, T))) = 

1273 
let val arg_Ts = binder_types T in 

1274 
list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0)) 

1275 
(index_seq 0 (length arg_Ts)) arg_Ts) 

1276 
end 

1277 
(* theory > typ > int * styp > term > term *) 

1278 
fun add_constr_case thy res_T (j, x) res_t = 

1279 
Const (@{const_name If}, [bool_T, res_T, res_T] > res_T) 

1280 
$ discriminate_value thy x (Bound 0) $ constr_case_body thy (j, x) $ res_t 

1281 
(* theory > typ > typ > term *) 

1282 
fun optimized_case_def thy dataT res_T = 

1283 
let 

1284 
val xs = datatype_constrs thy dataT 

1285 
val func_Ts = map ((fn T => binder_types T > res_T) o snd) xs 

1286 
val (xs', x) = split_last xs 

1287 
in 

1288 
constr_case_body thy (1, x) 

1289 
> fold_rev (add_constr_case thy res_T) (length xs downto 2 ~~ xs') 

1290 
> fold_rev (curry absdummy) (func_Ts @ [dataT]) 

1291 
end 

1292 

1293 
(* theory > string > typ > typ > term > term *) 

1294 
fun optimized_record_get thy s rec_T res_T t = 

1295 
let val constr_x = the_single (datatype_constrs thy rec_T) in 

1296 
case no_of_record_field thy s rec_T of 

1297 
~1 => (case rec_T of 

1298 
Type (_, Ts as _ :: _) => 

1299 
let 

1300 
val rec_T' = List.last Ts 

1301 
val j = num_record_fields thy rec_T  1 

1302 
in 

1303 
select_nth_constr_arg thy constr_x t j res_T 

1304 
> optimized_record_get thy s rec_T' res_T 

1305 
end 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

1306 
 _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T], 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33202
diff
changeset

1307 
[])) 
33192  1308 
 j => select_nth_constr_arg thy constr_x t j res_T 
1309 
end 

1310 
(* theory > string > typ > term > term > term *) 

1311 
fun optimized_record_update thy s rec_T fun_t rec_t = 

1312 
let 

1313 
val constr_x as (_, constr_T) = the_single (datatype_constrs thy rec_T) 

1314 
val Ts = binder_types constr_T 

1315 
val n = length Ts 

1316 
val special_j = no_of_record_field thy s rec_T 

1317 
val ts = map2 (fn j => fn T => 

1318 
let 

1319 
val t = select_nth_constr_arg thy constr_x rec_t j T 

1320 
in 

1321 
if j = special_j then 

1322 
betapply (fun_t, t) 

1323 
else if j = n  1 andalso special_j = ~1 then 

1324 
optimized_record_update thy s 

1325 
(rec_T > dest_Type > snd > List.last) fun_t t 

1326 
else 

1327 
t 

1328 
end) (index_seq 0 n) Ts 

1329 
in list_comb (Const constr_x, ts) end 

1330 

1331 
(* Constants "c" whose definition is of the form "c == c'", where "c'" is also a 

1332 
constant, are said to be trivial. For those, we ignore the simplification 

1333 
rules and use the definition instead, to ensure that builtin symbols like 

1334 
"ord_nat_inst.less_eq_nat" are picked up correctly. *) 

1335 
(* theory > const_table > styp > bool *) 

1336 
fun has_trivial_definition thy table x = 

1337 
case def_of_const thy table x of SOME (Const _) => true  _ => false 

1338 

1339 
(* theory > const_table > string * typ > fixpoint_kind *) 

1340 
fun fixpoint_kind_of_const thy table x = 

1341 
if is_built_in_const false x then 

1342 
NoFp 

1343 
else 

1344 
fixpoint_kind_of_rhs (the (def_of_const thy table x)) 

1345 
handle Option.Option => NoFp 

1346 

1347 
(* extended_context > styp > bool *) 

1348 
fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...} 

1349 
: extended_context) x = 

1350 
not (null (def_props_for_const thy fast_descrs intro_table x)) 

1351 
andalso fixpoint_kind_of_const thy def_table x <> NoFp 

1352 
fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...} 

1353 
: extended_context) x = 

1354 
exists (fn table => not (null (def_props_for_const thy fast_descrs table x))) 

1355 
[!simp_table, psimp_table] 

1356 
fun is_inductive_pred ext_ctxt = 

1357 
is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt) 

1358 
fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) = 

1359 
(is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt 

1360 
orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) 

1361 
andf (not o has_trivial_definition thy def_table) 

1362 

1363 
(* term * term > term *) 

1364 
fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t 

1365 
 s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t 

1366 
 s_betapply p = betapply p 

1367 
(* term * term list > term *) 

1368 
val s_betapplys = Library.foldl s_betapply 

1369 

1370 
(* term > term *) 

1371 
fun lhs_of_equation t = 

1372 
case t of 

1373 
Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1 

1374 
 Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1 

1375 
 @{const "==>"} $ _ $ t2 => lhs_of_equation t2 

1376 
 @{const Trueprop} $ t1 => lhs_of_equation t1 

1377 
 Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1 

1378 
 Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1 

1379 
 @{const "op >"} $ _ $ t2 => lhs_of_equation t2 

1380 
 _ => NONE 

1381 
(* theory > term > bool *) 

1382 
fun is_constr_pattern _ (Bound _) = true 

1383 
 is_constr_pattern thy t = 

1384 
case strip_comb t of 

1385 
(Const (x as (s, _)), args) => 

1386 
is_constr_like thy x andalso forall (is_constr_pattern thy) args 

1387 
 _ => false 

1388 
fun is_constr_pattern_lhs thy t = 

1389 
forall (is_constr_pattern thy) (snd (strip_comb t)) 

1390 
fun is_constr_pattern_formula thy t = 

1391 
case lhs_of_equation t of 

1392 
SOME t' => is_constr_pattern_lhs thy t' 

1393 
 NONE => false 

1394 

1395 
val unfold_max_depth = 63 

1396 
val axioms_max_depth = 63 

1397 

1398 
(* extended_context > term > term *) 

1399 
fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs, 

1400 
case_names, def_table, ground_thm_table, 

1401 
ersatz_table, ...}) = 