(* 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+ −
val eqvt_transform: Proof.context -> thm -> thm+ −
val is_eqvt: Proof.context -> term -> bool+ −
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 Termtab.table;+ −
val empty = Termtab.empty;+ −
val extend = I;+ −
val merge = Termtab.merge (K true));+ −
+ −
val eqvts = Item_Net.content o EqvtData.get;+ −
val eqvts_raw = map snd o Termtab.dest 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 add_raw_thm thm = + −
case prop_of thm of+ −
Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) + −
| _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) + −
+ −
fun del_raw_thm thm = + −
case prop_of thm of+ −
Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c)+ −
| _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) + −
+ −
fun is_eqvt ctxt trm =+ −
case trm of + −
(c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c+ −
| _ => false (* raise TERM ("Term must be a constant.", [trm]) *)+ −
+ −
+ −
+ −
(** transformation of eqvt lemmas **)+ −
+ −
fun get_perms trm =+ −
case trm of + −
Const (@{const_name permute}, _) $ _ $ (Bound _) => + −
raise TERM ("get_perms called on bound", [trm])+ −
| Const (@{const_name permute}, _) $ p $ _ => [p]+ −
| t $ u => get_perms t @ get_perms u+ −
| Abs (_, _, t) => get_perms t + −
| _ => []+ −
+ −
fun add_perm p trm =+ −
let+ −
fun aux trm = + −
case trm of + −
Bound _ => trm+ −
| Const _ => trm+ −
| t $ u => aux t $ aux u+ −
| Abs (x, ty, t) => Abs (x, ty, aux t)+ −
| _ => mk_perm p trm+ −
in+ −
strip_comb trm+ −
||> map aux+ −
|> list_comb+ −
end + −
+ −
+ −
(* tests whether there is a disagreement between the permutations, + −
and that there is at least one permutation *)+ −
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+ −
+ −
+ −
(* transforms equations into the "p o c == c"-form + −
from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)+ −
+ −
fun eqvt_transform_eq_tac thm = + −
let+ −
val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}+ −
in+ −
REPEAT o FIRST' + −
[CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms),+ −
rtac (thm RS @{thm trans}),+ −
rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]+ −
end+ −
+ −
fun eqvt_transform_eq ctxt thm = + −
let+ −
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))+ −
handle TERM _ => error "Equivariance lemma must be an equality."+ −
val (p, t) = dest_perm lhs + −
handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..."+ −
+ −
val ps = get_perms rhs handle TERM _ => [] + −
val (c, c') = (head_of t, head_of rhs)+ −
val msg = "Equivariance lemma is not of the right form "+ −
in+ −
if c <> c' + −
then error (msg ^ "(constants do not agree).")+ −
else if is_bad_list (p :: ps) + −
then error (msg ^ "(permutations do not agree).") + −
else if not (rhs aconv (add_perm p t))+ −
then error (msg ^ "(arguments do not agree).")+ −
else if is_Const t + −
then safe_mk_equiv thm+ −
else + −
let + −
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))+ −
val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt+ −
in+ −
Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)+ −
|> singleton (ProofContext.export ctxt' ctxt)+ −
|> safe_mk_equiv+ −
|> zero_var_indexes+ −
end+ −
end+ −
+ −
(* transforms equations into the "p o c == c"-form + −
from R x1 ...xn ==> R (p o x1) ... (p o xn) *)+ −
+ −
fun eqvt_transform_imp_tac ctxt p p' thm = + −
let+ −
val thy = ProofContext.theory_of ctxt+ −
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 eqvt_transform_imp ctxt thm =+ −
let+ −
val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))+ −
val (c, c') = (head_of prem, head_of concl)+ −
val ps = get_perms concl handle TERM _ => [] + −
val p = try hd ps+ −
val msg = "Equivariance lemma is not of the right form "+ −
in+ −
if c <> c' + −
then error (msg ^ "(constants do not agree).")+ −
else if is_bad_list ps + −
then error (msg ^ "(permutations do not agree).") + −
else if not (concl aconv (add_perm (the p) prem)) + −
then error (msg ^ "(arguments do not agree).")+ −
else + −
let+ −
val prem' = mk_perm (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 _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) + −
|> singleton (ProofContext.export ctxt' ctxt)+ −
end+ −
end + −
+ −
fun eqvt_transform ctxt thm = + −
case (prop_of thm) of+ −
@{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ + −
(Const (@{const_name "permute"}, _) $ _ $ _) $ _) => + −
eqvt_transform_eq ctxt thm+ −
| @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => + −
eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt+ −
| _ => raise error "Only _ = _ and _ ==> _ cases are implemented."+ −
+ −
+ −
(** attributes **)+ −
+ −
val eqvt_add = Thm.declaration_attribute + −
(fn thm => fn context =>+ −
let+ −
val thm' = eqvt_transform (Context.proof_of context) thm+ −
in+ −
context |> add_thm thm |> add_raw_thm thm'+ −
end)+ −
+ −
val eqvt_del = Thm.declaration_attribute+ −
(fn thm => fn context =>+ −
let+ −
val thm' = eqvt_transform (Context.proof_of context) thm+ −
in+ −
context |> del_thm thm |> del_raw_thm thm'+ −
end)+ −
+ −
val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;+ −
val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;+ −
+ −
+ −
(** setup function **)+ −
+ −
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"]) #>+ −
Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>+ −
Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);+ −
+ −
+ −
end;+ −