--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Eqvt.thy Wed Mar 02 12:49:01 2011 +0900
@@ -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/Ex/TypeVarsTest.thy Wed Mar 02 12:48:00 2011 +0900
+++ b/Nominal/Ex/TypeVarsTest.thy Wed Mar 02 12:49:01 2011 +0900
@@ -38,6 +38,12 @@
thm lam.fv_bn_eqvt
thm lam.size_eqvt
+(* FIXME: only works for type variables 'a 'b 'c *)
+
+nominal_datatype ('a, 'b, 'c) psi =
+ PsiNil
+| Output "'a" "'a" "('a, 'b, 'c) psi"
+
end
--- a/Nominal/Nominal2.thy Wed Mar 02 12:48:00 2011 +0900
+++ b/Nominal/Nominal2.thy Wed Mar 02 12:49:01 2011 +0900
@@ -1,6 +1,6 @@
theory Nominal2
imports
- Nominal2_Base Nominal2_Eqvt Nominal2_Abs
+ Nominal2_Base Nominal2_Abs
uses ("nominal_dt_rawfuns.ML")
("nominal_dt_alpha.ML")
("nominal_dt_quot.ML")
--- a/Nominal/Nominal2_Abs.thy Wed Mar 02 12:48:00 2011 +0900
+++ b/Nominal/Nominal2_Abs.thy Wed Mar 02 12:49:01 2011 +0900
@@ -1,6 +1,5 @@
theory Nominal2_Abs
imports "Nominal2_Base"
- "Nominal2_Eqvt"
"~~/src/HOL/Quotient"
"~~/src/HOL/Library/Quotient_List"
"~~/src/HOL/Library/Quotient_Product"
@@ -768,6 +767,15 @@
unfolding fresh_star_def
by(auto simp add: Abs_fresh_iff)
+lemma Abs_fresh_star2:
+ fixes x::"'a::fs"
+ shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_set bs x \<longleftrightarrow> as \<sharp>* x"
+ and "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_res bs x \<longleftrightarrow> as \<sharp>* x"
+ and "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* Abs_lst ds x \<longleftrightarrow> cs \<sharp>* x"
+ unfolding fresh_star_def Abs_fresh_iff
+ by auto
+
+
lemma Abs1_eq:
fixes x::"'a::fs"
shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"
--- a/Nominal/Nominal2_Base.thy Wed Mar 02 12:48:00 2011 +0900
+++ b/Nominal/Nominal2_Base.thy Wed Mar 02 12:49:01 2011 +0900
@@ -8,8 +8,12 @@
imports Main
"~~/src/HOL/Library/Infinite_Set"
"~~/src/HOL/Quotient_Examples/FSet"
-uses ("nominal_library.ML")
+uses ("nominal_basics.ML")
+ ("nominal_thmdecls.ML")
+ ("nominal_permeq.ML")
+ ("nominal_library.ML")
("nominal_atoms.ML")
+ ("nominal_eqvt.ML")
begin
section {* Atoms and Sorts *}
@@ -76,6 +80,7 @@
shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
by (induct a, induct b, simp)
+
section {* Sort-Respecting Permutations *}
typedef perm =
@@ -146,7 +151,8 @@
instance perm :: size ..
-subsection {* Permutations form a group *}
+
+subsection {* Permutations form a (multiplicative) group *}
instantiation perm :: group_add
begin
@@ -343,7 +349,7 @@
"c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> c = c"
unfolding swap_atom by simp_all
-lemma expand_perm_eq:
+lemma perm_eq_iff:
fixes p q :: "perm"
shows "p = q \<longleftrightarrow> (\<forall>a::atom. p \<bullet> a = q \<bullet> a)"
unfolding permute_atom_def
@@ -371,30 +377,11 @@
unfolding permute_perm_def
by (simp add: diff_minus add_assoc)
-lemma permute_eqvt:
- shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"
- unfolding permute_perm_def by simp
-
-lemma zero_perm_eqvt:
- shows "p \<bullet> (0::perm) = 0"
- unfolding permute_perm_def by simp
-
-lemma add_perm_eqvt:
- fixes p p1 p2 :: perm
- shows "p \<bullet> (p1 + p2) = p \<bullet> p1 + p \<bullet> p2"
- unfolding permute_perm_def
- by (simp add: expand_perm_eq)
-
-lemma swap_eqvt:
- shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)"
- unfolding permute_perm_def
- by (auto simp add: swap_atom expand_perm_eq)
-
-lemma uminus_eqvt:
- fixes p q::"perm"
- shows "p \<bullet> (- q) = - (p \<bullet> q)"
- unfolding permute_perm_def
- by (simp add: diff_minus minus_add add_assoc)
+lemma pemute_minus_self:
+ shows "- p \<bullet> p = p"
+ unfolding permute_perm_def
+ by (simp add: diff_minus add_assoc)
+
subsection {* Permutations for functions *}
@@ -431,38 +418,6 @@
end
-lemma Not_eqvt:
- shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
-by (simp add: permute_bool_def)
-
-lemma conj_eqvt:
- shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma imp_eqvt:
- shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma ex_eqvt:
- shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
- unfolding permute_fun_def permute_bool_def
- by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
-lemma all_eqvt:
- shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
- unfolding permute_fun_def permute_bool_def
- by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
-lemma ex1_eqvt:
- shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
- unfolding Ex1_def
- apply(simp add: ex_eqvt)
- unfolding permute_fun_def
- apply(simp add: conj_eqvt all_eqvt)
- unfolding permute_fun_def
- apply(simp add: imp_eqvt permute_bool_def)
- done
-
lemma permute_boolE:
fixes P::"bool"
shows "p \<bullet> P \<Longrightarrow> P"
@@ -477,7 +432,6 @@
lemma permute_set_eq:
fixes x::"'a::pt"
- and p::"perm"
shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"
unfolding permute_fun_def
unfolding permute_bool_def
@@ -497,15 +451,8 @@
lemma permute_finite [simp]:
shows "finite (p \<bullet> X) = finite X"
-apply(simp add: permute_set_eq_image)
-apply(rule iffI)
-apply(drule finite_imageD)
-using inj_permute[where p="p"]
-apply(simp add: inj_on_def)
-apply(assumption)
-apply(rule finite_imageI)
-apply(assumption)
-done
+ unfolding permute_set_eq_vimage
+ using bij_permute by (rule finite_vimage_iff)
lemma swap_set_not_in:
assumes a: "a \<notin> S" "b \<notin> S"
@@ -536,11 +483,6 @@
unfolding mem_def permute_fun_def permute_bool_def
by simp
-lemma mem_eqvt:
- shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
- unfolding mem_def
- by (simp add: permute_fun_app_eq)
-
lemma empty_eqvt:
shows "p \<bullet> {} = {}"
unfolding empty_def Collect_def
@@ -550,23 +492,8 @@
shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
unfolding permute_set_eq_image image_insert ..
-lemma Collect_eqvt:
- shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
- unfolding Collect_def permute_fun_def ..
-
-lemma inter_eqvt:
- shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
- unfolding Int_def
- apply(simp add: Collect_eqvt)
- apply(simp add: permute_fun_def)
- apply(simp add: conj_eqvt)
- apply(simp add: mem_eqvt)
- apply(simp add: permute_fun_def)
- done
-
-
-
-subsection {* Permutations for units *}
+
+subsection {* Permutations for @{typ unit} *}
instantiation unit :: pt
begin
@@ -610,7 +537,7 @@
end
-subsection {* Permutations for lists *}
+subsection {* Permutations for @{typ "'a list"} *}
instantiation list :: (pt) pt
begin
@@ -630,7 +557,9 @@
shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
-subsection {* Permutations for options *}
+
+
+subsection {* Permutations for @{typ "'a option"} *}
instantiation option :: (pt) pt
begin
@@ -647,7 +576,7 @@
end
-subsection {* Permutations for fsets *}
+subsection {* Permutations for @{typ "'a fset"} *}
lemma permute_fset_rsp[quot_respect]:
shows "(op = ===> list_eq ===> list_eq) permute permute"
@@ -677,6 +606,9 @@
and "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
by (lifting permute_list.simps)
+lemma fset_eqvt:
+ shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
+ by (lifting set_eqvt)
subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
@@ -757,7 +689,350 @@
instance int :: pure
proof qed (rule permute_int_def)
-subsection {* Supp, Freshness and Supports *}
+
+section {* Infrastructure for Equivariance and Perm_simp *}
+
+subsection {* Basic functions about permutations *}
+
+use "nominal_basics.ML"
+
+
+subsection {* Eqvt infrastructure *}
+
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+
+use "nominal_thmdecls.ML"
+setup "Nominal_ThmDecls.setup"
+
+
+lemmas [eqvt] =
+ (* pt types *)
+ permute_prod.simps
+ permute_list.simps
+ permute_option.simps
+ permute_sum.simps
+
+ (* sets *)
+ empty_eqvt insert_eqvt set_eqvt
+
+ (* fsets *)
+ permute_fset fset_eqvt
+
+
+
+subsection {* perm_simp infrastructure *}
+
+definition
+ "unpermute p = permute (- p)"
+
+lemma eqvt_apply:
+ fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ and x :: "'a::pt"
+ shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
+ unfolding permute_fun_def by simp
+
+lemma eqvt_lambda:
+ fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+ unfolding permute_fun_def unpermute_def by simp
+
+lemma eqvt_bound:
+ shows "p \<bullet> unpermute p x \<equiv> x"
+ unfolding unpermute_def by simp
+
+text {* provides perm_simp methods *}
+
+use "nominal_permeq.ML"
+setup Nominal_Permeq.setup
+
+method_setup perm_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ {* pushes permutations inside. *}
+
+method_setup perm_strict_simp =
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
+
+
+subsubsection {* Equivariance for permutations and swapping *}
+
+lemma permute_eqvt:
+ shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"
+ unfolding permute_perm_def by simp
+
+(* the normal version of this lemma would cause loops *)
+lemma permute_eqvt_raw[eqvt_raw]:
+ shows "p \<bullet> permute \<equiv> permute"
+apply(simp add: fun_eq_iff permute_fun_def)
+apply(subst permute_eqvt)
+apply(simp)
+done
+
+lemma zero_perm_eqvt [eqvt]:
+ shows "p \<bullet> (0::perm) = 0"
+ unfolding permute_perm_def by simp
+
+lemma add_perm_eqvt [eqvt]:
+ fixes p p1 p2 :: perm
+ shows "p \<bullet> (p1 + p2) = p \<bullet> p1 + p \<bullet> p2"
+ unfolding permute_perm_def
+ by (simp add: perm_eq_iff)
+
+lemma swap_eqvt [eqvt]:
+ shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)"
+ unfolding permute_perm_def
+ by (auto simp add: swap_atom perm_eq_iff)
+
+lemma uminus_eqvt [eqvt]:
+ fixes p q::"perm"
+ shows "p \<bullet> (- q) = - (p \<bullet> q)"
+ unfolding permute_perm_def
+ by (simp add: diff_minus minus_add add_assoc)
+
+
+subsubsection {* Equivariance of Logical Operators *}
+
+lemma eq_eqvt [eqvt]:
+ shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
+ unfolding permute_eq_iff permute_bool_def ..
+
+lemma Not_eqvt [eqvt]:
+ shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)"
+ by (simp add: permute_bool_def)
+
+lemma conj_eqvt [eqvt]:
+ shows "p \<bullet> (A \<and> B) \<longleftrightarrow> (p \<bullet> A) \<and> (p \<bullet> B)"
+ by (simp add: permute_bool_def)
+
+lemma imp_eqvt [eqvt]:
+ shows "p \<bullet> (A \<longrightarrow> B) \<longleftrightarrow> (p \<bullet> A) \<longrightarrow> (p \<bullet> B)"
+ by (simp add: permute_bool_def)
+
+declare imp_eqvt[folded induct_implies_def, eqvt]
+
+lemma ex_eqvt [eqvt]:
+ shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+
+lemma all_eqvt [eqvt]:
+ shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+
+declare all_eqvt[folded induct_forall_def, eqvt]
+
+lemma ex1_eqvt [eqvt]:
+ shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+ unfolding Ex1_def
+ by (perm_simp) (rule refl)
+
+lemma mem_eqvt [eqvt]:
+ shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+ unfolding mem_def
+ by (simp add: permute_fun_app_eq)
+
+lemma Collect_eqvt [eqvt]:
+ shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+ unfolding Collect_def permute_fun_def ..
+
+lemma inter_eqvt [eqvt]:
+ shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ unfolding Int_def
+ by (perm_simp) (rule refl)
+
+lemma image_eqvt [eqvt]:
+ shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+ unfolding permute_set_eq_image
+ unfolding permute_fun_def [where f=f]
+ by (simp add: image_image)
+
+lemma if_eqvt [eqvt]:
+ shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
+ by (simp add: permute_fun_def permute_bool_def)
+
+lemma True_eqvt [eqvt]:
+ shows "p \<bullet> True = True"
+ unfolding permute_bool_def ..
+
+lemma False_eqvt [eqvt]:
+ shows "p \<bullet> False = False"
+ unfolding permute_bool_def ..
+
+lemma disj_eqvt [eqvt]:
+ shows "p \<bullet> (A \<or> B) \<longleftrightarrow> (p \<bullet> A) \<or> (p \<bullet> B)"
+ by (simp add: permute_bool_def)
+
+lemma all_eqvt2:
+ shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma ex_eqvt2:
+ shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma ex1_eqvt2:
+ shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
+ by (perm_simp add: permute_minus_cancel) (rule refl)
+
+lemma the_eqvt:
+ assumes unique: "\<exists>!x. P x"
+ shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
+ apply(rule the1_equality [symmetric])
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_simp add: permute_minus_cancel)
+ apply(rule unique)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_simp add: permute_minus_cancel)
+ apply(rule theI'[OF unique])
+ done
+
+lemma the_eqvt2:
+ assumes unique: "\<exists>!x. P x"
+ shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
+ apply(rule the1_equality [symmetric])
+ apply(simp add: ex1_eqvt2[symmetric])
+ apply(simp add: permute_bool_def unique)
+ apply(simp add: permute_bool_def)
+ apply(rule theI'[OF unique])
+ done
+
+subsubsection {* Equivariance set operations *}
+
+lemma Bex_eqvt [eqvt]:
+ shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ unfolding Bex_def
+ by (perm_simp) (rule refl)
+
+lemma Ball_eqvt [eqvt]:
+ shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ unfolding Ball_def
+ by (perm_simp) (rule refl)
+
+lemma UNIV_eqvt [eqvt]:
+ shows "p \<bullet> UNIV = UNIV"
+ unfolding UNIV_def
+ by (perm_simp) (rule refl)
+
+lemma union_eqvt [eqvt]:
+ shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+ unfolding Un_def
+ by (perm_simp) (rule refl)
+
+lemma Diff_eqvt [eqvt]:
+ fixes A B :: "'a::pt set"
+ shows "p \<bullet> (A - B) = (p \<bullet> A) - (p \<bullet> B)"
+ unfolding set_diff_eq
+ by (perm_simp) (rule refl)
+
+lemma Compl_eqvt [eqvt]:
+ fixes A :: "'a::pt set"
+ shows "p \<bullet> (- A) = - (p \<bullet> A)"
+ unfolding Compl_eq_Diff_UNIV
+ by (perm_simp) (rule refl)
+
+lemma subset_eqvt [eqvt]:
+ shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
+ unfolding subset_eq
+ by (perm_simp) (rule refl)
+
+lemma psubset_eqvt [eqvt]:
+ shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
+ unfolding psubset_eq
+ by (perm_simp) (rule refl)
+
+lemma vimage_eqvt [eqvt]:
+ shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+ unfolding vimage_def
+ by (perm_simp) (rule refl)
+
+lemma Union_eqvt [eqvt]:
+ shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+ unfolding Union_eq
+ by (perm_simp) (rule refl)
+
+(* FIXME: eqvt attribute *)
+lemma Sigma_eqvt:
+ shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
+unfolding Sigma_def
+unfolding UNION_eq_Union_image
+by (perm_simp) (rule refl)
+
+lemma finite_eqvt [eqvt]:
+ shows "p \<bullet> finite A = finite (p \<bullet> A)"
+ unfolding permute_finite permute_bool_def ..
+
+subsubsection {* Equivariance for product operations *}
+
+lemma fst_eqvt [eqvt]:
+ "p \<bullet> (fst x) = fst (p \<bullet> x)"
+ by (cases x) simp
+
+lemma snd_eqvt [eqvt]:
+ "p \<bullet> (snd x) = snd (p \<bullet> x)"
+ by (cases x) simp
+
+lemma split_eqvt [eqvt]:
+ shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+ unfolding split_def
+ by (perm_simp) (rule refl)
+
+
+subsubsection {* Equivariance for list operations *}
+
+lemma append_eqvt [eqvt]:
+ shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+ by (induct xs) auto
+
+lemma rev_eqvt [eqvt]:
+ shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+ by (induct xs) (simp_all add: append_eqvt)
+
+lemma map_eqvt [eqvt]:
+ shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+ by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+
+lemma removeAll_eqvt [eqvt]:
+ shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+ by (induct xs) (auto)
+
+lemma filter_eqvt [eqvt]:
+ shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
+apply(induct xs)
+apply(simp)
+apply(simp only: filter.simps permute_list.simps if_eqvt)
+apply(simp only: permute_fun_app_eq)
+done
+
+lemma distinct_eqvt [eqvt]:
+ shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
+apply(induct xs)
+apply(simp add: permute_bool_def)
+apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
+done
+
+lemma length_eqvt [eqvt]:
+ shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
+by (induct xs) (simp_all add: permute_pure)
+
+
+subsubsection {* Equivariance for @{typ "'a fset"} *}
+
+lemma in_fset_eqvt [eqvt]:
+ shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
+unfolding in_fset
+by (perm_simp) (simp)
+
+lemma union_fset_eqvt [eqvt]:
+ shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
+by (induct S) (simp_all)
+
+lemma map_fset_eqvt [eqvt]:
+ shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+ by (lifting map_eqvt)
+
+
+section {* Supp, Freshness and Supports *}
context pt
begin
@@ -767,13 +1042,13 @@
where
"supp x = {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}}"
-end
-
definition
- fresh :: "atom \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp> _" [55, 55] 55)
+ fresh :: "atom \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [55, 55] 55)
where
"a \<sharp> x \<equiv> a \<notin> supp x"
+end
+
lemma supp_conv_fresh:
shows "supp x = {a. \<not> a \<sharp> x}"
unfolding fresh_def by simp
@@ -838,12 +1113,12 @@
finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" .
qed
-lemma fresh_eqvt:
+lemma fresh_eqvt [eqvt]:
shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)"
unfolding permute_bool_def
by (simp add: fresh_permute_iff)
-lemma supp_eqvt:
+lemma supp_eqvt [eqvt]:
shows "p \<bullet> (supp x) = supp (p \<bullet> x)"
unfolding supp_conv_fresh
unfolding Collect_def
@@ -863,7 +1138,7 @@
qed
-subsection {* supports *}
+section {* supports *}
definition
supports :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" (infixl "supports" 80)
@@ -881,7 +1156,7 @@
then obtain a where b1: "a \<in> supp x" and b2: "a \<notin> S" by auto
from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" unfolding supports_def by auto
then have "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" by auto
- with a2 have "finite {b. (a \<rightleftharpoons> b)\<bullet>x \<noteq> x}" by (simp add: finite_subset)
+ with a2 have "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" by (simp add: finite_subset)
then have "a \<notin> (supp x)" unfolding supp_def by simp
with b1 show False by simp
qed
@@ -972,7 +1247,8 @@
assumes finite_supp: "finite (supp x)"
lemma pure_supp:
- shows "supp (x::'a::pure) = {}"
+ fixes x::"'a::pure"
+ shows "supp x = {}"
unfolding supp_def by (simp add: permute_pure)
lemma pure_fresh:
@@ -1026,7 +1302,7 @@
apply (rule supports_perm)
apply (rule finite_perm_lemma)
apply (simp add: perm_swap_eq swap_eqvt)
-apply (auto simp add: expand_perm_eq swap_atom)
+apply (auto simp add: perm_eq_iff swap_atom)
done
lemma fresh_perm:
@@ -1074,14 +1350,11 @@
unfolding supp_conv_fresh
by (simp add: fresh_minus_perm)
-instance perm :: fs
-by default (simp add: supp_perm finite_perm_lemma)
-
lemma plus_perm_eq:
fixes p q::"perm"
assumes asm: "supp p \<inter> supp q = {}"
shows "p + q = q + p"
-unfolding expand_perm_eq
+unfolding perm_eq_iff
proof
fix a::"atom"
show "(p + q) \<bullet> a = (q + p) \<bullet> a"
@@ -1135,6 +1408,10 @@
by blast
qed
+instance perm :: fs
+by default (simp add: supp_perm finite_perm_lemma)
+
+
section {* Finite Support instances for other types *}
@@ -1240,6 +1517,25 @@
shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+lemma supp_rev:
+ shows "supp (rev xs) = supp xs"
+ by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+
+lemma fresh_rev:
+ shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
+ by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+
+lemma supp_removeAll:
+ fixes x::"atom"
+ shows "supp (removeAll x xs) = supp xs - {x}"
+ by (induct xs)
+ (auto simp add: supp_Nil supp_Cons supp_atom)
+
+lemma supp_of_atom_list:
+ fixes as::"atom list"
+ shows "supp as = set as"
+by (induct as)
+ (simp_all add: supp_Nil supp_Cons supp_atom)
instance list :: (fs) fs
apply default
@@ -1247,12 +1543,6 @@
apply (simp_all add: supp_Nil supp_Cons finite_supp)
done
-lemma supp_of_atom_list:
- fixes as::"atom list"
- shows "supp as = set as"
-by (induct as)
- (simp_all add: supp_Nil supp_Cons supp_atom)
-
section {* Support and Freshness for Applications *}
@@ -1261,19 +1551,12 @@
unfolding fresh_def supp_def
unfolding MOST_iff_cofinite by simp
-lemma supp_subset_fresh:
- assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y"
- shows "supp y \<subseteq> supp x"
- using a
- unfolding fresh_def
- by blast
-
lemma fresh_fun_app:
assumes "a \<sharp> f" and "a \<sharp> x"
shows "a \<sharp> f x"
using assms
unfolding fresh_conv_MOST
- unfolding permute_fun_app_eq
+ unfolding permute_fun_app_eq
by (elim MOST_rev_mp, simp)
lemma supp_fun_app:
@@ -1282,11 +1565,19 @@
unfolding fresh_def
by auto
-text {* Equivariant Functions *}
+
+subsection {* Equivariance Predicate @{text eqvt} and @{text eqvt_at}*}
definition
"eqvt f \<equiv> \<forall>p. p \<bullet> f = f"
+
+text {* equivariance of a function at a given argument *}
+
+definition
+ "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
+
+
lemma eqvtI:
shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"
unfolding eqvt_def
@@ -1310,9 +1601,12 @@
using supp_fun_app by auto
qed
-text {* equivariance of a function at a given argument *}
-definition
- "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"
+lemma supp_fun_app_eqvt:
+ assumes a: "eqvt f"
+ shows "supp (f x) \<subseteq> supp x"
+ using fresh_fun_eqvt_app[OF a]
+ unfolding fresh_def
+ by auto
lemma supp_eqvt_at:
assumes asm: "eqvt_at f x"
@@ -1346,7 +1640,8 @@
using supp_eqvt_at[OF asm fin]
by auto
-text {* helper functions for nominal_functions *}
+
+subsection {* helper functions for nominal_functions *}
lemma the_default_eqvt:
assumes unique: "\<exists>!x. P x"
@@ -1409,6 +1704,7 @@
using assms
by (auto intro: fundef_ex1_eqvt)
+
section {* Support of Finite Sets of Finitely Supported Elements *}
text {* support and freshness for atom sets *}
@@ -1438,27 +1734,6 @@
unfolding fresh_def
by (auto simp add: supp_finite_atom_set assms)
-
-lemma Union_fresh:
- shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
- unfolding Union_image_eq[symmetric]
- apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
- unfolding eqvt_def
- unfolding permute_fun_def
- apply(simp)
- unfolding UNION_def
- unfolding Collect_def
- unfolding Bex_def
- apply(simp add: ex_eqvt)
- unfolding permute_fun_def
- apply(simp add: conj_eqvt)
- apply(simp add: mem_eqvt)
- apply(simp add: supp_eqvt)
- unfolding permute_fun_def
- apply(simp)
- apply(assumption)
- done
-
lemma Union_supports_set:
shows "(\<Union>x \<in> S. supp x) supports S"
proof -
@@ -1482,12 +1757,14 @@
assumes fin: "finite S"
shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
proof -
+ have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)"
+ unfolding eqvt_def
+ by (perm_simp) (simp)
have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
- by (rule supp_finite_atom_set[symmetric])
- (rule Union_of_finite_supp_sets[OF fin])
- also have "\<dots> \<subseteq> supp S"
- by (rule supp_subset_fresh)
- (simp add: Union_fresh)
+ by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin])
+ also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp
+ also have "\<dots> \<subseteq> supp S" using eqvt
+ by (rule supp_fun_app_eqvt)
finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
qed
@@ -1557,10 +1834,6 @@
subsection {* Type @{typ "'a fset"} is finitely supported *}
-lemma fset_eqvt:
- shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
- by (lifting set_eqvt)
-
lemma supp_fset [simp]:
shows "supp (fset S) = supp S"
unfolding supp_def
@@ -1596,6 +1869,16 @@
shows "finite (supp S)"
by (induct S) (simp_all add: finite_supp)
+lemma supp_union_fset:
+ fixes S T::"'a::fs fset"
+ shows "supp (S |\<union>| T) = supp S \<union> supp T"
+by (induct S) (auto)
+
+lemma fresh_union_fset:
+ fixes S T::"'a::fs fset"
+ shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
+unfolding fresh_def
+by (simp add: supp_union_fset)
instance fset :: (fs) fs
apply (default)
@@ -1654,7 +1937,6 @@
done
lemma fresh_star_atom_set_conv:
- fixes p::"perm"
assumes fresh: "as \<sharp>* bs"
and fin: "finite as" "finite bs"
shows "bs \<sharp>* as"
@@ -1662,6 +1944,13 @@
unfolding fresh_star_def fresh_def
by (auto simp add: supp_finite_atom_set fin)
+lemma atom_fresh_star_disjoint:
+ assumes fin: "finite bs"
+ shows "as \<sharp>* bs \<longleftrightarrow> (as \<inter> bs = {})"
+
+unfolding fresh_star_def fresh_def
+by (auto simp add: supp_finite_atom_set fin)
+
lemma fresh_star_Pair:
shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)"
@@ -1738,23 +2027,11 @@
unfolding fresh_star_def
by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
-lemma fresh_star_eqvt:
+lemma fresh_star_eqvt [eqvt]:
shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)"
unfolding fresh_star_def
-unfolding Ball_def
-apply(simp add: all_eqvt)
-apply(subst permute_fun_def)
-apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
-done
-
-lemma at_fresh_star_inter:
- assumes a: "(p \<bullet> bs) \<sharp>* bs"
- and b: "finite bs"
- shows "p \<bullet> bs \<inter> bs = {}"
-using a b
-unfolding fresh_star_def
-unfolding fresh_def
-by (auto simp add: supp_finite_atom_set)
+by (perm_simp) (rule refl)
+
section {* Induction principle for permutations *}
@@ -1773,7 +2050,7 @@
then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
have as: "supp p \<subseteq> S" by fact
{ assume "supp p = {}"
- then have "p = 0" by (simp add: supp_perm expand_perm_eq)
+ then have "p = 0" by (simp add: supp_perm perm_eq_iff)
then have "P p" using zero by simp
}
moreover
@@ -1792,7 +2069,7 @@
have "supp ?q \<subseteq> S" using as a2 by simp
ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp
moreover
- have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
+ have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: perm_eq_iff)
ultimately have "P p" by simp
}
ultimately show "P p" by blast
@@ -2186,6 +2463,8 @@
assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
+declare atom_eqvt[eqvt]
+
class at = at_base +
assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
@@ -2295,6 +2574,7 @@
where
"(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
+
lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
unfolding flip_def by (rule swap_self)
@@ -2313,7 +2593,7 @@
lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
by (simp add: flip_commute)
-lemma flip_eqvt:
+lemma flip_eqvt [eqvt]:
fixes a b c::"'a::at_base"
shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
unfolding flip_def
@@ -2633,5 +2913,10 @@
use "nominal_atoms.ML"
+section {* automatic equivariance procedure for inductive definitions *}
+
+use "nominal_eqvt.ML"
+
+
end
--- a/Nominal/Nominal2_Eqvt.thy Wed Mar 02 12:48:00 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,426 +0,0 @@
-(* Title: Nominal2_Eqvt
- Author: Brian Huffman,
- Author: Christian Urban
-
- Equivariance, supp and freshness lemmas for various operators
- (contains many, but not all such lemmas).
-*)
-theory Nominal2_Eqvt
-imports Nominal2_Base
-uses ("nominal_thmdecls.ML")
- ("nominal_permeq.ML")
- ("nominal_eqvt.ML")
-begin
-
-
-section {* Permsimp and Eqvt infrastructure *}
-
-text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
-
-use "nominal_thmdecls.ML"
-setup "Nominal_ThmDecls.setup"
-
-
-section {* eqvt lemmas *}
-
-lemmas [eqvt] =
- conj_eqvt Not_eqvt ex_eqvt all_eqvt ex1_eqvt imp_eqvt uminus_eqvt
- imp_eqvt[folded induct_implies_def]
- all_eqvt[folded induct_forall_def]
-
- (* nominal *)
- supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt
- swap_eqvt flip_eqvt
-
- (* datatypes *)
- Pair_eqvt permute_list.simps permute_option.simps
- permute_sum.simps
-
- (* sets *)
- mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt
-
- (* fsets *)
- permute_fset fset_eqvt
-
-
-text {* helper lemmas for the perm_simp *}
-
-definition
- "unpermute p = permute (- p)"
-
-lemma eqvt_apply:
- fixes f :: "'a::pt \<Rightarrow> 'b::pt"
- and x :: "'a::pt"
- shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
- unfolding permute_fun_def by simp
-
-lemma eqvt_lambda:
- fixes f :: "'a::pt \<Rightarrow> 'b::pt"
- shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
- unfolding permute_fun_def unpermute_def by simp
-
-lemma eqvt_bound:
- shows "p \<bullet> unpermute p x \<equiv> x"
- unfolding unpermute_def by simp
-
-text {* provides perm_simp methods *}
-
-use "nominal_permeq.ML"
-setup Nominal_Permeq.setup
-
-method_setup perm_simp =
- {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
- {* pushes permutations inside. *}
-
-method_setup perm_strict_simp =
- {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
- {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
-
-(* the normal version of this lemma would cause loops *)
-lemma permute_eqvt_raw[eqvt_raw]:
- shows "p \<bullet> permute \<equiv> permute"
-apply(simp add: fun_eq_iff permute_fun_def)
-apply(subst permute_eqvt)
-apply(simp)
-done
-
-subsection {* Equivariance of Logical Operators *}
-
-lemma eq_eqvt[eqvt]:
- shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
- unfolding permute_eq_iff permute_bool_def ..
-
-lemma if_eqvt[eqvt]:
- shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
- by (simp add: permute_fun_def permute_bool_def)
-
-lemma True_eqvt[eqvt]:
- shows "p \<bullet> True = True"
- unfolding permute_bool_def ..
-
-lemma False_eqvt[eqvt]:
- shows "p \<bullet> False = False"
- unfolding permute_bool_def ..
-
-lemma disj_eqvt[eqvt]:
- shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma all_eqvt2:
- shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
- by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma ex_eqvt2:
- shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
- by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma ex1_eqvt2:
- shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
- by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma the_eqvt:
- assumes unique: "\<exists>!x. P x"
- shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
- apply(rule the1_equality [symmetric])
- apply(rule_tac p="-p" in permute_boolE)
- apply(perm_simp add: permute_minus_cancel)
- apply(rule unique)
- apply(rule_tac p="-p" in permute_boolE)
- apply(perm_simp add: permute_minus_cancel)
- apply(rule theI'[OF unique])
- done
-
-lemma the_eqvt2:
- assumes unique: "\<exists>!x. P x"
- shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
- apply(rule the1_equality [symmetric])
- apply(simp add: ex1_eqvt2[symmetric])
- apply(simp add: permute_bool_def unique)
- apply(simp add: permute_bool_def)
- apply(rule theI'[OF unique])
- done
-
-subsection {* Equivariance Set Operations *}
-
-lemma not_mem_eqvt:
- shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
- by (perm_simp) (rule refl)
-
-lemma Collect_eqvt[eqvt]:
- shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
- unfolding Collect_def permute_fun_def ..
-
-lemma Collect_eqvt2:
- shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
- by (perm_simp add: permute_minus_cancel) (rule refl)
-
-lemma Bex_eqvt[eqvt]:
- shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
- unfolding Bex_def
- by (perm_simp) (rule refl)
-
-lemma Ball_eqvt[eqvt]:
- shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
- unfolding Ball_def
- by (perm_simp) (rule refl)
-
-lemma UNIV_eqvt[eqvt]:
- shows "p \<bullet> UNIV = UNIV"
- unfolding UNIV_def
- by (perm_simp) (rule refl)
-
-lemma union_eqvt[eqvt]:
- shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
- unfolding Un_def
- by (perm_simp) (rule refl)
-
-lemma Diff_eqvt[eqvt]:
- fixes A B :: "'a::pt set"
- shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
- unfolding set_diff_eq
- by (perm_simp) (rule refl)
-
-lemma Compl_eqvt[eqvt]:
- fixes A :: "'a::pt set"
- shows "p \<bullet> (- A) = - (p \<bullet> A)"
- unfolding Compl_eq_Diff_UNIV
- by (perm_simp) (rule refl)
-
-lemma subset_eqvt[eqvt]:
- shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)"
- unfolding subset_eq
- by (perm_simp) (rule refl)
-
-lemma psubset_eqvt[eqvt]:
- shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)"
- unfolding psubset_eq
- by (perm_simp) (rule refl)
-
-lemma image_eqvt[eqvt]:
- shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
- unfolding permute_set_eq_image
- unfolding permute_fun_def [where f=f]
- by (simp add: image_image)
-
-lemma vimage_eqvt[eqvt]:
- shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
- unfolding vimage_def
- by (perm_simp) (rule refl)
-
-lemma Union_eqvt[eqvt]:
- shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
- unfolding Union_eq
- by (perm_simp) (rule refl)
-
-lemma Sigma_eqvt:
- shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
-unfolding Sigma_def
-unfolding UNION_eq_Union_image
-by (perm_simp) (rule refl)
-
-lemma finite_permute_iff:
- shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
- unfolding permute_set_eq_vimage
- using bij_permute by (rule finite_vimage_iff)
-
-lemma finite_eqvt[eqvt]:
- shows "p \<bullet> finite A = finite (p \<bullet> A)"
- unfolding finite_permute_iff permute_bool_def ..
-
-
-section {* List Operations *}
-
-lemma append_eqvt[eqvt]:
- shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
- by (induct xs) auto
-
-lemma rev_eqvt[eqvt]:
- shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
- by (induct xs) (simp_all add: append_eqvt)
-
-lemma supp_rev:
- shows "supp (rev xs) = supp xs"
- by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
-
-lemma fresh_rev:
- shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
- by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
-
-lemma map_eqvt[eqvt]:
- shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
- by (induct xs) (simp_all, simp only: permute_fun_app_eq)
-
-lemma removeAll_eqvt[eqvt]:
- shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
- by (induct xs) (auto)
-
-lemma supp_removeAll:
- fixes x::"atom"
- shows "supp (removeAll x xs) = supp xs - {x}"
- by (induct xs)
- (auto simp add: supp_Nil supp_Cons supp_atom)
-
-lemma filter_eqvt[eqvt]:
- shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
-apply(induct xs)
-apply(simp)
-apply(simp only: filter.simps permute_list.simps if_eqvt)
-apply(simp only: permute_fun_app_eq)
-done
-
-lemma distinct_eqvt[eqvt]:
- shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
-apply(induct xs)
-apply(simp add: permute_bool_def)
-apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
-done
-
-lemma length_eqvt[eqvt]:
- shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
-by (induct xs) (simp_all add: permute_pure)
-
-
-subsection {* Equivariance Finite-Set Operations *}
-
-lemma in_fset_eqvt[eqvt]:
- shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
-unfolding in_fset
-by (perm_simp) (simp)
-
-lemma union_fset_eqvt[eqvt]:
- shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
-by (induct S) (simp_all)
-
-lemma supp_union_fset:
- fixes S T::"'a::fs fset"
- shows "supp (S |\<union>| T) = supp S \<union> supp T"
-by (induct S) (auto)
-
-lemma fresh_union_fset:
- fixes S T::"'a::fs fset"
- shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
-unfolding fresh_def
-by (simp add: supp_union_fset)
-
-lemma map_fset_eqvt[eqvt]:
- shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
- by (lifting map_eqvt)
-
-
-subsection {* Product Operations *}
-
-lemma fst_eqvt[eqvt]:
- "p \<bullet> (fst x) = fst (p \<bullet> x)"
- by (cases x) simp
-
-lemma snd_eqvt[eqvt]:
- "p \<bullet> (snd x) = snd (p \<bullet> x)"
- by (cases x) simp
-
-lemma split_eqvt[eqvt]:
- shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
- unfolding split_def
- by (perm_simp) (rule refl)
-
-
-section {* Test cases *}
-
-
-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 Wed Mar 02 12:48:00 2011 +0900
+++ b/Nominal/ROOT.ML Wed Mar 02 12:49:01 2011 +0900
@@ -2,6 +2,7 @@
no_document use_thys
["Atoms",
+ "Eqvt",
"Ex/Weakening",
"Ex/Classical",
"Ex/Datatypes",
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_basics.ML Wed Mar 02 12:49:01 2011 +0900
@@ -0,0 +1,152 @@
+(* Title: nominal_basic.ML
+ Author: Christian Urban
+
+ Basic functions for nominal.
+*)
+
+signature NOMINAL_BASIC =
+sig
+ val trace: bool Unsynchronized.ref
+ val trace_msg: (unit -> string) -> unit
+
+ val last2: 'a list -> 'a * 'a
+ val split_last2: 'a list -> 'a list * 'a * 'a
+ val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
+ val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list
+ val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
+ val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
+ val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
+ val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a
+
+ val is_true: term -> bool
+
+ val dest_listT: typ -> typ
+ val dest_fsetT: typ -> typ
+
+ val mk_id: term -> term
+ val mk_all: (string * typ) -> term -> term
+ val mk_All: (string * typ) -> term -> term
+ val mk_exists: (string * typ) -> term -> term
+
+ val sum_case_const: typ -> typ -> typ -> term
+ val mk_sum_case: term -> term -> term
+
+ val mk_equiv: thm -> thm
+ val safe_mk_equiv: thm -> thm
+
+ val mk_minus: term -> term
+ val mk_plus: term -> term -> term
+
+ val perm_ty: typ -> typ
+ val perm_const: typ -> term
+ val mk_perm_ty: typ -> term -> term -> term
+ val mk_perm: term -> term -> term
+ val dest_perm: term -> term * term
+
+end
+
+
+structure Nominal_Basic: NOMINAL_BASIC =
+struct
+
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if ! trace then tracing (msg ()) else ()
+
+
+(* orders an AList according to keys - every key needs to be there *)
+fun order eq keys list =
+ map (the o AList.lookup eq list) keys
+
+(* orders an AList according to keys - returns default for non-existing keys *)
+fun order_default eq default keys list =
+ map (the_default default o AList.lookup eq list) keys
+
+(* remove duplicates *)
+fun remove_dups eq [] = []
+ | remove_dups eq (x :: xs) =
+ if member eq xs x
+ then remove_dups eq xs
+ else x :: remove_dups eq xs
+
+fun last2 [] = raise Empty
+ | last2 [_] = raise Empty
+ | last2 [x, y] = (x, y)
+ | last2 (_ :: xs) = last2 xs
+
+fun split_last2 xs =
+ let
+ val (xs', x) = split_last xs
+ val (xs'', y) = split_last xs'
+ in
+ (xs'', y, x)
+ end
+
+fun map4 _ [] [] [] [] = []
+ | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
+
+fun split_filter f [] = ([], [])
+ | split_filter f (x :: xs) =
+ let
+ val (r, l) = split_filter f xs
+ in
+ if f x
+ then (x :: r, l)
+ else (r, x :: l)
+ end
+
+(* to be used with left-infix binop-operations *)
+fun fold_left f [] z = z
+ | fold_left f [x] z = x
+ | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
+
+
+
+fun is_true @{term "Trueprop True"} = true
+ | is_true _ = false
+
+fun dest_listT (Type (@{type_name list}, [T])) = T
+ | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
+
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
+ | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+
+
+fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm
+
+fun mk_all (a, T) t = Term.all T $ Abs (a, T, t)
+
+fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t)
+
+fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t)
+
+fun sum_case_const ty1 ty2 ty3 =
+ Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
+
+fun mk_sum_case trm1 trm2 =
+ let
+ val ([ty1], ty3) = strip_type (fastype_of trm1)
+ val ty2 = domain_type (fastype_of trm2)
+ in
+ sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
+ end
+
+
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
+
+
+fun mk_minus p = @{term "uminus::perm => perm"} $ p
+
+fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
+
+fun perm_ty ty = @{typ "perm"} --> ty --> ty
+fun perm_const ty = Const (@{const_name "permute"}, perm_ty ty)
+fun mk_perm_ty ty p trm = perm_const ty $ p $ trm
+fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
+
+fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
+ | dest_perm t = raise TERM ("dest_perm", [t]);
+
+end (* structure *)
+
+open Nominal_Basic;
\ No newline at end of file
--- a/Nominal/nominal_library.ML Wed Mar 02 12:48:00 2011 +0900
+++ b/Nominal/nominal_library.ML Wed Mar 02 12:49:01 2011 +0900
@@ -1,45 +1,11 @@
(* Title: nominal_library.ML
Author: Christian Urban
- Basic functions for nominal.
+ Library functions for nominal.
*)
signature NOMINAL_LIBRARY =
sig
- val trace: bool Unsynchronized.ref
- val trace_msg: (unit -> string) -> unit
-
- val last2: 'a list -> 'a * 'a
- val split_last2: 'a list -> 'a list * 'a * 'a
- val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
- val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list
- val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
- val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
- val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list
- val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a
-
- val is_true: term -> bool
-
- val dest_listT: typ -> typ
- val dest_fsetT: typ -> typ
-
- val mk_id: term -> term
- val mk_all: (string * typ) -> term -> term
- val mk_All: (string * typ) -> term -> term
- val mk_exists: (string * typ) -> term -> term
-
- val sum_case_const: typ -> typ -> typ -> term
- val mk_sum_case: term -> term -> term
-
- val mk_minus: term -> term
- val mk_plus: term -> term -> term
-
- val perm_ty: typ -> typ
- val perm_const: typ -> term
- val mk_perm_ty: typ -> term -> term -> term
- val mk_perm: term -> term -> term
- val dest_perm: term -> term * term
-
val mk_sort_of: term -> term
val atom_ty: typ -> typ
val atom_const: typ -> term
@@ -91,9 +57,6 @@
val mk_finite_ty: typ -> term -> term
val mk_finite: term -> term
- val mk_equiv: thm -> thm
- val safe_mk_equiv: thm -> thm
-
val mk_diff: term * term -> term
val mk_append: term * term -> term
val mk_union: term * term -> term
@@ -144,101 +107,6 @@
structure Nominal_Library: NOMINAL_LIBRARY =
struct
-val trace = Unsynchronized.ref false
-fun trace_msg msg = if ! trace then tracing (msg ()) else ()
-
-
-(* orders an AList according to keys - every key needs to be there *)
-fun order eq keys list =
- map (the o AList.lookup eq list) keys
-
-(* orders an AList according to keys - returns default for non-existing keys *)
-fun order_default eq default keys list =
- map (the_default default o AList.lookup eq list) keys
-
-(* remove duplicates *)
-fun remove_dups eq [] = []
- | remove_dups eq (x :: xs) =
- if member eq xs x
- then remove_dups eq xs
- else x :: remove_dups eq xs
-
-fun last2 [] = raise Empty
- | last2 [_] = raise Empty
- | last2 [x, y] = (x, y)
- | last2 (_ :: xs) = last2 xs
-
-fun split_last2 xs =
- let
- val (xs', x) = split_last xs
- val (xs'', y) = split_last xs'
- in
- (xs'', y, x)
- end
-
-fun map4 _ [] [] [] [] = []
- | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
-
-fun split_filter f [] = ([], [])
- | split_filter f (x :: xs) =
- let
- val (r, l) = split_filter f xs
- in
- if f x
- then (x :: r, l)
- else (r, x :: l)
- end
-
-(* to be used with left-infix binop-operations *)
-fun fold_left f [] z = z
- | fold_left f [x] z = x
- | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
-
-
-
-fun is_true @{term "Trueprop True"} = true
- | is_true _ = false
-
-fun dest_listT (Type (@{type_name list}, [T])) = T
- | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
-
-fun dest_fsetT (Type (@{type_name fset}, [T])) = T
- | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
-
-
-fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm
-
-fun mk_all (a, T) t = Term.all T $ Abs (a, T, t)
-
-fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t)
-
-fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t)
-
-fun sum_case_const ty1 ty2 ty3 =
- Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)
-
-fun mk_sum_case trm1 trm2 =
- let
- val ([ty1], ty3) = strip_type (fastype_of trm1)
- val ty2 = domain_type (fastype_of trm2)
- in
- sum_case_const ty1 ty2 ty3 $ trm1 $ trm2
- end
-
-
-
-fun mk_minus p = @{term "uminus::perm => perm"} $ p
-
-fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q
-
-fun perm_ty ty = @{typ "perm"} --> ty --> ty
-fun perm_const ty = Const (@{const_name "permute"}, perm_ty ty)
-fun mk_perm_ty ty p trm = perm_const ty $ p $ trm
-fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
-
-fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
- | dest_perm t = raise TERM ("dest_perm", [t]);
-
fun mk_sort_of t = @{term "sort_of"} $ t;
fun atom_ty ty = ty --> @{typ "atom"};
@@ -358,10 +226,6 @@
fun mk_finite t = mk_finite_ty (fastype_of t) t
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
-
-
(* functions that construct differences, appends and unions
but avoid producing empty atom sets or empty atom lists *)
--- a/Pearl-jv/Paper.thy Wed Mar 02 12:48:00 2011 +0900
+++ b/Pearl-jv/Paper.thy Wed Mar 02 12:49:01 2011 +0900
@@ -1,9 +1,8 @@
(*<*)
theory Paper
imports "../Nominal/Nominal2_Base"
- "../Nominal/Nominal2_Eqvt"
"../Nominal/Atoms"
- "../Nominal/Abs"
+ "../Nominal/Nominal2_Abs"
"LaTeXsugar"
begin
@@ -41,15 +40,11 @@
(*>*)
-(*
- TODO: write about supp of finite sets, abstraction over finite sets
-*)
-
section {* Introduction *}
text {*
Nominal Isabelle provides a proving infratructure for convenient reasoning
- about programming language calculi involving binders such as lambda abstractions or
+ about programming language calculi involving binders, such as lambda abstractions or
quantifications in type schemes:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -59,129 +54,14 @@
\noindent
At its core Nominal Isabelle is based on the nominal logic work by Pitts at
- al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a
+ al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a
sort-respecting permutation operation defined over a countably infinite
- collection of sorted atoms. The atoms are used for representing variable names
- that might be bound or free. Multiple sorts are necessary for being able to
- represent different kinds of variables. For example, in the language Mini-ML
- there are bound term variables in lambda abstractions and bound type variables in
- type schemes. In order to be able to separate them, each kind of variables needs to be
- represented by a different sort of atoms.
-
- The existing nominal logic work usually leaves implicit the sorting
- information for atoms and as far as we know leaves out a description of how
- sorts are represented. In our formalisation, we therefore have to make a
- design decision about how to implement sorted atoms and sort-respecting
- permutations. One possibility, which we described in \cite{Urban08}, is to
- have separate types for the different
- kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. With this
- design one can represent permutations as lists of pairs of atoms and the
- operation of applying a permutation to an object as the function
-
-
- @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-
- \noindent
- where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
- of the objects on which the permutation acts. For atoms
- the permutation operation is defined over the length of lists as follows
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
- @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} &
- $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\
- @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
- @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
- \end{tabular}\hfill\numbered{atomperm}
- \end{isabelle}
-
- \noindent
- where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
- @{text "b"}. For atoms with different type than the permutation, we
- define @{text "\<pi> \<bullet> c \<equiv> c"}.
-
- With the separate atom types and the list representation of permutations it
- is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
- permutation, since the type system excludes lists containing atoms of
- different type. However, a disadvantage is that whenever we need to
- generalise induction hypotheses by quantifying over permutations, we have to
- build quantifications like
-
- @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
-
- \noindent
- where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
- The reason is that the permutation operation behaves differently for
- every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
- single quantification to stand for all permutations. Similarly, the
- notion of support
-
- @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
-
- \noindent
- which we will define later, cannot be
- used to express the support of an object over \emph{all} atoms. The reason
- is that support can behave differently for each @{text
- "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
- a statement that an object, say @{text "x"}, is finitely supported we end up
- with having to state premises of the form
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
- \end{tabular}\hfill\numbered{fssequence}
- \end{isabelle}
-
- \noindent
- Because of these disadvantages, we will use in this paper a single unified atom type to
- represent atoms of different sorts. Consequently, we have to deal with the
- case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
- the type systems to exclude them.
-
- We also will not represent permutations as lists of pairs of atoms (as done in
- \cite{Urban08}). Although an
- advantage of this representation is that the basic operations on
- permutations are already defined in Isabelle's list library: composition of
- two permutations (written @{text "_ @ _"}) is just list append, and
- inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
- list reversal, and another advantage is that there is a well-understood
- induction principle for lists, a disadvantage is that permutations
- do not have unique representations as lists. We have to explicitly identify
- them according to the relation
+ collection of sorted atoms. The nominal logic work has been starting
+ point for a number of formalisations, most notable Norrish \cite{norrish04}
+ in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own
+ work in Isabelle/HOL.
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
- \end{tabular}\hfill\numbered{permequ}
- \end{isabelle}
-
- \noindent
- This is a problem when lifting the permutation operation to other types, for
- example sets, functions and so on. For this we need to ensure that every definition
- is well-behaved in the sense that it satisfies some
- \emph{permutation properties}. In the list representation we need
- to state these properties as follows:
-
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
- i) & @{text "[] \<bullet> x = x"}\\
- ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
- iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
- \end{tabular}\hfill\numbered{permprops}
- \end{isabelle}
-
- \noindent
- where the last clause explicitly states that the permutation operation has
- to produce the same result for related permutations. Moreover,
- ``permutations-as-lists'' do not satisfy the group properties. This means by
- using this representation we will not be able to reuse the extensive
- reasoning infrastructure in Isabelle about groups. Because of this, we will represent
- in this paper permutations as functions from atoms to atoms. This representation
- is unique and satisfies the laws of non-commutative groups.
-
Using a single atom type to represent atoms of different sorts and
representing permutations as functions are not new ideas; see
\cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution
@@ -199,6 +79,24 @@
section {* Sorted Atoms and Sort-Respecting Permutations *}
text {*
+ The most basic notion in this work is a
+ sort-respecting permutation operation defined over a countably infinite
+ collection of sorted atoms. The atoms are used for representing variable names
+ that might be bound or free. Multiple sorts are necessary for being able to
+ represent different kinds of variables. For example, in the language Mini-ML
+ there are bound term variables in lambda abstractions and bound type variables in
+ type schemes. In order to be able to separate them, each kind of variables needs to be
+ represented by a different sort of atoms.
+
+
+ The existing nominal logic work usually leaves implicit the sorting
+ information for atoms and as far as we know leaves out a description of how
+ sorts are represented. In our formalisation, we therefore have to make a
+ design decision about how to implement sorted atoms and sort-respecting
+ permutations. One possibility, which we described in \cite{Urban08}, is to
+ have separate types for the different
+ kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}.
+
In the nominal logic work of Pitts, binders and bound variables are
represented by \emph{atoms}. As stated above, we need to have different
\emph{sorts} of atoms to be able to bind different kinds of variables. A
@@ -314,7 +212,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 minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
\end{tabular}
\end{isabelle}
@@ -1202,184 +1100,123 @@
*}
-section {* Multi-Sorted Concrete Atoms *}
-
-(*<*)
-datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _")
-(*>*)
-
-text {*
- The formalisation presented so far allows us to streamline proofs and reduce
- the amount of custom ML-code in the existing implementation of Nominal
- Isabelle. In this section we describe a mechanism that extends the
- capabilities of Nominal Isabelle. This mechanism is about variables with
- additional information, for example typing constraints.
- While we leave a detailed treatment of binders and binding of variables for a
- later paper, we will have a look here at how such variables can be
- represented by concrete atoms.
-
- In the previous section we considered concrete atoms that can be used in
- simple binders like \emph{@{text "\<lambda>x. x"}}. Such concrete atoms do
- not carry any information beyond their identities---comparing for equality
- is really the only way to analyse ordinary concrete atoms.
- However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms
- underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a
- more complicated structure. For example in the ``Church-style'' lambda-term
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}
- \end{tabular}\hfill\numbered{church}
- \end{isabelle}
-
- \noindent
- both variables and binders include typing information indicated by @{text \<alpha>}
- and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
- "x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
- variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
- @{text "x\<^isub>\<beta>"}.
-
- To illustrate how we can deal with this phenomenon, let us represent object
- types like @{text \<alpha>} and @{text \<beta>} by the datatype
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- \isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}
- \end{tabular}
- \end{isabelle}
-
- \noindent
- If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the
- problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
- will always permute \emph{both} occurrences of @{text x}, even if the types
- @{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will
- eventually mean that both occurrences of @{text x} will become bound by a
- corresponding binder.
-
- Another attempt might be to define variables as an instance of the concrete
- atom type class, where a @{text ty} is somehow encoded within each variable.
- Remember we defined atoms as the datatype:
-*}
-
- datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
-
-text {*
- \noindent
- Considering our method of defining concrete atom types, the usage of a string
- for the sort of atoms seems a natural choice. However, none of the results so
- far depend on this choice and we are free to change it.
- One possibility is to encode types or any other information by making the sort
- argument parametric as follows:
-*}
-
- datatype 'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat
-
-text {*
- \noindent
- The problem with this possibility is that we are then back in the old
- situation where our permutation operation is parametric in two types and
- this would require to work around Isabelle/HOL's restriction on type
- classes. Fortunately, encoding the types in a separate parameter is not
- necessary for what we want to achieve, as we only have to know when two
- types are equal or not. The solution is to use a different sort for each
- object type. Then we can use the fact that permutations respect \emph{sorts} to
- ensure that permutations also respect \emph{object types}. In order to do
- this, we must define an injective function @{text "sort_ty"} mapping from
- object types to sorts. For defining functions like @{text "sort_ty"}, it is
- more convenient to use a tree datatype for sorts. Therefore we define
-*}
-
- datatype sort = Sort string "(sort list)"
- datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
-
-text {*
- \noindent
- With this definition,
- the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.
- The point, however, is that we can now define the function @{text sort_ty} simply as
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\
- @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}
- \end{tabular}\hfill\numbered{sortty}
- \end{isabelle}
-
- \noindent
- which can easily be shown to be injective.
-
- Having settled on what the sorts should be for ``Church-like'' atoms, we have to
- give a subtype definition for concrete atoms. Previously we identified a subtype consisting
- of atoms of only one specified sort. This must be generalised to all sorts the
- function @{text "sort_ty"} might produce, i.e.~the
- range of @{text "sort_ty"}. Therefore we define
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}
- \end{isabelle}
-
- \noindent
- This command gives us again injective representation and abstraction
- functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and
- @{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively.
-
- We can define the permutation operation for @{text var} as @{thm
- permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the
- injective function to type @{typ atom} as @{thm atom_var_def[THEN
- eq_reflection, no_vars]}. Finally, we can define a constructor function that
- makes a @{text var} from a variable name and an object type:
-
- @{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}
-
- \noindent
- With these definitions we can verify all the properties for concrete atom
- types except Property \ref{atomprops}@{text ".iii)"}, which requires every
- atom to have the same sort. This last property is clearly not true for type
- @{text "var"}.
- This fact is slightly unfortunate since this
- property allowed us to use the type-checker in order to shield the user from
- all sort-constraints. But this failure is expected here, because we cannot
- burden the type-system of Isabelle/HOL with the task of deciding when two
- object types are equal. This means we sometimes need to explicitly state sort
- constraints or explicitly discharge them, but as we will see in the lemma
- below this seems a natural price to pay in these circumstances.
-
- To sum up this section, the encoding of type-information into atoms allows us
- to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following
- lemma
-*}
-
- lemma
- assumes asm: "\<alpha> \<noteq> \<beta>"
- shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"
- using asm by simp
-
-text {*
- \noindent
- As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the
- swapping. With this we can faithfully represent bindings in languages
- involving ``Church-style'' terms and bindings as shown in \eqref{church}. We
- expect that the creation of such atoms can be easily automated so that the
- user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
- where the argument, or arguments, are datatypes for which we can automatically
- define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
- Our hope is that with this approach Benzmueller and Paulson can make
- headway with formalising their results
- about simple type theory \cite{PaulsonBenzmueller}.
- Because of its limitations, they did not attempt this with the old version
- of Nominal Isabelle. We also hope we can make progress with formalisations of
- HOL-based languages.
-*}
section {* Related Work *}
text {*
Add here comparison with old work.
-
The main point is that the above reasoning blends smoothly with the reasoning
infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
type class suffices.
+
+ With this
+ design one can represent permutations as lists of pairs of atoms and the
+ operation of applying a permutation to an object as the function
+
+
+ @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+
+ \noindent
+ where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
+ of the objects on which the permutation acts. For atoms
+ the permutation operation is defined over the length of lists as follows
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
+ @{text "(a b)::\<pi> \<bullet> c"} & @{text "="} &
+ $\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\
+ @{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
+ @{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
+ \end{tabular}\hfill\numbered{atomperm}
+ \end{isabelle}
+
+ \noindent
+ where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
+ @{text "b"}. For atoms with different type than the permutation, we
+ define @{text "\<pi> \<bullet> c \<equiv> c"}.
+
+ With the separate atom types and the list representation of permutations it
+ is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
+ permutation, since the type system excludes lists containing atoms of
+ different type. However, a disadvantage is that whenever we need to
+ generalise induction hypotheses by quantifying over permutations, we have to
+ build quantifications like
+
+ @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
+
+ \noindent
+ where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
+ The reason is that the permutation operation behaves differently for
+ every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
+ single quantification to stand for all permutations. Similarly, the
+ notion of support
+
+ @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
+
+ \noindent
+ which we will define later, cannot be
+ used to express the support of an object over \emph{all} atoms. The reason
+ is that support can behave differently for each @{text
+ "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
+ a statement that an object, say @{text "x"}, is finitely supported we end up
+ with having to state premises of the form
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l}
+ @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
+ \end{tabular}\hfill\numbered{fssequence}
+ \end{isabelle}
+
+ \noindent
+ Because of these disadvantages, we will use in this paper a single unified atom type to
+ represent atoms of different sorts. Consequently, we have to deal with the
+ case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
+ the type systems to exclude them.
+
+ We also will not represent permutations as lists of pairs of atoms (as done in
+ \cite{Urban08}). Although an
+ advantage of this representation is that the basic operations on
+ permutations are already defined in Isabelle's list library: composition of
+ two permutations (written @{text "_ @ _"}) is just list append, and
+ inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
+ list reversal, and another advantage is that there is a well-understood
+ induction principle for lists, a disadvantage is that permutations
+ do not have unique representations as lists. We have to explicitly identify
+ them according to the relation
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l}
+ @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
+ \end{tabular}\hfill\numbered{permequ}
+ \end{isabelle}
+
+ \noindent
+ This is a problem when lifting the permutation operation to other types, for
+ example sets, functions and so on. For this we need to ensure that every definition
+ is well-behaved in the sense that it satisfies some
+ \emph{permutation properties}. In the list representation we need
+ to state these properties as follows:
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+ i) & @{text "[] \<bullet> x = x"}\\
+ ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
+ iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
+ \end{tabular}\hfill\numbered{permprops}
+ \end{isabelle}
+
+ \noindent
+ where the last clause explicitly states that the permutation operation has
+ to produce the same result for related permutations. Moreover,
+ ``permutations-as-lists'' do not satisfy the group properties. This means by
+ using this representation we will not be able to reuse the extensive
+ reasoning infrastructure in Isabelle about groups. Because of this, we will represent
+ in this paper permutations as functions from atoms to atoms. This representation
+ is unique and satisfies the laws of non-commutative groups.
*}
--- a/Pearl-jv/ROOT.ML Wed Mar 02 12:48:00 2011 +0900
+++ b/Pearl-jv/ROOT.ML Wed Mar 02 12:49:01 2011 +0900
@@ -1,5 +1,4 @@
no_document use_thys ["../Nominal/Nominal2_Base",
- "../Nominal/Nominal2_Eqvt",
"../Nominal/Atoms",
"../Nominal/Nominal2_Abs",
"LaTeXsugar"];
--- a/Pearl-jv/document/root.bib Wed Mar 02 12:48:00 2011 +0900
+++ b/Pearl-jv/document/root.bib Wed Mar 02 12:49:01 2011 +0900
@@ -8,6 +8,17 @@
year = "2008"
}
+@InProceedings{norrish04,
+ author = {M.~Norrish},
+ title = {{R}ecursive {F}unction {D}efinition for {T}ypes with {B}inders},
+ booktitle = {Proc.~of the 17th International Conference Theorem Proving in
+ Higher Order Logics (TPHOLs)},
+ pages = {241--256},
+ year = {2004},
+ volume = {3223},
+ series = {LNCS}
+}
+
@InProceedings{GunterOsbornPopescu09,
author = {E.L.~Gunter and C.J.~Osborn and A.~Popescu},
title = {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in
@@ -19,6 +30,16 @@
series = {ENTCS}
}
+@InProceedings{AydemirBohannonWeirich07,
+ author = {B.~Aydemir and A.~Bohannon and S.~Weihrich},
+ title = {{N}ominal {R}easoning {T}echniques in {C}oq ({E}xtended {A}bstract)},
+ booktitle = {Proc.~of the 1st International Workshop on Logical Frameworks and Meta-Languages:
+ Theory and Practice (LFMTP)},
+ pages = {69--77},
+ year = {2007},
+ series = {ENTCS}
+}
+
@Unpublished{SatoPollack10,
author = {M.~Sato and R.~Pollack},
title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},
--- a/Pearl-jv/document/root.tex Wed Mar 02 12:48:00 2011 +0900
+++ b/Pearl-jv/document/root.tex Wed Mar 02 12:49:01 2011 +0900
@@ -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 formulate the theory so that it is
+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 also describe a formalisation of an
+abstraction operator that binds sets of names.
\end{abstract}
% generated text of all theories
--- a/Pearl/Paper.thy Wed Mar 02 12:48:00 2011 +0900
+++ b/Pearl/Paper.thy Wed Mar 02 12:49:01 2011 +0900
@@ -1,7 +1,6 @@
(*<*)
theory Paper
imports "../Nominal/Nominal2_Base"
- "../Nominal/Nominal2_Eqvt"
"../Nominal/Atoms"
"LaTeXsugar"
begin
@@ -346,7 +345,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 minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
\end{tabular}
\end{isabelle}
--- a/Pearl/ROOT.ML Wed Mar 02 12:48:00 2011 +0900
+++ b/Pearl/ROOT.ML Wed Mar 02 12:49:01 2011 +0900
@@ -1,5 +1,4 @@
no_document use_thys ["../Nominal/Nominal2_Base",
- "../Nominal/Nominal2_Eqvt",
"../Nominal/Atoms",
"LaTeXsugar"];