diff -r 5f6fefdbf055 -r eee5deb35aa8 Nominal/Eqvt.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Eqvt.thy	Mon Feb 28 16:47:13 2011 +0000
@@ -0,0 +1,105 @@
+(*  Title:      Nominal2_Eqvt
+    Author:     Brian Huffman, 
+    Author:     Christian Urban
+
+    Test cases for perm_simp
+*)
+theory Eqvt
+imports Nominal2_Base 
+begin
+
+
+declare [[trace_eqvt = false]]
+(* declare [[trace_eqvt = true]] *)
+
+lemma 
+  fixes B::"'a::pt"
+  shows "p \<bullet> (B = C)"
+apply(perm_simp)
+oops
+
+lemma 
+  fixes B::"bool"
+  shows "p \<bullet> (B = C)"
+apply(perm_simp)
+oops
+
+lemma 
+  fixes B::"bool"
+  shows "p \<bullet> (A \<longrightarrow> B = C)"
+apply (perm_simp) 
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
+apply(perm_simp)
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo"
+apply (perm_simp)
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
+apply (perm_simp)
+oops
+
+lemma 
+  shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
+apply (perm_simp)
+oops
+
+lemma 
+  fixes p q::"perm"
+  and   x::"'a::pt"
+  shows "p \<bullet> (q \<bullet> x) = foo"
+apply(perm_simp)
+oops
+
+lemma 
+  fixes p q r::"perm"
+  and   x::"'a::pt"
+  shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
+apply(perm_simp)
+oops
+
+lemma 
+  fixes p r::"perm"
+  shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo"
+apply (perm_simp)
+oops
+
+lemma 
+  fixes C D::"bool"
+  shows "B (p \<bullet> (C = D))"
+apply(perm_simp)
+oops
+
+declare [[trace_eqvt = false]]
+
+text {* there is no raw eqvt-rule for The *}
+lemma "p \<bullet> (THE x. P x) = foo"
+apply(perm_strict_simp exclude: The)
+apply(perm_simp exclude: The)
+oops
+
+lemma 
+  fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
+  shows "p \<bullet> (P The) = foo"
+apply(perm_simp exclude: The)
+oops
+
+lemma
+  fixes  P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"
+  shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"
+apply(perm_simp)
+oops
+
+thm eqvts
+thm eqvts_raw
+
+ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
+
+
+end