(*  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+
−
+
−
  (* TEMPORARY FIX *)+
−
  val add_thm: thm -> Context.generic -> Context.generic+
−
  val add_raw_thm: thm -> Context.generic -> Context.generic+
−
end;+
−
+
−
structure Nominal_ThmDecls: NOMINAL_THMDECLS =+
−
struct+
−
+
−
fun get_ps trm =+
−
  case trm of +
−
     Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm])+
−
   | Const (@{const_name permute}, _) $ p $ _ => [p]+
−
   | t $ u => get_ps t @ get_ps u+
−
   | Abs (_, _, t) => get_ps t +
−
   | _ => []+
−
+
−
fun put_p p trm =+
−
  case trm of +
−
     Bound _ => trm+
−
   | Const _ => trm+
−
   | t $ u => put_p p t $ put_p p u+
−
   | Abs (x, ty, t) => Abs (x, ty, put_p p t)+
−
   | _ => mk_perm p trm+
−
+
−
(* tests whether the lists of ps 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+
−
+
−
+
−
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 add_raw_thm thm = +
−
  case prop_of thm of+
−
    Const ("==", _) $ _ $ _ => +
−
      EqvtRawData.map (Item_Net.update (zero_var_indexes thm))+
−
  | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) +
−
+
−
val del_raw_thm = EqvtRawData.map o Item_Net.remove;+
−
+
−
+
−
(** transformation of eqvt lemmas **)+
−
+
−
+
−
(* 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 ((p, t), rhs) = apfst dest_perm +
−
    (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)))+
−
    handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c...  = c..."+
−
  val ps = get_ps rhs handle TERM _ => []  +
−
  val (c, c') = (head_of t, head_of rhs)+
−
in+
−
  if c <> c' +
−
    then error "Eqvt lemma is not of the right form (constants do not agree)"+
−
  else if is_bad_list (p::ps)  +
−
    then error "Eqvt lemma is not of the right form (permutations do not agree)" +
−
  else if not (rhs aconv (put_p p t))+
−
    then error "Eqvt lemma is not of the right form (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+
−
    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 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 eqvt_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, c') = (head_of prem, head_of concl)+
−
  val ps = get_ps concl 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 not (concl aconv (put_p (the p) prem)) +
−
    then error "Eqvt lemma is not of the right form (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 thy (the p) p' thm 1) +
−
      |> singleton (ProofContext.export ctxt' ctxt)+
−
      |> eqvt_transform_eq ctxt+
−
    end+
−
end     +
−
+
−
fun eqvt_transform ctxt thm = +
−
 case (prop_of thm) of+
−
   @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ +
−
     (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => +
−
       eqvt_transform_eq ctxt thm+
−
 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => +
−
     eqvt_transform_imp ctxt thm+
−
 | _ => 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"]) #>+
−
  PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>+
−
  PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);+
−
+
−
+
−
end;+
−