1theory Nominal 2imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype" 3keywords 4 "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and 5 "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and 6 "avoids" 7begin 8 9declare [[typedef_overloaded]] 10 11 12section \<open>Permutations\<close> 13(*======================*) 14 15type_synonym 16 'x prm = "('x \<times> 'x) list" 17 18(* polymorphic constants for permutation and swapping *) 19consts 20 perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80) 21 swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" 22 23(* a "private" copy of the option type used in the abstraction function *) 24datatype 'a noption = nSome 'a | nNone 25 26datatype_compat noption 27 28(* a "private" copy of the product type used in the nominal induct method *) 29datatype ('a, 'b) nprod = nPair 'a 'b 30 31datatype_compat nprod 32 33(* an auxiliary constant for the decision procedure involving *) 34(* permutations (to avoid loops when using perm-compositions) *) 35definition 36 "perm_aux pi x = pi\<bullet>x" 37 38(* overloaded permutation operations *) 39overloading 40 perm_fun \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)" (unchecked) 41 perm_bool \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool" (unchecked) 42 perm_set \<equiv> "perm :: 'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set" (unchecked) 43 perm_unit \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit" (unchecked) 44 perm_prod \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" (unchecked) 45 perm_list \<equiv> "perm :: 'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" (unchecked) 46 perm_option \<equiv> "perm :: 'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" (unchecked) 47 perm_char \<equiv> "perm :: 'x prm \<Rightarrow> char \<Rightarrow> char" (unchecked) 48 perm_nat \<equiv> "perm :: 'x prm \<Rightarrow> nat \<Rightarrow> nat" (unchecked) 49 perm_int \<equiv> "perm :: 'x prm \<Rightarrow> int \<Rightarrow> int" (unchecked) 50 51 perm_noption \<equiv> "perm :: 'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" (unchecked) 52 perm_nprod \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked) 53begin 54 55definition perm_fun :: "'x prm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 56 "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))" 57 58definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where 59 "perm_bool pi b = b" 60 61definition perm_set :: "'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set" where 62 "perm_set pi X = {pi \<bullet> x | x. x \<in> X}" 63 64primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" where 65 "perm_unit pi () = ()" 66 67primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where 68 "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)" 69 70primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where 71 nil_eqvt: "perm_list pi [] = []" 72| cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)" 73 74primrec perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" where 75 some_eqvt: "perm_option pi (Some x) = Some (pi\<bullet>x)" 76| none_eqvt: "perm_option pi None = None" 77 78definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where 79 "perm_char pi c = c" 80 81definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where 82 "perm_nat pi i = i" 83 84definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where 85 "perm_int pi i = i" 86 87primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where 88 nsome_eqvt: "perm_noption pi (nSome x) = nSome (pi\<bullet>x)" 89| nnone_eqvt: "perm_noption pi nNone = nNone" 90 91primrec perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" where 92 "perm_nprod pi (nPair x y) = nPair (pi\<bullet>x) (pi\<bullet>y)" 93 94end 95 96(* permutations on booleans *) 97lemmas perm_bool = perm_bool_def 98 99lemma true_eqvt [simp]: 100 "pi \<bullet> True \<longleftrightarrow> True" 101 by (simp add: perm_bool_def) 102 103lemma false_eqvt [simp]: 104 "pi \<bullet> False \<longleftrightarrow> False" 105 by (simp add: perm_bool_def) 106 107lemma perm_boolI: 108 assumes a: "P" 109 shows "pi\<bullet>P" 110 using a by (simp add: perm_bool) 111 112lemma perm_boolE: 113 assumes a: "pi\<bullet>P" 114 shows "P" 115 using a by (simp add: perm_bool) 116 117lemma if_eqvt: 118 fixes pi::"'a prm" 119 shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))" 120 by (simp add: perm_fun_def) 121 122lemma imp_eqvt: 123 shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))" 124 by (simp add: perm_bool) 125 126lemma conj_eqvt: 127 shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))" 128 by (simp add: perm_bool) 129 130lemma disj_eqvt: 131 shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))" 132 by (simp add: perm_bool) 133 134lemma neg_eqvt: 135 shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))" 136 by (simp add: perm_bool) 137 138(* permutation on sets *) 139lemma empty_eqvt: 140 shows "pi\<bullet>{} = {}" 141 by (simp add: perm_set_def) 142 143lemma union_eqvt: 144 shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)" 145 by (auto simp add: perm_set_def) 146 147lemma insert_eqvt: 148 shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)" 149 by (auto simp add: perm_set_def) 150 151(* permutations on products *) 152lemma fst_eqvt: 153 "pi\<bullet>(fst x) = fst (pi\<bullet>x)" 154 by (cases x) simp 155 156lemma snd_eqvt: 157 "pi\<bullet>(snd x) = snd (pi\<bullet>x)" 158 by (cases x) simp 159 160(* permutation on lists *) 161lemma append_eqvt: 162 fixes pi :: "'x prm" 163 and l1 :: "'a list" 164 and l2 :: "'a list" 165 shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)" 166 by (induct l1) auto 167 168lemma rev_eqvt: 169 fixes pi :: "'x prm" 170 and l :: "'a list" 171 shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)" 172 by (induct l) (simp_all add: append_eqvt) 173 174lemma set_eqvt: 175 fixes pi :: "'x prm" 176 and xs :: "'a list" 177 shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)" 178by (induct xs) (auto simp add: empty_eqvt insert_eqvt) 179 180(* permutation on characters and strings *) 181lemma perm_string: 182 fixes s::"string" 183 shows "pi\<bullet>s = s" 184 by (induct s)(auto simp add: perm_char_def) 185 186 187section \<open>permutation equality\<close> 188(*==============================*) 189 190definition prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<triangleq> _ " [80,80] 80) where 191 "pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)" 192 193section \<open>Support, Freshness and Supports\<close> 194(*========================================*) 195definition supp :: "'a \<Rightarrow> ('x set)" where 196 "supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}" 197 198definition fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80) where 199 "a \<sharp> x \<longleftrightarrow> a \<notin> supp x" 200 201definition supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80) where 202 "S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))" 203 204(* lemmas about supp *) 205lemma supp_fresh_iff: 206 fixes x :: "'a" 207 shows "(supp x) = {a::'x. \<not>a\<sharp>x}" 208 by (simp add: fresh_def) 209 210lemma supp_unit: 211 shows "supp () = {}" 212 by (simp add: supp_def) 213 214lemma supp_set_empty: 215 shows "supp {} = {}" 216 by (force simp add: supp_def empty_eqvt) 217 218lemma supp_prod: 219 fixes x :: "'a" 220 and y :: "'b" 221 shows "(supp (x,y)) = (supp x)\<union>(supp y)" 222 by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 223 224lemma supp_nprod: 225 fixes x :: "'a" 226 and y :: "'b" 227 shows "(supp (nPair x y)) = (supp x)\<union>(supp y)" 228 by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 229 230lemma supp_list_nil: 231 shows "supp [] = {}" 232 by (simp add: supp_def) 233 234lemma supp_list_cons: 235 fixes x :: "'a" 236 and xs :: "'a list" 237 shows "supp (x#xs) = (supp x)\<union>(supp xs)" 238 by (auto simp add: supp_def Collect_imp_eq Collect_neg_eq) 239 240lemma supp_list_append: 241 fixes xs :: "'a list" 242 and ys :: "'a list" 243 shows "supp (xs@ys) = (supp xs)\<union>(supp ys)" 244 by (induct xs) (auto simp add: supp_list_nil supp_list_cons) 245 246lemma supp_list_rev: 247 fixes xs :: "'a list" 248 shows "supp (rev xs) = (supp xs)" 249 by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil) 250 251lemma supp_bool: 252 fixes x :: "bool" 253 shows "supp x = {}" 254 by (cases "x") (simp_all add: supp_def) 255 256lemma supp_some: 257 fixes x :: "'a" 258 shows "supp (Some x) = (supp x)" 259 by (simp add: supp_def) 260 261lemma supp_none: 262 fixes x :: "'a" 263 shows "supp (None) = {}" 264 by (simp add: supp_def) 265 266lemma supp_int: 267 fixes i::"int" 268 shows "supp (i) = {}" 269 by (simp add: supp_def perm_int_def) 270 271lemma supp_nat: 272 fixes n::"nat" 273 shows "(supp n) = {}" 274 by (simp add: supp_def perm_nat_def) 275 276lemma supp_char: 277 fixes c::"char" 278 shows "(supp c) = {}" 279 by (simp add: supp_def perm_char_def) 280 281lemma supp_string: 282 fixes s::"string" 283 shows "(supp s) = {}" 284 by (simp add: supp_def perm_string) 285 286(* lemmas about freshness *) 287lemma fresh_set_empty: 288 shows "a\<sharp>{}" 289 by (simp add: fresh_def supp_set_empty) 290 291lemma fresh_unit: 292 shows "a\<sharp>()" 293 by (simp add: fresh_def supp_unit) 294 295lemma fresh_prod: 296 fixes a :: "'x" 297 and x :: "'a" 298 and y :: "'b" 299 shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)" 300 by (simp add: fresh_def supp_prod) 301 302lemma fresh_list_nil: 303 fixes a :: "'x" 304 shows "a\<sharp>[]" 305 by (simp add: fresh_def supp_list_nil) 306 307lemma fresh_list_cons: 308 fixes a :: "'x" 309 and x :: "'a" 310 and xs :: "'a list" 311 shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)" 312 by (simp add: fresh_def supp_list_cons) 313 314lemma fresh_list_append: 315 fixes a :: "'x" 316 and xs :: "'a list" 317 and ys :: "'a list" 318 shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)" 319 by (simp add: fresh_def supp_list_append) 320 321lemma fresh_list_rev: 322 fixes a :: "'x" 323 and xs :: "'a list" 324 shows "a\<sharp>(rev xs) = a\<sharp>xs" 325 by (simp add: fresh_def supp_list_rev) 326 327lemma fresh_none: 328 fixes a :: "'x" 329 shows "a\<sharp>None" 330 by (simp add: fresh_def supp_none) 331 332lemma fresh_some: 333 fixes a :: "'x" 334 and x :: "'a" 335 shows "a\<sharp>(Some x) = a\<sharp>x" 336 by (simp add: fresh_def supp_some) 337 338lemma fresh_int: 339 fixes a :: "'x" 340 and i :: "int" 341 shows "a\<sharp>i" 342 by (simp add: fresh_def supp_int) 343 344lemma fresh_nat: 345 fixes a :: "'x" 346 and n :: "nat" 347 shows "a\<sharp>n" 348 by (simp add: fresh_def supp_nat) 349 350lemma fresh_char: 351 fixes a :: "'x" 352 and c :: "char" 353 shows "a\<sharp>c" 354 by (simp add: fresh_def supp_char) 355 356lemma fresh_string: 357 fixes a :: "'x" 358 and s :: "string" 359 shows "a\<sharp>s" 360 by (simp add: fresh_def supp_string) 361 362lemma fresh_bool: 363 fixes a :: "'x" 364 and b :: "bool" 365 shows "a\<sharp>b" 366 by (simp add: fresh_def supp_bool) 367 368text \<open>Normalization of freshness results; cf.\ \<open>nominal_induct\<close>\<close> 369lemma fresh_unit_elim: 370 shows "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C" 371 by (simp add: fresh_def supp_unit) 372 373lemma fresh_prod_elim: 374 shows "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)" 375 by rule (simp_all add: fresh_prod) 376 377(* this rule needs to be added before the fresh_prodD is *) 378(* added to the simplifier with mksimps *) 379lemma [simp]: 380 shows "a\<sharp>x1 \<Longrightarrow> a\<sharp>x2 \<Longrightarrow> a\<sharp>(x1,x2)" 381 by (simp add: fresh_prod) 382 383lemma fresh_prodD: 384 shows "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>x" 385 and "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y" 386 by (simp_all add: fresh_prod) 387 388ML \<open> 389 val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs; 390\<close> 391declaration \<open>fn _ => 392 Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs)) 393\<close> 394 395section \<open>Abstract Properties for Permutations and Atoms\<close> 396(*=========================================================*) 397 398(* properties for being a permutation type *) 399definition 400 "pt TYPE('a) TYPE('x) \<equiv> 401 (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 402 (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and> 403 (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<triangleq> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)" 404 405(* properties for being an atom type *) 406definition 407 "at TYPE('x) \<equiv> 408 (\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and> 409 (\<forall>(a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))\<bullet>x = swap (a,b) (pi\<bullet>x)) \<and> 410 (\<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> 411 (infinite (UNIV::'x set))" 412 413(* property of two atom-types being disjoint *) 414definition 415 "disjoint TYPE('x) TYPE('y) \<equiv> 416 (\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and> 417 (\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)" 418 419(* composition property of two permutation on a type 'a *) 420definition 421 "cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 422 (\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))" 423 424(* property of having finite support *) 425definition 426 "fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)" 427 428section \<open>Lemmas about the atom-type properties\<close> 429(*==============================================*) 430 431lemma at1: 432 fixes x::"'x" 433 assumes a: "at TYPE('x)" 434 shows "([]::'x prm)\<bullet>x = x" 435 using a by (simp add: at_def) 436 437lemma at2: 438 fixes a ::"'x" 439 and b ::"'x" 440 and x ::"'x" 441 and pi::"'x prm" 442 assumes a: "at TYPE('x)" 443 shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)" 444 using a by (simp only: at_def) 445 446lemma at3: 447 fixes a ::"'x" 448 and b ::"'x" 449 and c ::"'x" 450 assumes a: "at TYPE('x)" 451 shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))" 452 using a by (simp only: at_def) 453 454(* rules to calculate simple permutations *) 455lemmas at_calc = at2 at1 at3 456 457lemma at_swap_simps: 458 fixes a ::"'x" 459 and b ::"'x" 460 assumes a: "at TYPE('x)" 461 shows "[(a,b)]\<bullet>a = b" 462 and "[(a,b)]\<bullet>b = a" 463 and "\<lbrakk>a\<noteq>c; b\<noteq>c\<rbrakk> \<Longrightarrow> [(a,b)]\<bullet>c = c" 464 using a by (simp_all add: at_calc) 465 466lemma at4: 467 assumes a: "at TYPE('x)" 468 shows "infinite (UNIV::'x set)" 469 using a by (simp add: at_def) 470 471lemma at_append: 472 fixes pi1 :: "'x prm" 473 and pi2 :: "'x prm" 474 and c :: "'x" 475 assumes at: "at TYPE('x)" 476 shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)" 477proof (induct pi1) 478 case Nil show ?case by (simp add: at1[OF at]) 479next 480 case (Cons x xs) 481 have "(xs@pi2)\<bullet>c = xs\<bullet>(pi2\<bullet>c)" by fact 482 also have "(x#xs)@pi2 = x#(xs@pi2)" by simp 483 ultimately show ?case by (cases "x", simp add: at2[OF at]) 484qed 485 486lemma at_swap: 487 fixes a :: "'x" 488 and b :: "'x" 489 and c :: "'x" 490 assumes at: "at TYPE('x)" 491 shows "swap (a,b) (swap (a,b) c) = c" 492 by (auto simp add: at3[OF at]) 493 494lemma at_rev_pi: 495 fixes pi :: "'x prm" 496 and c :: "'x" 497 assumes at: "at TYPE('x)" 498 shows "(rev pi)\<bullet>(pi\<bullet>c) = c" 499proof(induct pi) 500 case Nil show ?case by (simp add: at1[OF at]) 501next 502 case (Cons x xs) thus ?case 503 by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at]) 504qed 505 506lemma at_pi_rev: 507 fixes pi :: "'x prm" 508 and x :: "'x" 509 assumes at: "at TYPE('x)" 510 shows "pi\<bullet>((rev pi)\<bullet>x) = x" 511 by (rule at_rev_pi[OF at, of "rev pi" _,simplified]) 512 513lemma at_bij1: 514 fixes pi :: "'x prm" 515 and x :: "'x" 516 and y :: "'x" 517 assumes at: "at TYPE('x)" 518 and a: "(pi\<bullet>x) = y" 519 shows "x=(rev pi)\<bullet>y" 520proof - 521 from a have "y=(pi\<bullet>x)" by (rule sym) 522 thus ?thesis by (simp only: at_rev_pi[OF at]) 523qed 524 525lemma at_bij2: 526 fixes pi :: "'x prm" 527 and x :: "'x" 528 and y :: "'x" 529 assumes at: "at TYPE('x)" 530 and a: "((rev pi)\<bullet>x) = y" 531 shows "x=pi\<bullet>y" 532proof - 533 from a have "y=((rev pi)\<bullet>x)" by (rule sym) 534 thus ?thesis by (simp only: at_pi_rev[OF at]) 535qed 536 537lemma at_bij: 538 fixes pi :: "'x prm" 539 and x :: "'x" 540 and y :: "'x" 541 assumes at: "at TYPE('x)" 542 shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)" 543proof 544 assume "pi\<bullet>x = pi\<bullet>y" 545 hence "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 546 thus "x=y" by (simp only: at_rev_pi[OF at]) 547next 548 assume "x=y" 549 thus "pi\<bullet>x = pi\<bullet>y" by simp 550qed 551 552lemma at_supp: 553 fixes x :: "'x" 554 assumes at: "at TYPE('x)" 555 shows "supp x = {x}" 556by(auto simp: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at] at4[OF at]) 557 558lemma at_fresh: 559 fixes a :: "'x" 560 and b :: "'x" 561 assumes at: "at TYPE('x)" 562 shows "(a\<sharp>b) = (a\<noteq>b)" 563 by (simp add: at_supp[OF at] fresh_def) 564 565lemma at_prm_fresh1: 566 fixes c :: "'x" 567 and pi:: "'x prm" 568 assumes at: "at TYPE('x)" 569 and a: "c\<sharp>pi" 570 shows "\<forall>(a,b)\<in>set pi. c\<noteq>a \<and> c\<noteq>b" 571using a by (induct pi) (auto simp add: fresh_list_cons fresh_prod at_fresh[OF at]) 572 573lemma at_prm_fresh2: 574 fixes c :: "'x" 575 and pi:: "'x prm" 576 assumes at: "at TYPE('x)" 577 and a: "\<forall>(a,b)\<in>set pi. c\<noteq>a \<and> c\<noteq>b" 578 shows "pi\<bullet>c = c" 579using a by(induct pi) (auto simp add: at1[OF at] at2[OF at] at3[OF at]) 580 581lemma at_prm_fresh: 582 fixes c :: "'x" 583 and pi:: "'x prm" 584 assumes at: "at TYPE('x)" 585 and a: "c\<sharp>pi" 586 shows "pi\<bullet>c = c" 587by (rule at_prm_fresh2[OF at], rule at_prm_fresh1[OF at, OF a]) 588 589lemma at_prm_rev_eq: 590 fixes pi1 :: "'x prm" 591 and pi2 :: "'x prm" 592 assumes at: "at TYPE('x)" 593 shows "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)" 594proof (simp add: prm_eq_def, auto) 595 fix x 596 assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x" 597 hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp 598 hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at]) 599 hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at]) 600 thus "pi1\<bullet>x = pi2\<bullet>x" by simp 601next 602 fix x 603 assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x" 604 hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp 605 hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at]) 606 hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at]) 607 thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp 608qed 609 610lemma at_prm_eq_append: 611 fixes pi1 :: "'x prm" 612 and pi2 :: "'x prm" 613 and pi3 :: "'x prm" 614 assumes at: "at TYPE('x)" 615 and a: "pi1 \<triangleq> pi2" 616 shows "(pi3@pi1) \<triangleq> (pi3@pi2)" 617using a by (simp add: prm_eq_def at_append[OF at] at_bij[OF at]) 618 619lemma at_prm_eq_append': 620 fixes pi1 :: "'x prm" 621 and pi2 :: "'x prm" 622 and pi3 :: "'x prm" 623 assumes at: "at TYPE('x)" 624 and a: "pi1 \<triangleq> pi2" 625 shows "(pi1@pi3) \<triangleq> (pi2@pi3)" 626using a by (simp add: prm_eq_def at_append[OF at]) 627 628lemma at_prm_eq_trans: 629 fixes pi1 :: "'x prm" 630 and pi2 :: "'x prm" 631 and pi3 :: "'x prm" 632 assumes a1: "pi1 \<triangleq> pi2" 633 and a2: "pi2 \<triangleq> pi3" 634 shows "pi1 \<triangleq> pi3" 635using a1 a2 by (auto simp add: prm_eq_def) 636 637lemma at_prm_eq_refl: 638 fixes pi :: "'x prm" 639 shows "pi \<triangleq> pi" 640by (simp add: prm_eq_def) 641 642lemma at_prm_rev_eq1: 643 fixes pi1 :: "'x prm" 644 and pi2 :: "'x prm" 645 assumes at: "at TYPE('x)" 646 shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)" 647 by (simp add: at_prm_rev_eq[OF at]) 648 649lemma at_ds1: 650 fixes a :: "'x" 651 assumes at: "at TYPE('x)" 652 shows "[(a,a)] \<triangleq> []" 653 by (force simp add: prm_eq_def at_calc[OF at]) 654 655lemma at_ds2: 656 fixes pi :: "'x prm" 657 and a :: "'x" 658 and b :: "'x" 659 assumes at: "at TYPE('x)" 660 shows "([(a,b)]@pi) \<triangleq> (pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)])" 661 by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 662 at_rev_pi[OF at] at_calc[OF at]) 663 664lemma at_ds3: 665 fixes a :: "'x" 666 and b :: "'x" 667 and c :: "'x" 668 assumes at: "at TYPE('x)" 669 and a: "distinct [a,b,c]" 670 shows "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" 671 using a by (force simp add: prm_eq_def at_calc[OF at]) 672 673lemma at_ds4: 674 fixes a :: "'x" 675 and b :: "'x" 676 and pi :: "'x prm" 677 assumes at: "at TYPE('x)" 678 shows "(pi@[(a,(rev pi)\<bullet>b)]) \<triangleq> ([(pi\<bullet>a,b)]@pi)" 679 by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 680 at_pi_rev[OF at] at_rev_pi[OF at]) 681 682lemma at_ds5: 683 fixes a :: "'x" 684 and b :: "'x" 685 assumes at: "at TYPE('x)" 686 shows "[(a,b)] \<triangleq> [(b,a)]" 687 by (force simp add: prm_eq_def at_calc[OF at]) 688 689lemma at_ds5': 690 fixes a :: "'x" 691 and b :: "'x" 692 assumes at: "at TYPE('x)" 693 shows "[(a,b),(b,a)] \<triangleq> []" 694 by (force simp add: prm_eq_def at_calc[OF at]) 695 696lemma at_ds6: 697 fixes a :: "'x" 698 and b :: "'x" 699 and c :: "'x" 700 assumes at: "at TYPE('x)" 701 and a: "distinct [a,b,c]" 702 shows "[(a,c),(a,b)] \<triangleq> [(b,c),(a,c)]" 703 using a by (force simp add: prm_eq_def at_calc[OF at]) 704 705lemma at_ds7: 706 fixes pi :: "'x prm" 707 assumes at: "at TYPE('x)" 708 shows "((rev pi)@pi) \<triangleq> []" 709 by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at]) 710 711lemma at_ds8_aux: 712 fixes pi :: "'x prm" 713 and a :: "'x" 714 and b :: "'x" 715 and c :: "'x" 716 assumes at: "at TYPE('x)" 717 shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)" 718 by (force simp add: at_calc[OF at] at_bij[OF at]) 719 720lemma at_ds8: 721 fixes pi1 :: "'x prm" 722 and pi2 :: "'x prm" 723 and a :: "'x" 724 and b :: "'x" 725 assumes at: "at TYPE('x)" 726 shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)" 727apply(induct_tac pi2) 728apply(simp add: prm_eq_def) 729apply(auto simp add: prm_eq_def) 730apply(simp add: at2[OF at]) 731apply(drule_tac x="aa" in spec) 732apply(drule sym) 733apply(simp) 734apply(simp add: at_append[OF at]) 735apply(simp add: at2[OF at]) 736apply(simp add: at_ds8_aux[OF at]) 737done 738 739lemma at_ds9: 740 fixes pi1 :: "'x prm" 741 and pi2 :: "'x prm" 742 and a :: "'x" 743 and b :: "'x" 744 assumes at: "at TYPE('x)" 745 shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))" 746apply(induct_tac pi2) 747apply(simp add: prm_eq_def) 748apply(auto simp add: prm_eq_def) 749apply(simp add: at_append[OF at]) 750apply(simp add: at2[OF at] at1[OF at]) 751apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec) 752apply(drule sym) 753apply(simp) 754apply(simp add: at_ds8_aux[OF at]) 755apply(simp add: at_rev_pi[OF at]) 756done 757 758lemma at_ds10: 759 fixes pi :: "'x prm" 760 and a :: "'x" 761 and b :: "'x" 762 assumes at: "at TYPE('x)" 763 and a: "b\<sharp>(rev pi)" 764 shows "([(pi\<bullet>a,b)]@pi) \<triangleq> (pi@[(a,b)])" 765using a 766apply - 767apply(rule at_prm_eq_trans) 768apply(rule at_ds2[OF at]) 769apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at]) 770apply(rule at_prm_eq_refl) 771done 772 773\<comment> \<open>there always exists an atom that is not being in a finite set\<close> 774lemma ex_in_inf: 775 fixes A::"'x set" 776 assumes at: "at TYPE('x)" 777 and fs: "finite A" 778 obtains c::"'x" where "c\<notin>A" 779proof - 780 from fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 781 by (simp add: Diff_infinite_finite) 782 hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:) 783 then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force 784 then have "c\<notin>A" by simp 785 then show ?thesis .. 786qed 787 788text \<open>there always exists a fresh name for an object with finite support\<close> 789lemma at_exists_fresh': 790 fixes x :: "'a" 791 assumes at: "at TYPE('x)" 792 and fs: "finite ((supp x)::'x set)" 793 shows "\<exists>c::'x. c\<sharp>x" 794 by (auto simp add: fresh_def intro: ex_in_inf[OF at, OF fs]) 795 796lemma at_exists_fresh: 797 fixes x :: "'a" 798 assumes at: "at TYPE('x)" 799 and fs: "finite ((supp x)::'x set)" 800 obtains c::"'x" where "c\<sharp>x" 801 by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def) 802 803lemma at_finite_select: 804 fixes S::"'a set" 805 assumes a: "at TYPE('a)" 806 and b: "finite S" 807 shows "\<exists>x. x \<notin> S" 808 using a b 809 apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite) 810 apply(simp add: at_def) 811 apply(subgoal_tac "UNIV - S \<noteq> {}") 812 apply(simp only: ex_in_conv [symmetric]) 813 apply(blast) 814 apply(rule notI) 815 apply(simp) 816 done 817 818lemma at_different: 819 assumes at: "at TYPE('x)" 820 shows "\<exists>(b::'x). a\<noteq>b" 821proof - 822 have "infinite (UNIV::'x set)" by (rule at4[OF at]) 823 hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove) 824 have "(UNIV-{a}) \<noteq> ({}::'x set)" 825 proof (rule_tac ccontr, drule_tac notnotD) 826 assume "UNIV-{a} = ({}::'x set)" 827 with inf2 have "infinite ({}::'x set)" by simp 828 then show "False" by auto 829 qed 830 hence "\<exists>(b::'x). b\<in>(UNIV-{a})" by blast 831 then obtain b::"'x" where mem2: "b\<in>(UNIV-{a})" by blast 832 from mem2 have "a\<noteq>b" by blast 833 then show "\<exists>(b::'x). a\<noteq>b" by blast 834qed 835 836\<comment> \<open>the at-props imply the pt-props\<close> 837lemma at_pt_inst: 838 assumes at: "at TYPE('x)" 839 shows "pt TYPE('x) TYPE('x)" 840apply(auto simp only: pt_def) 841apply(simp only: at1[OF at]) 842apply(simp only: at_append[OF at]) 843apply(simp only: prm_eq_def) 844done 845 846section \<open>finite support properties\<close> 847(*===================================*) 848 849lemma fs1: 850 fixes x :: "'a" 851 assumes a: "fs TYPE('a) TYPE('x)" 852 shows "finite ((supp x)::'x set)" 853 using a by (simp add: fs_def) 854 855lemma fs_at_inst: 856 fixes a :: "'x" 857 assumes at: "at TYPE('x)" 858 shows "fs TYPE('x) TYPE('x)" 859apply(simp add: fs_def) 860apply(simp add: at_supp[OF at]) 861done 862 863lemma fs_unit_inst: 864 shows "fs TYPE(unit) TYPE('x)" 865apply(simp add: fs_def) 866apply(simp add: supp_unit) 867done 868 869lemma fs_prod_inst: 870 assumes fsa: "fs TYPE('a) TYPE('x)" 871 and fsb: "fs TYPE('b) TYPE('x)" 872 shows "fs TYPE('a\<times>'b) TYPE('x)" 873apply(unfold fs_def) 874apply(auto simp add: supp_prod) 875apply(rule fs1[OF fsa]) 876apply(rule fs1[OF fsb]) 877done 878 879lemma fs_nprod_inst: 880 assumes fsa: "fs TYPE('a) TYPE('x)" 881 and fsb: "fs TYPE('b) TYPE('x)" 882 shows "fs TYPE(('a,'b) nprod) TYPE('x)" 883apply(unfold fs_def, rule allI) 884apply(case_tac x) 885apply(auto simp add: supp_nprod) 886apply(rule fs1[OF fsa]) 887apply(rule fs1[OF fsb]) 888done 889 890lemma fs_list_inst: 891 assumes fs: "fs TYPE('a) TYPE('x)" 892 shows "fs TYPE('a list) TYPE('x)" 893apply(simp add: fs_def, rule allI) 894apply(induct_tac x) 895apply(simp add: supp_list_nil) 896apply(simp add: supp_list_cons) 897apply(rule fs1[OF fs]) 898done 899 900lemma fs_option_inst: 901 assumes fs: "fs TYPE('a) TYPE('x)" 902 shows "fs TYPE('a option) TYPE('x)" 903apply(simp add: fs_def, rule allI) 904apply(case_tac x) 905apply(simp add: supp_none) 906apply(simp add: supp_some) 907apply(rule fs1[OF fs]) 908done 909 910section \<open>Lemmas about the permutation properties\<close> 911(*=================================================*) 912 913lemma pt1: 914 fixes x::"'a" 915 assumes a: "pt TYPE('a) TYPE('x)" 916 shows "([]::'x prm)\<bullet>x = x" 917 using a by (simp add: pt_def) 918 919lemma pt2: 920 fixes pi1::"'x prm" 921 and pi2::"'x prm" 922 and x ::"'a" 923 assumes a: "pt TYPE('a) TYPE('x)" 924 shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)" 925 using a by (simp add: pt_def) 926 927lemma pt3: 928 fixes pi1::"'x prm" 929 and pi2::"'x prm" 930 and x ::"'a" 931 assumes a: "pt TYPE('a) TYPE('x)" 932 shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x" 933 using a by (simp add: pt_def) 934 935lemma pt3_rev: 936 fixes pi1::"'x prm" 937 and pi2::"'x prm" 938 and x ::"'a" 939 assumes pt: "pt TYPE('a) TYPE('x)" 940 and at: "at TYPE('x)" 941 shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x" 942 by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at]) 943 944section \<open>composition properties\<close> 945(* ============================== *) 946lemma cp1: 947 fixes pi1::"'x prm" 948 and pi2::"'y prm" 949 and x ::"'a" 950 assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" 951 shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)" 952 using cp by (simp add: cp_def) 953 954lemma cp_pt_inst: 955 assumes pt: "pt TYPE('a) TYPE('x)" 956 and at: "at TYPE('x)" 957 shows "cp TYPE('a) TYPE('x) TYPE('x)" 958apply(auto simp add: cp_def pt2[OF pt,symmetric]) 959apply(rule pt3[OF pt]) 960apply(rule at_ds8[OF at]) 961done 962 963section \<open>disjointness properties\<close> 964(*=================================*) 965lemma dj_perm_forget: 966 fixes pi::"'y prm" 967 and x ::"'x" 968 assumes dj: "disjoint TYPE('x) TYPE('y)" 969 shows "pi\<bullet>x=x" 970 using dj by (simp_all add: disjoint_def) 971 972lemma dj_perm_set_forget: 973 fixes pi::"'y prm" 974 and x ::"'x set" 975 assumes dj: "disjoint TYPE('x) TYPE('y)" 976 shows "pi\<bullet>x=x" 977 using dj by (simp_all add: perm_set_def disjoint_def) 978 979lemma dj_perm_perm_forget: 980 fixes pi1::"'x prm" 981 and pi2::"'y prm" 982 assumes dj: "disjoint TYPE('x) TYPE('y)" 983 shows "pi2\<bullet>pi1=pi1" 984 using dj by (induct pi1, auto simp add: disjoint_def) 985 986lemma dj_cp: 987 fixes pi1::"'x prm" 988 and pi2::"'y prm" 989 and x ::"'a" 990 assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" 991 and dj: "disjoint TYPE('y) TYPE('x)" 992 shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)" 993 by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj]) 994 995lemma dj_supp: 996 fixes a::"'x" 997 assumes dj: "disjoint TYPE('x) TYPE('y)" 998 shows "(supp a) = ({}::'y set)" 999apply(simp add: supp_def dj_perm_forget[OF dj]) 1000done 1001 1002lemma at_fresh_ineq: 1003 fixes a :: "'x" 1004 and b :: "'y" 1005 assumes dj: "disjoint TYPE('y) TYPE('x)" 1006 shows "a\<sharp>b" 1007 by (simp add: fresh_def dj_supp[OF dj]) 1008 1009section \<open>permutation type instances\<close> 1010(* ===================================*) 1011 1012lemma pt_fun_inst: 1013 assumes pta: "pt TYPE('a) TYPE('x)" 1014 and ptb: "pt TYPE('b) TYPE('x)" 1015 and at: "at TYPE('x)" 1016 shows "pt TYPE('a\<Rightarrow>'b) TYPE('x)" 1017apply(auto simp only: pt_def) 1018apply(simp_all add: perm_fun_def) 1019apply(simp add: pt1[OF pta] pt1[OF ptb]) 1020apply(simp add: pt2[OF pta] pt2[OF ptb]) 1021apply(subgoal_tac "(rev pi1) \<triangleq> (rev pi2)")(*A*) 1022apply(simp add: pt3[OF pta] pt3[OF ptb]) 1023(*A*) 1024apply(simp add: at_prm_rev_eq[OF at]) 1025done 1026 1027lemma pt_bool_inst: 1028 shows "pt TYPE(bool) TYPE('x)" 1029 by (simp add: pt_def perm_bool_def) 1030 1031lemma pt_set_inst: 1032 assumes pt: "pt TYPE('a) TYPE('x)" 1033 shows "pt TYPE('a set) TYPE('x)" 1034apply(simp add: pt_def) 1035apply(simp_all add: perm_set_def) 1036apply(simp add: pt1[OF pt]) 1037apply(force simp add: pt2[OF pt] pt3[OF pt]) 1038done 1039 1040lemma pt_unit_inst: 1041 shows "pt TYPE(unit) TYPE('x)" 1042 by (simp add: pt_def) 1043 1044lemma pt_prod_inst: 1045 assumes pta: "pt TYPE('a) TYPE('x)" 1046 and ptb: "pt TYPE('b) TYPE('x)" 1047 shows "pt TYPE('a \<times> 'b) TYPE('x)" 1048 apply(auto simp add: pt_def) 1049 apply(rule pt1[OF pta]) 1050 apply(rule pt1[OF ptb]) 1051 apply(rule pt2[OF pta]) 1052 apply(rule pt2[OF ptb]) 1053 apply(rule pt3[OF pta],assumption) 1054 apply(rule pt3[OF ptb],assumption) 1055 done 1056 1057lemma pt_list_nil: 1058 fixes xs :: "'a list" 1059 assumes pt: "pt TYPE('a) TYPE ('x)" 1060 shows "([]::'x prm)\<bullet>xs = xs" 1061apply(induct_tac xs) 1062apply(simp_all add: pt1[OF pt]) 1063done 1064 1065lemma pt_list_append: 1066 fixes pi1 :: "'x prm" 1067 and pi2 :: "'x prm" 1068 and xs :: "'a list" 1069 assumes pt: "pt TYPE('a) TYPE ('x)" 1070 shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)" 1071apply(induct_tac xs) 1072apply(simp_all add: pt2[OF pt]) 1073done 1074 1075lemma pt_list_prm_eq: 1076 fixes pi1 :: "'x prm" 1077 and pi2 :: "'x prm" 1078 and xs :: "'a list" 1079 assumes pt: "pt TYPE('a) TYPE ('x)" 1080 shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs" 1081apply(induct_tac xs) 1082apply(simp_all add: prm_eq_def pt3[OF pt]) 1083done 1084 1085lemma pt_list_inst: 1086 assumes pt: "pt TYPE('a) TYPE('x)" 1087 shows "pt TYPE('a list) TYPE('x)" 1088apply(auto simp only: pt_def) 1089apply(rule pt_list_nil[OF pt]) 1090apply(rule pt_list_append[OF pt]) 1091apply(rule pt_list_prm_eq[OF pt],assumption) 1092done 1093 1094lemma pt_option_inst: 1095 assumes pta: "pt TYPE('a) TYPE('x)" 1096 shows "pt TYPE('a option) TYPE('x)" 1097apply(auto simp only: pt_def) 1098apply(case_tac "x") 1099apply(simp_all add: pt1[OF pta]) 1100apply(case_tac "x") 1101apply(simp_all add: pt2[OF pta]) 1102apply(case_tac "x") 1103apply(simp_all add: pt3[OF pta]) 1104done 1105 1106lemma pt_noption_inst: 1107 assumes pta: "pt TYPE('a) TYPE('x)" 1108 shows "pt TYPE('a noption) TYPE('x)" 1109apply(auto simp only: pt_def) 1110apply(case_tac "x") 1111apply(simp_all add: pt1[OF pta]) 1112apply(case_tac "x") 1113apply(simp_all add: pt2[OF pta]) 1114apply(case_tac "x") 1115apply(simp_all add: pt3[OF pta]) 1116done 1117 1118lemma pt_nprod_inst: 1119 assumes pta: "pt TYPE('a) TYPE('x)" 1120 and ptb: "pt TYPE('b) TYPE('x)" 1121 shows "pt TYPE(('a,'b) nprod) TYPE('x)" 1122 apply(auto simp add: pt_def) 1123 apply(case_tac x) 1124 apply(simp add: pt1[OF pta] pt1[OF ptb]) 1125 apply(case_tac x) 1126 apply(simp add: pt2[OF pta] pt2[OF ptb]) 1127 apply(case_tac x) 1128 apply(simp add: pt3[OF pta] pt3[OF ptb]) 1129 done 1130 1131section \<open>further lemmas for permutation types\<close> 1132(*==============================================*) 1133 1134lemma pt_rev_pi: 1135 fixes pi :: "'x prm" 1136 and x :: "'a" 1137 assumes pt: "pt TYPE('a) TYPE('x)" 1138 and at: "at TYPE('x)" 1139 shows "(rev pi)\<bullet>(pi\<bullet>x) = x" 1140proof - 1141 have "((rev pi)@pi) \<triangleq> ([]::'x prm)" by (simp add: at_ds7[OF at]) 1142 hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 1143 thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt]) 1144qed 1145 1146lemma pt_pi_rev: 1147 fixes pi :: "'x prm" 1148 and x :: "'a" 1149 assumes pt: "pt TYPE('a) TYPE('x)" 1150 and at: "at TYPE('x)" 1151 shows "pi\<bullet>((rev pi)\<bullet>x) = x" 1152 by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified]) 1153 1154lemma pt_bij1: 1155 fixes pi :: "'x prm" 1156 and x :: "'a" 1157 and y :: "'a" 1158 assumes pt: "pt TYPE('a) TYPE('x)" 1159 and at: "at TYPE('x)" 1160 and a: "(pi\<bullet>x) = y" 1161 shows "x=(rev pi)\<bullet>y" 1162proof - 1163 from a have "y=(pi\<bullet>x)" by (rule sym) 1164 thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at]) 1165qed 1166 1167lemma pt_bij2: 1168 fixes pi :: "'x prm" 1169 and x :: "'a" 1170 and y :: "'a" 1171 assumes pt: "pt TYPE('a) TYPE('x)" 1172 and at: "at TYPE('x)" 1173 and a: "x = (rev pi)\<bullet>y" 1174 shows "(pi\<bullet>x)=y" 1175 using a by (simp add: pt_pi_rev[OF pt, OF at]) 1176 1177lemma pt_bij: 1178 fixes pi :: "'x prm" 1179 and x :: "'a" 1180 and y :: "'a" 1181 assumes pt: "pt TYPE('a) TYPE('x)" 1182 and at: "at TYPE('x)" 1183 shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)" 1184proof 1185 assume "pi\<bullet>x = pi\<bullet>y" 1186 hence "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 1187 thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at]) 1188next 1189 assume "x=y" 1190 thus "pi\<bullet>x = pi\<bullet>y" by simp 1191qed 1192 1193lemma pt_eq_eqvt: 1194 fixes pi :: "'x prm" 1195 and x :: "'a" 1196 and y :: "'a" 1197 assumes pt: "pt TYPE('a) TYPE('x)" 1198 and at: "at TYPE('x)" 1199 shows "pi\<bullet>(x=y) = (pi\<bullet>x = pi\<bullet>y)" 1200 using pt at 1201 by (auto simp add: pt_bij perm_bool) 1202 1203lemma pt_bij3: 1204 fixes pi :: "'x prm" 1205 and x :: "'a" 1206 and y :: "'a" 1207 assumes a: "x=y" 1208 shows "(pi\<bullet>x = pi\<bullet>y)" 1209 using a by simp 1210 1211lemma pt_bij4: 1212 fixes pi :: "'x prm" 1213 and x :: "'a" 1214 and y :: "'a" 1215 assumes pt: "pt TYPE('a) TYPE('x)" 1216 and at: "at TYPE('x)" 1217 and a: "pi\<bullet>x = pi\<bullet>y" 1218 shows "x = y" 1219 using a by (simp add: pt_bij[OF pt, OF at]) 1220 1221lemma pt_swap_bij: 1222 fixes a :: "'x" 1223 and b :: "'x" 1224 and x :: "'a" 1225 assumes pt: "pt TYPE('a) TYPE('x)" 1226 and at: "at TYPE('x)" 1227 shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x" 1228 by (rule pt_bij2[OF pt, OF at], simp) 1229 1230lemma pt_swap_bij': 1231 fixes a :: "'x" 1232 and b :: "'x" 1233 and x :: "'a" 1234 assumes pt: "pt TYPE('a) TYPE('x)" 1235 and at: "at TYPE('x)" 1236 shows "[(a,b)]\<bullet>([(b,a)]\<bullet>x) = x" 1237apply(simp add: pt2[OF pt,symmetric]) 1238apply(rule trans) 1239apply(rule pt3[OF pt]) 1240apply(rule at_ds5'[OF at]) 1241apply(rule pt1[OF pt]) 1242done 1243 1244lemma pt_swap_bij'': 1245 fixes a :: "'x" 1246 and x :: "'a" 1247 assumes pt: "pt TYPE('a) TYPE('x)" 1248 and at: "at TYPE('x)" 1249 shows "[(a,a)]\<bullet>x = x" 1250apply(rule trans) 1251apply(rule pt3[OF pt]) 1252apply(rule at_ds1[OF at]) 1253apply(rule pt1[OF pt]) 1254done 1255 1256lemma supp_singleton: 1257 shows "supp {x} = supp x" 1258 by (force simp add: supp_def perm_set_def) 1259 1260lemma fresh_singleton: 1261 shows "a\<sharp>{x} = a\<sharp>x" 1262 by (simp add: fresh_def supp_singleton) 1263 1264lemma pt_set_bij1: 1265 fixes pi :: "'x prm" 1266 and x :: "'a" 1267 and X :: "'a set" 1268 assumes pt: "pt TYPE('a) TYPE('x)" 1269 and at: "at TYPE('x)" 1270 shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))" 1271 by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) 1272 1273lemma pt_set_bij1a: 1274 fixes pi :: "'x prm" 1275 and x :: "'a" 1276 and X :: "'a set" 1277 assumes pt: "pt TYPE('a) TYPE('x)" 1278 and at: "at TYPE('x)" 1279 shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)" 1280 by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) 1281 1282lemma pt_set_bij: 1283 fixes pi :: "'x prm" 1284 and x :: "'a" 1285 and X :: "'a set" 1286 assumes pt: "pt TYPE('a) TYPE('x)" 1287 and at: "at TYPE('x)" 1288 shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)" 1289 by (simp add: perm_set_def pt_bij[OF pt, OF at]) 1290 1291lemma pt_in_eqvt: 1292 fixes pi :: "'x prm" 1293 and x :: "'a" 1294 and X :: "'a set" 1295 assumes pt: "pt TYPE('a) TYPE('x)" 1296 and at: "at TYPE('x)" 1297 shows "pi\<bullet>(x\<in>X)=((pi\<bullet>x)\<in>(pi\<bullet>X))" 1298using assms 1299by (auto simp add: pt_set_bij perm_bool) 1300 1301lemma pt_set_bij2: 1302 fixes pi :: "'x prm" 1303 and x :: "'a" 1304 and X :: "'a set" 1305 assumes pt: "pt TYPE('a) TYPE('x)" 1306 and at: "at TYPE('x)" 1307 and a: "x\<in>X" 1308 shows "(pi\<bullet>x)\<in>(pi\<bullet>X)" 1309 using a by (simp add: pt_set_bij[OF pt, OF at]) 1310 1311lemma pt_set_bij2a: 1312 fixes pi :: "'x prm" 1313 and x :: "'a" 1314 and X :: "'a set" 1315 assumes pt: "pt TYPE('a) TYPE('x)" 1316 and at: "at TYPE('x)" 1317 and a: "x\<in>((rev pi)\<bullet>X)" 1318 shows "(pi\<bullet>x)\<in>X" 1319 using a by (simp add: pt_set_bij1[OF pt, OF at]) 1320 1321(* FIXME: is this lemma needed anywhere? *) 1322lemma pt_set_bij3: 1323 fixes pi :: "'x prm" 1324 and x :: "'a" 1325 and X :: "'a set" 1326 shows "pi\<bullet>(x\<in>X) = (x\<in>X)" 1327by (simp add: perm_bool) 1328 1329lemma pt_subseteq_eqvt: 1330 fixes pi :: "'x prm" 1331 and Y :: "'a set" 1332 and X :: "'a set" 1333 assumes pt: "pt TYPE('a) TYPE('x)" 1334 and at: "at TYPE('x)" 1335 shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))" 1336by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at]) 1337 1338lemma pt_set_diff_eqvt: 1339 fixes X::"'a set" 1340 and Y::"'a set" 1341 and pi::"'x prm" 1342 assumes pt: "pt TYPE('a) TYPE('x)" 1343 and at: "at TYPE('x)" 1344 shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)" 1345 by (auto simp add: perm_set_def pt_bij[OF pt, OF at]) 1346 1347lemma pt_Collect_eqvt: 1348 fixes pi::"'x prm" 1349 assumes pt: "pt TYPE('a) TYPE('x)" 1350 and at: "at TYPE('x)" 1351 shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}" 1352apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at]) 1353apply(rule_tac x="(rev pi)\<bullet>x" in exI) 1354apply(simp add: pt_pi_rev[OF pt, OF at]) 1355done 1356 1357\<comment> \<open>some helper lemmas for the pt_perm_supp_ineq lemma\<close> 1358lemma Collect_permI: 1359 fixes pi :: "'x prm" 1360 and x :: "'a" 1361 assumes a: "\<forall>x. (P1 x = P2 x)" 1362 shows "{pi\<bullet>x| x. P1 x} = {pi\<bullet>x| x. P2 x}" 1363 using a by force 1364 1365lemma Infinite_cong: 1366 assumes a: "X = Y" 1367 shows "infinite X = infinite Y" 1368 using a by (simp) 1369 1370lemma pt_set_eq_ineq: 1371 fixes pi :: "'y prm" 1372 assumes pt: "pt TYPE('x) TYPE('y)" 1373 and at: "at TYPE('y)" 1374 shows "{pi\<bullet>x| x::'x. P x} = {x::'x. P ((rev pi)\<bullet>x)}" 1375 by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) 1376 1377lemma pt_inject_on_ineq: 1378 fixes X :: "'y set" 1379 and pi :: "'x prm" 1380 assumes pt: "pt TYPE('y) TYPE('x)" 1381 and at: "at TYPE('x)" 1382 shows "inj_on (perm pi) X" 1383proof (unfold inj_on_def, intro strip) 1384 fix x::"'y" and y::"'y" 1385 assume "pi\<bullet>x = pi\<bullet>y" 1386 thus "x=y" by (simp add: pt_bij[OF pt, OF at]) 1387qed 1388 1389lemma pt_set_finite_ineq: 1390 fixes X :: "'x set" 1391 and pi :: "'y prm" 1392 assumes pt: "pt TYPE('x) TYPE('y)" 1393 and at: "at TYPE('y)" 1394 shows "finite (pi\<bullet>X) = finite X" 1395proof - 1396 have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def) 1397 show ?thesis 1398 proof (rule iffI) 1399 assume "finite (pi\<bullet>X)" 1400 hence "finite (perm pi ` X)" using image by (simp) 1401 thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD) 1402 next 1403 assume "finite X" 1404 hence "finite (perm pi ` X)" by (rule finite_imageI) 1405 thus "finite (pi\<bullet>X)" using image by (simp) 1406 qed 1407qed 1408 1409lemma pt_set_infinite_ineq: 1410 fixes X :: "'x set" 1411 and pi :: "'y prm" 1412 assumes pt: "pt TYPE('x) TYPE('y)" 1413 and at: "at TYPE('y)" 1414 shows "infinite (pi\<bullet>X) = infinite X" 1415using pt at by (simp add: pt_set_finite_ineq) 1416 1417lemma pt_perm_supp_ineq: 1418 fixes pi :: "'x prm" 1419 and x :: "'a" 1420 assumes pta: "pt TYPE('a) TYPE('x)" 1421 and ptb: "pt TYPE('y) TYPE('x)" 1422 and at: "at TYPE('x)" 1423 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 1424 shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS") 1425proof - 1426 have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def) 1427 also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}" 1428 proof (rule Collect_permI, rule allI, rule iffI) 1429 fix a 1430 assume "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}" 1431 hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at]) 1432 thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: perm_set_def) 1433 next 1434 fix a 1435 assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}" 1436 hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def) 1437 thus "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}" 1438 by (simp add: pt_set_infinite_ineq[OF ptb, OF at]) 1439 qed 1440 also have "\<dots> = {a. infinite {b::'y. [((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x \<noteq> x}}" 1441 by (simp add: pt_set_eq_ineq[OF ptb, OF at]) 1442 also have "\<dots> = {a. infinite {b. pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> (pi\<bullet>x)}}" 1443 by (simp add: pt_bij[OF pta, OF at]) 1444 also have "\<dots> = {a. infinite {b. [(a,b)]\<bullet>(pi\<bullet>x) \<noteq> (pi\<bullet>x)}}" 1445 proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong) 1446 fix a::"'y" and b::"'y" 1447 have "pi\<bullet>(([((rev pi)\<bullet>a,(rev pi)\<bullet>b)])\<bullet>x) = [(a,b)]\<bullet>(pi\<bullet>x)" 1448 by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at]) 1449 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 1450 qed 1451 finally show "?LHS = ?RHS" by (simp add: supp_def) 1452qed 1453 1454lemma pt_perm_supp: 1455 fixes pi :: "'x prm" 1456 and x :: "'a" 1457 assumes pt: "pt TYPE('a) TYPE('x)" 1458 and at: "at TYPE('x)" 1459 shows "(pi\<bullet>((supp x)::'x set)) = supp (pi\<bullet>x)" 1460apply(rule pt_perm_supp_ineq) 1461apply(rule pt) 1462apply(rule at_pt_inst) 1463apply(rule at)+ 1464apply(rule cp_pt_inst) 1465apply(rule pt) 1466apply(rule at) 1467done 1468 1469lemma pt_supp_finite_pi: 1470 fixes pi :: "'x prm" 1471 and x :: "'a" 1472 assumes pt: "pt TYPE('a) TYPE('x)" 1473 and at: "at TYPE('x)" 1474 and f: "finite ((supp x)::'x set)" 1475 shows "finite ((supp (pi\<bullet>x))::'x set)" 1476apply(simp add: pt_perm_supp[OF pt, OF at, symmetric]) 1477apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at]) 1478apply(rule f) 1479done 1480 1481lemma pt_fresh_left_ineq: 1482 fixes pi :: "'x prm" 1483 and x :: "'a" 1484 and a :: "'y" 1485 assumes pta: "pt TYPE('a) TYPE('x)" 1486 and ptb: "pt TYPE('y) TYPE('x)" 1487 and at: "at TYPE('x)" 1488 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 1489 shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x" 1490apply(simp add: fresh_def) 1491apply(simp add: pt_set_bij1[OF ptb, OF at]) 1492apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp]) 1493done 1494 1495lemma pt_fresh_right_ineq: 1496 fixes pi :: "'x prm" 1497 and x :: "'a" 1498 and a :: "'y" 1499 assumes pta: "pt TYPE('a) TYPE('x)" 1500 and ptb: "pt TYPE('y) TYPE('x)" 1501 and at: "at TYPE('x)" 1502 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 1503 shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)" 1504apply(simp add: fresh_def) 1505apply(simp add: pt_set_bij1[OF ptb, OF at]) 1506apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp]) 1507done 1508 1509lemma pt_fresh_bij_ineq: 1510 fixes pi :: "'x prm" 1511 and x :: "'a" 1512 and a :: "'y" 1513 assumes pta: "pt TYPE('a) TYPE('x)" 1514 and ptb: "pt TYPE('y) TYPE('x)" 1515 and at: "at TYPE('x)" 1516 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 1517 shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x" 1518apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) 1519apply(simp add: pt_rev_pi[OF ptb, OF at]) 1520done 1521 1522lemma pt_fresh_left: 1523 fixes pi :: "'x prm" 1524 and x :: "'a" 1525 and a :: "'x" 1526 assumes pt: "pt TYPE('a) TYPE('x)" 1527 and at: "at TYPE('x)" 1528 shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x" 1529apply(rule pt_fresh_left_ineq) 1530apply(rule pt) 1531apply(rule at_pt_inst) 1532apply(rule at)+ 1533apply(rule cp_pt_inst) 1534apply(rule pt) 1535apply(rule at) 1536done 1537 1538lemma pt_fresh_right: 1539 fixes pi :: "'x prm" 1540 and x :: "'a" 1541 and a :: "'x" 1542 assumes pt: "pt TYPE('a) TYPE('x)" 1543 and at: "at TYPE('x)" 1544 shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)" 1545apply(rule pt_fresh_right_ineq) 1546apply(rule pt) 1547apply(rule at_pt_inst) 1548apply(rule at)+ 1549apply(rule cp_pt_inst) 1550apply(rule pt) 1551apply(rule at) 1552done 1553 1554lemma pt_fresh_bij: 1555 fixes pi :: "'x prm" 1556 and x :: "'a" 1557 and a :: "'x" 1558 assumes pt: "pt TYPE('a) TYPE('x)" 1559 and at: "at TYPE('x)" 1560 shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x" 1561apply(rule pt_fresh_bij_ineq) 1562apply(rule pt) 1563apply(rule at_pt_inst) 1564apply(rule at)+ 1565apply(rule cp_pt_inst) 1566apply(rule pt) 1567apply(rule at) 1568done 1569 1570lemma pt_fresh_bij1: 1571 fixes pi :: "'x prm" 1572 and x :: "'a" 1573 and a :: "'x" 1574 assumes pt: "pt TYPE('a) TYPE('x)" 1575 and at: "at TYPE('x)" 1576 and a: "a\<sharp>x" 1577 shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)" 1578using a by (simp add: pt_fresh_bij[OF pt, OF at]) 1579 1580lemma pt_fresh_bij2: 1581 fixes pi :: "'x prm" 1582 and x :: "'a" 1583 and a :: "'x" 1584 assumes pt: "pt TYPE('a) TYPE('x)" 1585 and at: "at TYPE('x)" 1586 and a: "(pi\<bullet>a)\<sharp>(pi\<bullet>x)" 1587 shows "a\<sharp>x" 1588using a by (simp add: pt_fresh_bij[OF pt, OF at]) 1589 1590lemma pt_fresh_eqvt: 1591 fixes pi :: "'x prm" 1592 and x :: "'a" 1593 and a :: "'x" 1594 assumes pt: "pt TYPE('a) TYPE('x)" 1595 and at: "at TYPE('x)" 1596 shows "pi\<bullet>(a\<sharp>x) = (pi\<bullet>a)\<sharp>(pi\<bullet>x)" 1597 by (simp add: perm_bool pt_fresh_bij[OF pt, OF at]) 1598 1599lemma pt_perm_fresh1: 1600 fixes a :: "'x" 1601 and b :: "'x" 1602 and x :: "'a" 1603 assumes pt: "pt TYPE('a) TYPE('x)" 1604 and at: "at TYPE ('x)" 1605 and a1: "\<not>(a\<sharp>x)" 1606 and a2: "b\<sharp>x" 1607 shows "[(a,b)]\<bullet>x \<noteq> x" 1608proof 1609 assume neg: "[(a,b)]\<bullet>x = x" 1610 from a1 have a1':"a\<in>(supp x)" by (simp add: fresh_def) 1611 from a2 have a2':"b\<notin>(supp x)" by (simp add: fresh_def) 1612 from a1' a2' have a3: "a\<noteq>b" by force 1613 from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))" 1614 by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at]) 1615 hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_calc[OF at]) 1616 hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at]) 1617 with a2' neg show False by simp 1618qed 1619 1620(* the next two lemmas are needed in the proof *) 1621(* of the structural induction principle *) 1622lemma pt_fresh_aux: 1623 fixes a::"'x" 1624 and b::"'x" 1625 and c::"'x" 1626 and x::"'a" 1627 assumes pt: "pt TYPE('a) TYPE('x)" 1628 and at: "at TYPE ('x)" 1629 assumes a1: "c\<noteq>a" and a2: "a\<sharp>x" and a3: "c\<sharp>x" 1630 shows "c\<sharp>([(a,b)]\<bullet>x)" 1631using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at]) 1632 1633lemma pt_fresh_perm_app: 1634 fixes pi :: "'x prm" 1635 and a :: "'x" 1636 and x :: "'y" 1637 assumes pt: "pt TYPE('y) TYPE('x)" 1638 and at: "at TYPE('x)" 1639 and h1: "a\<sharp>pi" 1640 and h2: "a\<sharp>x" 1641 shows "a\<sharp>(pi\<bullet>x)" 1642using assms 1643proof - 1644 have "a\<sharp>(rev pi)"using h1 by (simp add: fresh_list_rev) 1645 then have "(rev pi)\<bullet>a = a" by (simp add: at_prm_fresh[OF at]) 1646 then have "((rev pi)\<bullet>a)\<sharp>x" using h2 by simp 1647 thus "a\<sharp>(pi\<bullet>x)" by (simp add: pt_fresh_right[OF pt, OF at]) 1648qed 1649 1650lemma pt_fresh_perm_app_ineq: 1651 fixes pi::"'x prm" 1652 and c::"'y" 1653 and x::"'a" 1654 assumes pta: "pt TYPE('a) TYPE('x)" 1655 and ptb: "pt TYPE('y) TYPE('x)" 1656 and at: "at TYPE('x)" 1657 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 1658 and dj: "disjoint TYPE('y) TYPE('x)" 1659 assumes a: "c\<sharp>x" 1660 shows "c\<sharp>(pi\<bullet>x)" 1661using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj]) 1662 1663lemma pt_fresh_eqvt_ineq: 1664 fixes pi::"'x prm" 1665 and c::"'y" 1666 and x::"'a" 1667 assumes pta: "pt TYPE('a) TYPE('x)" 1668 and ptb: "pt TYPE('y) TYPE('x)" 1669 and at: "at TYPE('x)" 1670 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 1671 and dj: "disjoint TYPE('y) TYPE('x)" 1672 shows "pi\<bullet>(c\<sharp>x) = (pi\<bullet>c)\<sharp>(pi\<bullet>x)" 1673by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool) 1674 1675\<comment> \<open>the co-set of a finite set is infinte\<close> 1676lemma finite_infinite: 1677 assumes a: "finite {b::'x. P b}" 1678 and b: "infinite (UNIV::'x set)" 1679 shows "infinite {b. \<not>P b}" 1680proof - 1681 from a b have "infinite (UNIV - {b::'x. P b})" by (simp add: Diff_infinite_finite) 1682 moreover 1683 have "{b::'x. \<not>P b} = UNIV - {b::'x. P b}" by auto 1684 ultimately show "infinite {b::'x. \<not>P b}" by simp 1685qed 1686 1687lemma pt_fresh_fresh: 1688 fixes x :: "'a" 1689 and a :: "'x" 1690 and b :: "'x" 1691 assumes pt: "pt TYPE('a) TYPE('x)" 1692 and at: "at TYPE ('x)" 1693 and a1: "a\<sharp>x" and a2: "b\<sharp>x" 1694 shows "[(a,b)]\<bullet>x=x" 1695proof (cases "a=b") 1696 assume "a=b" 1697 hence "[(a,b)] \<triangleq> []" by (simp add: at_ds1[OF at]) 1698 hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt]) 1699 thus ?thesis by (simp only: pt1[OF pt]) 1700next 1701 assume c2: "a\<noteq>b" 1702 from a1 have f1: "finite {c. [(a,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def) 1703 from a2 have f2: "finite {c. [(b,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def) 1704 from f1 and f2 have f3: "finite {c. perm [(a,c)] x \<noteq> x \<or> perm [(b,c)] x \<noteq> x}" 1705 by (force simp only: Collect_disj_eq) 1706 have "infinite {c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}" 1707 by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified]) 1708 hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" 1709 by (force dest: Diff_infinite_finite) 1710 hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}" 1711 by (metis finite_set set_empty2) 1712 hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force) 1713 then obtain c 1714 where eq1: "[(a,c)]\<bullet>x = x" 1715 and eq2: "[(b,c)]\<bullet>x = x" 1716 and ineq: "a\<noteq>c \<and> b\<noteq>c" 1717 by (force) 1718 hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>x)) = x" by simp 1719 hence eq3: "[(a,c),(b,c),(a,c)]\<bullet>x = x" by (simp add: pt2[OF pt,symmetric]) 1720 from c2 ineq have "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" by (simp add: at_ds3[OF at]) 1721 hence "[(a,c),(b,c),(a,c)]\<bullet>x = [(a,b)]\<bullet>x" by (rule pt3[OF pt]) 1722 thus ?thesis using eq3 by simp 1723qed 1724 1725lemma pt_pi_fresh_fresh: 1726 fixes x :: "'a" 1727 and pi :: "'x prm" 1728 assumes pt: "pt TYPE('a) TYPE('x)" 1729 and at: "at TYPE ('x)" 1730 and a: "\<forall>(a,b)\<in>set pi. a\<sharp>x \<and> b\<sharp>x" 1731 shows "pi\<bullet>x=x" 1732using a 1733proof (induct pi) 1734 case Nil 1735 show "([]::'x prm)\<bullet>x = x" by (rule pt1[OF pt]) 1736next 1737 case (Cons ab pi) 1738 have a: "\<forall>(a,b)\<in>set (ab#pi). a\<sharp>x \<and> b\<sharp>x" by fact 1739 have ih: "(\<forall>(a,b)\<in>set pi. a\<sharp>x \<and> b\<sharp>x) \<Longrightarrow> pi\<bullet>x=x" by fact 1740 obtain a b where e: "ab=(a,b)" by (cases ab) (auto) 1741 from a have a': "a\<sharp>x" "b\<sharp>x" using e by auto 1742 have "(ab#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x" using e by simp 1743 also have "\<dots> = [(a,b)]\<bullet>(pi\<bullet>x)" by (simp only: pt2[OF pt]) 1744 also have "\<dots> = [(a,b)]\<bullet>x" using ih a by simp 1745 also have "\<dots> = x" using a' by (simp add: pt_fresh_fresh[OF pt, OF at]) 1746 finally show "(ab#pi)\<bullet>x = x" by simp 1747qed 1748 1749lemma pt_perm_compose: 1750 fixes pi1 :: "'x prm" 1751 and pi2 :: "'x prm" 1752 and x :: "'a" 1753 assumes pt: "pt TYPE('a) TYPE('x)" 1754 and at: "at TYPE('x)" 1755 shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)" 1756proof - 1757 have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8 [OF at]) 1758 hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt]) 1759 thus ?thesis by (simp add: pt2[OF pt]) 1760qed 1761 1762lemma pt_perm_compose': 1763 fixes pi1 :: "'x prm" 1764 and pi2 :: "'x prm" 1765 and x :: "'a" 1766 assumes pt: "pt TYPE('a) TYPE('x)" 1767 and at: "at TYPE('x)" 1768 shows "(pi2\<bullet>pi1)\<bullet>x = pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x))" 1769proof - 1770 have "pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x)) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>((rev pi2)\<bullet>x))" 1771 by (rule pt_perm_compose[OF pt, OF at]) 1772 also have "\<dots> = (pi2\<bullet>pi1)\<bullet>x" by (simp add: pt_pi_rev[OF pt, OF at]) 1773 finally have "pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x)) = (pi2\<bullet>pi1)\<bullet>x" by simp 1774 thus ?thesis by simp 1775qed 1776 1777lemma pt_perm_compose_rev: 1778 fixes pi1 :: "'x prm" 1779 and pi2 :: "'x prm" 1780 and x :: "'a" 1781 assumes pt: "pt TYPE('a) TYPE('x)" 1782 and at: "at TYPE('x)" 1783 shows "(rev pi2)\<bullet>((rev pi1)\<bullet>x) = (rev pi1)\<bullet>(rev (pi1\<bullet>pi2)\<bullet>x)" 1784proof - 1785 have "((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at]) 1786 hence "((rev pi2)@(rev pi1))\<bullet>x = ((rev pi1)@(rev (pi1\<bullet>pi2)))\<bullet>x" by (rule pt3[OF pt]) 1787 thus ?thesis by (simp add: pt2[OF pt]) 1788qed 1789 1790section \<open>equivariance for some connectives\<close> 1791lemma pt_all_eqvt: 1792 fixes pi :: "'x prm" 1793 and x :: "'a" 1794 assumes pt: "pt TYPE('a) TYPE('x)" 1795 and at: "at TYPE('x)" 1796 shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))" 1797apply(auto simp add: perm_bool perm_fun_def) 1798apply(drule_tac x="pi\<bullet>x" in spec) 1799apply(simp add: pt_rev_pi[OF pt, OF at]) 1800done 1801 1802lemma pt_ex_eqvt: 1803 fixes pi :: "'x prm" 1804 and x :: "'a" 1805 assumes pt: "pt TYPE('a) TYPE('x)" 1806 and at: "at TYPE('x)" 1807 shows "pi\<bullet>(\<exists>(x::'a). P x) = (\<exists>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))" 1808apply(auto simp add: perm_bool perm_fun_def) 1809apply(rule_tac x="pi\<bullet>x" in exI) 1810apply(simp add: pt_rev_pi[OF pt, OF at]) 1811done 1812 1813lemma pt_ex1_eqvt: 1814 fixes pi :: "'x prm" 1815 and x :: "'a" 1816 assumes pt: "pt TYPE('a) TYPE('x)" 1817 and at: "at TYPE('x)" 1818 shows "(pi\<bullet>(\<exists>!x. P (x::'a))) = (\<exists>!x. pi\<bullet>(P (rev pi\<bullet>x)))" 1819unfolding Ex1_def 1820by (simp add: pt_ex_eqvt[OF pt at] conj_eqvt pt_all_eqvt[OF pt at] 1821 imp_eqvt pt_eq_eqvt[OF pt at] pt_pi_rev[OF pt at]) 1822 1823lemma pt_the_eqvt: 1824 fixes pi :: "'x prm" 1825 assumes pt: "pt TYPE('a) TYPE('x)" 1826 and at: "at TYPE('x)" 1827 and unique: "\<exists>!x. P x" 1828 shows "pi\<bullet>(THE(x::'a). P x) = (THE(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))" 1829 apply(rule the1_equality [symmetric]) 1830 apply(simp add: pt_ex1_eqvt[OF pt at,symmetric]) 1831 apply(simp add: perm_bool unique) 1832 apply(simp add: perm_bool pt_rev_pi [OF pt at]) 1833 apply(rule theI'[OF unique]) 1834 done 1835 1836section \<open>facts about supports\<close> 1837(*==============================*) 1838 1839lemma supports_subset: 1840 fixes x :: "'a" 1841 and S1 :: "'x set" 1842 and S2 :: "'x set" 1843 assumes a: "S1 supports x" 1844 and b: "S1 \<subseteq> S2" 1845 shows "S2 supports x" 1846 using a b 1847 by (force simp add: supports_def) 1848 1849lemma supp_is_subset: 1850 fixes S :: "'x set" 1851 and x :: "'a" 1852 assumes a1: "S supports x" 1853 and a2: "finite S" 1854 shows "(supp x)\<subseteq>S" 1855proof (rule ccontr) 1856 assume "\<not>(supp x \<subseteq> S)" 1857 hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force 1858 then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force 1859 from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold supports_def, force) 1860 hence "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by force 1861 with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset) 1862 hence "a\<notin>(supp x)" by (unfold supp_def, auto) 1863 with b1 show False by simp 1864qed 1865 1866lemma supp_supports: 1867 fixes x :: "'a" 1868 assumes pt: "pt TYPE('a) TYPE('x)" 1869 and at: "at TYPE ('x)" 1870 shows "((supp x)::'x set) supports x" 1871proof (unfold supports_def, intro strip) 1872 fix a b 1873 assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)" 1874 hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def) 1875 thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at]) 1876qed 1877 1878lemma supports_finite: 1879 fixes S :: "'x set" 1880 and x :: "'a" 1881 assumes a1: "S supports x" 1882 and a2: "finite S" 1883 shows "finite ((supp x)::'x set)" 1884proof - 1885 have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset) 1886 thus ?thesis using a2 by (simp add: finite_subset) 1887qed 1888 1889lemma supp_is_inter: 1890 fixes x :: "'a" 1891 assumes pt: "pt TYPE('a) TYPE('x)" 1892 and at: "at TYPE ('x)" 1893 and fs: "fs TYPE('a) TYPE('x)" 1894 shows "((supp x)::'x set) = (\<Inter>{S. finite S \<and> S supports x})" 1895proof (rule equalityI) 1896 show "((supp x)::'x set) \<subseteq> (\<Inter>{S. finite S \<and> S supports x})" 1897 proof (clarify) 1898 fix S c 1899 assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x" 1900 hence "((supp x)::'x set)\<subseteq>S" by (simp add: supp_is_subset) 1901 with b show "c\<in>S" by force 1902 qed 1903next 1904 show "(\<Inter>{S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)" 1905 proof (clarify, simp) 1906 fix c 1907 assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S" 1908 have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at]) 1909 with d fs1[OF fs] show "c\<in>supp x" by force 1910 qed 1911qed 1912 1913lemma supp_is_least_supports: 1914 fixes S :: "'x set" 1915 and x :: "'a" 1916 assumes pt: "pt TYPE('a) TYPE('x)" 1917 and at: "at TYPE ('x)" 1918 and a1: "S supports x" 1919 and a2: "finite S" 1920 and a3: "\<forall>S'. (S' supports x) \<longrightarrow> S\<subseteq>S'" 1921 shows "S = (supp x)" 1922proof (rule equalityI) 1923 show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset) 1924next 1925 have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at]) 1926 with a3 show "S\<subseteq>supp x" by force 1927qed 1928 1929lemma supports_set: 1930 fixes S :: "'x set" 1931 and X :: "'a set" 1932 assumes pt: "pt TYPE('a) TYPE('x)" 1933 and at: "at TYPE ('x)" 1934 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)" 1935 shows "S supports X" 1936using a 1937apply(auto simp add: supports_def) 1938apply(simp add: pt_set_bij1a[OF pt, OF at]) 1939apply(force simp add: pt_swap_bij[OF pt, OF at]) 1940apply(simp add: pt_set_bij1a[OF pt, OF at]) 1941done 1942 1943lemma supports_fresh: 1944 fixes S :: "'x set" 1945 and a :: "'x" 1946 and x :: "'a" 1947 assumes a1: "S supports x" 1948 and a2: "finite S" 1949 and a3: "a\<notin>S" 1950 shows "a\<sharp>x" 1951proof (simp add: fresh_def) 1952 have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset) 1953 thus "a\<notin>(supp x)" using a3 by force 1954qed 1955 1956lemma at_fin_set_supports: 1957 fixes X::"'x set" 1958 assumes at: "at TYPE('x)" 1959 shows "X supports X" 1960proof - 1961 have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X" 1962 by (auto simp add: perm_set_def at_calc[OF at]) 1963 then show ?thesis by (simp add: supports_def) 1964qed 1965 1966lemma infinite_Collection: 1967 assumes a1:"infinite X" 1968 and a2:"\<forall>b\<in>X. P(b)" 1969 shows "infinite {b\<in>X. P(b)}" 1970 using a1 a2 1971 apply auto 1972 apply (subgoal_tac "infinite (X - {b\<in>X. P b})") 1973 apply (simp add: set_diff_eq) 1974 apply (simp add: Diff_infinite_finite) 1975 done 1976 1977lemma at_fin_set_supp: 1978 fixes X::"'x set" 1979 assumes at: "at TYPE('x)" 1980 and fs: "finite X" 1981 shows "(supp X) = X" 1982proof (rule subset_antisym) 1983 show "(supp X) \<subseteq> X" using at_fin_set_supports[OF at] using fs by (simp add: supp_is_subset) 1984next 1985 have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite) 1986 { fix a::"'x" 1987 assume asm: "a\<in>X" 1988 hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X" 1989 by (auto simp add: perm_set_def at_calc[OF at]) 1990 with inf have "infinite {b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X}" by (rule infinite_Collection) 1991 hence "infinite {b. [(a,b)]\<bullet>X\<noteq>X}" by (rule_tac infinite_super, auto) 1992 hence "a\<in>(supp X)" by (simp add: supp_def) 1993 } 1994 then show "X\<subseteq>(supp X)" by blast 1995qed 1996 1997lemma at_fin_set_fresh: 1998 fixes X::"'x set" 1999 assumes at: "at TYPE('x)" 2000 and fs: "finite X" 2001 shows "(x \<sharp> X) = (x \<notin> X)" 2002 by (simp add: at_fin_set_supp fresh_def at fs) 2003 2004 2005section \<open>Permutations acting on Functions\<close> 2006(*==========================================*) 2007 2008lemma pt_fun_app_eq: 2009 fixes f :: "'a\<Rightarrow>'b" 2010 and x :: "'a" 2011 and pi :: "'x prm" 2012 assumes pt: "pt TYPE('a) TYPE('x)" 2013 and at: "at TYPE('x)" 2014 shows "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" 2015 by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at]) 2016 2017 2018\<comment> \<open>sometimes pt_fun_app_eq does too much; this lemma 'corrects it'\<close> 2019lemma pt_perm: 2020 fixes x :: "'a" 2021 and pi1 :: "'x prm" 2022 and pi2 :: "'x prm" 2023 assumes pt: "pt TYPE('a) TYPE('x)" 2024 and at: "at TYPE ('x)" 2025 shows "(pi1\<bullet>perm pi2)(pi1\<bullet>x) = pi1\<bullet>(pi2\<bullet>x)" 2026 by (simp add: pt_fun_app_eq[OF pt, OF at]) 2027 2028 2029lemma pt_fun_eq: 2030 fixes f :: "'a\<Rightarrow>'b" 2031 and pi :: "'x prm" 2032 assumes pt: "pt TYPE('a) TYPE('x)" 2033 and at: "at TYPE('x)" 2034 shows "(pi\<bullet>f = f) = (\<forall> x. pi\<bullet>(f x) = f (pi\<bullet>x))" (is "?LHS = ?RHS") 2035proof 2036 assume a: "?LHS" 2037 show "?RHS" 2038 proof 2039 fix x 2040 have "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pt, OF at]) 2041 also have "\<dots> = f (pi\<bullet>x)" using a by simp 2042 finally show "pi\<bullet>(f x) = f (pi\<bullet>x)" by simp 2043 qed 2044next 2045 assume b: "?RHS" 2046 show "?LHS" 2047 proof (rule ccontr) 2048 assume "(pi\<bullet>f) \<noteq> f" 2049 hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: fun_eq_iff) 2050 then obtain x where b1: "(pi\<bullet>f) x \<noteq> f x" by force 2051 from b have "pi\<bullet>(f ((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" by force 2052 hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" 2053 by (simp add: pt_fun_app_eq[OF pt, OF at]) 2054 hence "(pi\<bullet>f) x = f x" by (simp add: pt_pi_rev[OF pt, OF at]) 2055 with b1 show "False" by simp 2056 qed 2057qed 2058 2059\<comment> \<open>two helper lemmas for the equivariance of functions\<close> 2060lemma pt_swap_eq_aux: 2061 fixes y :: "'a" 2062 and pi :: "'x prm" 2063 assumes pt: "pt TYPE('a) TYPE('x)" 2064 and a: "\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y" 2065 shows "pi\<bullet>y = y" 2066proof(induct pi) 2067 case Nil show ?case by (simp add: pt1[OF pt]) 2068next 2069 case (Cons x xs) 2070 have ih: "xs\<bullet>y = y" by fact 2071 obtain a b where p: "x=(a,b)" by force 2072 have "((a,b)#xs)\<bullet>y = ([(a,b)]@xs)\<bullet>y" by simp 2073 also have "\<dots> = [(a,b)]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt]) 2074 finally show ?case using a ih p by simp 2075qed 2076 2077lemma pt_swap_eq: 2078 fixes y :: "'a" 2079 assumes pt: "pt TYPE('a) TYPE('x)" 2080 shows "(\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y) = (\<forall>pi::'x prm. pi\<bullet>y = y)" 2081 by (force intro: pt_swap_eq_aux[OF pt]) 2082 2083lemma pt_eqvt_fun1a: 2084 fixes f :: "'a\<Rightarrow>'b" 2085 assumes pta: "pt TYPE('a) TYPE('x)" 2086 and ptb: "pt TYPE('b) TYPE('x)" 2087 and at: "at TYPE('x)" 2088 and a: "((supp f)::'x set)={}" 2089 shows "\<forall>(pi::'x prm). pi\<bullet>f = f" 2090proof (intro strip) 2091 fix pi 2092 have "\<forall>a b. a\<notin>((supp f)::'x set) \<and> b\<notin>((supp f)::'x set) \<longrightarrow> (([(a,b)]\<bullet>f) = f)" 2093 by (intro strip, fold fresh_def, 2094 simp add: pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at],OF at]) 2095 with a have "\<forall>(a::'x) (b::'x). ([(a,b)]\<bullet>f) = f" by force 2096 hence "\<forall>(pi::'x prm). pi\<bullet>f = f" 2097 by (simp add: pt_swap_eq[OF pt_fun_inst[OF pta, OF ptb, OF at]]) 2098 thus "(pi::'x prm)\<bullet>f = f" by simp 2099qed 2100 2101lemma pt_eqvt_fun1b: 2102 fixes f :: "'a\<Rightarrow>'b" 2103 assumes a: "\<forall>(pi::'x prm). pi\<bullet>f = f" 2104 shows "((supp f)::'x set)={}" 2105using a by (simp add: supp_def) 2106 2107lemma pt_eqvt_fun1: 2108 fixes f :: "'a\<Rightarrow>'b" 2109 assumes pta: "pt TYPE('a) TYPE('x)" 2110 and ptb: "pt TYPE('b) TYPE('x)" 2111 and at: "at TYPE('x)" 2112 shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm). pi\<bullet>f = f)" (is "?LHS = ?RHS") 2113by (rule iffI, simp add: pt_eqvt_fun1a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun1b) 2114 2115lemma pt_eqvt_fun2a: 2116 fixes f :: "'a\<Rightarrow>'b" 2117 assumes pta: "pt TYPE('a) TYPE('x)" 2118 and ptb: "pt TYPE('b) TYPE('x)" 2119 and at: "at TYPE('x)" 2120 assumes a: "((supp f)::'x set)={}" 2121 shows "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)" 2122proof (intro strip) 2123 fix pi x 2124 from a have b: "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_eqvt_fun1[OF pta, OF ptb, OF at]) 2125 have "(pi::'x prm)\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pta, OF at]) 2126 with b show "(pi::'x prm)\<bullet>(f x) = f (pi\<bullet>x)" by force 2127qed 2128 2129lemma pt_eqvt_fun2b: 2130 fixes f :: "'a\<Rightarrow>'b" 2131 assumes pt1: "pt TYPE('a) TYPE('x)" 2132 and pt2: "pt TYPE('b) TYPE('x)" 2133 and at: "at TYPE('x)" 2134 assumes a: "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)" 2135 shows "((supp f)::'x set)={}" 2136proof - 2137 from a have "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_fun_eq[OF pt1, OF at, symmetric]) 2138 thus ?thesis by (simp add: supp_def) 2139qed 2140 2141lemma pt_eqvt_fun2: 2142 fixes f :: "'a\<Rightarrow>'b" 2143 assumes pta: "pt TYPE('a) TYPE('x)" 2144 and ptb: "pt TYPE('b) TYPE('x)" 2145 and at: "at TYPE('x)" 2146 shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x))" 2147by (rule iffI, 2148 simp add: pt_eqvt_fun2a[OF pta, OF ptb, OF at], 2149 simp add: pt_eqvt_fun2b[OF pta, OF ptb, OF at]) 2150 2151lemma pt_supp_fun_subset: 2152 fixes f :: "'a\<Rightarrow>'b" 2153 assumes pta: "pt TYPE('a) TYPE('x)" 2154 and ptb: "pt TYPE('b) TYPE('x)" 2155 and at: "at TYPE('x)" 2156 and f1: "finite ((supp f)::'x set)" 2157 and f2: "finite ((supp x)::'x set)" 2158 shows "supp (f x) \<subseteq> (((supp f)\<union>(supp x))::'x set)" 2159proof - 2160 have s1: "((supp f)\<union>((supp x)::'x set)) supports (f x)" 2161 proof (simp add: supports_def, fold fresh_def, auto) 2162 fix a::"'x" and b::"'x" 2163 assume "a\<sharp>f" and "b\<sharp>f" 2164 hence a1: "[(a,b)]\<bullet>f = f" 2165 by (rule pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at], OF at]) 2166 assume "a\<sharp>x" and "b\<sharp>x" 2167 hence a2: "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pta, OF at]) 2168 from a1 a2 show "[(a,b)]\<bullet>(f x) = (f x)" by (simp add: pt_fun_app_eq[OF pta, OF at]) 2169 qed 2170 from f1 f2 have "finite ((supp f)\<union>((supp x)::'x set))" by force 2171 with s1 show ?thesis by (rule supp_is_subset) 2172qed 2173 2174lemma pt_empty_supp_fun_subset: 2175 fixes f :: "'a\<Rightarrow>'b" 2176 assumes pta: "pt TYPE('a) TYPE('x)" 2177 and ptb: "pt TYPE('b) TYPE('x)" 2178 and at: "at TYPE('x)" 2179 and e: "(supp f)=({}::'x set)" 2180 shows "supp (f x) \<subseteq> ((supp x)::'x set)" 2181proof (unfold supp_def, auto) 2182 fix a::"'x" 2183 assume a1: "finite {b. [(a, b)]\<bullet>x \<noteq> x}" 2184 assume "infinite {b. [(a, b)]\<bullet>(f x) \<noteq> f x}" 2185 hence a2: "infinite {b. f ([(a, b)]\<bullet>x) \<noteq> f x}" using e 2186 by (simp add: pt_eqvt_fun2[OF pta, OF ptb, OF at]) 2187 have a3: "{b. f ([(a,b)]\<bullet>x) \<noteq> f x}\<subseteq>{b. [(a,b)]\<bullet>x \<noteq> x}" by force 2188 from a1 a2 a3 show False by (force dest: finite_subset) 2189qed 2190 2191section \<open>Facts about the support of finite sets of finitely supported things\<close> 2192(*=============================================================================*) 2193 2194definition X_to_Un_supp :: "('a set) \<Rightarrow> 'x set" where 2195 "X_to_Un_supp X \<equiv> \<Union>x\<in>X. ((supp x)::'x set)" 2196 2197lemma UNION_f_eqvt: 2198 fixes X::"('a set)" 2199 and f::"'a \<Rightarrow> 'x set" 2200 and pi::"'x prm" 2201 assumes pt: "pt TYPE('a) TYPE('x)" 2202 and at: "at TYPE('x)" 2203 shows "pi\<bullet>(\<Union>x\<in>X. f x) = (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)" 2204proof - 2205 have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at) 2206 show ?thesis 2207 proof (rule equalityI) 2208 show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)" 2209 apply(auto simp add: perm_set_def) 2210 apply(rule_tac x="pi\<bullet>xb" in exI) 2211 apply(rule conjI) 2212 apply(rule_tac x="xb" in exI) 2213 apply(simp) 2214 apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xb) = pi\<bullet>(f xb)")(*A*) 2215 apply(simp) 2216 apply(rule pt_set_bij2[OF pt_x, OF at]) 2217 apply(assumption) 2218 (*A*) 2219 apply(rule sym) 2220 apply(rule pt_fun_app_eq[OF pt, OF at]) 2221 done 2222 next 2223 show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)" 2224 apply(auto simp add: perm_set_def) 2225 apply(rule_tac x="(rev pi)\<bullet>x" in exI) 2226 apply(rule conjI) 2227 apply(simp add: pt_pi_rev[OF pt_x, OF at]) 2228 apply(rule_tac x="xb" in bexI) 2229 apply(simp add: pt_set_bij1[OF pt_x, OF at]) 2230 apply(simp add: pt_fun_app_eq[OF pt, OF at]) 2231 apply(assumption) 2232 done 2233 qed 2234qed 2235 2236lemma X_to_Un_supp_eqvt: 2237 fixes X::"('a set)" 2238 and pi::"'x prm" 2239 assumes pt: "pt TYPE('a) TYPE('x)" 2240 and at: "at TYPE('x)" 2241 shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)" 2242 apply(simp add: X_to_Un_supp_def) 2243 apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def) 2244 apply(simp add: pt_perm_supp[OF pt, OF at]) 2245 apply(simp add: pt_pi_rev[OF pt, OF at]) 2246 done 2247 2248lemma Union_supports_set: 2249 fixes X::"('a set)" 2250 assumes pt: "pt TYPE('a) TYPE('x)" 2251 and at: "at TYPE('x)" 2252 shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X" 2253 apply(simp add: supports_def fresh_def[symmetric]) 2254 apply(rule allI)+ 2255 apply(rule impI) 2256 apply(erule conjE) 2257 apply(simp add: perm_set_def) 2258 apply(auto) 2259 apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*) 2260 apply(simp) 2261 apply(rule pt_fresh_fresh[OF pt, OF at]) 2262 apply(force) 2263 apply(force) 2264 apply(rule_tac x="x" in exI) 2265 apply(simp) 2266 apply(rule sym) 2267 apply(rule pt_fresh_fresh[OF pt, OF at]) 2268 apply(force)+ 2269 done 2270 2271lemma Union_of_fin_supp_sets: 2272 fixes X::"('a set)" 2273 assumes fs: "fs TYPE('a) TYPE('x)" 2274 and fi: "finite X" 2275 shows "finite (\<Union>x\<in>X. ((supp x)::'x set))" 2276using fi by (induct, auto simp add: fs1[OF fs]) 2277 2278lemma Union_included_in_supp: 2279 fixes X::"('a set)" 2280 assumes pt: "pt TYPE('a) TYPE('x)" 2281 and at: "at TYPE('x)" 2282 and fs: "fs TYPE('a) TYPE('x)" 2283 and fi: "finite X" 2284 shows "(\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> supp X" 2285proof - 2286 have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)" 2287 apply(rule pt_empty_supp_fun_subset) 2288 apply(force intro: pt_set_inst at_pt_inst pt at)+ 2289 apply(rule pt_eqvt_fun2b) 2290 apply(force intro: pt_set_inst at_pt_inst pt at)+ 2291 apply(rule allI)+ 2292 apply(rule X_to_Un_supp_eqvt[OF pt, OF at]) 2293 done 2294 hence "supp (\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> ((supp X)::'x set)" by (simp add: X_to_Un_supp_def) 2295 moreover 2296 have "supp (\<Union>x\<in>X. ((supp x)::'x set)) = (\<Union>x\<in>X. ((supp x)::'x set))" 2297 apply(rule at_fin_set_supp[OF at]) 2298 apply(rule Union_of_fin_supp_sets[OF fs, OF fi]) 2299 done 2300 ultimately show ?thesis by force 2301qed 2302 2303lemma supp_of_fin_sets: 2304 fixes X::"('a set)" 2305 assumes pt: "pt TYPE('a) TYPE('x)" 2306 and at: "at TYPE('x)" 2307 and fs: "fs TYPE('a) TYPE('x)" 2308 and fi: "finite X" 2309 shows "(supp X) = (\<Union>x\<in>X. ((supp x)::'x set))" 2310apply(rule equalityI) 2311apply(rule supp_is_subset) 2312apply(rule Union_supports_set[OF pt, OF at]) 2313apply(rule Union_of_fin_supp_sets[OF fs, OF fi]) 2314apply(rule Union_included_in_supp[OF pt, OF at, OF fs, OF fi]) 2315done 2316 2317lemma supp_fin_union: 2318 fixes X::"('a set)" 2319 and Y::"('a set)" 2320 assumes pt: "pt TYPE('a) TYPE('x)" 2321 and at: "at TYPE('x)" 2322 and fs: "fs TYPE('a) TYPE('x)" 2323 and f1: "finite X" 2324 and f2: "finite Y" 2325 shows "(supp (X\<union>Y)) = (supp X)\<union>((supp Y)::'x set)" 2326using f1 f2 by (force simp add: supp_of_fin_sets[OF pt, OF at, OF fs]) 2327 2328lemma supp_fin_insert: 2329 fixes X::"('a set)" 2330 and x::"'a" 2331 assumes pt: "pt TYPE('a) TYPE('x)" 2332 and at: "at TYPE('x)" 2333 and fs: "fs TYPE('a) TYPE('x)" 2334 and f: "finite X" 2335 shows "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)" 2336proof - 2337 have "(supp (insert x X)) = ((supp ({x}\<union>(X::'a set)))::'x set)" by simp 2338 also have "\<dots> = (supp {x})\<union>(supp X)" 2339 by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f) 2340 finally show "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)" 2341 by (simp add: supp_singleton) 2342qed 2343 2344lemma fresh_fin_union: 2345 fixes X::"('a set)" 2346 and Y::"('a set)" 2347 and a::"'x" 2348 assumes pt: "pt TYPE('a) TYPE('x)" 2349 and at: "at TYPE('x)" 2350 and fs: "fs TYPE('a) TYPE('x)" 2351 and f1: "finite X" 2352 and f2: "finite Y" 2353 shows "a\<sharp>(X\<union>Y) = (a\<sharp>X \<and> a\<sharp>Y)" 2354apply(simp add: fresh_def) 2355apply(simp add: supp_fin_union[OF pt, OF at, OF fs, OF f1, OF f2]) 2356done 2357 2358lemma fresh_fin_insert: 2359 fixes X::"('a set)" 2360 and x::"'a" 2361 and a::"'x" 2362 assumes pt: "pt TYPE('a) TYPE('x)" 2363 and at: "at TYPE('x)" 2364 and fs: "fs TYPE('a) TYPE('x)" 2365 and f: "finite X" 2366 shows "a\<sharp>(insert x X) = (a\<sharp>x \<and> a\<sharp>X)" 2367apply(simp add: fresh_def) 2368apply(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF f]) 2369done 2370 2371lemma fresh_fin_insert1: 2372 fixes X::"('a set)" 2373 and x::"'a" 2374 and a::"'x" 2375 assumes pt: "pt TYPE('a) TYPE('x)" 2376 and at: "at TYPE('x)" 2377 and fs: "fs TYPE('a) TYPE('x)" 2378 and f: "finite X" 2379 and a1: "a\<sharp>x" 2380 and a2: "a\<sharp>X" 2381 shows "a\<sharp>(insert x X)" 2382 using a1 a2 2383 by (simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f]) 2384 2385lemma pt_list_set_supp: 2386 fixes xs :: "'a list" 2387 assumes pt: "pt TYPE('a) TYPE('x)" 2388 and at: "at TYPE('x)" 2389 and fs: "fs TYPE('a) TYPE('x)" 2390 shows "supp (set xs) = ((supp xs)::'x set)" 2391proof - 2392 have "supp (set xs) = (\<Union>x\<in>(set xs). ((supp x)::'x set))" 2393 by (rule supp_of_fin_sets[OF pt, OF at, OF fs], rule finite_set) 2394 also have "(\<Union>x\<in>(set xs). ((supp x)::'x set)) = (supp xs)" 2395 proof(induct xs) 2396 case Nil show ?case by (simp add: supp_list_nil) 2397 next 2398 case (Cons h t) thus ?case by (simp add: supp_list_cons) 2399 qed 2400 finally show ?thesis by simp 2401qed 2402 2403lemma pt_list_set_fresh: 2404 fixes a :: "'x" 2405 and xs :: "'a list" 2406 assumes pt: "pt TYPE('a) TYPE('x)" 2407 and at: "at TYPE('x)" 2408 and fs: "fs TYPE('a) TYPE('x)" 2409 shows "a\<sharp>(set xs) = a\<sharp>xs" 2410by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs]) 2411 2412 2413section \<open>generalisation of freshness to lists and sets of atoms\<close> 2414(*================================================================*) 2415 2416consts 2417 fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100) 2418 2419overloading fresh_star_set \<equiv> "fresh_star :: 'b set \<Rightarrow> 'a \<Rightarrow> bool" 2420begin 2421 definition fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>xs. x\<sharp>(c::'a)" 2422end 2423 2424overloading frsh_star_list \<equiv> "fresh_star :: 'b list \<Rightarrow> 'a \<Rightarrow> bool" 2425begin 2426 definition fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>set xs. x\<sharp>(c::'a)" 2427end 2428 2429lemmas fresh_star_def = fresh_star_list fresh_star_set 2430 2431lemma fresh_star_prod_set: 2432 fixes xs::"'a set" 2433 shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)" 2434by (auto simp add: fresh_star_def fresh_prod) 2435 2436lemma fresh_star_prod_list: 2437 fixes xs::"'a list" 2438 shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)" 2439 by (auto simp add: fresh_star_def fresh_prod) 2440 2441lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set 2442 2443lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c" 2444 by (simp add: fresh_star_def) 2445 2446lemma fresh_star_Un_elim: 2447 "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)" 2448 apply rule 2449 apply (simp_all add: fresh_star_def) 2450 apply (erule meta_mp) 2451 apply blast 2452 done 2453 2454lemma fresh_star_insert_elim: 2455 "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)" 2456 by rule (simp_all add: fresh_star_def) 2457 2458lemma fresh_star_empty_elim: 2459 "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C" 2460 by (simp add: fresh_star_def) 2461 2462text \<open>Normalization of freshness results; see \ \<open>nominal_induct\<close>\<close> 2463 2464lemma fresh_star_unit_elim: 2465 shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C" 2466 and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C" 2467 by (simp_all add: fresh_star_def fresh_def supp_unit) 2468 2469lemma fresh_star_prod_elim: 2470 shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)" 2471 and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)" 2472 by (rule, simp_all add: fresh_star_prod)+ 2473 2474 2475lemma pt_fresh_star_bij_ineq: 2476 fixes pi :: "'x prm" 2477 and x :: "'a" 2478 and a :: "'y set" 2479 and b :: "'y list" 2480 assumes pta: "pt TYPE('a) TYPE('x)" 2481 and ptb: "pt TYPE('y) TYPE('x)" 2482 and at: "at TYPE('x)" 2483 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 2484 shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x" 2485 and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x" 2486apply(unfold fresh_star_def) 2487apply(auto) 2488apply(drule_tac x="pi\<bullet>xa" in bspec) 2489apply(erule pt_set_bij2[OF ptb, OF at]) 2490apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp]) 2491apply(drule_tac x="(rev pi)\<bullet>xa" in bspec) 2492apply(simp add: pt_set_bij1[OF ptb, OF at]) 2493apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) 2494apply(drule_tac x="pi\<bullet>xa" in bspec) 2495apply(simp add: pt_set_bij1[OF ptb, OF at]) 2496apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at]) 2497apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp]) 2498apply(drule_tac x="(rev pi)\<bullet>xa" in bspec) 2499apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt) 2500apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) 2501done 2502 2503lemma pt_fresh_star_bij: 2504 fixes pi :: "'x prm" 2505 and x :: "'a" 2506 and a :: "'x set" 2507 and b :: "'x list" 2508 assumes pt: "pt TYPE('a) TYPE('x)" 2509 and at: "at TYPE('x)" 2510 shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x" 2511 and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x" 2512apply(rule pt_fresh_star_bij_ineq(1)) 2513apply(rule pt) 2514apply(rule at_pt_inst) 2515apply(rule at)+ 2516apply(rule cp_pt_inst) 2517apply(rule pt) 2518apply(rule at) 2519apply(rule pt_fresh_star_bij_ineq(2)) 2520apply(rule pt) 2521apply(rule at_pt_inst) 2522apply(rule at)+ 2523apply(rule cp_pt_inst) 2524apply(rule pt) 2525apply(rule at) 2526done 2527 2528lemma pt_fresh_star_eqvt: 2529 fixes pi :: "'x prm" 2530 and x :: "'a" 2531 and a :: "'x set" 2532 and b :: "'x list" 2533 assumes pt: "pt TYPE('a) TYPE('x)" 2534 and at: "at TYPE('x)" 2535 shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)" 2536 and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)" 2537 by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at]) 2538 2539lemma pt_fresh_star_eqvt_ineq: 2540 fixes pi::"'x prm" 2541 and a::"'y set" 2542 and b::"'y list" 2543 and x::"'a" 2544 assumes pta: "pt TYPE('a) TYPE('x)" 2545 and ptb: "pt TYPE('y) TYPE('x)" 2546 and at: "at TYPE('x)" 2547 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 2548 and dj: "disjoint TYPE('y) TYPE('x)" 2549 shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)" 2550 and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)" 2551 by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool) 2552 2553lemma pt_freshs_freshs: 2554 assumes pt: "pt TYPE('a) TYPE('x)" 2555 and at: "at TYPE ('x)" 2556 and pi: "set (pi::'x prm) \<subseteq> Xs \<times> Ys" 2557 and Xs: "Xs \<sharp>* (x::'a)" 2558 and Ys: "Ys \<sharp>* x" 2559 shows "pi\<bullet>x = x" 2560 using pi 2561proof (induct pi) 2562 case Nil 2563 show ?case by (simp add: pt1 [OF pt]) 2564next 2565 case (Cons p pi) 2566 obtain a b where p: "p = (a, b)" by (cases p) 2567 with Cons Xs Ys have "a \<sharp> x" "b \<sharp> x" 2568 by (simp_all add: fresh_star_def) 2569 with Cons p show ?case 2570 by (simp add: pt_fresh_fresh [OF pt at] 2571 pt2 [OF pt, of "[(a, b)]" pi, simplified]) 2572qed 2573 2574lemma pt_fresh_star_pi: 2575 fixes x::"'a" 2576 and pi::"'x prm" 2577 assumes pt: "pt TYPE('a) TYPE('x)" 2578 and at: "at TYPE('x)" 2579 and a: "((supp x)::'x set)\<sharp>* pi" 2580 shows "pi\<bullet>x = x" 2581using a 2582apply(induct pi) 2583apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt]) 2584apply(subgoal_tac "((a,b)#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x") 2585apply(simp only: pt2[OF pt]) 2586apply(rule pt_fresh_fresh[OF pt at]) 2587apply(simp add: fresh_def at_supp[OF at]) 2588apply(blast) 2589apply(simp add: fresh_def at_supp[OF at]) 2590apply(blast) 2591apply(simp add: pt2[OF pt]) 2592done 2593 2594section \<open>Infrastructure lemmas for strong rule inductions\<close> 2595(*==========================================================*) 2596 2597text \<open> 2598 For every set of atoms, there is another set of atoms 2599 avoiding a finitely supported c and there is a permutation 2600 which 'translates' between both sets. 2601\<close> 2602 2603lemma at_set_avoiding_aux: 2604 fixes Xs::"'a set" 2605 and As::"'a set" 2606 assumes at: "at TYPE('a)" 2607 and b: "Xs \<subseteq> As" 2608 and c: "finite As" 2609 and d: "finite ((supp c)::'a set)" 2610 shows "\<exists>(pi::'a prm). (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" 2611proof - 2612 from b c have "finite Xs" by (simp add: finite_subset) 2613 then show ?thesis using b 2614 proof (induct) 2615 case empty 2616 have "({}::'a set)\<sharp>*c" by (simp add: fresh_star_def) 2617 moreover 2618 have "({}::'a set) \<inter> As = {}" by simp 2619 moreover 2620 have "set ([]::'a prm) \<subseteq> {} \<times> {}" by simp 2621 ultimately show ?case by (simp add: empty_eqvt) 2622 next 2623 case (insert x Xs) 2624 then have ih: "\<exists>pi. (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by simp 2625 then obtain pi where a1: "(pi\<bullet>Xs)\<sharp>*c" and a2: "(pi\<bullet>Xs) \<inter> As = {}" and 2626 a4: "set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by blast 2627 have b: "x\<notin>Xs" by fact 2628 have d1: "finite As" by fact 2629 have d2: "finite Xs" by fact 2630 have d3: "({x} \<union> Xs) \<subseteq> As" using insert(4) by simp 2631 from d d1 d2 2632 obtain y::"'a" where fr: "y\<sharp>(c,pi\<bullet>Xs,As)" 2633 apply(rule_tac at_exists_fresh[OF at, where x="(c,pi\<bullet>Xs,As)"]) 2634 apply(auto simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at] 2635 pt_supp_finite_pi[OF pt_set_inst[OF at_pt_inst[OF at]] at]) 2636 done 2637 have "({y}\<union>(pi\<bullet>Xs))\<sharp>*c" using a1 fr by (simp add: fresh_star_def) 2638 moreover 2639 have "({y}\<union>(pi\<bullet>Xs))\<inter>As = {}" using a2 d1 fr 2640 by (simp add: fresh_prod at_fin_set_fresh[OF at]) 2641 moreover 2642 have "pi\<bullet>x=x" using a4 b a2 d3 2643 by (rule_tac at_prm_fresh2[OF at]) (auto) 2644 then have "set ((pi\<bullet>x,y)#pi) \<subseteq> ({x} \<union> Xs) \<times> ({y}\<union>(pi\<bullet>Xs))" using a4 by auto 2645 moreover 2646 have "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)" 2647 proof - 2648 have eq: "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 2649 proof - 2650 have "(pi\<bullet>x)\<sharp>(pi\<bullet>Xs)" using b d2 2651 by (simp add: pt_fresh_bij [OF pt_set_inst [OF at_pt_inst [OF at]], OF at] 2652 at_fin_set_fresh [OF at]) 2653 moreover 2654 have "y\<sharp>(pi\<bullet>Xs)" using fr by simp 2655 ultimately show "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 2656 by (simp add: pt_fresh_fresh[OF pt_set_inst 2657 [OF at_pt_inst[OF at]], OF at]) 2658 qed 2659 have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))" 2660 by (simp add: pt2[symmetric, OF pt_set_inst [OF at_pt_inst[OF at]]]) 2661 also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))" 2662 by (simp only: union_eqvt perm_set_def at_calc[OF at])(auto) 2663 finally show "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)" using eq by simp 2664 qed 2665 ultimately 2666 show ?case by (rule_tac x="(pi\<bullet>x,y)#pi" in exI) (auto) 2667 qed 2668qed 2669 2670lemma at_set_avoiding: 2671 fixes Xs::"'a set" 2672 assumes at: "at TYPE('a)" 2673 and a: "finite Xs" 2674 and b: "finite ((supp c)::'a set)" 2675 obtains pi::"'a prm" where "(pi\<bullet>Xs)\<sharp>*c" and "set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" 2676using a b at_set_avoiding_aux[OF at, where Xs="Xs" and As="Xs" and c="c"] 2677by (blast) 2678 2679section \<open>composition instances\<close> 2680(* ============================= *) 2681 2682lemma cp_list_inst: 2683 assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" 2684 shows "cp TYPE ('a list) TYPE('x) TYPE('y)" 2685using c1 2686apply(simp add: cp_def) 2687apply(auto) 2688apply(induct_tac x) 2689apply(auto) 2690done 2691 2692lemma cp_set_inst: 2693 assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" 2694 shows "cp TYPE ('a set) TYPE('x) TYPE('y)" 2695using c1 2696apply(simp add: cp_def) 2697apply(auto) 2698apply(auto simp add: perm_set_def) 2699apply(rule_tac x="pi2\<bullet>xc" in exI) 2700apply(auto) 2701done 2702 2703lemma cp_option_inst: 2704 assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" 2705 shows "cp TYPE ('a option) TYPE('x) TYPE('y)" 2706using c1 2707apply(simp add: cp_def) 2708apply(auto) 2709apply(case_tac x) 2710apply(auto) 2711done 2712 2713lemma cp_noption_inst: 2714 assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" 2715 shows "cp TYPE ('a noption) TYPE('x) TYPE('y)" 2716using c1 2717apply(simp add: cp_def) 2718apply(auto) 2719apply(case_tac x) 2720apply(auto) 2721done 2722 2723lemma cp_unit_inst: 2724 shows "cp TYPE (unit) TYPE('x) TYPE('y)" 2725apply(simp add: cp_def) 2726done 2727 2728lemma cp_bool_inst: 2729 shows "cp TYPE (bool) TYPE('x) TYPE('y)" 2730apply(simp add: cp_def) 2731apply(rule allI)+ 2732apply(induct_tac x) 2733apply(simp_all) 2734done 2735 2736lemma cp_prod_inst: 2737 assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" 2738 and c2: "cp TYPE ('b) TYPE('x) TYPE('y)" 2739 shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)" 2740using c1 c2 2741apply(simp add: cp_def) 2742done 2743 2744lemma cp_fun_inst: 2745 assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" 2746 and c2: "cp TYPE ('b) TYPE('x) TYPE('y)" 2747 and pt: "pt TYPE ('y) TYPE('x)" 2748 and at: "at TYPE ('x)" 2749 shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)" 2750using c1 c2 2751apply(auto simp add: cp_def perm_fun_def fun_eq_iff) 2752apply(simp add: rev_eqvt[symmetric]) 2753apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at]) 2754done 2755 2756 2757section \<open>Andy's freshness lemma\<close> 2758(*================================*) 2759 2760lemma freshness_lemma: 2761 fixes h :: "'x\<Rightarrow>'a" 2762 assumes pta: "pt TYPE('a) TYPE('x)" 2763 and at: "at TYPE('x)" 2764 and f1: "finite ((supp h)::'x set)" 2765 and a: "\<exists>a::'x. a\<sharp>(h,h a)" 2766 shows "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> (h a) = fr" 2767proof - 2768 have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 2769 have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 2770 from a obtain a0 where a1: "a0\<sharp>h" and a2: "a0\<sharp>(h a0)" by (force simp add: fresh_prod) 2771 show ?thesis 2772 proof 2773 let ?fr = "h (a0::'x)" 2774 show "\<forall>(a::'x). (a\<sharp>h \<longrightarrow> ((h a) = ?fr))" 2775 proof (intro strip) 2776 fix a 2777 assume a3: "(a::'x)\<sharp>h" 2778 show "h (a::'x) = h a0" 2779 proof (cases "a=a0") 2780 case True thus "h (a::'x) = h a0" by simp 2781 next 2782 case False 2783 assume "a\<noteq>a0" 2784 hence c1: "a\<notin>((supp a0)::'x set)" by (simp add: fresh_def[symmetric] at_fresh[OF at]) 2785 have c2: "a\<notin>((supp h)::'x set)" using a3 by (simp add: fresh_def) 2786 from c1 c2 have c3: "a\<notin>((supp h)\<union>((supp a0)::'x set))" by force 2787 have f2: "finite ((supp a0)::'x set)" by (simp add: at_supp[OF at]) 2788 from f1 f2 have "((supp (h a0))::'x set)\<subseteq>((supp h)\<union>(supp a0))" 2789 by (simp add: pt_supp_fun_subset[OF ptb, OF pta, OF at]) 2790 hence "a\<notin>((supp (h a0))::'x set)" using c3 by force 2791 hence "a\<sharp>(h a0)" by (simp add: fresh_def) 2792 with a2 have d1: "[(a0,a)]\<bullet>(h a0) = (h a0)" by (rule pt_fresh_fresh[OF pta, OF at]) 2793 from a1 a3 have d2: "[(a0,a)]\<bullet>h = h" by (rule pt_fresh_fresh[OF ptc, OF at]) 2794 from d1 have "h a0 = [(a0,a)]\<bullet>(h a0)" by simp 2795 also have "\<dots>= ([(a0,a)]\<bullet>h)([(a0,a)]\<bullet>a0)" by (simp add: pt_fun_app_eq[OF ptb, OF at]) 2796 also have "\<dots> = h ([(a0,a)]\<bullet>a0)" using d2 by simp 2797 also have "\<dots> = h a" by (simp add: at_calc[OF at]) 2798 finally show "h a = h a0" by simp 2799 qed 2800 qed 2801 qed 2802qed 2803 2804lemma freshness_lemma_unique: 2805 fixes h :: "'x\<Rightarrow>'a" 2806 assumes pt: "pt TYPE('a) TYPE('x)" 2807 and at: "at TYPE('x)" 2808 and f1: "finite ((supp h)::'x set)" 2809 and a: "\<exists>(a::'x). a\<sharp>(h,h a)" 2810 shows "\<exists>!(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr" 2811proof (rule ex_ex1I) 2812 from pt at f1 a show "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr" by (simp add: freshness_lemma) 2813next 2814 fix fr1 fr2 2815 assume b1: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr1" 2816 assume b2: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr2" 2817 from a obtain a where "(a::'x)\<sharp>h" by (force simp add: fresh_prod) 2818 with b1 b2 have "h a = fr1 \<and> h a = fr2" by force 2819 thus "fr1 = fr2" by force 2820qed 2821 2822\<comment> \<open>packaging the freshness lemma into a function\<close> 2823definition fresh_fun :: "('x\<Rightarrow>'a)\<Rightarrow>'a" where 2824 "fresh_fun (h) \<equiv> THE fr. (\<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr)" 2825 2826lemma fresh_fun_app: 2827 fixes h :: "'x\<Rightarrow>'a" 2828 and a :: "'x" 2829 assumes pt: "pt TYPE('a) TYPE('x)" 2830 and at: "at TYPE('x)" 2831 and f1: "finite ((supp h)::'x set)" 2832 and a: "\<exists>(a::'x). a\<sharp>(h,h a)" 2833 and b: "a\<sharp>h" 2834 shows "(fresh_fun h) = (h a)" 2835proof (unfold fresh_fun_def, rule the_equality) 2836 show "\<forall>(a'::'x). a'\<sharp>h \<longrightarrow> h a' = h a" 2837 proof (intro strip) 2838 fix a'::"'x" 2839 assume c: "a'\<sharp>h" 2840 from pt at f1 a have "\<exists>(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr" by (rule freshness_lemma) 2841 with b c show "h a' = h a" by force 2842 qed 2843next 2844 fix fr::"'a" 2845 assume "\<forall>a. a\<sharp>h \<longrightarrow> h a = fr" 2846 with b show "fr = h a" by force 2847qed 2848 2849lemma fresh_fun_app': 2850 fixes h :: "'x\<Rightarrow>'a" 2851 and a :: "'x" 2852 assumes pt: "pt TYPE('a) TYPE('x)" 2853 and at: "at TYPE('x)" 2854 and f1: "finite ((supp h)::'x set)" 2855 and a: "a\<sharp>h" "a\<sharp>h a" 2856 shows "(fresh_fun h) = (h a)" 2857apply(rule fresh_fun_app[OF pt, OF at, OF f1]) 2858apply(auto simp add: fresh_prod intro: a) 2859done 2860 2861lemma fresh_fun_equiv_ineq: 2862 fixes h :: "'y\<Rightarrow>'a" 2863 and pi:: "'x prm" 2864 assumes pta: "pt TYPE('a) TYPE('x)" 2865 and ptb: "pt TYPE('y) TYPE('x)" 2866 and ptb':"pt TYPE('a) TYPE('y)" 2867 and at: "at TYPE('x)" 2868 and at': "at TYPE('y)" 2869 and cpa: "cp TYPE('a) TYPE('x) TYPE('y)" 2870 and cpb: "cp TYPE('y) TYPE('x) TYPE('y)" 2871 and f1: "finite ((supp h)::'y set)" 2872 and a1: "\<exists>(a::'y). a\<sharp>(h,h a)" 2873 shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS") 2874proof - 2875 have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at']) 2876 have ptc: "pt TYPE('y\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 2877 have cpc: "cp TYPE('y\<Rightarrow>'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb cpa ptb at]) 2878 have f2: "finite ((supp (pi\<bullet>h))::'y set)" 2879 proof - 2880 from f1 have "finite (pi\<bullet>((supp h)::'y set))" 2881 by (simp add: pt_set_finite_ineq[OF ptb, OF at]) 2882 thus ?thesis 2883 by (simp add: pt_perm_supp_ineq[OF ptc, OF ptb, OF at, OF cpc]) 2884 qed 2885 from a1 obtain a' where c0: "a'\<sharp>(h,h a')" by force 2886 hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by (simp_all add: fresh_prod) 2887 have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1 2888 by (simp add: pt_fresh_bij_ineq[OF ptc, OF ptb, OF at, OF cpc]) 2889 have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')" 2890 proof - 2891 from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))" 2892 by (simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at,OF cpa]) 2893 thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at]) 2894 qed 2895 have a2: "\<exists>(a::'y). a\<sharp>(pi\<bullet>h,(pi\<bullet>h) a)" using c3 c4 by (force simp add: fresh_prod) 2896 have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF ptb', OF at', OF f1]) 2897 have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 2898 by (simp add: fresh_fun_app[OF ptb', OF at', OF f2]) 2899 show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at]) 2900qed 2901 2902lemma fresh_fun_equiv: 2903 fixes h :: "'x\<Rightarrow>'a" 2904 and pi:: "'x prm" 2905 assumes pta: "pt TYPE('a) TYPE('x)" 2906 and at: "at TYPE('x)" 2907 and f1: "finite ((supp h)::'x set)" 2908 and a1: "\<exists>(a::'x). a\<sharp>(h,h a)" 2909 shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS") 2910proof - 2911 have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 2912 have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 2913 have f2: "finite ((supp (pi\<bullet>h))::'x set)" 2914 proof - 2915 from f1 have "finite (pi\<bullet>((supp h)::'x set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at]) 2916 thus ?thesis by (simp add: pt_perm_supp[OF ptc, OF at]) 2917 qed 2918 from a1 obtain a' where c0: "a'\<sharp>(h,h a')" by force 2919 hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by (simp_all add: fresh_prod) 2920 have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1 by (simp add: pt_fresh_bij[OF ptc, OF at]) 2921 have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')" 2922 proof - 2923 from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))" by (simp add: pt_fresh_bij[OF pta, OF at]) 2924 thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at]) 2925 qed 2926 have a2: "\<exists>(a::'x). a\<sharp>(pi\<bullet>h,(pi\<bullet>h) a)" using c3 c4 by (force simp add: fresh_prod) 2927 have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF pta, OF at, OF f1]) 2928 have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2]) 2929 show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at]) 2930qed 2931 2932lemma fresh_fun_supports: 2933 fixes h :: "'x\<Rightarrow>'a" 2934 assumes pt: "pt TYPE('a) TYPE('x)" 2935 and at: "at TYPE('x)" 2936 and f1: "finite ((supp h)::'x set)" 2937 and a: "\<exists>(a::'x). a\<sharp>(h,h a)" 2938 shows "((supp h)::'x set) supports (fresh_fun h)" 2939 apply(simp add: supports_def fresh_def[symmetric]) 2940 apply(auto) 2941 apply(simp add: fresh_fun_equiv[OF pt, OF at, OF f1, OF a]) 2942 apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at]) 2943 done 2944 2945section \<open>Abstraction function\<close> 2946(*==============================*) 2947 2948lemma pt_abs_fun_inst: 2949 assumes pt: "pt TYPE('a) TYPE('x)" 2950 and at: "at TYPE('x)" 2951 shows "pt TYPE('x\<Rightarrow>('a noption)) TYPE('x)" 2952 by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at]) 2953 2954definition abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a noption))" ("[_]._" [100,100] 100) where 2955 "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))" 2956 2957(* FIXME: should be called perm_if and placed close to the definition of permutations on bools *) 2958lemma abs_fun_if: 2959 fixes pi :: "'x prm" 2960 and x :: "'a" 2961 and y :: "'a" 2962 and c :: "bool" 2963 shows "pi\<bullet>(if c then x else y) = (if c then (pi\<bullet>x) else (pi\<bullet>y))" 2964 by force 2965 2966lemma abs_fun_pi_ineq: 2967 fixes a :: "'y" 2968 and x :: "'a" 2969 and pi :: "'x prm" 2970 assumes pta: "pt TYPE('a) TYPE('x)" 2971 and ptb: "pt TYPE('y) TYPE('x)" 2972 and at: "at TYPE('x)" 2973 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 2974 shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)" 2975 apply(simp add: abs_fun_def perm_fun_def abs_fun_if) 2976 apply(simp only: fun_eq_iff) 2977 apply(rule allI) 2978 apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*) 2979 apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>x))")(*B*) 2980 apply(subgoal_tac "pi\<bullet>([(a,(rev pi)\<bullet>xa)]\<bullet>x) = [(pi\<bullet>a,xa)]\<bullet>(pi\<bullet>x)")(*C*) 2981 apply(simp) 2982(*C*) 2983 apply(simp add: cp1[OF cp]) 2984 apply(simp add: pt_pi_rev[OF ptb, OF at]) 2985(*B*) 2986 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp]) 2987(*A*) 2988 apply(rule iffI) 2989 apply(rule pt_bij2[OF ptb, OF at, THEN sym]) 2990 apply(simp) 2991 apply(rule pt_bij2[OF ptb, OF at]) 2992 apply(simp) 2993done 2994 2995lemma abs_fun_pi: 2996 fixes a :: "'x" 2997 and x :: "'a" 2998 and pi :: "'x prm" 2999 assumes pt: "pt TYPE('a) TYPE('x)" 3000 and at: "at TYPE('x)" 3001 shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)" 3002apply(rule abs_fun_pi_ineq) 3003apply(rule pt) 3004apply(rule at_pt_inst) 3005apply(rule at)+ 3006apply(rule cp_pt_inst) 3007apply(rule pt) 3008apply(rule at) 3009done 3010 3011lemma abs_fun_eq1: 3012 fixes x :: "'a" 3013 and y :: "'a" 3014 and a :: "'x" 3015 shows "([a].x = [a].y) = (x = y)" 3016apply(auto simp add: abs_fun_def) 3017apply(auto simp add: fun_eq_iff) 3018apply(drule_tac x="a" in spec) 3019apply(simp) 3020done 3021 3022lemma abs_fun_eq2: 3023 fixes x :: "'a" 3024 and y :: "'a" 3025 and a :: "'x" 3026 and b :: "'x" 3027 assumes pt: "pt TYPE('a) TYPE('x)" 3028 and at: "at TYPE('x)" 3029 and a1: "a\<noteq>b" 3030 and a2: "[a].x = [b].y" 3031 shows "x=[(a,b)]\<bullet>y \<and> a\<sharp>y" 3032proof - 3033 from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: fun_eq_iff) 3034 hence "([a].x) a = ([b].y) a" by simp 3035 hence a3: "nSome(x) = ([b].y) a" by (simp add: abs_fun_def) 3036 show "x=[(a,b)]\<bullet>y \<and> a\<sharp>y" 3037 proof (cases "a\<sharp>y") 3038 assume a4: "a\<sharp>y" 3039 hence "x=[(b,a)]\<bullet>y" using a3 a1 by (simp add: abs_fun_def) 3040 moreover 3041 have "[(a,b)]\<bullet>y = [(b,a)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at]) 3042 ultimately show ?thesis using a4 by simp 3043 next 3044 assume "\<not>a\<sharp>y" 3045 hence "nSome(x) = nNone" using a1 a3 by (simp add: abs_fun_def) 3046 hence False by simp 3047 thus ?thesis by simp 3048 qed 3049qed 3050 3051lemma abs_fun_eq3: 3052 fixes x :: "'a" 3053 and y :: "'a" 3054 and a :: "'x" 3055 and b :: "'x" 3056 assumes pt: "pt TYPE('a) TYPE('x)" 3057 and at: "at TYPE('x)" 3058 and a1: "a\<noteq>b" 3059 and a2: "x=[(a,b)]\<bullet>y" 3060 and a3: "a\<sharp>y" 3061 shows "[a].x =[b].y" 3062proof - 3063 show ?thesis 3064 proof (simp only: abs_fun_def fun_eq_iff, intro strip) 3065 fix c::"'x" 3066 let ?LHS = "if c=a then nSome(x) else if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone" 3067 and ?RHS = "if c=b then nSome(y) else if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone" 3068 show "?LHS=?RHS" 3069 proof - 3070 have "(c=a) \<or> (c=b) \<or> (c\<noteq>a \<and> c\<noteq>b)" by blast 3071 moreover \<comment> \<open>case c=a\<close> 3072 { have "nSome(x) = nSome([(a,b)]\<bullet>y)" using a2 by simp 3073 also have "\<dots> = nSome([(b,a)]\<bullet>y)" by (simp, rule pt3[OF pt], rule at_ds5[OF at]) 3074 finally have "nSome(x) = nSome([(b,a)]\<bullet>y)" by simp 3075 moreover 3076 assume "c=a" 3077 ultimately have "?LHS=?RHS" using a1 a3 by simp 3078 } 3079 moreover \<comment> \<open>case c=b\<close> 3080 { have a4: "y=[(a,b)]\<bullet>x" using a2 by (simp only: pt_swap_bij[OF pt, OF at]) 3081 hence "a\<sharp>([(a,b)]\<bullet>x)" using a3 by simp 3082 hence "b\<sharp>x" by (simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at]) 3083 moreover 3084 assume "c=b" 3085 ultimately have "?LHS=?RHS" using a1 a4 by simp 3086 } 3087 moreover \<comment> \<open>case c\<noteq>a \<and> c\<noteq>b\<close> 3088 { assume a5: "c\<noteq>a \<and> c\<noteq>b" 3089 moreover 3090 have "c\<sharp>x = c\<sharp>y" using a2 a5 by (force simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at]) 3091 moreover 3092 have "c\<sharp>y \<longrightarrow> [(a,c)]\<bullet>x = [(b,c)]\<bullet>y" 3093 proof (intro strip) 3094 assume a6: "c\<sharp>y" 3095 have "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" using a1 a5 by (force intro: at_ds3[OF at]) 3096 hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>y)) = [(a,b)]\<bullet>y" 3097 by (simp add: pt2[OF pt, symmetric] pt3[OF pt]) 3098 hence "[(a,c)]\<bullet>([(b,c)]\<bullet>y) = [(a,b)]\<bullet>y" using a3 a6 3099 by (simp add: pt_fresh_fresh[OF pt, OF at]) 3100 hence "[(a,c)]\<bullet>([(b,c)]\<bullet>y) = x" using a2 by simp 3101 hence "[(b,c)]\<bullet>y = [(a,c)]\<bullet>x" by (drule_tac pt_bij1[OF pt, OF at], simp) 3102 thus "[(a,c)]\<bullet>x = [(b,c)]\<bullet>y" by simp 3103 qed 3104 ultimately have "?LHS=?RHS" by simp 3105 } 3106 ultimately show "?LHS = ?RHS" by blast 3107 qed 3108 qed 3109qed 3110 3111(* alpha equivalence *) 3112lemma abs_fun_eq: 3113 fixes x :: "'a" 3114 and y :: "'a" 3115 and a :: "'x" 3116 and b :: "'x" 3117 assumes pt: "pt TYPE('a) TYPE('x)" 3118 and at: "at TYPE('x)" 3119 shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y))" 3120proof (rule iffI) 3121 assume b: "[a].x = [b].y" 3122 show "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)" 3123 proof (cases "a=b") 3124 case True with b show ?thesis by (simp add: abs_fun_eq1) 3125 next 3126 case False with b show ?thesis by (simp add: abs_fun_eq2[OF pt, OF at]) 3127 qed 3128next 3129 assume "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)" 3130 thus "[a].x = [b].y" 3131 proof 3132 assume "a=b \<and> x=y" thus ?thesis by simp 3133 next 3134 assume "a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y" 3135 thus ?thesis by (simp add: abs_fun_eq3[OF pt, OF at]) 3136 qed 3137qed 3138 3139(* symmetric version of alpha-equivalence *) 3140lemma abs_fun_eq': 3141 fixes x :: "'a" 3142 and y :: "'a" 3143 and a :: "'x" 3144 and b :: "'x" 3145 assumes pt: "pt TYPE('a) TYPE('x)" 3146 and at: "at TYPE('x)" 3147 shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> [(b,a)]\<bullet>x=y \<and> b\<sharp>x))" 3148by (auto simp add: abs_fun_eq[OF pt, OF at] pt_swap_bij'[OF pt, OF at] 3149 pt_fresh_left[OF pt, OF at] 3150 at_calc[OF at]) 3151 3152(* alpha_equivalence with a fresh name *) 3153lemma abs_fun_fresh: 3154 fixes x :: "'a" 3155 and y :: "'a" 3156 and c :: "'x" 3157 and a :: "'x" 3158 and b :: "'x" 3159 assumes pt: "pt TYPE('a) TYPE('x)" 3160 and at: "at TYPE('x)" 3161 and fr: "c\<noteq>a" "c\<noteq>b" "c\<sharp>x" "c\<sharp>y" 3162 shows "([a].x = [b].y) = ([(a,c)]\<bullet>x = [(b,c)]\<bullet>y)" 3163proof (rule iffI) 3164 assume eq0: "[a].x = [b].y" 3165 show "[(a,c)]\<bullet>x = [(b,c)]\<bullet>y" 3166 proof (cases "a=b") 3167 case True then show ?thesis using eq0 by (simp add: pt_bij[OF pt, OF at] abs_fun_eq[OF pt, OF at]) 3168 next 3169 case False 3170 have ineq: "a\<noteq>b" by fact 3171 with eq0 have eq: "x=[(a,b)]\<bullet>y" and fr': "a\<sharp>y" by (simp_all add: abs_fun_eq[OF pt, OF at]) 3172 from eq have "[(a,c)]\<bullet>x = [(a,c)]\<bullet>[(a,b)]\<bullet>y" by (simp add: pt_bij[OF pt, OF at]) 3173 also have "\<dots> = ([(a,c)]\<bullet>[(a,b)])\<bullet>([(a,c)]\<bullet>y)" by (rule pt_perm_compose[OF pt, OF at]) 3174 also have "\<dots> = [(c,b)]\<bullet>y" using ineq fr fr' 3175 by (simp add: pt_fresh_fresh[OF pt, OF at] at_calc[OF at]) 3176 also have "\<dots> = [(b,c)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at]) 3177 finally show ?thesis by simp 3178 qed 3179next 3180 assume eq: "[(a,c)]\<bullet>x = [(b,c)]\<bullet>y" 3181 thus "[a].x = [b].y" 3182 proof (cases "a=b") 3183 case True then show ?thesis using eq by (simp add: pt_bij[OF pt, OF at] abs_fun_eq[OF pt, OF at]) 3184 next 3185 case False 3186 have ineq: "a\<noteq>b" by fact 3187 from fr have "([(a,c)]\<bullet>c)\<sharp>([(a,c)]\<bullet>x)" by (simp add: pt_fresh_bij[OF pt, OF at]) 3188 hence "a\<sharp>([(b,c)]\<bullet>y)" using eq fr by (simp add: at_calc[OF at]) 3189 hence fr0: "a\<sharp>y" using ineq fr by (simp add: pt_fresh_left[OF pt, OF at] at_calc[OF at]) 3190 from eq have "x = (rev [(a,c)])\<bullet>([(b,c)]\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 3191 also have "\<dots> = [(a,c)]\<bullet>([(b,c)]\<bullet>y)" by simp 3192 also have "\<dots> = ([(a,c)]\<bullet>[(b,c)])\<bullet>([(a,c)]\<bullet>y)" by (rule pt_perm_compose[OF pt, OF at]) 3193 also have "\<dots> = [(b,a)]\<bullet>y" using ineq fr fr0 3194 by (simp add: pt_fresh_fresh[OF pt, OF at] at_calc[OF at]) 3195 also have "\<dots> = [(a,b)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at]) 3196 finally show ?thesis using ineq fr0 by (simp add: abs_fun_eq[OF pt, OF at]) 3197 qed 3198qed 3199 3200lemma abs_fun_fresh': 3201 fixes x :: "'a" 3202 and y :: "'a" 3203 and c :: "'x" 3204 and a :: "'x" 3205 and b :: "'x" 3206 assumes pt: "pt TYPE('a) TYPE('x)" 3207 and at: "at TYPE('x)" 3208 and as: "[a].x = [b].y" 3209 and fr: "c\<noteq>a" "c\<noteq>b" "c\<sharp>x" "c\<sharp>y" 3210 shows "x = [(a,c)]\<bullet>[(b,c)]\<bullet>y" 3211using as fr 3212apply(drule_tac sym) 3213apply(simp add: abs_fun_fresh[OF pt, OF at] pt_swap_bij[OF pt, OF at]) 3214done 3215 3216lemma abs_fun_supp_approx: 3217 fixes x :: "'a" 3218 and a :: "'x" 3219 assumes pt: "pt TYPE('a) TYPE('x)" 3220 and at: "at TYPE('x)" 3221 shows "((supp ([a].x))::'x set) \<subseteq> (supp (x,a))" 3222proof 3223 fix c 3224 assume "c\<in>((supp ([a].x))::'x set)" 3225 hence "infinite {b. [(c,b)]\<bullet>([a].x) \<noteq> [a].x}" by (simp add: supp_def) 3226 hence "infinite {b. [([(c,b)]\<bullet>a)].([(c,b)]\<bullet>x) \<noteq> [a].x}" by (simp add: abs_fun_pi[OF pt, OF at]) 3227 moreover 3228 have "{b. [([(c,b)]\<bullet>a)].([(c,b)]\<bullet>x) \<noteq> [a].x} \<subseteq> {b. ([(c,b)]\<bullet>x,[(c,b)]\<bullet>a) \<noteq> (x, a)}" by force 3229 ultimately have "infinite {b. ([(c,b)]\<bullet>x,[(c,b)]\<bullet>a) \<noteq> (x, a)}" by (simp add: infinite_super) 3230 thus "c\<in>(supp (x,a))" by (simp add: supp_def) 3231qed 3232 3233lemma abs_fun_finite_supp: 3234 fixes x :: "'a" 3235 and a :: "'x" 3236 assumes pt: "pt TYPE('a) TYPE('x)" 3237 and at: "at TYPE('x)" 3238 and f: "finite ((supp x)::'x set)" 3239 shows "finite ((supp ([a].x))::'x set)" 3240proof - 3241 from f have "finite ((supp (x,a))::'x set)" by (simp add: supp_prod at_supp[OF at]) 3242 moreover 3243 have "((supp ([a].x))::'x set) \<subseteq> (supp (x,a))" by (rule abs_fun_supp_approx[OF pt, OF at]) 3244 ultimately show ?thesis by (simp add: finite_subset) 3245qed 3246 3247lemma fresh_abs_funI1: 3248 fixes x :: "'a" 3249 and a :: "'x" 3250 and b :: "'x" 3251 assumes pt: "pt TYPE('a) TYPE('x)" 3252 and at: "at TYPE('x)" 3253 and f: "finite ((supp x)::'x set)" 3254 and a1: "b\<sharp>x" 3255 and a2: "a\<noteq>b" 3256 shows "b\<sharp>([a].x)" 3257 proof - 3258 have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)" 3259 proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) 3260 show "finite ((supp ([a].x))::'x set)" using f 3261 by (simp add: abs_fun_finite_supp[OF pt, OF at]) 3262 qed 3263 then obtain c where fr1: "c\<noteq>b" 3264 and fr2: "c\<noteq>a" 3265 and fr3: "c\<sharp>x" 3266 and fr4: "c\<sharp>([a].x)" 3267 by (force simp add: fresh_prod at_fresh[OF at]) 3268 have e: "[(c,b)]\<bullet>([a].x) = [a].([(c,b)]\<bullet>x)" using a2 fr1 fr2 3269 by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at]) 3270 from fr4 have "([(c,b)]\<bullet>c)\<sharp> ([(c,b)]\<bullet>([a].x))" 3271 by (simp add: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at]) 3272 hence "b\<sharp>([a].([(c,b)]\<bullet>x))" using fr1 fr2 e 3273 by (simp add: at_calc[OF at]) 3274 thus ?thesis using a1 fr3 3275 by (simp add: pt_fresh_fresh[OF pt, OF at]) 3276qed 3277 3278lemma fresh_abs_funE: 3279 fixes a :: "'x" 3280 and b :: "'x" 3281 and x :: "'a" 3282 assumes pt: "pt TYPE('a) TYPE('x)" 3283 and at: "at TYPE('x)" 3284 and f: "finite ((supp x)::'x set)" 3285 and a1: "b\<sharp>([a].x)" 3286 and a2: "b\<noteq>a" 3287 shows "b\<sharp>x" 3288proof - 3289 have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)" 3290 proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) 3291 show "finite ((supp ([a].x))::'x set)" using f 3292 by (simp add: abs_fun_finite_supp[OF pt, OF at]) 3293 qed 3294 then obtain c where fr1: "b\<noteq>c" 3295 and fr2: "c\<noteq>a" 3296 and fr3: "c\<sharp>x" 3297 and fr4: "c\<sharp>([a].x)" by (force simp add: fresh_prod at_fresh[OF at]) 3298 have "[a].x = [(b,c)]\<bullet>([a].x)" using a1 fr4 3299 by (simp add: pt_fresh_fresh[OF pt_abs_fun_inst[OF pt, OF at], OF at]) 3300 hence "[a].x = [a].([(b,c)]\<bullet>x)" using fr2 a2 3301 by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at]) 3302 hence b: "([(b,c)]\<bullet>x) = x" by (simp add: abs_fun_eq1) 3303 from fr3 have "([(b,c)]\<bullet>c)\<sharp>([(b,c)]\<bullet>x)" 3304 by (simp add: pt_fresh_bij[OF pt, OF at]) 3305 thus ?thesis using b fr1 by (simp add: at_calc[OF at]) 3306qed 3307 3308lemma fresh_abs_funI2: 3309 fixes a :: "'x" 3310 and x :: "'a" 3311 assumes pt: "pt TYPE('a) TYPE('x)" 3312 and at: "at TYPE('x)" 3313 and f: "finite ((supp x)::'x set)" 3314 shows "a\<sharp>([a].x)" 3315proof - 3316 have "\<exists>c::'x. c\<sharp>(a,x)" 3317 by (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) 3318 then obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a" 3319 and fr2: "c\<sharp>x" by (force simp add: fresh_prod at_fresh[OF at]) 3320 have "c\<sharp>([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at]) 3321 hence "([(c,a)]\<bullet>c)\<sharp>([(c,a)]\<bullet>([a].x))" using fr1 3322 by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at]) 3323 hence a: "a\<sharp>([c].([(c,a)]\<bullet>x))" using fr1_sym 3324 by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at]) 3325 have "[c].([(c,a)]\<bullet>x) = ([a].x)" using fr1_sym fr2 3326 by (simp add: abs_fun_eq[OF pt, OF at]) 3327 thus ?thesis using a by simp 3328qed 3329 3330lemma fresh_abs_fun_iff: 3331 fixes a :: "'x" 3332 and b :: "'x" 3333 and x :: "'a" 3334 assumes pt: "pt TYPE('a) TYPE('x)" 3335 and at: "at TYPE('x)" 3336 and f: "finite ((supp x)::'x set)" 3337 shows "(b\<sharp>([a].x)) = (b=a \<or> b\<sharp>x)" 3338 by (auto dest: fresh_abs_funE[OF pt, OF at,OF f] 3339 intro: fresh_abs_funI1[OF pt, OF at,OF f] 3340 fresh_abs_funI2[OF pt, OF at,OF f]) 3341 3342lemma abs_fun_supp: 3343 fixes a :: "'x" 3344 and x :: "'a" 3345 assumes pt: "pt TYPE('a) TYPE('x)" 3346 and at: "at TYPE('x)" 3347 and f: "finite ((supp x)::'x set)" 3348 shows "supp ([a].x) = (supp x)-{a}" 3349 by (force simp add: supp_fresh_iff fresh_abs_fun_iff[OF pt, OF at, OF f]) 3350 3351(* maybe needs to be better stated as supp intersection supp *) 3352lemma abs_fun_supp_ineq: 3353 fixes a :: "'y" 3354 and x :: "'a" 3355 assumes pta: "pt TYPE('a) TYPE('x)" 3356 and ptb: "pt TYPE('y) TYPE('x)" 3357 and at: "at TYPE('x)" 3358 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 3359 and dj: "disjoint TYPE('y) TYPE('x)" 3360 shows "((supp ([a].x))::'x set) = (supp x)" 3361apply(auto simp add: supp_def) 3362apply(auto simp add: abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp]) 3363apply(auto simp add: dj_perm_forget[OF dj]) 3364apply(auto simp add: abs_fun_eq1) 3365done 3366 3367lemma fresh_abs_fun_iff_ineq: 3368 fixes a :: "'y" 3369 and b :: "'x" 3370 and x :: "'a" 3371 assumes pta: "pt TYPE('a) TYPE('x)" 3372 and ptb: "pt TYPE('y) TYPE('x)" 3373 and at: "at TYPE('x)" 3374 and cp: "cp TYPE('a) TYPE('x) TYPE('y)" 3375 and dj: "disjoint TYPE('y) TYPE('x)" 3376 shows "b\<sharp>([a].x) = b\<sharp>x" 3377 by (simp add: fresh_def abs_fun_supp_ineq[OF pta, OF ptb, OF at, OF cp, OF dj]) 3378 3379section \<open>abstraction type for the parsing in nominal datatype\<close> 3380(*==============================================================*) 3381 3382inductive_set ABS_set :: "('x\<Rightarrow>('a noption)) set" 3383 where 3384 ABS_in: "(abs_fun a x)\<in>ABS_set" 3385 3386definition "ABS = ABS_set" 3387 3388typedef ('x, 'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) = 3389 "ABS::('x\<Rightarrow>('a noption)) set" 3390 morphisms Rep_ABS Abs_ABS 3391 unfolding ABS_def 3392proof 3393 fix x::"'a" and a::"'x" 3394 show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in) 3395qed 3396 3397 3398section \<open>lemmas for deciding permutation equations\<close> 3399(*===================================================*) 3400 3401lemma perm_aux_fold: 3402 shows "perm_aux pi x = pi\<bullet>x" by (simp only: perm_aux_def) 3403 3404lemma pt_perm_compose_aux: 3405 fixes pi1 :: "'x prm" 3406 and pi2 :: "'x prm" 3407 and x :: "'a" 3408 assumes pt: "pt TYPE('a) TYPE('x)" 3409 and at: "at TYPE('x)" 3410 shows "pi2\<bullet>(pi1\<bullet>x) = perm_aux (pi2\<bullet>pi1) (pi2\<bullet>x)" 3411proof - 3412 have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8[OF at]) 3413 hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt]) 3414 thus ?thesis by (simp add: pt2[OF pt] perm_aux_def) 3415qed 3416 3417lemma cp1_aux: 3418 fixes pi1::"'x prm" 3419 and pi2::"'y prm" 3420 and x ::"'a" 3421 assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" 3422 shows "pi1\<bullet>(pi2\<bullet>x) = perm_aux (pi1\<bullet>pi2) (pi1\<bullet>x)" 3423 using cp by (simp add: cp_def perm_aux_def) 3424 3425lemma perm_eq_app: 3426 fixes f :: "'a\<Rightarrow>'b" 3427 and x :: "'a" 3428 and pi :: "'x prm" 3429 assumes pt: "pt TYPE('a) TYPE('x)" 3430 and at: "at TYPE('x)" 3431 shows "(pi\<bullet>(f x)=y) = ((pi\<bullet>f)(pi\<bullet>x)=y)" 3432 by (simp add: pt_fun_app_eq[OF pt, OF at]) 3433 3434lemma perm_eq_lam: 3435 fixes f :: "'a\<Rightarrow>'b" 3436 and x :: "'a" 3437 and pi :: "'x prm" 3438 shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)" 3439 by (simp add: perm_fun_def) 3440 3441section \<open>test\<close> 3442lemma at_prm_eq_compose: 3443 fixes pi1 :: "'x prm" 3444 and pi2 :: "'x prm" 3445 and pi3 :: "'x prm" 3446 assumes at: "at TYPE('x)" 3447 and a: "pi1 \<triangleq> pi2" 3448 shows "(pi3\<bullet>pi1) \<triangleq> (pi3\<bullet>pi2)" 3449proof - 3450 have pt: "pt TYPE('x) TYPE('x)" by (rule at_pt_inst[OF at]) 3451 have pt_prm: "pt TYPE('x prm) TYPE('x)" 3452 by (rule pt_list_inst[OF pt_prod_inst[OF pt, OF pt]]) 3453 from a show ?thesis 3454 apply - 3455 apply(auto simp add: prm_eq_def) 3456 apply(rule_tac pi="rev pi3" in pt_bij4[OF pt, OF at]) 3457 apply(rule trans) 3458 apply(rule pt_perm_compose[OF pt, OF at]) 3459 apply(simp add: pt_rev_pi[OF pt_prm, OF at]) 3460 apply(rule sym) 3461 apply(rule trans) 3462 apply(rule pt_perm_compose[OF pt, OF at]) 3463 apply(simp add: pt_rev_pi[OF pt_prm, OF at]) 3464 done 3465qed 3466 3467(************************) 3468(* Various eqvt-lemmas *) 3469 3470lemma Zero_nat_eqvt: 3471 shows "pi\<bullet>(0::nat) = 0" 3472by (auto simp add: perm_nat_def) 3473 3474lemma One_nat_eqvt: 3475 shows "pi\<bullet>(1::nat) = 1" 3476by (simp add: perm_nat_def) 3477 3478lemma Suc_eqvt: 3479 shows "pi\<bullet>(Suc x) = Suc (pi\<bullet>x)" 3480by (auto simp add: perm_nat_def) 3481 3482lemma numeral_nat_eqvt: 3483 shows "pi\<bullet>((numeral n)::nat) = numeral n" 3484by (simp add: perm_nat_def perm_int_def) 3485 3486lemma max_nat_eqvt: 3487 fixes x::"nat" 3488 shows "pi\<bullet>(max x y) = max (pi\<bullet>x) (pi\<bullet>y)" 3489by (simp add:perm_nat_def) 3490 3491lemma min_nat_eqvt: 3492 fixes x::"nat" 3493 shows "pi\<bullet>(min x y) = min (pi\<bullet>x) (pi\<bullet>y)" 3494by (simp add:perm_nat_def) 3495 3496lemma plus_nat_eqvt: 3497 fixes x::"nat" 3498 shows "pi\<bullet>(x + y) = (pi\<bullet>x) + (pi\<bullet>y)" 3499by (simp add:perm_nat_def) 3500 3501lemma minus_nat_eqvt: 3502 fixes x::"nat" 3503 shows "pi\<bullet>(x - y) = (pi\<bullet>x) - (pi\<bullet>y)" 3504by (simp add:perm_nat_def) 3505 3506lemma mult_nat_eqvt: 3507 fixes x::"nat" 3508 shows "pi\<bullet>(x * y) = (pi\<bullet>x) * (pi\<bullet>y)" 3509by (simp add:perm_nat_def) 3510 3511lemma div_nat_eqvt: 3512 fixes x::"nat" 3513 shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)" 3514by (simp add:perm_nat_def) 3515 3516lemma Zero_int_eqvt: 3517 shows "pi\<bullet>(0::int) = 0" 3518by (auto simp add: perm_int_def) 3519 3520lemma One_int_eqvt: 3521 shows "pi\<bullet>(1::int) = 1" 3522by (simp add: perm_int_def) 3523 3524lemma numeral_int_eqvt: 3525 shows "pi\<bullet>((numeral n)::int) = numeral n" 3526by (simp add: perm_int_def perm_int_def) 3527 3528lemma neg_numeral_int_eqvt: 3529 shows "pi\<bullet>((- numeral n)::int) = - numeral n" 3530by (simp add: perm_int_def perm_int_def) 3531 3532lemma max_int_eqvt: 3533 fixes x::"int" 3534 shows "pi\<bullet>(max (x::int) y) = max (pi\<bullet>x) (pi\<bullet>y)" 3535by (simp add:perm_int_def) 3536 3537lemma min_int_eqvt: 3538 fixes x::"int" 3539 shows "pi\<bullet>(min x y) = min (pi\<bullet>x) (pi\<bullet>y)" 3540by (simp add:perm_int_def) 3541 3542lemma plus_int_eqvt: 3543 fixes x::"int" 3544 shows "pi\<bullet>(x + y) = (pi\<bullet>x) + (pi\<bullet>y)" 3545by (simp add:perm_int_def) 3546 3547lemma minus_int_eqvt: 3548 fixes x::"int" 3549 shows "pi\<bullet>(x - y) = (pi\<bullet>x) - (pi\<bullet>y)" 3550by (simp add:perm_int_def) 3551 3552lemma mult_int_eqvt: 3553 fixes x::"int" 3554 shows "pi\<bullet>(x * y) = (pi\<bullet>x) * (pi\<bullet>y)" 3555by (simp add:perm_int_def) 3556 3557lemma div_int_eqvt: 3558 fixes x::"int" 3559 shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)" 3560by (simp add:perm_int_def) 3561 3562(*******************************************************) 3563(* Setup of the theorem attributes eqvt and eqvt_force *) 3564ML_file "nominal_thmdecls.ML" 3565setup "NominalThmDecls.setup" 3566 3567lemmas [eqvt] = 3568 (* connectives *) 3569 if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 3570 true_eqvt false_eqvt 3571 imp_eqvt [folded HOL.induct_implies_def] 3572 3573 (* datatypes *) 3574 perm_unit.simps 3575 perm_list.simps append_eqvt 3576 perm_prod.simps 3577 fst_eqvt snd_eqvt 3578 perm_option.simps 3579 3580 (* nats *) 3581 Suc_eqvt Zero_nat_eqvt One_nat_eqvt min_nat_eqvt max_nat_eqvt 3582 plus_nat_eqvt minus_nat_eqvt mult_nat_eqvt div_nat_eqvt 3583 3584 (* ints *) 3585 Zero_int_eqvt One_int_eqvt min_int_eqvt max_int_eqvt 3586 plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt 3587 3588 (* sets *) 3589 union_eqvt empty_eqvt insert_eqvt set_eqvt 3590 3591 3592(* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *) 3593(* usual form of an eqvt-lemma, but they are needed for analysing *) 3594(* permutations on nats and ints *) 3595lemmas [eqvt_force] = numeral_nat_eqvt numeral_int_eqvt neg_numeral_int_eqvt 3596 3597(***************************************) 3598(* setup for the individial atom-kinds *) 3599(* and nominal datatypes *) 3600ML_file "nominal_atoms.ML" 3601 3602(************************************************************) 3603(* various tactics for analysing permutations, supports etc *) 3604ML_file "nominal_permeq.ML" 3605 3606method_setup perm_simp = 3607 \<open>NominalPermeq.perm_simp_meth\<close> 3608 \<open>simp rules and simprocs for analysing permutations\<close> 3609 3610method_setup perm_simp_debug = 3611 \<open>NominalPermeq.perm_simp_meth_debug\<close> 3612 \<open>simp rules and simprocs for analysing permutations including debugging facilities\<close> 3613 3614method_setup perm_extend_simp = 3615 \<open>NominalPermeq.perm_extend_simp_meth\<close> 3616 \<open>tactic for deciding equalities involving permutations\<close> 3617 3618method_setup perm_extend_simp_debug = 3619 \<open>NominalPermeq.perm_extend_simp_meth_debug\<close> 3620 \<open>tactic for deciding equalities involving permutations including debugging facilities\<close> 3621 3622method_setup supports_simp = 3623 \<open>NominalPermeq.supports_meth\<close> 3624 \<open>tactic for deciding whether something supports something else\<close> 3625 3626method_setup supports_simp_debug = 3627 \<open>NominalPermeq.supports_meth_debug\<close> 3628 \<open>tactic for deciding whether something supports something else including debugging facilities\<close> 3629 3630method_setup finite_guess = 3631 \<open>NominalPermeq.finite_guess_meth\<close> 3632 \<open>tactic for deciding whether something has finite support\<close> 3633 3634method_setup finite_guess_debug = 3635 \<open>NominalPermeq.finite_guess_meth_debug\<close> 3636 \<open>tactic for deciding whether something has finite support including debugging facilities\<close> 3637 3638method_setup fresh_guess = 3639 \<open>NominalPermeq.fresh_guess_meth\<close> 3640 \<open>tactic for deciding whether an atom is fresh for something\<close> 3641 3642method_setup fresh_guess_debug = 3643 \<open>NominalPermeq.fresh_guess_meth_debug\<close> 3644 \<open>tactic for deciding whether an atom is fresh for something including debugging facilities\<close> 3645 3646(*****************************************************************) 3647(* tactics for generating fresh names and simplifying fresh_funs *) 3648ML_file "nominal_fresh_fun.ML" 3649 3650method_setup generate_fresh = \<open> 3651 Args.type_name {proper = true, strict = true} >> 3652 (fn s => fn ctxt => SIMPLE_METHOD (generate_fresh_tac ctxt s)) 3653\<close> "generate a name fresh for all the variables in the goal" 3654 3655method_setup fresh_fun_simp = \<open> 3656 Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >> 3657 (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b)) 3658\<close> "delete one inner occurrence of fresh_fun" 3659 3660 3661(************************************************) 3662(* main file for constructing nominal datatypes *) 3663lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []" 3664 using assms .. 3665 3666ML_file "nominal_datatype.ML" 3667 3668(******************************************************) 3669(* primitive recursive functions on nominal datatypes *) 3670ML_file "nominal_primrec.ML" 3671 3672(****************************************************) 3673(* inductive definition involving nominal datatypes *) 3674ML_file "nominal_inductive.ML" 3675ML_file "nominal_inductive2.ML" 3676 3677(*****************************************) 3678(* setup for induction principles method *) 3679ML_file "nominal_induct.ML" 3680method_setup nominal_induct = 3681 \<open>NominalInduct.nominal_induct_method\<close> 3682 \<open>nominal induction\<close> 3683 3684end 3685