15 datatype bclause = BC of bmode * (term option * int) list * int list |
15 datatype bclause = BC of bmode * (term option * int) list * int list |
16 |
16 |
17 val setify: Proof.context -> term -> term |
17 val setify: Proof.context -> term -> term |
18 val listify: Proof.context -> term -> term |
18 val listify: Proof.context -> term -> term |
19 |
19 |
20 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> |
20 val define_raw_fvs: |
21 (term * 'a * 'b) list -> (term * int * (int * term option) list list) list -> |
21 string list -> term list -> |
22 bclause list list list -> Proof.context -> term list * term list * thm list * local_theory |
22 Datatype_Aux.descr -> |
|
23 (string * sort) list -> |
|
24 (term * int * (int * term option) list list) list -> |
|
25 (term * int * (int * term option) list list) list -> |
|
26 bclause list list list -> Proof.context -> term list * term list * thm list * local_theory |
23 end |
27 end |
24 |
28 |
25 |
29 |
26 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
30 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = |
27 struct |
31 struct |
28 |
32 |
29 datatype bmode = Lst | Res | Set |
33 datatype bmode = Lst | Res | Set |
30 datatype bclause = BC of bmode * (term option * int) list * int list |
34 datatype bclause = BC of bmode * (term option * int) list * int list |
31 |
35 |
32 (* atom types *) |
36 (* testing for concrete atom types *) |
33 fun is_atom ctxt ty = |
37 fun is_atom ctxt ty = |
34 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
38 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
35 |
39 |
36 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t |
40 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t |
37 | is_atom_set _ _ = false; |
41 | is_atom_set _ _ = false; |
41 |
45 |
42 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t |
46 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t |
43 | is_atom_list _ _ = false |
47 | is_atom_list _ _ = false |
44 |
48 |
45 |
49 |
46 (* functions for producing sets, fsets and lists *) |
50 (* functions for producing sets, fsets and lists of general atom type |
|
51 out from concrete atom types *) |
47 fun mk_atom_set t = |
52 fun mk_atom_set t = |
48 let |
53 let |
49 val ty = fastype_of t; |
54 val ty = fastype_of t; |
50 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
55 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
51 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
56 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
52 in |
57 in |
53 (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t) |
58 Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t |
54 end; |
59 end |
55 |
60 |
56 fun mk_atom_fset t = |
61 fun mk_atom_fset t = |
57 let |
62 let |
58 val ty = fastype_of t; |
63 val ty = fastype_of t; |
59 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |
64 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |
60 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
65 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
61 val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} |
66 val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} |
62 in |
67 in |
63 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
68 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
64 end; |
69 end |
65 |
70 |
66 (* |
|
67 fun mk_atom_list t = |
71 fun mk_atom_list t = |
68 let |
72 let |
69 val ty = fastype_of t; |
73 val ty = fastype_of t; |
70 val atom_ty = dest_listT ty --> @{typ atom}; |
74 val atom_ty = dest_listT ty --> @{typ atom}; |
71 val map_ty = atom_ty --> ty --> @{typ "atom list"}; |
75 val map_ty = atom_ty --> ty --> @{typ "atom list"}; |
72 in |
76 in |
73 (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t) |
77 Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t |
74 end; |
78 end |
75 *) |
79 |
76 |
80 (* functions that coerces concrete atoms, sets and fsets into sets |
77 (* functions that coerces atoms, sets and fsets into atom sets ? *) |
81 of general atoms *) |
78 fun setify ctxt t = |
82 fun setify ctxt t = |
79 let |
83 let |
80 val ty = fastype_of t; |
84 val ty = fastype_of t; |
81 in |
85 in |
82 if is_atom ctxt ty |
86 if is_atom ctxt ty |
107 else t |
112 else t |
108 |
113 |
109 |
114 |
110 (* functions that construct the equations for fv and fv_bn *) |
115 (* functions that construct the equations for fv and fv_bn *) |
111 |
116 |
112 fun make_fv_body fv_map args i = |
117 fun mk_fv_body fv_map args i = |
113 let |
118 let |
114 val arg = nth args i |
119 val arg = nth args i |
115 val ty = fastype_of arg |
120 val ty = fastype_of arg |
116 in |
121 in |
117 case (AList.lookup (op=) fv_map ty) of |
122 case (AList.lookup (op=) fv_map ty) of |
118 NONE => mk_supp arg |
123 NONE => mk_supp arg |
119 | SOME fv => fv $ arg |
124 | SOME fv => fv $ arg |
120 end |
125 end |
121 |
126 |
122 fun make_fv_binder lthy fv_bn_map args (bn_option, i) = |
127 fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = |
123 let |
|
124 val arg = nth args i |
|
125 in |
|
126 case bn_option of |
|
127 NONE => (setify lthy arg, @{term "{}::atom set"}) |
|
128 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
|
129 end |
|
130 |
|
131 fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
|
132 let |
|
133 val t1 = map (make_fv_body fv_map args) bodies |
|
134 val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders) |
|
135 in |
|
136 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
|
137 end |
|
138 |
|
139 fun make_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = |
|
140 let |
|
141 val arg_names = Datatype_Prop.make_tnames arg_tys |
|
142 val args = map Free (arg_names ~~ arg_tys) |
|
143 val fv = the (AList.lookup (op=) fv_map ty) |
|
144 val lhs = fv $ list_comb (constr, args) |
|
145 val rhs_trms = map (make_fv_rhs lthy fv_map fv_bn_map args) bclauses |
|
146 val rhs = fold_union rhs_trms |
|
147 in |
|
148 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
149 end |
|
150 |
|
151 |
|
152 fun make_fv_bn_body fv_map fv_bn_map bn_args args i = |
|
153 let |
128 let |
154 val arg = nth args i |
129 val arg = nth args i |
155 val ty = fastype_of arg |
130 val ty = fastype_of arg |
156 in |
131 in |
157 case AList.lookup (op=) bn_args i of |
132 case AList.lookup (op=) bn_args i of |
160 | SOME fv => fv $ arg) |
135 | SOME fv => fv $ arg) |
161 | SOME (NONE) => @{term "{}::atom set"} |
136 | SOME (NONE) => @{term "{}::atom set"} |
162 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
137 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
163 end |
138 end |
164 |
139 |
165 fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = |
140 fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = |
|
141 let |
|
142 val arg = nth args i |
|
143 in |
|
144 case bn_option of |
|
145 NONE => (setify lthy arg, @{term "{}::atom set"}) |
|
146 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
|
147 end |
|
148 |
|
149 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
|
150 let |
|
151 val t1 = map (mk_fv_body fv_map args) bodies |
|
152 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
|
153 in |
|
154 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
|
155 end |
|
156 |
|
157 fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = |
166 case bclause of |
158 case bclause of |
167 BC (_, [], bodies) => fold_union (map (make_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
159 BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
168 | BC (_, binders, bodies) => |
160 | BC (_, binders, bodies) => |
169 let |
161 let |
170 val t1 = map (make_fv_body fv_map args) bodies |
162 val t1 = map (mk_fv_body fv_map args) bodies |
171 val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders) |
163 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
172 in |
164 in |
173 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
165 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
174 end |
166 end |
175 |
167 |
176 fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses = |
168 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = |
|
169 let |
|
170 val arg_names = Datatype_Prop.make_tnames arg_tys |
|
171 val args = map Free (arg_names ~~ arg_tys) |
|
172 val fv = the (AList.lookup (op=) fv_map ty) |
|
173 val lhs = fv $ list_comb (constr, args) |
|
174 val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses |
|
175 val rhs = fold_union rhs_trms |
|
176 in |
|
177 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
178 end |
|
179 |
|
180 fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses = |
177 let |
181 let |
178 val arg_names = Datatype_Prop.make_tnames arg_tys |
182 val arg_names = Datatype_Prop.make_tnames arg_tys |
179 val args = map Free (arg_names ~~ arg_tys) |
183 val args = map Free (arg_names ~~ arg_tys) |
180 val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) |
184 val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) |
181 val lhs = fv_bn $ list_comb (constr, args) |
185 val lhs = fv_bn $ list_comb (constr, args) |
182 val rhs_trms = map (make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses |
186 val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses |
183 val rhs = fold_union rhs_trms |
187 val rhs = fold_union rhs_trms |
184 in |
188 in |
185 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
189 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
186 end |
190 end |
187 |
191 |
188 fun make_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = |
192 fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = |
189 let |
193 let |
190 val nth_constrs_info = nth constrs_info bn_n |
194 val nth_constrs_info = nth constrs_info bn_n |
191 val nth_bclausess = nth bclausesss bn_n |
195 val nth_bclausess = nth bclausesss bn_n |
192 in |
196 in |
193 map2 (make_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
197 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
194 end |
198 end |
195 |
199 |
196 fun define_raw_fvs dt_descr sorts bn_funs bn_funs2 bclausesss lthy = |
200 fun define_raw_fvs t1 t2 dt_descr sorts bn_funs bn_funs2 bclausesss lthy = |
197 let |
201 let |
|
202 val _ = tracing ("bn-functions to be defined\n " ^ commas t1) |
|
203 val _ = tracing ("bn-equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) t2)) |
198 |
204 |
199 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
205 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
200 val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr; |
206 val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr; |
201 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
207 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
202 val fv_frees = map Free (fv_names ~~ fv_tys); |
208 val fv_frees = map Free (fv_names ~~ fv_tys); |
210 val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2 |
216 val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2 |
211 val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2) |
217 val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2) |
212 val fv_bn_map2 = bns ~~ fv_bn_frees2 |
218 val fv_bn_map2 = bns ~~ fv_bn_frees2 |
213 val fv_bn_map3 = bns2 ~~ fv_bn_frees2 |
219 val fv_bn_map3 = bns2 ~~ fv_bn_frees2 |
214 |
220 |
|
221 val _ = tracing ("fn_bn_map2 " ^ @{make_string} fv_bn_map2) |
|
222 val _ = tracing ("fn_bn_map3 " ^ @{make_string} fv_bn_map3) |
|
223 |
215 val constrs_info = all_dtyp_constrs_types dt_descr sorts |
224 val constrs_info = all_dtyp_constrs_types dt_descr sorts |
216 |
225 |
217 val fv_eqs2 = map2 (map2 (make_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss |
226 val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss |
218 val fv_bn_eqs2 = map (make_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 |
227 val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 |
219 |
228 |
|
229 val _ = tracing ("functions to be defined\n " ^ @{make_string} (fv_names @ fv_bn_names2)) |
|
230 val _ = tracing ("equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_eqs2 @ flat fv_bn_eqs2))) |
|
231 |
220 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2) |
232 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2) |
221 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2) |
233 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2) |
222 |
234 |
223 fun pat_completeness_auto lthy = |
235 fun pat_completeness_auto lthy = |
224 Pat_Completeness.pat_completeness_tac lthy 1 |
236 Pat_Completeness.pat_completeness_tac lthy 1 |