author  blanchet 
Fri, 08 Sep 2017 00:03:06 +0200  
changeset 66635  dbe1dc1f0016 
parent 66634  56456f388867 
child 66646  383d8e388d1b 
permissions  rwrr 
64389  1 
(* Title: HOL/Nunchaku/Tools/nunchaku_collect.ML 
66614
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 12 years
blanchet
parents:
65458
diff
changeset

2 
Author: Jasmin Blanchette, VU Amsterdam 
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 12 years
blanchet
parents:
65458
diff
changeset

3 
Copyright 2015, 2016, 2017 
64389  4 

5 
Collecting of Isabelle/HOL definitions etc. for Nunchaku. 

6 
*) 

7 

8 
signature NUNCHAKU_COLLECT = 

9 
sig 

10 
val dest_co_datatype_case: Proof.context > string * typ > (string * typ) list 

11 

12 
type isa_type_spec = 

13 
{abs_typ: typ, 

14 
rep_typ: typ, 

15 
wrt: term, 

16 
abs: term, 

17 
rep: term} 

18 

19 
type isa_co_data_spec = 

20 
{typ: typ, 

21 
ctrs: term list} 

22 

23 
type isa_const_spec = 

24 
{const: term, 

25 
props: term list} 

26 

27 
type isa_rec_spec = 

28 
{const: term, 

29 
props: term list, 

30 
pat_complete: bool} 

31 

32 
type isa_consts_spec = 

33 
{consts: term list, 

34 
props: term list} 

35 

36 
datatype isa_command = 

37 
ITVal of typ * (int option * int option) 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

38 
 ITypedef of isa_type_spec 
64389  39 
 IQuotient of isa_type_spec 
40 
 ICoData of BNF_Util.fp_kind * isa_co_data_spec list 

41 
 IVal of term 

42 
 ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list 

43 
 IRec of isa_rec_spec list 

44 
 ISpec of isa_consts_spec 

45 
 IAxiom of term 

46 
 IGoal of term 

47 
 IEval of term 

48 

49 
type isa_problem = 

50 
{commandss: isa_command list list, 

51 
sound: bool, 

52 
complete: bool} 

53 

54 
exception CYCLIC_DEPS of unit 

55 
exception TOO_DEEP_DEPS of unit 

56 
exception TOO_META of term 

57 
exception UNEXPECTED_POLYMORPHISM of term 

58 
exception UNEXPECTED_VAR of term 

59 
exception UNSUPPORTED_FUNC of term 

60 

61 
val isa_problem_of_subgoal: Proof.context > bool > ((string * typ) option * bool option) list > 

62 
(term option * bool) list > (typ option * (int option * int option)) list > bool > 

63 
Time.time > term list > term list > term > term list * isa_problem 

64 
val pat_completes_of_isa_problem: isa_problem > term list 

65 
val str_of_isa_problem: Proof.context > isa_problem > string 

66 
end; 

67 

68 
structure Nunchaku_Collect : NUNCHAKU_COLLECT = 

69 
struct 

70 

71 
open Nunchaku_Util; 

72 

73 
type isa_type_spec = 

74 
{abs_typ: typ, 

75 
rep_typ: typ, 

76 
wrt: term, 

77 
abs: term, 

78 
rep: term}; 

79 

80 
type isa_co_data_spec = 

81 
{typ: typ, 

82 
ctrs: term list}; 

83 

84 
type isa_const_spec = 

85 
{const: term, 

86 
props: term list}; 

87 

88 
type isa_rec_spec = 

89 
{const: term, 

90 
props: term list, 

91 
pat_complete: bool}; 

92 

93 
type isa_consts_spec = 

94 
{consts: term list, 

95 
props: term list}; 

96 

97 
datatype isa_command = 

98 
ITVal of typ * (int option * int option) 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

99 
 ITypedef of isa_type_spec 
64389  100 
 IQuotient of isa_type_spec 
101 
 ICoData of BNF_Util.fp_kind * isa_co_data_spec list 

102 
 IVal of term 

103 
 ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list 

104 
 IRec of isa_rec_spec list 

105 
 ISpec of isa_consts_spec 

106 
 IAxiom of term 

107 
 IGoal of term 

108 
 IEval of term; 

109 

110 
type isa_problem = 

111 
{commandss: isa_command list list, 

112 
sound: bool, 

113 
complete: bool}; 

114 

115 
exception CYCLIC_DEPS of unit; 

116 
exception TOO_DEEP_DEPS of unit; 

117 
exception TOO_META of term; 

118 
exception UNEXPECTED_POLYMORPHISM of term; 

119 
exception UNEXPECTED_VAR of term; 

120 
exception UNSUPPORTED_FUNC of term; 

121 

122 
fun str_of_and_list str_of_elem = 

123 
map str_of_elem #> space_implode ("\nand "); 

124 

125 
val key_of_typ = 

126 
let 

127 
fun key_of (Type (s, [])) = s 

128 
 key_of (Type (s, Ts)) = s ^ "(" ^ commas (map key_of Ts) ^ ")" 

129 
 key_of (TFree (s, _)) = s; 

130 
in 

131 
prefix "y" o key_of 

132 
end; 

133 

134 
fun key_of_const ctxt = 

135 
let 

136 
val thy = Proof_Context.theory_of ctxt; 

137 

138 
fun key_of (Const (x as (s, _))) = 

139 
(case Sign.const_typargs thy x of 

140 
[] => s 

141 
 Ts => s ^ "(" ^ commas (map key_of_typ Ts) ^ ")") 

142 
 key_of (Free (s, _)) = s; 

143 
in 

144 
prefix "t" o key_of 

145 
end; 

146 

147 
val add_type_keys = fold_subtypes (insert (op =) o key_of_typ); 

148 

149 
fun add_aterm_keys ctxt t = 

150 
if is_Const t orelse is_Free t then insert (op =) (key_of_const ctxt t) else I; 

151 

152 
fun add_keys ctxt t = 

153 
fold_aterms (add_aterm_keys ctxt) t 

154 
#> fold_types add_type_keys t; 

155 

156 
fun close_form except t = 

157 
fold (fn ((s, i), T) => fn t' => 

158 
HOLogic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) 

159 
(Term.add_vars t [] > subtract (op =) except) t; 

160 

161 
(* "imp_conjL[symmetric]" is important for inductive predicates with multiple assumptions. *) 

162 
val basic_defs = 

163 
@{thms Ball_def[abs_def] Bex_def[abs_def] case_bool_if Ex1_def[abs_def] 

164 
imp_conjL[symmetric, abs_def] Let_def[abs_def] rmember_def[symmetric, abs_def]}; 

165 

166 
fun unfold_basic_def ctxt = 

167 
let val thy = Proof_Context.theory_of ctxt in 

168 
Pattern.rewrite_term thy (map (Logic.dest_equals o Thm.prop_of) basic_defs) [] 

169 
end; 

170 

