(* 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 -> boolend;structure Nominal_ThmDecls: NOMINAL_THMDECLS =structstructure 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}]endfun 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] endfun 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;