(* Title: nominal_thmdecls.ML+ −
Author: Christian Urban+ −
+ −
Infrastructure for the lemma collection "eqvts".+ −
+ −
Provides the attributes [eqvt] and [eqvt_raw], and the theorem+ −
lists eqvts and eqvts_raw. The first attribute will store the + −
theorem in the eqvts list and also in the eqvts_raw list. For + −
the latter the theorem is expected to be of the form+ −
+ −
p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1)+ −
+ −
or+ −
+ −
c x1 x2 ... ==> c (p o x1) (p o x2) ... (2)+ −
+ −
and it is stored in the form+ −
+ −
p o c == c+ −
+ −
The [eqvt_raw] attribute just adds the theorem to eqvts_raw.+ −
+ −
TODO: In case of the form in (2) one should also+ −
add the equational form to eqvts+ −
*)+ −
+ −
signature NOMINAL_THMDECLS =+ −
sig+ −
val eqvt_add: attribute+ −
val eqvt_del: attribute+ −
val eqvt_raw_add: attribute+ −
val eqvt_raw_del: attribute+ −
val setup: theory -> theory+ −
val get_eqvts_thms: Proof.context -> thm list+ −
val get_eqvts_raw_thms: Proof.context -> thm list+ −
+ −
end;+ −
+ −
structure Nominal_ThmDecls: NOMINAL_THMDECLS =+ −
struct+ −
+ −
structure EqvtData = Generic_Data+ −
( type T = thm Item_Net.T;+ −
val empty = Thm.full_rules;+ −
val extend = I;+ −
val merge = Item_Net.merge );+ −
+ −
structure EqvtRawData = Generic_Data+ −
( type T = thm Item_Net.T;+ −
val empty = Thm.full_rules;+ −
val extend = I;+ −
val merge = Item_Net.merge );+ −
+ −
val eqvts = Item_Net.content o EqvtData.get;+ −
val eqvts_raw = Item_Net.content o EqvtRawData.get;+ −
+ −
val get_eqvts_thms = eqvts o Context.Proof;+ −
val get_eqvts_raw_thms = eqvts_raw o Context.Proof;+ −
+ −
val add_thm = EqvtData.map o Item_Net.update;+ −
val del_thm = EqvtData.map o Item_Net.remove;+ −
+ −
fun is_equiv (Const ("==", _) $ _ $ _) = true+ −
| is_equiv _ = false+ −
+ −
fun add_raw_thm thm = + −
case prop_of thm of+ −
Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm)+ −
| _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) + −
+ −
val del_raw_thm = EqvtRawData.map o Item_Net.remove;+ −
+ −
fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)+ −
| dest_perm t = raise TERM ("dest_perm", [t])+ −
+ −
fun mk_perm p trm =+ −
let+ −
val ty = fastype_of trm+ −
in+ −
Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm+ −
end+ −
+ −
fun eq_transform_tac thm = REPEAT o FIRST' + −
[CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),+ −
rtac (thm RS @{thm trans}),+ −
rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]+ −
+ −
(* transform equations into the "p o c = c"-form *)+ −
fun transform_eq ctxt thm = + −
let+ −
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))+ −
val (p, t) = dest_perm lhs+ −
val (c, args) = strip_comb t+ −
val (c', args') = strip_comb rhs+ −
val eargs = map Envir.eta_contract args + −
val eargs' = map Envir.eta_contract args'+ −
val p_str = fst (fst (dest_Var p))+ −
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))+ −
in+ −
if c <> c' + −
then error "Eqvt lemma is not of the right form (constants do not agree)"+ −
else if eargs' <> map (mk_perm p) eargs + −
then error "Eqvt lemma is not of the right form (arguments do not agree)"+ −
else if args = [] + −
then thm+ −
else Goal.prove ctxt [p_str] [] goal+ −
(fn _ => eq_transform_tac thm 1)+ −
end+ −
+ −
+ −
(* tests whether the lists of pis all agree, and that there is at least one p *)+ −
fun is_bad_list [] = true+ −
| is_bad_list [_] = false+ −
| is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true+ −
+ −
fun mk_minus p = + −
Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p + −
+ −
fun imp_transform_tac thy p p' thm = + −
let+ −
val cp = Thm.cterm_of thy p+ −
val cp' = Thm.cterm_of thy (mk_minus p')+ −
val thm' = Drule.cterm_instantiate [(cp, cp')] thm+ −
val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)}+ −
in+ −
EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac,+ −
rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp]+ −
end+ −
+ −
fun transform_imp ctxt thm =+ −
let+ −
val thy = ProofContext.theory_of ctxt+ −
val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))+ −
val (c, prem_args) = strip_comb prem+ −
val (c', concl_args) = strip_comb concl+ −
val ps = map (fst o dest_perm) concl_args handle TERM _ => [] + −
val p = try hd ps+ −
in+ −
if c <> c' + −
then error "Eqvt lemma is not of the right form (constants do not agree)"+ −
else if is_bad_list ps + −
then error "Eqvt lemma is not of the right form (permutations do not agree)" + −
else if concl_args <> map (mk_perm (the p)) prem_args + −
then error "Eqvt lemma is not of the right form (arguments do not agree)"+ −
else + −
let+ −
val prem' = Const (@{const_name "permute"}, @{typ "perm => bool => bool"}) $ (the p) $ prem + −
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl))+ −
val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt+ −
in+ −
Goal.prove ctxt' [] [] goal'+ −
(fn _ => imp_transform_tac thy (the p) p' thm 1) + −
|> singleton (ProofContext.export ctxt' ctxt)+ −
|> transform_eq ctxt+ −
end+ −
end + −
+ −
fun mk_equiv r = r RS @{thm eq_reflection};+ −
fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;+ −
+ −
fun transform addel_fun thm context = + −
let+ −
val ctxt = Context.proof_of context+ −
in+ −
case (prop_of thm) of+ −
@{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ + −
(Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>+ −
addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context+ −
| @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => + −
addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context+ −
| _ => raise error "Only _ = _ and _ ==> _ cases are implemented."+ −
end + −
+ −
val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm));+ −
val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm));+ −
+ −
val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;+ −
val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;+ −
+ −
val setup =+ −
Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) + −
(cat_lines ["Declaration of equivariance lemmas - they will automtically be", + −
"brought into the form p o c == c"]) #>+ −
Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) + −
(cat_lines ["Declaration of equivariance lemmas - no",+ −
"transformation is performed"]) #>+ −
PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>+ −
PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);+ −
+ −
+ −
end;+ −