File ‹nominal_permeq.ML›
signature NOMINAL_PERMEQ =
sig
val perm_fun_simproc : simproc
val perm_app_simproc : simproc
val perm_simp_tac : Proof.context -> int -> tactic
val perm_extend_simp_tac : Proof.context -> int -> tactic
val supports_tac : Proof.context -> int -> tactic
val finite_guess_tac : Proof.context -> int -> tactic
val fresh_guess_tac : Proof.context -> int -> tactic
val perm_simp_meth : (Proof.context -> Proof.method) context_parser
val perm_simp_meth_debug : (Proof.context -> Proof.method) context_parser
val perm_extend_simp_meth : (Proof.context -> Proof.method) context_parser
val perm_extend_simp_meth_debug : (Proof.context -> Proof.method) context_parser
val supports_meth : (Proof.context -> Proof.method) context_parser
val supports_meth_debug : (Proof.context -> Proof.method) context_parser
val finite_guess_meth : (Proof.context -> Proof.method) context_parser
val finite_guess_meth_debug : (Proof.context -> Proof.method) context_parser
val fresh_guess_meth : (Proof.context -> Proof.method) context_parser
val fresh_guess_meth_debug : (Proof.context -> Proof.method) context_parser
end
structure NominalPermeq : NOMINAL_PERMEQ =
struct
val finite_emptyI = @{thm "finite.emptyI"};
val finite_Un = @{thm "finite_Un"};
val conj_absorb = @{thm "conj_absorb"};
val not_false = @{thm "not_False_eq_True"}
val perm_fun_def = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"};
val perm_eq_app = @{thm "Nominal.pt_fun_app_eq"};
val supports_def = Simpdata.mk_eq @{thm "Nominal.supports_def"};
val fresh_def = Simpdata.mk_eq @{thm "Nominal.fresh_def"};
val fresh_prod = @{thm "Nominal.fresh_prod"};
val fresh_unit = @{thm "Nominal.fresh_unit"};
val supports_rule = @{thm "supports_finite"};
val supp_prod = @{thm "supp_prod"};
val supp_unit = @{thm "supp_unit"};
val pt_perm_compose_aux = @{thm "pt_perm_compose_aux"};
val cp1_aux = @{thm "cp1_aux"};
val perm_aux_fold = @{thm "perm_aux_fold"};
val supports_fresh_rule = @{thm "supports_fresh"};
val strong_congs = [@{thm "if_cong"}]
val weak_congs = [@{thm "if_weak_cong"}]
fun DEBUG ctxt (msg,tac) =
CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]);
fun NO_DEBUG _ (_,tac) = CHANGED tac;
fun perm_app_proc ctxt ct =
let
val thy = Proof_Context.theory_of ctxt
val redex = Thm.term_of ct
fun applicable_app t =
(case (strip_comb t) of
(Const (\<^const_name>‹Nominal.perm›,_),ts) => (length ts) >= 2
| (Const _,_) => false
| _ => true)
in
case redex of
(Const(\<^const_name>‹Nominal.perm›,
Type(\<^type_name>‹fun›,
[Type(\<^type_name>‹list›, [Type(\<^type_name>‹prod›,[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(if (applicable_app f) then
let
val name = Long_Name.base_name n
val at_inst = Global_Theory.get_thm thy ("at_" ^ name ^ "_inst")
val pt_inst = Global_Theory.get_thm thy ("pt_" ^ name ^ "_inst")
in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
else NONE)
| _ => NONE
end
val perm_app_simproc = \<^simproc_setup>‹passive perm_app ("Nominal.perm pi x") = ‹K perm_app_proc››
fun perm_fun_proc ctxt ct =
let
val redex = Thm.term_of ct
fun applicable_fun t =
(case (strip_comb t) of
(Abs _ ,[]) => true
| (Const (\<^const_name>‹Nominal.perm›,_),_) => false
| (Const _, _) => true
| _ => false)
in
case redex of
(Const(\<^const_name>‹Nominal.perm›,_) $ pi $ f) =>
(if applicable_fun f then SOME perm_fun_def else NONE)
| _ => NONE
end
val perm_fun_simproc = \<^simproc_setup>‹passive perm_fun ("Nominal.perm pi x") = ‹K perm_fun_proc››
fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i =
("general simplification of permutations", fn st => SUBGOAL (fn _ =>
let
val ctxt' = ctxt
addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms)
addsimprocs [perm_fun_simproc, perm_app_simproc]
|> fold Simplifier.del_cong weak_congs
|> fold Simplifier.add_cong strong_congs
in
stac ctxt' i
end) i st);
fun perm_simp stac ctxt =
let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
in
perm_simp_gen stac simps [] ctxt
end;
fun eqvt_simp stac ctxt =
let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
val eqvts_thms = NominalThmDecls.get_eqvt_thms ctxt;
in
perm_simp_gen stac simps eqvts_thms ctxt
end;
fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i));
fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i));
val perm_simp_tac_i = perm_simp_tac_gen_i simp_tac
val perm_asm_simp_tac_i = perm_simp_tac_gen_i asm_simp_tac
val perm_full_simp_tac_i = perm_simp_tac_gen_i full_simp_tac
val perm_asm_lr_simp_tac_i = perm_simp_tac_gen_i asm_lr_simp_tac
val perm_asm_full_simp_tac_i = perm_simp_tac_gen_i asm_full_simp_tac
val eqvt_asm_full_simp_tac_i = eqvt_simp_tac_gen_i asm_full_simp_tac
fun perm_compose_proc ctxt ct =
(case Thm.term_of ct of
(Const (\<^const_name>‹Nominal.perm›, Type (\<^type_name>‹fun›, [Type (\<^type_name>‹list›,
[Type (\<^type_name>‹Product_Type.prod›, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (\<^const_name>‹Nominal.perm›,
Type (\<^type_name>‹fun›, [Type (\<^type_name>‹list›, [Type (\<^type_name>‹Product_Type.prod›, [U as Type (uname,_),_])]),_])) $
pi2 $ t)) =>
let
val thy = Proof_Context.theory_of ctxt
val tname' = Long_Name.base_name tname
val uname' = Long_Name.base_name uname
in
if pi1 <> pi2 then
if T = U then
SOME (Thm.instantiate'
[SOME (Thm.global_ctyp_of thy (fastype_of t))]
[SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
(mk_meta_eq ([Global_Theory.get_thm thy ("pt_"^tname'^"_inst"),
Global_Theory.get_thm thy ("at_"^tname'^"_inst")] MRS pt_perm_compose_aux)))
else
SOME (Thm.instantiate'
[SOME (Thm.global_ctyp_of thy (fastype_of t))]
[SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
(mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS
cp1_aux)))
else NONE
end
| _ => NONE);
val perm_compose_simproc =
\<^simproc_setup>‹passive perm_compose ("perm pi1 (perm pi2 t)") = ‹K perm_compose_proc››;
fun perm_compose_tac ctxt i =
("analysing permutation compositions on the lhs",
fn st => EVERY
[resolve_tac ctxt [trans] i,
asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i,
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st);
fun apply_cong_tac ctxt i = ("application of congruence", cong_tac ctxt i);
fun unfold_perm_fun_def_tac ctxt i =
("unfolding of permutations on functions",
resolve_tac ctxt [HOLogic.mk_obj_eq perm_fun_def RS trans] i)
fun ext_fun_tac ctxt i =
("extensionality expansion of functions", resolve_tac ctxt @{thms ext} i);
fun perm_extend_simp_tac_i tactical ctxt =
let fun perm_extend_simp_tac_aux tactical ctxt n =
if n=0 then K all_tac
else DETERM o
(FIRST'
[fn i => tactical ctxt ("splitting conjunctions on the rhs", resolve_tac ctxt [conjI] i),
fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
fn i => tactical ctxt (perm_compose_tac ctxt i),
fn i => tactical ctxt (apply_cong_tac ctxt i),
fn i => tactical ctxt (unfold_perm_fun_def_tac ctxt i),
fn i => tactical ctxt (ext_fun_tac ctxt i)]
THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
in perm_extend_simp_tac_aux tactical ctxt 10 end;
fun supports_tac_i tactical ctxt i =
let
val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod]
in
EVERY [tactical ctxt ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
tactical ctxt ("stripping of foralls ", REPEAT_DETERM (resolve_tac ctxt [allI] i)),
tactical ctxt ("geting rid of the imps ", resolve_tac ctxt [impI] i),
tactical ctxt ("eliminating conjuncts ", REPEAT_DETERM (eresolve_tac ctxt [conjE] i)),
tactical ctxt ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i)]
end;
fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs
| collect_vars i (v as Free _) vs = insert (op =) v vs
| collect_vars i (v as Var _) vs = insert (op =) v vs
| collect_vars i (Const _) vs = vs
| collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
| collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
fun finite_guess_tac_i tactical ctxt i st =
let val goal = nth (cprems_of st) (i - 1)
in
case Envir.eta_contract (Logic.strip_assums_concl (Thm.term_of goal)) of
_ $ (Const (\<^const_name>‹finite›, _) $ (Const (\<^const_name>‹Nominal.supp›, T) $ x)) =>
let
val ps = Logic.strip_params (Thm.term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 x [];
val s = fold_rev (fn v => fn s =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
vs HOLogic.unit;
val s' = fold_rev Term.abs ps
(Const (\<^const_name>‹Nominal.supp›, fastype_of1 (Ts, s) -->
Term.range_type T) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (Thm.prems_of supports_rule'));
val supports_rule'' =
infer_instantiate ctxt
[(#1 (dest_Var (head_of S)), Thm.cterm_of ctxt s')] supports_rule';
val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
(tactical ctxt ("guessing of the right supports-set",
EVERY [compose_tac ctxt (false, supports_rule'', 2) i,
asm_full_simp_tac ctxt' (i+1),
supports_tac_i tactical ctxt i])) st
end
| _ => Seq.empty
end
handle General.Subscript => Seq.empty
fun fresh_guess_tac_i tactical ctxt i st =
let
val goal = nth (cprems_of st) (i - 1)
val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm"
val ctxt1 = ctxt addsimps [Thm.symmetric fresh_def,fresh_prod,fresh_unit,conj_absorb,not_false]@fresh_atm
val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
case Logic.strip_assums_concl (Thm.term_of goal) of
_ $ (Const (\<^const_name>‹Nominal.fresh›, Type ("fun", [T, _])) $ _ $ t) =>
let
val ps = Logic.strip_params (Thm.term_of goal);
val Ts = rev (map snd ps);
val vs = collect_vars 0 t [];
val s = fold_rev (fn v => fn s =>
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
vs HOLogic.unit;
val s' =
fold_rev Term.abs ps
(Const (\<^const_name>‹Nominal.supp›, fastype_of1 (Ts, s) --> HOLogic.mk_setT T) $ s);
val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (Thm.prems_of supports_fresh_rule'));
val supports_fresh_rule'' =
infer_instantiate ctxt
[(#1 (dest_Var (head_of S)), Thm.cterm_of ctxt s')] supports_fresh_rule';
in
(tactical ctxt ("guessing of the right set that supports the goal",
(EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
asm_full_simp_tac ctxt1 (i+2),
asm_full_simp_tac ctxt2 (i+1),
supports_tac_i tactical ctxt i]))) st
end
| _ => (tactical ctxt ("if it is not of the form _♯_, then try the simplifier",
(asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st
end
handle General.Subscript => Seq.empty;
val eqvt_simp_tac = eqvt_asm_full_simp_tac_i NO_DEBUG;
val perm_simp_tac = perm_asm_full_simp_tac_i NO_DEBUG;
val perm_extend_simp_tac = perm_extend_simp_tac_i NO_DEBUG;
val supports_tac = supports_tac_i NO_DEBUG;
val finite_guess_tac = finite_guess_tac_i NO_DEBUG;
val fresh_guess_tac = fresh_guess_tac_i NO_DEBUG;
val dperm_simp_tac = perm_asm_full_simp_tac_i DEBUG;
val dperm_extend_simp_tac = perm_extend_simp_tac_i DEBUG;
val dsupports_tac = supports_tac_i DEBUG;
val dfinite_guess_tac = finite_guess_tac_i DEBUG;
val dfresh_guess_tac = fresh_guess_tac_i DEBUG;
val no_asmN = "no_asm";
val no_asm_useN = "no_asm_use";
val no_asm_simpN = "no_asm_simp";
val asm_lrN = "asm_lr";
val perm_simp_options =
(Args.parens (Args.$$$ no_asmN) >> K (perm_simp_tac_i NO_DEBUG) ||
Args.parens (Args.$$$ no_asm_simpN) >> K (perm_asm_simp_tac_i NO_DEBUG) ||
Args.parens (Args.$$$ no_asm_useN) >> K (perm_full_simp_tac_i NO_DEBUG) ||
Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG) ||
Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG));
val perm_simp_meth =
Scan.lift perm_simp_options --| Method.sections (Simplifier.simp_modifiers') >>
(fn tac => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o tac ctxt));
fun local_simp_meth_setup tac =
Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
(K (SIMPLE_METHOD' o tac));
fun basic_simp_meth_setup debug tac =
Scan.depend (fn context => Scan.succeed (Simplifier.map_ss (put_simpset HOL_basic_ss) context, ())) --
Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
(K (SIMPLE_METHOD' o (if debug then tac else SOLVED' o tac)));
val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac;
val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac;
val perm_extend_simp_meth_debug = local_simp_meth_setup dperm_extend_simp_tac;
val supports_meth = local_simp_meth_setup supports_tac;
val supports_meth_debug = local_simp_meth_setup dsupports_tac;
val finite_guess_meth = basic_simp_meth_setup false finite_guess_tac;
val finite_guess_meth_debug = basic_simp_meth_setup true dfinite_guess_tac;
val fresh_guess_meth = basic_simp_meth_setup false fresh_guess_tac;
val fresh_guess_meth_debug = basic_simp_meth_setup true dfresh_guess_tac;
end