--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/Nominal.thy Mon Oct 17 12:30:57 2005 +0200
@@ -0,0 +1,2309 @@
+(* $Id$ *)
+
+theory nominal
+imports Main
+ uses ("nominal_package.ML") ("nominal_induct.ML") ("nominal_permeq.ML")
+begin
+
+ML {* reset NameSpace.unique_names; *}
+
+section {* Permutations *}
+(*======================*)
+
+types
+ 'x prm = "('x \<times> 'x) list"
+
+(* polymorphic operations for permutation and swapping*)
+consts
+ perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [80,80] 80)
+ swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
+
+(* permutation on sets *)
+defs (overloaded)
+ perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
+
+(* permutation on units and products *)
+primrec (perm_unit)
+ "pi\<bullet>() = ()"
+
+primrec (perm_prod)
+ "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)"
+
+lemma perm_fst:
+ "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
+ by (cases x, simp)
+
+lemma perm_snd:
+ "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
+ by (cases x, simp)
+
+(* permutation on lists *)
+primrec (perm_list)
+ perm_nil_def: "pi\<bullet>[] = []"
+ perm_cons_def: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
+
+lemma perm_append:
+ fixes pi :: "'x prm"
+ and l1 :: "'a list"
+ and l2 :: "'a list"
+ shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
+ by (induct l1, auto)
+
+lemma perm_rev:
+ fixes pi :: "'x prm"
+ and l :: "'a list"
+ shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
+ by (induct l, simp_all add: perm_append)
+
+(* permutation on functions *)
+defs (overloaded)
+ perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
+
+(* permutation on bools *)
+primrec (perm_bool)
+ perm_true_def: "pi\<bullet>True = True"
+ perm_false_def: "pi\<bullet>False = False"
+
+(* permutation on options *)
+primrec (perm_option)
+ perm_some_def: "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
+ perm_none_def: "pi\<bullet>None = None"
+
+(* a "private" copy of the option type used in the abstraction function *)
+datatype 'a nOption = nSome 'a | nNone
+
+primrec (perm_noption)
+ perm_Nsome_def: "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
+ perm_Nnone_def: "pi\<bullet>nNone = nNone"
+
+(* permutation on characters (used in strings) *)
+defs (overloaded)
+ perm_char_def: "pi\<bullet>(s::char) \<equiv> s"
+
+(* permutation on ints *)
+defs (overloaded)
+ perm_int_def: "pi\<bullet>(i::int) \<equiv> i"
+
+(* permutation on nats *)
+defs (overloaded)
+ perm_nat_def: "pi\<bullet>(i::nat) \<equiv> i"
+
+section {* permutation equality *}
+(*==============================*)
+
+constdefs
+ prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<sim> _ " [80,80] 80)
+ "pi1 \<sim> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
+
+section {* Support, Freshness and Supports*}
+(*========================================*)
+constdefs
+ supp :: "'a \<Rightarrow> ('x set)"
+ "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
+
+ fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" (" _ \<sharp> _" [80,80] 80)
+ "a \<sharp> x \<equiv> a \<notin> supp x"
+
+ supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80)
+ "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
+
+lemma supp_fresh_iff:
+ fixes x :: "'a"
+ shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
+apply(simp add: fresh_def)
+done
+
+lemma supp_unit:
+ shows "supp () = {}"
+ by (simp add: supp_def)
+
+lemma supp_prod:
+ fixes x :: "'a"
+ and y :: "'b"
+ shows "(supp (x,y)) = (supp x)\<union>(supp y)"
+ by (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
+
+lemma supp_list_nil:
+ shows "supp [] = {}"
+apply(simp add: supp_def)
+done
+
+lemma supp_list_cons:
+ fixes x :: "'a"
+ and xs :: "'a list"
+ shows "supp (x#xs) = (supp x)\<union>(supp xs)"
+apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
+done
+
+lemma supp_list_append:
+ fixes xs :: "'a list"
+ and ys :: "'a list"
+ shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
+ by (induct xs, auto simp add: supp_list_nil supp_list_cons)
+
+lemma supp_list_rev:
+ fixes xs :: "'a list"
+ shows "supp (rev xs) = (supp xs)"
+ by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil)
+
+lemma supp_bool:
+ fixes x :: "bool"
+ shows "supp (x) = {}"
+ apply(case_tac "x")
+ apply(simp_all add: supp_def)
+done
+
+lemma supp_some:
+ fixes x :: "'a"
+ shows "supp (Some x) = (supp x)"
+ apply(simp add: supp_def)
+ done
+
+lemma supp_none:
+ fixes x :: "'a"
+ shows "supp (None) = {}"
+ apply(simp add: supp_def)
+ done
+
+lemma supp_int:
+ fixes i::"int"
+ shows "supp (i) = {}"
+ apply(simp add: supp_def perm_int_def)
+ done
+
+lemma fresh_prod:
+ fixes a :: "'x"
+ and x :: "'a"
+ and y :: "'b"
+ shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)"
+ by (simp add: fresh_def supp_prod)
+
+lemma fresh_list_nil:
+ fixes a :: "'x"
+ shows "a\<sharp>([]::'a list)"
+ by (simp add: fresh_def supp_list_nil)
+
+lemma fresh_list_cons:
+ fixes a :: "'x"
+ and x :: "'a"
+ and xs :: "'a list"
+ shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)"
+ by (simp add: fresh_def supp_list_cons)
+
+lemma fresh_list_append:
+ fixes a :: "'x"
+ and xs :: "'a list"
+ and ys :: "'a list"
+ shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)"
+ by (simp add: fresh_def supp_list_append)
+
+lemma fresh_list_rev:
+ fixes a :: "'x"
+ and xs :: "'a list"
+ shows "a\<sharp>(rev xs) = a\<sharp>xs"
+ by (simp add: fresh_def supp_list_rev)
+
+lemma fresh_none:
+ fixes a :: "'x"
+ shows "a\<sharp>None"
+ apply(simp add: fresh_def supp_none)
+ done
+
+lemma fresh_some:
+ fixes a :: "'x"
+ and x :: "'a"
+ shows "a\<sharp>(Some x) = a\<sharp>x"
+ apply(simp add: fresh_def supp_some)
+ done
+
+section {* Abstract Properties for Permutations and Atoms *}
+(*=========================================================*)
+
+(* properties for being a permutation type *)
+constdefs
+ "pt TYPE('a) TYPE('x) \<equiv>
+ (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and>
+ (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and>
+ (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<sim> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"
+
+(* properties for being an atom type *)
+constdefs
+ "at TYPE('x) \<equiv>
+ (\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and>
+ (\<forall>(a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))\<bullet>x = swap (a,b) (pi\<bullet>x)) \<and>
+ (\<forall>(a::'x) (b::'x) (c::'x). swap (a,b) c = (if a=c then b else (if b=c then a else c))) \<and>
+ (infinite (UNIV::'x set))"
+
+(* property of two atom-types being disjoint *)
+constdefs
+ "disjoint TYPE('x) TYPE('y) \<equiv>
+ (\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and>
+ (\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)"
+
+(* composition property of two permutation on a type 'a *)
+constdefs
+ "cp TYPE ('a) TYPE('x) TYPE('y) \<equiv>
+ (\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))"
+
+(* property of having finite support *)
+constdefs
+ "fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)"
+
+section {* Lemmas about the atom-type properties*}
+(*==============================================*)
+
+lemma at1:
+ fixes x::"'x"
+ assumes a: "at TYPE('x)"
+ shows "([]::'x prm)\<bullet>x = x"
+ using a by (simp add: at_def)
+
+lemma at2:
+ fixes a ::"'x"
+ and b ::"'x"
+ and x ::"'x"
+ and pi::"'x prm"
+ assumes a: "at TYPE('x)"
+ shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)"
+ using a by (simp only: at_def)
+
+lemma at3:
+ fixes a ::"'x"
+ and b ::"'x"
+ and c ::"'x"
+ assumes a: "at TYPE('x)"
+ shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
+ using a by (simp only: at_def)
+
+(* rules to calculate simple premutations *)
+lemmas at_calc = at2 at1 at3
+
+lemma at4:
+ assumes a: "at TYPE('x)"
+ shows "infinite (UNIV::'x set)"
+ using a by (simp add: at_def)
+
+lemma at_append:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ and c :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)"
+proof (induct pi1)
+ case Nil show ?case by (simp add: at1[OF at])
+next
+ case (Cons x xs)
+ assume i: "(xs @ pi2)\<bullet>c = xs\<bullet>(pi2\<bullet>c)"
+ have "(x#xs)@pi2 = x#(xs@pi2)" by simp
+ thus ?case using i by (cases "x", simp add: at2[OF at])
+qed
+
+lemma at_swap:
+ fixes a :: "'x"
+ and b :: "'x"
+ and c :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "swap (a,b) (swap (a,b) c) = c"
+ by (auto simp add: at3[OF at])
+
+lemma at_rev_pi:
+ fixes pi :: "'x prm"
+ and c :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "(rev pi)\<bullet>(pi\<bullet>c) = c"
+proof(induct pi)
+ case Nil show ?case by (simp add: at1[OF at])
+next
+ case (Cons x xs) thus ?case
+ by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at])
+qed
+
+lemma at_pi_rev:
+ fixes pi :: "'x prm"
+ and x :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "pi\<bullet>((rev pi)\<bullet>x) = x"
+ by (rule at_rev_pi[OF at, of "rev pi" _,simplified])
+
+lemma at_bij1:
+ fixes pi :: "'x prm"
+ and x :: "'x"
+ and y :: "'x"
+ assumes at: "at TYPE('x)"
+ and a: "(pi\<bullet>x) = y"
+ shows "x=(rev pi)\<bullet>y"
+proof -
+ from a have "y=(pi\<bullet>x)" by (rule sym)
+ thus ?thesis by (simp only: at_rev_pi[OF at])
+qed
+
+lemma at_bij2:
+ fixes pi :: "'x prm"
+ and x :: "'x"
+ and y :: "'x"
+ assumes at: "at TYPE('x)"
+ and a: "((rev pi)\<bullet>x) = y"
+ shows "x=pi\<bullet>y"
+proof -
+ from a have "y=((rev pi)\<bullet>x)" by (rule sym)
+ thus ?thesis by (simp only: at_pi_rev[OF at])
+qed
+
+lemma at_bij:
+ fixes pi :: "'x prm"
+ and x :: "'x"
+ and y :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
+proof
+ assume "pi\<bullet>x = pi\<bullet>y"
+ hence "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at])
+ thus "x=y" by (simp only: at_rev_pi[OF at])
+next
+ assume "x=y"
+ thus "pi\<bullet>x = pi\<bullet>y" by simp
+qed
+
+lemma at_supp:
+ fixes x :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "supp x = {x}"
+proof (simp add: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at], auto)
+ assume f: "finite {b::'x. b \<noteq> x}"
+ have a1: "{b::'x. b \<noteq> x} = UNIV-{x}" by force
+ have a2: "infinite (UNIV::'x set)" by (rule at4[OF at])
+ from f a1 a2 show False by force
+qed
+
+lemma at_fresh:
+ fixes a :: "'x"
+ and b :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "(a\<sharp>b) = (a\<noteq>b)"
+ by (simp add: at_supp[OF at] fresh_def)
+
+lemma at_prm_fresh[rule_format]:
+ fixes c :: "'x"
+ and pi:: "'x prm"
+ assumes at: "at TYPE('x)"
+ shows "c\<sharp>pi \<longrightarrow> pi\<bullet>c = c"
+apply(induct pi)
+apply(simp add: at1[OF at])
+apply(force simp add: fresh_list_cons at2[OF at] fresh_prod at_fresh[OF at] at3[OF at])
+done
+
+lemma at_prm_rev_eq:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ assumes at: "at TYPE('x)"
+ shows a: "((rev pi1) \<sim> (rev pi2)) = (pi1 \<sim> pi2)"
+proof (simp add: prm_eq_def, auto)
+ fix x
+ assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
+ hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp
+ hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at])
+ hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at])
+ thus "pi1 \<bullet> x = pi2 \<bullet> x" by simp
+next
+ fix x
+ assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x"
+ hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp
+ hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at])
+ hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at])
+ thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp
+qed
+
+lemma at_prm_rev_eq1:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ assumes at: "at TYPE('x)"
+ shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1) \<sim> (rev pi2)"
+ by (simp add: at_prm_rev_eq[OF at])
+
+lemma at_ds1:
+ fixes a :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "[(a,a)] \<sim> []"
+ by (force simp add: prm_eq_def at_calc[OF at])
+
+lemma at_ds2:
+ fixes pi :: "'x prm"
+ and a :: "'x"
+ and b :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "(pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)]) \<sim> ([(a,b)]@pi)"
+ by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at]
+ at_rev_pi[OF at] at_calc[OF at])
+
+lemma at_ds3:
+ fixes a :: "'x"
+ and b :: "'x"
+ and c :: "'x"
+ assumes at: "at TYPE('x)"
+ and a: "distinct [a,b,c]"
+ shows "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]"
+ using a by (force simp add: prm_eq_def at_calc[OF at])
+
+lemma at_ds4:
+ fixes a :: "'x"
+ and b :: "'x"
+ and pi :: "'x prm"
+ assumes at: "at TYPE('x)"
+ shows "(pi@[(a,(rev pi)\<bullet>b)]) \<sim> ([(pi\<bullet>a,b)]@pi)"
+ by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at]
+ at_pi_rev[OF at] at_rev_pi[OF at])
+
+lemma at_ds5:
+ fixes a :: "'x"
+ and b :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "[(a,b)] \<sim> [(b,a)]"
+ by (force simp add: prm_eq_def at_calc[OF at])
+
+lemma at_ds6:
+ fixes a :: "'x"
+ and b :: "'x"
+ and c :: "'x"
+ assumes at: "at TYPE('x)"
+ and a: "distinct [a,b,c]"
+ shows "[(a,c),(a,b)] \<sim> [(b,c),(a,c)]"
+ using a by (force simp add: prm_eq_def at_calc[OF at])
+
+lemma at_ds7:
+ fixes pi :: "'x prm"
+ assumes at: "at TYPE('x)"
+ shows "((rev pi)@pi) \<sim> []"
+ by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at])
+
+lemma at_ds8_aux:
+ fixes pi :: "'x prm"
+ and a :: "'x"
+ and b :: "'x"
+ and c :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)"
+ by (force simp add: at_calc[OF at] at_bij[OF at])
+
+lemma at_ds8:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ and a :: "'x"
+ and b :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "(pi1@pi2) \<sim> ((pi1\<bullet>pi2)@pi1)"
+apply(induct_tac pi2)
+apply(simp add: prm_eq_def)
+apply(auto simp add: prm_eq_def)
+apply(simp add: at2[OF at])
+apply(drule_tac x="aa" in spec)
+apply(drule sym)
+apply(simp)
+apply(simp add: at_append[OF at])
+apply(simp add: at2[OF at])
+apply(simp add: at_ds8_aux[OF at])
+done
+
+lemma at_ds9:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ and a :: "'x"
+ and b :: "'x"
+ assumes at: "at TYPE('x)"
+ shows " ((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
+apply(induct_tac pi2)
+apply(simp add: prm_eq_def)
+apply(auto simp add: prm_eq_def)
+apply(simp add: at_append[OF at])
+apply(simp add: at2[OF at] at1[OF at])
+apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec)
+apply(drule sym)
+apply(simp)
+apply(simp add: at_ds8_aux[OF at])
+apply(simp add: at_rev_pi[OF at])
+done
+
+--"there always exists an atom not being in a finite set"
+lemma ex_in_inf:
+ fixes A::"'x set"
+ assumes at: "at TYPE('x)"
+ and fs: "finite A"
+ shows "\<exists>c::'x. c\<notin>A"
+proof -
+ from fs at4[OF at] have "infinite ((UNIV::'x set) - A)"
+ by (simp add: Diff_infinite_finite)
+ hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
+ hence "\<exists>c::'x. c\<in>((UNIV::'x set) - A)" by force
+ thus "\<exists>c::'x. c\<notin>A" by force
+qed
+
+--"there always exists a fresh name for an object with finite support"
+lemma at_exists_fresh:
+ fixes x :: "'a"
+ assumes at: "at TYPE('x)"
+ and fs: "finite ((supp x)::'x set)"
+ shows "\<exists>c::'x. c\<sharp>x"
+ by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs])
+
+--"the at-props imply the pt-props"
+lemma at_pt_inst:
+ assumes at: "at TYPE('x)"
+ shows "pt TYPE('x) TYPE('x)"
+apply(auto simp only: pt_def)
+apply(simp only: at1[OF at])
+apply(simp only: at_append[OF at])
+apply(simp add: prm_eq_def)
+done
+
+section {* finite support properties *}
+(*===================================*)
+
+lemma fs1:
+ fixes x :: "'a"
+ assumes a: "fs TYPE('a) TYPE('x)"
+ shows "finite ((supp x)::'x set)"
+ using a by (simp add: fs_def)
+
+lemma fs_at_inst:
+ fixes a :: "'x"
+ assumes at: "at TYPE('x)"
+ shows "fs TYPE('x) TYPE('x)"
+apply(simp add: fs_def)
+apply(simp add: at_supp[OF at])
+done
+
+lemma fs_unit_inst:
+ shows "fs TYPE(unit) TYPE('x)"
+apply(simp add: fs_def)
+apply(simp add: supp_unit)
+done
+
+lemma fs_prod_inst:
+ assumes fsa: "fs TYPE('a) TYPE('x)"
+ and fsb: "fs TYPE('b) TYPE('x)"
+ shows "fs TYPE('a\<times>'b) TYPE('x)"
+apply(unfold fs_def)
+apply(auto simp add: supp_prod)
+apply(rule fs1[OF fsa])
+apply(rule fs1[OF fsb])
+done
+
+lemma fs_list_inst:
+ assumes fs: "fs TYPE('a) TYPE('x)"
+ shows "fs TYPE('a list) TYPE('x)"
+apply(simp add: fs_def, rule allI)
+apply(induct_tac x)
+apply(simp add: supp_list_nil)
+apply(simp add: supp_list_cons)
+apply(rule fs1[OF fs])
+done
+
+lemma fs_bool_inst:
+ shows "fs TYPE(bool) TYPE('x)"
+apply(simp add: fs_def, rule allI)
+apply(simp add: supp_bool)
+done
+
+lemma fs_int_inst:
+ shows "fs TYPE(int) TYPE('x)"
+apply(simp add: fs_def, rule allI)
+apply(simp add: supp_int)
+done
+
+section {* Lemmas about the permutation properties *}
+(*=================================================*)
+
+lemma pt1:
+ fixes x::"'a"
+ assumes a: "pt TYPE('a) TYPE('x)"
+ shows "([]::'x prm)\<bullet>x = x"
+ using a by (simp add: pt_def)
+
+lemma pt2:
+ fixes pi1::"'x prm"
+ and pi2::"'x prm"
+ and x ::"'a"
+ assumes a: "pt TYPE('a) TYPE('x)"
+ shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)"
+ using a by (simp add: pt_def)
+
+lemma pt3:
+ fixes pi1::"'x prm"
+ and pi2::"'x prm"
+ and x ::"'a"
+ assumes a: "pt TYPE('a) TYPE('x)"
+ shows "pi1 \<sim> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x"
+ using a by (simp add: pt_def)
+
+lemma pt3_rev:
+ fixes pi1::"'x prm"
+ and pi2::"'x prm"
+ and x ::"'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
+ by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])
+
+section {* composition properties *}
+(* ============================== *)
+lemma cp1:
+ fixes pi1::"'x prm"
+ and pi2::"'y prm"
+ and x ::"'a"
+ assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)"
+ using cp by (simp add: cp_def)
+
+lemma cp_pt_inst:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "cp TYPE('a) TYPE('x) TYPE('x)"
+apply(auto simp add: cp_def pt2[OF pt,symmetric])
+apply(rule pt3[OF pt])
+apply(rule at_ds8[OF at])
+done
+
+section {* permutation type instances *}
+(* ===================================*)
+
+lemma pt_set_inst:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ shows "pt TYPE('a set) TYPE('x)"
+apply(simp add: pt_def)
+apply(simp_all add: perm_set_def)
+apply(simp add: pt1[OF pt])
+apply(force simp add: pt2[OF pt] pt3[OF pt])
+done
+
+lemma pt_list_nil:
+ fixes xs :: "'a list"
+ assumes pt: "pt TYPE('a) TYPE ('x)"
+ shows "([]::'x prm)\<bullet>xs = xs"
+apply(induct_tac xs)
+apply(simp_all add: pt1[OF pt])
+done
+
+lemma pt_list_append:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ and xs :: "'a list"
+ assumes pt: "pt TYPE('a) TYPE ('x)"
+ shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)"
+apply(induct_tac xs)
+apply(simp_all add: pt2[OF pt])
+done
+
+lemma pt_list_prm_eq:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ and xs :: "'a list"
+ assumes pt: "pt TYPE('a) TYPE ('x)"
+ shows "pi1 \<sim> pi2 \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
+apply(induct_tac xs)
+apply(simp_all add: prm_eq_def pt3[OF pt])
+done
+
+lemma pt_list_inst:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ shows "pt TYPE('a list) TYPE('x)"
+apply(auto simp only: pt_def)
+apply(rule pt_list_nil[OF pt])
+apply(rule pt_list_append[OF pt])
+apply(rule pt_list_prm_eq[OF pt],assumption)
+done
+
+lemma pt_unit_inst:
+ shows "pt TYPE(unit) TYPE('x)"
+ by (simp add: pt_def)
+
+lemma pt_prod_inst:
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('b) TYPE('x)"
+ shows "pt TYPE('a \<times> 'b) TYPE('x)"
+ apply(auto simp add: pt_def)
+ apply(rule pt1[OF pta])
+ apply(rule pt1[OF ptb])
+ apply(rule pt2[OF pta])
+ apply(rule pt2[OF ptb])
+ apply(rule pt3[OF pta],assumption)
+ apply(rule pt3[OF ptb],assumption)
+ done
+
+lemma pt_fun_inst:
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('b) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pt TYPE('a\<Rightarrow>'b) TYPE('x)"
+apply(auto simp only: pt_def)
+apply(simp_all add: perm_fun_def)
+apply(simp add: pt1[OF pta] pt1[OF ptb])
+apply(simp add: pt2[OF pta] pt2[OF ptb])
+apply(subgoal_tac "(rev pi1) \<sim> (rev pi2)")(*A*)
+apply(simp add: pt3[OF pta] pt3[OF ptb])
+(*A*)
+apply(simp add: at_prm_rev_eq[OF at])
+done
+
+lemma pt_option_inst:
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ shows "pt TYPE('a option) TYPE('x)"
+apply(auto simp only: pt_def)
+apply(case_tac "x")
+apply(simp_all add: pt1[OF pta])
+apply(case_tac "x")
+apply(simp_all add: pt2[OF pta])
+apply(case_tac "x")
+apply(simp_all add: pt3[OF pta])
+done
+
+lemma pt_noption_inst:
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ shows "pt TYPE('a nOption) TYPE('x)"
+apply(auto simp only: pt_def)
+apply(case_tac "x")
+apply(simp_all add: pt1[OF pta])
+apply(case_tac "x")
+apply(simp_all add: pt2[OF pta])
+apply(case_tac "x")
+apply(simp_all add: pt3[OF pta])
+done
+
+lemma pt_bool_inst:
+ shows "pt TYPE(bool) TYPE('x)"
+ apply(auto simp add: pt_def)
+ apply(case_tac "x=True", simp add: perm_bool_def, simp add: perm_bool_def)+
+ done
+
+lemma pt_prm_inst:
+ assumes at: "at TYPE('x)"
+ shows "pt TYPE('x prm) TYPE('x)"
+apply(rule pt_list_inst)
+apply(rule pt_prod_inst)
+apply(rule at_pt_inst[OF at])+
+done
+
+section {* further lemmas for permutation types *}
+(*==============================================*)
+
+lemma pt_rev_pi:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(rev pi)\<bullet>(pi\<bullet>x) = x"
+proof -
+ have "((rev pi)@pi) \<sim> ([]::'x prm)" by (simp add: at_ds7[OF at])
+ hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt])
+ thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt])
+qed
+
+lemma pt_pi_rev:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>((rev pi)\<bullet>x) = x"
+ by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified])
+
+lemma pt_bij1:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and y :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a: "(pi\<bullet>x) = y"
+ shows "x=(rev pi)\<bullet>y"
+proof -
+ from a have "y=(pi\<bullet>x)" by (rule sym)
+ thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at])
+qed
+
+lemma pt_bij2:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and y :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a: "x = (rev pi)\<bullet>y"
+ shows "(pi\<bullet>x)=y"
+ using a by (simp add: pt_pi_rev[OF pt, OF at])
+
+lemma pt_bij:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and y :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
+proof
+ assume "pi\<bullet>x = pi\<bullet>y"
+ hence "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at])
+ thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at])
+next
+ assume "x=y"
+ thus "pi\<bullet>x = pi\<bullet>y" by simp
+qed
+
+lemma pt_bij3:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and y :: "'a"
+ assumes a: "x=y"
+ shows "(pi\<bullet>x = pi\<bullet>y)"
+using a by simp
+
+lemma pt_bij4:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and y :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a: "pi\<bullet>x = pi\<bullet>y"
+ shows "x = y"
+using a by (simp add: pt_bij[OF pt, OF at])
+
+lemma pt_swap_bij:
+ fixes a :: "'x"
+ and b :: "'x"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x"
+ by (rule pt_bij2[OF pt, OF at], simp)
+
+lemma pt_set_bij1:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and X :: "'a set"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
+ by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+
+lemma pt_set_bij1a:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and X :: "'a set"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
+ by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+
+lemma pt_set_bij:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and X :: "'a set"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
+ by (simp add: perm_set_def pt_set_bij1[OF pt, OF at] pt_bij[OF pt, OF at])
+
+lemma pt_set_bij2:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and X :: "'a set"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a: "x\<in>X"
+ shows "(pi\<bullet>x)\<in>(pi\<bullet>X)"
+ using a by (simp add: pt_set_bij[OF pt, OF at])
+
+lemma pt_set_bij3:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and X :: "'a set"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
+apply(case_tac "x\<in>X = True")
+apply(auto)
+done
+
+lemma pt_list_set_pi:
+ fixes pi :: "'x prm"
+ and xs :: "'a list"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
+by (induct xs, auto simp add: perm_set_def pt1[OF pt])
+
+-- "some helper lemmas for the pt_perm_supp_ineq lemma"
+lemma Collect_permI:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ assumes a: "\<forall>x. (P1 x = P2 x)"
+ shows "{pi\<bullet>x| x. P1 x} = {pi\<bullet>x| x. P2 x}"
+ using a by force
+
+lemma Infinite_cong:
+ assumes a: "X = Y"
+ shows "infinite X = infinite Y"
+ using a by (simp)
+
+lemma pt_set_eq_ineq:
+ fixes pi :: "'y prm"
+ assumes pt: "pt TYPE('x) TYPE('y)"
+ and at: "at TYPE('y)"
+ shows "{pi\<bullet>x| x::'x. P x} = {x::'x. P ((rev pi)\<bullet>x)}"
+ by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+
+lemma pt_inject_on_ineq:
+ fixes X :: "'y set"
+ and pi :: "'x prm"
+ assumes pt: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "inj_on (perm pi) X"
+proof (unfold inj_on_def, intro strip)
+ fix x::"'y" and y::"'y"
+ assume "pi\<bullet>x = pi\<bullet>y"
+ thus "x=y" by (simp add: pt_bij[OF pt, OF at])
+qed
+
+lemma pt_set_finite_ineq:
+ fixes X :: "'x set"
+ and pi :: "'y prm"
+ assumes pt: "pt TYPE('x) TYPE('y)"
+ and at: "at TYPE('y)"
+ shows "finite (pi\<bullet>X) = finite X"
+proof -
+ have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
+ show ?thesis
+ proof (rule iffI)
+ assume "finite (pi\<bullet>X)"
+ hence "finite (perm pi ` X)" using image by (simp)
+ thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD)
+ next
+ assume "finite X"
+ hence "finite (perm pi ` X)" by (rule finite_imageI)
+ thus "finite (pi\<bullet>X)" using image by (simp)
+ qed
+qed
+
+lemma pt_set_infinite_ineq:
+ fixes X :: "'x set"
+ and pi :: "'y prm"
+ assumes pt: "pt TYPE('x) TYPE('y)"
+ and at: "at TYPE('y)"
+ shows "infinite (pi\<bullet>X) = infinite X"
+using pt at by (simp add: pt_set_finite_ineq)
+
+lemma pt_perm_supp_ineq:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
+proof -
+ have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
+ also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}"
+ proof (rule Collect_permI, rule allI, rule iffI)
+ fix a
+ assume "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}"
+ hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
+ thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: perm_set_def)
+ next
+ fix a
+ assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
+ hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
+ thus "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}"
+ by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
+ qed
+ also have "\<dots> = {a. infinite {b::'y. [((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x \<noteq> x}}"
+ by (simp add: pt_set_eq_ineq[OF ptb, OF at])
+ also have "\<dots> = {a. infinite {b. pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> (pi\<bullet>x)}}"
+ by (simp add: pt_bij[OF pta, OF at])
+ also have "\<dots> = {a. infinite {b. [(a,b)]\<bullet>(pi\<bullet>x) \<noteq> (pi\<bullet>x)}}"
+ proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong)
+ fix a::"'y" and b::"'y"
+ have "pi\<bullet>(([((rev pi)\<bullet>a,(rev pi)\<bullet>b)])\<bullet>x) = [(a,b)]\<bullet>(pi\<bullet>x)"
+ by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at])
+ thus "(pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> pi\<bullet>x) = ([(a,b)]\<bullet>(pi\<bullet>x) \<noteq> pi\<bullet>x)" by simp
+ qed
+ finally show "?LHS = ?RHS" by (simp add: supp_def)
+qed
+
+lemma pt_perm_supp:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi\<bullet>((supp x)::'x set)) = supp (pi\<bullet>x)"
+apply(rule pt_perm_supp_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
+
+lemma pt_supp_finite_pi:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f: "finite ((supp x)::'x set)"
+ shows "finite ((supp (pi\<bullet>x))::'x set)"
+apply(simp add: pt_perm_supp[OF pt, OF at, symmetric])
+apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at])
+apply(rule f)
+done
+
+lemma pt_fresh_left_ineq:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'y"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
+apply(simp add: fresh_def)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
+done
+
+lemma pt_fresh_right_ineq:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'y"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
+apply(simp add: fresh_def)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
+done
+
+lemma pt_fresh_bij_ineq:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'y"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(simp add: pt_rev_pi[OF ptb, OF at])
+done
+
+lemma pt_fresh_left:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
+apply(rule pt_fresh_left_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
+
+lemma pt_fresh_right:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
+apply(rule pt_fresh_right_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
+
+lemma pt_fresh_bij:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
+apply(rule pt_fresh_bij_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
+
+lemma pt_fresh_bij1:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a: "a\<sharp>x"
+ shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
+using a by (simp add: pt_fresh_bij[OF pt, OF at])
+
+lemma pt_perm_fresh1:
+ fixes a :: "'x"
+ and b :: "'x"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ and a1: "\<not>(a\<sharp>x)"
+ and a2: "b\<sharp>x"
+ shows "[(a,b)]\<bullet>x \<noteq> x"
+proof
+ assume neg: "[(a,b)]\<bullet>x = x"
+ from a1 have a1':"a\<in>(supp x)" by (simp add: fresh_def)
+ from a2 have a2':"b\<notin>(supp x)" by (simp add: fresh_def)
+ from a1' a2' have a3: "a\<noteq>b" by force
+ from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))"
+ by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at])
+ hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_append[OF at] at_calc[OF at])
+ hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at])
+ with a2' neg show False by simp
+qed
+
+-- "three helper lemmas for the perm_fresh_fresh-lemma"
+lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
+ by (auto)
+
+lemma infinite_or_neg_infinite:
+ assumes h:"infinite (UNIV::'a set)"
+ shows "infinite {b::'a. P b} \<or> infinite {b::'a. \<not> P b}"
+proof (subst comprehension_neg_UNIV, case_tac "finite {b. P b}")
+ assume j:"finite {b::'a. P b}"
+ have "infinite ((UNIV::'a set) - {b::'a. P b})"
+ using Diff_infinite_finite[OF j h] by auto
+ thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" ..
+next
+ assume j:"infinite {b::'a. P b}"
+ thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" by simp
+qed
+
+--"the co-set of a finite set is infinte"
+lemma finite_infinite:
+ assumes a: "finite {b::'x. P b}"
+ and b: "infinite (UNIV::'x set)"
+ shows "infinite {b. \<not>P b}"
+ using a and infinite_or_neg_infinite[OF b] by simp
+
+lemma pt_fresh_fresh:
+ fixes x :: "'a"
+ and a :: "'x"
+ and b :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ and a1: "a\<sharp>x" and a2: "b\<sharp>x"
+ shows "[(a,b)]\<bullet>x=x"
+proof (cases "a=b")
+ assume c1: "a=b"
+ have "[(a,a)] \<sim> []" by (rule at_ds1[OF at])
+ hence "[(a,b)] \<sim> []" using c1 by simp
+ hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt])
+ thus ?thesis by (simp only: pt1[OF pt])
+next
+ assume c2: "a\<noteq>b"
+ from a1 have f1: "finite {c. [(a,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
+ from a2 have f2: "finite {c. [(b,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
+ from f1 and f2 have f3: "finite {c. perm [(a,c)] x \<noteq> x \<or> perm [(b,c)] x \<noteq> x}"
+ by (force simp only: Collect_disj_eq)
+ have "infinite {c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}"
+ by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
+ hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})"
+ by (force dest: Diff_infinite_finite)
+ hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
+ by (auto iff del: finite_Diff_insert Diff_eq_empty_iff)
+ hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
+ then obtain c
+ where eq1: "[(a,c)]\<bullet>x = x"
+ and eq2: "[(b,c)]\<bullet>x = x"
+ and ineq: "a\<noteq>c \<and> b\<noteq>c"
+ by (force)
+ hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>x)) = x" by simp
+ hence eq3: "[(a,c),(b,c),(a,c)]\<bullet>x = x" by (simp add: pt2[OF pt,symmetric])
+ from c2 ineq have "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]" by (simp add: at_ds3[OF at])
+ hence "[(a,c),(b,c),(a,c)]\<bullet>x = [(a,b)]\<bullet>x" by (rule pt3[OF pt])
+ thus ?thesis using eq3 by simp
+qed
+
+lemma pt_perm_compose:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)"
+proof -
+ have "(pi2@pi1) \<sim> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
+ hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
+ thus ?thesis by (simp add: pt2[OF pt])
+qed
+
+lemma pt_perm_compose_rev:
+ fixes pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(rev pi2)\<bullet>((rev pi1)\<bullet>x) = (rev pi1)\<bullet>(rev (pi1\<bullet>pi2)\<bullet>x)"
+proof -
+ have "((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at])
+ hence "((rev pi2)@(rev pi1))\<bullet>x = ((rev pi1)@(rev (pi1\<bullet>pi2)))\<bullet>x" by (rule pt3[OF pt])
+ thus ?thesis by (simp add: pt2[OF pt])
+qed
+
+section {* facts about supports *}
+(*==============================*)
+
+lemma supports_subset:
+ fixes x :: "'a"
+ and S1 :: "'x set"
+ and S2 :: "'x set"
+ assumes a: "S1 supports x"
+ and b: "S1\<subseteq>S2"
+ shows "S2 supports x"
+ using a b
+ by (force simp add: "op supports_def")
+
+lemma supp_supports:
+ fixes x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ shows "((supp x)::'x set) supports x"
+proof (unfold "op supports_def", intro strip)
+ fix a b
+ assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
+ hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
+ thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at])
+qed
+
+lemma supp_is_subset:
+ fixes S :: "'x set"
+ and x :: "'a"
+ assumes a1: "S supports x"
+ and a2: "finite S"
+ shows "(supp x)\<subseteq>S"
+proof (rule ccontr)
+ assume "\<not>(supp x \<subseteq> S)"
+ hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
+ then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
+ from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold "op supports_def", force)
+ with a1 have "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by (unfold "op supports_def", force)
+ with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
+ hence "a\<notin>(supp x)" by (unfold supp_def, auto)
+ with b1 show False by simp
+qed
+
+lemma supports_finite:
+ fixes S :: "'x set"
+ and x :: "'a"
+ assumes a1: "S supports x"
+ and a2: "finite S"
+ shows "finite ((supp x)::'x set)"
+proof -
+ have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
+ thus ?thesis using a2 by (simp add: finite_subset)
+qed
+
+lemma supp_is_inter:
+ fixes x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ and fs: "fs TYPE('a) TYPE('x)"
+ shows "((supp x)::'x set) = (\<Inter> {S. finite S \<and> S supports x})"
+proof (rule equalityI)
+ show "((supp x)::'x set) \<subseteq> (\<Inter> {S. finite S \<and> S supports x})"
+ proof (clarify)
+ fix S c
+ assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
+ hence "((supp x)::'x set)\<subseteq>S" by (simp add: supp_is_subset)
+ with b show "c\<in>S" by force
+ qed
+next
+ show "(\<Inter> {S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
+ proof (clarify, simp)
+ fix c
+ assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
+ have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
+ with d fs1[OF fs] show "c\<in>supp x" by force
+ qed
+qed
+
+lemma supp_is_least_supports:
+ fixes S :: "'x set"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ and a1: "S supports x"
+ and a2: "finite S"
+ and a3: "\<forall>S'. (finite S' \<and> S' supports x) \<longrightarrow> S\<subseteq>S'"
+ shows "S = (supp x)"
+proof (rule equalityI)
+ show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
+next
+ have s1: "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
+ have "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
+ hence "finite ((supp x)::'x set)" using a2 by (simp add: finite_subset)
+ with s1 a3 show "S\<subseteq>supp x" by force
+qed
+
+lemma supports_set:
+ fixes S :: "'x set"
+ and X :: "'a set"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ and a: "\<forall>x\<in>X. (\<forall>(a::'x) (b::'x). a\<notin>S\<and>b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x)\<in>X)"
+ shows "S supports X"
+using a
+apply(auto simp add: "op supports_def")
+apply(simp add: pt_set_bij1a[OF pt, OF at])
+apply(force simp add: pt_swap_bij[OF pt, OF at])
+apply(simp add: pt_set_bij1a[OF pt, OF at])
+done
+
+lemma supports_fresh:
+ fixes S :: "'x set"
+ and a :: "'x"
+ and x :: "'a"
+ assumes a1: "S supports x"
+ and a2: "finite S"
+ and a3: "a\<notin>S"
+ shows "a\<sharp>x"
+proof (simp add: fresh_def)
+ have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
+ thus "a\<notin>(supp x)" using a3 by force
+qed
+
+lemma at_fin_set_supports:
+ fixes X::"'x set"
+ assumes at: "at TYPE('x)"
+ shows "X supports X"
+proof (simp add: "op supports_def", intro strip)
+ fix a b
+ assume "a\<notin>X \<and> b\<notin>X"
+ thus "[(a,b)]\<bullet>X = X" by (force simp add: perm_set_def at_calc[OF at])
+qed
+
+lemma at_fin_set_supp:
+ fixes X::"'x set"
+ assumes at: "at TYPE('x)"
+ and fs: "finite X"
+ shows "(supp X) = X"
+proof -
+ have pt_set: "pt TYPE('x set) TYPE('x)"
+ by (rule pt_set_inst[OF at_pt_inst[OF at]])
+ have X_supports_X: "X supports X" by (rule at_fin_set_supports[OF at])
+ show ?thesis using pt_set at X_supports_X fs
+ proof (rule supp_is_least_supports[symmetric])
+ show "\<forall>S'. finite S' \<and> S' supports X \<longrightarrow> X \<subseteq> S'"
+ proof (auto)
+ fix S'::"'x set" and x::"'x"
+ assume f: "finite S'"
+ and s: "S' supports X"
+ and e1: "x\<in>X"
+ show "x\<in>S'"
+ proof (rule ccontr)
+ assume e2: "x\<notin>S'"
+ have "\<exists>b. b\<notin>(X\<union>S')" by (force intro: ex_in_inf[OF at] simp only: fs f)
+ then obtain b where b1: "b\<notin>X" and b2: "b\<notin>S'" by (auto)
+ from s e2 b2 have c1: "[(x,b)]\<bullet>X=X" by (simp add: "op supports_def")
+ from e1 b1 have c2: "[(x,b)]\<bullet>X\<noteq>X" by (force simp add: perm_set_def at_calc[OF at])
+ show "False" using c1 c2 by simp
+ qed
+ qed
+ qed
+qed
+
+section {* Permutations acting on Functions *}
+(*==========================================*)
+
+lemma pt_fun_app_eq:
+ fixes f :: "'a\<Rightarrow>'b"
+ and x :: "'a"
+ and pi :: "'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)"
+ by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at])
+
+
+--"sometimes pt_fun_app_eq does to much; this lemma 'corrects it'"
+lemma pt_perm:
+ fixes x :: "'a"
+ and pi1 :: "'x prm"
+ and pi2 :: "'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ shows "(pi1\<bullet>perm pi2)(pi1\<bullet>x) = pi1\<bullet>(pi2\<bullet>x)"
+ by (simp add: pt_fun_app_eq[OF pt, OF at])
+
+
+lemma pt_fun_eq:
+ fixes f :: "'a\<Rightarrow>'b"
+ and pi :: "'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi\<bullet>f = f) = (\<forall> x. pi\<bullet>(f x) = f (pi\<bullet>x))" (is "?LHS = ?RHS")
+proof
+ assume a: "?LHS"
+ show "?RHS"
+ proof
+ fix x
+ have "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pt, OF at])
+ also have "\<dots> = f (pi\<bullet>x)" using a by simp
+ finally show "pi\<bullet>(f x) = f (pi\<bullet>x)" by simp
+ qed
+next
+ assume b: "?RHS"
+ show "?LHS"
+ proof (rule ccontr)
+ assume "(pi\<bullet>f) \<noteq> f"
+ hence "\<exists>c. (pi\<bullet>f) c \<noteq> f c" by (simp add: expand_fun_eq)
+ then obtain c where b1: "(pi\<bullet>f) c \<noteq> f c" by force
+ from b have "pi\<bullet>(f ((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" by force
+ hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))"
+ by (simp add: pt_fun_app_eq[OF pt, OF at])
+ hence "(pi\<bullet>f) c = f c" by (simp add: pt_pi_rev[OF pt, OF at])
+ with b1 show "False" by simp
+ qed
+qed
+
+-- "two helper lemmas for the equivariance of functions"
+lemma pt_swap_eq_aux:
+ fixes y :: "'a"
+ and pi :: "'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and a: "\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y"
+ shows "pi\<bullet>y = y"
+proof(induct pi)
+ case Nil show ?case by (simp add: pt1[OF pt])
+ next
+ case (Cons x xs)
+ have "\<exists>a b. x=(a,b)" by force
+ then obtain a b where p: "x=(a,b)" by force
+ assume i: "xs\<bullet>y = y"
+ have "x#xs = [x]@xs" by simp
+ hence "(x#xs)\<bullet>y = ([x]@xs)\<bullet>y" by simp
+ hence "(x#xs)\<bullet>y = [x]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
+ thus ?case using a i p by (force)
+ qed
+
+lemma pt_swap_eq:
+ fixes y :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ shows "(\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y) = (\<forall>pi::'x prm. pi\<bullet>y = y)"
+ by (force intro: pt_swap_eq_aux[OF pt])
+
+lemma pt_eqvt_fun1a:
+ fixes f :: "'a\<Rightarrow>'b"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('b) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a: "((supp f)::'x set)={}"
+ shows "\<forall>(pi::'x prm). pi\<bullet>f = f"
+proof (intro strip)
+ fix pi
+ have "\<forall>a b. a\<notin>((supp f)::'x set) \<and> b\<notin>((supp f)::'x set) \<longrightarrow> (([(a,b)]\<bullet>f) = f)"
+ by (intro strip, fold fresh_def,
+ simp add: pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at],OF at])
+ with a have "\<forall>(a::'x) (b::'x). ([(a,b)]\<bullet>f) = f" by force
+ hence "\<forall>(pi::'x prm). pi\<bullet>f = f"
+ by (simp add: pt_swap_eq[OF pt_fun_inst[OF pta, OF ptb, OF at]])
+ thus "(pi::'x prm)\<bullet>f = f" by simp
+qed
+
+lemma pt_eqvt_fun1b:
+ fixes f :: "'a\<Rightarrow>'b"
+ assumes a: "\<forall>(pi::'x prm). pi\<bullet>f = f"
+ shows "((supp f)::'x set)={}"
+using a by (simp add: supp_def)
+
+lemma pt_eqvt_fun1:
+ fixes f :: "'a\<Rightarrow>'b"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('b) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm). pi\<bullet>f = f)" (is "?LHS = ?RHS")
+by (rule iffI, simp add: pt_eqvt_fun1a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun1b)
+
+lemma pt_eqvt_fun2a:
+ fixes f :: "'a\<Rightarrow>'b"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('b) TYPE('x)"
+ and at: "at TYPE('x)"
+ assumes a: "((supp f)::'x set)={}"
+ shows "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)"
+proof (intro strip)
+ fix pi x
+ from a have b: "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_eqvt_fun1[OF pta, OF ptb, OF at])
+ have "(pi::'x prm)\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pta, OF at])
+ with b show "(pi::'x prm)\<bullet>(f x) = f (pi\<bullet>x)" by force
+qed
+
+lemma pt_eqvt_fun2b:
+ fixes f :: "'a\<Rightarrow>'b"
+ assumes pt1: "pt TYPE('a) TYPE('x)"
+ and pt2: "pt TYPE('b) TYPE('x)"
+ and at: "at TYPE('x)"
+ assumes a: "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)"
+ shows "((supp f)::'x set)={}"
+proof -
+ from a have "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_fun_eq[OF pt1, OF at, symmetric])
+ thus ?thesis by (simp add: supp_def)
+qed
+
+lemma pt_eqvt_fun2:
+ fixes f :: "'a\<Rightarrow>'b"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('b) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x))"
+by (rule iffI,
+ simp add: pt_eqvt_fun2a[OF pta, OF ptb, OF at],
+ simp add: pt_eqvt_fun2b[OF pta, OF ptb, OF at])
+
+lemma pt_supp_fun_subset:
+ fixes f :: "'a\<Rightarrow>'b"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('b) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f1: "finite ((supp f)::'x set)"
+ and f2: "finite ((supp x)::'x set)"
+ shows "supp (f x) \<subseteq> (((supp f)\<union>(supp x))::'x set)"
+proof -
+ have s1: "((supp f)\<union>((supp x)::'x set)) supports (f x)"
+ proof (simp add: "op supports_def", fold fresh_def, auto)
+ fix a::"'x" and b::"'x"
+ assume "a\<sharp>f" and "b\<sharp>f"
+ hence a1: "[(a,b)]\<bullet>f = f"
+ by (rule pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at], OF at])
+ assume "a\<sharp>x" and "b\<sharp>x"
+ hence a2: "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pta, OF at])
+ from a1 a2 show "[(a,b)]\<bullet>(f x) = (f x)" by (simp add: pt_fun_app_eq[OF pta, OF at])
+ qed
+ from f1 f2 have "finite ((supp f)\<union>((supp x)::'x set))" by force
+ with s1 show ?thesis by (rule supp_is_subset)
+qed
+
+lemma pt_empty_supp_fun_subset:
+ fixes f :: "'a\<Rightarrow>'b"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('b) TYPE('x)"
+ and at: "at TYPE('x)"
+ and e: "(supp f)=({}::'x set)"
+ shows "supp (f x) \<subseteq> ((supp x)::'x set)"
+proof (unfold supp_def, auto)
+ fix a::"'x"
+ assume a1: "finite {b. [(a, b)]\<bullet>x \<noteq> x}"
+ assume "infinite {b. [(a, b)]\<bullet>(f x) \<noteq> f x}"
+ hence a2: "infinite {b. f ([(a, b)]\<bullet>x) \<noteq> f x}" using e
+ by (simp add: pt_eqvt_fun2[OF pta, OF ptb, OF at])
+ have a3: "{b. f ([(a,b)]\<bullet>x) \<noteq> f x}\<subseteq>{b. [(a,b)]\<bullet>x \<noteq> x}" by force
+ from a1 a2 a3 show False by (force dest: finite_subset)
+qed
+
+section {* Andy's freshness lemma *}
+(*================================*)
+
+lemma freshness_lemma:
+ fixes h :: "'x\<Rightarrow>'a"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f1: "finite ((supp h)::'x set)"
+ and a: "\<exists>a::'x. (a\<sharp>h \<and> a\<sharp>(h a))"
+ shows "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> (h a) = fr"
+proof -
+ have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at])
+ have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at])
+ from a obtain a0 where a1: "a0\<sharp>h" and a2: "a0\<sharp>(h a0)" by force
+ show ?thesis
+ proof
+ let ?fr = "h (a0::'x)"
+ show "\<forall>(a::'x). (a\<sharp>h \<longrightarrow> ((h a) = ?fr))"
+ proof (intro strip)
+ fix a
+ assume a3: "(a::'x)\<sharp>h"
+ show "h (a::'x) = h a0"
+ proof (cases "a=a0")
+ case True thus "h (a::'x) = h a0" by simp
+ next
+ case False
+ assume "a\<noteq>a0"
+ hence c1: "a\<notin>((supp a0)::'x set)" by (simp add: fresh_def[symmetric] at_fresh[OF at])
+ have c2: "a\<notin>((supp h)::'x set)" using a3 by (simp add: fresh_def)
+ from c1 c2 have c3: "a\<notin>((supp h)\<union>((supp a0)::'x set))" by force
+ have f2: "finite ((supp a0)::'x set)" by (simp add: at_supp[OF at])
+ from f1 f2 have "((supp (h a0))::'x set)\<subseteq>((supp h)\<union>(supp a0))"
+ by (simp add: pt_supp_fun_subset[OF ptb, OF pta, OF at])
+ hence "a\<notin>((supp (h a0))::'x set)" using c3 by force
+ hence "a\<sharp>(h a0)" by (simp add: fresh_def)
+ with a2 have d1: "[(a0,a)]\<bullet>(h a0) = (h a0)" by (rule pt_fresh_fresh[OF pta, OF at])
+ from a1 a3 have d2: "[(a0,a)]\<bullet>h = h" by (rule pt_fresh_fresh[OF ptc, OF at])
+ from d1 have "h a0 = [(a0,a)]\<bullet>(h a0)" by simp
+ also have "\<dots>= ([(a0,a)]\<bullet>h)([(a0,a)]\<bullet>a0)" by (simp add: pt_fun_app_eq[OF ptb, OF at])
+ also have "\<dots> = h ([(a0,a)]\<bullet>a0)" using d2 by simp
+ also have "\<dots> = h a" by (simp add: at_calc[OF at])
+ finally show "h a = h a0" by simp
+ qed
+ qed
+ qed
+qed
+
+lemma freshness_lemma_unique:
+ fixes h :: "'x\<Rightarrow>'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f1: "finite ((supp h)::'x set)"
+ and a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+ shows "\<exists>!(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr"
+proof
+ from pt at f1 a show "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr" by (simp add: freshness_lemma)
+next
+ fix fr1 fr2
+ assume b1: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr1"
+ assume b2: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr2"
+ from a obtain a where "(a::'x)\<sharp>h" by force
+ with b1 b2 have "h a = fr1 \<and> h a = fr2" by force
+ thus "fr1 = fr2" by force
+qed
+
+-- "packaging the freshness lemma into a function"
+constdefs
+ fresh_fun :: "('x\<Rightarrow>'a)\<Rightarrow>'a"
+ "fresh_fun (h) \<equiv> THE fr. (\<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr)"
+
+lemma fresh_fun_app:
+ fixes h :: "'x\<Rightarrow>'a"
+ and a :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f1: "finite ((supp h)::'x set)"
+ and a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+ and b: "a\<sharp>h"
+ shows "(fresh_fun h) = (h a)"
+proof (unfold fresh_fun_def, rule the_equality)
+ show "\<forall>(a'::'x). a'\<sharp>h \<longrightarrow> h a' = h a"
+ proof (intro strip)
+ fix a'::"'x"
+ assume c: "a'\<sharp>h"
+ from pt at f1 a have "\<exists>(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr" by (rule freshness_lemma)
+ with b c show "h a' = h a" by force
+ qed
+next
+ fix fr::"'a"
+ assume "\<forall>a. a\<sharp>h \<longrightarrow> h a = fr"
+ with b show "fr = h a" by force
+qed
+
+
+lemma fresh_fun_supports:
+ fixes h :: "'x\<Rightarrow>'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f1: "finite ((supp h)::'x set)"
+ and a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+ shows "((supp h)::'x set) supports (fresh_fun h)"
+ apply(simp add: "op supports_def")
+ apply(fold fresh_def)
+ apply(auto)
+ apply(subgoal_tac "\<exists>(a''::'x). a''\<sharp>(h,a,b)")(*A*)
+ apply(erule exE)
+ apply(simp add: fresh_prod)
+ apply(auto)
+ apply(rotate_tac 2)
+ apply(drule fresh_fun_app[OF pt, OF at, OF f1, OF a])
+ apply(simp add: at_fresh[OF at])
+ apply(simp add: pt_fun_app_eq[OF at_pt_inst[OF at], OF at])
+ apply(auto simp add: at_calc[OF at])
+ apply(subgoal_tac "[(a, b)]\<bullet>h = h")(*B*)
+ apply(simp)
+ (*B*)
+ apply(rule pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
+ apply(assumption)+
+ (*A*)
+ apply(rule at_exists_fresh[OF at])
+ apply(simp add: supp_prod)
+ apply(simp add: f1 at_supp[OF at])
+ done
+
+lemma fresh_fun_equiv:
+ fixes h :: "'x\<Rightarrow>'a"
+ and pi:: "'x prm"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f1: "finite ((supp h)::'x set)"
+ and a1: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
+ shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
+proof -
+ have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at])
+ have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at])
+ have f2: "finite ((supp (pi\<bullet>h))::'x set)"
+ proof -
+ from f1 have "finite (pi\<bullet>((supp h)::'x set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at])
+ thus ?thesis by (simp add: pt_perm_supp[OF ptc, OF at])
+ qed
+ from a1 obtain a' where c0: "a'\<sharp>h \<and> a'\<sharp>(h a')" by force
+ hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by simp_all
+ have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1 by (simp add: pt_fresh_bij[OF ptc, OF at])
+ have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
+ proof -
+ from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))" by (simp add: pt_fresh_bij[OF pta, OF at])
+ thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
+ qed
+ have a2: "\<exists>(a::'x). (a\<sharp>(pi\<bullet>h) \<and> a\<sharp>((pi\<bullet>h) a))" using c3 c4 by force
+ have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF pta, OF at, OF f1])
+ have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2])
+ show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
+qed
+
+section {* disjointness properties *}
+(*=================================*)
+lemma dj_perm_forget:
+ fixes pi::"'y prm"
+ and x ::"'x"
+ assumes dj: "disjoint TYPE('x) TYPE('y)"
+ shows "pi\<bullet>x=x"
+ using dj by (simp add: disjoint_def)
+
+lemma dj_perm_perm_forget:
+ fixes pi1::"'x prm"
+ and pi2::"'y prm"
+ assumes dj: "disjoint TYPE('x) TYPE('y)"
+ shows "pi2\<bullet>pi1=pi1"
+ using dj by (induct pi1, auto simp add: disjoint_def)
+
+lemma dj_cp:
+ fixes pi1::"'x prm"
+ and pi2::"'y prm"
+ and x ::"'a"
+ assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ and dj: "disjoint TYPE('y) TYPE('x)"
+ shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
+ by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
+
+lemma dj_supp:
+ fixes a::"'x"
+ assumes dj: "disjoint TYPE('x) TYPE('y)"
+ shows "(supp a) = ({}::'y set)"
+apply(simp add: supp_def dj_perm_forget[OF dj])
+done
+
+
+section {* composition instances *}
+(* ============================= *)
+
+lemma cp_list_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(induct_tac x)
+apply(auto)
+done
+
+lemma cp_set_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(auto simp add: perm_set_def)
+apply(rule_tac x="pi2\<bullet>aa" in exI)
+apply(auto)
+done
+
+lemma cp_option_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(case_tac x)
+apply(auto)
+done
+
+lemma cp_noption_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a nOption) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(case_tac x)
+apply(auto)
+done
+
+lemma cp_unit_inst:
+ shows "cp TYPE (unit) TYPE('x) TYPE('y)"
+apply(simp add: cp_def)
+done
+
+lemma cp_bool_inst:
+ shows "cp TYPE (bool) TYPE('x) TYPE('y)"
+apply(simp add: cp_def)
+apply(rule allI)+
+apply(induct_tac x)
+apply(simp_all)
+done
+
+lemma cp_prod_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ and c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
+using c1 c2
+apply(simp add: cp_def)
+done
+
+lemma cp_fun_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ and c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
+ and pt: "pt TYPE ('y) TYPE('x)"
+ and at: "at TYPE ('x)"
+ shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
+using c1 c2
+apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
+apply(simp add: perm_rev[symmetric])
+apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
+done
+
+
+section {* Abstraction function *}
+(*==============================*)
+
+lemma pt_abs_fun_inst:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pt TYPE('x\<Rightarrow>('a nOption)) TYPE('x)"
+ by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at])
+
+constdefs
+ abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a nOption))" ("[_]._" [100,100] 100)
+ "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))"
+
+lemma abs_fun_if:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and y :: "'a"
+ and c :: "bool"
+ shows "pi\<bullet>(if c then x else y) = (if c then (pi\<bullet>x) else (pi\<bullet>y))"
+ by force
+
+lemma abs_fun_pi_ineq:
+ fixes a :: "'y"
+ and x :: "'a"
+ and pi :: "'x prm"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
+ apply(simp add: abs_fun_def perm_fun_def abs_fun_if)
+ apply(simp only: expand_fun_eq)
+ apply(rule allI)
+ apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*)
+ apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>x))")(*B*)
+ apply(subgoal_tac "pi\<bullet>([(a,(rev pi)\<bullet>xa)]\<bullet>x) = [(pi\<bullet>a,xa)]\<bullet>(pi\<bullet>x)")(*C*)
+ apply(simp)
+(*C*)
+ apply(simp add: cp1[OF cp])
+ apply(simp add: pt_pi_rev[OF ptb, OF at])
+(*B*)
+ apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+(*A*)
+ apply(rule iffI)
+ apply(rule pt_bij2[OF ptb, OF at, THEN sym])
+ apply(simp)
+ apply(rule pt_bij2[OF ptb, OF at])
+ apply(simp)
+done
+
+lemma abs_fun_pi:
+ fixes a :: "'x"
+ and x :: "'a"
+ and pi :: "'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
+apply(rule abs_fun_pi_ineq)
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
+
+lemma abs_fun_eq1:
+ fixes x :: "'a"
+ and y :: "'a"
+ and a :: "'x"
+ shows "([a].x = [a].y) = (x = y)"
+apply(auto simp add: abs_fun_def)
+apply(auto simp add: expand_fun_eq)
+apply(drule_tac x="a" in spec)
+apply(simp)
+done
+
+lemma abs_fun_eq2:
+ fixes x :: "'a"
+ and y :: "'a"
+ and a :: "'x"
+ and b :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a1: "a\<noteq>b"
+ and a2: "[a].x = [b].y"
+ shows "x=[(a,b)]\<bullet>y\<and>a\<sharp>y"
+proof -
+ from a2 have a3:
+ "\<forall>c::'x. (if c=a then nSome(x) else (if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone))
+ = (if c=b then nSome(y) else (if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone))"
+ (is "\<forall>c::'x. ?P c = ?Q c")
+ by (force simp add: abs_fun_def expand_fun_eq)
+ from a3 have "?P a = ?Q a" by (blast)
+ hence a4: "nSome(x) = ?Q a" by simp
+ from a3 have "?P b = ?Q b" by (blast)
+ hence a5: "nSome(y) = ?P b" by simp
+ show ?thesis using a4 a5
+ proof (cases "a\<sharp>y")
+ assume a6: "a\<sharp>y"
+ hence a7: "x = [(b,a)]\<bullet>y" using a4 a1 by simp
+ have "[(a,b)]\<bullet>y = [(b,a)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at])
+ thus ?thesis using a6 a7 by simp
+ next
+ assume "\<not>a\<sharp>y"
+ hence "nSome(x) = nNone" using a1 a4 by simp
+ hence False by force
+ thus ?thesis by force
+ qed
+qed
+
+lemma abs_fun_eq3:
+ fixes x :: "'a"
+ and y :: "'a"
+ and a :: "'x"
+ and b :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and a1: "a\<noteq>b"
+ and a2: "x=[(a,b)]\<bullet>y"
+ and a3: "a\<sharp>y"
+ shows "[a].x =[b].y"
+proof -
+ show ?thesis using a1 a2 a3
+ apply(auto simp add: abs_fun_def)
+ apply(simp only: expand_fun_eq)
+ apply(rule allI)
+ apply(case_tac "x=a")
+ apply(simp)
+ apply(rule pt3[OF pt], rule at_ds5[OF at])
+ apply(case_tac "x=b")
+ apply(simp add: pt_swap_bij[OF pt, OF at])
+ apply(simp add: at_calc[OF at] at_bij[OF at] pt_fresh_left[OF pt, OF at])
+ apply(simp only: if_False)
+ apply(simp add: at_calc[OF at] at_bij[OF at] pt_fresh_left[OF pt, OF at])
+ apply(rule impI)
+ apply(subgoal_tac "[(a,x)]\<bullet>([(a,b)]\<bullet>y) = [(b,x)]\<bullet>([(a,x)]\<bullet>y)")(*A*)
+ apply(simp)
+ apply(simp only: pt_bij[OF pt, OF at])
+ apply(rule pt_fresh_fresh[OF pt, OF at])
+ apply(assumption)+
+ (*A*)
+ apply(simp only: pt2[OF pt, symmetric])
+ apply(rule pt3[OF pt])
+ apply(simp, rule at_ds6[OF at])
+ apply(force)
+ done
+ qed
+
+lemma abs_fun_eq:
+ fixes x :: "'a"
+ and y :: "'a"
+ and a :: "'x"
+ and b :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y))"
+proof (rule iffI)
+ assume b: "[a].x = [b].y"
+ show "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)"
+ proof (cases "a=b")
+ case True with b show ?thesis by (simp add: abs_fun_eq1)
+ next
+ case False with b show ?thesis by (simp add: abs_fun_eq2[OF pt, OF at])
+ qed
+next
+ assume "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)"
+ thus "[a].x = [b].y"
+ proof
+ assume "a=b \<and> x=y" thus ?thesis by simp
+ next
+ assume "a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
+ thus ?thesis by (simp add: abs_fun_eq3[OF pt, OF at])
+ qed
+qed
+
+-- "two helpers for the abst_supp_approx-lemma"
+lemma finite_minus:
+ assumes a: "finite {b. P b}"
+ shows "finite {b. b \<noteq> x \<and> P b}"
+ using a by (force simp add: Collect_conj_eq)
+
+lemma infinite_minus:
+ assumes a: "infinite {b. P b}"
+ shows "infinite {b. b \<noteq> x \<and> P b}"
+proof -
+ have "{b. b \<noteq> x \<and> P b}={b. P b}-{x}" by force
+ with a show ?thesis by force
+qed
+
+lemma abs_fun_supp_approx:
+ fixes x :: "'a"
+ and a :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "((supp ([a].x))::'x set) \<subseteq> (supp x)\<union>{a}"
+proof (unfold supp_def, auto simp only: abs_fun_pi[OF pt, OF at] at_calc[OF at] if_False)
+ fix c
+ assume a: "c\<noteq>a"
+ assume "finite {b::'x. [(c, b)]\<bullet>x \<noteq> x}"
+ hence f: "finite {b::'x. b\<noteq>a \<and> [(c, b)]\<bullet>x \<noteq> x}" by (rule finite_minus)
+ assume "infinite {b::'x. [(if (b=a) then c else a)].([(c,b)]\<bullet>x) \<noteq> ([a].x)}"
+ hence "infinite {b::'x. b\<noteq>a \<and> [(if (b=a) then c else a)].([(c,b)]\<bullet>x) \<noteq> ([a].x)}"
+ by (rule infinite_minus)
+ hence i: "infinite {b::'x. b\<noteq>a \<and> [a].([(c,b)]\<bullet>x) \<noteq> ([a].x)}"
+ proof (auto split add: split_if_asm)
+ assume c1: "infinite {b::'x. b\<noteq>a \<and> (b=a \<or> b\<noteq>a \<and> [a].([(c,b)]\<bullet>x) \<noteq> ([a].x))}"
+ assume c2: "finite {b::'x. b\<noteq>a \<and> [a].([(c, b)]\<bullet>x) \<noteq> ([a].x)}"
+ have "{b::'x. b\<noteq>a \<and> (b=a \<or> b\<noteq>a \<and> [a].([(c,b)]\<bullet>x) \<noteq> ([a].x))} =
+ {b::'x. b\<noteq>a \<and> [a].([(c,b)]\<bullet>x) \<noteq> ([a].x)}" by force
+ with c1 c2 show False by simp
+ qed
+ from f i show False by (simp add: abs_fun_eq1)
+qed
+
+lemma abs_fun_finite_supp:
+ fixes x :: "'a"
+ and a :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f: "finite ((supp x)::'x set)"
+ shows "finite ((supp ([a].x))::'x set)"
+proof -
+ from f have f1: "finite (((supp x)::'x set)\<union>{a})" by force
+ thus ?thesis using abs_fun_supp_approx[OF pt, OF at, of "a" "x"]
+ by (simp add: finite_subset)
+qed
+
+lemma fresh_abs_funI1:
+ fixes x :: "'a"
+ and a :: "'x"
+ and b :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f: "finite ((supp x)::'x set)"
+ and a1: "b\<sharp>x"
+ and a2: "a\<noteq>b"
+ shows "b\<sharp>([a].x)"
+ proof -
+ have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)"
+ proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
+ show "finite ((supp ([a].x))::'x set)" using f
+ by (simp add: abs_fun_finite_supp[OF pt, OF at])
+ qed
+ then obtain c where fr1: "c\<noteq>b"
+ and fr2: "c\<noteq>a"
+ and fr3: "c\<sharp>x"
+ and fr4: "c\<sharp>([a].x)"
+ by (force simp add: fresh_prod at_fresh[OF at])
+ have e: "[(c,b)]\<bullet>([a].x) = [a].([(c,b)]\<bullet>x)" using a2 fr1 fr2
+ by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
+ from fr4 have "([(c,b)]\<bullet>c)\<sharp> ([(c,b)]\<bullet>([a].x))"
+ by (simp add: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
+ hence "b\<sharp>([a].([(c,b)]\<bullet>x))" using fr1 fr2 e
+ by (simp add: at_calc[OF at])
+ thus ?thesis using a1 fr3
+ by (simp add: pt_fresh_fresh[OF pt, OF at])
+qed
+
+lemma fresh_abs_funE:
+ fixes a :: "'x"
+ and b :: "'x"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f: "finite ((supp x)::'x set)"
+ and a1: "b\<sharp>([a].x)"
+ and a2: "b\<noteq>a"
+ shows "b\<sharp>x"
+proof -
+ have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)"
+ proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
+ show "finite ((supp ([a].x))::'x set)" using f
+ by (simp add: abs_fun_finite_supp[OF pt, OF at])
+ qed
+ then obtain c where fr1: "b\<noteq>c"
+ and fr2: "c\<noteq>a"
+ and fr3: "c\<sharp>x"
+ and fr4: "c\<sharp>([a].x)" by (force simp add: fresh_prod at_fresh[OF at])
+ have "[a].x = [(b,c)]\<bullet>([a].x)" using a1 fr4
+ by (simp add: pt_fresh_fresh[OF pt_abs_fun_inst[OF pt, OF at], OF at])
+ hence "[a].x = [a].([(b,c)]\<bullet>x)" using fr2 a2
+ by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
+ hence b: "([(b,c)]\<bullet>x) = x" by (simp add: abs_fun_eq1)
+ from fr3 have "([(b,c)]\<bullet>c)\<sharp>([(b,c)]\<bullet>x)"
+ by (simp add: pt_fresh_bij[OF pt, OF at])
+ thus ?thesis using b fr1 by (simp add: at_calc[OF at])
+qed
+
+lemma fresh_abs_funI2:
+ fixes a :: "'x"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f: "finite ((supp x)::'x set)"
+ shows "a\<sharp>([a].x)"
+proof -
+ have "\<exists>c::'x. c\<sharp>(a,x)"
+ by (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
+ then obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a"
+ and fr2: "c\<sharp>x" by (force simp add: fresh_prod at_fresh[OF at])
+ have "c\<sharp>([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at])
+ hence "([(c,a)]\<bullet>c)\<sharp>([(c,a)]\<bullet>([a].x))" using fr1
+ by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
+ hence a: "a\<sharp>([c].([(c,a)]\<bullet>x))" using fr1_sym
+ by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
+ have "[c].([(c,a)]\<bullet>x) = ([a].x)" using fr1_sym fr2
+ by (simp add: abs_fun_eq[OF pt, OF at])
+ thus ?thesis using a by simp
+qed
+
+lemma fresh_abs_fun_iff:
+ fixes a :: "'x"
+ and b :: "'x"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f: "finite ((supp x)::'x set)"
+ shows "(b\<sharp>([a].x)) = (b=a \<or> b\<sharp>x)"
+ by (auto dest: fresh_abs_funE[OF pt, OF at,OF f]
+ intro: fresh_abs_funI1[OF pt, OF at,OF f]
+ fresh_abs_funI2[OF pt, OF at,OF f])
+
+lemma abs_fun_supp:
+ fixes a :: "'x"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ and f: "finite ((supp x)::'x set)"
+ shows "supp ([a].x) = (supp x)-{a}"
+ by (force simp add: supp_fresh_iff fresh_abs_fun_iff[OF pt, OF at, OF f])
+
+(* maybe needs to be stated by supp -supp *)
+
+lemma abs_fun_supp_ineq:
+ fixes a :: "'y"
+ and x :: "'a"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ and dj: "disjoint TYPE('y) TYPE('x)"
+ shows "((supp ([a].x))::'x set) = (supp x)"
+apply(auto simp add: supp_def)
+apply(auto simp add: abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(auto simp add: dj_perm_forget[OF dj])
+apply(auto simp add: abs_fun_eq1)
+done
+
+lemma fresh_abs_fun_iff_ineq:
+ fixes a :: "'y"
+ and b :: "'x"
+ and x :: "'a"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ and dj: "disjoint TYPE('y) TYPE('x)"
+ shows "b\<sharp>([a].x) = b\<sharp>x"
+ by (simp add: fresh_def abs_fun_supp_ineq[OF pta, OF ptb, OF at, OF cp, OF dj])
+
+section {* abstraction type for the datatype package (not really needed anymore) *}
+(*===============================================================================*)
+consts
+ "ABS_set" :: "('x\<Rightarrow>('a nOption)) set"
+inductive ABS_set
+ intros
+ ABS_in: "(abs_fun a x)\<in>ABS_set"
+
+typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a nOption)) set"
+proof
+ fix x::"'a" and a::"'x"
+ show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
+qed
+
+syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
+
+
+section {* Lemmas for Deciding Permutation Equations *}
+(*===================================================*)
+
+lemma perm_eq_app:
+ fixes f :: "'a\<Rightarrow>'b"
+ and x :: "'a"
+ and pi :: "'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi\<bullet>(f x)=y) = ((pi\<bullet>f)(pi\<bullet>x)=y)"
+ by (simp add: pt_fun_app_eq[OF pt, OF at])
+
+lemma perm_eq_lam:
+ fixes f :: "'a\<Rightarrow>'b"
+ and x :: "'a"
+ and pi :: "'x prm"
+ shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)"
+ by (simp add: perm_fun_def)
+
+
+
+(***************************************)
+(* setup for the individial atom-kinds *)
+(* and datatype *)
+use "nominal_package.ML"
+setup "NominalPackage.setup"
+
+(**********************************)
+(* setup for induction principles *)
+use "nominal_induct.ML";
+method_setup nominal_induct =
+ {* nominal_induct_method *}
+ {* nominal induction *}
+
+(*******************************)
+(* permutation equality tactic *)
+use "nominal_permeq.ML";
+method_setup perm_simp =
+ {* perm_eq_meth *}
+ {* tactic for deciding equalities involving permutations *}
+
+method_setup perm_simp_debug =
+ {* perm_eq_meth_debug *}
+ {* tactic for deciding equalities involving permutations including debuging facilities*}
+
+method_setup supports_simp =
+ {* supports_meth *}
+ {* tactic for deciding whether something supports semthing else *}
+
+method_setup supports_simp_debug =
+ {* supports_meth_debug *}
+ {* tactic for deciding equalities involving permutations including debuging facilities*}
+
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/nominal_package.ML Mon Oct 17 12:30:57 2005 +0200
@@ -0,0 +1,1760 @@
+(* $Id$ *)
+
+signature NOMINAL_PACKAGE =
+sig
+ val create_nom_typedecls : string list -> theory -> theory
+ val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix *
+ (bstring * string list * mixfix) list) list -> theory -> theory *
+ {distinct : thm list list,
+ inject : thm list list,
+ exhaustion : thm list,
+ rec_thms : thm list,
+ case_thms : thm list list,
+ split_thms : (thm * thm) list,
+ induction : thm,
+ size : thm list,
+ simps : thm list}
+ val setup : (theory -> theory) list
+end
+
+structure NominalPackage (*: NOMINAL_PACKAGE *) =
+struct
+
+open DatatypeAux;
+
+(* data kind 'HOL/nominal' *)
+
+structure NominalArgs =
+struct
+ val name = "HOL/nominal";
+ type T = unit Symtab.table;
+
+ val empty = Symtab.empty;
+ val copy = I;
+ val extend = I;
+ fun merge _ x = Symtab.merge (K true) x;
+
+ fun print sg tab = ();
+end;
+
+structure NominalData = TheoryDataFun(NominalArgs);
+
+fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));
+
+(* FIXME: add to hologic.ML ? *)
+fun mk_listT T = Type ("List.list", [T]);
+fun mk_permT T = mk_listT (HOLogic.mk_prodT (T, T));
+
+fun mk_Cons x xs =
+ let val T = fastype_of x
+ in Const ("List.list.Cons", T --> mk_listT T --> mk_listT T) $ x $ xs end;
+
+
+(* this function sets up all matters related to atom- *)
+(* kinds; the user specifies a list of atom-kind names *)
+(* atom_decl <ak1> ... <akn> *)
+fun create_nom_typedecls ak_names thy =
+ let
+ (* declares a type-decl for every atom-kind: *)
+ (* that is typedecl <ak> *)
+ val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;
+
+ (* produces a list consisting of pairs: *)
+ (* fst component is the atom-kind name *)
+ (* snd component is its type *)
+ val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names;
+ val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names;
+
+ (* adds for every atom-kind an axiom *)
+ (* <ak>_infinite: infinite (UNIV::<ak_type> set) *)
+ val (thy2,inf_axs) = PureThy.add_axioms_i (map (fn (ak_name, T) =>
+ let
+ val name = ak_name ^ "_infinite"
+ val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not
+ (HOLogic.mk_mem (HOLogic.mk_UNIV T,
+ Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))
+ in
+ ((name, axiom), [])
+ end) ak_names_types) thy1;
+
+ (* declares a swapping function for every atom-kind, it is *)
+ (* const swap_<ak> :: <akT> * <akT> => <akT> => <akT> *)
+ (* swap_<ak> (a,b) c = (if a=c then b (else if b=c then a else c)) *)
+ (* overloades then the general swap-function *)
+ val (thy3, swap_eqs) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
+ val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name);
+ val a = Free ("a", T);
+ val b = Free ("b", T);
+ val c = Free ("c", T);
+ val ab = Free ("ab", HOLogic.mk_prodT (T, T))
+ val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
+ val cswap_akname = Const (swap_name, swapT);
+ val cswap = Const ("nominal.swap", swapT)
+
+ val name = "swap_"^ak_name^"_def";
+ val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (cswap_akname $ HOLogic.mk_prod (a,b) $ c,
+ cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
+ val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
+ in
+ thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)]
+ |> (#1 o PureThy.add_defs_i true [((name, def2),[])])
+ |> PrimrecPackage.add_primrec_i "" [(("", def1),[])]
+ end) (thy2, ak_names_types);
+
+ (* declares a permutation function for every atom-kind acting *)
+ (* on such atoms *)
+ (* const <ak>_prm_<ak> :: (<akT> * <akT>)list => akT => akT *)
+ (* <ak>_prm_<ak> [] a = a *)
+ (* <ak>_prm_<ak> (x#xs) a = swap_<ak> x (perm xs a) *)
+ val (thy4, prm_eqs) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
+ val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name)
+ val prmT = mk_permT T --> T --> T;
+ val prm_name = ak_name ^ "_prm_" ^ ak_name;
+ val qu_prm_name = Sign.full_name (sign_of thy) prm_name;
+ val x = Free ("x", HOLogic.mk_prodT (T, T));
+ val xs = Free ("xs", mk_permT T);
+ val a = Free ("a", T) ;
+
+ val cnil = Const ("List.list.Nil", mk_permT T);
+
+ val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (qu_prm_name, prmT) $ cnil $ a, a));
+
+ val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
+ Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
+ in
+ thy |> Theory.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)]
+ |> PrimrecPackage.add_primrec_i "" [(("", def1), []),(("", def2), [])]
+ end) (thy3, ak_names_types);
+
+ (* defines permutation functions for all combinations of atom-kinds; *)
+ (* there are a trivial cases and non-trivial cases *)
+ (* non-trivial case: *)
+ (* <ak>_prm_<ak>_def: perm pi a == <ak>_prm_<ak> pi a *)
+ (* trivial case with <ak> != <ak'> *)
+ (* <ak>_prm<ak'>_def[simp]: perm pi a == a *)
+ (* *)
+ (* the trivial cases are added to the simplifier, while the non- *)
+ (* have their own rules proved below *)
+ val (thy5, perm_defs) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
+ val pi = Free ("pi", mk_permT T);
+ val a = Free ("a", T');
+ val cperm = Const ("nominal.perm", mk_permT T --> T' --> T');
+ val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T --> T' --> T');
+
+ val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
+ val def = Logic.mk_equals
+ (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
+ in
+ thy' |> PureThy.add_defs_i true [((name, def),[])]
+ end) (thy, ak_names_types)) (thy4, ak_names_types);
+
+ (* proves that every atom-kind is an instance of at *)
+ (* lemma at_<ak>_inst: *)
+ (* at TYPE(<ak>) *)
+ val (thy6, prm_cons_thms) =
+ thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
+ let
+ val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
+ val i_type = Type(ak_name_qu,[]);
+ val cat = Const ("nominal.at",(Term.itselfT i_type) --> HOLogic.boolT);
+ val at_type = Logic.mk_type i_type;
+ val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy5
+ [Name "at_def",
+ Name (ak_name ^ "_prm_" ^ ak_name ^ "_def"),
+ Name (ak_name ^ "_prm_" ^ ak_name ^ ".simps"),
+ Name ("swap_" ^ ak_name ^ "_def"),
+ Name ("swap_" ^ ak_name ^ ".simps"),
+ Name (ak_name ^ "_infinite")]
+
+ val name = "at_"^ak_name^ "_inst";
+ val statement = HOLogic.mk_Trueprop (cat $ at_type);
+
+ val proof = fn _ => [auto_tac (claset(),simp_s)];
+
+ in
+ ((name, prove_goalw_cterm [] (cterm_of (sign_of thy5) statement) proof), [])
+ end) ak_names_types);
+
+ (* declares a perm-axclass for every atom-kind *)
+ (* axclass pt_<ak> *)
+ (* pt_<ak>1[simp]: perm [] x = x *)
+ (* pt_<ak>2: perm (pi1@pi2) x = perm pi1 (perm pi2 x) *)
+ (* pt_<ak>3: pi1 ~ pi2 ==> perm pi1 x = perm pi2 x *)
+ val (thy7, pt_ax_classes) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val cl_name = "pt_"^ak_name;
+ val ty = TFree("'a",["HOL.type"]);
+ val x = Free ("x", ty);
+ val pi1 = Free ("pi1", mk_permT T);
+ val pi2 = Free ("pi2", mk_permT T);
+ val cperm = Const ("nominal.perm", mk_permT T --> ty --> ty);
+ val cnil = Const ("List.list.Nil", mk_permT T);
+ val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
+ val cprm_eq = Const ("nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
+ (* nil axiom *)
+ val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (cperm $ cnil $ x, x));
+ (* append axiom *)
+ val axiom2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (cperm $ (cappend $ pi1 $ pi2) $ x, cperm $ pi1 $ (cperm $ pi2 $ x)));
+ (* perm-eq axiom *)
+ val axiom3 = Logic.mk_implies
+ (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
+ in
+ thy |> AxClass.add_axclass_i (cl_name, ["HOL.type"])
+ [((cl_name^"1", axiom1),[Simplifier.simp_add_global]),
+ ((cl_name^"2", axiom2),[]),
+ ((cl_name^"3", axiom3),[])]
+ end) (thy6,ak_names_types);
+
+ (* proves that every pt_<ak>-type together with <ak>-type *)
+ (* instance of pt *)
+ (* lemma pt_<ak>_inst: *)
+ (* pt TYPE('x::pt_<ak>) TYPE(<ak>) *)
+ val (thy8, prm_inst_thms) =
+ thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
+ let
+ val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name);
+ val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);
+ val i_type1 = TFree("'x",[pt_name_qu]);
+ val i_type2 = Type(ak_name_qu,[]);
+ val cpt = Const ("nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
+ val pt_type = Logic.mk_type i_type1;
+ val at_type = Logic.mk_type i_type2;
+ val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy7
+ [Name "pt_def",
+ Name ("pt_" ^ ak_name ^ "1"),
+ Name ("pt_" ^ ak_name ^ "2"),
+ Name ("pt_" ^ ak_name ^ "3")];
+
+ val name = "pt_"^ak_name^ "_inst";
+ val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type);
+
+ val proof = fn _ => [auto_tac (claset(),simp_s)];
+ in
+ ((name, prove_goalw_cterm [] (cterm_of (sign_of thy7) statement) proof), [])
+ end) ak_names_types);
+
+ (* declares an fs-axclass for every atom-kind *)
+ (* axclass fs_<ak> *)
+ (* fs_<ak>1: finite ((supp x)::<ak> set) *)
+ val (thy11, fs_ax_classes) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val cl_name = "fs_"^ak_name;
+ val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val ty = TFree("'a",["HOL.type"]);
+ val x = Free ("x", ty);
+ val csupp = Const ("nominal.supp", ty --> HOLogic.mk_setT T);
+ val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
+
+ val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
+
+ in
+ thy |> AxClass.add_axclass_i (cl_name, [pt_name]) [((cl_name^"1", axiom1),[])]
+ end) (thy8,ak_names_types);
+
+ (* proves that every fs_<ak>-type together with <ak>-type *)
+ (* instance of fs-type *)
+ (* lemma abst_<ak>_inst: *)
+ (* fs TYPE('x::pt_<ak>) TYPE (<ak>) *)
+ val (thy12, fs_inst_thms) =
+ thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
+ let
+ val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name);
+ val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);
+ val i_type1 = TFree("'x",[fs_name_qu]);
+ val i_type2 = Type(ak_name_qu,[]);
+ val cfs = Const ("nominal.fs",
+ (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
+ val fs_type = Logic.mk_type i_type1;
+ val at_type = Logic.mk_type i_type2;
+ val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy11
+ [Name "fs_def",
+ Name ("fs_" ^ ak_name ^ "1")];
+
+ val name = "fs_"^ak_name^ "_inst";
+ val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type);
+
+ val proof = fn _ => [auto_tac (claset(),simp_s)];
+ in
+ ((name, prove_goalw_cterm [] (cterm_of (sign_of thy11) statement) proof), [])
+ end) ak_names_types);
+
+ (* declares for every atom-kind combination an axclass *)
+ (* cp_<ak1>_<ak2> giving a composition property *)
+ (* cp_<ak1>_<ak2>1: pi1 o pi2 o x = (pi1 o pi2) o (pi1 o x) *)
+ val (thy12b,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val cl_name = "cp_"^ak_name^"_"^ak_name';
+ val ty = TFree("'a",["HOL.type"]);
+ val x = Free ("x", ty);
+ val pi1 = Free ("pi1", mk_permT T);
+ val pi2 = Free ("pi2", mk_permT T');
+ val cperm1 = Const ("nominal.perm", mk_permT T --> ty --> ty);
+ val cperm2 = Const ("nominal.perm", mk_permT T' --> ty --> ty);
+ val cperm3 = Const ("nominal.perm", mk_permT T --> mk_permT T' --> mk_permT T');
+
+ val ax1 = HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
+ cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
+ in
+ (fst (AxClass.add_axclass_i (cl_name, ["HOL.type"]) [((cl_name^"1", ax1),[])] thy'),())
+ end)
+ (thy, ak_names_types)) (thy12, ak_names_types)
+
+ (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem; *)
+ (* lemma cp_<ak1>_<ak2>_inst: *)
+ (* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>) *)
+ val (thy12c, cp_thms) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val ak_name_qu = Sign.full_name (sign_of thy') (ak_name);
+ val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
+ val cp_name_qu = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+ val i_type0 = TFree("'a",[cp_name_qu]);
+ val i_type1 = Type(ak_name_qu,[]);
+ val i_type2 = Type(ak_name_qu',[]);
+ val ccp = Const ("nominal.cp",
+ (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
+ (Term.itselfT i_type2)-->HOLogic.boolT);
+ val at_type = Logic.mk_type i_type1;
+ val at_type' = Logic.mk_type i_type2;
+ val cp_type = Logic.mk_type i_type0;
+ val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy' [(Name "cp_def")];
+ val cp1 = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"1"));
+
+ val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
+ val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
+
+ val proof = fn _ => [auto_tac (claset(),simp_s), rtac cp1 1];
+ in
+ thy' |> PureThy.add_thms
+ [((name, prove_goalw_cterm [] (cterm_of (sign_of thy') statement) proof), [])]
+ end)
+ (thy, ak_names_types)) (thy12b, ak_names_types);
+
+ (* proves for every non-trivial <ak>-combination a disjointness *)
+ (* theorem; i.e. <ak1> != <ak2> *)
+ (* lemma ds_<ak1>_<ak2>: *)
+ (* dj TYPE(<ak1>) TYPE(<ak2>) *)
+ val (thy12d, dj_thms) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ (if not (ak_name = ak_name')
+ then
+ let
+ val ak_name_qu = Sign.full_name (sign_of thy') (ak_name);
+ val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
+ val i_type1 = Type(ak_name_qu,[]);
+ val i_type2 = Type(ak_name_qu',[]);
+ val cdj = Const ("nominal.disjoint",
+ (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
+ val at_type = Logic.mk_type i_type1;
+ val at_type' = Logic.mk_type i_type2;
+ val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy'
+ [Name "disjoint_def",
+ Name (ak_name^"_prm_"^ak_name'^"_def"),
+ Name (ak_name'^"_prm_"^ak_name^"_def")];
+
+ val name = "dj_"^ak_name^"_"^ak_name';
+ val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');
+
+ val proof = fn _ => [auto_tac (claset(),simp_s)];
+ in
+ thy' |> PureThy.add_thms
+ [((name, prove_goalw_cterm [] (cterm_of (sign_of thy') statement) proof), []) ]
+ end
+ else
+ (thy',[]))) (* do nothing branch, if ak_name = ak_name' *)
+ (thy, ak_names_types)) (thy12c, ak_names_types);
+
+ (*<<<<<<< pt_<ak> class instances >>>>>>>*)
+ (*=========================================*)
+
+ (* some frequently used theorems *)
+ val pt1 = PureThy.get_thm thy12c (Name "pt1");
+ val pt2 = PureThy.get_thm thy12c (Name "pt2");
+ val pt3 = PureThy.get_thm thy12c (Name "pt3");
+ val at_pt_inst = PureThy.get_thm thy12c (Name "at_pt_inst");
+ val pt_bool_inst = PureThy.get_thm thy12c (Name "pt_bool_inst");
+ val pt_set_inst = PureThy.get_thm thy12c (Name "pt_set_inst");
+ val pt_unit_inst = PureThy.get_thm thy12c (Name "pt_unit_inst");
+ val pt_prod_inst = PureThy.get_thm thy12c (Name "pt_prod_inst");
+ val pt_list_inst = PureThy.get_thm thy12c (Name "pt_list_inst");
+ val pt_optn_inst = PureThy.get_thm thy12c (Name "pt_option_inst");
+ val pt_noptn_inst = PureThy.get_thm thy12c (Name "pt_noption_inst");
+ val pt_fun_inst = PureThy.get_thm thy12c (Name "pt_fun_inst");
+
+ (* for all atom-kind combination shows that *)
+ (* every <ak> is an instance of pt_<ai> *)
+ val (thy13,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ (if ak_name = ak_name'
+ then
+ let
+ val qu_name = Sign.full_name (sign_of thy') ak_name;
+ val qu_class = Sign.full_name (sign_of thy') ("pt_"^ak_name);
+ val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name ^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((at_inst RS at_pt_inst) RS pt1) 1,
+ rtac ((at_inst RS at_pt_inst) RS pt2) 1,
+ rtac ((at_inst RS at_pt_inst) RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy',())
+ end
+ else
+ let
+ val qu_name' = Sign.full_name (sign_of thy') ak_name';
+ val qu_class = Sign.full_name (sign_of thy') ("pt_"^ak_name);
+ val simp_s = HOL_basic_ss addsimps
+ PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")];
+ val proof = EVERY [AxClass.intro_classes_tac [], auto_tac (claset(),simp_s)];
+ in
+ (AxClass.add_inst_arity_i (qu_name',[],[qu_class]) proof thy',())
+ end))
+ (thy, ak_names_types)) (thy12c, ak_names_types);
+
+ (* shows that bool is an instance of pt_<ak> *)
+ (* uses the theorem pt_bool_inst *)
+ val (thy14,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac (pt_bool_inst RS pt1) 1,
+ rtac (pt_bool_inst RS pt2) 1,
+ rtac (pt_bool_inst RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy,())
+ end) (thy13,ak_names_types);
+
+ (* shows that set(pt_<ak>) is an instance of pt_<ak> *)
+ (* unfolds the permutation definition and applies pt_<ak>i *)
+ val (thy15,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((pt_inst RS pt_set_inst) RS pt1) 1,
+ rtac ((pt_inst RS pt_set_inst) RS pt2) 1,
+ rtac ((pt_inst RS pt_set_inst) RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i ("set",[[qu_class]],[qu_class]) proof thy,())
+ end) (thy14,ak_names_types);
+
+ (* shows that unit is an instance of pt_<ak> *)
+ val (thy16,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac (pt_unit_inst RS pt1) 1,
+ rtac (pt_unit_inst RS pt2) 1,
+ rtac (pt_unit_inst RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy,())
+ end) (thy15,ak_names_types);
+
+ (* shows that *(pt_<ak>,pt_<ak>) is an instance of pt_<ak> *)
+ (* uses the theorem pt_prod_inst and pt_<ak>_inst *)
+ val (thy17,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt1) 1,
+ rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt2) 1,
+ rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy,())
+ end) (thy16,ak_names_types);
+
+ (* shows that list(pt_<ak>) is an instance of pt_<ak> *)
+ (* uses the theorem pt_list_inst and pt_<ak>_inst *)
+ val (thy18,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((pt_inst RS pt_list_inst) RS pt1) 1,
+ rtac ((pt_inst RS pt_list_inst) RS pt2) 1,
+ rtac ((pt_inst RS pt_list_inst) RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy,())
+ end) (thy17,ak_names_types);
+
+ (* shows that option(pt_<ak>) is an instance of pt_<ak> *)
+ (* uses the theorem pt_option_inst and pt_<ak>_inst *)
+ val (thy18a,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((pt_inst RS pt_optn_inst) RS pt1) 1,
+ rtac ((pt_inst RS pt_optn_inst) RS pt2) 1,
+ rtac ((pt_inst RS pt_optn_inst) RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i ("Datatype.option",[[qu_class]],[qu_class]) proof thy,())
+ end) (thy18,ak_names_types);
+
+ (* shows that nOption(pt_<ak>) is an instance of pt_<ak> *)
+ (* uses the theorem pt_option_inst and pt_<ak>_inst *)
+ val (thy18b,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((pt_inst RS pt_noptn_inst) RS pt1) 1,
+ rtac ((pt_inst RS pt_noptn_inst) RS pt2) 1,
+ rtac ((pt_inst RS pt_noptn_inst) RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i ("nominal.nOption",[[qu_class]],[qu_class]) proof thy,())
+ end) (thy18a,ak_names_types);
+
+
+ (* shows that fun(pt_<ak>,pt_<ak>) is an instance of pt_<ak> *)
+ (* uses the theorem pt_list_inst and pt_<ak>_inst *)
+ val (thy19,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
+ val at_thm = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
+ val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt1) 1,
+ rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt2) 1,
+ rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt3) 1,
+ atac 1];
+ in
+ (AxClass.add_inst_arity_i ("fun",[[qu_class],[qu_class]],[qu_class]) proof thy,())
+ end) (thy18b,ak_names_types);
+
+ (*<<<<<<< fs_<ak> class instances >>>>>>>*)
+ (*=========================================*)
+ val fs1 = PureThy.get_thm thy19 (Name "fs1");
+ val fs_at_inst = PureThy.get_thm thy19 (Name "fs_at_inst");
+ val fs_unit_inst = PureThy.get_thm thy19 (Name "fs_unit_inst");
+ val fs_bool_inst = PureThy.get_thm thy19 (Name "fs_bool_inst");
+ val fs_prod_inst = PureThy.get_thm thy19 (Name "fs_prod_inst");
+ val fs_list_inst = PureThy.get_thm thy19 (Name "fs_list_inst");
+
+ (* shows that <ak> is an instance of fs_<ak> *)
+ (* uses the theorem at_<ak>_inst *)
+ val (thy20,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_name = Sign.full_name (sign_of thy) ak_name;
+ val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
+ val at_thm = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((at_thm RS fs_at_inst) RS fs1) 1];
+ in
+ (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy,())
+ end) (thy19,ak_names_types);
+
+ (* shows that unit is an instance of fs_<ak> *)
+ (* uses the theorem fs_unit_inst *)
+ val (thy21,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac (fs_unit_inst RS fs1) 1];
+ in
+ (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy,())
+ end) (thy20,ak_names_types);
+
+ (* shows that bool is an instance of fs_<ak> *)
+ (* uses the theorem fs_bool_inst *)
+ val (thy22,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac (fs_bool_inst RS fs1) 1];
+ in
+ (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy,())
+ end) (thy21,ak_names_types);
+
+ (* shows that *(fs_<ak>,fs_<ak>) is an instance of fs_<ak> *)
+ (* uses the theorem fs_prod_inst *)
+ val (thy23,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
+ val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((fs_inst RS (fs_inst RS fs_prod_inst)) RS fs1) 1];
+ in
+ (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy,())
+ end) (thy22,ak_names_types);
+
+ (* shows that list(fs_<ak>) is an instance of fs_<ak> *)
+ (* uses the theorem fs_list_inst *)
+ val (thy24,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
+ val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((fs_inst RS fs_list_inst) RS fs1) 1];
+ in
+ (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy,())
+ end) (thy23,ak_names_types);
+
+ (*<<<<<<< cp_<ak>_<ai> class instances >>>>>>>*)
+ (*==============================================*)
+ val cp1 = PureThy.get_thm thy24 (Name "cp1");
+ val cp_unit_inst = PureThy.get_thm thy24 (Name "cp_unit_inst");
+ val cp_bool_inst = PureThy.get_thm thy24 (Name "cp_bool_inst");
+ val cp_prod_inst = PureThy.get_thm thy24 (Name "cp_prod_inst");
+ val cp_list_inst = PureThy.get_thm thy24 (Name "cp_list_inst");
+ val cp_fun_inst = PureThy.get_thm thy24 (Name "cp_fun_inst");
+ val cp_option_inst = PureThy.get_thm thy24 (Name "cp_option_inst");
+ val cp_noption_inst = PureThy.get_thm thy24 (Name "cp_noption_inst");
+ val pt_perm_compose = PureThy.get_thm thy24 (Name "pt_perm_compose");
+ val dj_pp_forget = PureThy.get_thm thy24 (Name "dj_perm_perm_forget");
+
+ (* shows that <aj> is an instance of cp_<ak>_<ai> *)
+ (* that needs a three-nested loop *)
+ val (thy25,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ foldl_map (fn (thy'', (ak_name'', T'')) =>
+ let
+ val qu_name = Sign.full_name (sign_of thy'') ak_name;
+ val qu_class = Sign.full_name (sign_of thy'') ("cp_"^ak_name'^"_"^ak_name'');
+ val proof =
+ (if (ak_name'=ak_name'') then
+ (let
+ val pt_inst = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
+ val at_inst = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
+ in
+ EVERY [AxClass.intro_classes_tac [],
+ rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
+ end)
+ else
+ (let
+ val dj_inst = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name'));
+ val simp_s = HOL_basic_ss addsimps
+ ((dj_inst RS dj_pp_forget)::
+ (PureThy.get_thmss thy''
+ [Name (ak_name' ^"_prm_"^ak_name^"_def"),
+ Name (ak_name''^"_prm_"^ak_name^"_def")]));
+ in
+ EVERY [AxClass.intro_classes_tac [], simp_tac simp_s 1]
+ end))
+ in
+ (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy'',())
+ end)
+ (thy', ak_names_types)) (thy, ak_names_types)) (thy24, ak_names_types);
+
+ (* shows that unit is an instance of cp_<ak>_<ai> *)
+ (* for every <ak>-combination *)
+ val (thy26,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+ val proof = EVERY [AxClass.intro_classes_tac [],rtac (cp_unit_inst RS cp1) 1];
+ in
+ (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy',())
+ end)
+ (thy, ak_names_types)) (thy25, ak_names_types);
+
+ (* shows that bool is an instance of cp_<ak>_<ai> *)
+ (* for every <ak>-combination *)
+ val (thy27,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+ val proof = EVERY [AxClass.intro_classes_tac [], rtac (cp_bool_inst RS cp1) 1];
+ in
+ (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy',())
+ end)
+ (thy, ak_names_types)) (thy26, ak_names_types);
+
+ (* shows that prod is an instance of cp_<ak>_<ai> *)
+ (* for every <ak>-combination *)
+ val (thy28,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+ val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((cp_inst RS (cp_inst RS cp_prod_inst)) RS cp1) 1];
+ in
+ (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy',())
+ end)
+ (thy, ak_names_types)) (thy27, ak_names_types);
+
+ (* shows that list is an instance of cp_<ak>_<ai> *)
+ (* for every <ak>-combination *)
+ val (thy29,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+ val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((cp_inst RS cp_list_inst) RS cp1) 1];
+ in
+ (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy',())
+ end)
+ (thy, ak_names_types)) (thy28, ak_names_types);
+
+ (* shows that function is an instance of cp_<ak>_<ai> *)
+ (* for every <ak>-combination *)
+ val (thy30,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+ val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
+ val pt_inst = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
+ val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)))) RS cp1) 1];
+ in
+ (AxClass.add_inst_arity_i ("fun",[[qu_class],[qu_class]],[qu_class]) proof thy',())
+ end)
+ (thy, ak_names_types)) (thy29, ak_names_types);
+
+ (* shows that option is an instance of cp_<ak>_<ai> *)
+ (* for every <ak>-combination *)
+ val (thy31,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+ val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((cp_inst RS cp_option_inst) RS cp1) 1];
+ in
+ (AxClass.add_inst_arity_i ("Datatype.option",[[qu_class]],[qu_class]) proof thy',())
+ end)
+ (thy, ak_names_types)) (thy30, ak_names_types);
+
+ (* shows that nOption is an instance of cp_<ak>_<ai> *)
+ (* for every <ak>-combination *)
+ val (thy32,_) = foldl_map (fn (thy, (ak_name, T)) =>
+ foldl_map (fn (thy', (ak_name', T')) =>
+ let
+ val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
+ val cp_inst = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
+ val proof = EVERY [AxClass.intro_classes_tac [],
+ rtac ((cp_inst RS cp_noption_inst) RS cp1) 1];
+ in
+ (AxClass.add_inst_arity_i ("nominal.nOption",[[qu_class]],[qu_class]) proof thy',())
+ end)
+ (thy, ak_names_types)) (thy31, ak_names_types);
+
+ (* abbreviations for some collection of rules *)
+ (*============================================*)
+ val abs_fun_pi = PureThy.get_thm thy32 (Name ("nominal.abs_fun_pi"));
+ val abs_fun_pi_ineq = PureThy.get_thm thy32 (Name ("nominal.abs_fun_pi_ineq"));
+ val abs_fun_eq = PureThy.get_thm thy32 (Name ("nominal.abs_fun_eq"));
+ val dj_perm_forget = PureThy.get_thm thy32 (Name ("nominal.dj_perm_forget"));
+ val dj_pp_forget = PureThy.get_thm thy32 (Name ("nominal.dj_perm_perm_forget"));
+ val fresh_iff = PureThy.get_thm thy32 (Name ("nominal.fresh_abs_fun_iff"));
+ val fresh_iff_ineq = PureThy.get_thm thy32 (Name ("nominal.fresh_abs_fun_iff_ineq"));
+ val abs_fun_supp = PureThy.get_thm thy32 (Name ("nominal.abs_fun_supp"));
+ val abs_fun_supp_ineq = PureThy.get_thm thy32 (Name ("nominal.abs_fun_supp_ineq"));
+ val pt_swap_bij = PureThy.get_thm thy32 (Name ("nominal.pt_swap_bij"));
+ val pt_fresh_fresh = PureThy.get_thm thy32 (Name ("nominal.pt_fresh_fresh"));
+ val pt_bij = PureThy.get_thm thy32 (Name ("nominal.pt_bij"));
+ val pt_perm_compose = PureThy.get_thm thy32 (Name ("nominal.pt_perm_compose"));
+ val perm_eq_app = PureThy.get_thm thy32 (Name ("nominal.perm_eq_app"));
+
+ (* abs_perm collects all lemmas for simplifying a permutation *)
+ (* in front of an abs_fun *)
+ val (thy33,_) =
+ let
+ val name = "abs_perm"
+ val thm_list = Library.flat (map (fn (ak_name, T) =>
+ let
+ val at_inst = PureThy.get_thm thy32 (Name ("at_"^ak_name^"_inst"));
+ val pt_inst = PureThy.get_thm thy32 (Name ("pt_"^ak_name^"_inst"));
+ val thm = [pt_inst, at_inst] MRS abs_fun_pi
+ val thm_list = map (fn (ak_name', T') =>
+ let
+ val cp_inst = PureThy.get_thm thy32 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
+ in
+ [pt_inst, pt_inst, at_inst, cp_inst] MRS abs_fun_pi_ineq
+ end) ak_names_types;
+ in thm::thm_list end) (ak_names_types))
+ in
+ (PureThy.add_thmss [((name, thm_list),[])] thy32)
+ end;
+
+ (* alpha collects all lemmas analysing an equation *)
+ (* between abs_funs *)
+ (*val (thy34,_) =
+ let
+ val name = "alpha"
+ val thm_list = map (fn (ak_name, T) =>
+ let
+ val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
+ val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));
+ in
+ [pt_inst, at_inst] MRS abs_fun_eq
+ end) ak_names_types
+ in
+ (PureThy.add_thmss [((name, thm_list),[])] thy33)
+ end;*)
+
+ val (thy34,_) =
+ let
+ fun inst_pt_at thm ak_name =
+ let
+ val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
+ val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));
+ in
+ [pt_inst, at_inst] MRS thm
+ end
+
+ in
+ thy33
+ |> PureThy.add_thmss [(("alpha", map (inst_pt_at abs_fun_eq) ak_names),[])]
+ |>>> PureThy.add_thmss [(("perm_swap", map (inst_pt_at pt_swap_bij) ak_names),[])]
+ |>>> PureThy.add_thmss [(("perm_fresh_fresh", map (inst_pt_at pt_fresh_fresh) ak_names),[])]
+ |>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])]
+ |>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])]
+ |>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])]
+ end;
+
+ (* perm_dj collects all lemmas that forget an permutation *)
+ (* when it acts on an atom of different type *)
+ val (thy35,_) =
+ let
+ val name = "perm_dj"
+ val thm_list = Library.flat (map (fn (ak_name, T) =>
+ Library.flat (map (fn (ak_name', T') =>
+ if not (ak_name = ak_name')
+ then
+ let
+ val dj_inst = PureThy.get_thm thy34 (Name ("dj_"^ak_name^"_"^ak_name'));
+ in
+ [dj_inst RS dj_perm_forget, dj_inst RS dj_pp_forget]
+ end
+ else []) ak_names_types)) ak_names_types)
+ in
+ (PureThy.add_thmss [((name, thm_list),[])] thy34)
+ end;
+
+ (* abs_fresh collects all lemmas for simplifying a freshness *)
+ (* proposition involving an abs_fun *)
+
+ val (thy36,_) =
+ let
+ val name = "abs_fresh"
+ val thm_list = Library.flat (map (fn (ak_name, T) =>
+ let
+ val at_inst = PureThy.get_thm thy35 (Name ("at_"^ak_name^"_inst"));
+ val pt_inst = PureThy.get_thm thy35 (Name ("pt_"^ak_name^"_inst"));
+ val fs_inst = PureThy.get_thm thy35 (Name ("fs_"^ak_name^"_inst"));
+ val thm = [pt_inst, at_inst, (fs_inst RS fs1)] MRS fresh_iff
+ val thm_list = Library.flat (map (fn (ak_name', T') =>
+ (if (not (ak_name = ak_name'))
+ then
+ let
+ val cp_inst = PureThy.get_thm thy35 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
+ val dj_inst = PureThy.get_thm thy35 (Name ("dj_"^ak_name'^"_"^ak_name));
+ in
+ [[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS fresh_iff_ineq]
+ end
+ else [])) ak_names_types);
+ in thm::thm_list end) (ak_names_types))
+ in
+ (PureThy.add_thmss [((name, thm_list),[])] thy35)
+ end;
+
+ (* abs_supp collects all lemmas for simplifying *)
+ (* support proposition involving an abs_fun *)
+
+ val (thy37,_) =
+ let
+ val name = "abs_supp"
+ val thm_list = Library.flat (map (fn (ak_name, T) =>
+ let
+ val at_inst = PureThy.get_thm thy36 (Name ("at_"^ak_name^"_inst"));
+ val pt_inst = PureThy.get_thm thy36 (Name ("pt_"^ak_name^"_inst"));
+ val fs_inst = PureThy.get_thm thy36 (Name ("fs_"^ak_name^"_inst"));
+ val thm1 = [pt_inst, at_inst, (fs_inst RS fs1)] MRS abs_fun_supp
+ val thm2 = [pt_inst, at_inst] MRS abs_fun_supp
+ val thm_list = Library.flat (map (fn (ak_name', T') =>
+ (if (not (ak_name = ak_name'))
+ then
+ let
+ val cp_inst = PureThy.get_thm thy36 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
+ val dj_inst = PureThy.get_thm thy36 (Name ("dj_"^ak_name'^"_"^ak_name));
+ in
+ [[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS abs_fun_supp_ineq]
+ end
+ else [])) ak_names_types);
+ in thm1::thm2::thm_list end) (ak_names_types))
+ in
+ (PureThy.add_thmss [((name, thm_list),[])] thy36)
+ end;
+
+ in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)
+ (NominalData.get thy11)) thy37
+ end;
+
+
+(* syntax und parsing *)
+structure P = OuterParse and K = OuterKeyword;
+
+val atom_declP =
+ OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
+ (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
+
+val _ = OuterSyntax.add_parsers [atom_declP];
+
+val setup = [NominalData.init];
+
+(*=======================================================================*)
+
+val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
+
+fun read_typ sign ((Ts, sorts), str) =
+ let
+ val T = Type.no_tvars (Sign.read_typ (sign, (AList.lookup op =)
+ (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
+ in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
+
+(** taken from HOL/Tools/datatype_aux.ML **)
+
+fun indtac indrule indnames i st =
+ let
+ val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
+ val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
+ (Logic.strip_imp_concl (List.nth (prems_of st, i - 1))));
+ val getP = if can HOLogic.dest_imp (hd ts) then
+ (apfst SOME) o HOLogic.dest_imp else pair NONE;
+ fun abstr (t1, t2) = (case t1 of
+ NONE => (case filter (fn Free (s, _) => s mem indnames | _ => false)
+ (term_frees t2) of
+ [Free (s, T)] => absfree (s, T, t2)
+ | _ => sys_error "indtac")
+ | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
+ val cert = cterm_of (Thm.sign_of_thm st);
+ val Ps = map (cert o head_of o snd o getP) ts;
+ val indrule' = cterm_instantiate (Ps ~~
+ (map (cert o abstr o getP) ts')) indrule
+ in
+ rtac indrule' i st
+ end;
+
+fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
+ let
+ (* this theory is used just for parsing *)
+
+ val tmp_thy = thy |>
+ Theory.copy |>
+ Theory.add_types (map (fn (tvs, tname, mx, _) =>
+ (tname, length tvs, mx)) dts);
+
+ val sign = Theory.sign_of tmp_thy;
+
+ val atoms = atoms_of thy;
+ val classes = map (NameSpace.map_base (fn s => "pt_" ^ s)) atoms;
+ val cp_classes = List.concat (map (fn atom1 => map (fn atom2 =>
+ Sign.intern_class thy ("cp_" ^ Sign.base_name atom1 ^ "_" ^
+ Sign.base_name atom2)) atoms) atoms);
+ fun augment_sort S = S union classes;
+ val augment_sort_typ = map_type_tfree (fn (s, S) => TFree (s, augment_sort S));
+
+ fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
+ let val (cargs', sorts') = Library.foldl (prep_typ sign) (([], sorts), cargs)
+ in (constrs @ [(cname, cargs', mx)], sorts') end
+
+ fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
+ let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
+ in (dts @ [(tvs, tname, mx, constrs')], sorts') end
+
+ val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
+ val sorts' = map (apsnd augment_sort) sorts;
+ val tyvars = map #1 dts';
+
+ val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
+ val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
+ map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
+
+ val ps = map (fn (_, n, _, _) =>
+ (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
+ val rps = map Library.swap ps;
+
+ fun replace_types (Type ("nominal.ABS", [T, U])) =
+ Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
+ | replace_types (Type (s, Ts)) =
+ Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
+ | replace_types T = T;
+
+ fun replace_types' (Type (s, Ts)) =
+ Type (getOpt (AList.lookup op = rps s, s), map replace_types' Ts)
+ | replace_types' T = T;
+
+ val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
+ map (fn (cname, cargs, mx) => (cname,
+ map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts';
+
+ val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
+ val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';
+
+ val (thy1, {induction, ...}) =
+ DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
+
+ val SOME {descr, ...} = Symtab.lookup
+ (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
+ val typ_of_dtyp = typ_of_dtyp descr sorts';
+ fun nth_dtyp i = typ_of_dtyp (DtRec i);
+
+ (**** define permutation functions ****)
+
+ val permT = mk_permT (TFree ("'x", HOLogic.typeS));
+ val pi = Free ("pi", permT);
+ val perm_types = map (fn (i, _) =>
+ let val T = nth_dtyp i
+ in permT --> T --> T end) descr;
+ val perm_names = replicate (length new_type_names) "nominal.perm" @
+ DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
+ ("perm_" ^ name_of_typ (nth_dtyp i)))
+ (length new_type_names upto length descr - 1));
+ val perm_names_types = perm_names ~~ perm_types;
+
+ val perm_eqs = List.concat (map (fn (i, (_, _, constrs)) =>
+ let val T = nth_dtyp i
+ in map (fn (cname, dts) =>
+ let
+ val Ts = map typ_of_dtyp dts;
+ val names = DatatypeProp.make_tnames Ts;
+ val args = map Free (names ~~ Ts);
+ val c = Const (cname, Ts ---> T);
+ fun perm_arg (dt, x) =
+ let val T = type_of x
+ in if is_rec_type dt then
+ let val (Us, _) = strip_type T
+ in list_abs (map (pair "x") Us,
+ Const (List.nth (perm_names_types, body_index dt)) $ pi $
+ list_comb (x, map (fn (i, U) =>
+ Const ("nominal.perm", permT --> U --> U) $
+ (Const ("List.rev", permT --> permT) $ pi) $
+ Bound i) ((length Us - 1 downto 0) ~~ Us)))
+ end
+ else Const ("nominal.perm", permT --> T --> T) $ pi $ x
+ end;
+ in
+ (("", HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (Const (List.nth (perm_names_types, i)) $
+ Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
+ list_comb (c, args),
+ list_comb (c, map perm_arg (dts ~~ args))))), [])
+ end) constrs
+ end) descr);
+
+ val (thy2, perm_simps) = thy1 |>
+ Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
+ (List.drop (perm_names_types, length new_type_names))) |>
+ PrimrecPackage.add_primrec_i "" perm_eqs;
+
+ (**** prove that permutation functions introduced by unfolding are ****)
+ (**** equivalent to already existing permutation functions ****)
+
+ val _ = warning ("length descr: " ^ string_of_int (length descr));
+ val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
+
+ val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
+ val perm_fun_def = PureThy.get_thm thy2 (Name "perm_fun_def");
+
+ val unfolded_perm_eq_thms =
+ if length descr = length new_type_names then []
+ else map standard (List.drop (split_conj_thm
+ (prove_goalw_cterm [] (cterm_of thy2
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map (fn (c as (s, T), x) =>
+ let val [T1, T2] = binder_types T
+ in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
+ Const ("nominal.perm", T) $ pi $ Free (x, T2))
+ end)
+ (perm_names_types ~~ perm_indnames)))))
+ (fn _ => [indtac induction perm_indnames 1,
+ ALLGOALS (asm_full_simp_tac
+ (simpset_of thy2 addsimps [perm_fun_def]))])),
+ length new_type_names));
+
+ (**** prove [] \<bullet> t = t ****)
+
+ val _ = warning "perm_empty_thms";
+
+ val perm_empty_thms = List.concat (map (fn a =>
+ let val permT = mk_permT (Type (a, []))
+ in map standard (List.take (split_conj_thm
+ (prove_goalw_cterm [] (cterm_of thy2
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map (fn ((s, T), x) => HOLogic.mk_eq
+ (Const (s, permT --> T --> T) $
+ Const ("List.list.Nil", permT) $ Free (x, T),
+ Free (x, T)))
+ (perm_names ~~
+ map body_type perm_types ~~ perm_indnames)))))
+ (fn _ => [indtac induction perm_indnames 1,
+ ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
+ length new_type_names))
+ end)
+ atoms);
+
+ (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
+
+ val _ = warning "perm_append_thms";
+
+ (*FIXME: these should be looked up statically*)
+ val at_pt_inst = PureThy.get_thm thy2 (Name "at_pt_inst");
+ val pt2 = PureThy.get_thm thy2 (Name "pt2");
+
+ val perm_append_thms = List.concat (map (fn a =>
+ let
+ val permT = mk_permT (Type (a, []));
+ val pi1 = Free ("pi1", permT);
+ val pi2 = Free ("pi2", permT);
+ val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
+ val pt2' = pt_inst RS pt2;
+ val pt2_ax = PureThy.get_thm thy2
+ (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a));
+ in List.take (map standard (split_conj_thm
+ (prove_goalw_cterm [] (cterm_of thy2
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map (fn ((s, T), x) =>
+ let val perm = Const (s, permT --> T --> T)
+ in HOLogic.mk_eq
+ (perm $ (Const ("List.op @", permT --> permT --> permT) $
+ pi1 $ pi2) $ Free (x, T),
+ perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
+ end)
+ (perm_names ~~
+ map body_type perm_types ~~ perm_indnames)))))
+ (fn _ => [indtac induction perm_indnames 1,
+ ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
+ length new_type_names)
+ end) atoms);
+
+ (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
+
+ val _ = warning "perm_eq_thms";
+
+ val pt3 = PureThy.get_thm thy2 (Name "pt3");
+ val pt3_rev = PureThy.get_thm thy2 (Name "pt3_rev");
+
+ val perm_eq_thms = List.concat (map (fn a =>
+ let
+ val permT = mk_permT (Type (a, []));
+ val pi1 = Free ("pi1", permT);
+ val pi2 = Free ("pi2", permT);
+ (*FIXME: not robust - better access these theorems using NominalData?*)
+ val at_inst = PureThy.get_thm thy2 (Name ("at_" ^ Sign.base_name a ^ "_inst"));
+ val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
+ val pt3' = pt_inst RS pt3;
+ val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
+ val pt3_ax = PureThy.get_thm thy2
+ (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
+ in List.take (map standard (split_conj_thm
+ (prove_goalw_cterm [] (cterm_of thy2 (Logic.mk_implies
+ (HOLogic.mk_Trueprop (Const ("nominal.prm_eq",
+ permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map (fn ((s, T), x) =>
+ let val perm = Const (s, permT --> T --> T)
+ in HOLogic.mk_eq
+ (perm $ pi1 $ Free (x, T),
+ perm $ pi2 $ Free (x, T))
+ end)
+ (perm_names ~~
+ map body_type perm_types ~~ perm_indnames))))))
+ (fn hyps => [cut_facts_tac hyps 1, indtac induction perm_indnames 1,
+ ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
+ length new_type_names)
+ end) atoms);
+
+ (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
+
+ val cp1 = PureThy.get_thm thy2 (Name "cp1");
+ val dj_cp = PureThy.get_thm thy2 (Name "dj_cp");
+ val pt_perm_compose = PureThy.get_thm thy2 (Name "pt_perm_compose");
+ val pt_perm_compose_rev = PureThy.get_thm thy2 (Name "pt_perm_compose_rev");
+ val dj_perm_perm_forget = PureThy.get_thm thy2 (Name "dj_perm_perm_forget");
+
+ fun composition_instance name1 name2 thy =
+ let
+ val name1' = Sign.base_name name1;
+ val name2' = Sign.base_name name2;
+ val cp_class = Sign.intern_class thy ("cp_" ^ name1' ^ "_" ^ name2');
+ val permT1 = mk_permT (Type (name1, []));
+ val permT2 = mk_permT (Type (name2, []));
+ val augment = map_type_tfree
+ (fn (x, S) => TFree (x, cp_class :: S));
+ val Ts = map (augment o body_type) perm_types;
+ val cp_inst = PureThy.get_thm thy
+ (Name ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"));
+ val simps = simpset_of thy addsimps (perm_fun_def ::
+ (if name1 <> name2 then
+ let val dj = PureThy.get_thm thy (Name ("dj_" ^ name2' ^ "_" ^ name1'))
+ in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
+ else
+ let
+ val at_inst = PureThy.get_thm thy (Name ("at_" ^ name1' ^ "_inst"));
+ val pt_inst = PureThy.get_thm thy (Name ("pt_" ^ name1' ^ "_inst"))
+ in
+ [cp_inst RS cp1 RS sym,
+ at_inst RS (pt_inst RS pt_perm_compose) RS sym,
+ at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
+ end))
+ val thms = split_conj_thm (prove_goalw_cterm [] (cterm_of thy
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map (fn ((s, T), x) =>
+ let
+ val pi1 = Free ("pi1", permT1);
+ val pi2 = Free ("pi2", permT2);
+ val perm1 = Const (s, permT1 --> T --> T);
+ val perm2 = Const (s, permT2 --> T --> T);
+ val perm3 = Const ("nominal.perm", permT1 --> permT2 --> permT2)
+ in HOLogic.mk_eq
+ (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
+ perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
+ end)
+ (perm_names ~~ Ts ~~ perm_indnames)))))
+ (fn _ => [indtac induction perm_indnames 1,
+ ALLGOALS (asm_full_simp_tac simps)]))
+ in
+ foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
+ (s, replicate (length tvs) (cp_class :: classes), [cp_class])
+ (AxClass.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
+ thy (full_new_type_names' ~~ tyvars)
+ end;
+
+ val (thy3, perm_thmss) = thy2 |>
+ fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
+ curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
+ AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
+ (AxClass.intro_classes_tac [] THEN REPEAT (EVERY
+ [resolve_tac perm_empty_thms 1,
+ resolve_tac perm_append_thms 1,
+ resolve_tac perm_eq_thms 1, assume_tac 1])) thy))
+ (List.take (descr, length new_type_names)) |>
+ PureThy.add_thmss
+ [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
+ unfolded_perm_eq_thms), [Simplifier.simp_add_global]),
+ ((space_implode "_" new_type_names ^ "_perm_empty",
+ perm_empty_thms), [Simplifier.simp_add_global]),
+ ((space_implode "_" new_type_names ^ "_perm_append",
+ perm_append_thms), [Simplifier.simp_add_global]),
+ ((space_implode "_" new_type_names ^ "_perm_eq",
+ perm_eq_thms), [Simplifier.simp_add_global])];
+
+ (**** Define representing sets ****)
+
+ val _ = warning "representing sets";
+
+ val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names
+ (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
+ val big_rep_name =
+ space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
+ (fn (i, ("nominal.nOption", _, _)) => NONE
+ | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
+ val _ = warning ("big_rep_name: " ^ big_rep_name);
+
+ fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
+ (case AList.lookup op = descr i of
+ SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
+ apfst (cons dt) (strip_option dt')
+ | _ => ([], dtf))
+ | strip_option dt = ([], dt);
+
+ fun make_intr s T (cname, cargs) =
+ let
+ fun mk_prem (dt, (j, j', prems, ts)) =
+ let
+ val (dts, dt') = strip_option dt;
+ val (dts', dt'') = strip_dtyp dt';
+ val Ts = map typ_of_dtyp dts;
+ val Us = map typ_of_dtyp dts';
+ val T = typ_of_dtyp dt'';
+ val free = mk_Free "x" (Us ---> T) j;
+ val free' = app_bnds free (length Us);
+ fun mk_abs_fun (T, (i, t)) =
+ let val U = fastype_of t
+ in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
+ Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
+ end
+ in (j + 1, j' + length Ts,
+ case dt'' of
+ DtRec k => list_all (map (pair "x") Us,
+ HOLogic.mk_Trueprop (HOLogic.mk_mem (free',
+ Const (List.nth (rep_set_names, k),
+ HOLogic.mk_setT T)))) :: prems
+ | _ => prems,
+ snd (foldr mk_abs_fun (j', free) Ts) :: ts)
+ end;
+
+ val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs;
+ val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
+ (list_comb (Const (cname, map fastype_of ts ---> T), ts),
+ Const (s, HOLogic.mk_setT T)))
+ in Logic.list_implies (prems, concl)
+ end;
+
+ val (intr_ts, ind_consts) =
+ apfst List.concat (ListPair.unzip (List.mapPartial
+ (fn ((_, ("nominal.nOption", _, _)), _) => NONE
+ | ((i, (_, _, constrs)), rep_set_name) =>
+ let val T = nth_dtyp i
+ in SOME (map (make_intr rep_set_name T) constrs,
+ Const (rep_set_name, HOLogic.mk_setT T))
+ end)
+ (descr ~~ rep_set_names)));
+
+ val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
+ setmp InductivePackage.quiet_mode false
+ (InductivePackage.add_inductive_i false true big_rep_name false true false
+ ind_consts (map (fn x => (("", x), [])) intr_ts) []) thy3;
+
+ (**** Prove that representing set is closed under permutation ****)
+
+ val _ = warning "proving closure under permutation...";
+
+ val perm_indnames' = List.mapPartial
+ (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
+ (perm_indnames ~~ descr);
+
+ fun mk_perm_closed name = map (fn th => standard (th RS mp))
+ (List.take (split_conj_thm (prove_goalw_cterm [] (cterm_of thy4
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
+ (fn (S, x) =>
+ let
+ val S = map_term_types (map_type_tfree
+ (fn (s, cs) => TFree (s, cs union cp_classes))) S;
+ val T = HOLogic.dest_setT (fastype_of S);
+ val permT = mk_permT (Type (name, []))
+ in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
+ HOLogic.mk_mem (Const ("nominal.perm", permT --> T --> T) $
+ Free ("pi", permT) $ Free (x, T), S))
+ end) (ind_consts ~~ perm_indnames')))))
+ (fn _ => (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
+ [indtac rep_induct [] 1,
+ ALLGOALS (simp_tac (simpset_of thy4 addsimps
+ (symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))),
+ ALLGOALS (resolve_tac rep_intrs
+ THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])),
+ length new_type_names));
+
+ (* FIXME: theorems are stored in database for testing only *)
+ val perm_closed_thmss = map mk_perm_closed atoms;
+ val (thy5, _) = PureThy.add_thmss [(("perm_closed",
+ List.concat perm_closed_thmss), [])] thy4;
+
+ (**** typedef ****)
+
+ val _ = warning "defining type...";
+
+ val (thy6, typedefs) =
+ foldl_map (fn (thy, ((((name, mx), tvs), c), name')) =>
+ setmp TypedefPackage.quiet_mode true
+ (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
+ (rtac exI 1 THEN
+ QUIET_BREADTH_FIRST (has_fewer_prems 1)
+ (resolve_tac rep_intrs 1))) thy |> (fn (thy, r) =>
+ let
+ val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
+ val pi = Free ("pi", permT);
+ val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
+ val T = Type (Sign.intern_type thy name, tvs');
+ val Const (_, Type (_, [U])) = c
+ in apsnd (pair r o hd)
+ (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
+ (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
+ Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
+ (Const ("nominal.perm", permT --> U --> U) $ pi $
+ (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
+ Free ("x", T))))), [])] thy)
+ end))
+ (thy5, types_syntax ~~ tyvars ~~
+ (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
+
+ val perm_defs = map snd typedefs;
+ val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
+ val Rep_thms = map (#Rep o fst) typedefs;
+
+ (** prove that new types are in class pt_<name> **)
+
+ val _ = warning "prove that new types are in class pt_<name> ...";
+
+ fun pt_instance ((class, atom), perm_closed_thms) =
+ fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
+ perm_def), name), tvs), perm_closed) => fn thy =>
+ AxClass.add_inst_arity_i
+ (Sign.intern_type thy name,
+ replicate (length tvs) (classes @ cp_classes), [class])
+ (EVERY [AxClass.intro_classes_tac [],
+ rewrite_goals_tac [perm_def],
+ asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
+ asm_full_simp_tac (simpset_of thy addsimps
+ [Rep RS perm_closed RS Abs_inverse]) 1,
+ asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
+ (Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy)
+ (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms);
+
+
+ (** prove that new types are in class cp_<name1>_<name2> **)
+
+ val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
+
+ fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
+ let
+ val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
+ val class = Sign.intern_class thy name;
+ val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
+ in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
+ perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
+ AxClass.add_inst_arity_i
+ (Sign.intern_type thy name,
+ replicate (length tvs) (classes @ cp_classes), [class])
+ (EVERY [AxClass.intro_classes_tac [],
+ rewrite_goals_tac [perm_def],
+ asm_full_simp_tac (simpset_of thy addsimps
+ ((Rep RS perm_closed1 RS Abs_inverse) ::
+ (if atom1 = atom2 then []
+ else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
+ DatatypeAux.cong_tac 1,
+ rtac refl 1,
+ rtac cp1' 1]) thy)
+ (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~
+ perm_closed_thms2) thy
+ end;
+
+ val thy7 = fold (fn x => fn thy => thy |>
+ pt_instance x |>
+ fold (cp_instance (apfst snd x)) (atoms ~~ perm_closed_thmss))
+ (classes ~~ atoms ~~ perm_closed_thmss) thy6;
+
+ (**** constructors ****)
+
+ fun mk_abs_fun (x, t) =
+ let
+ val T = fastype_of x;
+ val U = fastype_of t
+ in
+ Const ("nominal.abs_fun", T --> U --> T -->
+ Type ("nominal.nOption", [U])) $ x $ t
+ end;
+
+ val typ_of_dtyp' = replace_types' o typ_of_dtyp;
+
+ val rep_names = map (fn s =>
+ Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
+ val abs_names = map (fn s =>
+ Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
+
+ val recTs = get_rec_types descr sorts;
+ val newTs' = Library.take (length new_type_names, recTs);
+ val newTs = map replace_types' newTs';
+
+ val full_new_type_names = map (Sign.full_name (sign_of thy)) new_type_names;
+
+ fun make_constr_def tname T T' ((thy, defs, eqns), ((cname, cargs), (cname', mx))) =
+ let
+ fun constr_arg (dt, (j, l_args, r_args)) =
+ let
+ val x' = mk_Free "x" (typ_of_dtyp' dt) j;
+ val (dts, dt') = strip_option dt;
+ val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp' dt) i)
+ (dts ~~ (j upto j + length dts - 1))
+ val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts)
+ val (dts', dt'') = strip_dtyp dt'
+ in case dt'' of
+ DtRec k => if k < length new_type_names then
+ (j + length dts + 1,
+ xs @ x :: l_args,
+ foldr mk_abs_fun
+ (list_abs (map (pair "z" o typ_of_dtyp') dts',
+ Const (List.nth (rep_names, k), typ_of_dtyp' dt'' -->
+ typ_of_dtyp dt'') $ app_bnds x (length dts')))
+ xs :: r_args)
+ else error "nested recursion not (yet) supported"
+ | _ => (j + 1, x' :: l_args, x' :: r_args)
+ end
+
+ val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
+ val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
+ val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
+ val constrT = map fastype_of l_args ---> T;
+ val lhs = list_comb (Const (Sign.full_name thy (Sign.base_name cname),
+ constrT), l_args);
+ val rhs = list_comb (Const (cname, map fastype_of r_args ---> T'), r_args);
+ val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
+ val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (Const (rep_name, T --> T') $ lhs, rhs));
+ val def_name = (Sign.base_name cname) ^ "_def";
+ val (thy', [def_thm]) = thy |>
+ Theory.add_consts_i [(cname', constrT, mx)] |>
+ (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
+ in (thy', defs @ [def_thm], eqns @ [eqn]) end;
+
+ fun dt_constr_defs ((thy, defs, eqns, dist_lemmas),
+ (((((_, (_, _, constrs)), tname), T), T'), constr_syntax)) =
+ let
+ val rep_const = cterm_of thy
+ (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
+ val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
+ val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
+ ((Theory.add_path tname thy, defs, []), constrs ~~ constr_syntax)
+ in
+ (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
+ end;
+
+ val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
+ ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
+ new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
+
+ val abs_inject_thms = map (fn tname =>
+ PureThy.get_thm thy8 (Name ("Abs_" ^ tname ^ "_inject"))) new_type_names;
+
+ val rep_inject_thms = map (fn tname =>
+ PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inject"))) new_type_names;
+
+ val rep_thms = map (fn tname =>
+ PureThy.get_thm thy8 (Name ("Rep_" ^ tname))) new_type_names;
+
+ val rep_inverse_thms = map (fn tname =>
+ PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inverse"))) new_type_names;
+
+ (* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *)
+
+ fun prove_constr_rep_thm eqn =
+ let
+ val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
+ val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms
+ in prove_goalw_cterm [] (cterm_of thy8 eqn) (fn _ =>
+ [resolve_tac inj_thms 1,
+ rewrite_goals_tac rewrites,
+ rtac refl 3,
+ resolve_tac rep_intrs 2,
+ REPEAT (resolve_tac rep_thms 1)])
+ end;
+
+ val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
+
+ (* prove theorem pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
+
+ fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
+ let
+ val _ $ (_ $ (Rep $ x) $ _) = Logic.unvarify (prop_of th);
+ val Type ("fun", [T, U]) = fastype_of Rep;
+ val permT = mk_permT (Type (atom, []));
+ val pi = Free ("pi", permT);
+ in
+ prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (Const ("nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
+ Rep $ (Const ("nominal.perm", permT --> T --> T) $ pi $ x)))))
+ (fn _ => [simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
+ perm_closed_thms @ Rep_thms)) 1])
+ end) Rep_thms;
+
+ val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
+ (atoms ~~ perm_closed_thmss));
+
+ (* prove distinctness theorems *)
+
+ fun make_distincts_1 _ [] = []
+ | make_distincts_1 tname ((cname, cargs)::constrs) =
+ let
+ val cname = Sign.intern_const thy8
+ (NameSpace.append tname (Sign.base_name cname));
+ val (Ts, T) = strip_type (the (Sign.const_type thy8 cname));
+ val frees = map Free ((DatatypeProp.make_tnames Ts) ~~ Ts);
+ val t = list_comb (Const (cname, Ts ---> T), frees);
+
+ fun make_distincts' [] = []
+ | make_distincts' ((cname', cargs')::constrs') =
+ let
+ val cname' = Sign.intern_const thy8
+ (NameSpace.append tname (Sign.base_name cname'));
+ val Ts' = binder_types (the (Sign.const_type thy8 cname'));
+ val frees' = map Free ((map ((op ^) o (rpair "'"))
+ (DatatypeProp.make_tnames Ts')) ~~ Ts');
+ val t' = list_comb (Const (cname', Ts' ---> T), frees')
+ in
+ (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')))::
+ (make_distincts' constrs')
+ end
+
+ in (make_distincts' constrs) @ (make_distincts_1 tname constrs)
+ end;
+
+ val distinct_props = map (fn ((_, (_, _, constrs)), tname) =>
+ make_distincts_1 tname constrs)
+ (List.take (descr, length new_type_names) ~~ new_type_names);
+
+ val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
+ dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
+ (constr_rep_thmss ~~ dist_lemmas);
+
+ fun prove_distinct_thms (_, []) = []
+ | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
+ let
+ val dist_thm = prove_goalw_cterm [] (cterm_of thy8 t) (fn _ =>
+ [simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1])
+ in dist_thm::(standard (dist_thm RS not_sym))::
+ (prove_distinct_thms (p, ts))
+ end;
+
+ val distinct_thms = map prove_distinct_thms
+ (constr_rep_thmss ~~ dist_lemmas ~~ distinct_props);
+
+ (** prove equations for permutation functions **)
+
+ val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *)
+
+ val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
+ let val T = replace_types' (nth_dtyp i)
+ in List.concat (map (fn (atom, perm_closed_thms) =>
+ map (fn ((cname, dts), constr_rep_thm) =>
+ let
+ val cname = Sign.intern_const thy8
+ (NameSpace.append tname (Sign.base_name cname));
+ val permT = mk_permT (Type (atom, []));
+ val pi = Free ("pi", permT);
+
+ fun perm t =
+ let val T = fastype_of t
+ in Const ("nominal.perm", permT --> T --> T) $ pi $ t end;
+
+ fun constr_arg (dt, (j, l_args, r_args)) =
+ let
+ val x' = mk_Free "x" (typ_of_dtyp' dt) j;
+ val (dts, dt') = strip_option dt;
+ val Ts = map typ_of_dtyp' dts;
+ val xs = map (fn (T, i) => mk_Free "x" T i)
+ (Ts ~~ (j upto j + length dts - 1))
+ val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
+ val (dts', dt'') = strip_dtyp dt';
+ in case dt'' of
+ DtRec k => if k < length new_type_names then
+ (j + length dts + 1,
+ xs @ x :: l_args,
+ map perm (xs @ [x]) @ r_args)
+ else error "nested recursion not (yet) supported"
+ | _ => (j + 1, x' :: l_args, perm x' :: r_args)
+ end
+
+ val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts;
+ val c = Const (cname, map fastype_of l_args ---> T)
+ in
+ prove_goalw_cterm [] (cterm_of thy8
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
+ (fn _ =>
+ [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
+ simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
+ constr_defs @ perm_closed_thms)) 1,
+ TRY (simp_tac (HOL_basic_ss addsimps
+ (symmetric perm_fun_def :: abs_perm)) 1),
+ TRY (simp_tac (HOL_basic_ss addsimps
+ (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
+ perm_closed_thms)) 1)])
+ end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
+ end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
+
+ (** prove injectivity of constructors **)
+
+ val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
+ val alpha = PureThy.get_thms thy8 (Name "alpha");
+ val abs_fresh = PureThy.get_thms thy8 (Name "abs_fresh");
+ val fresh_def = PureThy.get_thm thy8 (Name "fresh_def");
+ val supp_def = PureThy.get_thm thy8 (Name "supp_def");
+
+ val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
+ let val T = replace_types' (nth_dtyp i)
+ in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
+ if null dts then NONE else SOME
+ let
+ val cname = Sign.intern_const thy8
+ (NameSpace.append tname (Sign.base_name cname));
+
+ fun make_inj (dt, (j, args1, args2, eqs)) =
+ let
+ val x' = mk_Free "x" (typ_of_dtyp' dt) j;
+ val y' = mk_Free "y" (typ_of_dtyp' dt) j;
+ val (dts, dt') = strip_option dt;
+ val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
+ val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
+ val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
+ val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
+ val y = mk_Free "y" (typ_of_dtyp' dt') (j + length dts);
+ val (dts', dt'') = strip_dtyp dt';
+ in case dt'' of
+ DtRec k => if k < length new_type_names then
+ (j + length dts + 1,
+ xs @ (x :: args1), ys @ (y :: args2),
+ HOLogic.mk_eq
+ (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs)
+ else error "nested recursion not (yet) supported"
+ | _ => (j + 1, x' :: args1, y' :: args2, HOLogic.mk_eq (x', y') :: eqs)
+ end;
+
+ val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts;
+ val Ts = map fastype_of args1;
+ val c = Const (cname, Ts ---> T)
+ in
+ prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
+ foldr1 HOLogic.mk_conj eqs))))
+ (fn _ =>
+ [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
+ rep_inject_thms')) 1,
+ TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
+ alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
+ perm_rep_perm_thms)) 1)])
+ end) (constrs ~~ constr_rep_thms)
+ end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
+
+ val (thy9, _) = thy8 |>
+ DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
+ DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
+ DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
+ DatatypeAux.store_thmss "inject" new_type_names inject_thms;
+
+ in
+ (thy9, perm_eq_thms)
+ end;
+
+val add_nominal_datatype = gen_add_nominal_datatype read_typ true;
+
+
+(* FIXME: The following stuff should be exported by DatatypePackage *)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val datatype_decl =
+ Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
+ (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
+
+fun mk_datatype args =
+ let
+ val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
+ val specs = map (fn ((((_, vs), t), mx), cons) =>
+ (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
+ in #1 o add_nominal_datatype false names specs end;
+
+val nominal_datatypeP =
+ OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
+ (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
+
+val _ = OuterSyntax.add_parsers [nominal_datatypeP];
+
+end;
+
+end
\ No newline at end of file