10 

    11 

    12 section {* Fresh-Star *}

    13 

    14 

    15 text {* The fresh-star generalisation of fresh is used in strong

    16   induction principles. *}

    17 

    18 definition 

    19   fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)

    20 where 

    21   "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"

    22 

    23 lemma fresh_star_prod:

    24   fixes as::"atom set"

    25   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 

    26   by (auto simp add: fresh_star_def fresh_Pair)

    27 

    28 lemma fresh_star_union:

    29   shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"

    30   by (auto simp add: fresh_star_def)

    31 

    32 lemma fresh_star_insert:

    33   shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"

    34   by (auto simp add: fresh_star_def)

    35 

    36 lemma fresh_star_Un_elim:

    37   "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"

    38   unfolding fresh_star_def

    39   apply(rule)

    40   apply(erule meta_mp)

    41   apply(auto)

    42   done

    43 

    44 lemma fresh_star_insert_elim:

    45   "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"

    46   unfolding fresh_star_def

    47   by rule (simp_all add: fresh_star_def)

    48 

    49 lemma fresh_star_empty_elim:

    50   "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"

    51   by (simp add: fresh_star_def)

    52 

    53 lemma fresh_star_unit_elim: 

    54   shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"

    55   by (simp add: fresh_star_def fresh_unit) 

    56 

    57 lemma fresh_star_prod_elim: 

    58   shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"

    59   by (rule, simp_all add: fresh_star_prod)

    60 

    61 lemma fresh_star_zero:

    62   shows "as \<sharp>* (0::perm)"

    63   unfolding fresh_star_def

    64   by (simp add: fresh_zero_perm)

    65 

    66 lemma fresh_star_plus:

    67   fixes p q::perm

    68   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"

    69   unfolding fresh_star_def

    70   by (simp add: fresh_plus_perm)

    71 

    72 

    73 lemma fresh_star_permute_iff:

    74   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"

    75   unfolding fresh_star_def

    76   by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)

    77 

    78 lemma fresh_star_eqvt[eqvt]:

    79   shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"

    80 unfolding fresh_star_def

    81 unfolding Ball_def

    82 apply(simp add: all_eqvt)

    83 apply(subst permute_fun_def)

    84 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)

    85 done

    86 

    87 section {* Avoiding of atom sets *}

    88 

    89 text {* 

    90   For every set of atoms, there is another set of atoms

    91   avoiding a finitely supported c and there is a permutation

    92   which 'translates' between both sets.

    93 *}

    94 

    95 lemma at_set_avoiding_aux:

    96   fixes Xs::"atom set"

    97   and   As::"atom set"

    98   assumes b: "Xs \<subseteq> As"

    99   and     c: "finite As"

   100   shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"

   101 proof -

   102   from b c have "finite Xs" by (rule finite_subset)

   103   then show ?thesis using b

   104   proof (induct rule: finite_subset_induct)

   105     case empty

   106     have "0 \<bullet> {} \<inter> As = {}" by simp

   107     moreover

   108     have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)

   109     ultimately show ?case by blast

   110   next

   111     case (insert x Xs)

   112     then obtain p where

   113       p1: "(p \<bullet> Xs) \<inter> As = {}" and 

   114       p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast

   115     from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast

   116     with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast

   117     hence px: "p \<bullet> x = x" unfolding supp_perm by simp

   118     have "finite (As \<union> p \<bullet> Xs)"

   119       using `finite As` `finite Xs`

   120       by (simp add: permute_set_eq_image)

   121     then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"

   122       by (rule obtain_atom)

   123     hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"

   124       by simp_all

   125     let ?q = "(x \<rightleftharpoons> y) + p"

   126     have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"

   127       unfolding insert_eqvt

   128       using `p \<bullet> x = x` `sort_of y = sort_of x`

   129       using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`

   130       by (simp add: swap_atom swap_set_not_in)

   131     have "?q \<bullet> insert x Xs \<inter> As = {}"

   132       using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`

   133       unfolding q by simp

   134     moreover

   135     have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"

   136       using p2 unfolding q

   137       by (intro subset_trans [OF supp_plus_perm])

   138          (auto simp add: supp_swap)

   139     ultimately show ?case by blast

   140   qed

   141 qed

   142 

   143 lemma at_set_avoiding:

   144   assumes a: "finite Xs"

   145   and     b: "finite (supp c)"

   146   obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"

   147   using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]

   148   unfolding fresh_star_def fresh_def by blast

   149 

   150 lemma at_set_avoiding2:

   151   assumes "finite xs"

   152   and     "finite (supp c)" "finite (supp x)"

   153   and     "xs \<sharp>* x"

   154   shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"

   155 using assms

   156 apply(erule_tac c="(c, x)" in at_set_avoiding)

   157 apply(simp add: supp_Pair)

   158 apply(rule_tac x="p" in exI)

   159 apply(simp add: fresh_star_prod)

   160 apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")

   161 apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]

   162 apply(auto simp add: fresh_star_def fresh_def)

   163 done

   164 

   165 lemma at_set_avoiding2_atom:

   166   assumes "finite (supp c)" "finite (supp x)"

   167   and     b: "a \<sharp> x"

   168   shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"

   169 proof -

   170   have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)

   171   obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"

   172     using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast

   173   have c: "(p \<bullet> a) \<sharp> c" using p1

   174     unfolding fresh_star_def Ball_def 

   175     by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)

   176   hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast

   177   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast

   178 qed

   179 

   180 

   181 section {* The freshness lemma according to Andy Pitts *}

   182 

   183 lemma freshness_lemma:

   184   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   185   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   186   shows  "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   187 proof -

   188   from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"

   189     by (auto simp add: fresh_Pair)

   190   show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   191   proof (intro exI allI impI)

   192     fix a :: 'a

   193     assume a3: "atom a \<sharp> h"

   194     show "h a = h b"

   195     proof (cases "a = b")

   196       assume "a = b"

   197       thus "h a = h b" by simp

   198     next

   199       assume "a \<noteq> b"

   200       hence "atom a \<sharp> b" by (simp add: fresh_at_base)

   201       with a3 have "atom a \<sharp> h b" 

   202         by (rule fresh_fun_app)

   203       with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"

   204         by (rule swap_fresh_fresh)

   205       from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"

   206         by (rule swap_fresh_fresh)

   207       from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp

   208       also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"

   209         by (rule permute_fun_app_eq)

   210       also have "\<dots> = h a"

   211         using d2 by simp

   212       finally show "h a = h b"  by simp

   213     qed

   214   qed

   215 qed

   216 

   217 lemma freshness_lemma_unique:

   218   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   219   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   220   shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   221 proof (rule ex_ex1I)

   222   from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   223     by (rule freshness_lemma)

   224 next

   225   fix x y

   226   assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"

   227   assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"

   228   from a x y show "x = y"

   229     by (auto simp add: fresh_Pair)

   230 qed

   231 

   232 text {* packaging the freshness lemma into a function *}

   233 

   234 definition

   235   fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"

   236 where

   237   "fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"

   238 

   239 lemma fresh_fun_app:

   240   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   241   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   242   assumes b: "atom a \<sharp> h"

   243   shows "fresh_fun h = h a"

   244 unfolding fresh_fun_def

   245 proof (rule the_equality)

   246   show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"

   247   proof (intro strip)

   248     fix a':: 'a

   249     assume c: "atom a' \<sharp> h"

   250     from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)

   251     with b c show "h a' = h a" by auto

   252   qed

   253 next

   254   fix fr :: 'b

   255   assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"

   256   with b show "fr = h a" by auto

   257 qed

   258 

   259 lemma fresh_fun_app':

   260   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   261   assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"

   262   shows "fresh_fun h = h a"

   263   apply (rule fresh_fun_app)

   264   apply (auto simp add: fresh_Pair intro: a)

   265   done

   266 

   267 lemma fresh_fun_eqvt:

   268   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   269   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   270   shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"

   271   using a

   272   apply (clarsimp simp add: fresh_Pair)

   273   apply (subst fresh_fun_app', assumption+)

   274   apply (drule fresh_permute_iff [where p=p, THEN iffD2])

   275   apply (drule fresh_permute_iff [where p=p, THEN iffD2])

   276   apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])

   277   apply (erule (1) fresh_fun_app' [symmetric])

   278   done

   279 

   280 lemma fresh_fun_supports:

   281   fixes h :: "'a::at \<Rightarrow> 'b::pt"

   282   assumes a: "\<exists>a. atom a \<sharp> (h, h a)"

   283   shows "(supp h) supports (fresh_fun h)"

   284   apply (simp add: supports_def fresh_def [symmetric])

   285   apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)

   286   done

   287 

   288 notation fresh_fun (binder "FRESH " 10)

   289 

   290 lemma FRESH_f_iff:

   291   fixes P :: "'a::at \<Rightarrow> 'b::pure"

   292   fixes f :: "'b \<Rightarrow> 'c::pure"

   293   assumes P: "finite (supp P)"

   294   shows "(FRESH x. f (P x)) = f (FRESH x. P x)"

   295 proof -

   296   obtain a::'a where "atom a \<notin> supp P"

   297     using P by (rule obtain_at_base)

   298   hence "atom a \<sharp> P"

   299     by (simp add: fresh_def)

   300   show "(FRESH x. f (P x)) = f (FRESH x. P x)"

   301     apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])

   302     apply (cut_tac `atom a \<sharp> P`)

   303     apply (simp add: fresh_conv_MOST)

   304     apply (elim MOST_rev_mp, rule MOST_I, clarify)

   305     apply (simp add: permute_fun_def permute_pure expand_fun_eq)

   306     apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])

   307     apply (rule refl)

   308     done

   309 qed

   310 

   311 lemma FRESH_binop_iff:

   312   fixes P :: "'a::at \<Rightarrow> 'b::pure"

   313   fixes Q :: "'a::at \<Rightarrow> 'c::pure"

   314   fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"

   315   assumes P: "finite (supp P)" 

   316   and     Q: "finite (supp Q)"

   317   shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"

   318 proof -

   319   from assms have "finite (supp P \<union> supp Q)" by simp

   320   then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"

   321     by (rule obtain_at_base)

   322   hence "atom a \<sharp> P" and "atom a \<sharp> Q"

   323     by (simp_all add: fresh_def)

   324   show ?thesis

   325     apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])

   326     apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)

   327     apply (simp add: fresh_conv_MOST)

   328     apply (elim MOST_rev_mp, rule MOST_I, clarify)

   329     apply (simp add: permute_fun_def permute_pure expand_fun_eq)

   330     apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])

   331     apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> Q` pure_fresh])

   332     apply (rule refl)

   333     done

   334 qed

   335 

   336 lemma FRESH_conj_iff:

   337   fixes P Q :: "'a::at \<Rightarrow> bool"

   338   assumes P: "finite (supp P)" and Q: "finite (supp Q)"

   339   shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"

   340 using P Q by (rule FRESH_binop_iff)

   341 

   342 lemma FRESH_disj_iff:

   343   fixes P Q :: "'a::at \<Rightarrow> bool"

   344   assumes P: "finite (supp P)" and Q: "finite (supp Q)"

   345   shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"

   346 using P Q by (rule FRESH_binop_iff)

   347 

   348 

   349 section {* @{const nat_of} is an example of a function 

   350   without finite support *}

   351 

   352 

   353 lemma not_fresh_nat_of:

   354   shows "\<not> a \<sharp> nat_of"

   355 unfolding fresh_def supp_def

   356 proof (clarsimp)

   357   assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"

   358   hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"

   359     by simp

   360   then obtain b where

   361     b1: "b \<noteq> a" and

   362     b2: "sort_of b = sort_of a" and

   363     b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"

   364     by (rule obtain_atom) auto

   365   have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)

   366   also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)

   367   also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp

   368   also have "\<dots> = nat_of b" using b2 by simp

   369   finally have "nat_of a = nat_of b" by simp

   370   with b2 have "a = b" by (simp add: atom_components_eq_iff)

   371   with b1 show "False" by simp

   372 qed

   373 

   374 lemma supp_nat_of:

   375   shows "supp nat_of = UNIV"

   376   using not_fresh_nat_of [unfolded fresh_def] by auto

   377