7 |
7 |
8 signature NOMINAL_DT_ALPHA = |
8 signature NOMINAL_DT_ALPHA = |
9 sig |
9 sig |
10 val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term |
10 val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term |
11 |
11 |
12 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
12 val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list -> |
13 bclause list list list -> term list -> Proof.context -> alpha_result * local_theory |
13 Proof.context -> alpha_result * local_theory |
14 |
14 |
15 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
15 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
16 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
16 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
17 |
17 |
18 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
18 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
19 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
19 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
20 |
20 |
21 val raw_prove_alpha_distincts: Proof.context -> alpha_result -> thm list -> string list -> thm list |
21 val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list |
22 val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> thm list -> thm list -> thm list |
22 val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list |
23 val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list |
23 val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list |
24 val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list |
24 val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list |
25 val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list |
25 val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list |
26 val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> |
26 val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> |
27 thm list * thm list |
27 thm list * thm list |
222 val nth_bclausess = nth bclausesss bn_n |
222 val nth_bclausess = nth bclausesss bn_n |
223 in |
223 in |
224 map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
224 map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
225 end |
225 end |
226 |
226 |
227 fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy = |
227 fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy = |
228 let |
228 let |
229 val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names |
229 val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info |
|
230 |
|
231 val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_names |
230 val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys |
232 val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys |
231 val alpha_frees = map Free (alpha_names ~~ alpha_tys) |
233 val alpha_frees = map Free (alpha_names ~~ alpha_tys) |
232 val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs) |
234 val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs) |
233 |
235 |
234 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
236 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) |
237 val alpha_bn_arg_tys = map (nth raw_tys) bn_tys |
239 val alpha_bn_arg_tys = map (nth raw_tys) bn_tys |
238 val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys |
240 val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys |
239 val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) |
241 val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) |
240 val alpha_bn_map = bns ~~ alpha_bn_frees |
242 val alpha_bn_map = bns ~~ alpha_bn_frees |
241 |
243 |
242 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) cns_info bclausesss |
244 val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss |
243 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info |
245 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info |
244 |
246 |
245 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
247 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
246 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
248 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
247 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
249 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
248 |
250 |
391 |
393 |
392 fun distinct_tac cases_thms distinct_thms = |
394 fun distinct_tac cases_thms distinct_thms = |
393 rtac notI THEN' eresolve_tac cases_thms |
395 rtac notI THEN' eresolve_tac cases_thms |
394 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
396 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
395 |
397 |
396 fun raw_prove_alpha_distincts ctxt alpha_result raw_distinct_thms raw_dt_names = |
398 fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = |
397 let |
399 let |
398 val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result |
400 val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result |
|
401 val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info |
399 |
402 |
400 val ty_trm_assoc = raw_dt_names ~~ alpha_names |
403 val ty_trm_assoc = raw_dt_names ~~ alpha_names |
401 |
404 |
402 fun mk_alpha_distinct raw_distinct_trm = |
405 fun mk_alpha_distinct raw_distinct_trm = |
403 let |
406 let |
437 in |
440 in |
438 if hyps = [] then HOLogic.mk_Trueprop concl |
441 if hyps = [] then HOLogic.mk_Trueprop concl |
439 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
442 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
440 end; |
443 end; |
441 |
444 |
442 fun raw_prove_alpha_eq_iff ctxt alpha_result raw_distinct_thms raw_inject_thms = |
445 fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info = |
443 let |
446 let |
444 val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result |
447 val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result |
|
448 val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info |
445 |
449 |
446 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
450 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
447 val goals = map mk_alpha_eq_iff_goal thms_imp; |
451 val goals = map mk_alpha_eq_iff_goal thms_imp; |
448 val tac = alpha_eq_iff_tac (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; |
452 val tac = alpha_eq_iff_tac (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; |
449 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
453 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |