1.1 --- a/src/HOL/Nominal/Nominal.thy Sun Apr 26 20:23:09 2009 +0200
1.2 +++ b/src/HOL/Nominal/Nominal.thy Sun Apr 26 23:16:24 2009 +0200
1.3 @@ -18,7 +18,7 @@
1.4 types
1.5 'x prm = "('x \<times> 'x) list"
1.6
1.7 -(* polymorphic operations for permutation and swapping *)
1.8 +(* polymorphic constants for permutation and swapping *)
1.9 consts
1.10 perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80)
1.11 swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
1.12 @@ -34,7 +34,7 @@
1.13 constdefs
1.14 "perm_aux pi x \<equiv> pi\<bullet>x"
1.15
1.16 -(* permutation operations *)
1.17 +(* overloaded permutation operations *)
1.18 overloading
1.19 perm_fun \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)" (unchecked)
1.20 perm_bool \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool" (unchecked)
1.21 @@ -203,11 +203,12 @@
1.22 supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80)
1.23 "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
1.24
1.25 +(* lemmas about supp *)
1.26 lemma supp_fresh_iff:
1.27 fixes x :: "'a"
1.28 shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
1.29 -apply(simp add: fresh_def)
1.30 -done
1.31 + by (simp add: fresh_def)
1.32 +
1.33
1.34 lemma supp_unit:
1.35 shows "supp () = {}"
1.36 @@ -238,14 +239,13 @@
1.37 fixes x :: "'a"
1.38 and xs :: "'a list"
1.39 shows "supp (x#xs) = (supp x)\<union>(supp xs)"
1.40 -apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
1.41 -done
1.42 + by (auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
1.43
1.44 lemma supp_list_append:
1.45 fixes xs :: "'a list"
1.46 and ys :: "'a list"
1.47 shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
1.48 - by (induct xs, auto simp add: supp_list_nil supp_list_cons)
1.49 + by (induct xs) (auto simp add: supp_list_nil supp_list_cons)
1.50
1.51 lemma supp_list_rev:
1.52 fixes xs :: "'a list"
1.53 @@ -287,6 +287,7 @@
1.54 shows "(supp s) = {}"
1.55 by (simp add: supp_def perm_string)
1.56
1.57 +(* lemmas about freshness *)
1.58 lemma fresh_set_empty:
1.59 shows "a\<sharp>{}"
1.60 by (simp add: fresh_def supp_set_empty)
1.61 @@ -395,63 +396,6 @@
1.62 Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
1.63 *}
1.64
1.65 -section {* generalisation of freshness to lists and sets of atoms *}
1.66 -(*================================================================*)
1.67 -
1.68 -consts
1.69 - fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
1.70 -
1.71 -defs (overloaded)
1.72 - fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
1.73 -
1.74 -defs (overloaded)
1.75 - fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
1.76 -
1.77 -lemmas fresh_star_def = fresh_star_list fresh_star_set
1.78 -
1.79 -lemma fresh_star_prod_set:
1.80 - fixes xs::"'a set"
1.81 - shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
1.82 -by (auto simp add: fresh_star_def fresh_prod)
1.83 -
1.84 -lemma fresh_star_prod_list:
1.85 - fixes xs::"'a list"
1.86 - shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
1.87 - by (auto simp add: fresh_star_def fresh_prod)
1.88 -
1.89 -lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
1.90 -
1.91 -lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c"
1.92 - by (simp add: fresh_star_def)
1.93 -
1.94 -lemma fresh_star_Un_elim:
1.95 - "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
1.96 - apply rule
1.97 - apply (simp_all add: fresh_star_def)
1.98 - apply (erule meta_mp)
1.99 - apply blast
1.100 - done
1.101 -
1.102 -lemma fresh_star_insert_elim:
1.103 - "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
1.104 - by rule (simp_all add: fresh_star_def)
1.105 -
1.106 -lemma fresh_star_empty_elim:
1.107 - "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
1.108 - by (simp add: fresh_star_def)
1.109 -
1.110 -text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
1.111 -
1.112 -lemma fresh_star_unit_elim:
1.113 - shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
1.114 - and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
1.115 - by (simp_all add: fresh_star_def fresh_def supp_unit)
1.116 -
1.117 -lemma fresh_star_prod_elim:
1.118 - shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
1.119 - and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
1.120 - by (rule, simp_all add: fresh_star_prod)+
1.121 -
1.122 section {* Abstract Properties for Permutations and Atoms *}
1.123 (*=========================================================*)
1.124
1.125 @@ -511,7 +455,7 @@
1.126 shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
1.127 using a by (simp only: at_def)
1.128
1.129 -(* rules to calculate simple premutations *)
1.130 +(* rules to calculate simple permutations *)
1.131 lemmas at_calc = at2 at1 at3
1.132
1.133 lemma at_swap_simps:
1.134 @@ -706,7 +650,6 @@
1.135 shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
1.136 by (simp add: at_prm_rev_eq[OF at])
1.137
1.138 -
1.139 lemma at_ds1:
1.140 fixes a :: "'x"
1.141 assumes at: "at TYPE('x)"
1.142 @@ -862,15 +805,18 @@
1.143 by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def)
1.144
1.145 lemma at_finite_select:
1.146 - shows "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S"
1.147 - apply (drule Diff_infinite_finite)
1.148 - apply (simp add: at_def)
1.149 - apply blast
1.150 - apply (subgoal_tac "UNIV - S \<noteq> {}")
1.151 - apply (simp only: ex_in_conv [symmetric])
1.152 - apply blast
1.153 - apply (rule notI)
1.154 - apply simp
1.155 + fixes S::"'a set"
1.156 + assumes a: "at TYPE('a)"
1.157 + and b: "finite S"
1.158 + shows "\<exists>x. x \<notin> S"
1.159 + using a b
1.160 + apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite)
1.161 + apply(simp add: at_def)
1.162 + apply(subgoal_tac "UNIV - S \<noteq> {}")
1.163 + apply(simp only: ex_in_conv [symmetric])
1.164 + apply(blast)
1.165 + apply(rule notI)
1.166 + apply(simp)
1.167 done
1.168
1.169 lemma at_different:
1.170 @@ -1246,8 +1192,8 @@
1.171 assumes pt: "pt TYPE('a) TYPE('x)"
1.172 and at: "at TYPE('x)"
1.173 shows "pi\<bullet>(x=y) = (pi\<bullet>x = pi\<bullet>y)"
1.174 -using assms
1.175 -by (auto simp add: pt_bij perm_bool)
1.176 + using pt at
1.177 + by (auto simp add: pt_bij perm_bool)
1.178
1.179 lemma pt_bij3:
1.180 fixes pi :: "'x prm"
1.181 @@ -1255,7 +1201,7 @@
1.182 and y :: "'a"
1.183 assumes a: "x=y"
1.184 shows "(pi\<bullet>x = pi\<bullet>y)"
1.185 -using a by simp
1.186 + using a by simp
1.187
1.188 lemma pt_bij4:
1.189 fixes pi :: "'x prm"
1.190 @@ -1265,7 +1211,7 @@
1.191 and at: "at TYPE('x)"
1.192 and a: "pi\<bullet>x = pi\<bullet>y"
1.193 shows "x = y"
1.194 -using a by (simp add: pt_bij[OF pt, OF at])
1.195 + using a by (simp add: pt_bij[OF pt, OF at])
1.196
1.197 lemma pt_swap_bij:
1.198 fixes a :: "'x"
1.199 @@ -1598,35 +1544,6 @@
1.200 apply(simp add: pt_rev_pi[OF ptb, OF at])
1.201 done
1.202
1.203 -lemma pt_fresh_star_bij_ineq:
1.204 - fixes pi :: "'x prm"
1.205 - and x :: "'a"
1.206 - and a :: "'y set"
1.207 - and b :: "'y list"
1.208 - assumes pta: "pt TYPE('a) TYPE('x)"
1.209 - and ptb: "pt TYPE('y) TYPE('x)"
1.210 - and at: "at TYPE('x)"
1.211 - and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
1.212 - shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
1.213 - and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
1.214 -apply(unfold fresh_star_def)
1.215 -apply(auto)
1.216 -apply(drule_tac x="pi\<bullet>xa" in bspec)
1.217 -apply(rule pt_set_bij2[OF ptb, OF at])
1.218 -apply(assumption)
1.219 -apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
1.220 -apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
1.221 -apply(simp add: pt_set_bij1[OF ptb, OF at])
1.222 -apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
1.223 -apply(drule_tac x="pi\<bullet>xa" in bspec)
1.224 -apply(simp add: pt_set_bij1[OF ptb, OF at])
1.225 -apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
1.226 -apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
1.227 -apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
1.228 -apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
1.229 -apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
1.230 -done
1.231 -
1.232 lemma pt_fresh_left:
1.233 fixes pi :: "'x prm"
1.234 and x :: "'a"
1.235 @@ -1675,56 +1592,6 @@
1.236 apply(rule at)
1.237 done
1.238
1.239 -lemma pt_fresh_star_bij:
1.240 - fixes pi :: "'x prm"
1.241 - and x :: "'a"
1.242 - and a :: "'x set"
1.243 - and b :: "'x list"
1.244 - assumes pt: "pt TYPE('a) TYPE('x)"
1.245 - and at: "at TYPE('x)"
1.246 - shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
1.247 - and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
1.248 -apply(rule pt_fresh_star_bij_ineq(1))
1.249 -apply(rule pt)
1.250 -apply(rule at_pt_inst)
1.251 -apply(rule at)+
1.252 -apply(rule cp_pt_inst)
1.253 -apply(rule pt)
1.254 -apply(rule at)
1.255 -apply(rule pt_fresh_star_bij_ineq(2))
1.256 -apply(rule pt)
1.257 -apply(rule at_pt_inst)
1.258 -apply(rule at)+
1.259 -apply(rule cp_pt_inst)
1.260 -apply(rule pt)
1.261 -apply(rule at)
1.262 -done
1.263 -
1.264 -lemma pt_fresh_star_eqvt:
1.265 - fixes pi :: "'x prm"
1.266 - and x :: "'a"
1.267 - and a :: "'x set"
1.268 - and b :: "'x list"
1.269 - assumes pt: "pt TYPE('a) TYPE('x)"
1.270 - and at: "at TYPE('x)"
1.271 - shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
1.272 - and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
1.273 - by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])
1.274 -
1.275 -lemma pt_fresh_star_eqvt_ineq:
1.276 - fixes pi::"'x prm"
1.277 - and a::"'y set"
1.278 - and b::"'y list"
1.279 - and x::"'a"
1.280 - assumes pta: "pt TYPE('a) TYPE('x)"
1.281 - and ptb: "pt TYPE('y) TYPE('x)"
1.282 - and at: "at TYPE('x)"
1.283 - and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
1.284 - and dj: "disjoint TYPE('y) TYPE('x)"
1.285 - shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
1.286 - and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
1.287 - by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
1.288 -
1.289 lemma pt_fresh_bij1:
1.290 fixes pi :: "'x prm"
1.291 and x :: "'a"
1.292 @@ -1777,7 +1644,6 @@
1.293
1.294 (* the next two lemmas are needed in the proof *)
1.295 (* of the structural induction principle *)
1.296 -
1.297 lemma pt_fresh_aux:
1.298 fixes a::"'x"
1.299 and b::"'x"
1.300 @@ -1881,27 +1747,6 @@
1.301 thus ?thesis using eq3 by simp
1.302 qed
1.303
1.304 -lemma pt_freshs_freshs:
1.305 - assumes pt: "pt TYPE('a) TYPE('x)"
1.306 - and at: "at TYPE ('x)"
1.307 - and pi: "set (pi::'x prm) \<subseteq> Xs \<times> Ys"
1.308 - and Xs: "Xs \<sharp>* (x::'a)"
1.309 - and Ys: "Ys \<sharp>* x"
1.310 - shows "pi \<bullet> x = x"
1.311 - using pi
1.312 -proof (induct pi)
1.313 - case Nil
1.314 - show ?case by (simp add: pt1 [OF pt])
1.315 -next
1.316 - case (Cons p pi)
1.317 - obtain a b where p: "p = (a, b)" by (cases p)
1.318 - with Cons Xs Ys have "a \<sharp> x" "b \<sharp> x"
1.319 - by (simp_all add: fresh_star_def)
1.320 - with Cons p show ?case
1.321 - by (simp add: pt_fresh_fresh [OF pt at]
1.322 - pt2 [OF pt, of "[(a, b)]" pi, simplified])
1.323 -qed
1.324 -
1.325 lemma pt_pi_fresh_fresh:
1.326 fixes x :: "'a"
1.327 and pi :: "'x prm"
1.328 @@ -1967,8 +1812,7 @@
1.329 thus ?thesis by (simp add: pt2[OF pt])
1.330 qed
1.331
1.332 -section {* equivaraince for some connectives *}
1.333 -
1.334 +section {* equivariance for some connectives *}
1.335 lemma pt_all_eqvt:
1.336 fixes pi :: "'x prm"
1.337 and x :: "'a"
1.338 @@ -2014,8 +1858,6 @@
1.339 apply(rule theI'[OF unique])
1.340 done
1.341
1.342 -
1.343 -
1.344 section {* facts about supports *}
1.345 (*==============================*)
1.346
1.347 @@ -2184,6 +2026,7 @@
1.348 shows "(x \<sharp> X) = (x \<notin> X)"
1.349 by (simp add: at_fin_set_supp fresh_def at fs)
1.350
1.351 +
1.352 section {* Permutations acting on Functions *}
1.353 (*==========================================*)
1.354
1.355 @@ -2564,9 +2407,8 @@
1.356 and a1: "a\<sharp>x"
1.357 and a2: "a\<sharp>X"
1.358 shows "a\<sharp>(insert x X)"
1.359 -using a1 a2
1.360 -apply(simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
1.361 -done
1.362 + using a1 a2
1.363 + by (simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
1.364
1.365 lemma pt_list_set_supp:
1.366 fixes xs :: "'a list"
1.367 @@ -2595,14 +2437,191 @@
1.368 shows "a\<sharp>(set xs) = a\<sharp>xs"
1.369 by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
1.370
1.371 +
1.372 +section {* generalisation of freshness to lists and sets of atoms *}
1.373 +(*================================================================*)
1.374 +
1.375 +consts
1.376 + fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
1.377 +
1.378 +defs (overloaded)
1.379 + fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x\<in>xs. x\<sharp>c"
1.380 +
1.381 +defs (overloaded)
1.382 + fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x\<in>set xs. x\<sharp>c"
1.383 +
1.384 +lemmas fresh_star_def = fresh_star_list fresh_star_set
1.385 +
1.386 +lemma fresh_star_prod_set:
1.387 + fixes xs::"'a set"
1.388 + shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
1.389 +by (auto simp add: fresh_star_def fresh_prod)
1.390 +
1.391 +lemma fresh_star_prod_list:
1.392 + fixes xs::"'a list"
1.393 + shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
1.394 + by (auto simp add: fresh_star_def fresh_prod)
1.395 +
1.396 +lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
1.397 +
1.398 +lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c"
1.399 + by (simp add: fresh_star_def)
1.400 +
1.401 +lemma fresh_star_Un_elim:
1.402 + "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
1.403 + apply rule
1.404 + apply (simp_all add: fresh_star_def)
1.405 + apply (erule meta_mp)
1.406 + apply blast
1.407 + done
1.408 +
1.409 +lemma fresh_star_insert_elim:
1.410 + "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
1.411 + by rule (simp_all add: fresh_star_def)
1.412 +
1.413 +lemma fresh_star_empty_elim:
1.414 + "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
1.415 + by (simp add: fresh_star_def)
1.416 +
1.417 +text {* Normalization of freshness results; see \ @{text nominal_induct} *}
1.418 +
1.419 +lemma fresh_star_unit_elim:
1.420 + shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
1.421 + and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
1.422 + by (simp_all add: fresh_star_def fresh_def supp_unit)
1.423 +
1.424 +lemma fresh_star_prod_elim:
1.425 + shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
1.426 + and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
1.427 + by (rule, simp_all add: fresh_star_prod)+
1.428 +
1.429 +
1.430 +lemma pt_fresh_star_bij_ineq:
1.431 + fixes pi :: "'x prm"
1.432 + and x :: "'a"
1.433 + and a :: "'y set"
1.434 + and b :: "'y list"
1.435 + assumes pta: "pt TYPE('a) TYPE('x)"
1.436 + and ptb: "pt TYPE('y) TYPE('x)"
1.437 + and at: "at TYPE('x)"
1.438 + and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
1.439 + shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
1.440 + and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
1.441 +apply(unfold fresh_star_def)
1.442 +apply(auto)
1.443 +apply(drule_tac x="pi\<bullet>xa" in bspec)
1.444 +apply(erule pt_set_bij2[OF ptb, OF at])
1.445 +apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
1.446 +apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
1.447 +apply(simp add: pt_set_bij1[OF ptb, OF at])
1.448 +apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
1.449 +apply(drule_tac x="pi\<bullet>xa" in bspec)
1.450 +apply(simp add: pt_set_bij1[OF ptb, OF at])
1.451 +apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
1.452 +apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
1.453 +apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
1.454 +apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
1.455 +apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
1.456 +done
1.457 +
1.458 +lemma pt_fresh_star_bij:
1.459 + fixes pi :: "'x prm"
1.460 + and x :: "'a"
1.461 + and a :: "'x set"
1.462 + and b :: "'x list"
1.463 + assumes pt: "pt TYPE('a) TYPE('x)"
1.464 + and at: "at TYPE('x)"
1.465 + shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
1.466 + and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
1.467 +apply(rule pt_fresh_star_bij_ineq(1))
1.468 +apply(rule pt)
1.469 +apply(rule at_pt_inst)
1.470 +apply(rule at)+
1.471 +apply(rule cp_pt_inst)
1.472 +apply(rule pt)
1.473 +apply(rule at)
1.474 +apply(rule pt_fresh_star_bij_ineq(2))
1.475 +apply(rule pt)
1.476 +apply(rule at_pt_inst)
1.477 +apply(rule at)+
1.478 +apply(rule cp_pt_inst)
1.479 +apply(rule pt)
1.480 +apply(rule at)
1.481 +done
1.482 +
1.483 +lemma pt_fresh_star_eqvt:
1.484 + fixes pi :: "'x prm"
1.485 + and x :: "'a"
1.486 + and a :: "'x set"
1.487 + and b :: "'x list"
1.488 + assumes pt: "pt TYPE('a) TYPE('x)"
1.489 + and at: "at TYPE('x)"
1.490 + shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
1.491 + and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
1.492 + by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])
1.493 +
1.494 +lemma pt_fresh_star_eqvt_ineq:
1.495 + fixes pi::"'x prm"
1.496 + and a::"'y set"
1.497 + and b::"'y list"
1.498 + and x::"'a"
1.499 + assumes pta: "pt TYPE('a) TYPE('x)"
1.500 + and ptb: "pt TYPE('y) TYPE('x)"
1.501 + and at: "at TYPE('x)"
1.502 + and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
1.503 + and dj: "disjoint TYPE('y) TYPE('x)"
1.504 + shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
1.505 + and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
1.506 + by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
1.507 +
1.508 +lemma pt_freshs_freshs:
1.509 + assumes pt: "pt TYPE('a) TYPE('x)"
1.510 + and at: "at TYPE ('x)"
1.511 + and pi: "set (pi::'x prm) \<subseteq> Xs \<times> Ys"
1.512 + and Xs: "Xs \<sharp>* (x::'a)"
1.513 + and Ys: "Ys \<sharp>* x"
1.514 + shows "pi\<bullet>x = x"
1.515 + using pi
1.516 +proof (induct pi)
1.517 + case Nil
1.518 + show ?case by (simp add: pt1 [OF pt])
1.519 +next
1.520 + case (Cons p pi)
1.521 + obtain a b where p: "p = (a, b)" by (cases p)
1.522 + with Cons Xs Ys have "a \<sharp> x" "b \<sharp> x"
1.523 + by (simp_all add: fresh_star_def)
1.524 + with Cons p show ?case
1.525 + by (simp add: pt_fresh_fresh [OF pt at]
1.526 + pt2 [OF pt, of "[(a, b)]" pi, simplified])
1.527 +qed
1.528 +
1.529 +lemma pt_fresh_star_pi:
1.530 + fixes x::"'a"
1.531 + and pi::"'x prm"
1.532 + assumes pt: "pt TYPE('a) TYPE('x)"
1.533 + and at: "at TYPE('x)"
1.534 + and a: "((supp x)::'x set)\<sharp>* pi"
1.535 + shows "pi\<bullet>x = x"
1.536 +using a
1.537 +apply(induct pi)
1.538 +apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt])
1.539 +apply(subgoal_tac "((a,b)#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x")
1.540 +apply(simp only: pt2[OF pt])
1.541 +apply(rule pt_fresh_fresh[OF pt at])
1.542 +apply(simp add: fresh_def at_supp[OF at])
1.543 +apply(blast)
1.544 +apply(simp add: fresh_def at_supp[OF at])
1.545 +apply(blast)
1.546 +apply(simp add: pt2[OF pt])
1.547 +done
1.548 +
1.549 section {* Infrastructure lemmas for strong rule inductions *}
1.550 (*==========================================================*)
1.551
1.552 -
1.553 text {*
1.554 For every set of atoms, there is another set of atoms
1.555 avoiding a finitely supported c and there is a permutation
1.556 - which make 'translates' between both sets.
1.557 + which 'translates' between both sets.
1.558 *}
1.559 lemma at_set_avoiding_aux:
1.560 fixes Xs::"'a set"
1.561 @@ -3389,7 +3408,6 @@
1.562
1.563 syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
1.564
1.565 -
1.566 section {* lemmas for deciding permutation equations *}
1.567 (*===================================================*)
1.568
1.569 @@ -3550,8 +3568,8 @@
1.570 shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)"
1.571 by (simp add:perm_int_def)
1.572
1.573 -(*******************************************************************)
1.574 -(* Setup of the theorem attributes eqvt, eqvt_force, fresh and bij *)
1.575 +(*******************************************************)
1.576 +(* Setup of the theorem attributes eqvt and eqvt_force *)
1.577 use "nominal_thmdecls.ML"
1.578 setup "NominalThmDecls.setup"
1.579