12 type bn_info = (term * int * (int * term option) list list) list |
12 type bn_info = (term * int * (int * term option) list list) list |
13 |
13 |
14 (* binding modes and binding clauses *) |
14 (* binding modes and binding clauses *) |
15 datatype bmode = Lst | Res | Set |
15 datatype bmode = Lst | Res | Set |
16 datatype bclause = BC of bmode * (term option * int) list * int list |
16 datatype bclause = BC of bmode * (term option * int) list * int list |
|
17 |
|
18 val is_atom: Proof.context -> typ -> bool |
|
19 val is_atom_set: Proof.context -> typ -> bool |
|
20 val is_atom_fset: Proof.context -> typ -> bool |
|
21 val is_atom_list: Proof.context -> typ -> bool |
|
22 val mk_atom_set: term -> term |
|
23 val mk_atom_fset: term -> term |
|
24 |
17 |
25 |
18 val setify: Proof.context -> term -> term |
26 val setify: Proof.context -> term -> term |
19 val listify: Proof.context -> term -> term |
27 val listify: Proof.context -> term -> term |
20 |
28 |
21 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
29 val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
149 val ty = fastype_of arg |
157 val ty = fastype_of arg |
150 in |
158 in |
151 case AList.lookup (op=) bn_args i of |
159 case AList.lookup (op=) bn_args i of |
152 NONE => (case (AList.lookup (op=) fv_map ty) of |
160 NONE => (case (AList.lookup (op=) fv_map ty) of |
153 NONE => mk_supp arg |
161 NONE => mk_supp arg |
154 | SOME fv => fv $ arg) |
162 | SOME fv => fv $ arg) |
155 | SOME (NONE) => @{term "{}::atom set"} |
163 | SOME (NONE) => @{term "{}::atom set"} |
156 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
164 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
157 end |
165 end |
158 in |
166 in |
159 case bclause of |
167 case bclause of |
160 BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
168 BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
161 | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause |
169 | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause |
162 end |
170 end |
163 |
171 |
164 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = |
172 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = |
165 let |
173 let |
166 val arg_names = Datatype_Prop.make_tnames arg_tys |
174 val arg_names = Datatype_Prop.make_tnames arg_tys |
167 val args = map Free (arg_names ~~ arg_tys) |
175 val args = map Free (arg_names ~~ arg_tys) |
168 val fv = the (AList.lookup (op=) fv_map ty) |
176 val fv = the (AList.lookup (op=) fv_map ty) |
169 val lhs = fv $ list_comb (constr, args) |
177 val lhs = fv $ list_comb (constr, args) |
171 val rhs = fold_union rhs_trms |
179 val rhs = fold_union rhs_trms |
172 in |
180 in |
173 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
181 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
174 end |
182 end |
175 |
183 |
176 fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses = |
184 fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = |
177 let |
185 let |
178 val arg_names = Datatype_Prop.make_tnames arg_tys |
186 val arg_names = Datatype_Prop.make_tnames arg_tys |
179 val args = map Free (arg_names ~~ arg_tys) |
187 val args = map Free (arg_names ~~ arg_tys) |
180 val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) |
188 val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) |
181 val lhs = fv_bn $ list_comb (constr, args) |
189 val lhs = fv_bn $ list_comb (constr, args) |
194 end |
202 end |
195 |
203 |
196 fun define_raw_fvs descr sorts bn_info bclausesss lthy = |
204 fun define_raw_fvs descr sorts bn_info bclausesss lthy = |
197 let |
205 let |
198 val fv_names = prefix_dt_names descr sorts "fv_" |
206 val fv_names = prefix_dt_names descr sorts "fv_" |
199 val fv_arg_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
207 val fv_arg_tys = all_dtyps descr sorts |
200 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
208 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
201 val fv_frees = map Free (fv_names ~~ fv_tys); |
209 val fv_frees = map Free (fv_names ~~ fv_tys); |
202 val fv_map = fv_arg_tys ~~ fv_frees |
210 val fv_map = fv_arg_tys ~~ fv_frees |
203 |
211 |
204 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
212 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |