diff -r a8724924a62e -r 13ab4f0a0b0e Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Tue Mar 26 16:41:31 2013 +0100
+++ b/Nominal/nominal_thmdecls.ML	Wed Mar 27 16:08:30 2013 +0100
@@ -1,27 +1,59 @@
 (*  Title:      nominal_thmdecls.ML
     Author:     Christian Urban
+    Author:     Tjark Weber
 
-  Infrastructure for the lemma collection "eqvts".
+  Infrastructure for the lemma collections "eqvts", "eqvts_raw".
 
   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
+  lists "eqvts" and "eqvts_raw".
+
+  The [eqvt] attribute expects a theorem of the form
+
+    ?p \<bullet> (c ?x1 ?x2 ...) = c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ...    (1)
+
+  or, if c is a relation with arity >= 1, of the form
+
+    c ?x1 ?x2 ... ==> c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ...         (2)
 
-    p o (c x1 x2 ...) = c (p o x1) (p o x2) ...    (1)
+  [eqvt] will store this theorem in the form (1) or, if c
+  is a relation with arity >= 1, in the form
+
+    c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ... = c ?x1 ?x2 ...           (3)
 
-  or
+  in "eqvts". (The orientation of (3) was chosen because
+  Isabelle's simplifier uses equations from left to right.)
+  [eqvt] will also derive and store the theorem
+
+    ?p \<bullet> c == c                                           (4)
+
+  in "eqvts_raw".
 
-    c x1 x2 ... ==> c (p o x1) (p o x2) ...        (2)
+  (1)-(4) are all logically equivalent. We consider (1) and (2)
+  to be more end-user friendly, i.e., slightly more natural to
+  understand and prove, while (3) and (4) make the rewriting
+  system for equivariance more predictable and less prone to
+  looping in Isabelle.
 
-  and it is stored in the form
+  The [eqvt_raw] attribute expects a theorem of the form (4),
+  and merely stores it in "eqvts_raw".
 
-    p o c == c
+  [eqvt_raw] is provided because certain equivariance theorems
+  would lead to looping when used for simplification in the form
+  (1): notably, equivariance of permute (infix \<bullet>), i.e.,
+  ?p \<bullet> (?q \<bullet> ?x) = (?p \<bullet> ?q) \<bullet> (?p \<bullet> ?x).
 
-  The [eqvt_raw] attribute just adds the theorem to eqvts_raw.
+  To support binders such as All/Ex/Ball/Bex etc., which are
+  typically applied to abstractions, argument terms ?xi (as well
+  as permuted arguments ?p \<bullet> ?xi) in (1)-(3) need not be eta-
+  contracted, i.e., they may be of the form "%z. ?xi z" or
+  "%z. (?p \<bullet> ?x) z", respectively.
 
-  TODO: In case of the form in (2) one should also
-        add the equational form to eqvts
+  For convenience, argument terms ?xi (as well as permuted
+  arguments ?p \<bullet> ?xi) in (1)-(3) may actually be tuples, e.g.,
+  "(?xi, ?xj)" or "(?p \<bullet> ?xi, ?p \<bullet> ?xj)", respectively.
+
+  In (1)-(4), "c" is either a (global) constant or a locally
+  fixed parameter, e.g., of a locale or type class.
 *)
 
 signature NOMINAL_THMDECLS =
@@ -46,206 +78,246 @@
   val extend = I;
   val merge = Item_Net.merge);
 
+(* EqvtRawData is implemented with a Termtab (rather than an
+   Item_Net) so that we can efficiently decide whether a given
+   constant has a corresponding equivariance theorem stored, cf.
+   the function is_eqvt. *)
 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;
-
-fun checked_update key net =
-  (if Item_Net.member net key then 
-     warning "Theorem already declared as equivariant."
-   else (); 
-   Item_Net.update key net)
-
-val add_thm = EqvtData.map o checked_update;
-val del_thm = EqvtData.map o Item_Net.remove;
+val eqvts = Item_Net.content o EqvtData.get
+val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get
 
-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]) *)
-
+val get_eqvts_thms = eqvts o Context.Proof
+val get_eqvts_raw_thms = eqvts_raw o Context.Proof
 
 
-(** transformation of eqvt lemmas **)
+(** raw equivariance 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 
-   | _ => []
+(* Returns true iff an equivariance lemma exists in "eqvts_raw"
+   for a given term. *)
+val is_eqvt =
+  Termtab.defined o EqvtRawData.get o Context.Proof
 
-fun add_perm p trm =
+(* Returns c if thm is of the form (4), raises an error
+   otherwise. *)
+fun key_of_raw_thm context thm =
   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
+    fun error_msg () =
+      error
+        ("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^
+         Syntax.string_of_term (Context.proof_of context) (prop_of thm))
+  in
+    case prop_of thm of
+      Const ("==", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' =>
+        if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then
+          c
+        else
+          error_msg ()
+    | _ => error_msg ()
+  end
+
+fun add_raw_thm thm context =
+  let
+    val c = key_of_raw_thm context thm
   in
-    strip_comb trm
-    ||> map aux
-    |> list_comb
-  end  
+    if Termtab.defined (EqvtRawData.get context) c then
+      warning ("Replacing existing raw equivariance theorem for \"" ^
+        Syntax.string_of_term (Context.proof_of context) c ^ "\".")
+    else ();
+    EqvtRawData.map (Termtab.update (c, thm)) context
+  end
+
+fun del_raw_thm thm context =
+  let
+    val c = key_of_raw_thm context thm
+  in
+    if Termtab.defined (EqvtRawData.get context) c then
+      EqvtRawData.map (Termtab.delete c) context
+    else (
+      warning ("Cannot delete non-existing raw equivariance theorem for \"" ^
+        Syntax.string_of_term (Context.proof_of context) c ^ "\".");
+      context
+    )
+  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
+(** adding/deleting lemmas to/from "eqvts" **)
+
+fun add_thm thm context =
+  (
+    if Item_Net.member (EqvtData.get context) thm then
+      warning ("Theorem already declared as equivariant:\n" ^
+        Syntax.string_of_term (Context.proof_of context) (prop_of thm))
+    else ();
+    EqvtData.map (Item_Net.update thm) context
+  )
+
+fun del_thm thm context =
+  (
+    if Item_Net.member (EqvtData.get context) thm then
+      EqvtData.map (Item_Net.remove thm) context
+    else (
+      warning ("Cannot delete non-existing equivariance theorem:\n" ^
+        Syntax.string_of_term (Context.proof_of context) (prop_of thm));
+      context
+    )
+  )
 
 
-(* transforms equations into the "p o c == c"-form 
-   from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)
+(** transformation of equivariance lemmas **)
+
+(* Transforms a theorem of the form (1) into the form (4). *)
+local
 
-fun eqvt_transform_eq_tac thm = 
-let
-  val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}
+fun 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
+
 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 "
+fun thm_4_of_1 ctxt thm =
+  let
+    val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop
+      |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt)
+    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
-    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 (Proof_Context.export ctxt' ctxt)
-        |> safe_mk_equiv
-        |> zero_var_indexes
-      end
+    Goal.prove ctxt [] [] goal' (fn _ => tac thm 1)
+      |> singleton (Proof_Context.export ctxt' ctxt)
+      |> (fn th => th RS @{thm "eq_reflection"})
+      |> zero_var_indexes
+  end
+  handle TERM _ =>
+    raise THM ("thm_4_of_1", 0, [thm])
+
+end (* local *)
+
+(* Transforms a theorem of the form (2) into the form (1). *)
+local
+
+fun tac thm thm' =
+  let
+    val ss_thms = @{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 (HOL_basic_ss addsimps ss_thms)]
   end
 
-(* transforms equations into the "p o c == c"-form 
-   from R x1 ...xn ==> R (p o x1) ... (p o xn) *)
+in
 
-fun eqvt_transform_imp_tac ctxt p p' thm = 
+fun thm_1_of_2 ctxt thm =
   let
-    val thy = Proof_Context.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 "
+    val (prem, concl) = thm |> prop_of |> Logic.dest_implies |> pairself HOLogic.dest_Trueprop
+    (* since argument terms "?p \<bullet> ?x1" may actually be eta-expanded
+       or tuples, we need the following function to find ?p *)
+    fun find_perm (Const (@{const_name "permute"}, _) $ (p as Var _) $ _) = p
+      | find_perm (Const (@{const_name "Pair"}, _) $ x $ _) = find_perm x
+      | find_perm (Abs (_, _, body)) = find_perm body
+      | find_perm _ = raise THM ("thm_3_of_2", 0, [thm])
+    val p = concl |> dest_comb |> snd |> find_perm
+    val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl))
+    val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
+    val certify = cterm_of (theory_of_thm thm)
+    val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm
   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 (Proof_Context.export ctxt' ctxt)
-      end
-  end     
+    Goal.prove ctxt' [] [] goal' (fn _ => tac thm thm' 1)
+      |> singleton (Proof_Context.export ctxt' ctxt)
+  end
+  handle TERM _ =>
+    raise THM ("thm_1_of_2", 0, [thm])
+
+end (* local *)
+
+(* Transforms a theorem of the form (1) into the form (3). *)
+fun thm_3_of_1 _ thm =
+  (thm RS (@{thm "permute_bool_def"} RS @{thm "sym"} RS @{thm "trans"}) RS @{thm "sym"})
+    |> zero_var_indexes
+
+local
+  val msg = cat_lines
+    ["Equivariance theorem must be of the form",
+     "  ?p \<bullet> (c ?x1 ?x2 ...) = c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ...",
+     "or, if c is a relation with arity >= 1, of the form",
+     "  c ?x1 ?x2 ... ==> c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ..."]
+in
 
-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."
- 
+(* Transforms a theorem of the form (1) or (2) into the form (4). *)
+fun eqvt_transform ctxt thm =
+  (case prop_of thm of @{const "Trueprop"} $ _ =>
+    thm_4_of_1 ctxt thm
+  | @{const "==>"} $ _ $ _ =>
+    thm_4_of_1 ctxt (thm_1_of_2 ctxt thm)
+  | _ =>
+    error msg)
+  handle THM _ =>
+    error msg
+
+(* Transforms a theorem of the form (1) into theorems of the
+   form (1) (or, if c is a relation with arity >= 1, of the form
+   (3)) and (4); transforms a theorem of the form (2) into
+   theorems of the form (3) and (4). *)
+fun eqvt_and_raw_transform ctxt thm =
+  (case prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) =>
+    let
+      val th' =
+        if fastype_of c_args = @{typ "bool"}
+            andalso (not o null) (snd (fixed_nonfixed_args ctxt c_args)) then
+          thm_3_of_1 ctxt thm
+        else
+          thm
+    in
+      (th', thm_4_of_1 ctxt thm)
+    end
+  | @{const "==>"} $ _ $ _ =>
+    let
+      val th1 = thm_1_of_2 ctxt thm
+    in
+      (thm_3_of_1 ctxt th1, thm_4_of_1 ctxt th1)
+    end
+  | _ =>
+    error msg)
+  handle THM _ =>
+    error msg
+
+end (* local *)
+
 
 (** 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_raw_add = Thm.declaration_attribute add_raw_thm
+val eqvt_raw_del = Thm.declaration_attribute del_raw_thm
 
-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)
+fun eqvt_add_or_del eqvt_fn raw_fn =
+  Thm.declaration_attribute
+    (fn thm => fn context =>
+      let
+        val (eqvt, raw) = eqvt_and_raw_transform (Context.proof_of context) thm
+      in
+        context |> eqvt_fn eqvt |> raw_fn raw
+      end)
 
-val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
-val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;
+val eqvt_add = eqvt_add_or_del add_thm add_raw_thm
+val eqvt_del = eqvt_add_or_del del_thm 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"]) #>
+  Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del)
+    "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #>
+  Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del)
+    "Declaration of raw equivariance lemmas - no transformation is performed" #>
   Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
-  Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);
-
+  Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw)
 
 end;