author | wenzelm |
Sun, 13 Dec 2020 23:11:41 +0100 | |
changeset 72907 | 3883f536d84d |
parent 72450 | 24bd1316eaae |
child 74561 | 8e6c973003c8 |
permissions | -rw-r--r-- |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
1 |
signature DATATYPE_RECORDS = sig |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
2 |
type ctr_options = string -> bool |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
3 |
type ctr_options_cmd = Proof.context -> string -> bool |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
4 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
5 |
val default_ctr_options: ctr_options |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
6 |
val default_ctr_options_cmd: ctr_options_cmd |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
7 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
8 |
val mk_update_defs: string -> local_theory -> local_theory |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
9 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
10 |
val record: binding -> ctr_options -> (binding option * (typ * sort)) list -> |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
11 |
(binding * typ) list -> local_theory -> local_theory |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
12 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
13 |
val record_cmd: binding -> ctr_options_cmd -> |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
14 |
(binding option * (string * string option)) list -> (binding * string) list -> local_theory -> |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
15 |
local_theory |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
16 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
17 |
val setup: theory -> theory |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
18 |
end |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
19 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
20 |
structure Datatype_Records : DATATYPE_RECORDS = struct |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
21 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
22 |
type ctr_options = string -> bool |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
23 |
type ctr_options_cmd = Proof.context -> string -> bool |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
24 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
25 |
val default_ctr_options = Plugin_Name.default_filter |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
26 |
val default_ctr_options_cmd = K Plugin_Name.default_filter |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
27 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
28 |
type data = string Symtab.table |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
29 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
30 |
structure Data = Theory_Data |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
31 |
( |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
32 |
type T = data |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
33 |
val empty = Symtab.empty |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
34 |
val merge = Symtab.merge op = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
35 |
val extend = I |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
36 |
) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
37 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
38 |
fun mk_eq_dummy (lhs, rhs) = |
69593 | 39 |
Const (\<^const_name>\<open>HOL.eq\<close>, dummyT --> dummyT --> \<^typ>\<open>bool\<close>) $ lhs $ rhs |
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
40 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
41 |
val dummify = map_types (K dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
42 |
fun repeat_split_tac ctxt thm = REPEAT_ALL_NEW (CHANGED o Splitter.split_tac ctxt [thm]) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
43 |
|
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
44 |
fun mk_update_defs typ_name lthy = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
45 |
let |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
46 |
val short_name = Long_Name.base_name typ_name |
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
47 |
val {ctrs, casex, selss, split, sel_thmss, injects, ...} = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
48 |
the (Ctr_Sugar.ctr_sugar_of lthy typ_name) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
49 |
val ctr = case ctrs of [ctr] => ctr | _ => error "Datatype_Records.mk_update_defs: expected only single constructor" |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
50 |
val sels = case selss of [sels] => sels | _ => error "Datatype_Records.mk_update_defs: expected selectors" |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
51 |
val sels_dummy = map dummify sels |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
52 |
val ctr_dummy = dummify ctr |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
53 |
val casex_dummy = dummify casex |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
54 |
val len = length sels |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
55 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
56 |
val simp_thms = flat sel_thmss @ injects |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
57 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
58 |
fun mk_name sel = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
59 |
Binding.name ("update_" ^ Long_Name.base_name (fst (dest_Const sel))) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
60 |
|
68910
a21202dfe3eb
proper binding position for the resulting definition command, not this source file;
wenzelm
parents:
68686
diff
changeset
|
61 |
val thms_binding = (Binding.name "record_simps", @{attributes [simp]}) |
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
62 |
|
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
63 |
fun mk_t idx = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
64 |
let |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
65 |
val body = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
66 |
fold_rev (fn pos => fn t => t $ (if len - pos = idx + 1 then Bound len $ Bound pos else Bound pos)) (0 upto len - 1) ctr_dummy |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
67 |
|> fold_rev (fn idx => fn t => Abs ("x" ^ Value.print_int idx, dummyT, t)) (1 upto len) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
68 |
in |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
69 |
Abs ("f", dummyT, casex_dummy $ body) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
70 |
end |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
71 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
72 |
fun simp_only_tac ctxt = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
73 |
REPEAT_ALL_NEW (resolve_tac ctxt @{thms impI allI}) THEN' |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
74 |
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp_thms) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
75 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
76 |
fun prove ctxt defs ts n = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
77 |
let |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
78 |
val t = nth ts n |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
79 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
80 |
val sel_dummy = nth sels_dummy n |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
81 |
val t_dummy = dummify t |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
82 |
fun tac {context = ctxt, ...} = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
83 |
Goal.conjunction_tac 1 THEN |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
84 |
Local_Defs.unfold_tac ctxt defs THEN |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
85 |
PARALLEL_ALLGOALS (repeat_split_tac ctxt split THEN' simp_only_tac ctxt) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
86 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
87 |
val sel_upd_same_thm = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
88 |
let |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
89 |
val ([f, x], ctxt') = Variable.add_fixes ["f", "x"] ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
90 |
val f = Free (f, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
91 |
val x = Free (x, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
92 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
93 |
val lhs = sel_dummy $ (t_dummy $ f $ x) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
94 |
val rhs = f $ (sel_dummy $ x) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
95 |
val prop = Syntax.check_term ctxt' (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs))) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
96 |
in |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
97 |
[Goal.prove_future ctxt' [] [] prop tac] |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
98 |
|> Variable.export ctxt' ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
99 |
end |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
100 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
101 |
val sel_upd_diff_thms = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
102 |
let |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
103 |
val ([f, x], ctxt') = Variable.add_fixes ["f", "x"] ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
104 |
val f = Free (f, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
105 |
val x = Free (x, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
106 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
107 |
fun lhs sel = sel $ (t_dummy $ f $ x) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
108 |
fun rhs sel = sel $ x |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
109 |
fun eq sel = (lhs sel, rhs sel) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
110 |
fun is_n i = i = n |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
111 |
val props = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
112 |
sels_dummy ~~ (0 upto len - 1) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
113 |
|> filter_out (is_n o snd) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
114 |
|> map (HOLogic.mk_Trueprop o mk_eq_dummy o eq o fst) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
115 |
|> Syntax.check_terms ctxt' |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
116 |
in |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
117 |
if length props > 0 then |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
118 |
Goal.prove_common ctxt' (SOME ~1) [] [] props tac |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
119 |
|> Variable.export ctxt' ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
120 |
else |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
121 |
[] |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
122 |
end |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
123 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
124 |
val upd_comp_thm = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
125 |
let |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
126 |
val ([f, g, x], ctxt') = Variable.add_fixes ["f", "g", "x"] ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
127 |
val f = Free (f, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
128 |
val g = Free (g, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
129 |
val x = Free (x, dummyT) |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
130 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
131 |
val lhs = t_dummy $ f $ (t_dummy $ g $ x) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
132 |
val rhs = t_dummy $ Abs ("a", dummyT, f $ (g $ Bound 0)) $ x |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
133 |
val prop = Syntax.check_term ctxt' (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs))) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
134 |
in |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
135 |
[Goal.prove_future ctxt' [] [] prop tac] |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
136 |
|> Variable.export ctxt' ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
137 |
end |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
138 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
139 |
val upd_comm_thms = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
140 |
let |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
141 |
fun prop i ctxt = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
142 |
let |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
143 |
val ([f, g, x], ctxt') = Variable.variant_fixes ["f", "g", "x"] ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
144 |
val self = t_dummy $ Free (f, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
145 |
val other = dummify (nth ts i) $ Free (g, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
146 |
val lhs = other $ (self $ Free (x, dummyT)) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
147 |
val rhs = self $ (other $ Free (x, dummyT)) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
148 |
in |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
149 |
(HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs)), ctxt') |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
150 |
end |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
151 |
val (props, ctxt') = fold_map prop (0 upto n - 1) ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
152 |
val props = Syntax.check_terms ctxt' props |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
153 |
in |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
154 |
if length props > 0 then |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
155 |
Goal.prove_common ctxt' (SOME ~1) [] [] props tac |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
156 |
|> Variable.export ctxt' ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
157 |
else |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
158 |
[] |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
159 |
end |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
160 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
161 |
val upd_sel_thm = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
162 |
let |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
163 |
val ([x], ctxt') = Variable.add_fixes ["x"] ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
164 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
165 |
val lhs = t_dummy $ Abs("_", dummyT, (sel_dummy $ Free(x, dummyT))) $ Free (x, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
166 |
val rhs = Free (x, dummyT) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
167 |
val prop = Syntax.check_term ctxt (HOLogic.mk_Trueprop (mk_eq_dummy (lhs, rhs))) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
168 |
in |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
169 |
[Goal.prove_future ctxt [] [] prop tac] |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
170 |
|> Variable.export ctxt' ctxt |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
171 |
end |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
172 |
in |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
173 |
sel_upd_same_thm @ sel_upd_diff_thms @ upd_comp_thm @ upd_comm_thms @ upd_sel_thm |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
174 |
end |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
175 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
176 |
fun define name t = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
177 |
Local_Theory.define ((name, NoSyn), ((Binding.empty, @{attributes [datatype_record_update, code]}),t)) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
178 |
#> apfst (apsnd snd) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
179 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
180 |
val (updates, (lthy'', lthy')) = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
181 |
lthy |
72450 | 182 |
|> (snd o Local_Theory.begin_nested) |
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
183 |
|> Local_Theory.map_background_naming (Name_Space.qualified_path false (Binding.name short_name)) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
184 |
|> @{fold_map 2} define (map mk_name sels) (Syntax.check_terms lthy (map mk_t (0 upto len - 1))) |
72450 | 185 |
||> `Local_Theory.end_nested |
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
186 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
187 |
val phi = Proof_Context.export_morphism lthy' lthy'' |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
188 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
189 |
val (update_ts, update_defs) = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
190 |
split_list updates |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
191 |
|>> map (Morphism.term phi) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
192 |
||> map (Morphism.thm phi) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
193 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
194 |
val thms = flat (map (prove lthy'' update_defs update_ts) (0 upto len-1)) |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
195 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
196 |
fun insert sel = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
197 |
Symtab.insert op = (fst (dest_Const sel), Local_Theory.full_name lthy' (mk_name sel)) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
198 |
in |
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
199 |
lthy'' |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
200 |
|> Local_Theory.map_background_naming (Name_Space.mandatory_path short_name) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
201 |
|> Local_Theory.note (thms_binding, thms) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
202 |
|> snd |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
203 |
|> Local_Theory.restore_background_naming lthy |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
204 |
|> Local_Theory.background_theory (Data.map (fold insert sels)) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
205 |
end |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
206 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
207 |
fun record binding opts tyargs args lthy = |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
208 |
let |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
209 |
val constructor = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
210 |
(((Binding.empty, Binding.map_name (fn c => "make_" ^ c) binding), args), NoSyn) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
211 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
212 |
val datatyp = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
213 |
((tyargs, binding), NoSyn) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
214 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
215 |
val dtspec = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
216 |
((opts, false), |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
217 |
[(((datatyp, [constructor]), (Binding.empty, Binding.empty, Binding.empty)), [])]) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
218 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
219 |
val lthy' = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
220 |
BNF_FP_Def_Sugar.co_datatypes BNF_Util.Least_FP BNF_LFP.construct_lfp dtspec lthy |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
221 |
|> mk_update_defs (Local_Theory.full_name lthy binding) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
222 |
in |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
223 |
lthy' |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
224 |
end |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
225 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
226 |
fun record_cmd binding opts tyargs args lthy = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
227 |
record binding (opts lthy) |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
228 |
(map (apsnd (apfst (Syntax.parse_typ lthy) o apsnd (Typedecl.read_constraint lthy))) tyargs) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
229 |
(map (apsnd (Syntax.parse_typ lthy)) args) lthy |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
230 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
231 |
(* syntax *) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
232 |
(* copied and adapted from record.ML *) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
233 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
234 |
val read_const = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
235 |
dest_Const oo Proof_Context.read_const {proper = true, strict = true} |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
236 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
237 |
fun field_tr ((Const (\<^syntax_const>\<open>_datatype_field\<close>, _) $ Const (name, _) $ arg)) = (name, arg) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
238 |
| field_tr t = raise TERM ("field_tr", [t]); |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
239 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
240 |
fun fields_tr (Const (\<^syntax_const>\<open>_datatype_fields\<close>, _) $ t $ u) = field_tr t :: fields_tr u |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
241 |
| fields_tr t = [field_tr t]; |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
242 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
243 |
fun record_fields_tr ctxt t = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
244 |
let |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
245 |
val assns = map (apfst (read_const ctxt)) (fields_tr t) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
246 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
247 |
val typ_name = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
248 |
snd (fst (hd assns)) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
249 |
|> domain_type |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
250 |
|> dest_Type |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
251 |
|> fst |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
252 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
253 |
val assns' = map (apfst fst) assns |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
254 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
255 |
val {ctrs, selss, ...} = the (Ctr_Sugar.ctr_sugar_of ctxt typ_name) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
256 |
val ctr = case ctrs of [ctr] => ctr | _ => error "BNF_Record.record_fields_tr: expected only single constructor" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
257 |
val sels = case selss of [sels] => sels | _ => error "BNF_Record.record_fields_tr: expected selectors" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
258 |
val ctr_dummy = Const (fst (dest_Const ctr), dummyT) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
259 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
260 |
fun mk_arg name = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
261 |
case AList.lookup op = assns' name of |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
262 |
NONE => error ("BNF_Record.record_fields_tr: missing field " ^ name) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
263 |
| SOME t => t |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
264 |
in |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
265 |
if length assns = length sels then |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
266 |
list_comb (ctr_dummy, map (mk_arg o fst o dest_Const) sels) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
267 |
else |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
268 |
error ("BNF_Record.record_fields_tr: expected " ^ Value.print_int (length sels) ^ " field(s)") |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
269 |
end |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
270 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
271 |
fun field_update_tr ctxt (Const (\<^syntax_const>\<open>_datatype_field_update\<close>, _) $ Const (name, _) $ arg) = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
272 |
let |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
273 |
val thy = Proof_Context.theory_of ctxt |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
274 |
val (name, _) = read_const ctxt name |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
275 |
in |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
276 |
case Symtab.lookup (Data.get thy) name of |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
277 |
NONE => raise Fail ("not a valid record field: " ^ name) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
278 |
| SOME s => Const (s, dummyT) $ Abs (Name.uu_, dummyT, arg) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
279 |
end |
69598 | 280 |
| field_update_tr _ t = raise TERM ("field_update_tr", [t]); |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
281 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
282 |
fun field_updates_tr ctxt (Const (\<^syntax_const>\<open>_datatype_field_updates\<close>, _) $ t $ u) = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
283 |
field_update_tr ctxt t :: field_updates_tr ctxt u |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
284 |
| field_updates_tr ctxt t = [field_update_tr ctxt t]; |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
285 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
286 |
fun record_tr ctxt [t] = record_fields_tr ctxt t |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
287 |
| record_tr _ ts = raise TERM ("record_tr", ts); |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
288 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
289 |
fun record_update_tr ctxt [t, u] = fold (curry op $) (field_updates_tr ctxt u) t |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
290 |
| record_update_tr _ ts = raise TERM ("record_update_tr", ts); |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
291 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
292 |
val parse_ctr_options = |
69593 | 293 |
Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.list1 (Plugin_Name.parse_filter >> K) --| \<^keyword>\<open>)\<close> >> |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
294 |
(fn fs => fold I fs default_ctr_options_cmd)) default_ctr_options_cmd |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
295 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
296 |
val parser = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
297 |
(parse_ctr_options -- BNF_Util.parse_type_args_named_constrained -- Parse.binding) -- |
71376 | 298 |
(\<^keyword>\<open>=\<close> |-- Scan.repeat1 (Parse.binding -- (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.typ))) |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
299 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
300 |
val _ = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
301 |
Outer_Syntax.local_theory |
69593 | 302 |
\<^command_keyword>\<open>datatype_record\<close> |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
303 |
"Defines a record based on the BNF/datatype machinery" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
304 |
(parser >> (fn (((ctr_options, tyargs), binding), args) => |
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
305 |
record_cmd binding ctr_options tyargs args)) |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
306 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
307 |
val setup = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
308 |
(Sign.parse_translation |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
309 |
[(\<^syntax_const>\<open>_datatype_record_update\<close>, record_update_tr), |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
310 |
(\<^syntax_const>\<open>_datatype_record\<close>, record_tr)]); |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
311 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
312 |
end |