6 |
6 |
7 TODO: |
7 TODO: |
8 - field types: typedef; |
8 - field types: typedef; |
9 - trfuns for record types; |
9 - trfuns for record types; |
10 - operations and theorems: split, split_all/ex, ...; |
10 - operations and theorems: split, split_all/ex, ...; |
11 - field constructor: specific type for snd component (?); |
11 - field constructor: more specific type for snd component; |
12 - update_more operation; |
12 - update_more operation; |
13 - "..." for "... = more", "?..." for "?... = ?more"; |
13 - field syntax: "..." for "... = more", "?..." for "?... = ?more"; |
14 *) |
14 *) |
15 |
15 |
16 signature RECORD_PACKAGE = |
16 signature RECORD_PACKAGE = |
17 sig |
17 sig |
18 val moreS: sort |
18 val moreS: sort |
61 |
61 |
62 val (op :==) = Logic.mk_defpair; |
62 val (op :==) = Logic.mk_defpair; |
63 val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
63 val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
64 |
64 |
65 fun get_defs thy specs = map (PureThy.get_tthm thy o fst) specs; |
65 fun get_defs thy specs = map (PureThy.get_tthm thy o fst) specs; |
66 fun add_simps ss simps = Simplifier.addsimps (ss, map Attribute.thm_of simps); |
|
67 |
66 |
68 |
67 |
69 (* proof by simplification *) |
68 (* proof by simplification *) |
70 |
69 |
71 fun prove_simp opt_ss simps = |
70 fun prove_simp thy simps = |
72 let |
71 let |
73 val ss = add_simps (if_none opt_ss HOL_basic_ss) simps; |
72 val sign = Theory.sign_of thy; |
74 fun prove thy goal = |
73 val ss = Simplifier.addsimps (HOL_basic_ss, map Attribute.thm_of simps); |
|
74 |
|
75 fun prove goal = |
75 Attribute.tthm_of |
76 Attribute.tthm_of |
76 (Goals.prove_goalw_cterm [] (Thm.cterm_of (Theory.sign_of thy) goal) |
77 (Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal) |
77 (K [ALLGOALS (Simplifier.simp_tac ss)]) |
78 (K [ALLGOALS (Simplifier.simp_tac ss)]) |
78 handle ERROR => error ("The error(s) above occurred while trying to prove " |
79 handle ERROR => error ("The error(s) above occurred while trying to prove " |
79 ^ quote (Sign.string_of_term (Theory.sign_of thy) goal))); |
80 ^ quote (Sign.string_of_term sign goal))); |
80 in prove end; |
81 in prove end; |
81 |
82 |
82 |
83 |
83 |
84 |
84 (*** syntax operations ***) |
85 (*** syntax operations ***) |
245 |
246 |
246 type record_info = |
247 type record_info = |
247 {args: (string * sort) list, |
248 {args: (string * sort) list, |
248 parent: (typ list * string) option, |
249 parent: (typ list * string) option, |
249 fields: (string * typ) list, |
250 fields: (string * typ) list, |
250 simpset: Simplifier.simpset}; |
251 simps: tthm list}; |
251 |
252 |
252 type parent_info = |
253 type parent_info = |
253 {name: string, |
254 {name: string, |
254 fields: (string * typ) list, |
255 fields: (string * typ) list, |
255 simpset: Simplifier.simpset}; |
256 simps: tthm list}; |
256 |
257 |
257 |
258 |
258 (* theory data *) |
259 (* theory data *) |
259 |
260 |
260 val recordsK = "HOL/records"; |
261 val recordsK = "HOL/records"; |
280 [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]]; |
281 [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]]; |
281 |
282 |
282 fun pretty_field (c, T) = Pretty.block |
283 fun pretty_field (c, T) = Pretty.block |
283 [Pretty.str (ext_const c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)]; |
284 [Pretty.str (ext_const c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)]; |
284 |
285 |
285 fun pretty_record (name, {args, parent, fields, simpset = _}) = Pretty.block (Pretty.fbreaks |
286 fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks |
286 (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] :: |
287 (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] :: |
287 pretty_parent parent @ map pretty_field fields)); |
288 pretty_parent parent @ map pretty_field fields)); |
288 in |
289 in |
289 seq (Pretty.writeln o pretty_record) (Symtab.dest tab) |
290 seq (Pretty.writeln o pretty_record) (Symtab.dest tab) |
290 end; |
291 end; |
304 |
305 |
305 fun put_records tab thy = |
306 fun put_records tab thy = |
306 Theory.put_data (recordsK, Records tab) thy; |
307 Theory.put_data (recordsK, Records tab) thy; |
307 |
308 |
308 fun put_record name info thy = |
309 fun put_record name info thy = |
309 thy |> put_records (Symtab.update ((name, info), get_records thy)); |
310 put_records (Symtab.update ((name, info), get_records thy)) thy; |
310 |
311 |
311 |
312 |
312 (* parent records *) |
313 (* parent records *) |
313 |
314 |
314 fun inst_record thy (types, name) = |
315 fun inst_record thy (types, name) = |
315 let |
316 let |
316 val sign = Theory.sign_of thy; |
317 val sign = Theory.sign_of thy; |
317 fun err msg = error (msg ^ " parent record " ^ quote name); |
318 fun err msg = error (msg ^ " parent record " ^ quote name); |
318 |
319 |
319 val {args, parent, fields, simpset} = |
320 val {args, parent, fields, simps} = |
320 (case get_record thy name of Some info => info | None => err "Unknown"); |
321 (case get_record thy name of Some info => info | None => err "Unknown"); |
|
322 val _ = if length types <> length args then err "Bad number of arguments for" else (); |
321 |
323 |
322 fun bad_inst ((x, S), T) = |
324 fun bad_inst ((x, S), T) = |
323 if Sign.of_sort sign (T, S) then None else Some x |
325 if Sign.of_sort sign (T, S) then None else Some x |
324 val bads = mapfilter bad_inst (args ~~ types); |
326 val bads = mapfilter bad_inst (args ~~ types); |
325 |
327 |
326 val inst = map fst args ~~ types; |
328 val inst = map fst args ~~ types; |
327 val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x))); |
329 val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x))); |
328 in |
330 in |
329 if length types <> length args then |
331 if not (null bads) then |
330 err "Bad number of arguments for" |
|
331 else if not (null bads) then |
|
332 err ("Ill-sorted instantiation of " ^ commas bads ^ " in") |
332 err ("Ill-sorted instantiation of " ^ commas bads ^ " in") |
333 else (apsome (apfst (map subst)) parent, map (apsnd subst) fields, simpset) |
333 else (apsome (apfst (map subst)) parent, map (apsnd subst) fields, simps) |
334 end; |
334 end; |
335 |
335 |
336 fun add_parents thy (None, parents) = parents |
336 fun add_parents thy (None, parents) = parents |
337 | add_parents thy (Some (types, name), parents) = |
337 | add_parents thy (Some (types, name), parents) = |
338 let val (pparent, pfields, psimpset) = inst_record thy (types, name) |
338 let val (pparent, pfields, psimps) = inst_record thy (types, name) |
339 in add_parents thy (pparent, {name = name, fields = pfields, simpset = psimpset} :: parents) end; |
339 in add_parents thy (pparent, {name = name, fields = pfields, simps = psimps} :: parents) end; |
340 |
340 |
341 |
341 |
342 |
342 |
343 (** internal theory extenders **) |
343 (** internal theory extenders **) |
344 |
344 |
371 val field_specs = map mk_field_spec named_vars; |
371 val field_specs = map mk_field_spec named_vars; |
372 |
372 |
373 (*field destructors*) |
373 (*field destructors*) |
374 fun mk_dest_spec dest dest' (c, T) = |
374 fun mk_dest_spec dest dest' (c, T) = |
375 let |
375 let |
376 val p = Free ("p", mk_fieldT ((c, T), moreT)); |
376 val p = Free ("p", mk_fieldT ((c, T), moreT)); |
377 val p' = Free ("p", HOLogic.mk_prodT (T, moreT)); |
377 val p' = Free ("p", HOLogic.mk_prodT (T, moreT)); |
378 (*note: field types are just abbreviations*) |
378 (*note: field types are just abbreviations*) |
379 in dest p :== dest' p' end; |
379 in dest p :== dest' p' end; |
380 val dest_specs = |
380 val dest_specs = |
381 map (mk_dest_spec mk_fst HOLogic.mk_fst) fields @ |
381 map (mk_dest_spec mk_fst HOLogic.mk_fst) fields @ |
382 map (mk_dest_spec mk_snd HOLogic.mk_snd) fields; |
382 map (mk_dest_spec mk_snd HOLogic.mk_snd) fields; |
385 (* prepare theorems *) |
385 (* prepare theorems *) |
386 |
386 |
387 fun mk_dest_prop dest dest' (c, v) = |
387 fun mk_dest_prop dest dest' (c, v) = |
388 dest (mk_field ((c, v), more)) === dest' (v, more); |
388 dest (mk_field ((c, v), more)) === dest' (v, more); |
389 val dest_props = |
389 val dest_props = |
390 map (mk_dest_prop mk_fst fst) named_vars @ map (mk_dest_prop mk_snd snd) named_vars; |
390 map (mk_dest_prop mk_fst fst) named_vars @ |
|
391 map (mk_dest_prop mk_snd snd) named_vars; |
391 |
392 |
392 |
393 |
393 (* 1st stage: defs_thy *) |
394 (* 1st stage: defs_thy *) |
394 |
395 |
395 val defs_thy = |
396 val defs_thy = |
460 val all_vars = parent_vars @ vars; |
458 val all_vars = parent_vars @ vars; |
461 val all_named_vars = parent_named_vars @ named_vars; |
459 val all_named_vars = parent_named_vars @ named_vars; |
462 |
460 |
463 val zeta = variant alphas "'z"; |
461 val zeta = variant alphas "'z"; |
464 val moreT = TFree (zeta, moreS); |
462 val moreT = TFree (zeta, moreS); |
465 val more = Free (variant xs moreN, moreT); |
463 val more = Free (moreN, moreT); |
466 fun more_part t = mk_more t (full moreN); |
464 fun more_part t = mk_more t (full moreN); |
467 |
465 |
468 val parent_more = funpow parent_len mk_snd; |
466 val parent_more = funpow parent_len mk_snd; |
469 val idxs = 0 upto (len - 1); |
467 val idxs = 0 upto (len - 1); |
470 |
468 |
491 (mk_makeC recT (makeN, all_types))]; |
489 (mk_makeC recT (makeN, all_types))]; |
492 |
490 |
493 |
491 |
494 (* prepare definitions *) |
492 (* prepare definitions *) |
495 |
493 |
496 (* record (scheme) type abbreviation *) |
494 (*record (scheme) type abbreviation*) |
497 val recordT_specs = |
495 val recordT_specs = |
498 [(suffix schemeN bname, alphas @ [zeta], rec_schemeT, Syntax.NoSyn), |
496 [(suffix schemeN bname, alphas @ [zeta], rec_schemeT, Syntax.NoSyn), |
499 (bname, alphas, recT, Syntax.NoSyn)]; |
497 (bname, alphas, recT, Syntax.NoSyn)]; |
500 |
498 |
501 (*selectors*) |
499 (*selectors*) |
562 val make_defs = get_defs defs_thy make_specs; |
560 val make_defs = get_defs defs_thy make_specs; |
563 |
561 |
564 |
562 |
565 (* 3rd stage: thms_thy *) |
563 (* 3rd stage: thms_thy *) |
566 |
564 |
567 val parent_simpset = |
565 val parent_simps = flat (map #simps parents); |
568 (case parent of |
566 val prove = prove_simp defs_thy; |
569 None => HOL_basic_ss |
567 |
570 | Some (_, pname) => #simpset (the (get_record thy pname))); |
568 val sel_convs = map (prove (parent_simps @ sel_defs @ field_simps)) sel_props; |
571 |
569 val update_convs = map (prove (parent_simps @ update_defs @ sel_convs)) update_props; |
572 val pss = Some parent_simpset; |
570 |
573 |
|
574 val sel_convs = map (prove_simp pss (sel_defs @ field_simps) defs_thy) sel_props; |
|
575 val update_convs = map (prove_simp pss (update_defs @ sel_convs) defs_thy) update_props; |
|
576 val simps = field_simps @ sel_convs @ update_convs @ make_defs; |
571 val simps = field_simps @ sel_convs @ update_convs @ make_defs; |
577 |
572 |
578 val thms_thy = |
573 val thms_thy = |
579 defs_thy |
574 defs_thy |
580 |> (PureThy.add_tthmss o map Attribute.none) |
575 |> (PureThy.add_tthmss o map Attribute.none) |
581 [("selector_defs", sel_defs), |
576 [("select_defs", sel_defs), |
582 ("update_defs", update_defs), |
577 ("update_defs", update_defs), |
583 ("make_defs", make_defs), |
578 ("make_defs", make_defs), |
584 ("selector_convs", sel_convs), |
579 ("select_convs", sel_convs), |
585 ("update_convs", update_convs)] |
580 ("update_convs", update_convs)] |
586 |> PureThy.add_tthmss [(("simps", simps), [Simplifier.simp_add_global])]; |
581 |> PureThy.add_tthmss [(("simps", simps), [Simplifier.simp_add_global])]; |
587 |
582 |
588 |
583 |
589 (* 4th stage: final_thy *) |
584 (* 4th stage: final_thy *) |
590 |
585 |
591 val simpset = add_simps parent_simpset simps; |
|
592 |
|
593 val final_thy = |
586 val final_thy = |
594 thms_thy |
587 thms_thy |
595 |> put_record name {args = args, parent = parent, fields = fields, simpset = simpset} |
588 |> put_record name {args = args, parent = parent, fields = fields, simps = simps} |
596 |> Theory.parent_path; |
589 |> Theory.parent_path; |
597 |
590 |
598 in final_thy end; |
591 in final_thy end; |
599 |
592 |
600 |
593 |
621 in (Term.add_typ_tfrees (T, env), T) end; |
614 in (Term.add_typ_tfrees (T, env), T) end; |
622 |
615 |
623 |
616 |
624 (* add_record *) |
617 (* add_record *) |
625 |
618 |
626 (*do all preparations and error checks here, deferring the real work |
619 (*we do all preparations and error checks here, deferring the real |
627 to record_definition above*) |
620 work to record_definition*) |
628 |
621 |
629 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy = |
622 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy = |
630 let |
623 let |
631 val _ = Theory.require thy "Record" "record definitions"; |
624 val _ = Theory.require thy "Record" "record definitions"; |
632 val sign = Theory.sign_of thy; |
625 val sign = Theory.sign_of thy; |
|
626 val _ = writeln ("Defining record " ^ quote bname ^ " ..."); |
633 |
627 |
634 |
628 |
635 (* parents *) |
629 (* parents *) |
636 |
630 |
637 fun prep_inst T = snd (cert_typ sign ([], T)); |
631 fun prep_inst T = snd (cert_typ sign ([], T)); |