Initial revision.
authorberghofe
Mon Oct 17 12:30:57 2005 +0200 (2005-10-17)
changeset 17870c35381811d5c
parent 17869 585c1f08499e
child 17871 67ffbfcd6fef
Initial revision.
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Oct 17 12:30:57 2005 +0200
     1.3 @@ -0,0 +1,2309 @@
     1.4 +(* $Id$ *)
     1.5 +
     1.6 +theory nominal 
     1.7 +imports Main
     1.8 +  uses ("nominal_package.ML") ("nominal_induct.ML") ("nominal_permeq.ML")
     1.9 +begin 
    1.10 +
    1.11 +ML {* reset NameSpace.unique_names; *}
    1.12 +
    1.13 +section {* Permutations *}
    1.14 +(*======================*)
    1.15 +
    1.16 +types 
    1.17 +  'x prm = "('x \<times> 'x) list"
    1.18 +
    1.19 +(* polymorphic operations for permutation and swapping*)
    1.20 +consts 
    1.21 +  perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     ("_ \<bullet> _" [80,80] 80)
    1.22 +  swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
    1.23 +
    1.24 +(* permutation on sets *)
    1.25 +defs (overloaded)
    1.26 +  perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
    1.27 +
    1.28 +(* permutation on units and products *)
    1.29 +primrec (perm_unit)
    1.30 +  "pi\<bullet>()    = ()"
    1.31 +
    1.32 +primrec (perm_prod)
    1.33 +  "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)"
    1.34 +
    1.35 +lemma perm_fst:
    1.36 +  "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
    1.37 + by (cases x, simp)
    1.38 +
    1.39 +lemma perm_snd:
    1.40 +  "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
    1.41 + by (cases x, simp)
    1.42 +
    1.43 +(* permutation on lists *)
    1.44 +primrec (perm_list)
    1.45 +  perm_nil_def:  "pi\<bullet>[]     = []"
    1.46 +  perm_cons_def: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
    1.47 +
    1.48 +lemma perm_append:
    1.49 +  fixes pi :: "'x prm"
    1.50 +  and   l1 :: "'a list"
    1.51 +  and   l2 :: "'a list"
    1.52 +  shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
    1.53 +  by (induct l1, auto)
    1.54 +
    1.55 +lemma perm_rev:
    1.56 +  fixes pi :: "'x prm"
    1.57 +  and   l  :: "'a list"
    1.58 +  shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
    1.59 +  by (induct l, simp_all add: perm_append)
    1.60 +
    1.61 +(* permutation on functions *)
    1.62 +defs (overloaded)
    1.63 +  perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    1.64 +
    1.65 +(* permutation on bools *)
    1.66 +primrec (perm_bool)
    1.67 +  perm_true_def:  "pi\<bullet>True  = True"
    1.68 +  perm_false_def: "pi\<bullet>False = False"
    1.69 +
    1.70 +(* permutation on options *)
    1.71 +primrec (perm_option)
    1.72 +  perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
    1.73 +  perm_none_def:  "pi\<bullet>None    = None"
    1.74 +
    1.75 +(* a "private" copy of the option type used in the abstraction function *)
    1.76 +datatype 'a nOption = nSome 'a | nNone
    1.77 +
    1.78 +primrec (perm_noption)
    1.79 +  perm_Nsome_def:  "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
    1.80 +  perm_Nnone_def:  "pi\<bullet>nNone    = nNone"
    1.81 +
    1.82 +(* permutation on characters (used in strings) *)
    1.83 +defs (overloaded)
    1.84 +  perm_char_def: "pi\<bullet>(s::char) \<equiv> s"
    1.85 +
    1.86 +(* permutation on ints *)
    1.87 +defs (overloaded)
    1.88 +  perm_int_def:    "pi\<bullet>(i::int) \<equiv> i"
    1.89 +
    1.90 +(* permutation on nats *)
    1.91 +defs (overloaded)
    1.92 +  perm_nat_def:    "pi\<bullet>(i::nat) \<equiv> i"
    1.93 +
    1.94 +section {* permutation equality *}
    1.95 +(*==============================*)
    1.96 +
    1.97 +constdefs
    1.98 +  prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool"  (" _ \<sim> _ " [80,80] 80)
    1.99 +  "pi1 \<sim> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
   1.100 +
   1.101 +section {* Support, Freshness and Supports*}
   1.102 +(*========================================*)
   1.103 +constdefs
   1.104 +   supp :: "'a \<Rightarrow> ('x set)"  
   1.105 +   "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
   1.106 +
   1.107 +   fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" (" _ \<sharp> _" [80,80] 80)
   1.108 +   "a \<sharp> x \<equiv> a \<notin> supp x"
   1.109 +
   1.110 +   supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80)
   1.111 +   "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
   1.112 +
   1.113 +lemma supp_fresh_iff: 
   1.114 +  fixes x :: "'a"
   1.115 +  shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
   1.116 +apply(simp add: fresh_def)
   1.117 +done
   1.118 +
   1.119 +lemma supp_unit:
   1.120 +  shows "supp () = {}"
   1.121 +  by (simp add: supp_def)
   1.122 +
   1.123 +lemma supp_prod: 
   1.124 +  fixes x :: "'a"
   1.125 +  and   y :: "'b"
   1.126 +  shows "(supp (x,y)) = (supp x)\<union>(supp y)"
   1.127 +  by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
   1.128 +
   1.129 +lemma supp_list_nil:
   1.130 +  shows "supp [] = {}"
   1.131 +apply(simp add: supp_def)
   1.132 +done
   1.133 +
   1.134 +lemma supp_list_cons:
   1.135 +  fixes x  :: "'a"
   1.136 +  and   xs :: "'a list"
   1.137 +  shows "supp (x#xs) = (supp x)\<union>(supp xs)"
   1.138 +apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
   1.139 +done
   1.140 +
   1.141 +lemma supp_list_append:
   1.142 +  fixes xs :: "'a list"
   1.143 +  and   ys :: "'a list"
   1.144 +  shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
   1.145 +  by (induct xs, auto simp add: supp_list_nil supp_list_cons)
   1.146 +
   1.147 +lemma supp_list_rev:
   1.148 +  fixes xs :: "'a list"
   1.149 +  shows "supp (rev xs) = (supp xs)"
   1.150 +  by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil)
   1.151 +
   1.152 +lemma supp_bool:
   1.153 +  fixes x  :: "bool"
   1.154 +  shows "supp (x) = {}"
   1.155 +  apply(case_tac "x")
   1.156 +  apply(simp_all add: supp_def)
   1.157 +done
   1.158 +
   1.159 +lemma supp_some:
   1.160 +  fixes x :: "'a"
   1.161 +  shows "supp (Some x) = (supp x)"
   1.162 +  apply(simp add: supp_def)
   1.163 +  done
   1.164 +
   1.165 +lemma supp_none:
   1.166 +  fixes x :: "'a"
   1.167 +  shows "supp (None) = {}"
   1.168 +  apply(simp add: supp_def)
   1.169 +  done
   1.170 +
   1.171 +lemma supp_int:
   1.172 +  fixes i::"int"
   1.173 +  shows "supp (i) = {}"
   1.174 +  apply(simp add: supp_def perm_int_def)
   1.175 +  done
   1.176 +
   1.177 +lemma fresh_prod:
   1.178 +  fixes a :: "'x"
   1.179 +  and   x :: "'a"
   1.180 +  and   y :: "'b"
   1.181 +  shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)"
   1.182 +  by (simp add: fresh_def supp_prod)
   1.183 +
   1.184 +lemma fresh_list_nil:
   1.185 +  fixes a :: "'x"
   1.186 +  shows "a\<sharp>([]::'a list)"
   1.187 +  by (simp add: fresh_def supp_list_nil) 
   1.188 +
   1.189 +lemma fresh_list_cons:
   1.190 +  fixes a :: "'x"
   1.191 +  and   x :: "'a"
   1.192 +  and   xs :: "'a list"
   1.193 +  shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)"
   1.194 +  by (simp add: fresh_def supp_list_cons)
   1.195 +
   1.196 +lemma fresh_list_append:
   1.197 +  fixes a :: "'x"
   1.198 +  and   xs :: "'a list"
   1.199 +  and   ys :: "'a list"
   1.200 +  shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)"
   1.201 +  by (simp add: fresh_def supp_list_append)
   1.202 +
   1.203 +lemma fresh_list_rev:
   1.204 +  fixes a :: "'x"
   1.205 +  and   xs :: "'a list"
   1.206 +  shows "a\<sharp>(rev xs) = a\<sharp>xs"
   1.207 +  by (simp add: fresh_def supp_list_rev)
   1.208 +
   1.209 +lemma fresh_none:
   1.210 +  fixes a :: "'x"
   1.211 +  shows "a\<sharp>None"
   1.212 +  apply(simp add: fresh_def supp_none)
   1.213 +  done
   1.214 +
   1.215 +lemma fresh_some:
   1.216 +  fixes a :: "'x"
   1.217 +  and   x :: "'a"
   1.218 +  shows "a\<sharp>(Some x) = a\<sharp>x"
   1.219 +  apply(simp add: fresh_def supp_some)
   1.220 +  done
   1.221 +
   1.222 +section {* Abstract Properties for Permutations and  Atoms *}
   1.223 +(*=========================================================*)
   1.224 +
   1.225 +(* properties for being a permutation type *)
   1.226 +constdefs 
   1.227 +  "pt TYPE('a) TYPE('x) \<equiv> 
   1.228 +     (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 
   1.229 +     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and> 
   1.230 +     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<sim> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"
   1.231 +
   1.232 +(* properties for being an atom type *)
   1.233 +constdefs 
   1.234 +  "at TYPE('x) \<equiv> 
   1.235 +     (\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and>
   1.236 +     (\<forall>(a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))\<bullet>x = swap (a,b) (pi\<bullet>x)) \<and> 
   1.237 +     (\<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> 
   1.238 +     (infinite (UNIV::'x set))"
   1.239 +
   1.240 +(* property of two atom-types being disjoint *)
   1.241 +constdefs
   1.242 +  "disjoint TYPE('x) TYPE('y) \<equiv> 
   1.243 +       (\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and> 
   1.244 +       (\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)"
   1.245 +
   1.246 +(* composition property of two permutation on a type 'a *)
   1.247 +constdefs
   1.248 +  "cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 
   1.249 +      (\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))" 
   1.250 +
   1.251 +(* property of having finite support *)
   1.252 +constdefs 
   1.253 +  "fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)"
   1.254 +
   1.255 +section {* Lemmas about the atom-type properties*}
   1.256 +(*==============================================*)
   1.257 +
   1.258 +lemma at1: 
   1.259 +  fixes x::"'x"
   1.260 +  assumes a: "at TYPE('x)"
   1.261 +  shows "([]::'x prm)\<bullet>x = x"
   1.262 +  using a by (simp add: at_def)
   1.263 +
   1.264 +lemma at2: 
   1.265 +  fixes a ::"'x"
   1.266 +  and   b ::"'x"
   1.267 +  and   x ::"'x"
   1.268 +  and   pi::"'x prm"
   1.269 +  assumes a: "at TYPE('x)"
   1.270 +  shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)"
   1.271 +  using a by (simp only: at_def)
   1.272 +
   1.273 +lemma at3: 
   1.274 +  fixes a ::"'x"
   1.275 +  and   b ::"'x"
   1.276 +  and   c ::"'x"
   1.277 +  assumes a: "at TYPE('x)"
   1.278 +  shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
   1.279 +  using a by (simp only: at_def)
   1.280 +
   1.281 +(* rules to calculate simple premutations *)
   1.282 +lemmas at_calc = at2 at1 at3
   1.283 +
   1.284 +lemma at4: 
   1.285 +  assumes a: "at TYPE('x)"
   1.286 +  shows "infinite (UNIV::'x set)"
   1.287 +  using a by (simp add: at_def)
   1.288 +
   1.289 +lemma at_append:
   1.290 +  fixes pi1 :: "'x prm"
   1.291 +  and   pi2 :: "'x prm"
   1.292 +  and   c   :: "'x"
   1.293 +  assumes at: "at TYPE('x)" 
   1.294 +  shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)"
   1.295 +proof (induct pi1)
   1.296 +  case Nil show ?case by (simp add: at1[OF at])
   1.297 +next
   1.298 +  case (Cons x xs)
   1.299 +  assume i: "(xs @ pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)"
   1.300 +  have "(x#xs)@pi2 = x#(xs@pi2)" by simp
   1.301 +  thus ?case using i by (cases "x", simp add:  at2[OF at])
   1.302 +qed
   1.303 + 
   1.304 +lemma at_swap:
   1.305 +  fixes a :: "'x"
   1.306 +  and   b :: "'x"
   1.307 +  and   c :: "'x"
   1.308 +  assumes at: "at TYPE('x)" 
   1.309 +  shows "swap (a,b) (swap (a,b) c) = c"
   1.310 +  by (auto simp add: at3[OF at])
   1.311 +
   1.312 +lemma at_rev_pi:
   1.313 +  fixes pi :: "'x prm"
   1.314 +  and   c  :: "'x"
   1.315 +  assumes at: "at TYPE('x)"
   1.316 +  shows "(rev pi)\<bullet>(pi\<bullet>c) = c"
   1.317 +proof(induct pi)
   1.318 +  case Nil show ?case by (simp add: at1[OF at])
   1.319 +next
   1.320 +  case (Cons x xs) thus ?case 
   1.321 +    by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at])
   1.322 +qed
   1.323 +
   1.324 +lemma at_pi_rev:
   1.325 +  fixes pi :: "'x prm"
   1.326 +  and   x  :: "'x"
   1.327 +  assumes at: "at TYPE('x)"
   1.328 +  shows "pi\<bullet>((rev pi)\<bullet>x) = x"
   1.329 +  by (rule at_rev_pi[OF at, of "rev pi" _,simplified])
   1.330 +
   1.331 +lemma at_bij1: 
   1.332 +  fixes pi :: "'x prm"
   1.333 +  and   x  :: "'x"
   1.334 +  and   y  :: "'x"
   1.335 +  assumes at: "at TYPE('x)"
   1.336 +  and     a:  "(pi\<bullet>x) = y"
   1.337 +  shows   "x=(rev pi)\<bullet>y"
   1.338 +proof -
   1.339 +  from a have "y=(pi\<bullet>x)" by (rule sym)
   1.340 +  thus ?thesis by (simp only: at_rev_pi[OF at])
   1.341 +qed
   1.342 +
   1.343 +lemma at_bij2: 
   1.344 +  fixes pi :: "'x prm"
   1.345 +  and   x  :: "'x"
   1.346 +  and   y  :: "'x"
   1.347 +  assumes at: "at TYPE('x)"
   1.348 +  and     a:  "((rev pi)\<bullet>x) = y"
   1.349 +  shows   "x=pi\<bullet>y"
   1.350 +proof -
   1.351 +  from a have "y=((rev pi)\<bullet>x)" by (rule sym)
   1.352 +  thus ?thesis by (simp only: at_pi_rev[OF at])
   1.353 +qed
   1.354 +
   1.355 +lemma at_bij:
   1.356 +  fixes pi :: "'x prm"
   1.357 +  and   x  :: "'x"
   1.358 +  and   y  :: "'x"
   1.359 +  assumes at: "at TYPE('x)"
   1.360 +  shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
   1.361 +proof 
   1.362 +  assume "pi\<bullet>x = pi\<bullet>y" 
   1.363 +  hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 
   1.364 +  thus "x=y" by (simp only: at_rev_pi[OF at])
   1.365 +next
   1.366 +  assume "x=y"
   1.367 +  thus "pi\<bullet>x = pi\<bullet>y" by simp
   1.368 +qed
   1.369 +
   1.370 +lemma at_supp:
   1.371 +  fixes x :: "'x"
   1.372 +  assumes at: "at TYPE('x)"
   1.373 +  shows "supp x = {x}"
   1.374 +proof (simp add: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at], auto)
   1.375 +  assume f: "finite {b::'x. b \<noteq> x}"
   1.376 +  have a1: "{b::'x. b \<noteq> x} = UNIV-{x}" by force
   1.377 +  have a2: "infinite (UNIV::'x set)" by (rule at4[OF at])
   1.378 +  from f a1 a2 show False by force
   1.379 +qed
   1.380 +
   1.381 +lemma at_fresh:
   1.382 +  fixes a :: "'x"
   1.383 +  and   b :: "'x"
   1.384 +  assumes at: "at TYPE('x)"
   1.385 +  shows "(a\<sharp>b) = (a\<noteq>b)" 
   1.386 +  by (simp add: at_supp[OF at] fresh_def)
   1.387 +
   1.388 +lemma at_prm_fresh[rule_format]:
   1.389 +  fixes c :: "'x"
   1.390 +  and   pi:: "'x prm"
   1.391 +  assumes at: "at TYPE('x)"
   1.392 +  shows "c\<sharp>pi \<longrightarrow> pi\<bullet>c = c"
   1.393 +apply(induct pi)
   1.394 +apply(simp add: at1[OF at]) 
   1.395 +apply(force simp add: fresh_list_cons at2[OF at] fresh_prod at_fresh[OF at] at3[OF at])
   1.396 +done
   1.397 +
   1.398 +lemma at_prm_rev_eq:
   1.399 +  fixes pi1 :: "'x prm"
   1.400 +  and   pi2 :: "'x prm"
   1.401 +  assumes at: "at TYPE('x)"
   1.402 +  shows a: "((rev pi1) \<sim> (rev pi2)) = (pi1 \<sim> pi2)"
   1.403 +proof (simp add: prm_eq_def, auto)
   1.404 +  fix x
   1.405 +  assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
   1.406 +  hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp
   1.407 +  hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at])
   1.408 +  hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at])
   1.409 +  thus "pi1 \<bullet> x  =  pi2 \<bullet> x" by simp
   1.410 +next
   1.411 +  fix x
   1.412 +  assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x"
   1.413 +  hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp
   1.414 +  hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at])
   1.415 +  hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at])
   1.416 +  thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp
   1.417 +qed
   1.418 +  
   1.419 +lemma at_prm_rev_eq1:
   1.420 +  fixes pi1 :: "'x prm"
   1.421 +  and   pi2 :: "'x prm"
   1.422 +  assumes at: "at TYPE('x)"
   1.423 +  shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1) \<sim> (rev pi2)"
   1.424 +  by (simp add: at_prm_rev_eq[OF at])
   1.425 +
   1.426 +lemma at_ds1:
   1.427 +  fixes a  :: "'x"
   1.428 +  assumes at: "at TYPE('x)"
   1.429 +  shows "[(a,a)] \<sim> []"
   1.430 +  by (force simp add: prm_eq_def at_calc[OF at])
   1.431 +
   1.432 +lemma at_ds2: 
   1.433 +  fixes pi :: "'x prm"
   1.434 +  and   a  :: "'x"
   1.435 +  and   b  :: "'x"
   1.436 +  assumes at: "at TYPE('x)"
   1.437 +  shows "(pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)]) \<sim> ([(a,b)]@pi)"
   1.438 +  by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 
   1.439 +      at_rev_pi[OF at] at_calc[OF at])
   1.440 +
   1.441 +lemma at_ds3: 
   1.442 +  fixes a  :: "'x"
   1.443 +  and   b  :: "'x"
   1.444 +  and   c  :: "'x"
   1.445 +  assumes at: "at TYPE('x)"
   1.446 +  and     a:  "distinct [a,b,c]"
   1.447 +  shows "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]"
   1.448 +  using a by (force simp add: prm_eq_def at_calc[OF at])
   1.449 +
   1.450 +lemma at_ds4: 
   1.451 +  fixes a  :: "'x"
   1.452 +  and   b  :: "'x"
   1.453 +  and   pi  :: "'x prm"
   1.454 +  assumes at: "at TYPE('x)"
   1.455 +  shows "(pi@[(a,(rev pi)\<bullet>b)]) \<sim> ([(pi\<bullet>a,b)]@pi)"
   1.456 +  by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 
   1.457 +      at_pi_rev[OF at] at_rev_pi[OF at])
   1.458 +
   1.459 +lemma at_ds5: 
   1.460 +  fixes a  :: "'x"
   1.461 +  and   b  :: "'x"
   1.462 +  assumes at: "at TYPE('x)"
   1.463 +  shows "[(a,b)] \<sim> [(b,a)]"
   1.464 +  by (force simp add: prm_eq_def at_calc[OF at])
   1.465 +
   1.466 +lemma at_ds6: 
   1.467 +  fixes a  :: "'x"
   1.468 +  and   b  :: "'x"
   1.469 +  and   c  :: "'x"
   1.470 +  assumes at: "at TYPE('x)"
   1.471 +  and     a: "distinct [a,b,c]"
   1.472 +  shows "[(a,c),(a,b)] \<sim> [(b,c),(a,c)]"
   1.473 +  using a by (force simp add: prm_eq_def at_calc[OF at])
   1.474 +
   1.475 +lemma at_ds7:
   1.476 +  fixes pi :: "'x prm"
   1.477 +  assumes at: "at TYPE('x)"
   1.478 +  shows "((rev pi)@pi) \<sim> []"
   1.479 +  by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at])
   1.480 +
   1.481 +lemma at_ds8_aux:
   1.482 +  fixes pi :: "'x prm"
   1.483 +  and   a  :: "'x"
   1.484 +  and   b  :: "'x"
   1.485 +  and   c  :: "'x"
   1.486 +  assumes at: "at TYPE('x)"
   1.487 +  shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)"
   1.488 +  by (force simp add: at_calc[OF at] at_bij[OF at])
   1.489 +
   1.490 +lemma at_ds8: 
   1.491 +  fixes pi1 :: "'x prm"
   1.492 +  and   pi2 :: "'x prm"
   1.493 +  and   a  :: "'x"
   1.494 +  and   b  :: "'x"
   1.495 +  assumes at: "at TYPE('x)"
   1.496 +  shows "(pi1@pi2) \<sim> ((pi1\<bullet>pi2)@pi1)"
   1.497 +apply(induct_tac pi2)
   1.498 +apply(simp add: prm_eq_def)
   1.499 +apply(auto simp add: prm_eq_def)
   1.500 +apply(simp add: at2[OF at])
   1.501 +apply(drule_tac x="aa" in spec)
   1.502 +apply(drule sym)
   1.503 +apply(simp)
   1.504 +apply(simp add: at_append[OF at])
   1.505 +apply(simp add: at2[OF at])
   1.506 +apply(simp add: at_ds8_aux[OF at])
   1.507 +done
   1.508 +
   1.509 +lemma at_ds9: 
   1.510 +  fixes pi1 :: "'x prm"
   1.511 +  and   pi2 :: "'x prm"
   1.512 +  and   a  :: "'x"
   1.513 +  and   b  :: "'x"
   1.514 +  assumes at: "at TYPE('x)"
   1.515 +  shows " ((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
   1.516 +apply(induct_tac pi2)
   1.517 +apply(simp add: prm_eq_def)
   1.518 +apply(auto simp add: prm_eq_def)
   1.519 +apply(simp add: at_append[OF at])
   1.520 +apply(simp add: at2[OF at] at1[OF at])
   1.521 +apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec)
   1.522 +apply(drule sym)
   1.523 +apply(simp)
   1.524 +apply(simp add: at_ds8_aux[OF at])
   1.525 +apply(simp add: at_rev_pi[OF at])
   1.526 +done
   1.527 +
   1.528 +--"there always exists an atom not being in a finite set"
   1.529 +lemma ex_in_inf:
   1.530 +  fixes   A::"'x set"
   1.531 +  assumes at: "at TYPE('x)"
   1.532 +  and     fs: "finite A"
   1.533 +  shows "\<exists>c::'x. c\<notin>A"
   1.534 +proof -
   1.535 +  from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 
   1.536 +    by (simp add: Diff_infinite_finite)
   1.537 +  hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
   1.538 +  hence "\<exists>c::'x. c\<in>((UNIV::'x set) - A)" by force
   1.539 +  thus "\<exists>c::'x. c\<notin>A" by force
   1.540 +qed
   1.541 +
   1.542 +--"there always exists a fresh name for an object with finite support"
   1.543 +lemma at_exists_fresh: 
   1.544 +  fixes  x :: "'a"
   1.545 +  assumes at: "at TYPE('x)"
   1.546 +  and     fs: "finite ((supp x)::'x set)"
   1.547 +  shows "\<exists>c::'x. c\<sharp>x"
   1.548 +  by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs])
   1.549 +
   1.550 +--"the at-props imply the pt-props"
   1.551 +lemma at_pt_inst:
   1.552 +  assumes at: "at TYPE('x)"
   1.553 +  shows "pt TYPE('x) TYPE('x)"
   1.554 +apply(auto simp only: pt_def)
   1.555 +apply(simp only: at1[OF at])
   1.556 +apply(simp only: at_append[OF at]) 
   1.557 +apply(simp add: prm_eq_def)
   1.558 +done
   1.559 +
   1.560 +section {* finite support properties *}
   1.561 +(*===================================*)
   1.562 +
   1.563 +lemma fs1:
   1.564 +  fixes x :: "'a"
   1.565 +  assumes a: "fs TYPE('a) TYPE('x)"
   1.566 +  shows "finite ((supp x)::'x set)"
   1.567 +  using a by (simp add: fs_def)
   1.568 +
   1.569 +lemma fs_at_inst:
   1.570 +  fixes a :: "'x"
   1.571 +  assumes at: "at TYPE('x)"
   1.572 +  shows "fs TYPE('x) TYPE('x)"
   1.573 +apply(simp add: fs_def) 
   1.574 +apply(simp add: at_supp[OF at])
   1.575 +done
   1.576 +
   1.577 +lemma fs_unit_inst:
   1.578 +  shows "fs TYPE(unit) TYPE('x)"
   1.579 +apply(simp add: fs_def)
   1.580 +apply(simp add: supp_unit)
   1.581 +done
   1.582 +
   1.583 +lemma fs_prod_inst:
   1.584 +  assumes fsa: "fs TYPE('a) TYPE('x)"
   1.585 +  and     fsb: "fs TYPE('b) TYPE('x)"
   1.586 +  shows "fs TYPE('a\<times>'b) TYPE('x)"
   1.587 +apply(unfold fs_def)
   1.588 +apply(auto simp add: supp_prod)
   1.589 +apply(rule fs1[OF fsa])
   1.590 +apply(rule fs1[OF fsb])
   1.591 +done
   1.592 +
   1.593 +lemma fs_list_inst:
   1.594 +  assumes fs: "fs TYPE('a) TYPE('x)"
   1.595 +  shows "fs TYPE('a list) TYPE('x)"
   1.596 +apply(simp add: fs_def, rule allI)
   1.597 +apply(induct_tac x)
   1.598 +apply(simp add: supp_list_nil)
   1.599 +apply(simp add: supp_list_cons)
   1.600 +apply(rule fs1[OF fs])
   1.601 +done
   1.602 +
   1.603 +lemma fs_bool_inst:
   1.604 +  shows "fs TYPE(bool) TYPE('x)"
   1.605 +apply(simp add: fs_def, rule allI)
   1.606 +apply(simp add: supp_bool)
   1.607 +done
   1.608 +
   1.609 +lemma fs_int_inst:
   1.610 +  shows "fs TYPE(int) TYPE('x)"
   1.611 +apply(simp add: fs_def, rule allI)
   1.612 +apply(simp add: supp_int)
   1.613 +done
   1.614 +
   1.615 +section {* Lemmas about the permutation properties *}
   1.616 +(*=================================================*)
   1.617 +
   1.618 +lemma pt1:
   1.619 +  fixes x::"'a"
   1.620 +  assumes a: "pt TYPE('a) TYPE('x)"
   1.621 +  shows "([]::'x prm)\<bullet>x = x"
   1.622 +  using a by (simp add: pt_def)
   1.623 +
   1.624 +lemma pt2: 
   1.625 +  fixes pi1::"'x prm"
   1.626 +  and   pi2::"'x prm"
   1.627 +  and   x  ::"'a"
   1.628 +  assumes a: "pt TYPE('a) TYPE('x)"
   1.629 +  shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)"
   1.630 +  using a by (simp add: pt_def)
   1.631 +
   1.632 +lemma pt3:
   1.633 +  fixes pi1::"'x prm"
   1.634 +  and   pi2::"'x prm"
   1.635 +  and   x  ::"'a"
   1.636 +  assumes a: "pt TYPE('a) TYPE('x)"
   1.637 +  shows "pi1 \<sim> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x"
   1.638 +  using a by (simp add: pt_def)
   1.639 +
   1.640 +lemma pt3_rev:
   1.641 +  fixes pi1::"'x prm"
   1.642 +  and   pi2::"'x prm"
   1.643 +  and   x  ::"'a"
   1.644 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.645 +  and     at: "at TYPE('x)"
   1.646 +  shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
   1.647 +  by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])
   1.648 +
   1.649 +section {* composition properties *}
   1.650 +(* ============================== *)
   1.651 +lemma cp1:
   1.652 +  fixes pi1::"'x prm"
   1.653 +  and   pi2::"'y prm"
   1.654 +  and   x  ::"'a"
   1.655 +  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
   1.656 +  shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)"
   1.657 +  using cp by (simp add: cp_def)
   1.658 +
   1.659 +lemma cp_pt_inst:
   1.660 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.661 +  and     at: "at TYPE('x)"
   1.662 +  shows "cp TYPE('a) TYPE('x) TYPE('x)"
   1.663 +apply(auto simp add: cp_def pt2[OF pt,symmetric])
   1.664 +apply(rule pt3[OF pt])
   1.665 +apply(rule at_ds8[OF at])
   1.666 +done
   1.667 +
   1.668 +section {* permutation type instances *}
   1.669 +(* ===================================*)
   1.670 +
   1.671 +lemma pt_set_inst:
   1.672 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.673 +  shows  "pt TYPE('a set) TYPE('x)"
   1.674 +apply(simp add: pt_def)
   1.675 +apply(simp_all add: perm_set_def)
   1.676 +apply(simp add: pt1[OF pt])
   1.677 +apply(force simp add: pt2[OF pt] pt3[OF pt])
   1.678 +done
   1.679 +
   1.680 +lemma pt_list_nil: 
   1.681 +  fixes xs :: "'a list"
   1.682 +  assumes pt: "pt TYPE('a) TYPE ('x)"
   1.683 +  shows "([]::'x prm)\<bullet>xs = xs" 
   1.684 +apply(induct_tac xs)
   1.685 +apply(simp_all add: pt1[OF pt])
   1.686 +done
   1.687 +
   1.688 +lemma pt_list_append: 
   1.689 +  fixes pi1 :: "'x prm"
   1.690 +  and   pi2 :: "'x prm"
   1.691 +  and   xs  :: "'a list"
   1.692 +  assumes pt: "pt TYPE('a) TYPE ('x)"
   1.693 +  shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)"
   1.694 +apply(induct_tac xs)
   1.695 +apply(simp_all add: pt2[OF pt])
   1.696 +done
   1.697 +
   1.698 +lemma pt_list_prm_eq: 
   1.699 +  fixes pi1 :: "'x prm"
   1.700 +  and   pi2 :: "'x prm"
   1.701 +  and   xs  :: "'a list"
   1.702 +  assumes pt: "pt TYPE('a) TYPE ('x)"
   1.703 +  shows "pi1 \<sim> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
   1.704 +apply(induct_tac xs)
   1.705 +apply(simp_all add: prm_eq_def pt3[OF pt])
   1.706 +done
   1.707 +
   1.708 +lemma pt_list_inst:
   1.709 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.710 +  shows  "pt TYPE('a list) TYPE('x)"
   1.711 +apply(auto simp only: pt_def)
   1.712 +apply(rule pt_list_nil[OF pt])
   1.713 +apply(rule pt_list_append[OF pt])
   1.714 +apply(rule pt_list_prm_eq[OF pt],assumption)
   1.715 +done
   1.716 +
   1.717 +lemma pt_unit_inst:
   1.718 +  shows  "pt TYPE(unit) TYPE('x)"
   1.719 +  by (simp add: pt_def)
   1.720 +
   1.721 +lemma pt_prod_inst:
   1.722 +  assumes pta: "pt TYPE('a) TYPE('x)"
   1.723 +  and     ptb: "pt TYPE('b) TYPE('x)"
   1.724 +  shows  "pt TYPE('a \<times> 'b) TYPE('x)"
   1.725 +  apply(auto simp add: pt_def)
   1.726 +  apply(rule pt1[OF pta])
   1.727 +  apply(rule pt1[OF ptb])
   1.728 +  apply(rule pt2[OF pta])
   1.729 +  apply(rule pt2[OF ptb])
   1.730 +  apply(rule pt3[OF pta],assumption)
   1.731 +  apply(rule pt3[OF ptb],assumption)
   1.732 +  done
   1.733 +
   1.734 +lemma pt_fun_inst:
   1.735 +  assumes pta: "pt TYPE('a) TYPE('x)"
   1.736 +  and     ptb: "pt TYPE('b) TYPE('x)"
   1.737 +  and     at:  "at TYPE('x)"
   1.738 +  shows  "pt TYPE('a\<Rightarrow>'b) TYPE('x)"
   1.739 +apply(auto simp only: pt_def)
   1.740 +apply(simp_all add: perm_fun_def)
   1.741 +apply(simp add: pt1[OF pta] pt1[OF ptb])
   1.742 +apply(simp add: pt2[OF pta] pt2[OF ptb])
   1.743 +apply(subgoal_tac "(rev pi1) \<sim> (rev pi2)")(*A*)
   1.744 +apply(simp add: pt3[OF pta] pt3[OF ptb])
   1.745 +(*A*)
   1.746 +apply(simp add: at_prm_rev_eq[OF at])
   1.747 +done
   1.748 +
   1.749 +lemma pt_option_inst:
   1.750 +  assumes pta: "pt TYPE('a) TYPE('x)"
   1.751 +  shows  "pt TYPE('a option) TYPE('x)"
   1.752 +apply(auto simp only: pt_def)
   1.753 +apply(case_tac "x")
   1.754 +apply(simp_all add: pt1[OF pta])
   1.755 +apply(case_tac "x")
   1.756 +apply(simp_all add: pt2[OF pta])
   1.757 +apply(case_tac "x")
   1.758 +apply(simp_all add: pt3[OF pta])
   1.759 +done
   1.760 +
   1.761 +lemma pt_noption_inst:
   1.762 +  assumes pta: "pt TYPE('a) TYPE('x)"
   1.763 +  shows  "pt TYPE('a nOption) TYPE('x)"
   1.764 +apply(auto simp only: pt_def)
   1.765 +apply(case_tac "x")
   1.766 +apply(simp_all add: pt1[OF pta])
   1.767 +apply(case_tac "x")
   1.768 +apply(simp_all add: pt2[OF pta])
   1.769 +apply(case_tac "x")
   1.770 +apply(simp_all add: pt3[OF pta])
   1.771 +done
   1.772 +
   1.773 +lemma pt_bool_inst:
   1.774 +  shows  "pt TYPE(bool) TYPE('x)"
   1.775 +  apply(auto simp add: pt_def)
   1.776 +  apply(case_tac "x=True", simp add: perm_bool_def, simp add: perm_bool_def)+
   1.777 +  done
   1.778 +
   1.779 +lemma pt_prm_inst:
   1.780 +  assumes at: "at TYPE('x)"
   1.781 +  shows  "pt TYPE('x prm) TYPE('x)"
   1.782 +apply(rule pt_list_inst)
   1.783 +apply(rule pt_prod_inst)
   1.784 +apply(rule at_pt_inst[OF at])+
   1.785 +done
   1.786 +
   1.787 +section {* further lemmas for permutation types *}
   1.788 +(*==============================================*)
   1.789 +
   1.790 +lemma pt_rev_pi:
   1.791 +  fixes pi :: "'x prm"
   1.792 +  and   x  :: "'a"
   1.793 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.794 +  and     at: "at TYPE('x)"
   1.795 +  shows "(rev pi)\<bullet>(pi\<bullet>x) = x"
   1.796 +proof -
   1.797 +  have "((rev pi)@pi) \<sim> ([]::'x prm)" by (simp add: at_ds7[OF at])
   1.798 +  hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 
   1.799 +  thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt])
   1.800 +qed
   1.801 +
   1.802 +lemma pt_pi_rev:
   1.803 +  fixes pi :: "'x prm"
   1.804 +  and   x  :: "'a"
   1.805 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.806 +  and     at: "at TYPE('x)"
   1.807 +  shows "pi\<bullet>((rev pi)\<bullet>x) = x"
   1.808 +  by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified])
   1.809 +
   1.810 +lemma pt_bij1: 
   1.811 +  fixes pi :: "'x prm"
   1.812 +  and   x  :: "'a"
   1.813 +  and   y  :: "'a"
   1.814 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.815 +  and     at: "at TYPE('x)"
   1.816 +  and     a:  "(pi\<bullet>x) = y"
   1.817 +  shows   "x=(rev pi)\<bullet>y"
   1.818 +proof -
   1.819 +  from a have "y=(pi\<bullet>x)" by (rule sym)
   1.820 +  thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at])
   1.821 +qed
   1.822 +
   1.823 +lemma pt_bij2: 
   1.824 +  fixes pi :: "'x prm"
   1.825 +  and   x  :: "'a"
   1.826 +  and   y  :: "'a"
   1.827 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.828 +  and     at: "at TYPE('x)"
   1.829 +  and     a:  "x = (rev pi)\<bullet>y"
   1.830 +  shows   "(pi\<bullet>x)=y"
   1.831 +  using a by (simp add: pt_pi_rev[OF pt, OF at])
   1.832 +
   1.833 +lemma pt_bij:
   1.834 +  fixes pi :: "'x prm"
   1.835 +  and   x  :: "'a"
   1.836 +  and   y  :: "'a"
   1.837 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.838 +  and     at: "at TYPE('x)"
   1.839 +  shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
   1.840 +proof 
   1.841 +  assume "pi\<bullet>x = pi\<bullet>y" 
   1.842 +  hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 
   1.843 +  thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at])
   1.844 +next
   1.845 +  assume "x=y"
   1.846 +  thus "pi\<bullet>x = pi\<bullet>y" by simp
   1.847 +qed
   1.848 +
   1.849 +lemma pt_bij3:
   1.850 +  fixes pi :: "'x prm"
   1.851 +  and   x  :: "'a"
   1.852 +  and   y  :: "'a"
   1.853 +  assumes a:  "x=y"
   1.854 +  shows "(pi\<bullet>x = pi\<bullet>y)"
   1.855 +using a by simp 
   1.856 +
   1.857 +lemma pt_bij4:
   1.858 +  fixes pi :: "'x prm"
   1.859 +  and   x  :: "'a"
   1.860 +  and   y  :: "'a"
   1.861 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.862 +  and     at: "at TYPE('x)"
   1.863 +  and     a:  "pi\<bullet>x = pi\<bullet>y"
   1.864 +  shows "x = y"
   1.865 +using a by (simp add: pt_bij[OF pt, OF at])
   1.866 +
   1.867 +lemma pt_swap_bij:
   1.868 +  fixes a  :: "'x"
   1.869 +  and   b  :: "'x"
   1.870 +  and   x  :: "'a"
   1.871 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.872 +  and     at: "at TYPE('x)"
   1.873 +  shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x"
   1.874 +  by (rule pt_bij2[OF pt, OF at], simp)
   1.875 +
   1.876 +lemma pt_set_bij1:
   1.877 +  fixes pi :: "'x prm"
   1.878 +  and   x  :: "'a"
   1.879 +  and   X  :: "'a set"
   1.880 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.881 +  and     at: "at TYPE('x)"
   1.882 +  shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
   1.883 +  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
   1.884 +
   1.885 +lemma pt_set_bij1a:
   1.886 +  fixes pi :: "'x prm"
   1.887 +  and   x  :: "'a"
   1.888 +  and   X  :: "'a set"
   1.889 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.890 +  and     at: "at TYPE('x)"
   1.891 +  shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
   1.892 +  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
   1.893 +
   1.894 +lemma pt_set_bij:
   1.895 +  fixes pi :: "'x prm"
   1.896 +  and   x  :: "'a"
   1.897 +  and   X  :: "'a set"
   1.898 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.899 +  and     at: "at TYPE('x)"
   1.900 +  shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
   1.901 +  by (simp add: perm_set_def pt_set_bij1[OF pt, OF at] pt_bij[OF pt, OF at])
   1.902 +
   1.903 +lemma pt_set_bij2:
   1.904 +  fixes pi :: "'x prm"
   1.905 +  and   x  :: "'a"
   1.906 +  and   X  :: "'a set"
   1.907 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.908 +  and     at: "at TYPE('x)"
   1.909 +  and     a:  "x\<in>X"
   1.910 +  shows "(pi\<bullet>x)\<in>(pi\<bullet>X)"
   1.911 +  using a by (simp add: pt_set_bij[OF pt, OF at])
   1.912 +
   1.913 +lemma pt_set_bij3:
   1.914 +  fixes pi :: "'x prm"
   1.915 +  and   x  :: "'a"
   1.916 +  and   X  :: "'a set"
   1.917 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.918 +  and     at: "at TYPE('x)"
   1.919 +  shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
   1.920 +apply(case_tac "x\<in>X = True")
   1.921 +apply(auto)
   1.922 +done
   1.923 +
   1.924 +lemma pt_list_set_pi:
   1.925 +  fixes pi :: "'x prm"
   1.926 +  and   xs :: "'a list"
   1.927 +  assumes pt: "pt TYPE('a) TYPE('x)"
   1.928 +  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
   1.929 +by (induct xs, auto simp add: perm_set_def pt1[OF pt])
   1.930 +
   1.931 +-- "some helper lemmas for the pt_perm_supp_ineq lemma"
   1.932 +lemma Collect_permI: 
   1.933 +  fixes pi :: "'x prm"
   1.934 +  and   x  :: "'a"
   1.935 +  assumes a: "\<forall>x. (P1 x = P2 x)" 
   1.936 +  shows "{pi\<bullet>x| x. P1 x} = {pi\<bullet>x| x. P2 x}"
   1.937 +  using a by force
   1.938 +
   1.939 +lemma Infinite_cong:
   1.940 +  assumes a: "X = Y"
   1.941 +  shows "infinite X = infinite Y"
   1.942 +  using a by (simp)
   1.943 +
   1.944 +lemma pt_set_eq_ineq:
   1.945 +  fixes pi :: "'y prm"
   1.946 +  assumes pt: "pt TYPE('x) TYPE('y)"
   1.947 +  and     at: "at TYPE('y)"
   1.948 +  shows "{pi\<bullet>x| x::'x. P x} = {x::'x. P ((rev pi)\<bullet>x)}"
   1.949 +  by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
   1.950 +
   1.951 +lemma pt_inject_on_ineq:
   1.952 +  fixes X  :: "'y set"
   1.953 +  and   pi :: "'x prm"
   1.954 +  assumes pt: "pt TYPE('y) TYPE('x)"
   1.955 +  and     at: "at TYPE('x)"
   1.956 +  shows "inj_on (perm pi) X"
   1.957 +proof (unfold inj_on_def, intro strip)
   1.958 +  fix x::"'y" and y::"'y"
   1.959 +  assume "pi\<bullet>x = pi\<bullet>y"
   1.960 +  thus "x=y" by (simp add: pt_bij[OF pt, OF at])
   1.961 +qed
   1.962 +
   1.963 +lemma pt_set_finite_ineq: 
   1.964 +  fixes X  :: "'x set"
   1.965 +  and   pi :: "'y prm"
   1.966 +  assumes pt: "pt TYPE('x) TYPE('y)"
   1.967 +  and     at: "at TYPE('y)"
   1.968 +  shows "finite (pi\<bullet>X) = finite X"
   1.969 +proof -
   1.970 +  have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
   1.971 +  show ?thesis
   1.972 +  proof (rule iffI)
   1.973 +    assume "finite (pi\<bullet>X)"
   1.974 +    hence "finite (perm pi ` X)" using image by (simp)
   1.975 +    thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD)
   1.976 +  next
   1.977 +    assume "finite X"
   1.978 +    hence "finite (perm pi ` X)" by (rule finite_imageI)
   1.979 +    thus "finite (pi\<bullet>X)" using image by (simp)
   1.980 +  qed
   1.981 +qed
   1.982 +
   1.983 +lemma pt_set_infinite_ineq: 
   1.984 +  fixes X  :: "'x set"
   1.985 +  and   pi :: "'y prm"
   1.986 +  assumes pt: "pt TYPE('x) TYPE('y)"
   1.987 +  and     at: "at TYPE('y)"
   1.988 +  shows "infinite (pi\<bullet>X) = infinite X"
   1.989 +using pt at by (simp add: pt_set_finite_ineq)
   1.990 +
   1.991 +lemma pt_perm_supp_ineq:
   1.992 +  fixes  pi  :: "'x prm"
   1.993 +  and    x   :: "'a"
   1.994 +  assumes pta: "pt TYPE('a) TYPE('x)"
   1.995 +  and     ptb: "pt TYPE('y) TYPE('x)"
   1.996 +  and     at:  "at TYPE('x)"
   1.997 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
   1.998 +  shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
   1.999 +proof -
  1.1000 +  have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
  1.1001 +  also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}" 
  1.1002 +  proof (rule Collect_permI, rule allI, rule iffI)
  1.1003 +    fix a
  1.1004 +    assume "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}"
  1.1005 +    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  1.1006 +    thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_def)
  1.1007 +  next
  1.1008 +    fix a
  1.1009 +    assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
  1.1010 +    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
  1.1011 +    thus "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}" 
  1.1012 +      by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  1.1013 +  qed
  1.1014 +  also have "\<dots> = {a. infinite {b::'y. [((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x \<noteq> x}}" 
  1.1015 +    by (simp add: pt_set_eq_ineq[OF ptb, OF at])
  1.1016 +  also have "\<dots> = {a. infinite {b. pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> (pi\<bullet>x)}}"
  1.1017 +    by (simp add: pt_bij[OF pta, OF at])
  1.1018 +  also have "\<dots> = {a. infinite {b. [(a,b)]\<bullet>(pi\<bullet>x) \<noteq> (pi\<bullet>x)}}"
  1.1019 +  proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong)
  1.1020 +    fix a::"'y" and b::"'y"
  1.1021 +    have "pi\<bullet>(([((rev pi)\<bullet>a,(rev pi)\<bullet>b)])\<bullet>x) = [(a,b)]\<bullet>(pi\<bullet>x)"
  1.1022 +      by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at])
  1.1023 +    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
  1.1024 +  qed
  1.1025 +  finally show "?LHS = ?RHS" by (simp add: supp_def) 
  1.1026 +qed
  1.1027 +
  1.1028 +lemma pt_perm_supp:
  1.1029 +  fixes  pi  :: "'x prm"
  1.1030 +  and    x   :: "'a"
  1.1031 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1032 +  and     at: "at TYPE('x)"
  1.1033 +  shows "(pi\<bullet>((supp x)::'x set)) = supp (pi\<bullet>x)"
  1.1034 +apply(rule pt_perm_supp_ineq)
  1.1035 +apply(rule pt)
  1.1036 +apply(rule at_pt_inst)
  1.1037 +apply(rule at)+
  1.1038 +apply(rule cp_pt_inst)
  1.1039 +apply(rule pt)
  1.1040 +apply(rule at)
  1.1041 +done
  1.1042 +
  1.1043 +lemma pt_supp_finite_pi:
  1.1044 +  fixes  pi  :: "'x prm"
  1.1045 +  and    x   :: "'a"
  1.1046 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1047 +  and     at: "at TYPE('x)"
  1.1048 +  and     f: "finite ((supp x)::'x set)"
  1.1049 +  shows "finite ((supp (pi\<bullet>x))::'x set)"
  1.1050 +apply(simp add: pt_perm_supp[OF pt, OF at, symmetric])
  1.1051 +apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at])
  1.1052 +apply(rule f)
  1.1053 +done
  1.1054 +
  1.1055 +lemma pt_fresh_left_ineq:  
  1.1056 +  fixes  pi :: "'x prm"
  1.1057 +  and     x :: "'a"
  1.1058 +  and     a :: "'y"
  1.1059 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1060 +  and     ptb: "pt TYPE('y) TYPE('x)"
  1.1061 +  and     at:  "at TYPE('x)"
  1.1062 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1.1063 +  shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
  1.1064 +apply(simp add: fresh_def)
  1.1065 +apply(simp add: pt_set_bij1[OF ptb, OF at])
  1.1066 +apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
  1.1067 +done
  1.1068 +
  1.1069 +lemma pt_fresh_right_ineq:  
  1.1070 +  fixes  pi :: "'x prm"
  1.1071 +  and     x :: "'a"
  1.1072 +  and     a :: "'y"
  1.1073 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1074 +  and     ptb: "pt TYPE('y) TYPE('x)"
  1.1075 +  and     at:  "at TYPE('x)"
  1.1076 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1.1077 +  shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
  1.1078 +apply(simp add: fresh_def)
  1.1079 +apply(simp add: pt_set_bij1[OF ptb, OF at])
  1.1080 +apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
  1.1081 +done
  1.1082 +
  1.1083 +lemma pt_fresh_bij_ineq:
  1.1084 +  fixes  pi :: "'x prm"
  1.1085 +  and     x :: "'a"
  1.1086 +  and     a :: "'y"
  1.1087 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1088 +  and     ptb: "pt TYPE('y) TYPE('x)"
  1.1089 +  and     at:  "at TYPE('x)"
  1.1090 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1.1091 +  shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
  1.1092 +apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  1.1093 +apply(simp add: pt_rev_pi[OF ptb, OF at])
  1.1094 +done
  1.1095 +
  1.1096 +lemma pt_fresh_left:  
  1.1097 +  fixes  pi :: "'x prm"
  1.1098 +  and     x :: "'a"
  1.1099 +  and     a :: "'x"
  1.1100 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1101 +  and     at: "at TYPE('x)"
  1.1102 +  shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
  1.1103 +apply(rule pt_fresh_left_ineq)
  1.1104 +apply(rule pt)
  1.1105 +apply(rule at_pt_inst)
  1.1106 +apply(rule at)+
  1.1107 +apply(rule cp_pt_inst)
  1.1108 +apply(rule pt)
  1.1109 +apply(rule at)
  1.1110 +done
  1.1111 +
  1.1112 +lemma pt_fresh_right:  
  1.1113 +  fixes  pi :: "'x prm"
  1.1114 +  and     x :: "'a"
  1.1115 +  and     a :: "'x"
  1.1116 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1117 +  and     at: "at TYPE('x)"
  1.1118 +  shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
  1.1119 +apply(rule pt_fresh_right_ineq)
  1.1120 +apply(rule pt)
  1.1121 +apply(rule at_pt_inst)
  1.1122 +apply(rule at)+
  1.1123 +apply(rule cp_pt_inst)
  1.1124 +apply(rule pt)
  1.1125 +apply(rule at)
  1.1126 +done
  1.1127 +
  1.1128 +lemma pt_fresh_bij:
  1.1129 +  fixes  pi :: "'x prm"
  1.1130 +  and     x :: "'a"
  1.1131 +  and     a :: "'x"
  1.1132 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1133 +  and     at: "at TYPE('x)"
  1.1134 +  shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
  1.1135 +apply(rule pt_fresh_bij_ineq)
  1.1136 +apply(rule pt)
  1.1137 +apply(rule at_pt_inst)
  1.1138 +apply(rule at)+
  1.1139 +apply(rule cp_pt_inst)
  1.1140 +apply(rule pt)
  1.1141 +apply(rule at)
  1.1142 +done
  1.1143 +
  1.1144 +lemma pt_fresh_bij1:
  1.1145 +  fixes  pi :: "'x prm"
  1.1146 +  and     x :: "'a"
  1.1147 +  and     a :: "'x"
  1.1148 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1149 +  and     at: "at TYPE('x)"
  1.1150 +  and     a:  "a\<sharp>x"
  1.1151 +  shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
  1.1152 +using a by (simp add: pt_fresh_bij[OF pt, OF at])
  1.1153 +
  1.1154 +lemma pt_perm_fresh1:
  1.1155 +  fixes a :: "'x"
  1.1156 +  and   b :: "'x"
  1.1157 +  and   x :: "'a"
  1.1158 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1159 +  and     at: "at TYPE ('x)"
  1.1160 +  and     a1: "\<not>(a\<sharp>x)"
  1.1161 +  and     a2: "b\<sharp>x"
  1.1162 +  shows "[(a,b)]\<bullet>x \<noteq> x"
  1.1163 +proof
  1.1164 +  assume neg: "[(a,b)]\<bullet>x = x"
  1.1165 +  from a1 have a1':"a\<in>(supp x)" by (simp add: fresh_def) 
  1.1166 +  from a2 have a2':"b\<notin>(supp x)" by (simp add: fresh_def) 
  1.1167 +  from a1' a2' have a3: "a\<noteq>b" by force
  1.1168 +  from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))" 
  1.1169 +    by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at])
  1.1170 +  hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_append[OF at] at_calc[OF at])
  1.1171 +  hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at])
  1.1172 +  with a2' neg show False by simp
  1.1173 +qed
  1.1174 +
  1.1175 +-- "three helper lemmas for the perm_fresh_fresh-lemma"
  1.1176 +lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
  1.1177 +  by (auto)
  1.1178 +
  1.1179 +lemma infinite_or_neg_infinite:
  1.1180 +  assumes h:"infinite (UNIV::'a set)"
  1.1181 +  shows "infinite {b::'a. P b} \<or> infinite {b::'a. \<not> P b}"
  1.1182 +proof (subst comprehension_neg_UNIV, case_tac "finite {b. P b}")
  1.1183 +  assume j:"finite {b::'a. P b}"
  1.1184 +  have "infinite ((UNIV::'a set) - {b::'a. P b})"
  1.1185 +    using Diff_infinite_finite[OF j h] by auto
  1.1186 +  thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" ..
  1.1187 +next
  1.1188 +  assume j:"infinite {b::'a. P b}"
  1.1189 +  thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" by simp
  1.1190 +qed
  1.1191 +
  1.1192 +--"the co-set of a finite set is infinte"
  1.1193 +lemma finite_infinite:
  1.1194 +  assumes a: "finite {b::'x. P b}"
  1.1195 +  and     b: "infinite (UNIV::'x set)"        
  1.1196 +  shows "infinite {b. \<not>P b}"
  1.1197 +  using a and infinite_or_neg_infinite[OF b] by simp
  1.1198 +
  1.1199 +lemma pt_fresh_fresh:
  1.1200 +  fixes   x :: "'a"
  1.1201 +  and     a :: "'x"
  1.1202 +  and     b :: "'x"
  1.1203 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1204 +  and     at: "at TYPE ('x)"
  1.1205 +  and     a1: "a\<sharp>x" and a2: "b\<sharp>x" 
  1.1206 +  shows "[(a,b)]\<bullet>x=x"
  1.1207 +proof (cases "a=b")
  1.1208 +  assume c1: "a=b"
  1.1209 +  have "[(a,a)] \<sim> []" by (rule at_ds1[OF at])
  1.1210 +  hence "[(a,b)] \<sim> []" using c1 by simp
  1.1211 +  hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt])
  1.1212 +  thus ?thesis by (simp only: pt1[OF pt])
  1.1213 +next
  1.1214 +  assume c2: "a\<noteq>b"
  1.1215 +  from a1 have f1: "finite {c. [(a,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
  1.1216 +  from a2 have f2: "finite {c. [(b,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
  1.1217 +  from f1 and f2 have f3: "finite {c. perm [(a,c)] x \<noteq> x \<or> perm [(b,c)] x \<noteq> x}" 
  1.1218 +    by (force simp only: Collect_disj_eq)
  1.1219 +  have "infinite {c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}" 
  1.1220 +    by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
  1.1221 +  hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" 
  1.1222 +    by (force dest: Diff_infinite_finite)
  1.1223 +  hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}" 
  1.1224 +    by (auto iff del: finite_Diff_insert Diff_eq_empty_iff)
  1.1225 +  hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
  1.1226 +  then obtain c 
  1.1227 +    where eq1: "[(a,c)]\<bullet>x = x" 
  1.1228 +      and eq2: "[(b,c)]\<bullet>x = x" 
  1.1229 +      and ineq: "a\<noteq>c \<and> b\<noteq>c"
  1.1230 +    by (force)
  1.1231 +  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>x)) = x" by simp 
  1.1232 +  hence eq3: "[(a,c),(b,c),(a,c)]\<bullet>x = x" by (simp add: pt2[OF pt,symmetric])
  1.1233 +  from c2 ineq have "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]" by (simp add: at_ds3[OF at])
  1.1234 +  hence "[(a,c),(b,c),(a,c)]\<bullet>x = [(a,b)]\<bullet>x" by (rule pt3[OF pt])
  1.1235 +  thus ?thesis using eq3 by simp
  1.1236 +qed
  1.1237 +
  1.1238 +lemma pt_perm_compose:
  1.1239 +  fixes pi1 :: "'x prm"
  1.1240 +  and   pi2 :: "'x prm"
  1.1241 +  and   x  :: "'a"
  1.1242 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1243 +  and     at: "at TYPE('x)"
  1.1244 +  shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)" 
  1.1245 +proof -
  1.1246 +  have "(pi2@pi1) \<sim> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
  1.1247 +  hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
  1.1248 +  thus ?thesis by (simp add: pt2[OF pt])
  1.1249 +qed
  1.1250 +
  1.1251 +lemma pt_perm_compose_rev:
  1.1252 +  fixes pi1 :: "'x prm"
  1.1253 +  and   pi2 :: "'x prm"
  1.1254 +  and   x  :: "'a"
  1.1255 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1256 +  and     at: "at TYPE('x)"
  1.1257 +  shows "(rev pi2)\<bullet>((rev pi1)\<bullet>x) = (rev pi1)\<bullet>(rev (pi1\<bullet>pi2)\<bullet>x)" 
  1.1258 +proof -
  1.1259 +  have "((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at])
  1.1260 +  hence "((rev pi2)@(rev pi1))\<bullet>x = ((rev pi1)@(rev (pi1\<bullet>pi2)))\<bullet>x" by (rule pt3[OF pt])
  1.1261 +  thus ?thesis by (simp add: pt2[OF pt])
  1.1262 +qed
  1.1263 +
  1.1264 +section {* facts about supports *}
  1.1265 +(*==============================*)
  1.1266 +
  1.1267 +lemma supports_subset:
  1.1268 +  fixes x  :: "'a"
  1.1269 +  and   S1 :: "'x set"
  1.1270 +  and   S2 :: "'x set"
  1.1271 +  assumes  a: "S1 supports x"
  1.1272 +  and      b: "S1\<subseteq>S2"
  1.1273 +  shows "S2 supports x"
  1.1274 +  using a b
  1.1275 +  by (force simp add: "op supports_def")
  1.1276 +
  1.1277 +lemma supp_supports:
  1.1278 +  fixes x :: "'a"
  1.1279 +  assumes  pt: "pt TYPE('a) TYPE('x)"
  1.1280 +  and      at: "at TYPE ('x)"
  1.1281 +  shows "((supp x)::'x set) supports x"
  1.1282 +proof (unfold "op supports_def", intro strip)
  1.1283 +  fix a b
  1.1284 +  assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
  1.1285 +  hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
  1.1286 +  thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at])
  1.1287 +qed
  1.1288 +
  1.1289 +lemma supp_is_subset:
  1.1290 +  fixes S :: "'x set"
  1.1291 +  and   x :: "'a"
  1.1292 +  assumes a1: "S supports x"
  1.1293 +  and     a2: "finite S"
  1.1294 +  shows "(supp x)\<subseteq>S"
  1.1295 +proof (rule ccontr)
  1.1296 +  assume "\<not>(supp x \<subseteq> S)"
  1.1297 +  hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
  1.1298 +  then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
  1.1299 +  from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold "op supports_def", force)
  1.1300 +  with a1 have "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by (unfold "op supports_def", force)
  1.1301 +  with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
  1.1302 +  hence "a\<notin>(supp x)" by (unfold supp_def, auto)
  1.1303 +  with b1 show False by simp
  1.1304 +qed
  1.1305 +
  1.1306 +lemma supports_finite:
  1.1307 +  fixes S :: "'x set"
  1.1308 +  and   x :: "'a"
  1.1309 +  assumes a1: "S supports x"
  1.1310 +  and     a2: "finite S"
  1.1311 +  shows "finite ((supp x)::'x set)"
  1.1312 +proof -
  1.1313 +  have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1.1314 +  thus ?thesis using a2 by (simp add: finite_subset)
  1.1315 +qed
  1.1316 +  
  1.1317 +lemma supp_is_inter:
  1.1318 +  fixes  x :: "'a"
  1.1319 +  assumes  pt: "pt TYPE('a) TYPE('x)"
  1.1320 +  and      at: "at TYPE ('x)"
  1.1321 +  and      fs: "fs TYPE('a) TYPE('x)"
  1.1322 +  shows "((supp x)::'x set) = (\<Inter> {S. finite S \<and> S supports x})"
  1.1323 +proof (rule equalityI)
  1.1324 +  show "((supp x)::'x set) \<subseteq> (\<Inter> {S. finite S \<and> S supports x})"
  1.1325 +  proof (clarify)
  1.1326 +    fix S c
  1.1327 +    assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
  1.1328 +    hence  "((supp x)::'x set)\<subseteq>S" by (simp add: supp_is_subset) 
  1.1329 +    with b show "c\<in>S" by force
  1.1330 +  qed
  1.1331 +next
  1.1332 +  show "(\<Inter> {S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
  1.1333 +  proof (clarify, simp)
  1.1334 +    fix c
  1.1335 +    assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
  1.1336 +    have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
  1.1337 +    with d fs1[OF fs] show "c\<in>supp x" by force
  1.1338 +  qed
  1.1339 +qed
  1.1340 +    
  1.1341 +lemma supp_is_least_supports:
  1.1342 +  fixes S :: "'x set"
  1.1343 +  and   x :: "'a"
  1.1344 +  assumes  pt: "pt TYPE('a) TYPE('x)"
  1.1345 +  and      at: "at TYPE ('x)"
  1.1346 +  and      a1: "S supports x"
  1.1347 +  and      a2: "finite S"
  1.1348 +  and      a3: "\<forall>S'. (finite S' \<and> S' supports x) \<longrightarrow> S\<subseteq>S'"
  1.1349 +  shows "S = (supp x)"
  1.1350 +proof (rule equalityI)
  1.1351 +  show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1.1352 +next
  1.1353 +  have s1: "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
  1.1354 +  have "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1.1355 +  hence "finite ((supp x)::'x set)" using a2 by (simp add: finite_subset)
  1.1356 +  with s1 a3 show "S\<subseteq>supp x" by force
  1.1357 +qed
  1.1358 +
  1.1359 +lemma supports_set:
  1.1360 +  fixes S :: "'x set"
  1.1361 +  and   X :: "'a set"
  1.1362 +  assumes  pt: "pt TYPE('a) TYPE('x)"
  1.1363 +  and      at: "at TYPE ('x)"
  1.1364 +  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)"
  1.1365 +  shows  "S supports X"
  1.1366 +using a
  1.1367 +apply(auto simp add: "op supports_def")
  1.1368 +apply(simp add: pt_set_bij1a[OF pt, OF at])
  1.1369 +apply(force simp add: pt_swap_bij[OF pt, OF at])
  1.1370 +apply(simp add: pt_set_bij1a[OF pt, OF at])
  1.1371 +done
  1.1372 +
  1.1373 +lemma supports_fresh:
  1.1374 +  fixes S :: "'x set"
  1.1375 +  and   a :: "'x"
  1.1376 +  and   x :: "'a"
  1.1377 +  assumes a1: "S supports x"
  1.1378 +  and     a2: "finite S"
  1.1379 +  and     a3: "a\<notin>S"
  1.1380 +  shows "a\<sharp>x"
  1.1381 +proof (simp add: fresh_def)
  1.1382 +  have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1.1383 +  thus "a\<notin>(supp x)" using a3 by force
  1.1384 +qed
  1.1385 +
  1.1386 +lemma at_fin_set_supports:
  1.1387 +  fixes X::"'x set"
  1.1388 +  assumes at: "at TYPE('x)"
  1.1389 +  shows "X supports X"
  1.1390 +proof (simp add: "op supports_def", intro strip)
  1.1391 +  fix a b
  1.1392 +  assume "a\<notin>X \<and> b\<notin>X"
  1.1393 +  thus "[(a,b)]\<bullet>X = X" by (force simp add: perm_set_def at_calc[OF at])
  1.1394 +qed
  1.1395 +
  1.1396 +lemma at_fin_set_supp:
  1.1397 +  fixes X::"'x set"
  1.1398 +  assumes at: "at TYPE('x)"
  1.1399 +  and     fs: "finite X"
  1.1400 +  shows "(supp X) = X"
  1.1401 +proof -
  1.1402 +  have pt_set: "pt TYPE('x set) TYPE('x)" 
  1.1403 +    by (rule pt_set_inst[OF at_pt_inst[OF at]])
  1.1404 +  have X_supports_X: "X supports X" by (rule at_fin_set_supports[OF at])
  1.1405 +  show ?thesis using  pt_set at X_supports_X fs
  1.1406 +  proof (rule supp_is_least_supports[symmetric])
  1.1407 +    show "\<forall>S'. finite S' \<and> S' supports X \<longrightarrow> X \<subseteq> S'"
  1.1408 +    proof (auto)
  1.1409 +      fix S'::"'x set" and x::"'x"
  1.1410 +      assume f: "finite S'"
  1.1411 +      and    s: "S' supports X"
  1.1412 +      and    e1: "x\<in>X"
  1.1413 +      show "x\<in>S'"
  1.1414 +      proof (rule ccontr)
  1.1415 +	assume e2: "x\<notin>S'"
  1.1416 +	have "\<exists>b. b\<notin>(X\<union>S')" by (force intro: ex_in_inf[OF at] simp only: fs f)
  1.1417 +	then obtain b where b1: "b\<notin>X" and b2: "b\<notin>S'" by (auto)
  1.1418 +	from s e2 b2 have c1: "[(x,b)]\<bullet>X=X" by (simp add: "op supports_def")
  1.1419 +	from e1 b1 have c2: "[(x,b)]\<bullet>X\<noteq>X" by (force simp add: perm_set_def at_calc[OF at])
  1.1420 +	show "False" using c1 c2 by simp
  1.1421 +      qed
  1.1422 +    qed
  1.1423 +  qed
  1.1424 +qed
  1.1425 +
  1.1426 +section {* Permutations acting on Functions *}
  1.1427 +(*==========================================*)
  1.1428 +
  1.1429 +lemma pt_fun_app_eq:
  1.1430 +  fixes f  :: "'a\<Rightarrow>'b"
  1.1431 +  and   x  :: "'a"
  1.1432 +  and   pi :: "'x prm"
  1.1433 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1434 +  and     at: "at TYPE('x)"
  1.1435 +  shows "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)"
  1.1436 +  by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at])
  1.1437 +
  1.1438 +
  1.1439 +--"sometimes pt_fun_app_eq does to much; this lemma 'corrects it'"
  1.1440 +lemma pt_perm:
  1.1441 +  fixes x  :: "'a"
  1.1442 +  and   pi1 :: "'x prm"
  1.1443 +  and   pi2 :: "'x prm"
  1.1444 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1445 +  and     at: "at TYPE ('x)"
  1.1446 +  shows "(pi1\<bullet>perm pi2)(pi1\<bullet>x) = pi1\<bullet>(pi2\<bullet>x)" 
  1.1447 +  by (simp add: pt_fun_app_eq[OF pt, OF at])
  1.1448 +
  1.1449 +
  1.1450 +lemma pt_fun_eq:
  1.1451 +  fixes f  :: "'a\<Rightarrow>'b"
  1.1452 +  and   pi :: "'x prm"
  1.1453 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1454 +  and     at: "at TYPE('x)"
  1.1455 +  shows "(pi\<bullet>f = f) = (\<forall> x. pi\<bullet>(f x) = f (pi\<bullet>x))" (is "?LHS = ?RHS")
  1.1456 +proof
  1.1457 +  assume a: "?LHS"
  1.1458 +  show "?RHS"
  1.1459 +  proof
  1.1460 +    fix x
  1.1461 +    have "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pt, OF at])
  1.1462 +    also have "\<dots> = f (pi\<bullet>x)" using a by simp
  1.1463 +    finally show "pi\<bullet>(f x) = f (pi\<bullet>x)" by simp
  1.1464 +  qed
  1.1465 +next
  1.1466 +  assume b: "?RHS"
  1.1467 +  show "?LHS"
  1.1468 +  proof (rule ccontr)
  1.1469 +    assume "(pi\<bullet>f) \<noteq> f"
  1.1470 +    hence "\<exists>c. (pi\<bullet>f) c \<noteq> f c" by (simp add: expand_fun_eq)
  1.1471 +    then obtain c where b1: "(pi\<bullet>f) c \<noteq> f c" by force
  1.1472 +    from b have "pi\<bullet>(f ((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" by force
  1.1473 +    hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" 
  1.1474 +      by (simp add: pt_fun_app_eq[OF pt, OF at])
  1.1475 +    hence "(pi\<bullet>f) c = f c" by (simp add: pt_pi_rev[OF pt, OF at])
  1.1476 +    with b1 show "False" by simp
  1.1477 +  qed
  1.1478 +qed
  1.1479 +
  1.1480 +-- "two helper lemmas for the equivariance of functions"
  1.1481 +lemma pt_swap_eq_aux:
  1.1482 +  fixes   y :: "'a"
  1.1483 +  and    pi :: "'x prm"
  1.1484 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1485 +  and     a: "\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y"
  1.1486 +  shows "pi\<bullet>y = y"
  1.1487 +proof(induct pi)
  1.1488 +    case Nil show ?case by (simp add: pt1[OF pt])
  1.1489 +  next
  1.1490 +    case (Cons x xs)
  1.1491 +    have "\<exists>a b. x=(a,b)" by force
  1.1492 +    then obtain a b where p: "x=(a,b)" by force
  1.1493 +    assume i: "xs\<bullet>y = y"
  1.1494 +    have "x#xs = [x]@xs" by simp
  1.1495 +    hence "(x#xs)\<bullet>y = ([x]@xs)\<bullet>y" by simp
  1.1496 +    hence "(x#xs)\<bullet>y = [x]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
  1.1497 +    thus ?case using a i p by (force)
  1.1498 +  qed
  1.1499 +
  1.1500 +lemma pt_swap_eq:
  1.1501 +  fixes   y :: "'a"
  1.1502 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1503 +  shows "(\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y) = (\<forall>pi::'x prm. pi\<bullet>y = y)"
  1.1504 +  by (force intro: pt_swap_eq_aux[OF pt])
  1.1505 +
  1.1506 +lemma pt_eqvt_fun1a:
  1.1507 +  fixes f     :: "'a\<Rightarrow>'b"
  1.1508 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1509 +  and     ptb: "pt TYPE('b) TYPE('x)"
  1.1510 +  and     at:  "at TYPE('x)"
  1.1511 +  and     a:   "((supp f)::'x set)={}"
  1.1512 +  shows "\<forall>(pi::'x prm). pi\<bullet>f = f" 
  1.1513 +proof (intro strip)
  1.1514 +  fix pi
  1.1515 +  have "\<forall>a b. a\<notin>((supp f)::'x set) \<and> b\<notin>((supp f)::'x set) \<longrightarrow> (([(a,b)]\<bullet>f) = f)" 
  1.1516 +    by (intro strip, fold fresh_def, 
  1.1517 +      simp add: pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at],OF at])
  1.1518 +  with a have "\<forall>(a::'x) (b::'x). ([(a,b)]\<bullet>f) = f" by force
  1.1519 +  hence "\<forall>(pi::'x prm). pi\<bullet>f = f" 
  1.1520 +    by (simp add: pt_swap_eq[OF pt_fun_inst[OF pta, OF ptb, OF at]])
  1.1521 +  thus "(pi::'x prm)\<bullet>f = f" by simp
  1.1522 +qed
  1.1523 +
  1.1524 +lemma pt_eqvt_fun1b:
  1.1525 +  fixes f     :: "'a\<Rightarrow>'b"
  1.1526 +  assumes a: "\<forall>(pi::'x prm). pi\<bullet>f = f"
  1.1527 +  shows "((supp f)::'x set)={}"
  1.1528 +using a by (simp add: supp_def)
  1.1529 +
  1.1530 +lemma pt_eqvt_fun1:
  1.1531 +  fixes f     :: "'a\<Rightarrow>'b"
  1.1532 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1533 +  and     ptb: "pt TYPE('b) TYPE('x)"
  1.1534 +  and     at: "at TYPE('x)"
  1.1535 +  shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm). pi\<bullet>f = f)" (is "?LHS = ?RHS")
  1.1536 +by (rule iffI, simp add: pt_eqvt_fun1a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun1b)
  1.1537 +
  1.1538 +lemma pt_eqvt_fun2a:
  1.1539 +  fixes f     :: "'a\<Rightarrow>'b"
  1.1540 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1541 +  and     ptb: "pt TYPE('b) TYPE('x)"
  1.1542 +  and     at: "at TYPE('x)"
  1.1543 +  assumes a: "((supp f)::'x set)={}"
  1.1544 +  shows "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)" 
  1.1545 +proof (intro strip)
  1.1546 +  fix pi x
  1.1547 +  from a have b: "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_eqvt_fun1[OF pta, OF ptb, OF at]) 
  1.1548 +  have "(pi::'x prm)\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pta, OF at]) 
  1.1549 +  with b show "(pi::'x prm)\<bullet>(f x) = f (pi\<bullet>x)" by force 
  1.1550 +qed
  1.1551 +
  1.1552 +lemma pt_eqvt_fun2b:
  1.1553 +  fixes f     :: "'a\<Rightarrow>'b"
  1.1554 +  assumes pt1: "pt TYPE('a) TYPE('x)"
  1.1555 +  and     pt2: "pt TYPE('b) TYPE('x)"
  1.1556 +  and     at: "at TYPE('x)"
  1.1557 +  assumes a: "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)"
  1.1558 +  shows "((supp f)::'x set)={}"
  1.1559 +proof -
  1.1560 +  from a have "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_fun_eq[OF pt1, OF at, symmetric])
  1.1561 +  thus ?thesis by (simp add: supp_def)
  1.1562 +qed
  1.1563 +
  1.1564 +lemma pt_eqvt_fun2:
  1.1565 +  fixes f     :: "'a\<Rightarrow>'b"
  1.1566 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1567 +  and     ptb: "pt TYPE('b) TYPE('x)"
  1.1568 +  and     at: "at TYPE('x)"
  1.1569 +  shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x))" 
  1.1570 +by (rule iffI, 
  1.1571 +    simp add: pt_eqvt_fun2a[OF pta, OF ptb, OF at], 
  1.1572 +    simp add: pt_eqvt_fun2b[OF pta, OF ptb, OF at])
  1.1573 +
  1.1574 +lemma pt_supp_fun_subset:
  1.1575 +  fixes f :: "'a\<Rightarrow>'b"
  1.1576 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1577 +  and     ptb: "pt TYPE('b) TYPE('x)"
  1.1578 +  and     at: "at TYPE('x)" 
  1.1579 +  and     f1: "finite ((supp f)::'x set)"
  1.1580 +  and     f2: "finite ((supp x)::'x set)"
  1.1581 +  shows "supp (f x) \<subseteq> (((supp f)\<union>(supp x))::'x set)"
  1.1582 +proof -
  1.1583 +  have s1: "((supp f)\<union>((supp x)::'x set)) supports (f x)"
  1.1584 +  proof (simp add: "op supports_def", fold fresh_def, auto)
  1.1585 +    fix a::"'x" and b::"'x"
  1.1586 +    assume "a\<sharp>f" and "b\<sharp>f"
  1.1587 +    hence a1: "[(a,b)]\<bullet>f = f" 
  1.1588 +      by (rule pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at], OF at])
  1.1589 +    assume "a\<sharp>x" and "b\<sharp>x"
  1.1590 +    hence a2: "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pta, OF at])
  1.1591 +    from a1 a2 show "[(a,b)]\<bullet>(f x) = (f x)" by (simp add: pt_fun_app_eq[OF pta, OF at])
  1.1592 +  qed
  1.1593 +  from f1 f2 have "finite ((supp f)\<union>((supp x)::'x set))" by force
  1.1594 +  with s1 show ?thesis by (rule supp_is_subset)
  1.1595 +qed
  1.1596 +      
  1.1597 +lemma pt_empty_supp_fun_subset:
  1.1598 +  fixes f :: "'a\<Rightarrow>'b"
  1.1599 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1600 +  and     ptb: "pt TYPE('b) TYPE('x)"
  1.1601 +  and     at:  "at TYPE('x)" 
  1.1602 +  and     e:   "(supp f)=({}::'x set)"
  1.1603 +  shows "supp (f x) \<subseteq> ((supp x)::'x set)"
  1.1604 +proof (unfold supp_def, auto)
  1.1605 +  fix a::"'x"
  1.1606 +  assume a1: "finite {b. [(a, b)]\<bullet>x \<noteq> x}"
  1.1607 +  assume "infinite {b. [(a, b)]\<bullet>(f x) \<noteq> f x}"
  1.1608 +  hence a2: "infinite {b. f ([(a, b)]\<bullet>x) \<noteq> f x}" using e
  1.1609 +    by (simp add: pt_eqvt_fun2[OF pta, OF ptb, OF at])
  1.1610 +  have a3: "{b. f ([(a,b)]\<bullet>x) \<noteq> f x}\<subseteq>{b. [(a,b)]\<bullet>x \<noteq> x}" by force
  1.1611 +  from a1 a2 a3 show False by (force dest: finite_subset)
  1.1612 +qed
  1.1613 +
  1.1614 +section {* Andy's freshness lemma *}
  1.1615 +(*================================*)
  1.1616 +
  1.1617 +lemma freshness_lemma:
  1.1618 +  fixes h :: "'x\<Rightarrow>'a"
  1.1619 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1620 +  and     at:  "at TYPE('x)" 
  1.1621 +  and     f1:  "finite ((supp h)::'x set)"
  1.1622 +  and     a: "\<exists>a::'x. (a\<sharp>h \<and> a\<sharp>(h a))"
  1.1623 +  shows  "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> (h a) = fr"
  1.1624 +proof -
  1.1625 +  have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
  1.1626 +  have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  1.1627 +  from a obtain a0 where a1: "a0\<sharp>h" and a2: "a0\<sharp>(h a0)" by force
  1.1628 +  show ?thesis
  1.1629 +  proof
  1.1630 +    let ?fr = "h (a0::'x)"
  1.1631 +    show "\<forall>(a::'x). (a\<sharp>h \<longrightarrow> ((h a) = ?fr))" 
  1.1632 +    proof (intro strip)
  1.1633 +      fix a
  1.1634 +      assume a3: "(a::'x)\<sharp>h"
  1.1635 +      show "h (a::'x) = h a0"
  1.1636 +      proof (cases "a=a0")
  1.1637 +	case True thus "h (a::'x) = h a0" by simp
  1.1638 +      next
  1.1639 +	case False 
  1.1640 +	assume "a\<noteq>a0"
  1.1641 +	hence c1: "a\<notin>((supp a0)::'x set)" by  (simp add: fresh_def[symmetric] at_fresh[OF at])
  1.1642 +	have c2: "a\<notin>((supp h)::'x set)" using a3 by (simp add: fresh_def)
  1.1643 +	from c1 c2 have c3: "a\<notin>((supp h)\<union>((supp a0)::'x set))" by force
  1.1644 +	have f2: "finite ((supp a0)::'x set)" by (simp add: at_supp[OF at])
  1.1645 +	from f1 f2 have "((supp (h a0))::'x set)\<subseteq>((supp h)\<union>(supp a0))"
  1.1646 +	  by (simp add: pt_supp_fun_subset[OF ptb, OF pta, OF at])
  1.1647 +	hence "a\<notin>((supp (h a0))::'x set)" using c3 by force
  1.1648 +	hence "a\<sharp>(h a0)" by (simp add: fresh_def) 
  1.1649 +	with a2 have d1: "[(a0,a)]\<bullet>(h a0) = (h a0)" by (rule pt_fresh_fresh[OF pta, OF at])
  1.1650 +	from a1 a3 have d2: "[(a0,a)]\<bullet>h = h" by (rule pt_fresh_fresh[OF ptc, OF at])
  1.1651 +	from d1 have "h a0 = [(a0,a)]\<bullet>(h a0)" by simp
  1.1652 +	also have "\<dots>= ([(a0,a)]\<bullet>h)([(a0,a)]\<bullet>a0)" by (simp add: pt_fun_app_eq[OF ptb, OF at])
  1.1653 +	also have "\<dots> = h ([(a0,a)]\<bullet>a0)" using d2 by simp
  1.1654 +	also have "\<dots> = h a" by (simp add: at_calc[OF at])
  1.1655 +	finally show "h a = h a0" by simp
  1.1656 +      qed
  1.1657 +    qed
  1.1658 +  qed
  1.1659 +qed
  1.1660 +	    
  1.1661 +lemma freshness_lemma_unique:
  1.1662 +  fixes h :: "'x\<Rightarrow>'a"
  1.1663 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1664 +  and     at: "at TYPE('x)" 
  1.1665 +  and     f1: "finite ((supp h)::'x set)"
  1.1666 +  and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
  1.1667 +  shows  "\<exists>!(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr"
  1.1668 +proof
  1.1669 +  from pt at f1 a show "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr" by (simp add: freshness_lemma)
  1.1670 +next
  1.1671 +  fix fr1 fr2
  1.1672 +  assume b1: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr1"
  1.1673 +  assume b2: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr2"
  1.1674 +  from a obtain a where "(a::'x)\<sharp>h" by force 
  1.1675 +  with b1 b2 have "h a = fr1 \<and> h a = fr2" by force
  1.1676 +  thus "fr1 = fr2" by force
  1.1677 +qed
  1.1678 +
  1.1679 +-- "packaging the freshness lemma into a function"
  1.1680 +constdefs
  1.1681 +  fresh_fun :: "('x\<Rightarrow>'a)\<Rightarrow>'a"
  1.1682 +  "fresh_fun (h) \<equiv> THE fr. (\<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr)"
  1.1683 +
  1.1684 +lemma fresh_fun_app:
  1.1685 +  fixes h :: "'x\<Rightarrow>'a"
  1.1686 +  and   a :: "'x"
  1.1687 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1688 +  and     at: "at TYPE('x)" 
  1.1689 +  and     f1: "finite ((supp h)::'x set)"
  1.1690 +  and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
  1.1691 +  and     b: "a\<sharp>h"
  1.1692 +  shows "(fresh_fun h) = (h a)"
  1.1693 +proof (unfold fresh_fun_def, rule the_equality)
  1.1694 +  show "\<forall>(a'::'x). a'\<sharp>h \<longrightarrow> h a' = h a"
  1.1695 +  proof (intro strip)
  1.1696 +    fix a'::"'x"
  1.1697 +    assume c: "a'\<sharp>h"
  1.1698 +    from pt at f1 a have "\<exists>(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr" by (rule freshness_lemma)
  1.1699 +    with b c show "h a' = h a" by force
  1.1700 +  qed
  1.1701 +next
  1.1702 +  fix fr::"'a"
  1.1703 +  assume "\<forall>a. a\<sharp>h \<longrightarrow> h a = fr"
  1.1704 +  with b show "fr = h a" by force
  1.1705 +qed
  1.1706 +
  1.1707 +
  1.1708 +lemma fresh_fun_supports:
  1.1709 +  fixes h :: "'x\<Rightarrow>'a"
  1.1710 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1711 +  and     at: "at TYPE('x)" 
  1.1712 +  and     f1: "finite ((supp h)::'x set)"
  1.1713 +  and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
  1.1714 +  shows "((supp h)::'x set) supports (fresh_fun h)"
  1.1715 +  apply(simp add: "op supports_def")
  1.1716 +  apply(fold fresh_def)
  1.1717 +  apply(auto)
  1.1718 +  apply(subgoal_tac "\<exists>(a''::'x). a''\<sharp>(h,a,b)")(*A*)
  1.1719 +  apply(erule exE)
  1.1720 +  apply(simp add: fresh_prod)
  1.1721 +  apply(auto)
  1.1722 +  apply(rotate_tac 2)
  1.1723 +  apply(drule fresh_fun_app[OF pt, OF at, OF f1, OF a])
  1.1724 +  apply(simp add: at_fresh[OF at])
  1.1725 +  apply(simp add: pt_fun_app_eq[OF at_pt_inst[OF at], OF at])
  1.1726 +  apply(auto simp add: at_calc[OF at])
  1.1727 +  apply(subgoal_tac "[(a, b)]\<bullet>h = h")(*B*)
  1.1728 +  apply(simp)
  1.1729 +  (*B*)
  1.1730 +  apply(rule pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
  1.1731 +  apply(assumption)+
  1.1732 +  (*A*)
  1.1733 +  apply(rule at_exists_fresh[OF at])
  1.1734 +  apply(simp add: supp_prod)
  1.1735 +  apply(simp add: f1 at_supp[OF at])
  1.1736 +  done
  1.1737 +
  1.1738 +lemma fresh_fun_equiv:
  1.1739 +  fixes h :: "'x\<Rightarrow>'a"
  1.1740 +  and   pi:: "'x prm"
  1.1741 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1742 +  and     at:  "at TYPE('x)" 
  1.1743 +  and     f1:  "finite ((supp h)::'x set)"
  1.1744 +  and     a1: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
  1.1745 +  shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
  1.1746 +proof -
  1.1747 +  have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
  1.1748 +  have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  1.1749 +  have f2: "finite ((supp (pi\<bullet>h))::'x set)"
  1.1750 +  proof -
  1.1751 +    from f1 have "finite (pi\<bullet>((supp h)::'x set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at])
  1.1752 +    thus ?thesis by (simp add: pt_perm_supp[OF ptc, OF at])
  1.1753 +  qed
  1.1754 +  from a1 obtain a' where c0: "a'\<sharp>h \<and> a'\<sharp>(h a')" by force
  1.1755 +  hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by simp_all
  1.1756 +  have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1 by (simp add: pt_fresh_bij[OF ptc, OF at])
  1.1757 +  have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
  1.1758 +  proof -
  1.1759 +    from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))" by (simp add: pt_fresh_bij[OF pta, OF at])
  1.1760 +    thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
  1.1761 +  qed
  1.1762 +  have a2: "\<exists>(a::'x). (a\<sharp>(pi\<bullet>h) \<and> a\<sharp>((pi\<bullet>h) a))" using c3 c4 by force
  1.1763 +  have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF pta, OF at, OF f1])
  1.1764 +  have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2])
  1.1765 +  show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
  1.1766 +qed
  1.1767 +  
  1.1768 +section {* disjointness properties *}
  1.1769 +(*=================================*)
  1.1770 +lemma dj_perm_forget:
  1.1771 +  fixes pi::"'y prm"
  1.1772 +  and   x ::"'x"
  1.1773 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
  1.1774 +  shows "pi\<bullet>x=x"
  1.1775 +  using dj by (simp add: disjoint_def)
  1.1776 +
  1.1777 +lemma dj_perm_perm_forget:
  1.1778 +  fixes pi1::"'x prm"
  1.1779 +  and   pi2::"'y prm"
  1.1780 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
  1.1781 +  shows "pi2\<bullet>pi1=pi1"
  1.1782 +  using dj by (induct pi1, auto simp add: disjoint_def)
  1.1783 +
  1.1784 +lemma dj_cp:
  1.1785 +  fixes pi1::"'x prm"
  1.1786 +  and   pi2::"'y prm"
  1.1787 +  and   x  ::"'a"
  1.1788 +  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
  1.1789 +  and     dj: "disjoint TYPE('y) TYPE('x)"
  1.1790 +  shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
  1.1791 +  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
  1.1792 +
  1.1793 +lemma dj_supp:
  1.1794 +  fixes a::"'x"
  1.1795 +  assumes dj: "disjoint TYPE('x) TYPE('y)"
  1.1796 +  shows "(supp a) = ({}::'y set)"
  1.1797 +apply(simp add: supp_def dj_perm_forget[OF dj])
  1.1798 +done
  1.1799 +
  1.1800 +
  1.1801 +section {* composition instances *}
  1.1802 +(* ============================= *)
  1.1803 +
  1.1804 +lemma cp_list_inst:
  1.1805 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  1.1806 +  shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
  1.1807 +using c1
  1.1808 +apply(simp add: cp_def)
  1.1809 +apply(auto)
  1.1810 +apply(induct_tac x)
  1.1811 +apply(auto)
  1.1812 +done
  1.1813 +
  1.1814 +lemma cp_set_inst:
  1.1815 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  1.1816 +  shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
  1.1817 +using c1
  1.1818 +apply(simp add: cp_def)
  1.1819 +apply(auto)
  1.1820 +apply(auto simp add: perm_set_def)
  1.1821 +apply(rule_tac x="pi2\<bullet>aa" in exI)
  1.1822 +apply(auto)
  1.1823 +done
  1.1824 +
  1.1825 +lemma cp_option_inst:
  1.1826 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  1.1827 +  shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
  1.1828 +using c1
  1.1829 +apply(simp add: cp_def)
  1.1830 +apply(auto)
  1.1831 +apply(case_tac x)
  1.1832 +apply(auto)
  1.1833 +done
  1.1834 +
  1.1835 +lemma cp_noption_inst:
  1.1836 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  1.1837 +  shows "cp TYPE ('a nOption) TYPE('x) TYPE('y)"
  1.1838 +using c1
  1.1839 +apply(simp add: cp_def)
  1.1840 +apply(auto)
  1.1841 +apply(case_tac x)
  1.1842 +apply(auto)
  1.1843 +done
  1.1844 +
  1.1845 +lemma cp_unit_inst:
  1.1846 +  shows "cp TYPE (unit) TYPE('x) TYPE('y)"
  1.1847 +apply(simp add: cp_def)
  1.1848 +done
  1.1849 +
  1.1850 +lemma cp_bool_inst:
  1.1851 +  shows "cp TYPE (bool) TYPE('x) TYPE('y)"
  1.1852 +apply(simp add: cp_def)
  1.1853 +apply(rule allI)+
  1.1854 +apply(induct_tac x)
  1.1855 +apply(simp_all)
  1.1856 +done
  1.1857 +
  1.1858 +lemma cp_prod_inst:
  1.1859 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  1.1860 +  and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
  1.1861 +  shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
  1.1862 +using c1 c2
  1.1863 +apply(simp add: cp_def)
  1.1864 +done
  1.1865 +
  1.1866 +lemma cp_fun_inst:
  1.1867 +  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  1.1868 +  and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
  1.1869 +  and     pt: "pt TYPE ('y) TYPE('x)"
  1.1870 +  and     at: "at TYPE ('x)"
  1.1871 +  shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
  1.1872 +using c1 c2
  1.1873 +apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
  1.1874 +apply(simp add: perm_rev[symmetric])
  1.1875 +apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
  1.1876 +done
  1.1877 +
  1.1878 +
  1.1879 +section {* Abstraction function *}
  1.1880 +(*==============================*)
  1.1881 +
  1.1882 +lemma pt_abs_fun_inst:
  1.1883 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1884 +  and     at: "at TYPE('x)"
  1.1885 +  shows "pt TYPE('x\<Rightarrow>('a nOption)) TYPE('x)"
  1.1886 +  by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at])
  1.1887 +
  1.1888 +constdefs
  1.1889 +  abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a nOption))" ("[_]._" [100,100] 100)
  1.1890 +  "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))"
  1.1891 +
  1.1892 +lemma abs_fun_if: 
  1.1893 +  fixes pi :: "'x prm"
  1.1894 +  and   x  :: "'a"
  1.1895 +  and   y  :: "'a"
  1.1896 +  and   c  :: "bool"
  1.1897 +  shows "pi\<bullet>(if c then x else y) = (if c then (pi\<bullet>x) else (pi\<bullet>y))"   
  1.1898 +  by force
  1.1899 +
  1.1900 +lemma abs_fun_pi_ineq:
  1.1901 +  fixes a  :: "'y"
  1.1902 +  and   x  :: "'a"
  1.1903 +  and   pi :: "'x prm"
  1.1904 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.1905 +  and     ptb: "pt TYPE('y) TYPE('x)"
  1.1906 +  and     at:  "at TYPE('x)"
  1.1907 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1.1908 +  shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
  1.1909 +  apply(simp add: abs_fun_def perm_fun_def abs_fun_if)
  1.1910 +  apply(simp only: expand_fun_eq)
  1.1911 +  apply(rule allI)
  1.1912 +  apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*)
  1.1913 +  apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>x))")(*B*)
  1.1914 +  apply(subgoal_tac "pi\<bullet>([(a,(rev pi)\<bullet>xa)]\<bullet>x) = [(pi\<bullet>a,xa)]\<bullet>(pi\<bullet>x)")(*C*)
  1.1915 +  apply(simp)
  1.1916 +(*C*)
  1.1917 +  apply(simp add: cp1[OF cp])
  1.1918 +  apply(simp add: pt_pi_rev[OF ptb, OF at])
  1.1919 +(*B*)
  1.1920 +  apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  1.1921 +(*A*)
  1.1922 +  apply(rule iffI)
  1.1923 +  apply(rule pt_bij2[OF ptb, OF at, THEN sym])
  1.1924 +  apply(simp)
  1.1925 +  apply(rule pt_bij2[OF ptb, OF at])
  1.1926 +  apply(simp)
  1.1927 +done
  1.1928 +
  1.1929 +lemma abs_fun_pi:
  1.1930 +  fixes a  :: "'x"
  1.1931 +  and   x  :: "'a"
  1.1932 +  and   pi :: "'x prm"
  1.1933 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1934 +  and     at: "at TYPE('x)"
  1.1935 +  shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
  1.1936 +apply(rule abs_fun_pi_ineq)
  1.1937 +apply(rule pt)
  1.1938 +apply(rule at_pt_inst)
  1.1939 +apply(rule at)+
  1.1940 +apply(rule cp_pt_inst)
  1.1941 +apply(rule pt)
  1.1942 +apply(rule at)
  1.1943 +done
  1.1944 +
  1.1945 +lemma abs_fun_eq1: 
  1.1946 +  fixes x  :: "'a"
  1.1947 +  and   y  :: "'a"
  1.1948 +  and   a  :: "'x"
  1.1949 +  shows "([a].x = [a].y) = (x = y)"
  1.1950 +apply(auto simp add: abs_fun_def)
  1.1951 +apply(auto simp add: expand_fun_eq)
  1.1952 +apply(drule_tac x="a" in spec)
  1.1953 +apply(simp)
  1.1954 +done
  1.1955 +
  1.1956 +lemma abs_fun_eq2:
  1.1957 +  fixes x  :: "'a"
  1.1958 +  and   y  :: "'a"
  1.1959 +  and   a  :: "'x"
  1.1960 +  and   b  :: "'x"
  1.1961 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1962 +      and at: "at TYPE('x)"
  1.1963 +      and a1: "a\<noteq>b" 
  1.1964 +      and a2: "[a].x = [b].y" 
  1.1965 +  shows "x=[(a,b)]\<bullet>y\<and>a\<sharp>y"
  1.1966 +proof -
  1.1967 +  from a2 have a3: 
  1.1968 +         "\<forall>c::'x. (if c=a then nSome(x) else (if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone))
  1.1969 +                = (if c=b then nSome(y) else (if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone))"
  1.1970 +         (is "\<forall>c::'x. ?P c = ?Q c")
  1.1971 +    by (force simp add: abs_fun_def expand_fun_eq)
  1.1972 +  from a3 have "?P a = ?Q a" by (blast)
  1.1973 +  hence a4: "nSome(x) = ?Q a" by simp
  1.1974 +  from a3 have "?P b = ?Q b" by (blast)
  1.1975 +  hence a5: "nSome(y) = ?P b" by simp
  1.1976 +  show ?thesis using a4 a5
  1.1977 +  proof (cases "a\<sharp>y")
  1.1978 +    assume a6: "a\<sharp>y"
  1.1979 +    hence a7: "x = [(b,a)]\<bullet>y" using a4 a1 by simp
  1.1980 +    have "[(a,b)]\<bullet>y = [(b,a)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at])
  1.1981 +    thus ?thesis using a6 a7 by simp
  1.1982 +  next
  1.1983 +    assume "\<not>a\<sharp>y"
  1.1984 +    hence "nSome(x) = nNone" using a1 a4 by simp
  1.1985 +    hence False by force
  1.1986 +    thus ?thesis by force
  1.1987 +  qed
  1.1988 +qed
  1.1989 +
  1.1990 +lemma abs_fun_eq3: 
  1.1991 +  fixes x  :: "'a"
  1.1992 +  and   y  :: "'a"
  1.1993 +  and   a   :: "'x"
  1.1994 +  and   b   :: "'x"
  1.1995 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.1996 +      and at: "at TYPE('x)"
  1.1997 +      and a1: "a\<noteq>b" 
  1.1998 +      and a2: "x=[(a,b)]\<bullet>y" 
  1.1999 +      and a3: "a\<sharp>y" 
  1.2000 +  shows "[a].x =[b].y"
  1.2001 +proof -
  1.2002 +  show ?thesis using a1 a2 a3
  1.2003 +    apply(auto simp add: abs_fun_def)
  1.2004 +    apply(simp only: expand_fun_eq)
  1.2005 +    apply(rule allI)
  1.2006 +    apply(case_tac "x=a")
  1.2007 +    apply(simp)
  1.2008 +    apply(rule pt3[OF pt], rule at_ds5[OF at])
  1.2009 +    apply(case_tac "x=b")
  1.2010 +    apply(simp add: pt_swap_bij[OF pt, OF at])
  1.2011 +    apply(simp add: at_calc[OF at] at_bij[OF at] pt_fresh_left[OF pt, OF at])
  1.2012 +    apply(simp only: if_False)
  1.2013 +    apply(simp add: at_calc[OF at] at_bij[OF at] pt_fresh_left[OF pt, OF at])
  1.2014 +    apply(rule impI)
  1.2015 +    apply(subgoal_tac "[(a,x)]\<bullet>([(a,b)]\<bullet>y) = [(b,x)]\<bullet>([(a,x)]\<bullet>y)")(*A*)
  1.2016 +    apply(simp)
  1.2017 +    apply(simp only:  pt_bij[OF pt, OF at])
  1.2018 +    apply(rule pt_fresh_fresh[OF pt, OF at])
  1.2019 +    apply(assumption)+
  1.2020 +    (*A*)
  1.2021 +    apply(simp only: pt2[OF pt, symmetric])
  1.2022 +    apply(rule pt3[OF pt])
  1.2023 +    apply(simp, rule at_ds6[OF at])
  1.2024 +    apply(force)
  1.2025 +    done
  1.2026 +  qed
  1.2027 +
  1.2028 +lemma abs_fun_eq: 
  1.2029 +  fixes x  :: "'a"
  1.2030 +  and   y  :: "'a"
  1.2031 +  and   a  :: "'x"
  1.2032 +  and   b  :: "'x"
  1.2033 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.2034 +      and at: "at TYPE('x)"
  1.2035 +  shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y))"
  1.2036 +proof (rule iffI)
  1.2037 +  assume b: "[a].x = [b].y"
  1.2038 +  show "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)"
  1.2039 +  proof (cases "a=b")
  1.2040 +    case True with b show ?thesis by (simp add: abs_fun_eq1)
  1.2041 +  next
  1.2042 +    case False with b show ?thesis by (simp add: abs_fun_eq2[OF pt, OF at])
  1.2043 +  qed
  1.2044 +next
  1.2045 +  assume "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)"
  1.2046 +  thus "[a].x = [b].y"
  1.2047 +  proof
  1.2048 +    assume "a=b \<and> x=y" thus ?thesis by simp
  1.2049 +  next
  1.2050 +    assume "a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y" 
  1.2051 +    thus ?thesis by (simp add: abs_fun_eq3[OF pt, OF at])
  1.2052 +  qed
  1.2053 +qed
  1.2054 +
  1.2055 +-- "two helpers for the abst_supp_approx-lemma"
  1.2056 +lemma finite_minus:   
  1.2057 +  assumes a: "finite {b. P b}"
  1.2058 +  shows "finite {b. b \<noteq> x \<and> P b}" 
  1.2059 +  using a by (force simp add: Collect_conj_eq)
  1.2060 +
  1.2061 +lemma infinite_minus: 
  1.2062 +  assumes a: "infinite {b. P b}" 
  1.2063 +  shows "infinite {b. b \<noteq> x \<and> P b}"
  1.2064 +proof -
  1.2065 +  have "{b. b \<noteq> x \<and> P b}={b. P b}-{x}" by force
  1.2066 +  with a show ?thesis by force
  1.2067 +qed
  1.2068 +
  1.2069 +lemma abs_fun_supp_approx:
  1.2070 +  fixes x :: "'a"
  1.2071 +  and   a :: "'x"
  1.2072 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.2073 +  and     at: "at TYPE('x)"
  1.2074 +  shows "((supp ([a].x))::'x set) \<subseteq> (supp x)\<union>{a}"
  1.2075 +proof (unfold supp_def, auto simp only: abs_fun_pi[OF pt, OF at] at_calc[OF at] if_False)
  1.2076 +  fix c
  1.2077 +  assume a: "c\<noteq>a"
  1.2078 +  assume "finite {b::'x. [(c, b)]\<bullet>x \<noteq> x}"
  1.2079 +  hence f: "finite {b::'x. b\<noteq>a \<and> [(c, b)]\<bullet>x \<noteq> x}" by (rule finite_minus)
  1.2080 +  assume "infinite {b::'x. [(if (b=a) then c else a)].([(c,b)]\<bullet>x) \<noteq> ([a].x)}"
  1.2081 +  hence "infinite {b::'x. b\<noteq>a \<and> [(if (b=a) then c else a)].([(c,b)]\<bullet>x) \<noteq> ([a].x)}" 
  1.2082 +    by (rule infinite_minus)
  1.2083 +  hence i: "infinite {b::'x. b\<noteq>a \<and> [a].([(c,b)]\<bullet>x) \<noteq> ([a].x)}"
  1.2084 +  proof (auto split add: split_if_asm)
  1.2085 +    assume c1: "infinite {b::'x. b\<noteq>a \<and> (b=a \<or> b\<noteq>a \<and> [a].([(c,b)]\<bullet>x) \<noteq> ([a].x))}"
  1.2086 +    assume c2: "finite {b::'x. b\<noteq>a \<and>  [a].([(c, b)]\<bullet>x) \<noteq> ([a].x)}"
  1.2087 +    have "{b::'x. b\<noteq>a \<and> (b=a \<or> b\<noteq>a \<and> [a].([(c,b)]\<bullet>x) \<noteq> ([a].x))} =
  1.2088 +          {b::'x. b\<noteq>a \<and> [a].([(c,b)]\<bullet>x) \<noteq> ([a].x)}" by force
  1.2089 +    with c1 c2 show False by simp
  1.2090 +  qed
  1.2091 +  from f i show False by (simp add: abs_fun_eq1) 
  1.2092 +qed
  1.2093 +
  1.2094 +lemma abs_fun_finite_supp:
  1.2095 +  fixes x :: "'a"
  1.2096 +  and   a :: "'x"
  1.2097 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.2098 +  and     at: "at TYPE('x)"
  1.2099 +  and     f:  "finite ((supp x)::'x set)"
  1.2100 +  shows "finite ((supp ([a].x))::'x set)"
  1.2101 +proof -
  1.2102 +  from f have f1: "finite (((supp x)::'x set)\<union>{a})" by force
  1.2103 +  thus ?thesis using abs_fun_supp_approx[OF pt, OF at, of "a" "x"]
  1.2104 +   by (simp add: finite_subset)
  1.2105 +qed
  1.2106 +
  1.2107 +lemma fresh_abs_funI1:
  1.2108 +  fixes  x :: "'a"
  1.2109 +  and    a :: "'x"
  1.2110 +  and    b :: "'x"
  1.2111 +  assumes pt:  "pt TYPE('a) TYPE('x)"
  1.2112 +  and     at:   "at TYPE('x)"
  1.2113 +  and f:  "finite ((supp x)::'x set)"
  1.2114 +  and a1: "b\<sharp>x" 
  1.2115 +  and a2: "a\<noteq>b"
  1.2116 +  shows "b\<sharp>([a].x)"
  1.2117 +  proof -
  1.2118 +    have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)" 
  1.2119 +    proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
  1.2120 +      show "finite ((supp ([a].x))::'x set)" using f
  1.2121 +	by (simp add: abs_fun_finite_supp[OF pt, OF at])	
  1.2122 +    qed
  1.2123 +    then obtain c where fr1: "c\<noteq>b"
  1.2124 +                  and   fr2: "c\<noteq>a"
  1.2125 +                  and   fr3: "c\<sharp>x"
  1.2126 +                  and   fr4: "c\<sharp>([a].x)"
  1.2127 +                  by (force simp add: fresh_prod at_fresh[OF at])
  1.2128 +    have e: "[(c,b)]\<bullet>([a].x) = [a].([(c,b)]\<bullet>x)" using a2 fr1 fr2 
  1.2129 +      by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  1.2130 +    from fr4 have "([(c,b)]\<bullet>c)\<sharp> ([(c,b)]\<bullet>([a].x))"
  1.2131 +      by (simp add: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  1.2132 +    hence "b\<sharp>([a].([(c,b)]\<bullet>x))" using fr1 fr2 e  
  1.2133 +      by (simp add: at_calc[OF at])
  1.2134 +    thus ?thesis using a1 fr3 
  1.2135 +      by (simp add: pt_fresh_fresh[OF pt, OF at])
  1.2136 +qed
  1.2137 +
  1.2138 +lemma fresh_abs_funE:
  1.2139 +  fixes a :: "'x"
  1.2140 +  and   b :: "'x"
  1.2141 +  and   x :: "'a"
  1.2142 +  assumes pt:  "pt TYPE('a) TYPE('x)"
  1.2143 +  and     at:  "at TYPE('x)"
  1.2144 +  and     f:  "finite ((supp x)::'x set)"
  1.2145 +  and     a1: "b\<sharp>([a].x)" 
  1.2146 +  and     a2: "b\<noteq>a" 
  1.2147 +  shows "b\<sharp>x"
  1.2148 +proof -
  1.2149 +  have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)"
  1.2150 +  proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
  1.2151 +    show "finite ((supp ([a].x))::'x set)" using f
  1.2152 +      by (simp add: abs_fun_finite_supp[OF pt, OF at])	
  1.2153 +  qed
  1.2154 +  then obtain c where fr1: "b\<noteq>c"
  1.2155 +                and   fr2: "c\<noteq>a"
  1.2156 +                and   fr3: "c\<sharp>x"
  1.2157 +                and   fr4: "c\<sharp>([a].x)" by (force simp add: fresh_prod at_fresh[OF at])
  1.2158 +  have "[a].x = [(b,c)]\<bullet>([a].x)" using a1 fr4 
  1.2159 +    by (simp add: pt_fresh_fresh[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  1.2160 +  hence "[a].x = [a].([(b,c)]\<bullet>x)" using fr2 a2 
  1.2161 +    by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  1.2162 +  hence b: "([(b,c)]\<bullet>x) = x" by (simp add: abs_fun_eq1)
  1.2163 +  from fr3 have "([(b,c)]\<bullet>c)\<sharp>([(b,c)]\<bullet>x)" 
  1.2164 +    by (simp add: pt_fresh_bij[OF pt, OF at]) 
  1.2165 +  thus ?thesis using b fr1 by (simp add: at_calc[OF at])
  1.2166 +qed
  1.2167 +
  1.2168 +lemma fresh_abs_funI2:
  1.2169 +  fixes a :: "'x"
  1.2170 +  and   x :: "'a"
  1.2171 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.2172 +  and     at: "at TYPE('x)"
  1.2173 +  and     f: "finite ((supp x)::'x set)"
  1.2174 +  shows "a\<sharp>([a].x)"
  1.2175 +proof -
  1.2176 +  have "\<exists>c::'x. c\<sharp>(a,x)"
  1.2177 +    by  (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f) 
  1.2178 +  then obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a" 
  1.2179 +                and   fr2: "c\<sharp>x" by (force simp add: fresh_prod at_fresh[OF at])
  1.2180 +  have "c\<sharp>([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at])
  1.2181 +  hence "([(c,a)]\<bullet>c)\<sharp>([(c,a)]\<bullet>([a].x))" using fr1  
  1.2182 +    by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  1.2183 +  hence a: "a\<sharp>([c].([(c,a)]\<bullet>x))" using fr1_sym 
  1.2184 +    by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  1.2185 +  have "[c].([(c,a)]\<bullet>x) = ([a].x)" using fr1_sym fr2 
  1.2186 +    by (simp add: abs_fun_eq[OF pt, OF at])
  1.2187 +  thus ?thesis using a by simp
  1.2188 +qed
  1.2189 +
  1.2190 +lemma fresh_abs_fun_iff: 
  1.2191 +  fixes a :: "'x"
  1.2192 +  and   b :: "'x"
  1.2193 +  and   x :: "'a"
  1.2194 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.2195 +  and     at: "at TYPE('x)"
  1.2196 +  and     f: "finite ((supp x)::'x set)"
  1.2197 +  shows "(b\<sharp>([a].x)) = (b=a \<or> b\<sharp>x)" 
  1.2198 +  by (auto  dest: fresh_abs_funE[OF pt, OF at,OF f] 
  1.2199 +           intro: fresh_abs_funI1[OF pt, OF at,OF f] 
  1.2200 +                  fresh_abs_funI2[OF pt, OF at,OF f])
  1.2201 +
  1.2202 +lemma abs_fun_supp: 
  1.2203 +  fixes a :: "'x"
  1.2204 +  and   x :: "'a"
  1.2205 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.2206 +  and     at: "at TYPE('x)"
  1.2207 +  and     f: "finite ((supp x)::'x set)"
  1.2208 +  shows "supp ([a].x) = (supp x)-{a}"
  1.2209 + by (force simp add: supp_fresh_iff fresh_abs_fun_iff[OF pt, OF at, OF f])
  1.2210 +
  1.2211 +(* maybe needs to be stated by supp -supp *)
  1.2212 +
  1.2213 +lemma abs_fun_supp_ineq: 
  1.2214 +  fixes a :: "'y"
  1.2215 +  and   x :: "'a"
  1.2216 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.2217 +  and     ptb: "pt TYPE('y) TYPE('x)"
  1.2218 +  and     at:  "at TYPE('x)"
  1.2219 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1.2220 +  and     dj:  "disjoint TYPE('y) TYPE('x)"
  1.2221 +  shows "((supp ([a].x))::'x set) = (supp x)"
  1.2222 +apply(auto simp add: supp_def)
  1.2223 +apply(auto simp add: abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp])
  1.2224 +apply(auto simp add: dj_perm_forget[OF dj])
  1.2225 +apply(auto simp add: abs_fun_eq1) 
  1.2226 +done
  1.2227 +
  1.2228 +lemma fresh_abs_fun_iff_ineq: 
  1.2229 +  fixes a :: "'y"
  1.2230 +  and   b :: "'x"
  1.2231 +  and   x :: "'a"
  1.2232 +  assumes pta: "pt TYPE('a) TYPE('x)"
  1.2233 +  and     ptb: "pt TYPE('y) TYPE('x)"
  1.2234 +  and     at:  "at TYPE('x)"
  1.2235 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1.2236 +  and     dj:  "disjoint TYPE('y) TYPE('x)"
  1.2237 +  shows "b\<sharp>([a].x) = b\<sharp>x" 
  1.2238 +  by (simp add: fresh_def abs_fun_supp_ineq[OF pta, OF ptb, OF at, OF cp, OF dj])
  1.2239 +
  1.2240 +section {* abstraction type for the datatype package (not really needed anymore) *}
  1.2241 +(*===============================================================================*)
  1.2242 +consts
  1.2243 +  "ABS_set" :: "('x\<Rightarrow>('a nOption)) set"
  1.2244 +inductive ABS_set
  1.2245 +  intros
  1.2246 +  ABS_in: "(abs_fun a x)\<in>ABS_set"
  1.2247 +
  1.2248 +typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a nOption)) set"
  1.2249 +proof 
  1.2250 +  fix x::"'a" and a::"'x"
  1.2251 +  show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
  1.2252 +qed
  1.2253 +
  1.2254 +syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
  1.2255 +
  1.2256 +
  1.2257 +section {* Lemmas for Deciding Permutation Equations *}
  1.2258 +(*===================================================*)
  1.2259 +
  1.2260 +lemma perm_eq_app:
  1.2261 +  fixes f  :: "'a\<Rightarrow>'b"
  1.2262 +  and   x  :: "'a"
  1.2263 +  and   pi :: "'x prm"
  1.2264 +  assumes pt: "pt TYPE('a) TYPE('x)"
  1.2265 +  and     at: "at TYPE('x)"
  1.2266 +  shows "(pi\<bullet>(f x)=y) = ((pi\<bullet>f)(pi\<bullet>x)=y)"
  1.2267 +  by (simp add: pt_fun_app_eq[OF pt, OF at])
  1.2268 +
  1.2269 +lemma perm_eq_lam:
  1.2270 +  fixes f  :: "'a\<Rightarrow>'b"
  1.2271 +  and   x  :: "'a"
  1.2272 +  and   pi :: "'x prm"
  1.2273 +  shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)"
  1.2274 +  by (simp add: perm_fun_def)
  1.2275 +
  1.2276 +
  1.2277 +
  1.2278 +(***************************************)
  1.2279 +(* setup for the individial atom-kinds *)
  1.2280 +(* and datatype                        *)
  1.2281 +use "nominal_package.ML"
  1.2282 +setup "NominalPackage.setup"
  1.2283 +
  1.2284 +(**********************************)
  1.2285 +(* setup for induction principles *)
  1.2286 +use "nominal_induct.ML";
  1.2287 +method_setup nominal_induct =
  1.2288 +  {* nominal_induct_method *}
  1.2289 +  {* nominal induction *}
  1.2290 +
  1.2291 +(*******************************)
  1.2292 +(* permutation equality tactic *)
  1.2293 +use "nominal_permeq.ML";
  1.2294 +method_setup perm_simp =
  1.2295 +  {* perm_eq_meth *}
  1.2296 +  {* tactic for deciding equalities involving permutations *}
  1.2297 +
  1.2298 +method_setup perm_simp_debug =
  1.2299 +  {* perm_eq_meth_debug *}
  1.2300 +  {* tactic for deciding equalities involving permutations including debuging facilities*}
  1.2301 +
  1.2302 +method_setup supports_simp =
  1.2303 +  {* supports_meth *}
  1.2304 +  {* tactic for deciding whether something supports semthing else *}
  1.2305 +
  1.2306 +method_setup supports_simp_debug =
  1.2307 +  {* supports_meth_debug *}
  1.2308 +  {* tactic for deciding equalities involving permutations including debuging facilities*}
  1.2309 +
  1.2310 +end
  1.2311 +
  1.2312 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Mon Oct 17 12:30:57 2005 +0200
     2.3 @@ -0,0 +1,88 @@
     2.4 +(* $Id$ *)
     2.5 +
     2.6 +local
     2.7 +
     2.8 +(* A function that takes a list of Variables and a term t;                    *)
     2.9 +(* it builds up an abstraction of the Variables packaged in a tuple(!)        *)
    2.10 +(* over the term t.                                                           *)
    2.11 +(* E.g  tuple_lambda [] t        produces %x . t where x is a dummy Variable  *) 
    2.12 +(*      tuple_lambda [a] t       produces %a . t                              *) 
    2.13 +(*      tuple_lambda [a,b,c] t   produces %(a,b,c). t                         *)
    2.14 +
    2.15 +  fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
    2.16 +    | tuple_lambda [x] t = lambda x t
    2.17 +    | tuple_lambda (x::xs) t =
    2.18 +       let
    2.19 +         val t' = tuple_lambda xs t;
    2.20 +         val Type ("fun", [T,U]) = fastype_of t';
    2.21 +       in
    2.22 +         HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
    2.23 +       end; 
    2.24 +
    2.25 +fun find_var frees name =
    2.26 +  (case Library.find_first (equal name o fst o dest_Free) frees of
    2.27 +    NONE => error ("No such Variable in term: " ^ quote name)
    2.28 +  | SOME v => v);
    2.29 +
    2.30 +fun nominal_induct_tac (names, rule) facts state =
    2.31 +  let
    2.32 +    val sg     = Thm.sign_of_thm state;
    2.33 +    val cert   = Thm.cterm_of sg;
    2.34 +    val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
    2.35 +    val frees  = Term.term_frees goal;
    2.36 +    val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
    2.37 +    val vars = map (find_var frees) names;
    2.38 +
    2.39 +    fun inst_rule rule =
    2.40 +      let
    2.41 +        val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
    2.42 +        val (P :: ts, x) = split_last concl_vars
    2.43 +          handle Empty => error "Malformed conclusion of induction rule"
    2.44 +            | Bind => error "Malformed conclusion of induction rule";
    2.45 +      in
    2.46 +        cterm_instantiate
    2.47 +          ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
    2.48 +           (cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) ::
    2.49 +           (map cert ts ~~ map cert vars)) rule
    2.50 +      end;
    2.51 +
    2.52 +    val simplify_rule =
    2.53 +      Simplifier.full_simplify (HOL_basic_ss addsimps
    2.54 +        [split_conv, split_paired_All, split_paired_all]);
    2.55 +
    2.56 +    val facts1 = Library.take (1, facts);
    2.57 +    val facts2 = Library.drop (1, facts);
    2.58 +
    2.59 +  in
    2.60 +    rule
    2.61 +    |> inst_rule
    2.62 +    |> Method.multi_resolve facts1
    2.63 +    |> Seq.map simplify_rule
    2.64 +    |> Seq.map (RuleCases.save rule)
    2.65 +    |> Seq.map RuleCases.add
    2.66 +    |> Seq.map (fn (r, (cases, _)) =>
    2.67 +        HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state
    2.68 +        |> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases)))
    2.69 +    |> Seq.flat
    2.70 +  end
    2.71 +  handle Subscript => Seq.empty;
    2.72 +
    2.73 +val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;
    2.74 +
    2.75 +val nominal_induct_args =
    2.76 +  Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec;
    2.77 +
    2.78 +in
    2.79 +
    2.80 +val nominal_induct_method =
    2.81 +  Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);
    2.82 +
    2.83 +(* nominal_induc_method needs to have the type
    2.84 +
    2.85 +   Args.src -> Proof.context -> Proof.method
    2.86 +
    2.87 +   CHECK THAT
    2.88 +
    2.89 +*)
    2.90 +
    2.91 +end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 12:30:57 2005 +0200
     3.3 @@ -0,0 +1,1760 @@
     3.4 +(* $Id$ *)
     3.5 +
     3.6 +signature NOMINAL_PACKAGE =
     3.7 +sig
     3.8 +  val create_nom_typedecls : string list -> theory -> theory
     3.9 +  val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix *
    3.10 +    (bstring * string list * mixfix) list) list -> theory -> theory *
    3.11 +      {distinct : thm list list,
    3.12 +       inject : thm list list,
    3.13 +       exhaustion : thm list,
    3.14 +       rec_thms : thm list,
    3.15 +       case_thms : thm list list,
    3.16 +       split_thms : (thm * thm) list,
    3.17 +       induction : thm,
    3.18 +       size : thm list,
    3.19 +       simps : thm list}
    3.20 +  val setup : (theory -> theory) list
    3.21 +end
    3.22 +
    3.23 +structure NominalPackage (*: NOMINAL_PACKAGE *) =
    3.24 +struct
    3.25 +
    3.26 +open DatatypeAux;
    3.27 +
    3.28 +(* data kind 'HOL/nominal' *)
    3.29 +
    3.30 +structure NominalArgs =
    3.31 +struct
    3.32 +  val name = "HOL/nominal";
    3.33 +  type T = unit Symtab.table;
    3.34 +
    3.35 +  val empty = Symtab.empty;
    3.36 +  val copy = I;
    3.37 +  val extend = I;
    3.38 +  fun merge _ x = Symtab.merge (K true) x;
    3.39 +
    3.40 +  fun print sg tab = ();
    3.41 +end;
    3.42 +
    3.43 +structure NominalData = TheoryDataFun(NominalArgs);
    3.44 +
    3.45 +fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));
    3.46 +
    3.47 +(* FIXME: add to hologic.ML ? *)
    3.48 +fun mk_listT T = Type ("List.list", [T]);
    3.49 +fun mk_permT T = mk_listT (HOLogic.mk_prodT (T, T));
    3.50 +
    3.51 +fun mk_Cons x xs =
    3.52 +  let val T = fastype_of x
    3.53 +  in Const ("List.list.Cons", T --> mk_listT T --> mk_listT T) $ x $ xs end;
    3.54 +
    3.55 +
    3.56 +(* this function sets up all matters related to atom-  *)
    3.57 +(* kinds; the user specifies a list of atom-kind names *)
    3.58 +(* atom_decl <ak1> ... <akn>                           *)
    3.59 +fun create_nom_typedecls ak_names thy =
    3.60 +  let
    3.61 +    (* declares a type-decl for every atom-kind: *) 
    3.62 +    (* that is typedecl <ak>                     *)
    3.63 +    val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;
    3.64 +    
    3.65 +    (* produces a list consisting of pairs:         *)
    3.66 +    (*  fst component is the atom-kind name         *)
    3.67 +    (*  snd component is its type                   *)
    3.68 +    val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names;
    3.69 +    val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names;
    3.70 +     
    3.71 +    (* adds for every atom-kind an axiom             *)
    3.72 +    (* <ak>_infinite: infinite (UNIV::<ak_type> set) *)
    3.73 +    val (thy2,inf_axs) = PureThy.add_axioms_i (map (fn (ak_name, T) =>
    3.74 +      let 
    3.75 +	val name = ak_name ^ "_infinite"
    3.76 +        val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not
    3.77 +                    (HOLogic.mk_mem (HOLogic.mk_UNIV T,
    3.78 +                     Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))
    3.79 +      in
    3.80 +	((name, axiom), []) 
    3.81 +      end) ak_names_types) thy1;
    3.82 +    
    3.83 +    (* declares a swapping function for every atom-kind, it is         *)
    3.84 +    (* const swap_<ak> :: <akT> * <akT> => <akT> => <akT>              *)
    3.85 +    (* swap_<ak> (a,b) c = (if a=c then b (else if b=c then a else c)) *)
    3.86 +    (* overloades then the general swap-function                       *) 
    3.87 +    val (thy3, swap_eqs) = foldl_map (fn (thy, (ak_name, T)) =>
    3.88 +      let
    3.89 +        val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
    3.90 +        val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name);
    3.91 +        val a = Free ("a", T);
    3.92 +        val b = Free ("b", T);
    3.93 +        val c = Free ("c", T);
    3.94 +        val ab = Free ("ab", HOLogic.mk_prodT (T, T))
    3.95 +        val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
    3.96 +        val cswap_akname = Const (swap_name, swapT);
    3.97 +        val cswap = Const ("nominal.swap", swapT)
    3.98 +
    3.99 +        val name = "swap_"^ak_name^"_def";
   3.100 +        val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.101 +		   (cswap_akname $ HOLogic.mk_prod (a,b) $ c,
   3.102 +                    cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
   3.103 +        val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
   3.104 +      in
   3.105 +        thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
   3.106 +            |> (#1 o PureThy.add_defs_i true [((name, def2),[])])
   3.107 +            |> PrimrecPackage.add_primrec_i "" [(("", def1),[])]            
   3.108 +      end) (thy2, ak_names_types);
   3.109 +    
   3.110 +    (* declares a permutation function for every atom-kind acting  *)
   3.111 +    (* on such atoms                                               *)
   3.112 +    (* const <ak>_prm_<ak> :: (<akT> * <akT>)list => akT => akT    *)
   3.113 +    (* <ak>_prm_<ak> []     a = a                                  *)
   3.114 +    (* <ak>_prm_<ak> (x#xs) a = swap_<ak> x (perm xs a)            *)
   3.115 +    val (thy4, prm_eqs) = foldl_map (fn (thy, (ak_name, T)) =>
   3.116 +      let
   3.117 +        val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
   3.118 +        val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name)
   3.119 +        val prmT = mk_permT T --> T --> T;
   3.120 +        val prm_name = ak_name ^ "_prm_" ^ ak_name;
   3.121 +        val qu_prm_name = Sign.full_name (sign_of thy) prm_name;
   3.122 +        val x  = Free ("x", HOLogic.mk_prodT (T, T));
   3.123 +        val xs = Free ("xs", mk_permT T);
   3.124 +        val a  = Free ("a", T) ;
   3.125 +
   3.126 +        val cnil  = Const ("List.list.Nil", mk_permT T);
   3.127 +        
   3.128 +        val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (qu_prm_name, prmT) $ cnil $ a, a));
   3.129 +
   3.130 +        val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.131 +                   (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
   3.132 +                    Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
   3.133 +      in
   3.134 +        thy |> Theory.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
   3.135 +            |> PrimrecPackage.add_primrec_i "" [(("", def1), []),(("", def2), [])]
   3.136 +      end) (thy3, ak_names_types);
   3.137 +    
   3.138 +    (* defines permutation functions for all combinations of atom-kinds; *)
   3.139 +    (* there are a trivial cases and non-trivial cases                   *)
   3.140 +    (* non-trivial case:                                                 *)
   3.141 +    (* <ak>_prm_<ak>_def:  perm pi a == <ak>_prm_<ak> pi a               *)
   3.142 +    (* trivial case with <ak> != <ak'>                                   *)
   3.143 +    (* <ak>_prm<ak'>_def[simp]:  perm pi a == a                          *)
   3.144 +    (*                                                                   *)
   3.145 +    (* the trivial cases are added to the simplifier, while the non-     *)
   3.146 +    (* have their own rules proved below                                 *)  
   3.147 +    val (thy5, perm_defs) = foldl_map (fn (thy, (ak_name, T)) =>
   3.148 +      foldl_map (fn (thy', (ak_name', T')) =>
   3.149 +        let
   3.150 +          val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
   3.151 +          val pi = Free ("pi", mk_permT T);
   3.152 +          val a  = Free ("a", T');
   3.153 +          val cperm = Const ("nominal.perm", mk_permT T --> T' --> T');
   3.154 +          val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T --> T' --> T');
   3.155 +
   3.156 +          val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
   3.157 +          val def = Logic.mk_equals
   3.158 +                    (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
   3.159 +        in
   3.160 +          thy' |> PureThy.add_defs_i true [((name, def),[])] 
   3.161 +        end) (thy, ak_names_types)) (thy4, ak_names_types);
   3.162 +    
   3.163 +    (* proves that every atom-kind is an instance of at *)
   3.164 +    (* lemma at_<ak>_inst:                              *)
   3.165 +    (* at TYPE(<ak>)                                    *)
   3.166 +    val (thy6, prm_cons_thms) = 
   3.167 +      thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
   3.168 +      let
   3.169 +        val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
   3.170 +        val i_type = Type(ak_name_qu,[]);
   3.171 +	val cat = Const ("nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
   3.172 +        val at_type = Logic.mk_type i_type;
   3.173 +        val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy5
   3.174 +                                  [Name "at_def",
   3.175 +                                   Name (ak_name ^ "_prm_" ^ ak_name ^ "_def"),
   3.176 +                                   Name (ak_name ^ "_prm_" ^ ak_name ^ ".simps"),
   3.177 +                                   Name ("swap_" ^ ak_name ^ "_def"),
   3.178 +                                   Name ("swap_" ^ ak_name ^ ".simps"),
   3.179 +                                   Name (ak_name ^ "_infinite")]
   3.180 +	    
   3.181 +	val name = "at_"^ak_name^ "_inst";
   3.182 +        val statement = HOLogic.mk_Trueprop (cat $ at_type);
   3.183 +
   3.184 +        val proof = fn _ => [auto_tac (claset(),simp_s)];
   3.185 +
   3.186 +      in 
   3.187 +        ((name, prove_goalw_cterm [] (cterm_of (sign_of thy5) statement) proof), []) 
   3.188 +      end) ak_names_types);
   3.189 +
   3.190 +    (* declares a perm-axclass for every atom-kind               *)
   3.191 +    (* axclass pt_<ak>                                           *)
   3.192 +    (* pt_<ak>1[simp]: perm [] x = x                             *)
   3.193 +    (* pt_<ak>2:       perm (pi1@pi2) x = perm pi1 (perm pi2 x)  *)
   3.194 +    (* pt_<ak>3:       pi1 ~ pi2 ==> perm pi1 x = perm pi2 x     *)
   3.195 +     val (thy7, pt_ax_classes) =  foldl_map (fn (thy, (ak_name, T)) =>
   3.196 +      let 
   3.197 +	  val cl_name = "pt_"^ak_name;
   3.198 +          val ty = TFree("'a",["HOL.type"]);
   3.199 +          val x   = Free ("x", ty);
   3.200 +          val pi1 = Free ("pi1", mk_permT T);
   3.201 +          val pi2 = Free ("pi2", mk_permT T);
   3.202 +          val cperm = Const ("nominal.perm", mk_permT T --> ty --> ty);
   3.203 +          val cnil  = Const ("List.list.Nil", mk_permT T);
   3.204 +          val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
   3.205 +          val cprm_eq = Const ("nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
   3.206 +          (* nil axiom *)
   3.207 +          val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
   3.208 +                       (cperm $ cnil $ x, x));
   3.209 +          (* append axiom *)
   3.210 +          val axiom2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
   3.211 +                       (cperm $ (cappend $ pi1 $ pi2) $ x, cperm $ pi1 $ (cperm $ pi2 $ x)));
   3.212 +          (* perm-eq axiom *)
   3.213 +          val axiom3 = Logic.mk_implies
   3.214 +                       (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
   3.215 +                        HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
   3.216 +      in
   3.217 +        thy |> AxClass.add_axclass_i (cl_name, ["HOL.type"])
   3.218 +                [((cl_name^"1", axiom1),[Simplifier.simp_add_global]), 
   3.219 +                 ((cl_name^"2", axiom2),[]),                           
   3.220 +                 ((cl_name^"3", axiom3),[])]                          
   3.221 +      end) (thy6,ak_names_types);
   3.222 +
   3.223 +    (* proves that every pt_<ak>-type together with <ak>-type *)
   3.224 +    (* instance of pt                                         *)
   3.225 +    (* lemma pt_<ak>_inst:                                    *)
   3.226 +    (* pt TYPE('x::pt_<ak>) TYPE(<ak>)                        *)
   3.227 +    val (thy8, prm_inst_thms) = 
   3.228 +      thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
   3.229 +      let
   3.230 +        val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name);
   3.231 +        val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);
   3.232 +        val i_type1 = TFree("'x",[pt_name_qu]);
   3.233 +        val i_type2 = Type(ak_name_qu,[]);
   3.234 +	val cpt = Const ("nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   3.235 +        val pt_type = Logic.mk_type i_type1;
   3.236 +        val at_type = Logic.mk_type i_type2;
   3.237 +        val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy7
   3.238 +                                  [Name "pt_def",
   3.239 +                                   Name ("pt_" ^ ak_name ^ "1"),
   3.240 +                                   Name ("pt_" ^ ak_name ^ "2"),
   3.241 +                                   Name ("pt_" ^ ak_name ^ "3")];
   3.242 +
   3.243 +	val name = "pt_"^ak_name^ "_inst";
   3.244 +        val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type);
   3.245 +
   3.246 +        val proof = fn _ => [auto_tac (claset(),simp_s)];
   3.247 +      in 
   3.248 +        ((name, prove_goalw_cterm [] (cterm_of (sign_of thy7) statement) proof), []) 
   3.249 +      end) ak_names_types);
   3.250 +
   3.251 +     (* declares an fs-axclass for every atom-kind       *)
   3.252 +     (* axclass fs_<ak>                                  *)
   3.253 +     (* fs_<ak>1: finite ((supp x)::<ak> set)            *)
   3.254 +     val (thy11, fs_ax_classes) =  foldl_map (fn (thy, (ak_name, T)) =>
   3.255 +       let 
   3.256 +	  val cl_name = "fs_"^ak_name;
   3.257 +	  val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.258 +          val ty = TFree("'a",["HOL.type"]);
   3.259 +          val x   = Free ("x", ty);
   3.260 +          val csupp    = Const ("nominal.supp", ty --> HOLogic.mk_setT T);
   3.261 +          val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
   3.262 +          
   3.263 +          val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
   3.264 +
   3.265 +       in  
   3.266 +        thy |> AxClass.add_axclass_i (cl_name, [pt_name]) [((cl_name^"1", axiom1),[])]            
   3.267 +       end) (thy8,ak_names_types); 
   3.268 +
   3.269 +     (* proves that every fs_<ak>-type together with <ak>-type   *)
   3.270 +     (* instance of fs-type                                      *)
   3.271 +     (* lemma abst_<ak>_inst:                                    *)
   3.272 +     (* fs TYPE('x::pt_<ak>) TYPE (<ak>)                         *)
   3.273 +     val (thy12, fs_inst_thms) = 
   3.274 +       thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
   3.275 +       let
   3.276 +         val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name);
   3.277 +         val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);
   3.278 +         val i_type1 = TFree("'x",[fs_name_qu]);
   3.279 +         val i_type2 = Type(ak_name_qu,[]);
   3.280 + 	 val cfs = Const ("nominal.fs", 
   3.281 +                                 (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   3.282 +         val fs_type = Logic.mk_type i_type1;
   3.283 +         val at_type = Logic.mk_type i_type2;
   3.284 +	 val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy11
   3.285 +                                   [Name "fs_def",
   3.286 +                                    Name ("fs_" ^ ak_name ^ "1")];
   3.287 +    
   3.288 +	 val name = "fs_"^ak_name^ "_inst";
   3.289 +         val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type);
   3.290 +
   3.291 +         val proof = fn _ => [auto_tac (claset(),simp_s)];
   3.292 +       in 
   3.293 +         ((name, prove_goalw_cterm [] (cterm_of (sign_of thy11) statement) proof), []) 
   3.294 +       end) ak_names_types);
   3.295 +
   3.296 +       (* declares for every atom-kind combination an axclass            *)
   3.297 +       (* cp_<ak1>_<ak2> giving a composition property                   *)
   3.298 +       (* cp_<ak1>_<ak2>1: pi1 o pi2 o x = (pi1 o pi2) o (pi1 o x)       *)
   3.299 +        val (thy12b,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.300 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.301 +	     let
   3.302 +	       val cl_name = "cp_"^ak_name^"_"^ak_name';
   3.303 +	       val ty = TFree("'a",["HOL.type"]);
   3.304 +               val x   = Free ("x", ty);
   3.305 +               val pi1 = Free ("pi1", mk_permT T);
   3.306 +	       val pi2 = Free ("pi2", mk_permT T');                  
   3.307 +	       val cperm1 = Const ("nominal.perm", mk_permT T  --> ty --> ty);
   3.308 +               val cperm2 = Const ("nominal.perm", mk_permT T' --> ty --> ty);
   3.309 +               val cperm3 = Const ("nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
   3.310 +
   3.311 +               val ax1   = HOLogic.mk_Trueprop 
   3.312 +			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
   3.313 +                                           cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
   3.314 +	       in  
   3.315 +	       (fst (AxClass.add_axclass_i (cl_name, ["HOL.type"]) [((cl_name^"1", ax1),[])] thy'),())  
   3.316 +	       end) 
   3.317 +	   (thy, ak_names_types)) (thy12, ak_names_types)
   3.318 +
   3.319 +        (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
   3.320 +        (* lemma cp_<ak1>_<ak2>_inst:                                           *)
   3.321 +        (* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>)                  *)
   3.322 +        val (thy12c, cp_thms) = foldl_map (fn (thy, (ak_name, T)) =>
   3.323 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.324 +           let
   3.325 +             val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
   3.326 +	     val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
   3.327 +             val cp_name_qu  = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   3.328 +             val i_type0 = TFree("'a",[cp_name_qu]);
   3.329 +             val i_type1 = Type(ak_name_qu,[]);
   3.330 +             val i_type2 = Type(ak_name_qu',[]);
   3.331 +	     val ccp = Const ("nominal.cp",
   3.332 +                             (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
   3.333 +                                                      (Term.itselfT i_type2)-->HOLogic.boolT);
   3.334 +             val at_type  = Logic.mk_type i_type1;
   3.335 +             val at_type' = Logic.mk_type i_type2;
   3.336 +	     val cp_type  = Logic.mk_type i_type0;
   3.337 +             val simp_s   = HOL_basic_ss addsimps PureThy.get_thmss thy' [(Name "cp_def")];
   3.338 +	     val cp1      = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"1"));
   3.339 +
   3.340 +	     val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
   3.341 +             val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
   3.342 +
   3.343 +             val proof = fn _ => [auto_tac (claset(),simp_s), rtac cp1 1];
   3.344 +	   in
   3.345 +	     thy' |> PureThy.add_thms 
   3.346 +                    [((name, prove_goalw_cterm [] (cterm_of (sign_of thy') statement) proof), [])]
   3.347 +	   end) 
   3.348 +	   (thy, ak_names_types)) (thy12b, ak_names_types);
   3.349 +       
   3.350 +        (* proves for every non-trivial <ak>-combination a disjointness   *)
   3.351 +        (* theorem; i.e. <ak1> != <ak2>                                   *)
   3.352 +        (* lemma ds_<ak1>_<ak2>:                                          *)
   3.353 +        (* dj TYPE(<ak1>) TYPE(<ak2>)                                     *)
   3.354 +        val (thy12d, dj_thms) = foldl_map (fn (thy, (ak_name, T)) =>
   3.355 +	  foldl_map (fn (thy', (ak_name', T')) =>
   3.356 +          (if not (ak_name = ak_name') 
   3.357 +           then 
   3.358 +	       let
   3.359 +		 val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
   3.360 +	         val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
   3.361 +                 val i_type1 = Type(ak_name_qu,[]);
   3.362 +                 val i_type2 = Type(ak_name_qu',[]);
   3.363 +	         val cdj = Const ("nominal.disjoint",
   3.364 +                           (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   3.365 +                 val at_type  = Logic.mk_type i_type1;
   3.366 +                 val at_type' = Logic.mk_type i_type2;
   3.367 +                 val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy' 
   3.368 +					   [Name "disjoint_def",
   3.369 +                                            Name (ak_name^"_prm_"^ak_name'^"_def"),
   3.370 +                                            Name (ak_name'^"_prm_"^ak_name^"_def")];
   3.371 +
   3.372 +	         val name = "dj_"^ak_name^"_"^ak_name';
   3.373 +                 val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');
   3.374 +
   3.375 +                 val proof = fn _ => [auto_tac (claset(),simp_s)];
   3.376 +	       in
   3.377 +		   thy' |> PureThy.add_thms 
   3.378 +                        [((name, prove_goalw_cterm [] (cterm_of (sign_of thy') statement) proof), []) ]
   3.379 +	       end
   3.380 +           else 
   3.381 +            (thy',[])))  (* do nothing branch, if ak_name = ak_name' *) 
   3.382 +	   (thy, ak_names_types)) (thy12c, ak_names_types);
   3.383 +
   3.384 +     (*<<<<<<<  pt_<ak> class instances  >>>>>>>*)
   3.385 +     (*=========================================*)
   3.386 +     
   3.387 +     (* some frequently used theorems *)
   3.388 +      val pt1 = PureThy.get_thm thy12c (Name "pt1");
   3.389 +      val pt2 = PureThy.get_thm thy12c (Name "pt2");
   3.390 +      val pt3 = PureThy.get_thm thy12c (Name "pt3");
   3.391 +      val at_pt_inst    = PureThy.get_thm thy12c (Name "at_pt_inst");
   3.392 +      val pt_bool_inst  = PureThy.get_thm thy12c (Name "pt_bool_inst");
   3.393 +      val pt_set_inst   = PureThy.get_thm thy12c (Name "pt_set_inst"); 
   3.394 +      val pt_unit_inst  = PureThy.get_thm thy12c (Name "pt_unit_inst");
   3.395 +      val pt_prod_inst  = PureThy.get_thm thy12c (Name "pt_prod_inst"); 
   3.396 +      val pt_list_inst  = PureThy.get_thm thy12c (Name "pt_list_inst");   
   3.397 +      val pt_optn_inst  = PureThy.get_thm thy12c (Name "pt_option_inst");   
   3.398 +      val pt_noptn_inst = PureThy.get_thm thy12c (Name "pt_noption_inst");   
   3.399 +      val pt_fun_inst   = PureThy.get_thm thy12c (Name "pt_fun_inst");     
   3.400 +
   3.401 +     (* for all atom-kind combination shows that         *)
   3.402 +     (* every <ak> is an instance of pt_<ai>             *)
   3.403 +     val (thy13,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.404 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.405 +          (if ak_name = ak_name'
   3.406 +	   then
   3.407 +	     let
   3.408 +	      val qu_name =  Sign.full_name (sign_of thy') ak_name;
   3.409 +              val qu_class = Sign.full_name (sign_of thy') ("pt_"^ak_name);
   3.410 +              val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name ^"_inst"));
   3.411 +              val proof = EVERY [AxClass.intro_classes_tac [],
   3.412 +                                 rtac ((at_inst RS at_pt_inst) RS pt1) 1,
   3.413 +                                 rtac ((at_inst RS at_pt_inst) RS pt2) 1,
   3.414 +                                 rtac ((at_inst RS at_pt_inst) RS pt3) 1,
   3.415 +                                 atac 1];
   3.416 +             in 
   3.417 +	      (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy',()) 
   3.418 +             end
   3.419 +           else 
   3.420 +             let
   3.421 +	      val qu_name' = Sign.full_name (sign_of thy') ak_name';
   3.422 +              val qu_class = Sign.full_name (sign_of thy') ("pt_"^ak_name);
   3.423 +              val simp_s = HOL_basic_ss addsimps 
   3.424 +                           PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")];  
   3.425 +              val proof = EVERY [AxClass.intro_classes_tac [], auto_tac (claset(),simp_s)];
   3.426 +             in 
   3.427 +	      (AxClass.add_inst_arity_i (qu_name',[],[qu_class]) proof thy',()) 
   3.428 +             end)) 
   3.429 +	     (thy, ak_names_types)) (thy12c, ak_names_types);
   3.430 +
   3.431 +     (* shows that bool is an instance of pt_<ak>     *)
   3.432 +     (* uses the theorem pt_bool_inst                 *)
   3.433 +     val (thy14,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.434 +       let
   3.435 +          val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.436 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.437 +                             rtac (pt_bool_inst RS pt1) 1,
   3.438 +                             rtac (pt_bool_inst RS pt2) 1,
   3.439 +                             rtac (pt_bool_inst RS pt3) 1,
   3.440 +                             atac 1];
   3.441 +       in 
   3.442 +	 (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy,()) 
   3.443 +       end) (thy13,ak_names_types); 
   3.444 +
   3.445 +     (* shows that set(pt_<ak>) is an instance of pt_<ak>          *)
   3.446 +     (* unfolds the permutation definition and applies pt_<ak>i    *)
   3.447 +     val (thy15,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.448 +       let
   3.449 +          val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.450 +          val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));  
   3.451 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.452 +                             rtac ((pt_inst RS pt_set_inst) RS pt1) 1,
   3.453 +                             rtac ((pt_inst RS pt_set_inst) RS pt2) 1,
   3.454 +                             rtac ((pt_inst RS pt_set_inst) RS pt3) 1,
   3.455 +                             atac 1];
   3.456 +       in 
   3.457 +	 (AxClass.add_inst_arity_i ("set",[[qu_class]],[qu_class]) proof thy,()) 
   3.458 +       end) (thy14,ak_names_types); 
   3.459 +
   3.460 +     (* shows that unit is an instance of pt_<ak>          *)
   3.461 +     val (thy16,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.462 +       let
   3.463 +          val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.464 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.465 +                             rtac (pt_unit_inst RS pt1) 1,
   3.466 +                             rtac (pt_unit_inst RS pt2) 1,
   3.467 +                             rtac (pt_unit_inst RS pt3) 1,
   3.468 +                             atac 1];
   3.469 +       in 
   3.470 +	 (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy,()) 
   3.471 +       end) (thy15,ak_names_types); 
   3.472 +
   3.473 +     (* shows that *(pt_<ak>,pt_<ak>) is an instance of pt_<ak> *)
   3.474 +     (* uses the theorem pt_prod_inst and pt_<ak>_inst          *)
   3.475 +     val (thy17,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.476 +       let
   3.477 +          val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.478 +          val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));  
   3.479 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.480 +                             rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt1) 1,
   3.481 +                             rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt2) 1,
   3.482 +                             rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt3) 1,
   3.483 +                             atac 1];
   3.484 +       in 
   3.485 +          (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy,()) 
   3.486 +       end) (thy16,ak_names_types); 
   3.487 +
   3.488 +     (* shows that list(pt_<ak>) is an instance of pt_<ak>     *)
   3.489 +     (* uses the theorem pt_list_inst and pt_<ak>_inst         *)
   3.490 +     val (thy18,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.491 +       let
   3.492 +          val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.493 +          val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   3.494 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.495 +                             rtac ((pt_inst RS pt_list_inst) RS pt1) 1,
   3.496 +                             rtac ((pt_inst RS pt_list_inst) RS pt2) 1,
   3.497 +                             rtac ((pt_inst RS pt_list_inst) RS pt3) 1,
   3.498 +                             atac 1];      
   3.499 +       in 
   3.500 +	 (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy,()) 
   3.501 +       end) (thy17,ak_names_types); 
   3.502 +
   3.503 +     (* shows that option(pt_<ak>) is an instance of pt_<ak>   *)
   3.504 +     (* uses the theorem pt_option_inst and pt_<ak>_inst       *)
   3.505 +     val (thy18a,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.506 +       let
   3.507 +          val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.508 +          val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   3.509 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.510 +                             rtac ((pt_inst RS pt_optn_inst) RS pt1) 1,
   3.511 +                             rtac ((pt_inst RS pt_optn_inst) RS pt2) 1,
   3.512 +                             rtac ((pt_inst RS pt_optn_inst) RS pt3) 1,
   3.513 +                             atac 1];      
   3.514 +       in 
   3.515 +	 (AxClass.add_inst_arity_i ("Datatype.option",[[qu_class]],[qu_class]) proof thy,()) 
   3.516 +       end) (thy18,ak_names_types); 
   3.517 +
   3.518 +     (* shows that nOption(pt_<ak>) is an instance of pt_<ak>   *)
   3.519 +     (* uses the theorem pt_option_inst and pt_<ak>_inst       *)
   3.520 +     val (thy18b,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.521 +       let
   3.522 +          val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.523 +          val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   3.524 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.525 +                             rtac ((pt_inst RS pt_noptn_inst) RS pt1) 1,
   3.526 +                             rtac ((pt_inst RS pt_noptn_inst) RS pt2) 1,
   3.527 +                             rtac ((pt_inst RS pt_noptn_inst) RS pt3) 1,
   3.528 +                             atac 1];      
   3.529 +       in 
   3.530 +	 (AxClass.add_inst_arity_i ("nominal.nOption",[[qu_class]],[qu_class]) proof thy,()) 
   3.531 +       end) (thy18a,ak_names_types); 
   3.532 +
   3.533 +
   3.534 +     (* shows that fun(pt_<ak>,pt_<ak>) is an instance of pt_<ak>     *)
   3.535 +     (* uses the theorem pt_list_inst and pt_<ak>_inst                *)
   3.536 +     val (thy19,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.537 +       let
   3.538 +          val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   3.539 +          val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
   3.540 +          val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   3.541 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.542 +                             rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt1) 1,
   3.543 +                             rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt2) 1,
   3.544 +                             rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt3) 1,
   3.545 +                             atac 1];      
   3.546 +       in 
   3.547 +	 (AxClass.add_inst_arity_i ("fun",[[qu_class],[qu_class]],[qu_class]) proof thy,()) 
   3.548 +       end) (thy18b,ak_names_types);
   3.549 +
   3.550 +       (*<<<<<<<  fs_<ak> class instances  >>>>>>>*)
   3.551 +       (*=========================================*)
   3.552 +       val fs1          = PureThy.get_thm thy19 (Name "fs1");
   3.553 +       val fs_at_inst   = PureThy.get_thm thy19 (Name "fs_at_inst");
   3.554 +       val fs_unit_inst = PureThy.get_thm thy19 (Name "fs_unit_inst");
   3.555 +       val fs_bool_inst = PureThy.get_thm thy19 (Name "fs_bool_inst");
   3.556 +       val fs_prod_inst = PureThy.get_thm thy19 (Name "fs_prod_inst");
   3.557 +       val fs_list_inst = PureThy.get_thm thy19 (Name "fs_list_inst");
   3.558 +
   3.559 +       (* shows that <ak> is an instance of fs_<ak>     *)
   3.560 +       (* uses the theorem at_<ak>_inst                 *)
   3.561 +       val (thy20,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.562 +       let
   3.563 +          val qu_name =  Sign.full_name (sign_of thy) ak_name;
   3.564 +          val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   3.565 +          val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
   3.566 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.567 +                             rtac ((at_thm RS fs_at_inst) RS fs1) 1];      
   3.568 +       in 
   3.569 +	 (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy,()) 
   3.570 +       end) (thy19,ak_names_types);  
   3.571 +
   3.572 +       (* shows that unit is an instance of fs_<ak>     *)
   3.573 +       (* uses the theorem fs_unit_inst                 *)
   3.574 +       val (thy21,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.575 +       let
   3.576 +          val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   3.577 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.578 +                             rtac (fs_unit_inst RS fs1) 1];      
   3.579 +       in 
   3.580 +	 (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy,()) 
   3.581 +       end) (thy20,ak_names_types);  
   3.582 +
   3.583 +       (* shows that bool is an instance of fs_<ak>     *)
   3.584 +       (* uses the theorem fs_bool_inst                 *)
   3.585 +       val (thy22,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.586 +       let
   3.587 +          val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   3.588 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.589 +                             rtac (fs_bool_inst RS fs1) 1];      
   3.590 +       in 
   3.591 +	 (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy,()) 
   3.592 +       end) (thy21,ak_names_types);  
   3.593 +
   3.594 +       (* shows that *(fs_<ak>,fs_<ak>) is an instance of fs_<ak>     *)
   3.595 +       (* uses the theorem fs_prod_inst                               *)
   3.596 +       val (thy23,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.597 +       let
   3.598 +          val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   3.599 +          val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
   3.600 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.601 +                             rtac ((fs_inst RS (fs_inst RS fs_prod_inst)) RS fs1) 1];      
   3.602 +       in 
   3.603 +	 (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy,()) 
   3.604 +       end) (thy22,ak_names_types);  
   3.605 +
   3.606 +       (* shows that list(fs_<ak>) is an instance of fs_<ak>     *)
   3.607 +       (* uses the theorem fs_list_inst                          *)
   3.608 +       val (thy24,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.609 +       let
   3.610 +          val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   3.611 +          val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
   3.612 +          val proof = EVERY [AxClass.intro_classes_tac [],
   3.613 +                              rtac ((fs_inst RS fs_list_inst) RS fs1) 1];      
   3.614 +       in 
   3.615 +	 (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy,()) 
   3.616 +       end) (thy23,ak_names_types);  
   3.617 +	   
   3.618 +       (*<<<<<<<  cp_<ak>_<ai> class instances  >>>>>>>*)
   3.619 +       (*==============================================*)
   3.620 +       val cp1             = PureThy.get_thm thy24 (Name "cp1");
   3.621 +       val cp_unit_inst    = PureThy.get_thm thy24 (Name "cp_unit_inst");
   3.622 +       val cp_bool_inst    = PureThy.get_thm thy24 (Name "cp_bool_inst");
   3.623 +       val cp_prod_inst    = PureThy.get_thm thy24 (Name "cp_prod_inst");
   3.624 +       val cp_list_inst    = PureThy.get_thm thy24 (Name "cp_list_inst");
   3.625 +       val cp_fun_inst     = PureThy.get_thm thy24 (Name "cp_fun_inst");
   3.626 +       val cp_option_inst  = PureThy.get_thm thy24 (Name "cp_option_inst");
   3.627 +       val cp_noption_inst = PureThy.get_thm thy24 (Name "cp_noption_inst");
   3.628 +       val pt_perm_compose = PureThy.get_thm thy24 (Name "pt_perm_compose");
   3.629 +       val dj_pp_forget    = PureThy.get_thm thy24 (Name "dj_perm_perm_forget");
   3.630 +
   3.631 +       (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
   3.632 +       (* that needs a three-nested loop *)
   3.633 +       val (thy25,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.634 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.635 +          foldl_map (fn (thy'', (ak_name'', T'')) =>
   3.636 +            let
   3.637 +              val qu_name =  Sign.full_name (sign_of thy'') ak_name;
   3.638 +              val qu_class = Sign.full_name (sign_of thy'') ("cp_"^ak_name'^"_"^ak_name'');
   3.639 +              val proof =
   3.640 +                (if (ak_name'=ak_name'') then 
   3.641 +		  (let
   3.642 +                    val pt_inst  = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
   3.643 +		    val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
   3.644 +                  in 
   3.645 +		   EVERY [AxClass.intro_classes_tac [], 
   3.646 +                          rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
   3.647 +                  end)
   3.648 +		else
   3.649 +		  (let 
   3.650 +                     val dj_inst  = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name'));
   3.651 +		     val simp_s = HOL_basic_ss addsimps 
   3.652 +                                        ((dj_inst RS dj_pp_forget)::
   3.653 +                                         (PureThy.get_thmss thy'' 
   3.654 +					   [Name (ak_name' ^"_prm_"^ak_name^"_def"),
   3.655 +                                            Name (ak_name''^"_prm_"^ak_name^"_def")]));  
   3.656 +		  in 
   3.657 +                    EVERY [AxClass.intro_classes_tac [], simp_tac simp_s 1]
   3.658 +                  end))
   3.659 +	      in
   3.660 +                (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy'',())
   3.661 +	      end)
   3.662 +	   (thy', ak_names_types)) (thy, ak_names_types)) (thy24, ak_names_types);
   3.663 +      
   3.664 +       (* shows that unit is an instance of cp_<ak>_<ai>     *)
   3.665 +       (* for every <ak>-combination                         *)
   3.666 +       val (thy26,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.667 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.668 +          let
   3.669 +            val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   3.670 +            val proof = EVERY [AxClass.intro_classes_tac [],rtac (cp_unit_inst RS cp1) 1];     
   3.671 +	  in
   3.672 +            (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy',())
   3.673 +	  end) 
   3.674 +	   (thy, ak_names_types)) (thy25, ak_names_types);
   3.675 +       
   3.676 +       (* shows that bool is an instance of cp_<ak>_<ai>     *)
   3.677 +       (* for every <ak>-combination                         *)
   3.678 +       val (thy27,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.679 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.680 +           let
   3.681 +	     val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   3.682 +             val proof = EVERY [AxClass.intro_classes_tac [], rtac (cp_bool_inst RS cp1) 1];     
   3.683 +	   in
   3.684 +             (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy',())
   3.685 +	   end) 
   3.686 +	   (thy, ak_names_types)) (thy26, ak_names_types);
   3.687 +
   3.688 +       (* shows that prod is an instance of cp_<ak>_<ai>     *)
   3.689 +       (* for every <ak>-combination                         *)
   3.690 +       val (thy28,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.691 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.692 +          let
   3.693 +	    val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   3.694 +            val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   3.695 +            val proof = EVERY [AxClass.intro_classes_tac [],
   3.696 +                               rtac ((cp_inst RS (cp_inst RS cp_prod_inst)) RS cp1) 1];     
   3.697 +	  in
   3.698 +            (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy',())
   3.699 +	  end)  
   3.700 +	  (thy, ak_names_types)) (thy27, ak_names_types);
   3.701 +
   3.702 +       (* shows that list is an instance of cp_<ak>_<ai>     *)
   3.703 +       (* for every <ak>-combination                         *)
   3.704 +       val (thy29,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.705 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.706 +           let
   3.707 +	     val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   3.708 +             val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   3.709 +             val proof = EVERY [AxClass.intro_classes_tac [],
   3.710 +                                rtac ((cp_inst RS cp_list_inst) RS cp1) 1];     
   3.711 +	   in
   3.712 +            (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy',())
   3.713 +	   end) 
   3.714 +	   (thy, ak_names_types)) (thy28, ak_names_types);
   3.715 +
   3.716 +       (* shows that function is an instance of cp_<ak>_<ai>     *)
   3.717 +       (* for every <ak>-combination                             *)
   3.718 +       val (thy30,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.719 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.720 +          let
   3.721 +	    val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   3.722 +            val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   3.723 +            val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
   3.724 +            val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
   3.725 +            val proof = EVERY [AxClass.intro_classes_tac [],
   3.726 +                    rtac ((at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)))) RS cp1) 1];  
   3.727 +	  in
   3.728 +            (AxClass.add_inst_arity_i ("fun",[[qu_class],[qu_class]],[qu_class]) proof thy',())
   3.729 +	  end) 
   3.730 +	  (thy, ak_names_types)) (thy29, ak_names_types);
   3.731 +
   3.732 +       (* shows that option is an instance of cp_<ak>_<ai>     *)
   3.733 +       (* for every <ak>-combination                           *)
   3.734 +       val (thy31,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.735 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.736 +          let
   3.737 +	    val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   3.738 +            val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   3.739 +            val proof = EVERY [AxClass.intro_classes_tac [],
   3.740 +                               rtac ((cp_inst RS cp_option_inst) RS cp1) 1];     
   3.741 +	  in
   3.742 +            (AxClass.add_inst_arity_i ("Datatype.option",[[qu_class]],[qu_class]) proof thy',())
   3.743 +	  end) 
   3.744 +	  (thy, ak_names_types)) (thy30, ak_names_types);
   3.745 +
   3.746 +       (* shows that nOption is an instance of cp_<ak>_<ai>     *)
   3.747 +       (* for every <ak>-combination                            *)
   3.748 +       val (thy32,_) = foldl_map (fn (thy, (ak_name, T)) =>
   3.749 +	 foldl_map (fn (thy', (ak_name', T')) =>
   3.750 +          let
   3.751 +	    val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   3.752 +            val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   3.753 +            val proof = EVERY [AxClass.intro_classes_tac [],
   3.754 +                               rtac ((cp_inst RS cp_noption_inst) RS cp1) 1];     
   3.755 +	  in
   3.756 +           (AxClass.add_inst_arity_i ("nominal.nOption",[[qu_class]],[qu_class]) proof thy',())
   3.757 +	  end) 
   3.758 +	  (thy, ak_names_types)) (thy31, ak_names_types);
   3.759 +
   3.760 +       (* abbreviations for some collection of rules *)
   3.761 +       (*============================================*)
   3.762 +       val abs_fun_pi        = PureThy.get_thm thy32 (Name ("nominal.abs_fun_pi"));
   3.763 +       val abs_fun_pi_ineq   = PureThy.get_thm thy32 (Name ("nominal.abs_fun_pi_ineq"));
   3.764 +       val abs_fun_eq        = PureThy.get_thm thy32 (Name ("nominal.abs_fun_eq"));
   3.765 +       val dj_perm_forget    = PureThy.get_thm thy32 (Name ("nominal.dj_perm_forget"));
   3.766 +       val dj_pp_forget      = PureThy.get_thm thy32 (Name ("nominal.dj_perm_perm_forget"));
   3.767 +       val fresh_iff         = PureThy.get_thm thy32 (Name ("nominal.fresh_abs_fun_iff"));
   3.768 +       val fresh_iff_ineq    = PureThy.get_thm thy32 (Name ("nominal.fresh_abs_fun_iff_ineq"));
   3.769 +       val abs_fun_supp      = PureThy.get_thm thy32 (Name ("nominal.abs_fun_supp"));
   3.770 +       val abs_fun_supp_ineq = PureThy.get_thm thy32 (Name ("nominal.abs_fun_supp_ineq"));
   3.771 +       val pt_swap_bij       = PureThy.get_thm thy32 (Name ("nominal.pt_swap_bij"));
   3.772 +       val pt_fresh_fresh    = PureThy.get_thm thy32 (Name ("nominal.pt_fresh_fresh"));
   3.773 +       val pt_bij            = PureThy.get_thm thy32 (Name ("nominal.pt_bij"));
   3.774 +       val pt_perm_compose   = PureThy.get_thm thy32 (Name ("nominal.pt_perm_compose"));
   3.775 +       val perm_eq_app       = PureThy.get_thm thy32 (Name ("nominal.perm_eq_app"));
   3.776 +
   3.777 +       (* abs_perm collects all lemmas for simplifying a permutation *)
   3.778 +       (* in front of an abs_fun                                     *)
   3.779 +       val (thy33,_) = 
   3.780 +	   let 
   3.781 +	     val name = "abs_perm"
   3.782 +             val thm_list = Library.flat (map (fn (ak_name, T) =>
   3.783 +	        let	
   3.784 +		  val at_inst = PureThy.get_thm thy32 (Name ("at_"^ak_name^"_inst"));
   3.785 +		  val pt_inst = PureThy.get_thm thy32 (Name ("pt_"^ak_name^"_inst"));	      
   3.786 +	          val thm = [pt_inst, at_inst] MRS abs_fun_pi
   3.787 +                  val thm_list = map (fn (ak_name', T') =>
   3.788 +                     let
   3.789 +                      val cp_inst = PureThy.get_thm thy32 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   3.790 +	             in
   3.791 +                     [pt_inst, pt_inst, at_inst, cp_inst] MRS abs_fun_pi_ineq
   3.792 +	             end) ak_names_types;
   3.793 +                 in thm::thm_list end) (ak_names_types))
   3.794 +           in
   3.795 +             (PureThy.add_thmss [((name, thm_list),[])] thy32)
   3.796 +           end;
   3.797 +
   3.798 +        (* alpha collects all lemmas analysing an equation *)
   3.799 +        (* between abs_funs                                *)
   3.800 +        (*val (thy34,_) = 
   3.801 +	   let 
   3.802 +	     val name = "alpha"
   3.803 +             val thm_list = map (fn (ak_name, T) =>
   3.804 +	        let	
   3.805 +		  val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
   3.806 +		  val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
   3.807 +	        in
   3.808 +                  [pt_inst, at_inst] MRS abs_fun_eq
   3.809 +	        end) ak_names_types
   3.810 +           in
   3.811 +             (PureThy.add_thmss [((name, thm_list),[])] thy33)
   3.812 +           end;*)
   3.813 + 
   3.814 +          val (thy34,_) = 
   3.815 +	   let 
   3.816 +	     fun inst_pt_at thm ak_name =
   3.817 +		 let	
   3.818 +		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
   3.819 +		   val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
   3.820 +	         in
   3.821 +                     [pt_inst, at_inst] MRS thm
   3.822 +	         end	 
   3.823 +
   3.824 +           in
   3.825 +            thy33 
   3.826 +	    |> PureThy.add_thmss   [(("alpha", map (inst_pt_at abs_fun_eq) ak_names),[])]
   3.827 +            |>>> PureThy.add_thmss [(("perm_swap", map (inst_pt_at pt_swap_bij) ak_names),[])]
   3.828 +            |>>> PureThy.add_thmss [(("perm_fresh_fresh", map (inst_pt_at pt_fresh_fresh) ak_names),[])]
   3.829 +            |>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])]
   3.830 +            |>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])]
   3.831 +            |>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])]
   3.832 +	   end;
   3.833 +
   3.834 +         (* perm_dj collects all lemmas that forget an permutation *)
   3.835 +         (* when it acts on an atom of different type              *)
   3.836 +         val (thy35,_) = 
   3.837 +	   let 
   3.838 +	     val name = "perm_dj"
   3.839 +             val thm_list = Library.flat (map (fn (ak_name, T) =>
   3.840 +	        Library.flat (map (fn (ak_name', T') => 
   3.841 +                 if not (ak_name = ak_name') 
   3.842 +                 then 
   3.843 +		    let
   3.844 +                      val dj_inst = PureThy.get_thm thy34 (Name ("dj_"^ak_name^"_"^ak_name'));
   3.845 +                    in
   3.846 +                      [dj_inst RS dj_perm_forget, dj_inst RS dj_pp_forget]
   3.847 +                    end 
   3.848 +                 else []) ak_names_types)) ak_names_types)
   3.849 +           in
   3.850 +             (PureThy.add_thmss [((name, thm_list),[])] thy34)
   3.851 +           end;
   3.852 +
   3.853 +         (* abs_fresh collects all lemmas for simplifying a freshness *)
   3.854 +         (* proposition involving an abs_fun                          *)
   3.855 +
   3.856 +         val (thy36,_) = 
   3.857 +	   let 
   3.858 +	     val name = "abs_fresh"
   3.859 +             val thm_list = Library.flat (map (fn (ak_name, T) =>
   3.860 +	        let	
   3.861 +		  val at_inst = PureThy.get_thm thy35 (Name ("at_"^ak_name^"_inst"));
   3.862 +		  val pt_inst = PureThy.get_thm thy35 (Name ("pt_"^ak_name^"_inst"));
   3.863 +                  val fs_inst = PureThy.get_thm thy35 (Name ("fs_"^ak_name^"_inst"));	      
   3.864 +	          val thm = [pt_inst, at_inst, (fs_inst RS fs1)] MRS fresh_iff
   3.865 +                  val thm_list = Library.flat (map (fn (ak_name', T') =>
   3.866 +                     (if (not (ak_name = ak_name')) 
   3.867 +                     then
   3.868 +                       let
   3.869 +                        val cp_inst = PureThy.get_thm thy35 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   3.870 +	                val dj_inst = PureThy.get_thm thy35 (Name ("dj_"^ak_name'^"_"^ak_name));
   3.871 +                       in
   3.872 +                        [[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS fresh_iff_ineq]
   3.873 +	               end
   3.874 +                     else [])) ak_names_types);
   3.875 +                 in thm::thm_list end) (ak_names_types))
   3.876 +           in
   3.877 +             (PureThy.add_thmss [((name, thm_list),[])] thy35)
   3.878 +           end;
   3.879 +
   3.880 +         (* abs_supp collects all lemmas for simplifying  *)
   3.881 +         (* support proposition involving an abs_fun      *)
   3.882 +
   3.883 +         val (thy37,_) = 
   3.884 +	   let 
   3.885 +	     val name = "abs_supp"
   3.886 +             val thm_list = Library.flat (map (fn (ak_name, T) =>
   3.887 +	        let	
   3.888 +		  val at_inst = PureThy.get_thm thy36 (Name ("at_"^ak_name^"_inst"));
   3.889 +		  val pt_inst = PureThy.get_thm thy36 (Name ("pt_"^ak_name^"_inst"));
   3.890 +                  val fs_inst = PureThy.get_thm thy36 (Name ("fs_"^ak_name^"_inst"));	      
   3.891 +	          val thm1 = [pt_inst, at_inst, (fs_inst RS fs1)] MRS abs_fun_supp
   3.892 +                  val thm2 = [pt_inst, at_inst] MRS abs_fun_supp
   3.893 +                  val thm_list = Library.flat (map (fn (ak_name', T') =>
   3.894 +                     (if (not (ak_name = ak_name')) 
   3.895 +                     then
   3.896 +                       let
   3.897 +                        val cp_inst = PureThy.get_thm thy36 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   3.898 +	                val dj_inst = PureThy.get_thm thy36 (Name ("dj_"^ak_name'^"_"^ak_name));
   3.899 +                       in
   3.900 +                        [[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS abs_fun_supp_ineq]
   3.901 +	               end
   3.902 +                     else [])) ak_names_types);
   3.903 +                 in thm1::thm2::thm_list end) (ak_names_types))
   3.904 +           in
   3.905 +             (PureThy.add_thmss [((name, thm_list),[])] thy36)
   3.906 +           end;
   3.907 +
   3.908 +    in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)
   3.909 +      (NominalData.get thy11)) thy37
   3.910 +    end;
   3.911 +
   3.912 +
   3.913 +(* syntax und parsing *)
   3.914 +structure P = OuterParse and K = OuterKeyword;
   3.915 +
   3.916 +val atom_declP =
   3.917 +  OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
   3.918 +    (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
   3.919 +
   3.920 +val _ = OuterSyntax.add_parsers [atom_declP];
   3.921 +
   3.922 +val setup = [NominalData.init];
   3.923 +
   3.924 +(*=======================================================================*)
   3.925 +
   3.926 +val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
   3.927 +
   3.928 +fun read_typ sign ((Ts, sorts), str) =
   3.929 +  let
   3.930 +    val T = Type.no_tvars (Sign.read_typ (sign, (AList.lookup op =)
   3.931 +      (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
   3.932 +  in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
   3.933 +
   3.934 +(** taken from HOL/Tools/datatype_aux.ML **)
   3.935 +
   3.936 +fun indtac indrule indnames i st =
   3.937 +  let
   3.938 +    val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
   3.939 +    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
   3.940 +      (Logic.strip_imp_concl (List.nth (prems_of st, i - 1))));
   3.941 +    val getP = if can HOLogic.dest_imp (hd ts) then
   3.942 +      (apfst SOME) o HOLogic.dest_imp else pair NONE;
   3.943 +    fun abstr (t1, t2) = (case t1 of
   3.944 +        NONE => (case filter (fn Free (s, _) => s mem indnames | _ => false)
   3.945 +              (term_frees t2) of
   3.946 +            [Free (s, T)] => absfree (s, T, t2)
   3.947 +          | _ => sys_error "indtac")
   3.948 +      | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
   3.949 +    val cert = cterm_of (Thm.sign_of_thm st);
   3.950 +    val Ps = map (cert o head_of o snd o getP) ts;
   3.951 +    val indrule' = cterm_instantiate (Ps ~~
   3.952 +      (map (cert o abstr o getP) ts')) indrule
   3.953 +  in
   3.954 +    rtac indrule' i st
   3.955 +  end;
   3.956 +
   3.957 +fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
   3.958 +  let
   3.959 +    (* this theory is used just for parsing *)
   3.960 +  
   3.961 +    val tmp_thy = thy |>
   3.962 +      Theory.copy |>
   3.963 +      Theory.add_types (map (fn (tvs, tname, mx, _) =>
   3.964 +        (tname, length tvs, mx)) dts);
   3.965 +
   3.966 +    val sign = Theory.sign_of tmp_thy;
   3.967 +
   3.968 +    val atoms = atoms_of thy;
   3.969 +    val classes = map (NameSpace.map_base (fn s => "pt_" ^ s)) atoms;
   3.970 +    val cp_classes = List.concat (map (fn atom1 => map (fn atom2 =>
   3.971 +      Sign.intern_class thy ("cp_" ^ Sign.base_name atom1 ^ "_" ^
   3.972 +        Sign.base_name atom2)) atoms) atoms);
   3.973 +    fun augment_sort S = S union classes;
   3.974 +    val augment_sort_typ = map_type_tfree (fn (s, S) => TFree (s, augment_sort S));
   3.975 +
   3.976 +    fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
   3.977 +      let val (cargs', sorts') = Library.foldl (prep_typ sign) (([], sorts), cargs)
   3.978 +      in (constrs @ [(cname, cargs', mx)], sorts') end
   3.979 +
   3.980 +    fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
   3.981 +      let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
   3.982 +      in (dts @ [(tvs, tname, mx, constrs')], sorts') end
   3.983 +
   3.984 +    val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
   3.985 +    val sorts' = map (apsnd augment_sort) sorts;
   3.986 +    val tyvars = map #1 dts';
   3.987 +
   3.988 +    val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
   3.989 +    val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
   3.990 +      map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
   3.991 +
   3.992 +    val ps = map (fn (_, n, _, _) =>
   3.993 +      (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
   3.994 +    val rps = map Library.swap ps;
   3.995 +
   3.996 +    fun replace_types (Type ("nominal.ABS", [T, U])) = 
   3.997 +          Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
   3.998 +      | replace_types (Type (s, Ts)) =
   3.999 +          Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
  3.1000 +      | replace_types T = T;
  3.1001 +
  3.1002 +    fun replace_types' (Type (s, Ts)) =
  3.1003 +          Type (getOpt (AList.lookup op = rps s, s), map replace_types' Ts)
  3.1004 +      | replace_types' T = T;
  3.1005 +
  3.1006 +    val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
  3.1007 +      map (fn (cname, cargs, mx) => (cname,
  3.1008 +        map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts';
  3.1009 +
  3.1010 +    val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
  3.1011 +    val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';
  3.1012 +
  3.1013 +    val (thy1, {induction, ...}) =
  3.1014 +      DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
  3.1015 +
  3.1016 +    val SOME {descr, ...} = Symtab.lookup
  3.1017 +      (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
  3.1018 +    val typ_of_dtyp = typ_of_dtyp descr sorts';
  3.1019 +    fun nth_dtyp i = typ_of_dtyp (DtRec i);
  3.1020 +
  3.1021 +    (**** define permutation functions ****)
  3.1022 +
  3.1023 +    val permT = mk_permT (TFree ("'x", HOLogic.typeS));
  3.1024 +    val pi = Free ("pi", permT);
  3.1025 +    val perm_types = map (fn (i, _) =>
  3.1026 +      let val T = nth_dtyp i
  3.1027 +      in permT --> T --> T end) descr;
  3.1028 +    val perm_names = replicate (length new_type_names) "nominal.perm" @
  3.1029 +      DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
  3.1030 +        ("perm_" ^ name_of_typ (nth_dtyp i)))
  3.1031 +          (length new_type_names upto length descr - 1));
  3.1032 +    val perm_names_types = perm_names ~~ perm_types;
  3.1033 +
  3.1034 +    val perm_eqs = List.concat (map (fn (i, (_, _, constrs)) =>
  3.1035 +      let val T = nth_dtyp i
  3.1036 +      in map (fn (cname, dts) => 
  3.1037 +        let
  3.1038 +          val Ts = map typ_of_dtyp dts;
  3.1039 +          val names = DatatypeProp.make_tnames Ts;
  3.1040 +          val args = map Free (names ~~ Ts);
  3.1041 +          val c = Const (cname, Ts ---> T);
  3.1042 +          fun perm_arg (dt, x) =
  3.1043 +            let val T = type_of x
  3.1044 +            in if is_rec_type dt then
  3.1045 +                let val (Us, _) = strip_type T
  3.1046 +                in list_abs (map (pair "x") Us,
  3.1047 +                  Const (List.nth (perm_names_types, body_index dt)) $ pi $
  3.1048 +                    list_comb (x, map (fn (i, U) =>
  3.1049 +                      Const ("nominal.perm", permT --> U --> U) $
  3.1050 +                        (Const ("List.rev", permT --> permT) $ pi) $
  3.1051 +                        Bound i) ((length Us - 1 downto 0) ~~ Us)))
  3.1052 +                end
  3.1053 +              else Const ("nominal.perm", permT --> T --> T) $ pi $ x
  3.1054 +            end;  
  3.1055 +        in
  3.1056 +          (("", HOLogic.mk_Trueprop (HOLogic.mk_eq
  3.1057 +            (Const (List.nth (perm_names_types, i)) $
  3.1058 +               Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
  3.1059 +               list_comb (c, args),
  3.1060 +             list_comb (c, map perm_arg (dts ~~ args))))), [])
  3.1061 +        end) constrs
  3.1062 +      end) descr);
  3.1063 +
  3.1064 +    val (thy2, perm_simps) = thy1 |>
  3.1065 +      Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
  3.1066 +        (List.drop (perm_names_types, length new_type_names))) |>
  3.1067 +      PrimrecPackage.add_primrec_i "" perm_eqs;
  3.1068 +
  3.1069 +    (**** prove that permutation functions introduced by unfolding are ****)
  3.1070 +    (**** equivalent to already existing permutation functions         ****)
  3.1071 +
  3.1072 +    val _ = warning ("length descr: " ^ string_of_int (length descr));
  3.1073 +    val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
  3.1074 +
  3.1075 +    val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
  3.1076 +    val perm_fun_def = PureThy.get_thm thy2 (Name "perm_fun_def");
  3.1077 +
  3.1078 +    val unfolded_perm_eq_thms =
  3.1079 +      if length descr = length new_type_names then []
  3.1080 +      else map standard (List.drop (split_conj_thm
  3.1081 +        (prove_goalw_cterm [] (cterm_of thy2 
  3.1082 +          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  3.1083 +            (map (fn (c as (s, T), x) =>
  3.1084 +               let val [T1, T2] = binder_types T
  3.1085 +               in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
  3.1086 +                 Const ("nominal.perm", T) $ pi $ Free (x, T2))
  3.1087 +               end)
  3.1088 +             (perm_names_types ~~ perm_indnames)))))
  3.1089 +          (fn _ => [indtac induction perm_indnames 1,
  3.1090 +            ALLGOALS (asm_full_simp_tac
  3.1091 +              (simpset_of thy2 addsimps [perm_fun_def]))])),
  3.1092 +        length new_type_names));
  3.1093 +
  3.1094 +    (**** prove [] \<bullet> t = t ****)
  3.1095 +
  3.1096 +    val _ = warning "perm_empty_thms";
  3.1097 +
  3.1098 +    val perm_empty_thms = List.concat (map (fn a =>
  3.1099 +      let val permT = mk_permT (Type (a, []))
  3.1100 +      in map standard (List.take (split_conj_thm
  3.1101 +        (prove_goalw_cterm [] (cterm_of thy2
  3.1102 +          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  3.1103 +            (map (fn ((s, T), x) => HOLogic.mk_eq
  3.1104 +                (Const (s, permT --> T --> T) $
  3.1105 +                   Const ("List.list.Nil", permT) $ Free (x, T),
  3.1106 +                 Free (x, T)))
  3.1107 +             (perm_names ~~
  3.1108 +              map body_type perm_types ~~ perm_indnames)))))
  3.1109 +          (fn _ => [indtac induction perm_indnames 1,
  3.1110 +            ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
  3.1111 +        length new_type_names))
  3.1112 +      end)
  3.1113 +      atoms);
  3.1114 +
  3.1115 +    (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
  3.1116 +
  3.1117 +    val _ = warning "perm_append_thms";
  3.1118 +
  3.1119 +    (*FIXME: these should be looked up statically*)
  3.1120 +    val at_pt_inst = PureThy.get_thm thy2 (Name "at_pt_inst");
  3.1121 +    val pt2 = PureThy.get_thm thy2 (Name "pt2");
  3.1122 +
  3.1123 +    val perm_append_thms = List.concat (map (fn a =>
  3.1124 +      let
  3.1125 +        val permT = mk_permT (Type (a, []));
  3.1126 +        val pi1 = Free ("pi1", permT);
  3.1127 +        val pi2 = Free ("pi2", permT);
  3.1128 +        val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
  3.1129 +        val pt2' = pt_inst RS pt2;
  3.1130 +        val pt2_ax = PureThy.get_thm thy2
  3.1131 +          (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a));
  3.1132 +      in List.take (map standard (split_conj_thm
  3.1133 +        (prove_goalw_cterm [] (cterm_of thy2
  3.1134 +             (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  3.1135 +                (map (fn ((s, T), x) =>
  3.1136 +                    let val perm = Const (s, permT --> T --> T)
  3.1137 +                    in HOLogic.mk_eq
  3.1138 +                      (perm $ (Const ("List.op @", permT --> permT --> permT) $
  3.1139 +                         pi1 $ pi2) $ Free (x, T),
  3.1140 +                       perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
  3.1141 +                    end)
  3.1142 +                  (perm_names ~~
  3.1143 +                   map body_type perm_types ~~ perm_indnames)))))
  3.1144 +           (fn _ => [indtac induction perm_indnames 1,
  3.1145 +              ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
  3.1146 +         length new_type_names)
  3.1147 +      end) atoms);
  3.1148 +
  3.1149 +    (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
  3.1150 +
  3.1151 +    val _ = warning "perm_eq_thms";
  3.1152 +
  3.1153 +    val pt3 = PureThy.get_thm thy2 (Name "pt3");
  3.1154 +    val pt3_rev = PureThy.get_thm thy2 (Name "pt3_rev");
  3.1155 +
  3.1156 +    val perm_eq_thms = List.concat (map (fn a =>
  3.1157 +      let
  3.1158 +        val permT = mk_permT (Type (a, []));
  3.1159 +        val pi1 = Free ("pi1", permT);
  3.1160 +        val pi2 = Free ("pi2", permT);
  3.1161 +        (*FIXME: not robust - better access these theorems using NominalData?*)
  3.1162 +        val at_inst = PureThy.get_thm thy2 (Name ("at_" ^ Sign.base_name a ^ "_inst"));
  3.1163 +        val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
  3.1164 +        val pt3' = pt_inst RS pt3;
  3.1165 +        val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
  3.1166 +        val pt3_ax = PureThy.get_thm thy2
  3.1167 +          (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
  3.1168 +      in List.take (map standard (split_conj_thm
  3.1169 +        (prove_goalw_cterm [] (cterm_of thy2 (Logic.mk_implies
  3.1170 +             (HOLogic.mk_Trueprop (Const ("nominal.prm_eq",
  3.1171 +                permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
  3.1172 +              HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  3.1173 +                (map (fn ((s, T), x) =>
  3.1174 +                    let val perm = Const (s, permT --> T --> T)
  3.1175 +                    in HOLogic.mk_eq
  3.1176 +                      (perm $ pi1 $ Free (x, T),
  3.1177 +                       perm $ pi2 $ Free (x, T))
  3.1178 +                    end)
  3.1179 +                  (perm_names ~~
  3.1180 +                   map body_type perm_types ~~ perm_indnames))))))
  3.1181 +           (fn hyps => [cut_facts_tac hyps 1, indtac induction perm_indnames 1,
  3.1182 +              ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
  3.1183 +         length new_type_names)
  3.1184 +      end) atoms);
  3.1185 +
  3.1186 +    (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
  3.1187 +
  3.1188 +    val cp1 = PureThy.get_thm thy2 (Name "cp1");
  3.1189 +    val dj_cp = PureThy.get_thm thy2 (Name "dj_cp");
  3.1190 +    val pt_perm_compose = PureThy.get_thm thy2 (Name "pt_perm_compose");
  3.1191 +    val pt_perm_compose_rev = PureThy.get_thm thy2 (Name "pt_perm_compose_rev");
  3.1192 +    val dj_perm_perm_forget = PureThy.get_thm thy2 (Name "dj_perm_perm_forget");
  3.1193 +
  3.1194 +    fun composition_instance name1 name2 thy =
  3.1195 +      let
  3.1196 +        val name1' = Sign.base_name name1;
  3.1197 +        val name2' = Sign.base_name name2;
  3.1198 +        val cp_class = Sign.intern_class thy ("cp_" ^ name1' ^ "_" ^ name2');
  3.1199 +        val permT1 = mk_permT (Type (name1, []));
  3.1200 +        val permT2 = mk_permT (Type (name2, []));
  3.1201 +        val augment = map_type_tfree
  3.1202 +          (fn (x, S) => TFree (x, cp_class :: S));
  3.1203 +        val Ts = map (augment o body_type) perm_types;
  3.1204 +        val cp_inst = PureThy.get_thm thy
  3.1205 +          (Name ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"));
  3.1206 +        val simps = simpset_of thy addsimps (perm_fun_def ::
  3.1207 +          (if name1 <> name2 then
  3.1208 +             let val dj = PureThy.get_thm thy (Name ("dj_" ^ name2' ^ "_" ^ name1'))
  3.1209 +             in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
  3.1210 +           else
  3.1211 +             let
  3.1212 +               val at_inst = PureThy.get_thm thy (Name ("at_" ^ name1' ^ "_inst"));
  3.1213 +               val pt_inst = PureThy.get_thm thy (Name ("pt_" ^ name1' ^ "_inst"))
  3.1214 +             in
  3.1215 +               [cp_inst RS cp1 RS sym,
  3.1216 +                at_inst RS (pt_inst RS pt_perm_compose) RS sym,
  3.1217 +                at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
  3.1218 +            end))
  3.1219 +        val thms = split_conj_thm (prove_goalw_cterm [] (cterm_of thy
  3.1220 +            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  3.1221 +              (map (fn ((s, T), x) =>
  3.1222 +                  let
  3.1223 +                    val pi1 = Free ("pi1", permT1);
  3.1224 +                    val pi2 = Free ("pi2", permT2);
  3.1225 +                    val perm1 = Const (s, permT1 --> T --> T);
  3.1226 +                    val perm2 = Const (s, permT2 --> T --> T);
  3.1227 +                    val perm3 = Const ("nominal.perm", permT1 --> permT2 --> permT2)
  3.1228 +                  in HOLogic.mk_eq
  3.1229 +                    (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
  3.1230 +                     perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
  3.1231 +                  end)
  3.1232 +                (perm_names ~~ Ts ~~ perm_indnames)))))
  3.1233 +          (fn _ => [indtac induction perm_indnames 1,
  3.1234 +             ALLGOALS (asm_full_simp_tac simps)]))
  3.1235 +      in
  3.1236 +        foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
  3.1237 +            (s, replicate (length tvs) (cp_class :: classes), [cp_class])
  3.1238 +            (AxClass.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
  3.1239 +          thy (full_new_type_names' ~~ tyvars)
  3.1240 +      end;
  3.1241 +
  3.1242 +    val (thy3, perm_thmss) = thy2 |>
  3.1243 +      fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
  3.1244 +      curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
  3.1245 +        AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
  3.1246 +        (AxClass.intro_classes_tac [] THEN REPEAT (EVERY
  3.1247 +           [resolve_tac perm_empty_thms 1,
  3.1248 +            resolve_tac perm_append_thms 1,
  3.1249 +            resolve_tac perm_eq_thms 1, assume_tac 1])) thy))
  3.1250 +        (List.take (descr, length new_type_names)) |>
  3.1251 +      PureThy.add_thmss
  3.1252 +        [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
  3.1253 +          unfolded_perm_eq_thms), [Simplifier.simp_add_global]),
  3.1254 +         ((space_implode "_" new_type_names ^ "_perm_empty",
  3.1255 +          perm_empty_thms), [Simplifier.simp_add_global]),
  3.1256 +         ((space_implode "_" new_type_names ^ "_perm_append",
  3.1257 +          perm_append_thms), [Simplifier.simp_add_global]),
  3.1258 +         ((space_implode "_" new_type_names ^ "_perm_eq",
  3.1259 +          perm_eq_thms), [Simplifier.simp_add_global])];
  3.1260 +  
  3.1261 +    (**** Define representing sets ****)
  3.1262 +
  3.1263 +    val _ = warning "representing sets";
  3.1264 +
  3.1265 +    val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names
  3.1266 +      (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
  3.1267 +    val big_rep_name =
  3.1268 +      space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
  3.1269 +        (fn (i, ("nominal.nOption", _, _)) => NONE
  3.1270 +          | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
  3.1271 +    val _ = warning ("big_rep_name: " ^ big_rep_name);
  3.1272 +
  3.1273 +    fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
  3.1274 +          (case AList.lookup op = descr i of
  3.1275 +             SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
  3.1276 +               apfst (cons dt) (strip_option dt')
  3.1277 +           | _ => ([], dtf))
  3.1278 +      | strip_option dt = ([], dt);
  3.1279 +
  3.1280 +    fun make_intr s T (cname, cargs) =
  3.1281 +      let
  3.1282 +        fun mk_prem (dt, (j, j', prems, ts)) = 
  3.1283 +          let
  3.1284 +            val (dts, dt') = strip_option dt;
  3.1285 +            val (dts', dt'') = strip_dtyp dt';
  3.1286 +            val Ts = map typ_of_dtyp dts;
  3.1287 +            val Us = map typ_of_dtyp dts';
  3.1288 +            val T = typ_of_dtyp dt'';
  3.1289 +            val free = mk_Free "x" (Us ---> T) j;
  3.1290 +            val free' = app_bnds free (length Us);
  3.1291 +            fun mk_abs_fun (T, (i, t)) =
  3.1292 +              let val U = fastype_of t
  3.1293 +              in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
  3.1294 +                Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
  3.1295 +              end
  3.1296 +          in (j + 1, j' + length Ts,
  3.1297 +            case dt'' of
  3.1298 +                DtRec k => list_all (map (pair "x") Us,
  3.1299 +                  HOLogic.mk_Trueprop (HOLogic.mk_mem (free',
  3.1300 +                    Const (List.nth (rep_set_names, k),
  3.1301 +                      HOLogic.mk_setT T)))) :: prems
  3.1302 +              | _ => prems,
  3.1303 +            snd (foldr mk_abs_fun (j', free) Ts) :: ts)
  3.1304 +          end;
  3.1305 +
  3.1306 +        val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs;
  3.1307 +        val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
  3.1308 +          (list_comb (Const (cname, map fastype_of ts ---> T), ts),
  3.1309 +           Const (s, HOLogic.mk_setT T)))
  3.1310 +      in Logic.list_implies (prems, concl)
  3.1311 +      end;
  3.1312 +
  3.1313 +    val (intr_ts, ind_consts) =
  3.1314 +      apfst List.concat (ListPair.unzip (List.mapPartial
  3.1315 +        (fn ((_, ("nominal.nOption", _, _)), _) => NONE
  3.1316 +          | ((i, (_, _, constrs)), rep_set_name) =>
  3.1317 +              let val T = nth_dtyp i
  3.1318 +              in SOME (map (make_intr rep_set_name T) constrs,
  3.1319 +                Const (rep_set_name, HOLogic.mk_setT T))
  3.1320 +              end)
  3.1321 +                (descr ~~ rep_set_names)));
  3.1322 +
  3.1323 +    val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
  3.1324 +      setmp InductivePackage.quiet_mode false
  3.1325 +        (InductivePackage.add_inductive_i false true big_rep_name false true false
  3.1326 +           ind_consts (map (fn x => (("", x), [])) intr_ts) []) thy3;
  3.1327 +
  3.1328 +    (**** Prove that representing set is closed under permutation ****)
  3.1329 +
  3.1330 +    val _ = warning "proving closure under permutation...";
  3.1331 +
  3.1332 +    val perm_indnames' = List.mapPartial
  3.1333 +      (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
  3.1334 +      (perm_indnames ~~ descr);
  3.1335 +
  3.1336 +    fun mk_perm_closed name = map (fn th => standard (th RS mp))
  3.1337 +      (List.take (split_conj_thm (prove_goalw_cterm [] (cterm_of thy4 
  3.1338 +        (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
  3.1339 +           (fn (S, x) =>
  3.1340 +              let
  3.1341 +                val S = map_term_types (map_type_tfree
  3.1342 +                  (fn (s, cs) => TFree (s, cs union cp_classes))) S;
  3.1343 +                val T = HOLogic.dest_setT (fastype_of S);
  3.1344 +                val permT = mk_permT (Type (name, []))
  3.1345 +              in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
  3.1346 +                HOLogic.mk_mem (Const ("nominal.perm", permT --> T --> T) $
  3.1347 +                  Free ("pi", permT) $ Free (x, T), S))
  3.1348 +              end) (ind_consts ~~ perm_indnames')))))
  3.1349 +        (fn _ =>  (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
  3.1350 +           [indtac rep_induct [] 1,
  3.1351 +            ALLGOALS (simp_tac (simpset_of thy4 addsimps
  3.1352 +              (symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))),
  3.1353 +            ALLGOALS (resolve_tac rep_intrs 
  3.1354 +               THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])),
  3.1355 +        length new_type_names));
  3.1356 +
  3.1357 +    (* FIXME: theorems are stored in database for testing only *)
  3.1358 +    val perm_closed_thmss = map mk_perm_closed atoms;
  3.1359 +    val (thy5, _) = PureThy.add_thmss [(("perm_closed",
  3.1360 +      List.concat perm_closed_thmss), [])] thy4;
  3.1361 +
  3.1362 +    (**** typedef ****)
  3.1363 +
  3.1364 +    val _ = warning "defining type...";
  3.1365 +
  3.1366 +    val (thy6, typedefs) =
  3.1367 +      foldl_map (fn (thy, ((((name, mx), tvs), c), name')) =>
  3.1368 +        setmp TypedefPackage.quiet_mode true
  3.1369 +          (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
  3.1370 +            (rtac exI 1 THEN
  3.1371 +              QUIET_BREADTH_FIRST (has_fewer_prems 1)
  3.1372 +              (resolve_tac rep_intrs 1))) thy |> (fn (thy, r) =>
  3.1373 +        let
  3.1374 +          val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
  3.1375 +          val pi = Free ("pi", permT);
  3.1376 +          val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
  3.1377 +          val T = Type (Sign.intern_type thy name, tvs');
  3.1378 +          val Const (_, Type (_, [U])) = c
  3.1379 +        in apsnd (pair r o hd)
  3.1380 +          (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
  3.1381 +            (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
  3.1382 +             Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
  3.1383 +               (Const ("nominal.perm", permT --> U --> U) $ pi $
  3.1384 +                 (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
  3.1385 +                   Free ("x", T))))), [])] thy)
  3.1386 +        end))
  3.1387 +          (thy5, types_syntax ~~ tyvars ~~
  3.1388 +            (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
  3.1389 +
  3.1390 +    val perm_defs = map snd typedefs;
  3.1391 +    val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
  3.1392 +    val Rep_thms = map (#Rep o fst) typedefs;
  3.1393 +
  3.1394 +    (** prove that new types are in class pt_<name> **)
  3.1395 +
  3.1396 +    val _ = warning "prove that new types are in class pt_<name> ...";
  3.1397 +
  3.1398 +    fun pt_instance ((class, atom), perm_closed_thms) =
  3.1399 +      fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
  3.1400 +        perm_def), name), tvs), perm_closed) => fn thy =>
  3.1401 +          AxClass.add_inst_arity_i
  3.1402 +            (Sign.intern_type thy name,
  3.1403 +              replicate (length tvs) (classes @ cp_classes), [class])
  3.1404 +            (EVERY [AxClass.intro_classes_tac [],
  3.1405 +              rewrite_goals_tac [perm_def],
  3.1406 +              asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
  3.1407 +              asm_full_simp_tac (simpset_of thy addsimps
  3.1408 +                [Rep RS perm_closed RS Abs_inverse]) 1,
  3.1409 +              asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
  3.1410 +                (Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy)
  3.1411 +        (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms);
  3.1412 +
  3.1413 +
  3.1414 +    (** prove that new types are in class cp_<name1>_<name2> **)
  3.1415 +
  3.1416 +    val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
  3.1417 +
  3.1418 +    fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
  3.1419 +      let
  3.1420 +        val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
  3.1421 +        val class = Sign.intern_class thy name;
  3.1422 +        val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
  3.1423 +      in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
  3.1424 +        perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
  3.1425 +          AxClass.add_inst_arity_i
  3.1426 +            (Sign.intern_type thy name,
  3.1427 +              replicate (length tvs) (classes @ cp_classes), [class])
  3.1428 +            (EVERY [AxClass.intro_classes_tac [],
  3.1429 +              rewrite_goals_tac [perm_def],
  3.1430 +              asm_full_simp_tac (simpset_of thy addsimps
  3.1431 +                ((Rep RS perm_closed1 RS Abs_inverse) ::
  3.1432 +                 (if atom1 = atom2 then []
  3.1433 +                  else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
  3.1434 +              DatatypeAux.cong_tac 1,
  3.1435 +              rtac refl 1,
  3.1436 +              rtac cp1' 1]) thy)
  3.1437 +        (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~
  3.1438 +          perm_closed_thms2) thy
  3.1439 +      end;
  3.1440 +
  3.1441 +    val thy7 = fold (fn x => fn thy => thy |>
  3.1442 +      pt_instance x |>
  3.1443 +      fold (cp_instance (apfst snd x)) (atoms ~~ perm_closed_thmss))
  3.1444 +        (classes ~~ atoms ~~ perm_closed_thmss) thy6;
  3.1445 +
  3.1446 +    (**** constructors ****)
  3.1447 +
  3.1448 +    fun mk_abs_fun (x, t) =
  3.1449 +      let
  3.1450 +        val T = fastype_of x;
  3.1451 +        val U = fastype_of t
  3.1452 +      in
  3.1453 +        Const ("nominal.abs_fun", T --> U --> T -->
  3.1454 +          Type ("nominal.nOption", [U])) $ x $ t
  3.1455 +      end;
  3.1456 +
  3.1457 +    val typ_of_dtyp' = replace_types' o typ_of_dtyp;
  3.1458 +
  3.1459 +    val rep_names = map (fn s =>
  3.1460 +      Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
  3.1461 +    val abs_names = map (fn s =>
  3.1462 +      Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
  3.1463 +
  3.1464 +    val recTs = get_rec_types descr sorts;
  3.1465 +    val newTs' = Library.take (length new_type_names, recTs);
  3.1466 +    val newTs = map replace_types' newTs';
  3.1467 +
  3.1468 +    val full_new_type_names = map (Sign.full_name (sign_of thy)) new_type_names;
  3.1469 +
  3.1470 +    fun make_constr_def tname T T' ((thy, defs, eqns), ((cname, cargs), (cname', mx))) =
  3.1471 +      let
  3.1472 +        fun constr_arg (dt, (j, l_args, r_args)) =
  3.1473 +          let
  3.1474 +            val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  3.1475 +            val (dts, dt') = strip_option dt;
  3.1476 +            val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp' dt) i)
  3.1477 +              (dts ~~ (j upto j + length dts - 1))
  3.1478 +            val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts)
  3.1479 +            val (dts', dt'') = strip_dtyp dt'
  3.1480 +          in case dt'' of
  3.1481 +              DtRec k => if k < length new_type_names then
  3.1482 +                  (j + length dts + 1,
  3.1483 +                   xs @ x :: l_args,
  3.1484 +                   foldr mk_abs_fun
  3.1485 +                     (list_abs (map (pair "z" o typ_of_dtyp') dts',
  3.1486 +                       Const (List.nth (rep_names, k), typ_of_dtyp' dt'' -->
  3.1487 +                         typ_of_dtyp dt'') $ app_bnds x (length dts')))
  3.1488 +                     xs :: r_args)
  3.1489 +                else error "nested recursion not (yet) supported"
  3.1490 +            | _ => (j + 1, x' :: l_args, x' :: r_args)
  3.1491 +          end
  3.1492 +
  3.1493 +        val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
  3.1494 +        val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
  3.1495 +        val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
  3.1496 +        val constrT = map fastype_of l_args ---> T;
  3.1497 +        val lhs = list_comb (Const (Sign.full_name thy (Sign.base_name cname),
  3.1498 +          constrT), l_args);
  3.1499 +        val rhs = list_comb (Const (cname, map fastype_of r_args ---> T'), r_args);
  3.1500 +        val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
  3.1501 +        val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
  3.1502 +          (Const (rep_name, T --> T') $ lhs, rhs));
  3.1503 +        val def_name = (Sign.base_name cname) ^ "_def";
  3.1504 +        val (thy', [def_thm]) = thy |>
  3.1505 +          Theory.add_consts_i [(cname', constrT, mx)] |>
  3.1506 +          (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
  3.1507 +      in (thy', defs @ [def_thm], eqns @ [eqn]) end;
  3.1508 +
  3.1509 +    fun dt_constr_defs ((thy, defs, eqns, dist_lemmas),
  3.1510 +        (((((_, (_, _, constrs)), tname), T), T'), constr_syntax)) =
  3.1511 +      let
  3.1512 +        val rep_const = cterm_of thy
  3.1513 +          (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
  3.1514 +        val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
  3.1515 +        val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
  3.1516 +          ((Theory.add_path tname thy, defs, []), constrs ~~ constr_syntax)
  3.1517 +      in
  3.1518 +        (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
  3.1519 +      end;
  3.1520 +
  3.1521 +    val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
  3.1522 +      ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
  3.1523 +        new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
  3.1524 +
  3.1525 +    val abs_inject_thms = map (fn tname =>
  3.1526 +      PureThy.get_thm thy8 (Name ("Abs_" ^ tname ^ "_inject"))) new_type_names;
  3.1527 +
  3.1528 +    val rep_inject_thms = map (fn tname =>
  3.1529 +      PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inject"))) new_type_names;
  3.1530 +
  3.1531 +    val rep_thms = map (fn tname =>
  3.1532 +      PureThy.get_thm thy8 (Name ("Rep_" ^ tname))) new_type_names;
  3.1533 +
  3.1534 +    val rep_inverse_thms = map (fn tname =>
  3.1535 +      PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inverse"))) new_type_names;
  3.1536 +
  3.1537 +    (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
  3.1538 +    
  3.1539 +    fun prove_constr_rep_thm eqn =
  3.1540 +      let
  3.1541 +        val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
  3.1542 +        val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms
  3.1543 +      in prove_goalw_cterm [] (cterm_of thy8 eqn) (fn _ =>
  3.1544 +        [resolve_tac inj_thms 1,
  3.1545 +         rewrite_goals_tac rewrites,
  3.1546 +         rtac refl 3,
  3.1547 +         resolve_tac rep_intrs 2,
  3.1548 +         REPEAT (resolve_tac rep_thms 1)])
  3.1549 +      end;
  3.1550 +
  3.1551 +    val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
  3.1552 +
  3.1553 +    (* prove theorem  pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
  3.1554 +
  3.1555 +    fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
  3.1556 +      let
  3.1557 +        val _ $ (_ $ (Rep $ x) $ _) = Logic.unvarify (prop_of th);
  3.1558 +        val Type ("fun", [T, U]) = fastype_of Rep;
  3.1559 +        val permT = mk_permT (Type (atom, []));
  3.1560 +        val pi = Free ("pi", permT);
  3.1561 +      in
  3.1562 +        prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
  3.1563 +            (Const ("nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
  3.1564 +             Rep $ (Const ("nominal.perm", permT --> T --> T) $ pi $ x)))))
  3.1565 +          (fn _ => [simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
  3.1566 +            perm_closed_thms @ Rep_thms)) 1])
  3.1567 +      end) Rep_thms;
  3.1568 +
  3.1569 +    val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
  3.1570 +      (atoms ~~ perm_closed_thmss));
  3.1571 +
  3.1572 +    (* prove distinctness theorems *)
  3.1573 +
  3.1574 +    fun make_distincts_1 _ [] = []
  3.1575 +      | make_distincts_1 tname ((cname, cargs)::constrs) =
  3.1576 +          let
  3.1577 +            val cname = Sign.intern_const thy8
  3.1578 +              (NameSpace.append tname (Sign.base_name cname));
  3.1579 +            val (Ts, T) = strip_type (the (Sign.const_type thy8 cname));
  3.1580 +            val frees = map Free ((DatatypeProp.make_tnames Ts) ~~ Ts);
  3.1581 +            val t = list_comb (Const (cname, Ts ---> T), frees);
  3.1582 +
  3.1583 +            fun make_distincts' [] = []
  3.1584 +              | make_distincts' ((cname', cargs')::constrs') =
  3.1585 +                  let
  3.1586 +                    val cname' = Sign.intern_const thy8
  3.1587 +                      (NameSpace.append tname (Sign.base_name cname'));
  3.1588 +                    val Ts' = binder_types (the (Sign.const_type thy8 cname'));
  3.1589 +                    val frees' = map Free ((map ((op ^) o (rpair "'"))
  3.1590 +                      (DatatypeProp.make_tnames Ts')) ~~ Ts');
  3.1591 +                    val t' = list_comb (Const (cname', Ts' ---> T), frees')
  3.1592 +                  in
  3.1593 +                    (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')))::
  3.1594 +                      (make_distincts' constrs')
  3.1595 +                  end
  3.1596 +
  3.1597 +          in (make_distincts' constrs) @ (make_distincts_1 tname constrs)
  3.1598 +          end;
  3.1599 +
  3.1600 +    val distinct_props = map (fn ((_, (_, _, constrs)), tname) =>
  3.1601 +        make_distincts_1 tname constrs)
  3.1602 +      (List.take (descr, length new_type_names) ~~ new_type_names);
  3.1603 +
  3.1604 +    val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
  3.1605 +      dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
  3.1606 +        (constr_rep_thmss ~~ dist_lemmas);
  3.1607 +
  3.1608 +    fun prove_distinct_thms (_, []) = []
  3.1609 +      | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
  3.1610 +          let
  3.1611 +            val dist_thm = prove_goalw_cterm [] (cterm_of thy8 t) (fn _ =>
  3.1612 +              [simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1])
  3.1613 +          in dist_thm::(standard (dist_thm RS not_sym))::
  3.1614 +            (prove_distinct_thms (p, ts))
  3.1615 +          end;
  3.1616 +
  3.1617 +    val distinct_thms = map prove_distinct_thms
  3.1618 +      (constr_rep_thmss ~~ dist_lemmas ~~ distinct_props);
  3.1619 +
  3.1620 +    (** prove equations for permutation functions **)
  3.1621 +
  3.1622 +    val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *)
  3.1623 +
  3.1624 +    val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
  3.1625 +      let val T = replace_types' (nth_dtyp i)
  3.1626 +      in List.concat (map (fn (atom, perm_closed_thms) =>
  3.1627 +          map (fn ((cname, dts), constr_rep_thm) => 
  3.1628 +        let
  3.1629 +          val cname = Sign.intern_const thy8
  3.1630 +            (NameSpace.append tname (Sign.base_name cname));
  3.1631 +          val permT = mk_permT (Type (atom, []));
  3.1632 +          val pi = Free ("pi", permT);
  3.1633 +
  3.1634 +          fun perm t =
  3.1635 +            let val T = fastype_of t
  3.1636 +            in Const ("nominal.perm", permT --> T --> T) $ pi $ t end;
  3.1637 +
  3.1638 +          fun constr_arg (dt, (j, l_args, r_args)) =
  3.1639 +            let
  3.1640 +              val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  3.1641 +              val (dts, dt') = strip_option dt;
  3.1642 +              val Ts = map typ_of_dtyp' dts;
  3.1643 +              val xs = map (fn (T, i) => mk_Free "x" T i)
  3.1644 +                (Ts ~~ (j upto j + length dts - 1))
  3.1645 +              val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
  3.1646 +              val (dts', dt'') = strip_dtyp dt';
  3.1647 +            in case dt'' of
  3.1648 +                DtRec k => if k < length new_type_names then
  3.1649 +                    (j + length dts + 1,
  3.1650 +                     xs @ x :: l_args,
  3.1651 +                     map perm (xs @ [x]) @ r_args)
  3.1652 +                  else error "nested recursion not (yet) supported"
  3.1653 +              | _ => (j + 1, x' :: l_args, perm x' :: r_args)
  3.1654 +            end
  3.1655 +
  3.1656 +          val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts;
  3.1657 +          val c = Const (cname, map fastype_of l_args ---> T)
  3.1658 +        in
  3.1659 +          prove_goalw_cterm [] (cterm_of thy8
  3.1660 +            (HOLogic.mk_Trueprop (HOLogic.mk_eq
  3.1661 +              (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
  3.1662 +            (fn _ =>
  3.1663 +              [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
  3.1664 +               simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
  3.1665 +                 constr_defs @ perm_closed_thms)) 1,
  3.1666 +               TRY (simp_tac (HOL_basic_ss addsimps
  3.1667 +                 (symmetric perm_fun_def :: abs_perm)) 1),
  3.1668 +               TRY (simp_tac (HOL_basic_ss addsimps
  3.1669 +                 (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
  3.1670 +                    perm_closed_thms)) 1)])
  3.1671 +        end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
  3.1672 +      end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
  3.1673 +
  3.1674 +    (** prove injectivity of constructors **)
  3.1675 +
  3.1676 +    val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
  3.1677 +    val alpha = PureThy.get_thms thy8 (Name "alpha");
  3.1678 +    val abs_fresh = PureThy.get_thms thy8 (Name "abs_fresh");
  3.1679 +    val fresh_def = PureThy.get_thm thy8 (Name "fresh_def");
  3.1680 +    val supp_def = PureThy.get_thm thy8 (Name "supp_def");
  3.1681 +
  3.1682 +    val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
  3.1683 +      let val T = replace_types' (nth_dtyp i)
  3.1684 +      in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
  3.1685 +        if null dts then NONE else SOME
  3.1686 +        let
  3.1687 +          val cname = Sign.intern_const thy8
  3.1688 +            (NameSpace.append tname (Sign.base_name cname));
  3.1689 +
  3.1690 +          fun make_inj (dt, (j, args1, args2, eqs)) =
  3.1691 +            let
  3.1692 +              val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  3.1693 +              val y' = mk_Free "y" (typ_of_dtyp' dt) j;
  3.1694 +              val (dts, dt') = strip_option dt;
  3.1695 +              val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
  3.1696 +              val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
  3.1697 +              val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
  3.1698 +              val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
  3.1699 +              val y = mk_Free "y" (typ_of_dtyp' dt') (j + length dts);
  3.1700 +              val (dts', dt'') = strip_dtyp dt';
  3.1701 +            in case dt'' of
  3.1702 +                DtRec k => if k < length new_type_names then
  3.1703 +                    (j + length dts + 1,
  3.1704 +                     xs @ (x :: args1), ys @ (y :: args2),
  3.1705 +                     HOLogic.mk_eq
  3.1706 +                       (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs)
  3.1707 +                  else error "nested recursion not (yet) supported"
  3.1708 +              | _ => (j + 1, x' :: args1, y' :: args2, HOLogic.mk_eq (x', y') :: eqs)
  3.1709 +            end;
  3.1710 +
  3.1711 +          val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts;
  3.1712 +          val Ts = map fastype_of args1;
  3.1713 +          val c = Const (cname, Ts ---> T)
  3.1714 +        in
  3.1715 +          prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
  3.1716 +              (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
  3.1717 +               foldr1 HOLogic.mk_conj eqs))))
  3.1718 +            (fn _ =>
  3.1719 +               [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
  3.1720 +                  rep_inject_thms')) 1,
  3.1721 +                TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
  3.1722 +                  alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
  3.1723 +                  perm_rep_perm_thms)) 1)])
  3.1724 +        end) (constrs ~~ constr_rep_thms)
  3.1725 +      end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
  3.1726 +
  3.1727 +    val (thy9, _) = thy8 |>
  3.1728 +      DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
  3.1729 +      DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
  3.1730 +      DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
  3.1731 +      DatatypeAux.store_thmss "inject" new_type_names inject_thms;
  3.1732 +
  3.1733 +  in
  3.1734 +    (thy9, perm_eq_thms)
  3.1735 +  end;
  3.1736 +
  3.1737 +val add_nominal_datatype = gen_add_nominal_datatype read_typ true;
  3.1738 +
  3.1739 +
  3.1740 +(* FIXME: The following stuff should be exported by DatatypePackage *)
  3.1741 +
  3.1742 +local structure P = OuterParse and K = OuterKeyword in
  3.1743 +
  3.1744 +val datatype_decl =
  3.1745 +  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
  3.1746 +    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
  3.1747 +
  3.1748 +fun mk_datatype args =
  3.1749 +  let
  3.1750 +    val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
  3.1751 +    val specs = map (fn ((((_, vs), t), mx), cons) =>
  3.1752 +      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
  3.1753 +  in #1 o add_nominal_datatype false names specs end;
  3.1754 +
  3.1755 +val nominal_datatypeP =
  3.1756 +  OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
  3.1757 +    (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
  3.1758 +
  3.1759 +val _ = OuterSyntax.add_parsers [nominal_datatypeP];
  3.1760 +
  3.1761 +end;
  3.1762 +
  3.1763 +end
  3.1764 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Oct 17 12:30:57 2005 +0200
     4.3 @@ -0,0 +1,109 @@
     4.4 +(* $Id$ *)
     4.5 +
     4.6 +(* METHOD FOR ANALYSING EQUATION INVOLVING PERMUTATION *)
     4.7 +
     4.8 +local
     4.9 +
    4.10 +(* applies the expand_fun_eq rule to the first goal and strips off all universal quantifiers *)
    4.11 +val Expand_Fun_Eq_tac =    
    4.12 +    ("extensionality on functions",
    4.13 +    EVERY [simp_tac (HOL_basic_ss addsimps [expand_fun_eq]) 1, REPEAT_DETERM (rtac allI 1)]);
    4.14 +
    4.15 +(* applies the perm_compose rule - this rule would loop in the simplifier *)
    4.16 +fun Apply_Perm_Compose_tac ctxt = 
    4.17 +    let 
    4.18 +	val perm_compose = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("perm_compose"));
    4.19 +    in ("analysing permutation compositions",rtac (perm_compose RS trans)  1)
    4.20 +    end;
    4.21 +
    4.22 +(* unfolds the definition of permutations applied to functions *)
    4.23 +fun Unfold_Perm_Fun_Def_tac ctxt = 
    4.24 +    let 
    4.25 +	val perm_fun_def = PureThy.get_thm (ProofContext.theory_of ctxt) (Name ("nominal.perm_fun_def"))
    4.26 +    in ("unfolding of perms on functions", simp_tac (HOL_basic_ss addsimps [perm_fun_def]) 1)
    4.27 +    end
    4.28 +    
    4.29 +(* applies the perm_eq_lam and perm_eq_app simplifications *)
    4.30 +fun Apply_SimProc_tac ctxt = 
    4.31 +    let
    4.32 +        val thy = ProofContext.theory_of ctxt;
    4.33 +	val perm_app_eq = PureThy.get_thm thy (Name ("perm_app_eq"));
    4.34 +        val perm_lam_eq = PureThy.get_thm thy (Name ("perm_eq_lam"));
    4.35 +    in
    4.36 +	("simplification of permutation on applications and lambdas", 
    4.37 +	 asm_full_simp_tac (HOL_basic_ss addsimps [perm_app_eq,perm_lam_eq]) 1)
    4.38 +    end;
    4.39 +
    4.40 +(* applying Stefan's smart congruence tac *)
    4.41 +val Apply_Cong_tac = ("application of congruence",
    4.42 +                     (fn st => DatatypeAux.cong_tac  1 st handle Subscript => no_tac st));
    4.43 +
    4.44 +(* initial simplification step in the tactic *)
    4.45 +fun Initial_Simp_tac thms ctxt =
    4.46 +    let
    4.47 +	val thy = ProofContext.theory_of ctxt;
    4.48 +	val perm_swap  = PureThy.get_thm thy (Name ("perm_swap"));
    4.49 +        val perm_fresh = PureThy.get_thm thy (Name ("perm_fresh_fresh"));
    4.50 +        val perm_bij   = PureThy.get_thm thy (Name ("perm_bij"));
    4.51 +        val simps = (local_simpset_of ctxt) addsimps (thms @ [perm_swap,perm_fresh,perm_bij])
    4.52 +    in
    4.53 +      ("general simplification step", FIRST [rtac conjI 1, asm_full_simp_tac simps 1])
    4.54 +    end;
    4.55 +
    4.56 +
    4.57 +(* debugging *)
    4.58 +fun DEBUG_tac (msg,tac) = 
    4.59 +    EVERY [print_tac ("before application of "^msg), CHANGED tac, print_tac ("after "^msg)]; 
    4.60 +fun NO_DEBUG_tac (_,tac) = CHANGED tac; 
    4.61 +
    4.62 +(* Main Tactic *)
    4.63 +(* "repeating"-depth is set to 40 - this seems sufficient *)
    4.64 +fun perm_simp_tac tactical thms ctxt = 
    4.65 +    REPEAT_DETERM_N 40 
    4.66 +      (FIRST[tactical (Initial_Simp_tac thms ctxt),
    4.67 +             tactical (Apply_Perm_Compose_tac ctxt),
    4.68 +             tactical (Apply_SimProc_tac ctxt),
    4.69 +             tactical Apply_Cong_tac, 
    4.70 +             tactical (Unfold_Perm_Fun_Def_tac ctxt),
    4.71 +             tactical Expand_Fun_Eq_tac]);
    4.72 +
    4.73 +(* tactic that unfolds first the support definition *)
    4.74 +(* and then applies perm_simp                       *)
    4.75 +fun supports_tac tactical thms ctxt =
    4.76 +  let
    4.77 +    val thy = ProofContext.theory_of ctxt;
    4.78 +    val supports_def = PureThy.get_thm thy (Name ("nominal.op supports_def"));
    4.79 +    val fresh_def    = PureThy.get_thm thy (Name ("nominal.fresh_def"));
    4.80 +    val fresh_prod   = PureThy.get_thm thy (Name ("nominal.fresh_prod"));
    4.81 +    val simps        = [supports_def,symmetric fresh_def,fresh_prod];
    4.82 +
    4.83 +  in
    4.84 +      EVERY [tactical ("unfolding of supports",simp_tac (HOL_basic_ss addsimps simps) 1),
    4.85 +             tactical ("stripping of foralls " ,REPEAT_DETERM (rtac allI 1)),
    4.86 +             tactical ("geting rid of the imp",rtac impI 1),
    4.87 +             tactical ("eliminating conjuncts",REPEAT_DETERM (etac  conjE 1)),
    4.88 +             tactical ("applying perm_simp   ",perm_simp_tac tactical thms ctxt)]
    4.89 +  end;
    4.90 +
    4.91 +in             
    4.92 +
    4.93 +val perm_eq_meth = 
    4.94 +    Method.thms_ctxt_args 
    4.95 +	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac NO_DEBUG_tac thms ctxt)));
    4.96 +
    4.97 +val perm_eq_meth_debug = 
    4.98 +    Method.thms_ctxt_args 
    4.99 +	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (perm_simp_tac DEBUG_tac thms ctxt)));
   4.100 +
   4.101 +val supports_meth = 
   4.102 +    Method.thms_ctxt_args 
   4.103 +	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac NO_DEBUG_tac thms ctxt)));
   4.104 +
   4.105 +val supports_meth_debug = 
   4.106 +    Method.thms_ctxt_args 
   4.107 +	(fn thms => fn ctxt => Method.SIMPLE_METHOD (DETERM (supports_tac DEBUG_tac thms ctxt)));
   4.108 +
   4.109 +end
   4.110 +
   4.111 +
   4.112 +