171 
val has_polymorphism = exists_type (exists_subtype is_TVar); 

172 

173 
fun whack_term thy whacks = 

174 
let 

175 
fun whk t = 

176 
if triple_lookup (term_match thy o swap) whacks t = SOME true then 

177 
Const (@{const_name unreachable}, fastype_of t) 

178 
else 

179 
(case t of 

180 
u $ v => whk u $ whk v 

181 
 Abs (s, T, u) => Abs (s, T, whk u) 

182 
 _ => t); 

183 
in 

184 
whk 

185 
end; 

186 

187 
fun preprocess_term_basic falsify ctxt whacks t = 

188 
let val thy = Proof_Context.theory_of ctxt in 

189 
if has_polymorphism t then 

190 
raise UNEXPECTED_POLYMORPHISM t 

191 
else 

192 
t 

193 
> attach_typeS 

194 
> whack_term thy whacks 

195 
> Object_Logic.atomize_term ctxt 

196 
> tap (fn t' => fastype_of t' <> @{typ prop} orelse raise TOO_META t) 

197 
> falsify ? HOLogic.mk_not 

198 
> unfold_basic_def ctxt 

199 
end; 

200 

201 
val check_closed = tap (fn t => null (Term.add_vars t []) orelse raise UNEXPECTED_VAR t); 

202 

203 
val preprocess_prop = close_form [] oooo preprocess_term_basic; 

204 
val preprocess_closed_term = check_closed ooo preprocess_term_basic false; 

205 

206 
val is_type_builtin = member (op =) [@{type_name bool}, @{type_name fun}]; 

207 

208 
val is_const_builtin = 

209 
member (op =) [@{const_name All}, @{const_name conj}, @{const_name disj}, @{const_name Eps}, 

210 
@{const_name HOL.eq}, @{const_name Ex}, @{const_name False}, @{const_name If}, 

211 
@{const_name implies}, @{const_name Not}, @{const_name The}, @{const_name The_unsafe}, 

212 
@{const_name True}]; 

213 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

214 
datatype type_classification = Builtin  TVal  Typedef  Quotient  Co_Datatype; 
64389  215 

216 
fun classify_type_name ctxt T_name = 

217 
if is_type_builtin T_name then 

218 
Builtin 

219 
else if T_name = @{type_name itself} then 

220 
Co_Datatype 

221 
else 

222 
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of 

223 
SOME _ => Co_Datatype 

224 
 NONE => 

225 
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of 

226 
SOME _ => Co_Datatype 

227 
 NONE => 

228 
(case Quotient_Info.lookup_quotients ctxt T_name of 

229 
SOME _ => Quotient 

230 
 NONE => 

231 
if T_name = @{type_name set} then 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

232 
Typedef 
64389  233 
else 
234 
(case Typedef.get_info ctxt T_name of 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

235 
_ :: _ => Typedef 
64389  236 
 [] => TVal)))); 
237 

238 
fun fp_kind_of_ctr_sugar_kind Ctr_Sugar.Codatatype = BNF_Util.Greatest_FP 

239 
 fp_kind_of_ctr_sugar_kind _ = BNF_Util.Least_FP; 

240 

241 
fun mutual_co_datatypes_of ctxt (T_name, Ts) = 

242 
(if T_name = @{type_name itself} then 

243 
(BNF_Util.Least_FP, [@{typ "'a itself"}], [[@{const Pure.type ('a)}]]) 

244 
else 

245 
let 

246 
val (fp, ctr_sugars) = 

247 
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of 

248 
SOME (fp_sugar as {fp, fp_res = {Ts, ...}, ...}) => 

249 
(fp, 

250 
(case Ts of 

251 
[_] => [fp_sugar] 

252 
 _ => map (the o BNF_FP_Def_Sugar.fp_sugar_of ctxt o fst o dest_Type) Ts) 

253 
> map (#ctr_sugar o #fp_ctr_sugar)) 

254 
 NONE => 

255 
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of 

256 
SOME (ctr_sugar as {kind, ...}) => 

257 
(* Any freely constructed type that is not a codatatype is considered a datatype. This 

258 
is sound (but incomplete) for model finding. *) 

259 
(fp_kind_of_ctr_sugar_kind kind, [ctr_sugar]))); 

260 
in 

261 
(fp, map #T ctr_sugars, map #ctrs ctr_sugars) 

262 
end) 

263 
> @{apply 3(2)} (map ((fn Type (s, _) => Type (s, Ts)))) 

264 
> @{apply 3(3)} (map (map (Ctr_Sugar.mk_ctr Ts))); 

265 

66624  266 
fun typedef_of ctxt T_name = 
64389  267 
if T_name = @{type_name set} then 
268 
let 

269 
val A = Logic.varifyT_global @{typ 'a}; 

270 
val absT = Type (@{type_name set}, [A]); 

271 
val repT = A > HOLogic.boolT; 

66624  272 
val pred = Abs (Name.uu, repT, @{const True}); 
64389  273 
val abs = Const (@{const_name Collect}, repT > absT); 
274 
val rep = Const (@{const_name rmember}, absT > repT); 

275 
in 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

276 
(absT, repT, pred, abs, rep) 
64389  277 
end 
278 
else 

279 
(case Typedef.get_info ctxt T_name of 

280 
(* When several entries are returned, it shouldn't matter much which one we take (according to 

281 
Florian Haftmann). The "Logic.varifyT_global" calls are a workaround because these types' 

282 
variables sometimes clash with locally fixed type variables. *) 

283 
({abs_type, rep_type, Abs_name, Rep_name, ...}, {Rep, ...}) :: _ => 

284 
let 

285 
val absT = Logic.varifyT_global abs_type; 

286 
val repT = Logic.varifyT_global rep_type; 

66624  287 
val set = Thm.prop_of Rep 
64389  288 
> HOLogic.dest_Trueprop 
289 
> HOLogic.dest_mem 

290 
> snd; 

66624  291 
val pred = Abs (Name.uu, repT, HOLogic.mk_mem (Bound 0, set)); 
64389  292 
val abs = Const (Abs_name, repT > absT); 
293 
val rep = Const (Rep_name, absT > repT); 

294 
in 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

295 
(absT, repT, pred, abs, rep) 
64389  296 
end); 
297 

66624  298 
fun quotient_of ctxt T_name = 
64412  299 
(case Quotient_Info.lookup_quotients ctxt T_name of 
66624  300 
SOME {equiv_rel, qtyp, rtyp, quot_thm, ...} => 
301 
let val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm in 

64412  302 
(qtyp, rtyp, equiv_rel, abs, rep) 
303 
end); 

304 

64389  305 
fun is_co_datatype_ctr ctxt (s, T) = 
306 
(case body_type T of 

307 
Type (fpT_name, Ts) => 

308 
classify_type_name ctxt fpT_name = Co_Datatype andalso 

309 
let 

310 
val ctrs = 

311 
if fpT_name = @{type_name itself} then 

312 
[Const (@{const_name Pure.type}, @{typ "'a itself"})] 

313 
else 

314 
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of 

315 
SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} => ctrs 

316 
 NONE => 

317 
(case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of 

318 
SOME {ctrs, ...} => ctrs 

319 
 _ => [])); 

320 

321 
fun is_right_ctr (t' as Const (s', _)) = 

322 
s = s' andalso fastype_of (Ctr_Sugar.mk_ctr Ts t') = T; 

323 
in 

324 
exists is_right_ctr ctrs 

325 
end 

326 
 _ => false); 

327 

328 
fun dest_co_datatype_case ctxt (s, T) = 

329 
let val thy = Proof_Context.theory_of ctxt in 

330 
(case strip_fun_type (Sign.the_const_type thy s) of 

331 
(gen_branch_Ts, gen_body_fun_T) => 

332 
(case gen_body_fun_T of 

333 
Type (@{type_name fun}, [Type (fpT_name, _), _]) => 

334 
if classify_type_name ctxt fpT_name = Co_Datatype then 

335 
let 

336 
val Type (_, fpTs) = domain_type (funpow (length gen_branch_Ts) range_type T); 

337 
val (ctrs0, Const (case_name, _)) = 

338 
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of 

339 
SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, casex, ...}, ...}, ...} => (ctrs, casex) 

340 
 NONE => 

341 
(case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of 

342 
SOME {ctrs, casex, ...} => (ctrs, casex))); 

