# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1298911633 0
# Node ID eee5deb35aa82c9eea4ffc0406a1a249639bbcec
# Parent  5f6fefdbf05539e2735e5f59847ea2516e6e5322
included old test cases for perm_simp into ROOT.ML file

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
diff -r 5f6fefdbf055 -r eee5deb35aa8 Nominal/Nominal2_Eqvt.thy
--- a/Nominal/Nominal2_Eqvt.thy	Mon Feb 28 15:21:10 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(*  Title:      Nominal2_Eqvt
-    Author:     Brian Huffman, 
-    Author:     Christian Urban
-
-    Test cases for perm_simp
-*)
-theory Nominal2_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"} *}
-
-
-section {* automatic equivariance procedure for inductive definitions *}
-
-use "nominal_eqvt.ML"
-
-end
diff -r 5f6fefdbf055 -r eee5deb35aa8 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Mon Feb 28 15:21:10 2011 +0000
+++ b/Nominal/ROOT.ML	Mon Feb 28 16:47:13 2011 +0000
@@ -2,6 +2,7 @@
 
 no_document use_thys
    ["Atoms",
+    "Eqvt",
     "Ex/Weakening",
     "Ex/Classical",    
     "Ex/Datatypes",
diff -r 5f6fefdbf055 -r eee5deb35aa8 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Mon Feb 28 15:21:10 2011 +0000
+++ b/Pearl-jv/Paper.thy	Mon Feb 28 16:47:13 2011 +0000
@@ -3,7 +3,7 @@
 imports "../Nominal/Nominal2_Base" 
         "../Nominal/Nominal2_Eqvt"
         "../Nominal/Atoms" 
-        "../Nominal/Abs"
+        "../Nominal/Nominal2_Abs"
         "LaTeXsugar"
 begin
 
@@ -314,7 +314,7 @@
   @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
   @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
   @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
-  @{thm diff_def[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} 
+  @{thm diff_def[where M="\<pi>\<^isub>1" and N="\<pi>\<^isub>2"]} 
   \end{tabular}
   \end{isabelle}
 
diff -r 5f6fefdbf055 -r eee5deb35aa8 Pearl-jv/document/root.tex
--- a/Pearl-jv/document/root.tex	Mon Feb 28 15:21:10 2011 +0000
+++ b/Pearl-jv/document/root.tex	Mon Feb 28 16:47:13 2011 +0000
@@ -36,12 +36,13 @@
 Pitts et al introduced a beautiful theory about names and binding based on the
 notions of atoms, permutations and support. The engineering challenge is to
 smoothly adapt this theory to a theorem prover environment, in our case
-Isabelle/HOL.  We present a formalisation of this work that is based on a
-unified atom type and that represents permutations by bijective functions from
-atoms to atoms. Interestingly, we allow swappings, which are permutations
-build from two atoms, to be ill-sorted.  Furthermore we extend the nominal
-logic work with names that carry additional information and with a
-formalisation of abstractions that bind finite sets of names.
+Isabelle/HOL. For this we have to make the theory compatible with choice
+principles, which the work by Pitts is not.  We present a formalisation of
+this work that is based on a unified atom type and that represents
+permutations by bijective functions from atoms to atoms. Interestingly, we
+allow swappings, which are permutations build from two atoms, to be
+ill-sorted.  We extend the nominal logic work with a formalisation of an
+abstraction operator that binds sets of names.
 \end{abstract}
 
 % generated text of all theories