--- a/Nominal/Nominal2.thy Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2.thy Mon Feb 28 15:21:10 2011 +0000
@@ -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 Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Abs.thy Mon Feb 28 15:21:10 2011 +0000
@@ -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"
--- a/Nominal/Nominal2_Base.thy Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Base.thy Mon Feb 28 15:21:10 2011 +0000
@@ -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 *}
@@ -437,38 +441,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"
@@ -541,11 +513,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
@@ -555,22 +522,6 @@
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 *}
instantiation unit :: pt
@@ -635,6 +586,8 @@
shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
+
+
subsection {* Permutations for options *}
instantiation option :: (pt) pt
@@ -654,6 +607,8 @@
subsection {* Permutations for fsets *}
+
+
lemma permute_fset_rsp[quot_respect]:
shows "(op = ===> list_eq ===> list_eq) permute permute"
unfolding fun_rel_def
@@ -682,7 +637,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} *}
@@ -762,6 +719,277 @@
instance int :: pure
proof qed (rule permute_int_def)
+
+
+subsection {* Basic functions about permutations *}
+
+use "nominal_basics.ML"
+
+
+subsection {* Equivariance infrastructure *}
+
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+
+use "nominal_thmdecls.ML"
+setup "Nominal_ThmDecls.setup"
+
+
+lemmas [eqvt] =
+ (* permutations *)
+ uminus_eqvt add_perm_eqvt swap_eqvt
+
+ (* datatypes *)
+ Pair_eqvt
+ 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. *}
+
+(* 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
+
+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) = (\<not> (p \<bullet> A))"
+by (simp add: permute_bool_def)
+
+lemma conj_eqvt [eqvt]:
+ shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+ by (simp add: permute_bool_def)
+
+lemma imp_eqvt [eqvt]:
+ shows "p \<bullet> (A \<longrightarrow> B) = ((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) = ((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)
+
+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 ..
+
+
+subsubsection {* 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)
+
+
+
+
subsection {* Supp, Freshness and Supports *}
context pt
@@ -843,12 +1071,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
@@ -970,7 +1198,6 @@
"supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}"
-
section {* Finitely-supported types *}
class fs = pt +
@@ -1246,6 +1473,58 @@
by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+subsubsection {* 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)
+
+
instance list :: (fs) fs
apply default
apply (induct_tac x)
@@ -1266,13 +1545,6 @@
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"
@@ -1316,6 +1588,16 @@
using supp_fun_app by auto
qed
+lemma supp_fun_app_eqvt:
+ assumes a: "eqvt f"
+ shows "supp (f x) \<subseteq> supp x"
+proof -
+ from a have "supp f = {}" by (simp add: supp_fun_eqvt)
+ then show "supp (f x) \<subseteq> supp x" using supp_fun_app by blast
+qed
+
+
+
text {* equivariance of a function at a given argument *}
definition
@@ -1353,7 +1635,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"
@@ -1445,27 +1728,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 -
@@ -1489,12 +1751,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
@@ -1564,10 +1828,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
@@ -1610,6 +1870,30 @@
done
+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)
+
section {* Freshness and Fresh-Star *}
lemma fresh_Unit_elim:
@@ -1751,15 +2035,10 @@
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
-
+by (perm_simp) (rule refl)
section {* Induction principle for permutations *}
@@ -2191,6 +2470,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)"
@@ -2300,6 +2581,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)
@@ -2318,7 +2600,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
@@ -2638,5 +2920,10 @@
use "nominal_atoms.ML"
+section {* automatic equivariance procedure for inductive definitions *}
+
+use "nominal_eqvt.ML"
+
+
end
--- a/Nominal/Nominal2_Eqvt.thy Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy Mon Feb 28 15:21:10 2011 +0000
@@ -2,330 +2,13 @@
Author: Brian Huffman,
Author: Christian Urban
- Equivariance, supp and freshness lemmas for various operators
- (contains many, but not all such lemmas).
+ Test cases for perm_simp
*)
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]] *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/nominal_basics.ML Mon Feb 28 15:21:10 2011 +0000
@@ -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 Fri Feb 25 21:23:30 2011 +0000
+++ b/Nominal/nominal_library.ML Mon Feb 28 15:21:10 2011 +0000
@@ -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 *)