343 
in 

344 
if s = case_name then map (dest_Const o Ctr_Sugar.mk_ctr fpTs) ctrs0 

345 
else raise Fail "noncase" 

346 
end 

347 
else 

348 
raise Fail "noncase")) 

349 
end; 

350 

351 
val is_co_datatype_case = can o dest_co_datatype_case; 

352 

66624  353 
fun is_quotient_abs ctxt (s, T) = 
64389  354 
(case T of 
355 
Type (@{type_name fun}, [_, Type (absT_name, _)]) => 

356 
classify_type_name ctxt absT_name = Quotient andalso 

66624  357 
(case quotient_of ctxt absT_name of 
64389  358 
(_, _, _, Const (s', _), _) => s' = s) 
359 
 _ => false); 

360 

66624  361 
fun is_quotient_rep ctxt (s, T) = 
64389  362 
(case T of 
363 
Type (@{type_name fun}, [Type (absT_name, _), _]) => 

364 
classify_type_name ctxt absT_name = Quotient andalso 

66624  365 
(case quotient_of ctxt absT_name of 
64389  366 
(_, _, _, _, Const (s', _)) => s' = s) 
367 
 _ => false); 

368 

66624  369 
fun is_maybe_typedef_abs ctxt absT_name s = 
64389  370 
if absT_name = @{type_name set} then 
371 
s = @{const_name Collect} 

372 
else 

66624  373 
(case try (typedef_of ctxt) absT_name of 
64389  374 
SOME (_, _, _, Const (s', _), _) => s' = s 
375 
 NONE => false); 

376 

66624  377 
fun is_maybe_typedef_rep ctxt absT_name s = 
64389  378 
if absT_name = @{type_name set} then 
379 
s = @{const_name rmember} 

380 
else 

66624  381 
(case try (typedef_of ctxt) absT_name of 
64389  382 
SOME (_, _, _, _, Const (s', _)) => s' = s 
383 
 NONE => false); 

384 

66624  385 
fun is_typedef_abs ctxt (s, T) = 
64389  386 
(case T of 
387 
Type (@{type_name fun}, [_, Type (absT_name, _)]) => 

66624  388 
classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_abs ctxt absT_name s 
64389  389 
 _ => false); 
390 

66624  391 
fun is_typedef_rep ctxt (s, T) = 
64389  392 
(case T of 
393 
Type (@{type_name fun}, [Type (absT_name, _), _]) => 

66624  394 
classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_rep ctxt absT_name s 
64389  395 
 _ => false); 
396 

66624  397 
fun is_stale_typedef_abs ctxt (s, T) = 
64389  398 
(case T of 
399 
Type (@{type_name fun}, [_, Type (absT_name, _)]) => 

66624  400 
classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_abs ctxt absT_name s 
64389  401 
 _ => false); 
402 

66624  403 
fun is_stale_typedef_rep ctxt (s, T) = 
64389  404 
(case T of 
405 
Type (@{type_name fun}, [Type (absT_name, _), _]) => 

66624  406 
classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_rep ctxt absT_name s 
64389  407 
 _ => false); 
408 

409 
fun instantiate_constant_types_in_term ctxt csts target = 

410 
let 

411 
val thy = Proof_Context.theory_of ctxt; 

412 

413 
fun try_const _ _ (res as SOME _) = res 

414 
 try_const (s', T') cst NONE = 

415 
(case cst of 

416 
Const (s, T) => 

417 
if s = s' then 

418 
SOME (Sign.typ_match thy (T', T) Vartab.empty) 

419 
handle Type.TYPE_MATCH => NONE 

420 
else 

421 
NONE 

422 
 _ => NONE); 

423 

424 
fun subst_for (Const x) = fold (try_const x) csts NONE 

425 
 subst_for (t as Free _) = if member (op aconv) csts t then SOME Vartab.empty else NONE 

426 
 subst_for (t1 $ t2) = (case subst_for t1 of SOME subst => SOME subst  NONE => subst_for t2) 

427 
 subst_for (Abs (_, _, t')) = subst_for t' 

428 
 subst_for _ = NONE; 

429 
in 

430 
(case subst_for target of 

431 
SOME subst => Envir.subst_term_types subst target 

432 
 NONE => raise Type.TYPE_MATCH) 

433 
end; 

434 

435 
datatype card = One  Fin  Fin_or_Inf  Inf 

436 

437 
(* Similar to "ATP_Util.tiny_card_of_type". *) 

438 
fun card_of_type ctxt = 

439 
let 

440 
fun max_card Inf _ = Inf 

441 
 max_card _ Inf = Inf 

442 
 max_card Fin_or_Inf _ = Fin_or_Inf 

443 
 max_card _ Fin_or_Inf = Fin_or_Inf 

444 
 max_card Fin _ = Fin 

445 
 max_card _ Fin = Fin 

446 
 max_card One One = One; 

447 

448 
fun card_of avoid T = 

449 
if member (op =) avoid T then 

450 
Inf 

451 
else 

452 
(case T of 

453 
TFree _ => Fin_or_Inf 

454 
 TVar _ => Inf 

455 
 Type (@{type_name fun}, [T1, T2]) => 

456 
(case (card_of avoid T1, card_of avoid T2) of 

457 
(_, One) => One 

458 
 (k1, k2) => max_card k1 k2) 

459 
 Type (@{type_name prod}, [T1, T2]) => 

460 
(case (card_of avoid T1, card_of avoid T2) of 

461 
(k1, k2) => max_card k1 k2) 

462 
 Type (@{type_name set}, [T']) => card_of avoid (T' > HOLogic.boolT) 

463 
 Type (T_name, Ts) => 

464 
(case try (mutual_co_datatypes_of ctxt) (T_name, Ts) of 

465 
NONE => Inf 

466 
 SOME (_, fpTs, ctrss) => 

467 
(case ctrss of [[_]] => One  _ => Fin) 

468 
> fold (fold (fold (max_card o card_of (fpTs @ avoid)) o binder_types o fastype_of)) 

469 
ctrss)); 

470 
in 

471 
card_of [] 

472 
end; 

473 

474 
fun int_of_classif Spec_Rules.Equational = 1 

475 
 int_of_classif Spec_Rules.Inductive = 2 

476 
 int_of_classif Spec_Rules.Co_Inductive = 3 

477 
 int_of_classif Spec_Rules.Unknown = 4; 

478 

479 
val classif_ord = int_ord o apply2 int_of_classif; 

480 

481 
fun spec_rules_of ctxt (x as (s, T)) = 

482 
let 

483 
val thy = Proof_Context.theory_of ctxt; 

484 

485 
fun subst_of t0 = 

486 
try (Sign.typ_match thy (fastype_of t0, T)) Vartab.empty; 

487 

488 
fun process_spec _ (res as SOME _) = res 

489 
 process_spec (classif, (ts0, ths as _ :: _)) NONE = 

490 
(case get_first subst_of ts0 of 

491 
SOME subst => 

492 
(let 

493 
val ts = map (Envir.subst_term_types subst) ts0; 

494 
val poly_props = map Thm.prop_of ths; 

495 
val props = map (instantiate_constant_types_in_term ctxt ts) poly_props; 

496 
in 

497 
if exists (exists (exists_type (exists_subtype is_TVar))) [ts, props] then NONE 

498 
else SOME (classif, ts, props, poly_props) 

499 
end 

500 
handle Type.TYPE_MATCH => NONE) 

501 
 NONE => NONE) 

502 
 process_spec _ NONE = NONE; 

503 

504 
fun spec_rules () = 

505 
Spec_Rules.retrieve ctxt (Const x) 

506 
> sort (classif_ord o apply2 fst); 

507 

508 
val specs = 

509 
if s = @{const_name The} then 

510 
[(Spec_Rules.Unknown, ([Logic.varify_global @{term The}], [@{thm theI_unique}]))] 

511 
else if s = @{const_name finite} then 

512 
let val card = card_of_type ctxt T in 

513 
if card = Inf orelse card = Fin_or_Inf then 

514 
spec_rules () 

515 
else 

516 
[(Spec_Rules.Equational, ([Logic.varify_global @{term finite}], 

517 
[Skip_Proof.make_thm thy (Logic.varify_global @{prop "finite A = True"})]))] 

518 
end 

519 
else 

520 
spec_rules (); 

521 
in 

522 
fold process_spec specs NONE 

523 
end; 

524 

525 
fun lhs_of_equation (Const (@{const_name Pure.eq}, _) $ t $ _) = t 

526 
 lhs_of_equation (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _)) = t; 

527 

528 
fun specialize_definition_type thy x def0 = 

529 
let 

530 
val def = specialize_type thy x def0; 

531 
val lhs = lhs_of_equation def; 

532 
in 

533 
if exists_Const (curry (op =) x) lhs then def else raise Fail "cannot specialize" 

534 
end; 

535 

536 
fun definition_of thy (x as (s, _)) = 

537 
Defs.specifications_of (Theory.defs_of thy) (Defs.Const, s) 

538 
> map_filter #def 

539 
> map_filter (try (specialize_definition_type thy x o Thm.prop_of o Thm.axiom thy)) 

540 
> try hd; 

541 

542 
fun is_builtin_theory thy_id = 

543 
Context.subthy_id (thy_id, Context.theory_id @{theory Hilbert_Choice}); 

544 

545 
val orphan_axioms_of = 

546 
Spec_Rules.get 

547 
#> filter (curry (op =) Spec_Rules.Unknown o fst) 

548 
#> map snd 

549 
#> filter (null o fst) 

550 
#> maps snd 

65458  551 
#> filter_out (is_builtin_theory o Thm.theory_id) 
64389  552 
#> map Thm.prop_of; 
553 

554 
fun keys_of _ (ITVal (T, _)) = [key_of_typ T] 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

555 
 keys_of _ (ITypedef {abs_typ, ...}) = [key_of_typ abs_typ] 
64389  556 
 keys_of _ (IQuotient {abs_typ, ...}) = [key_of_typ abs_typ] 
557 
 keys_of _ (ICoData (_, specs)) = map (key_of_typ o #typ) specs 

558 
 keys_of ctxt (IVal const) = [key_of_const ctxt const] 

559 
 keys_of ctxt (ICoPred (_, _, specs)) = map (key_of_const ctxt o #const) specs 

560 
 keys_of ctxt (IRec specs) = map (key_of_const ctxt o #const) specs 

561 
 keys_of ctxt (ISpec {consts, ...}) = map (key_of_const ctxt) consts 

562 
 keys_of _ (IAxiom _) = [] 

563 
 keys_of _ (IGoal _) = [] 

564 
 keys_of _ (IEval _) = []; 

565 

566 
fun co_data_spec_deps_of ctxt ({ctrs, ...} : isa_co_data_spec) = 

567 
fold (add_keys ctxt) ctrs []; 

568 
fun const_spec_deps_of ctxt consts props = 

569 
fold (add_keys ctxt) props [] > subtract (op =) (map (key_of_const ctxt) consts); 

570 
fun consts_spec_deps_of ctxt {consts, props} = 

571 
fold (add_keys ctxt) props [] > subtract (op =) (map (key_of_const ctxt) consts); 

572 

573 
fun deps_of _ (ITVal _) = [] 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

574 
 deps_of ctxt (ITypedef {wrt, ...}) = add_keys ctxt wrt [] 
64389  575 
 deps_of ctxt (IQuotient {wrt, ...}) = add_keys ctxt wrt [] 
576 
 deps_of ctxt (ICoData (_, specs)) = maps (co_data_spec_deps_of ctxt) specs 

577 
 deps_of _ (IVal const) = add_type_keys (fastype_of const) [] 

578 
 deps_of ctxt (ICoPred (_, _, specs)) = 

579 
maps (const_spec_deps_of ctxt (map #const specs) o #props) specs 

580 
 deps_of ctxt (IRec specs) = maps (const_spec_deps_of ctxt (map #const specs) o #props) specs 

581 
 deps_of ctxt (ISpec spec) = consts_spec_deps_of ctxt spec 

582 
 deps_of ctxt (IAxiom prop) = add_keys ctxt prop [] 

583 
 deps_of ctxt (IGoal prop) = add_keys ctxt prop [] 

584 
 deps_of ctxt (IEval t) = add_keys ctxt t []; 

585 

586 
fun consts_of_rec_or_spec (IRec specs) = map #const specs 

587 
 consts_of_rec_or_spec (ISpec {consts, ...}) = consts; 

588 

589 
fun props_of_rec_or_spec (IRec specs) = maps #props specs 

590 
 props_of_rec_or_spec (ISpec {props, ...}) = props; 

591 

592 
fun merge_two_rec_or_spec cmd cmd' = 

593 
ISpec {consts = consts_of_rec_or_spec cmd @ consts_of_rec_or_spec cmd', 

594 
props = props_of_rec_or_spec cmd @ props_of_rec_or_spec cmd'}; 

595 

596 
fun merge_two (ICoData (fp, specs)) (ICoData (fp', specs'), complete) = 

597 
(ICoData (BNF_Util.case_fp fp fp fp', specs @ specs'), complete andalso fp = fp') 

598 
 merge_two (IRec specs) (IRec specs', complete) = (IRec (specs @ specs'), complete) 

599 
 merge_two (cmd as IRec _) (cmd' as ISpec _, complete) = 

600 
(merge_two_rec_or_spec cmd cmd', complete) 

601 
 merge_two (cmd as ISpec _) (cmd' as IRec _, complete) = 

602 
(merge_two_rec_or_spec cmd cmd', complete) 

603 
 merge_two (cmd as ISpec _) (cmd' as ISpec _, complete) = 

604 
(merge_two_rec_or_spec cmd cmd', complete) 

605 
 merge_two _ _ = raise CYCLIC_DEPS (); 

606 

607 
fun sort_isa_commands_topologically ctxt cmds = 

608 
let 

609 
fun normal_pairs [] = [] 

610 
 normal_pairs (all as normal :: _) = map (rpair normal) all; 

611 

612 
fun add_node [] _ = I 

613 
 add_node (normal :: _) cmd = Graph.new_node (normal, cmd); 

614 

615 
fun merge_scc (cmd :: cmds) complete = fold merge_two cmds (cmd, complete); 

616 

617 
fun sort_problem (cmds, complete) = 

618 
let 

619 
val keyss = map (keys_of ctxt) cmds; 

620 
val normal_keys = Symtab.make (maps normal_pairs keyss); 

621 
val normalize = Symtab.lookup normal_keys; 

622 

623 
fun add_deps [] _ = I 

624 
 add_deps (normal :: _) cmd = 

625 
let 

626 
val deps = deps_of ctxt cmd 

627 
> map_filter normalize 

628 
> remove (op =) normal; 

629 
in 

630 
fold (fn dep => Graph.add_edge (dep, normal)) deps 

631 
end; 

632 

633 
val cmd_of_key = the o AList.lookup (op =) (map hd keyss ~~ cmds); 

634 

635 
val G = Graph.empty 

636 
> fold2 add_node keyss cmds 

637 
> fold2 add_deps keyss cmds; 

638 

639 
val cmd_sccs = rev (Graph.strong_conn G) 

640 
> map (map cmd_of_key); 

641 
in 

642 
if exists (can (fn _ :: _ :: _ => ())) cmd_sccs then 

643 
sort_problem (fold_map merge_scc cmd_sccs complete) 

644 
else 

645 
(Graph.schedule (K snd) G, complete) 

646 
end; 

647 

648 
val typedecls = filter (can (fn ITVal _ => ())) cmds; 

649 
val (mixed, complete) = 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

650 
(filter (can (fn ITypedef _ => ()  IQuotient _ => ()  ICoData _ => ()  IVal _ => () 
64389  651 
 ICoPred _ => ()  IRec _ => ()  ISpec _ => ())) cmds, true) 
652 
> sort_problem; 

653 
val axioms = filter (can (fn IAxiom _ => ())) cmds; 

654 
val goals = filter (can (fn IGoal _ => ())) cmds; 

655 
val evals = filter (can (fn IEval _ => ())) cmds; 

656 
in 

657 
(typedecls @ mixed @ axioms @ goals @ evals, complete) 

658 
end; 

659 

660 
fun group_of (ITVal _) = 1 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

661 
 group_of (ITypedef _) = 2 
64389  662 
 group_of (IQuotient _) = 3 
663 
 group_of (ICoData _) = 4 

664 
 group_of (IVal _) = 5 

665 
 group_of (ICoPred _) = 6 

666 
 group_of (IRec _) = 7 

667 
 group_of (ISpec _) = 8 

668 
 group_of (IAxiom _) = 9 

669 
 group_of (IGoal _) = 10 

670 
 group_of (IEval _) = 11; 

671 

672 
fun group_isa_commands [] = [] 

673 
 group_isa_commands [cmd] = [[cmd]] 

674 
 group_isa_commands (cmd :: cmd' :: cmds) = 

675 
let val (group :: groups) = group_isa_commands (cmd' :: cmds) in 

676 
if group_of cmd = group_of cmd' then 

677 
(cmd :: group) :: groups 

678 
else 

679 
[cmd] :: (group :: groups) 

680 
end; 

681 

682 
fun defined_by (Const (@{const_name All}, _) $ t) = defined_by t 

683 
 defined_by (Abs (_, _, t)) = defined_by t 

684 
 defined_by (@{const implies} $ _ $ u) = defined_by u 

685 
 defined_by (Const (@{const_name HOL.eq}, _) $ t $ _) = head_of t 

686 
 defined_by t = head_of t; 

687 

688 
fun partition_props [_] props = SOME [props] 

689 
 partition_props consts props = 

690 
let 

691 
val propss = map (fn const => filter (fn prop => defined_by prop aconv const) props) consts; 

692 
in 

693 
if eq_set (op aconv) (props, flat propss) andalso forall (not o null) propss then SOME propss 

694 
else NONE 

695 
end; 

696 

697 
fun hol_concl_head (Const (@{const_name All}, _) $ Abs (_, _, t)) = hol_concl_head t 

698 
 hol_concl_head (Const (@{const_name implies}, _) $ _ $ t) = hol_concl_head t 

699 
 hol_concl_head (t $ _) = hol_concl_head t 

700 
 hol_concl_head t = t; 

701 

702 
fun is_inductive_set_intro t = 

703 
(case hol_concl_head t of 

704 
Const (@{const_name rmember}, _) => true 

705 
 _ => false); 

706 

707 
exception NO_TRIPLE of unit; 

708 

709 
fun triple_for_intro_rule ctxt x rule = 

710 
let 

711 
val (prems, concl) = Logic.strip_horn rule 

712 
>> map (Object_Logic.atomize_term ctxt) 

713 
> Object_Logic.atomize_term ctxt; 

714 

715 
val (mains, sides) = List.partition (exists_Const (curry (op =) x)) prems; 

716 

717 
val is_right_head = curry (op aconv) (Const x) o head_of; 

718 
in 

719 
if forall is_right_head mains then (sides, mains, concl) else raise NO_TRIPLE () 

720 
end; 

721 

722 
val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb; 

723 

724 
fun wf_constraint_for rel sides concl mains = 

725 
HOLogic.mk_mem (HOLogic.mk_prod (apply2 tuple_for_args (mains, concl)), Var rel) 

726 
> fold (curry HOLogic.mk_imp) sides 

727 
> close_form [rel]; 

728 

729 
fun wf_constraint_for_triple rel (sides, mains, concl) = 

730 
map (wf_constraint_for rel sides concl) mains 

731 
> foldr1 HOLogic.mk_conj; 

732 

733 
fun terminates_by ctxt timeout goal tac = 

734 
can (SINGLE (Classical.safe_tac ctxt) #> the 

735 
#> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt))) #> the 

736 
#> Goal.finish ctxt) goal; 

737 

738 
val max_cached_wfs = 50; 

739 
val cached_timeout = Synchronized.var "Nunchaku_Collect.cached_timeout" Time.zeroTime; 

740 
val cached_wf_props = Synchronized.var "Nunchaku_Collect.cached_wf_props" ([] : (term * bool) list); 

741 

742 
val termination_tacs = [Lexicographic_Order.lex_order_tac true, ScnpReconstruct.sizechange_tac]; 

743 

744 
fun is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout const intros = 

745 
let 

746 
val thy = Proof_Context.theory_of ctxt; 

747 

748 
val Const (x as (_, T)) = head_of (HOLogic.dest_Trueprop (Logic.strip_imp_concl (hd intros))); 

749 
in 

750 
(case triple_lookup (const_match thy o swap) wfs (dest_Const const) of 

751 
SOME (SOME wf) => wf 

752 
 _ => 

753 
(case map (triple_for_intro_rule ctxt x) intros > filter_out (null o #2) of 

754 
[] => true 

755 
 triples => 

756 
let 

757 
val binders_T = HOLogic.mk_tupleT (binder_types T); 

758 
val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T)); 

759 
val j = fold (Integer.max o maxidx_of_term) intros 0 + 1; 

760 
val rel = (("R", j), rel_T); 

761 
val prop = 

762 
Const (@{const_name wf}, rel_T > HOLogic.boolT) $ Var rel :: 

763 
map (wf_constraint_for_triple rel) triples 

764 
> foldr1 HOLogic.mk_conj 

765 
> HOLogic.mk_Trueprop; 

766 
in 

767 
if debug then writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop) 

768 
else (); 

769 
if wf_timeout = Synchronized.value cached_timeout andalso 

770 
length (Synchronized.value cached_wf_props) < max_cached_wfs then 

771 
() 

772 
else 

773 
(Synchronized.change cached_wf_props (K []); 

774 
Synchronized.change cached_timeout (K wf_timeout)); 

775 
(case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of 

776 
SOME wf => wf 

777 
 NONE => 

778 
let 

779 
val goal = Goal.init (Thm.cterm_of ctxt prop); 

780 
val wf = exists (terminates_by ctxt wf_timeout goal) termination_tacs; 

781 
in 

782 
Synchronized.change cached_wf_props (cons (prop, wf)); wf 

783 
end) 

784 
end) 

785 
handle 

786 
List.Empty => false 

787 
 NO_TRIPLE () => false) 

788 
end; 

789 

790 
datatype lhs_pat = 

791 
Only_Vars 

792 
 Prim_Pattern of string 

793 
 Any_Pattern; 

794 

66634
56456f388867
eliminate artifact of translation in printed Nunchaku model
blanchet
parents:
66624
diff
changeset

795 
fun is_apparently_pat_complete ctxt props = 
64389  796 
let 
797 
val is_Var_or_Bound = is_Var orf is_Bound; 

798 

799 
fun lhs_pat_of t = 

800 
(case t of 

801 
Const (@{const_name All}, _) $ Abs (_, _, t) => lhs_pat_of t 

802 
 Const (@{const_name HOL.eq}, _) $ u $ _ => 

803 
(case filter_out is_Var_or_Bound (snd (strip_comb u)) of 

804 
[] => Only_Vars 

805 
 [v] => 

806 
(case strip_comb v of 

807 
(cst as Const (_, T), args) => 

808 
(case body_type T of 

809 
Type (T_name, _) => 

810 
if can (Ctr_Sugar.dest_ctr ctxt T_name) cst andalso forall is_Var_or_Bound args then 

811 
Prim_Pattern T_name 

812 
else 

813 
Any_Pattern 

814 
 _ => Any_Pattern) 

815 
 _ => Any_Pattern) 

816 
 _ => Any_Pattern) 

817 
 _ => Any_Pattern); 

818 
in 

819 
(case map lhs_pat_of props of 

820 
[] => false 

821 
 pats as Prim_Pattern T_name :: _ => 

822 
forall (can (fn Prim_Pattern _ => ())) pats andalso 

823 
length pats = length (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt T_name))) 

824 
 pats => forall (curry (op =) Only_Vars) pats) 

825 
end; 

826 

827 
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *) 

828 
val axioms_max_depth = 255 

829 

830 
fun isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals0 some_assms0 

831 
subgoal0 = 

832 
let 

833 
val thy = Proof_Context.theory_of ctxt; 

834 

835 
fun card_of T = 

836 
(case triple_lookup (typ_match thy o swap) cards T of 

837 
NONE => (NONE, NONE) 

838 
 SOME (c1, c2) => (if c1 = SOME 1 then NONE else c1, c2)); 

839 

840 
fun axioms_of_class class = 

841 
#axioms (Axclass.get_info thy class) 

842 
handle ERROR _ => []; 

843 

844 
fun monomorphize_class_axiom T t = 

845 
(case Term.add_tvars t [] of 

846 
[] => t 

847 
 [(x, S)] => Envir.subst_term_types (Vartab.make [(x, (S, T))]) t); 

848 

849 
fun consider_sort depth T S (seens as (seenS, seenT, seen), problem) = 

850 
if member (op =) seenS S then 

851 
(seens, problem) 

852 
else if depth > axioms_max_depth then 

853 
raise TOO_DEEP_DEPS () 

854 
else 

855 
let 

856 
val seenS = S :: seenS; 

857 
val seens = (seenS, seenT, seen); 

858 

859 
val supers = Sign.complete_sort thy S; 

860 
val axioms0 = maps (map Thm.prop_of o axioms_of_class) supers; 

861 
val axioms = map (preprocess_prop false ctxt whacks o monomorphize_class_axiom T) axioms0; 

862 
in 

863 
(seens, map IAxiom axioms @ problem) 

864 
> fold (consider_term (depth + 1)) axioms 

865 
end 

866 
and consider_type depth T = 

867 
(case T of 

868 
Type (s, Ts) => 

869 
if is_type_builtin s then fold (consider_type depth) Ts 

870 
else consider_non_builtin_type depth T 

871 
 _ => consider_non_builtin_type depth T) 

872 
and consider_non_builtin_type depth T (seens as (seenS, seenT, seen), problem) = 

873 
if member (op =) seenT T then 

874 
(seens, problem) 

875 
else 

876 
let 

877 
val seenT = T :: seenT; 

878 
val seens = (seenS, seenT, seen); 

879 

64412  880 
fun consider_typedef_or_quotient itypedef_or_quotient tuple_of s = 
64389  881 
let 
66624  882 
val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt s; 
64389  883 
val tyenv = Sign.typ_match thy (T0, T) Vartab.empty; 
884 
val substT = Envir.subst_type tyenv; 

885 
val subst = Envir.subst_term_types tyenv; 

886 
val repT = substT repT0; 

66624  887 
val wrt = preprocess_prop false ctxt whacks (subst wrt0); 
64389  888 
val abs = subst abs0; 
889 
val rep = subst rep0; 

890 
in 

64412  891 
apsnd (cons (itypedef_or_quotient {abs_typ = T, rep_typ = repT, wrt = wrt, abs = abs, 
64389  892 
rep = rep})) 
893 
#> consider_term (depth + 1) wrt 

894 
end; 

895 
in 

896 
(seens, problem) 

897 
> (case T of 

898 
TFree (_, S) => 

899 
apsnd (cons (ITVal (T, card_of T))) 

900 
#> consider_sort depth T S 

901 
 TVar (_, S) => consider_sort depth T S 

902 
 Type (s, Ts) => 

903 
fold (consider_type depth) Ts 

904 
#> (case classify_type_name ctxt s of 

905 
Co_Datatype => 

906 
let 

907 
val (fp, fpTs, ctrss) = mutual_co_datatypes_of ctxt (s, Ts); 

908 
val specs = map2 (fn T => fn ctrs => {typ = T, ctrs = ctrs}) fpTs ctrss; 

909 
in 

910 
(fn ((seenS, seenT, seen), problem) => 

911 
((seenS, union (op =) fpTs seenT, seen), ICoData (fp, specs) :: problem)) 

912 
#> fold (fold (consider_type (depth + 1) o fastype_of)) ctrss 

913 
end 

64412  914 
 Typedef => consider_typedef_or_quotient ITypedef typedef_of s 
915 
 Quotient => consider_typedef_or_quotient IQuotient quotient_of s 

64389  916 
 TVal => apsnd (cons (ITVal (T, card_of T))))) 
917 
end 

918 
and consider_term depth t = 

919 
(case t of 

920 
t1 $ t2 => fold (consider_term depth) [t1, t2] 

921 
 Var (_, T) => consider_type depth T 

922 
 Bound _ => I 

923 
 Abs (_, T, t') => 

924 
consider_term depth t' 

925 
#> consider_type depth T 

926 
 _ => (fn (seens as (seenS, seenT, seen), problem) => 

927 
if member (op aconv) seen t then 

928 
(seens, problem) 

929 
else if depth > axioms_max_depth then 

930 
raise TOO_DEEP_DEPS () 

931 
else 

932 
let 

933 
val seen = t :: seen; 

934 
val seens = (seenS, seenT, seen); 

935 
in 

936 
(case t of 

937 
Const (x as (s, T)) => 

938 
(if is_const_builtin s orelse is_co_datatype_ctr ctxt x orelse 

66624  939 
is_co_datatype_case ctxt x orelse is_quotient_abs ctxt x orelse 
940 
is_quotient_rep ctxt x orelse is_typedef_abs ctxt x orelse 

941 
is_typedef_rep ctxt x then 

64389  942 
(seens, problem) 
66624  943 
else if is_stale_typedef_abs ctxt x orelse is_stale_typedef_rep ctxt x then 
64389  944 
raise UNSUPPORTED_FUNC t 
945 
else 

946 
(case spec_rules_of ctxt x of 

947 
SOME (classif, consts, props0, poly_props) => 

948 
let 

949 
val props = map (preprocess_prop false ctxt whacks) props0; 

950 

951 
fun def_or_spec () = 

952 
(case definition_of thy x of 

953 
SOME eq0 => 

954 
let val eq = preprocess_prop false ctxt whacks eq0 in 

955 
([eq], [IRec [{const = t, props = [eq], pat_complete = true}]]) 

956 
end 

957 
 NONE => (props, [ISpec {consts = consts, props = props}])); 

958 

959 
val (props', cmds) = 

960 
if null props then 

961 
([], map IVal consts) 

962 
else if classif = Spec_Rules.Equational then 

963 
(case partition_props consts props of 

964 
SOME propss => 

965 
(props, 

966 
[IRec (map2 (fn const => fn props => 

967 
{const = const, props = props, 

66634
56456f388867
eliminate artifact of translation in printed Nunchaku model
blanchet
parents:
66624
diff
changeset

968 
pat_complete = is_apparently_pat_complete ctxt props}) 
64389  969 
consts propss)]) 
970 
 NONE => def_or_spec ()) 

971 
else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] 

972 
classif then 

973 
if is_inductive_set_intro (hd props) then 

974 
def_or_spec () 

975 
else 

976 
(case partition_props consts props of 

977 
SOME propss => 

978 
(props, 

979 
[ICoPred (if classif = Spec_Rules.Inductive then BNF_Util.Least_FP 

980 
else BNF_Util.Greatest_FP, 

981 
length consts = 1 andalso 

982 
is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout 

983 
(the_single consts) poly_props, 

984 
map2 (fn const => fn props => {const = const, props = props}) 

985 
consts propss)]) 

986 
 NONE => def_or_spec ()) 

987 
else 

988 
def_or_spec (); 

989 
in 

990 
((seenS, seenT, union (op aconv) consts seen), cmds @ problem) 

991 
> fold (consider_term (depth + 1)) props' 

992 
end 

993 
 NONE => 

994 
(case definition_of thy x of 

995 
SOME eq0 => 

996 
let val eq = preprocess_prop false ctxt whacks eq0 in 

997 
(seens, IRec [{const = t, props = [eq], pat_complete = true}] :: problem) 

998 
> consider_term (depth + 1) eq 

999 
end 

1000 
 NONE => (seens, IVal t :: problem)))) 

1001 
> consider_type depth T 

1002 
 Free (_, T) => 

1003 
(seens, IVal t :: problem) 

1004 
> consider_type depth T) 

1005 
end)); 

1006 

1007 
val (poly_axioms, mono_axioms0) = orphan_axioms_of ctxt 

1008 
> List.partition has_polymorphism; 

1009 

1010 
fun implicit_evals_of pol (@{const Not} $ t) = implicit_evals_of (not pol) t 

1011 
 implicit_evals_of pol (@{const implies} $ t $ u) = 

1012 
(case implicit_evals_of pol u of 

1013 
[] => implicit_evals_of (not pol) t 

1014 
 ts => ts) 

1015 
 implicit_evals_of pol (@{const conj} $ t $ u) = 

1016 
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u) 

1017 
 implicit_evals_of pol (@{const disj} $ t $ u) = 

1018 
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u) 

1019 
 implicit_evals_of false (Const (@{const_name HOL.eq}, _) $ t $ u) = 

1020 
distinct (op aconv) [t, u] 

1021 
 implicit_evals_of true (Const (@{const_name HOL.eq}, _) $ t $ _) = [t] 

1022 
 implicit_evals_of _ _ = []; 

1023 

1024 
val mono_axioms_and_some_assms = 

1025 
map (preprocess_prop false ctxt whacks) (mono_axioms0 @ some_assms0); 

1026 
val subgoal = preprocess_prop falsify ctxt whacks subgoal0; 

1027 
val implicit_evals = implicit_evals_of true subgoal; 

1028 
val evals = map (preprocess_closed_term ctxt whacks) evals0; 

1029 
val seens = ([], [], []); 

1030 

1031 
val (commandss, complete) = 

1032 
(seens, 

1033 
map IAxiom mono_axioms_and_some_assms @ [IGoal subgoal] @ map IEval (implicit_evals @ evals)) 

1034 
> fold (consider_term 0) (subgoal :: evals @ mono_axioms_and_some_assms) 

1035 
> snd 

1036 
> rev (* prettier *) 

1037 
> sort_isa_commands_topologically ctxt 

1038 
>> group_isa_commands; 

1039 
in 

1040 
(poly_axioms, {commandss = commandss, sound = true, complete = complete}) 

1041 
end; 

1042 

1043 
fun add_pat_complete_of_command cmd = 

1044 
(case cmd of 

1045 
ICoPred (_, _, specs) => union (op =) (map #const specs) 

1046 
 IRec specs => 

1047 
union (op =) (map_filter (try (fn {const, pat_complete = true, ...} => const)) specs) 

1048 
 _ => I); 

1049 

1050 
fun pat_completes_of_isa_problem {commandss, ...} = 

1051 
fold (fold add_pat_complete_of_command) commandss []; 

1052 

1053 
fun str_of_isa_term_with_type ctxt t = 

1054 
Syntax.string_of_term ctxt t ^ " : " ^ Syntax.string_of_typ ctxt (fastype_of t); 

1055 

1056 
fun is_triv_wrt (Abs (_, _, body)) = is_triv_wrt body 

1057 
 is_triv_wrt @{const True} = true 

1058 
 is_triv_wrt _ = false; 

1059 

1060 
fun str_of_isa_type_spec ctxt {abs_typ, rep_typ, wrt, abs, rep} = 

1061 
Syntax.string_of_typ ctxt abs_typ ^ " := " ^ Syntax.string_of_typ ctxt rep_typ ^ 

1062 
(if is_triv_wrt wrt then "" else "\n wrt " ^ Syntax.string_of_term ctxt wrt) ^ 

1063 
"\n abstract " ^ Syntax.string_of_term ctxt abs ^ 

1064 
"\n concrete " ^ Syntax.string_of_term ctxt rep; 

1065 

1066 
fun str_of_isa_co_data_spec ctxt {typ, ctrs} = 

1067 
Syntax.string_of_typ ctxt typ ^ " :=\n " ^ 

1068 
space_implode "\n " (map (str_of_isa_term_with_type ctxt) ctrs); 

1069 

1070 
fun str_of_isa_const_spec ctxt {const, props} = 

1071 
str_of_isa_term_with_type ctxt const ^ " :=\n " ^ 

1072 
space_implode ";\n " (map (Syntax.string_of_term ctxt) props); 

1073 

1074 
fun str_of_isa_rec_spec ctxt {const, props, pat_complete} = 

1075 
str_of_isa_term_with_type ctxt const ^ (if pat_complete then " [pat_complete]" else "") ^ 

66635  1076 
" :=\n " ^ space_implode ";\n " (map (Syntax.string_of_term ctxt) props); 
64389  1077 

1078 
fun str_of_isa_consts_spec ctxt {consts, props} = 

1079 
space_implode " and\n " (map (str_of_isa_term_with_type ctxt) consts) ^ " :=\n " ^ 

1080 
space_implode ";\n " (map (Syntax.string_of_term ctxt) props); 

1081 

1082 
fun str_of_isa_card NONE = "" 

1083 
 str_of_isa_card (SOME k) = signed_string_of_int k; 

1084 

1085 
fun str_of_isa_cards_suffix (NONE, NONE) = "" 

1086 
 str_of_isa_cards_suffix (c1, c2) = " " ^ str_of_isa_card c1 ^ "" ^ str_of_isa_card c2; 

1087 

1088 
fun str_of_isa_command ctxt (ITVal (T, cards)) = 

1089 
"type " ^ Syntax.string_of_typ ctxt T ^ str_of_isa_cards_suffix cards 

64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset

1090 
 str_of_isa_command ctxt (ITypedef spec) = "typedef " ^ str_of_isa_type_spec ctxt spec 
64389  1091 
 str_of_isa_command ctxt (IQuotient spec) = "quotient " ^ str_of_isa_type_spec ctxt spec 
1092 
 str_of_isa_command ctxt (ICoData (fp, specs)) = 

1093 
BNF_Util.case_fp fp "data" "codata" ^ " " ^ str_of_and_list (str_of_isa_co_data_spec ctxt) specs 

1094 
 str_of_isa_command ctxt (IVal t) = "val " ^ str_of_isa_term_with_type ctxt t 

1095 
 str_of_isa_command ctxt (ICoPred (fp, wf, specs)) = 

1096 
BNF_Util.case_fp fp "pred" "copred" ^ " " ^ (if wf then "[wf] " else "") ^ 

1097 
str_of_and_list (str_of_isa_const_spec ctxt) specs 

1098 
 str_of_isa_command ctxt (IRec specs) = "rec " ^ str_of_and_list (str_of_isa_rec_spec ctxt) specs 

1099 
 str_of_isa_command ctxt (ISpec spec) = "spec " ^ str_of_isa_consts_spec ctxt spec 

1100 
 str_of_isa_command ctxt (IAxiom prop) = "axiom " ^ Syntax.string_of_term ctxt prop 

1101 
 str_of_isa_command ctxt (IGoal prop) = "goal " ^ Syntax.string_of_term ctxt prop 

1102 
 str_of_isa_command ctxt (IEval t) = "eval " ^ Syntax.string_of_term ctxt t; 

1103 

1104 
fun str_of_isa_problem ctxt {commandss, sound, complete} = 

1105 
map (cat_lines o map (suffix "." o str_of_isa_command ctxt)) commandss 

1106 
> space_implode "\n\n" > suffix "\n" 

1107 
> prefix ("# " ^ (if sound then "sound" else "unsound") ^ "\n") 

1108 
> prefix ("# " ^ (if complete then "complete" else "incomplete") ^ "\n"); 

1109 

1110 
end; 