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 swap_set_fresh:

    70   assumes a: "a \<notin> S" "b \<notin> S"

    71   shows "(a \<rightleftharpoons> b) \<bullet> S = S"

    72   using a

    73   by (auto simp add: permute_set_eq swap_atom)

    74 

    75 lemma at_set_avoiding_aux:

    76   fixes Xs::"atom set"

    77   and   As::"atom set"

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

    79   and     c: "finite As"

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

    81 proof -

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

    83   then show ?thesis using b

    84   proof (induct rule: finite_subset_induct)

    85     case empty

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

    87     moreover

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

    89     ultimately show ?case by blast

    90   next

    91     case (insert x Xs)

    92     then obtain p where

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

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

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

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

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

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

    99       using `finite As` `finite Xs`

   100       by (simp add: permute_set_eq_image)

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

   102       by (rule obtain_atom)

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

   104       by simp_all

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

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

   107       unfolding insert_eqvt

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

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

   110       by (simp add: swap_atom swap_set_fresh)

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

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

   113       unfolding q by simp

   114     moreover

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

   116       using p2 unfolding q

   117       apply (intro subset_trans [OF supp_plus_perm])

   118       apply (auto simp add: supp_swap)

   119       done

   120     ultimately show ?case by blast

   121   qed

   122 qed

   123 

   124 lemma at_set_avoiding:

   125   assumes a: "finite Xs"

   126   and     b: "finite (supp c)"

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

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

   129   unfolding fresh_star_def fresh_def by blast

   130 

   131 

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

   133 

   134 lemma fresh_conv_MOST: 

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

   136   unfolding fresh_def supp_def MOST_iff_cofinite by simp

   137 

   138 lemma fresh_apply:

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

   140   shows "a \<sharp> f x"

   141   using assms unfolding fresh_conv_MOST

   142   unfolding permute_fun_app_eq [where f=f]

   143   by (elim MOST_rev_mp, simp)

   144 

   145 lemma freshness_lemma:

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

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

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

   149 proof -

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

   151     by (auto simp add: fresh_Pair)

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

   153   proof (intro exI allI impI)

   154     fix a :: 'a

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

   156     show "h a = h b"

   157     proof (cases "a = b")

   158       assume "a = b"

   159       thus "h a = h b" by simp

   160     next

   161       assume "a \<noteq> b"

   162       hence "atom a \<sharp> b" by (simp add: fresh_at)

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

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

   165         by (rule swap_fresh_fresh)

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

   167         by (rule swap_fresh_fresh)

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

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

   170         by (rule permute_fun_app_eq)

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

   172         using d2 by simp

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

   174     qed

   175   qed

   176 qed

   177 

   178 lemma freshness_lemma_unique:

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

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

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

   182 proof (rule ex_ex1I)

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

   184     by (rule freshness_lemma)

   185 next

   186   fix x y

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

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

   189   from a x y show "x = y"

   190     by (auto simp add: fresh_Pair)

   191 qed

   192 

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

   194 

   195 definition

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

   197 where

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

   199 

   200 lemma fresh_fun_app:

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

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

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

   204   shows "fresh_fun h = h a"

   205 unfolding fresh_fun_def

   206 proof (rule the_equality)

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

   208   proof (intro strip)

   209     fix a':: 'a

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

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

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

   213   qed

   214 next

   215   fix fr :: 'b

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

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

   218 qed

   219 

   220 lemma fresh_fun_app':

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

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

   223   shows "fresh_fun h = h a"

   224   apply (rule fresh_fun_app)

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

   226   done

   227 

   228 lemma fresh_fun_eqvt:

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

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

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

   232   using a

   233   apply (clarsimp simp add: fresh_Pair)

   234   apply (subst fresh_fun_app', assumption+)

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

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

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

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

   239   done

   240 

   241 lemma fresh_fun_supports:

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

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

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

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

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

   247   done

   248 

   249 notation fresh_fun (binder "FRESH " 10)

   250 

   251 lemma FRESH_f_iff:

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

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

   254   assumes P: "finite (supp P)"

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

   256 proof -

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

   258     using P by (rule obtain_at_base)

   259   hence "atom a \<sharp> P"

   260     by (simp add: fresh_def)

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

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

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

   264     apply (simp add: fresh_conv_MOST)

   265     apply (elim MOST_rev_mp, rule MOST_I, clarify)

   266     apply (simp add: permute_fun_def permute_pure expand_fun_eq)

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

   268     apply (rule refl)

   269     done

   270 qed

   271 

   272 lemma FRESH_binop_iff:

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

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

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

   276   assumes P: "finite (supp P)" 

   277   and     Q: "finite (supp Q)"

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

   279 proof -

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

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

   282     by (rule obtain_at_base)

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

   284     by (simp_all add: fresh_def)

   285   show ?thesis

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

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

   288     apply (simp add: fresh_conv_MOST)

   289     apply (elim MOST_rev_mp, rule MOST_I, clarify)

   290     apply (simp add: permute_fun_def permute_pure expand_fun_eq)

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

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

   293     apply (rule refl)

   294     done

   295 qed

   296 

   297 lemma FRESH_conj_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 \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"

   301 using P Q by (rule FRESH_binop_iff)

   302 

   303 lemma FRESH_disj_iff:

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

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

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

   307 using P Q by (rule FRESH_binop_iff)

   308 

   309 

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

   311 

   312 primrec

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

   314 where

   315   "nat_of (Atom s n) = n"

   316 

   317 lemma atom_eq_iff:

   318   fixes a b :: atom

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

   320   by (induct a, induct b, simp)

   321 

   322 lemma not_fresh_nat_of:

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

   324 unfolding fresh_def supp_def

   325 proof (clarsimp)

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

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

   328     by simp

   329   then obtain b where

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

   331     b2: "sort_of b = sort_of a" and

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

   333     by (rule obtain_atom) auto

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

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

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

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

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

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

   340   with b1 show "False" by simp

   341 qed

   342 

   343 lemma supp_nat_of:

   344   shows "supp nat_of = UNIV"

   345   using not_fresh_nat_of [unfolded fresh_def] by auto

   346 

   347 

   348 (*

   349 section {* Characterisation of the support of sets of atoms *}

   350 

   351 lemma swap_set_ineq:

   352   fixes a b::"'a::at"

   353   assumes "a \<in> S" "b \<notin> S"

   354   shows "(a \<leftrightarrow> b) \<bullet> S \<noteq> S"

   355 using assms

   356 unfolding permute_set_eq 

   357 by (auto simp add: permute_flip_at)

   358 

   359 lemma supp_finite:

   360   fixes S::"'a::at set"

   361   assumes asm: "finite S"

   362   shows "(supp S) = atom ` S"

   363 sorry

   364 

   365 lemma supp_infinite:

   366   fixes S::"atom set"

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

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

   369 apply(rule finite_supp_unique)

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

   371 apply(rule asm)

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

   373 done

   374 

   375 lemma supp_infinite_coinfinite:

   376   fixes S::"atom set"

   377   assumes asm1: "infinite S"

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

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

   380 *)

   381 

   382 

   383 end