--- /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
--- 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
--- 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",
--- 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}
--- 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