Started proving strong induction.
(* Title: nominal_thmdecls.ML+ −
Author: Brian Huffman, Christian Urban+ −
*)+ −
+ −
signature NOMINAL_PERMEQ =+ −
sig+ −
val eqvt_tac: Proof.context -> int -> tactic + −
+ −
end;+ −
+ −
(* TODO:+ −
+ −
- provide a method interface with the usual add and del options+ −
+ −
- print a warning if for a constant no eqvt lemma is stored+ −
+ −
- there seems to be too much simplified in case of multiple + −
permutations, like+ −
+ −
p o q o r o x + −
+ −
we usually only want the outermost permutation to "float" in+ −
*)+ −
+ −
+ −
structure Nominal_Permeq: NOMINAL_PERMEQ =+ −
struct+ −
+ −
local+ −
+ −
fun eqvt_apply_conv ctxt ct =+ −
case (term_of ct) of+ −
(Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>+ −
let+ −
val (perm, t) = Thm.dest_comb ct+ −
val (_, p) = Thm.dest_comb perm+ −
val (f, x) = Thm.dest_comb t+ −
val a = ctyp_of_term x;+ −
val b = ctyp_of_term t;+ −
val ty_insts = map SOME [b, a]+ −
val term_insts = map SOME [p, f, x]+ −
in+ −
Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}+ −
end+ −
| _ => Conv.no_conv ct+ −
+ −
fun eqvt_lambda_conv ctxt ct =+ −
case (term_of ct) of+ −
(Const (@{const_name "permute"}, _) $ _ $ Abs _) =>+ −
Conv.rewr_conv @{thm eqvt_lambda} ct+ −
| _ => Conv.no_conv ct+ −
+ −
in+ −
+ −
fun eqvt_conv ctxt ct =+ −
Conv.first_conv+ −
[ Conv.rewr_conv @{thm eqvt_bound},+ −
eqvt_apply_conv ctxt+ −
then_conv Conv.comb_conv (eqvt_conv ctxt),+ −
eqvt_lambda_conv ctxt+ −
then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,+ −
More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt),+ −
Conv.all_conv+ −
] ct+ −
+ −
fun eqvt_tac ctxt = + −
CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)+ −
+ −
end+ −
+ −
end; (* structure *)+ −