equal
deleted
inserted
replaced
59 type bn_info = (term * int * (int * term option) list list) list |
59 type bn_info = (term * int * (int * term option) list list) list |
60 |
60 |
61 |
61 |
62 datatype bmode = Lst | Res | Set |
62 datatype bmode = Lst | Res | Set |
63 datatype bclause = BC of bmode * (term option * int) list * int list |
63 datatype bclause = BC of bmode * (term option * int) list * int list |
|
64 |
|
65 fun lookup xs x = the (AList.lookup (op=) xs x) |
|
66 |
64 |
67 |
65 (* testing for concrete atom types *) |
68 (* testing for concrete atom types *) |
66 fun is_atom ctxt ty = |
69 fun is_atom ctxt ty = |
67 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
70 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
68 |
71 |
164 let |
167 let |
165 val arg = nth args i |
168 val arg = nth args i |
166 in |
169 in |
167 case bn_option of |
170 case bn_option of |
168 NONE => (setify lthy arg, @{term "{}::atom set"}) |
171 NONE => (setify lthy arg, @{term "{}::atom set"}) |
169 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
172 | SOME bn => (to_set (bn $ arg), |
|
173 if member (op=) bodies i then @{term "{}::atom set"} |
|
174 else lookup fv_bn_map bn $ arg) |
170 end |
175 end |
171 |
176 |
172 val t1 = map (mk_fv_body fv_map args) bodies |
177 val t1 = map (mk_fv_body fv_map args) bodies |
173 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
178 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
174 in |
179 in |
187 case AList.lookup (op=) bn_args i of |
192 case AList.lookup (op=) bn_args i of |
188 NONE => (case (AList.lookup (op=) fv_map ty) of |
193 NONE => (case (AList.lookup (op=) fv_map ty) of |
189 NONE => mk_supp arg |
194 NONE => mk_supp arg |
190 | SOME fv => fv $ arg) |
195 | SOME fv => fv $ arg) |
191 | SOME (NONE) => @{term "{}::atom set"} |
196 | SOME (NONE) => @{term "{}::atom set"} |
192 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
197 | SOME (SOME bn) => lookup fv_bn_map bn $ arg |
193 end |
198 end |
194 in |
199 in |
195 case bclause of |
200 case bclause of |
196 BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
201 BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
197 | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause |
202 | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause |
199 |
204 |
200 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = |
205 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = |
201 let |
206 let |
202 val arg_names = Datatype_Prop.make_tnames arg_tys |
207 val arg_names = Datatype_Prop.make_tnames arg_tys |
203 val args = map Free (arg_names ~~ arg_tys) |
208 val args = map Free (arg_names ~~ arg_tys) |
204 val fv = the (AList.lookup (op=) fv_map ty) |
209 val fv = lookup fv_map ty |
205 val lhs = fv $ list_comb (constr, args) |
210 val lhs = fv $ list_comb (constr, args) |
206 val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses |
211 val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses |
207 val rhs = fold_union rhs_trms |
212 val rhs = fold_union rhs_trms |
208 in |
213 in |
209 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
214 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
211 |
216 |
212 fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = |
217 fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = |
213 let |
218 let |
214 val arg_names = Datatype_Prop.make_tnames arg_tys |
219 val arg_names = Datatype_Prop.make_tnames arg_tys |
215 val args = map Free (arg_names ~~ arg_tys) |
220 val args = map Free (arg_names ~~ arg_tys) |
216 val fv_bn = the (AList.lookup (op=) fv_bn_map bn_trm) |
221 val fv_bn = lookup fv_bn_map bn_trm |
217 val lhs = fv_bn $ list_comb (constr, args) |
222 val lhs = fv_bn $ list_comb (constr, args) |
218 val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses |
223 val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses |
219 val rhs = fold_union rhs_trms |
224 val rhs = fold_union rhs_trms |
220 in |
225 in |
221 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
226 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |