1 (*  Title:      Nominal2_Supp

     2     Authors:    Brian Huffman, Christian Urban

     3 

     4     Supplementary Lemmas and Definitions for 

     5     Nominal Isabelle. 

     6 *)

     7 theory Nominal2_Supp

     8 imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms

     9 begin

    10 

    11 

    12 section {* Fresh-Star *}

    13 

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

    15   induction principles. *}

    16 

    17 definition 

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

    19 where 

    20   "xs \<sharp>* c \<equiv> \<forall>x \<in> xs. x \<sharp> c"

    21 

    22 lemma fresh_star_prod:

    23   fixes xs::"atom set"

    24   shows "xs \<sharp>* (a, b) = (xs \<sharp>* a \<and> xs \<sharp>* b)"

    25   by (auto simp add: fresh_star_def fresh_Pair)

    26 

    27 lemma fresh_star_union:

    28   shows "(xs \<union> ys) \<sharp>* c = (xs \<sharp>* c \<and> ys \<sharp>* c)"

    29   by (auto simp add: fresh_star_def)

    30 

    31 lemma fresh_star_insert:

    32   shows "(insert x ys) \<sharp>* c = (x \<sharp> c \<and> ys \<sharp>* c)"

    33   by (auto simp add: fresh_star_def)

    34 

    35 lemma fresh_star_Un_elim:

    36   "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"

    37   unfolding fresh_star_def

    38   apply(rule)

    39   apply(erule meta_mp)

    40   apply(auto)

    41   done

    42 

    43 lemma fresh_star_insert_elim:

    44   "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"

    45   unfolding fresh_star_def

    46   by rule (simp_all add: fresh_star_def)

    47 

    48 lemma fresh_star_empty_elim:

    49   "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"

    50   by (simp add: fresh_star_def)

    51 

    52 lemma fresh_star_unit_elim: 

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

    54   by (simp add: fresh_star_def fresh_unit) 

    55 

    56 lemma fresh_star_prod_elim: 

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

    58   by (rule, simp_all add: fresh_star_prod)

    59 

    60 

    61 section {* Avoiding of atom sets *}

    62 

    63 text {* 

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

    65   avoiding a finitely supported c and there is a permutation

    66   which 'translates' between both sets.

    67 *}

    68 

    69 lemma at_set_avoiding_aux:

    70   fixes Xs::"atom set"

    71   and   As::"atom set"

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

    73   and     c: "finite As"

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

    75 proof -

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

    77   then show ?thesis using b

    78   proof (induct rule: finite_subset_induct)

    79     case empty

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

    81     moreover

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

    83     ultimately show ?case by blast

    84   next

    85     case (insert x Xs)

    86     then obtain p where

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

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

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

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

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

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

    93       using `finite As` `finite Xs`

    94       by (simp add: permute_set_eq_image)

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

    96       by (rule obtain_atom)

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

    98       by simp_all

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

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

   101       unfolding insert_eqvt

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

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

   104       by (simp add: swap_atom swap_set_not_in)

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

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

   107       unfolding q by simp

   108     moreover

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

   110       using p2 unfolding q

   111       apply (intro subset_trans [OF supp_plus_perm])

   112       apply (auto simp add: supp_swap)

   113       done

   114     ultimately show ?case by blast

   115   qed

   116 qed

   117 

   118 lemma at_set_avoiding:

   119   assumes a: "finite Xs"

   120   and     b: "finite (supp c)"

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

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

   123   unfolding fresh_star_def fresh_def by blast

   124 

   125 

   126 section {* The freshness lemma according to Andrew Pitts *}

   127 

   128 lemma fresh_conv_MOST: 

   129   shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"

   130   unfolding fresh_def supp_def MOST_iff_cofinite by simp

   131 

   132 lemma fresh_apply:

   133   assumes "a \<sharp> f" and "a \<sharp> x" 

   134   shows "a \<sharp> f x"

   135   using assms unfolding fresh_conv_MOST

   136   unfolding permute_fun_app_eq [where f=f]

   137   by (elim MOST_rev_mp, simp)

   138 

   139 lemma freshness_lemma:

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

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

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

   143 proof -

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

   145     by (auto simp add: fresh_Pair)

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

   147   proof (intro exI allI impI)

   148     fix a :: 'a

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

   150     show "h a = h b"

   151     proof (cases "a = b")

   152       assume "a = b"

   153       thus "h a = h b" by simp

   154     next

   155       assume "a \<noteq> b"

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

   157       with a3 have "atom a \<sharp> h b" by (rule fresh_apply)

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

   159         by (rule swap_fresh_fresh)

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

   161         by (rule swap_fresh_fresh)

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

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

   164         by (rule permute_fun_app_eq)

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

   166         using d2 by simp

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

   168     qed

   169   qed

   170 qed

   171 

   172 lemma freshness_lemma_unique:

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

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

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

   176 proof (rule ex_ex1I)

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

   178     by (rule freshness_lemma)

   179 next

   180   fix x y

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

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

   183   from a x y show "x = y"

   184     by (auto simp add: fresh_Pair)

   185 qed

   186 

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

   188 

   189 definition

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

   191 where

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

   193 

   194 lemma fresh_fun_app:

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

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

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

   198   shows "fresh_fun h = h a"

   199 unfolding fresh_fun_def

   200 proof (rule the_equality)

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

   202   proof (intro strip)

   203     fix a':: 'a

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

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

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

   207   qed

   208 next

   209   fix fr :: 'b

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

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

   212 qed

   213 

   214 lemma fresh_fun_app':

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

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

   217   shows "fresh_fun h = h a"

   218   apply (rule fresh_fun_app)

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

   220   done

   221 

   222 lemma fresh_fun_eqvt:

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

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

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

   226   using a

   227   apply (clarsimp simp add: fresh_Pair)

   228   apply (subst fresh_fun_app', assumption+)

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

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

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

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

   233   done

   234 

   235 lemma fresh_fun_supports:

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

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

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

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

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

   241   done

   242 

   243 notation fresh_fun (binder "FRESH " 10)

   244 

   245 lemma FRESH_f_iff:

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

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

   248   assumes P: "finite (supp P)"

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

   250 proof -

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

   252     using P by (rule obtain_at_base)

   253   hence "atom a \<sharp> P"

   254     by (simp add: fresh_def)

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

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

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

   258     apply (simp add: fresh_conv_MOST)

   259     apply (elim MOST_rev_mp, rule MOST_I, clarify)

   260     apply (simp add: permute_fun_def permute_pure expand_fun_eq)

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

   262     apply (rule refl)

   263     done

   264 qed

   265 

   266 lemma FRESH_binop_iff:

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

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

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

   270   assumes P: "finite (supp P)" 

   271   and     Q: "finite (supp Q)"

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

   273 proof -

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

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

   276     by (rule obtain_at_base)

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

   278     by (simp_all add: fresh_def)

   279   show ?thesis

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

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

   282     apply (simp add: fresh_conv_MOST)

   283     apply (elim MOST_rev_mp, rule MOST_I, clarify)

   284     apply (simp add: permute_fun_def permute_pure expand_fun_eq)

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

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

   287     apply (rule refl)

   288     done

   289 qed

   290 

   291 lemma FRESH_conj_iff:

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

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

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

   295 using P Q by (rule FRESH_binop_iff)

   296 

   297 lemma FRESH_disj_iff:

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

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

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

   301 using P Q by (rule FRESH_binop_iff)

   302 

   303 

   304 section {* An example of a function without finite support *}

   305 

   306 primrec

   307   nat_of :: "atom \<Rightarrow> nat"

   308 where

   309   "nat_of (Atom s n) = n"

   310 

   311 lemma atom_eq_iff:

   312   fixes a b :: atom

   313   shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"

   314   by (induct a, induct b, simp)

   315 

   316 lemma not_fresh_nat_of:

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

   318 unfolding fresh_def supp_def

   319 proof (clarsimp)

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

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

   322     by simp

   323   then obtain b where

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

   325     b2: "sort_of b = sort_of a" and

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

   327     by (rule obtain_atom) auto

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

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

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

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

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

   333   with b2 have "a = b" by (simp add: atom_eq_iff)

   334   with b1 show "False" by simp

   335 qed

   336 

   337 lemma supp_nat_of:

   338   shows "supp nat_of = UNIV"

   339   using not_fresh_nat_of [unfolded fresh_def] by auto

   340 

   341 

   342 section {* Support for sets of atoms *}

   343 

   344 lemma supp_finite_atom_set:

   345   fixes S::"atom set"

   346   assumes "finite S"

   347   shows "supp S = S"

   348   apply(rule finite_supp_unique)

   349   apply(simp add: supports_def)

   350   apply(simp add: swap_set_not_in)

   351   apply(rule assms)

   352   apply(simp add: swap_set_in)

   353 done

   354 

   355 

   356 (*

   357 lemma supp_infinite:

   358   fixes S::"atom set"

   359   assumes asm: "finite (UNIV - S)"

   360   shows "(supp S) = (UNIV - S)"

   361 apply(rule finite_supp_unique)

   362 apply(auto simp add: supports_def permute_set_eq swap_atom)[1]

   363 apply(rule asm)

   364 apply(auto simp add: permute_set_eq swap_atom)[1]

   365 done

   366 

   367 lemma supp_infinite_coinfinite:

   368   fixes S::"atom set"

   369   assumes asm1: "infinite S"

   370   and     asm2: "infinite (UNIV-S)"

   371   shows "(supp S) = (UNIV::atom set)"

   372 *)

   373 

   374 

   375 end