(* Title: nominal_dt_alpha.ML+ −
Author: Cezary Kaliszyk+ −
Author: Christian Urban+ −
+ −
Definitions and proofs for the alpha-relations.+ −
*)+ −
+ −
signature NOMINAL_DT_ALPHA =+ −
sig+ −
val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term+ −
+ −
val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> + −
bclause list list list -> term list -> Proof.context -> + −
term list * term list * thm list * thm list * thm * local_theory+ −
+ −
val mk_alpha_distincts: Proof.context -> thm list -> thm list -> + −
term list -> typ list -> thm list+ −
+ −
val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> + −
thm list -> thm list+ −
+ −
val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> + −
(Proof.context -> int -> tactic) -> Proof.context -> thm list+ −
+ −
val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> + −
(Proof.context -> int -> tactic) -> Proof.context -> thm list+ −
+ −
val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list+ −
val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list+ −
val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list+ −
val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> + −
Proof.context -> thm list * thm list+ −
+ −
val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list+ −
val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> + −
term list -> thm -> thm list -> Proof.context -> thm list+ −
val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list+ −
val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list+ −
val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list+ −
val raw_perm_bn_rsp: term list -> term list -> thm -> thm list -> thm list -> + −
Proof.context -> thm list+ −
+ −
val mk_funs_rsp: thm -> thm+ −
val mk_alpha_permute_rsp: thm -> thm + −
end+ −
+ −
structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =+ −
struct+ −
+ −
open Nominal_Permeq+ −
+ −
fun lookup xs x = the (AList.lookup (op=) xs x)+ −
fun group xs = AList.group (op=) xs+ −
+ −
(** definition of the inductive rules for alpha and alpha_bn **)+ −
+ −
(* construct the compound terms for prod_fv and prod_alpha *)+ −
fun mk_prod_fv (t1, t2) =+ −
let+ −
val ty1 = fastype_of t1+ −
val ty2 = fastype_of t2 + −
val resT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2) --> @{typ "atom set"}+ −
in+ −
Const (@{const_name "prod_fv"}, [ty1, ty2] ---> resT) $ t1 $ t2+ −
end+ −
+ −
fun mk_prod_alpha (t1, t2) =+ −
let+ −
val ty1 = fastype_of t1+ −
val ty2 = fastype_of t2 + −
val prodT = HOLogic.mk_prodT (domain_type ty1, domain_type ty2)+ −
val resT = [prodT, prodT] ---> @{typ "bool"}+ −
in+ −
Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2+ −
end+ −
+ −
(* generates the compound binder terms *)+ −
fun comb_binders lthy bmode args binders = + −
let + −
fun bind_set lthy args (NONE, i) = setify lthy (nth args i)+ −
| bind_set _ args (SOME bn, i) = bn $ (nth args i)+ −
fun bind_lst lthy args (NONE, i) = listify lthy (nth args i)+ −
| bind_lst _ args (SOME bn, i) = bn $ (nth args i)+ −
+ −
val (combine_fn, bind_fn) =+ −
case bmode of+ −
Lst => (mk_append, bind_lst) + −
| Set => (mk_union, bind_set)+ −
| Res => (mk_union, bind_set)+ −
in+ −
binders+ −
|> map (bind_fn lthy args)+ −
|> foldl1 combine_fn + −
end+ −
+ −
(* produces the term for an alpha with abstraction *)+ −
fun mk_alpha_term bmode fv alpha args args' binders binders' =+ −
let+ −
val (alpha_name, binder_ty) = + −
case bmode of+ −
Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})+ −
| Set => (@{const_name "alpha_set"}, @{typ "atom set"})+ −
| Res => (@{const_name "alpha_res"}, @{typ "atom set"})+ −
val ty = fastype_of args+ −
val pair_ty = HOLogic.mk_prodT (binder_ty, ty)+ −
val alpha_ty = [ty, ty] ---> @{typ "bool"}+ −
val fv_ty = ty --> @{typ "atom set"}+ −
val pair_lhs = HOLogic.mk_prod (binders, args)+ −
val pair_rhs = HOLogic.mk_prod (binders', args')+ −
in+ −
HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm},+ −
Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) + −
$ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs)+ −
end+ −
+ −
(* for non-recursive binders we have to produce alpha_bn premises *)+ −
fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = + −
case binder of+ −
(NONE, _) => []+ −
| (SOME bn, i) =>+ −
if member (op=) bodies i then [] + −
else [lookup alpha_bn_map bn $ nth args i $ nth args' i]+ −
+ −
(* generate the premises for an alpha rule; mk_frees is used+ −
if no binders are present *)+ −
fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause =+ −
let+ −
fun mk_frees i =+ −
let+ −
val arg = nth args i+ −
val arg' = nth args' i+ −
val ty = fastype_of arg+ −
in+ −
if nth is_rec i+ −
then fst (lookup alpha_map ty) $ arg $ arg'+ −
else HOLogic.mk_eq (arg, arg')+ −
end+ −
+ −
fun mk_alpha_fv i = + −
let+ −
val ty = fastype_of (nth args i)+ −
in+ −
case AList.lookup (op=) alpha_map ty of+ −
NONE => (HOLogic.eq_const ty, supp_const ty) + −
| SOME (alpha, fv) => (alpha, fv) + −
end + −
in+ −
case bclause of+ −
BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies + −
| BC (bmode, binders, bodies) => + −
let+ −
val (alphas, fvs) = split_list (map mk_alpha_fv bodies)+ −
val comp_fv = foldl1 mk_prod_fv fvs+ −
val comp_alpha = foldl1 mk_prod_alpha alphas+ −
val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies)+ −
val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies)+ −
val comp_binders = comb_binders lthy bmode args binders+ −
val comp_binders' = comb_binders lthy bmode args' binders+ −
val alpha_prem = + −
mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders'+ −
val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders)+ −
in+ −
map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems)+ −
end+ −
end+ −
+ −
(* produces the introduction rule for an alpha rule *)+ −
fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = + −
let+ −
val arg_names = Datatype_Prop.make_tnames arg_tys+ −
val arg_names' = Name.variant_list arg_names arg_names+ −
val args = map Free (arg_names ~~ arg_tys)+ −
val args' = map Free (arg_names' ~~ arg_tys)+ −
val alpha = fst (lookup alpha_map ty)+ −
val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args'))+ −
val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses+ −
in+ −
Library.foldr Logic.mk_implies (flat prems, concl)+ −
end+ −
+ −
(* produces the premise of an alpha-bn rule; we only need to+ −
treat the case special where the binding clause is empty;+ −
+ −
- if the body is not included in the bn_info, then we either+ −
produce an equation or an alpha-premise+ −
+ −
- if the body is included in the bn_info, then we create+ −
either a recursive call to alpha-bn, or no premise *)+ −
fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause =+ −
let+ −
fun mk_alpha_bn_prem i = + −
let+ −
val arg = nth args i+ −
val arg' = nth args' i+ −
val ty = fastype_of arg+ −
in+ −
case AList.lookup (op=) bn_args i of+ −
NONE => (case (AList.lookup (op=) alpha_map ty) of+ −
NONE => [HOLogic.mk_eq (arg, arg')]+ −
| SOME (alpha, _) => [alpha $ arg $ arg'])+ −
| SOME (NONE) => []+ −
| SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg']+ −
end + −
in+ −
case bclause of+ −
BC (_, [], bodies) => + −
map HOLogic.mk_Trueprop (flat (map mk_alpha_bn_prem bodies))+ −
| _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause+ −
end+ −
+ −
fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =+ −
let+ −
val arg_names = Datatype_Prop.make_tnames arg_tys+ −
val arg_names' = Name.variant_list arg_names arg_names+ −
val args = map Free (arg_names ~~ arg_tys)+ −
val args' = map Free (arg_names' ~~ arg_tys)+ −
val alpha_bn = lookup alpha_bn_map bn_trm+ −
val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args'))+ −
val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses+ −
in+ −
Library.foldr Logic.mk_implies (flat prems, concl)+ −
end+ −
+ −
fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = + −
let+ −
val nth_constrs_info = nth constrs_info bn_n+ −
val nth_bclausess = nth bclausesss bn_n+ −
in+ −
map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess+ −
end+ −
+ −
fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy =+ −
let+ −
val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names+ −
val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys+ −
val alpha_frees = map Free (alpha_names ~~ alpha_tys)+ −
val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs)+ −
+ −
val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)+ −
val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns+ −
val alpha_bn_names = map (prefix "alpha_") bn_names+ −
val alpha_bn_arg_tys = map (nth raw_tys) bn_tys+ −
val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys+ −
val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)+ −
val alpha_bn_map = bns ~~ alpha_bn_frees+ −
+ −
val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) cns_info bclausesss + −
val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info+ −
+ −
val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))+ −
(alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)+ −
val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)+ −
+ −
val (alphas, lthy') = Inductive.add_inductive_i+ −
{quiet_mode = true, verbose = false, alt_name = Binding.empty,+ −
coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}+ −
all_alpha_names [] all_alpha_intros [] lthy+ −
+ −
val all_alpha_trms_loc = #preds alphas;+ −
val alpha_induct_loc = #raw_induct alphas;+ −
val alpha_intros_loc = #intrs alphas;+ −
val alpha_cases_loc = #elims alphas;+ −
val phi = ProofContext.export_morphism lthy' lthy;+ −
+ −
val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc+ −
val (all_alpha_trms', _) = Variable.importT_terms all_alpha_trms lthy + −
val alpha_induct = Morphism.thm phi alpha_induct_loc;+ −
val alpha_intros = map (Morphism.thm phi) alpha_intros_loc+ −
val alpha_cases = map (Morphism.thm phi) alpha_cases_loc+ −
+ −
val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms'+ −
in+ −
(alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')+ −
end+ −
+ −
+ −
+ −
(** produces the distinctness theorems **)+ −
+ −
(* transforms the distinctness theorems of the constructors + −
to "not-alphas" of the constructors *)+ −
fun mk_distinct_goal ty_trm_assoc neq =+ −
let+ −
val (lhs, rhs) = + −
neq+ −
|> HOLogic.dest_Trueprop+ −
|> HOLogic.dest_not+ −
|> HOLogic.dest_eq+ −
val ty = fastype_of lhs+ −
in+ −
(lookup ty_trm_assoc ty) $ lhs $ rhs+ −
|> HOLogic.mk_not+ −
|> HOLogic.mk_Trueprop+ −
end+ −
+ −
fun distinct_tac cases_thms distinct_thms =+ −
rtac notI THEN' eresolve_tac cases_thms + −
THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)+ −
+ −
+ −
fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =+ −
let+ −
(* proper import of type-variables does not work,+ −
since then they are replaced by new variables, messing+ −
up the ty_trm assoc list *)+ −
val distinct_thms' = map Thm.legacy_freezeT distinct_thms+ −
val ty_trm_assoc = alpha_tys ~~ alpha_trms+ −
+ −
fun mk_alpha_distinct distinct_trm =+ −
let+ −
val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt+ −
val goal = mk_distinct_goal ty_trm_assoc distinct_trm+ −
in+ −
Goal.prove ctxt' [] [] goal + −
(K (distinct_tac cases_thms distinct_thms 1))+ −
|> singleton (Variable.export ctxt' ctxt)+ −
end+ −
+ −
in+ −
map (mk_alpha_distinct o prop_of) distinct_thms'+ −
|> map Thm.varifyT_global+ −
end+ −
+ −
+ −
+ −
(** produces the alpha_eq_iff simplification rules **)+ −
+ −
(* in case a theorem is of the form (Rel Const Const), it will be+ −
rewritten to ((Rel Const = Const) = True) + −
*)+ −
fun mk_simp_rule thm =+ −
case (prop_of thm) of+ −
@{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI}+ −
| _ => thm+ −
+ −
fun alpha_eq_iff_tac dist_inj intros elims =+ −
SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE'+ −
(rtac @{thm iffI} THEN' + −
RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj),+ −
asm_full_simp_tac (HOL_ss addsimps intros)])+ −
+ −
fun mk_alpha_eq_iff_goal thm =+ −
let+ −
val prop = prop_of thm;+ −
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);+ −
val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);+ −
fun list_conj l = foldr1 HOLogic.mk_conj l;+ −
in+ −
if hyps = [] then HOLogic.mk_Trueprop concl+ −
else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))+ −
end;+ −
+ −
fun mk_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims =+ −
let+ −
val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;+ −
val goals = map mk_alpha_eq_iff_goal thms_imp;+ −
val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1;+ −
val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals;+ −
in+ −
Variable.export ctxt' ctxt thms+ −
|> map mk_simp_rule+ −
end+ −
+ −
+ −
(** proof by induction over types **)+ −
+ −
fun induct_prove tys props induct_thm cases_tac ctxt =+ −
let+ −
val (arg_names, ctxt') =+ −
Variable.variant_fixes (replicate (length tys) "x") ctxt+ −
+ −
val args = map2 (curry Free) arg_names tys+ −
+ −
val true_trms = replicate (length tys) (K @{term True})+ −
+ −
fun apply_all x fs = map (fn f => f x) fs+ −
+ −
val goals = + −
group (props @ (tys ~~ true_trms))+ −
|> map snd + −
|> map2 apply_all args+ −
|> map fold_conj+ −
|> foldr1 HOLogic.mk_conj+ −
|> HOLogic.mk_Trueprop+ −
+ −
fun tac ctxt =+ −
HEADGOAL + −
(DETERM o (rtac induct_thm) + −
THEN_ALL_NEW + −
(REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))+ −
in+ −
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)+ −
|> singleton (ProofContext.export ctxt' ctxt)+ −
|> Datatype_Aux.split_conj_thm+ −
|> map Datatype_Aux.split_conj_thm+ −
|> flat+ −
|> filter_out (is_true o concl_of)+ −
|> map zero_var_indexes+ −
end+ −
+ −
+ −
(** proof by induction over the alpha-definitions **)+ −
+ −
fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =+ −
let+ −
val arg_tys = map (domain_type o fastype_of) alphas+ −
+ −
val ((arg_names1, arg_names2), ctxt') =+ −
ctxt+ −
|> Variable.variant_fixes (replicate (length alphas) "x") + −
||>> Variable.variant_fixes (replicate (length alphas) "y")+ −
+ −
val args1 = map2 (curry Free) arg_names1 arg_tys+ −
val args2 = map2 (curry Free) arg_names2 arg_tys+ −
+ −
val true_trms = replicate (length alphas) (K @{term True})+ −
+ −
fun apply_all x fs = map (fn f => f x) fs+ −
+ −
val goals_rhs = + −
group (props @ (alphas ~~ true_trms))+ −
|> map snd + −
|> map2 apply_all (args1 ~~ args2)+ −
|> map fold_conj+ −
+ −
fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2+ −
val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)+ −
+ −
val goals =+ −
(map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)+ −
|> foldr1 HOLogic.mk_conj+ −
|> HOLogic.mk_Trueprop+ −
+ −
fun tac ctxt =+ −
HEADGOAL + −
(DETERM o (rtac alpha_induct_thm) + −
THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])+ −
in+ −
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)+ −
|> singleton (ProofContext.export ctxt' ctxt)+ −
|> Datatype_Aux.split_conj_thm+ −
|> map (fn th => th RS mp) + −
|> map Datatype_Aux.split_conj_thm+ −
|> flat+ −
|> filter_out (is_true o concl_of)+ −
|> map zero_var_indexes+ −
end+ −
+ −
+ −
(** reflexivity proof for the alphas **)+ −
+ −
val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}+ −
+ −
fun cases_tac intros ctxt =+ −
let+ −
val prod_simps = @{thms split_conv prod_alpha_def prod_rel_def}+ −
+ −
val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac + −
+ −
val bound_tac = + −
EVERY' [ rtac exi_zero, + −
resolve_tac @{thms alpha_refl}, + −
asm_full_simp_tac (HOL_ss addsimps prod_simps) ]+ −
in+ −
resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]+ −
end+ −
+ −
fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt =+ −
let+ −
val arg_tys = + −
alpha_trms+ −
|> map fastype_of+ −
|> map domain_type+ −
+ −
val arg_bn_tys = + −
alpha_bns+ −
|> map fastype_of+ −
|> map domain_type+ −
+ −
val props = + −
map (fn (ty, c) => (ty, fn x => c $ x $ x)) + −
((arg_tys ~~ alpha_trms) @ (arg_bn_tys ~~ alpha_bns))+ −
in+ −
induct_prove arg_tys props raw_dt_induct (cases_tac alpha_intros) ctxt + −
end+ −
+ −
+ −
+ −
(** symmetry proof for the alphas **)+ −
+ −
val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"+ −
by (erule exE, rule_tac x="-p" in exI, auto)}+ −
+ −
(* for premises that contain binders *)+ −
fun prem_bound_tac pred_names ctxt = + −
let+ −
fun trans_prem_tac pred_names ctxt = + −
SUBPROOF (fn {prems, context, ...} => + −
let+ −
val prems' = map (transform_prem1 context pred_names) prems+ −
in+ −
resolve_tac prems' 1+ −
end) ctxt+ −
val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas}+ −
in+ −
EVERY' + −
[ etac exi_neg,+ −
resolve_tac @{thms alpha_sym_eqvt},+ −
asm_full_simp_tac (HOL_ss addsimps prod_simps),+ −
eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},+ −
trans_prem_tac pred_names ctxt ] + −
end+ −
+ −
fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =+ −
let+ −
val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms+ −
+ −
fun tac ctxt = + −
let+ −
val alpha_names = map (fst o dest_Const) alpha_trms + −
in+ −
resolve_tac alpha_intros THEN_ALL_NEW + −
FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt]+ −
end+ −
in+ −
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt + −
end+ −
+ −
+ −
(** transitivity proof for alphas **)+ −
+ −
(* applies cases rules and resolves them with the last premise *)+ −
fun ecases_tac cases = + −
Subgoal.FOCUS (fn {prems, ...} =>+ −
HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))+ −
+ −
fun aatac pred_names = + −
SUBPROOF (fn {prems, context, ...} =>+ −
HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))+ −
+ −
(* instantiates exI with the permutation p + q *)+ −
val perm_inst_tac =+ −
Subgoal.FOCUS (fn {params, ...} => + −
let+ −
val (p, q) = pairself snd (last2 params)+ −
val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q]+ −
val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}+ −
in+ −
HEADGOAL (rtac exi_inst)+ −
end)+ −
+ −
fun non_trivial_cases_tac pred_names intros ctxt = + −
let+ −
val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def}+ −
in+ −
resolve_tac intros+ −
THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' + −
TRY o EVERY' (* if binders are present *)+ −
[ etac @{thm exE},+ −
etac @{thm exE},+ −
perm_inst_tac ctxt, + −
resolve_tac @{thms alpha_trans_eqvt}, + −
atac,+ −
aatac pred_names ctxt, + −
eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},+ −
asm_full_simp_tac (HOL_ss addsimps prod_simps) ])+ −
end+ −
+ −
fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt =+ −
let+ −
fun all_cases ctxt = + −
asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) + −
THEN' TRY o non_trivial_cases_tac pred_names intros ctxt+ −
in+ −
EVERY' [ rtac @{thm allI}, rtac @{thm impI}, + −
ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]+ −
end+ −
+ −
fun prep_trans_goal alpha_trm (arg1, arg2) =+ −
let+ −
val arg_ty = fastype_of arg1+ −
val mid = alpha_trm $ arg2 $ (Bound 0)+ −
val rhs = alpha_trm $ arg1 $ (Bound 0) + −
in+ −
HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))+ −
end+ −
+ −
fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =+ −
let+ −
val alpha_names = map (fst o dest_Const) alpha_trms + −
val props = map prep_trans_goal alpha_trms+ −
in+ −
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct+ −
(prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt+ −
end+ −
+ −
+ −
(** proves the equivp predicate for all alphas **)+ −
+ −
val reflp_def' = + −
@{lemma "reflp R == !x. R x x" by (simp add: reflp_def refl_on_def)}+ −
+ −
val symp_def' =+ −
@{lemma "symp R == !x y . R x y --> R y x" by (simp add: symp_def sym_def)}+ −
+ −
val transp_def' =+ −
@{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" + −
by (rule eq_reflection, auto simp add: trans_def transp_def)}+ −
+ −
fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = + −
let+ −
val refl' = map (fold_rule [reflp_def'] o atomize) refl+ −
val symm' = map (fold_rule [symp_def'] o atomize) symm+ −
val trans' = map (fold_rule [transp_def'] o atomize) trans+ −
+ −
fun prep_goal t = + −
HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) + −
in + −
Goal.prove_multi ctxt [] [] (map prep_goal (alphas @ alpha_bns))+ −
(K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' + −
RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))+ −
|> chop (length alphas)+ −
end+ −
+ −
+ −
(* proves that alpha_raw implies alpha_bn *)+ −
+ −
fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = + −
SUBPROOF (fn {prems, context, ...} => + −
let+ −
val prems' = flat (map Datatype_Aux.split_conj_thm prems)+ −
val prems'' = map (transform_prem1 context pred_names) prems'+ −
in+ −
HEADGOAL + −
(REPEAT_ALL_NEW + −
(FIRST' [ rtac @{thm TrueI}, + −
rtac @{thm conjI}, + −
resolve_tac prems', + −
resolve_tac prems'',+ −
resolve_tac alpha_intros ]))+ −
end) ctxt+ −
+ −
fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt =+ −
let+ −
val arg_ty = domain_type o fastype_of + −
val alpha_names = map (fst o dest_Const) alpha_trms+ −
val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms+ −
val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms+ −
in+ −
alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct + −
(raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt+ −
end+ −
+ −
+ −
(* respectfulness for fv_raw / bn_raw *)+ −
+ −
fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =+ −
let+ −
val arg_ty = domain_type o fastype_of + −
val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms+ −
fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)+ −
+ −
val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs+ −
val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)+ −
val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns+ −
+ −
val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} + −
@ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) + −
+ −
in+ −
alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct + −
(K (asm_full_simp_tac ss)) ctxt+ −
end+ −
+ −
+ −
(* respectfulness for size *)+ −
+ −
fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =+ −
let+ −
val arg_tys = map (domain_type o fastype_of) all_alpha_trms+ −
+ −
fun mk_prop ty (x, y) = HOLogic.mk_eq + −
(HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)+ −
+ −
val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys + −
+ −
val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def + −
permute_prod_def prod.cases prod.recs})+ −
+ −
val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss+ −
in+ −
alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt+ −
end+ −
+ −
+ −
(* respectfulness for constructors *)+ −
+ −
fun raw_constr_rsp_tac alpha_intros simps = + −
let+ −
val pre_ss = HOL_ss addsimps @{thms fun_rel_def}+ −
val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel_def + −
prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps+ −
in+ −
asm_full_simp_tac pre_ss+ −
THEN' REPEAT o (resolve_tac @{thms allI impI})+ −
THEN' resolve_tac alpha_intros+ −
THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)+ −
end+ −
+ −
+ −
fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =+ −
let+ −
val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms+ −
+ −
fun lookup ty = + −
case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of+ −
NONE => HOLogic.eq_const ty+ −
| SOME alpha => alpha + −
+ −
fun fun_rel_app t1 t2 = + −
Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2+ −
+ −
fun prep_goal trm =+ −
trm+ −
|> strip_type o fastype_of+ −
|>> map lookup+ −
||> lookup+ −
|> uncurry (fold_rev fun_rel_app)+ −
|> (fn t => t $ trm $ trm)+ −
|> Syntax.check_term ctxt+ −
|> HOLogic.mk_Trueprop+ −
in+ −
Goal.prove_multi ctxt [] [] (map prep_goal constrs)+ −
(K (HEADGOAL + −
(Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))+ −
end+ −
+ −
+ −
(* rsp lemmas for alpha_bn relations *)+ −
+ −
val rsp_equivp =+ −
@{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q"+ −
by (simp only: fun_rel_def equivp_def, metis)}+ −
+ −
+ −
(* we have to reorder the alpha_bn_imps theorems in order+ −
to be in order with alpha_bn_trms *)+ −
fun raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp alpha_bn_imps =+ −
let+ −
fun mk_map thm =+ −
thm |> `prop_of+ −
|>> List.last o snd o strip_comb+ −
|>> HOLogic.dest_Trueprop+ −
|>> head_of+ −
|>> fst o dest_Const+ −
+ −
val alpha_bn_imps' = + −
map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms+ −
+ −
fun mk_thm thm1 thm2 = + −
(forall_intr_vars thm2) COMP (thm1 RS rsp_equivp)+ −
in+ −
map2 mk_thm alpha_bn_equivp alpha_bn_imps'+ −
end+ −
+ −
+ −
(* rsp for permute_bn functions *)+ −
+ −
val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f"+ −
by (simp add: fun_rel_def)}+ −
+ −
fun raw_prove_perm_bn_tac pred_names alpha_intros simps ctxt = + −
SUBPROOF (fn {prems, context, ...} => + −
let+ −
val prems' = flat (map Datatype_Aux.split_conj_thm prems)+ −
val prems'' = map (transform_prem1 context pred_names) prems'+ −
in+ −
HEADGOAL + −
(simp_tac (HOL_basic_ss addsimps (simps @ prems'))+ −
THEN' TRY o REPEAT_ALL_NEW + −
(FIRST' [ rtac @{thm TrueI}, + −
rtac @{thm conjI}, + −
rtac @{thm refl},+ −
resolve_tac prems', + −
resolve_tac prems'',+ −
resolve_tac alpha_intros ]))+ −
end) ctxt+ −
+ −
fun raw_perm_bn_rsp alpha_trms perm_bns alpha_induct alpha_intros simps ctxt =+ −
let+ −
val arg_ty = domain_type o fastype_of+ −
val perm_bn_ty = range_type o range_type o fastype_of+ −
val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms+ −
+ −
val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt + −
val p = Free (p, @{typ perm})+ −
+ −
fun mk_prop t =+ −
let+ −
val alpha_trm = lookup ty_assoc (perm_bn_ty t)+ −
in+ −
(alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y))+ −
end+ −
+ −
val goals = map mk_prop perm_bns+ −
val alpha_names = map (fst o dest_Const) alpha_trms + −
+ −
in+ −
alpha_prove alpha_trms goals alpha_induct + −
(raw_prove_perm_bn_tac alpha_names alpha_intros simps) ctxt+ −
|> ProofContext.export ctxt' ctxt+ −
|> map atomize+ −
|> map single+ −
|> map (curry (op OF) perm_bn_rsp)+ −
end+ −
+ −
+ −
+ −
(* transformation of the natural rsp-lemmas into standard form *)+ −
+ −
val fun_rsp = @{lemma+ −
"(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)}+ −
+ −
fun mk_funs_rsp thm = + −
thm+ −
|> atomize+ −
|> single+ −
|> curry (op OF) fun_rsp+ −
+ −
+ −
val permute_rsp = @{lemma + −
"(!x y p. R x y --> R (permute p x) (permute p y)) + −
==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)}+ −
+ −
fun mk_alpha_permute_rsp thm = + −
thm+ −
|> atomize+ −
|> single+ −
|> curry (op OF) permute_rsp+ −
+ −
+ −
+ −
+ −
end (* structure *)+ −
+ −