5 Definitions and proofs for the alpha-relations. |
5 Definitions and proofs for the alpha-relations. |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_DT_ALPHA = |
8 signature NOMINAL_DT_ALPHA = |
9 sig |
9 sig |
10 val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
10 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> |
11 bclause list list list -> term list -> Proof.context -> |
11 term list -> Proof.context -> term list * term list * thm list * thm list * thm * local_theory |
12 term list * term list * thm list * thm list * thm * local_theory |
|
13 |
12 |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
13 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
15 term list -> typ list -> thm list |
14 term list -> typ list -> thm list |
16 |
15 |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
16 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
218 val nth_bclausess = nth bclausesss bn_n |
217 val nth_bclausess = nth bclausesss bn_n |
219 in |
218 in |
220 map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
219 map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
221 end |
220 end |
222 |
221 |
223 fun define_raw_alpha descr sorts bn_info bclausesss fvs lthy = |
222 fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy = |
224 let |
223 let |
225 val alpha_names = prefix_dt_names descr sorts "alpha_" |
224 val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names |
226 val alpha_arg_tys = all_dtyps descr sorts |
225 val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys |
227 val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys |
|
228 val alpha_frees = map Free (alpha_names ~~ alpha_tys) |
226 val alpha_frees = map Free (alpha_names ~~ alpha_tys) |
229 val alpha_map = alpha_arg_tys ~~ (alpha_frees ~~ fvs) |
227 val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs) |
230 |
228 |
231 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
229 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
232 val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns |
230 val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns |
233 val alpha_bn_names = map (prefix "alpha_") bn_names |
231 val alpha_bn_names = map (prefix "alpha_") bn_names |
234 val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys |
232 val alpha_bn_arg_tys = map (nth raw_tys) bn_tys |
235 val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys |
233 val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys |
236 val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) |
234 val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) |
237 val alpha_bn_map = bns ~~ alpha_bn_frees |
235 val alpha_bn_map = bns ~~ alpha_bn_frees |
238 |
236 |
239 val constrs_info = all_dtyp_constrs_types descr sorts |
237 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) cns_info bclausesss |
240 |
238 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info |
241 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss |
|
242 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info |
|
243 |
239 |
244 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
240 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
245 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
241 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
246 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
242 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
247 |
243 |