# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272280094 -7200
# Node ID 186d8486dfd57ac1c400637650b796508a3c830d
# Parent  7de54c9f81ac880f254c398369595a962987f7cc
rewrote eqvts_raw to be a symtab, that can be looked up

diff -r 7de54c9f81ac -r 186d8486dfd5 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Mon Apr 26 08:19:11 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Mon Apr 26 13:08:14 2010 +0200
@@ -235,6 +235,7 @@
 apply(simp)
 done
 
+
 section {* Equivariance automation *}
 
 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
@@ -242,6 +243,7 @@
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
+ML {* Thm.full_rules *}
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
@@ -369,6 +371,15 @@
 apply(perm_simp exclude: The)
 oops
 
+
+thm eqvts
+thm eqvts_raw
+
+ML {*
+Nominal_ThmDecls.is_eqvt @{context} @{term "supp"}
+*}
+
+
 (* automatic equivariance procedure for 
    inductive definitions *)
 use "nominal_eqvt.ML"
diff -r 7de54c9f81ac -r 186d8486dfd5 Nominal-General/nominal_thmdecls.ML
--- a/Nominal-General/nominal_thmdecls.ML	Mon Apr 26 08:19:11 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML	Mon Apr 26 13:08:14 2010 +0200
@@ -34,6 +34,7 @@
   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
 
   (* TEMPORARY FIX *)
   val add_thm: thm -> Context.generic -> Context.generic
@@ -43,44 +44,20 @@
 structure Nominal_ThmDecls: NOMINAL_THMDECLS =
 struct
 
-fun get_ps trm =
-  case trm of 
-     Const (@{const_name permute}, _) $ p $ (Bound _) => 
-       raise TERM ("get_ps called on bound", [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 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
-
-
 structure EqvtData = Generic_Data
 ( type T = thm Item_Net.T;
   val empty = Thm.full_rules;
   val extend = I;
-  val merge = Item_Net.merge );
+  val merge = Item_Net.merge);
 
 structure EqvtRawData = Generic_Data
-( type T = thm Item_Net.T;
-  val empty = Thm.full_rules;
+( type T = thm Symtab.table;
+  val empty = Symtab.empty;
   val extend = I;
-  val merge = Item_Net.merge );
+  val merge = Symtab.merge (K true));
 
 val eqvts = Item_Net.content o EqvtData.get;
-val eqvts_raw = Item_Net.content o EqvtRawData.get;
+val eqvts_raw = map snd o Symtab.dest o EqvtRawData.get;
 
 val get_eqvts_thms = eqvts o  Context.Proof;
 val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
@@ -90,14 +67,46 @@
 
 fun add_raw_thm thm = 
   case prop_of thm of
-    Const ("==", _) $ _ $ _ => (EqvtRawData.map o Item_Net.update) thm
-  | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) 
+    Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.update (c, thm))
+  | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) 
 
-val del_raw_thm = EqvtRawData.map o Item_Net.remove;
+fun del_raw_thm thm = 
+  case prop_of thm of
+    Const ("==", _) $ _ $ Const (c, _) => EqvtRawData.map (Symtab.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 
+    Const (c, _) => Symtab.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) *)
@@ -119,15 +128,15 @@
   val (p, t) = dest_perm lhs 
     handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c...  = c..."
 
-  val ps = get_ps rhs handle TERM _ => []  
+  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)  
+  else if is_bad_list (p :: ps)  
     then error (msg ^ "(permutations do not agree).") 
-  else if not (rhs aconv (put_p p t))
+  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
@@ -162,7 +171,7 @@
 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_ps concl handle TERM _ => []  
+  val ps = get_perms concl handle TERM _ => []  
   val p = try hd ps
   val msg = "Equivariance lemma is not of the right form "
 in
@@ -170,7 +179,7 @@
     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_p (the p) prem)) 
+  else if not (concl aconv (put_perm (the p) prem)) 
     then error (msg ^ "(arguments do not agree).")
   else 
     let
@@ -181,7 +190,6 @@
       Goal.prove ctxt' [] [] goal'
         (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) 
       |> singleton (ProofContext.export ctxt' ctxt)
-      |> eqvt_transform_eq ctxt
     end
 end     
 
@@ -191,7 +199,7 @@
      (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => 
        eqvt_transform_eq ctxt thm
  | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => 
-     eqvt_transform_imp ctxt thm
+     eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt
  | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
  
 
@@ -210,7 +218,7 @@
    let
      val thm' = eqvt_transform (Context.proof_of context) thm
    in
-     context |> del_thm thm |> del_raw_thm thm'
+     context |> del_thm thm  |> del_raw_thm thm'
    end)
 
 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;