diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Sun Nov 14 12:09:14 2010 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,237 +0,0 @@
-(*  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
-  | _ => raise TERM ("Term must be a constsnt.", [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 put_perm p trm =
-  case trm of 
-     Bound _ => trm
-   | Const _ => trm
-   | t $ u => put_perm p t $ put_perm p u
-   | Abs (x, ty, t) => Abs (x, ty, put_perm p t)
-   | _ => mk_perm p trm
-
-(* 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 (put_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 (put_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;