(*  Title:      Nominal2_Supp
    Authors:    Brian Huffman, Christian Urban

    Supplementary Lemmas and Definitions for 
    Nominal Isabelle. 
*)
theory Nominal2_Supp
imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms
begin


section {* Fresh-Star *}

text {* The fresh-star generalisation of fresh is used in strong
  induction principles. *}

definition 
  fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)
where 
  "xs \<sharp>* c \<equiv> \<forall>x \<in> xs. x \<sharp> c"

lemma fresh_star_prod:
  fixes xs::"atom set"
  shows "xs \<sharp>* (a, b) = (xs \<sharp>* a \<and> xs \<sharp>* b)"
  by (auto simp add: fresh_star_def fresh_Pair)

lemma fresh_star_union:
  shows "(xs \<union> ys) \<sharp>* c = (xs \<sharp>* c \<and> ys \<sharp>* c)"
  by (auto simp add: fresh_star_def)

lemma fresh_star_insert:
  shows "(insert x ys) \<sharp>* c = (x \<sharp> c \<and> ys \<sharp>* c)"
  by (auto simp add: fresh_star_def)

lemma fresh_star_Un_elim:
  "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
  unfolding fresh_star_def
  apply(rule)
  apply(erule meta_mp)
  apply(auto)
  done

lemma fresh_star_insert_elim:
  "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
  unfolding fresh_star_def
  by rule (simp_all add: fresh_star_def)

lemma fresh_star_empty_elim:
  "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
  by (simp add: fresh_star_def)

lemma fresh_star_unit_elim: 
  shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
  by (simp add: fresh_star_def fresh_unit) 

lemma fresh_star_prod_elim: 
  shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
  by (rule, simp_all add: fresh_star_prod)

lemma fresh_star_plus:
  fixes p q::perm
  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
  unfolding fresh_star_def
  by (simp add: fresh_plus_perm)

lemma fresh_star_permute_iff:
  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
  unfolding fresh_star_def
  by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff)

lemma fresh_star_eqvt:
  shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
unfolding fresh_star_def
unfolding Ball_def
apply(simp add: all_eqvt)
apply(subst permute_fun_def)
apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
done

section {* Avoiding of atom sets *}

text {* 
  For every set of atoms, there is another set of atoms
  avoiding a finitely supported c and there is a permutation
  which 'translates' between both sets.
*}

lemma at_set_avoiding_aux:
  fixes Xs::"atom set"
  and   As::"atom set"
  assumes b: "Xs \<subseteq> As"
  and     c: "finite As"
  shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
proof -
  from b c have "finite Xs" by (rule finite_subset)
  then show ?thesis using b
  proof (induct rule: finite_subset_induct)
    case empty
    have "0 \<bullet> {} \<inter> As = {}" by simp
    moreover
    have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
    ultimately show ?case by blast
  next
    case (insert x Xs)
    then obtain p where
      p1: "(p \<bullet> Xs) \<inter> As = {}" and 
      p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast
    from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast
    with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast
    hence px: "p \<bullet> x = x" unfolding supp_perm by simp
    have "finite (As \<union> p \<bullet> Xs)"
      using `finite As` `finite Xs`
      by (simp add: permute_set_eq_image)
    then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"
      by (rule obtain_atom)
    hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"
      by simp_all
    let ?q = "(x \<rightleftharpoons> y) + p"
    have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
      unfolding insert_eqvt
      using `p \<bullet> x = x` `sort_of y = sort_of x`
      using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
      by (simp add: swap_atom swap_set_not_in)
    have "?q \<bullet> insert x Xs \<inter> As = {}"
      using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
      unfolding q by simp
    moreover
    have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
      using p2 unfolding q
      apply (intro subset_trans [OF supp_plus_perm])
      apply (auto simp add: supp_swap)
      done
    ultimately show ?case by blast
  qed
qed

lemma at_set_avoiding:
  assumes a: "finite Xs"
  and     b: "finite (supp c)"
  obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
  using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
  unfolding fresh_star_def fresh_def by blast


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

lemma fresh_conv_MOST: 
  shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
  unfolding fresh_def supp_def MOST_iff_cofinite by simp

lemma fresh_apply:
  assumes "a \<sharp> f" and "a \<sharp> x" 
  shows "a \<sharp> f x"
  using assms unfolding fresh_conv_MOST
  unfolding permute_fun_app_eq [where f=f]
  by (elim MOST_rev_mp, simp)

lemma freshness_lemma:
  fixes h :: "'a::at \<Rightarrow> 'b::pt"
  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
  shows  "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
proof -
  from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"
    by (auto simp add: fresh_Pair)
  show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
  proof (intro exI allI impI)
    fix a :: 'a
    assume a3: "atom a \<sharp> h"
    show "h a = h b"
    proof (cases "a = b")
      assume "a = b"
      thus "h a = h b" by simp
    next
      assume "a \<noteq> b"
      hence "atom a \<sharp> b" by (simp add: fresh_at_base)
      with a3 have "atom a \<sharp> h b" by (rule fresh_apply)
      with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
        by (rule swap_fresh_fresh)
      from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
        by (rule swap_fresh_fresh)
      from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp
      also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"
        by (rule permute_fun_app_eq)
      also have "\<dots> = h a"
        using d2 by simp
      finally show "h a = h b"  by simp
    qed
  qed
qed

lemma freshness_lemma_unique:
  fixes h :: "'a::at \<Rightarrow> 'b::pt"
  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
  shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
proof (rule ex_ex1I)
  from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
    by (rule freshness_lemma)
next
  fix x y
  assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
  assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"
  from a x y show "x = y"
    by (auto simp add: fresh_Pair)
qed

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

definition
  fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
where
  "fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"

lemma fresh_fun_app:
  fixes h :: "'a::at \<Rightarrow> 'b::pt"
  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
  assumes b: "atom a \<sharp> h"
  shows "fresh_fun h = h a"
unfolding fresh_fun_def
proof (rule the_equality)
  show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"
  proof (intro strip)
    fix a':: 'a
    assume c: "atom a' \<sharp> h"
    from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)
    with b c show "h a' = h a" by auto
  qed
next
  fix fr :: 'b
  assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"
  with b show "fr = h a" by auto
qed

lemma fresh_fun_app':
  fixes h :: "'a::at \<Rightarrow> 'b::pt"
  assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
  shows "fresh_fun h = h a"
  apply (rule fresh_fun_app)
  apply (auto simp add: fresh_Pair intro: a)
  done

lemma fresh_fun_eqvt:
  fixes h :: "'a::at \<Rightarrow> 'b::pt"
  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
  shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"
  using a
  apply (clarsimp simp add: fresh_Pair)
  apply (subst fresh_fun_app', assumption+)
  apply (drule fresh_permute_iff [where p=p, THEN iffD2])
  apply (drule fresh_permute_iff [where p=p, THEN iffD2])
  apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])
  apply (erule (1) fresh_fun_app' [symmetric])
  done

lemma fresh_fun_supports:
  fixes h :: "'a::at \<Rightarrow> 'b::pt"
  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
  shows "(supp h) supports (fresh_fun h)"
  apply (simp add: supports_def fresh_def [symmetric])
  apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)
  done

notation fresh_fun (binder "FRESH " 10)

lemma FRESH_f_iff:
  fixes P :: "'a::at \<Rightarrow> 'b::pure"
  fixes f :: "'b \<Rightarrow> 'c::pure"
  assumes P: "finite (supp P)"
  shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
proof -
  obtain a::'a where "atom a \<notin> supp P"
    using P by (rule obtain_at_base)
  hence "atom a \<sharp> P"
    by (simp add: fresh_def)
  show "(FRESH x. f (P x)) = f (FRESH x. P x)"
    apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])
    apply (cut_tac `atom a \<sharp> P`)
    apply (simp add: fresh_conv_MOST)
    apply (elim MOST_rev_mp, rule MOST_I, clarify)
    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
    apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])
    apply (rule refl)
    done
qed

lemma FRESH_binop_iff:
  fixes P :: "'a::at \<Rightarrow> 'b::pure"
  fixes Q :: "'a::at \<Rightarrow> 'c::pure"
  fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"
  assumes P: "finite (supp P)" 
  and     Q: "finite (supp Q)"
  shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"
proof -
  from assms have "finite (supp P \<union> supp Q)" by simp
  then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"
    by (rule obtain_at_base)
  hence "atom a \<sharp> P" and "atom a \<sharp> Q"
    by (simp_all add: fresh_def)
  show ?thesis
    apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])
    apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
    apply (simp add: fresh_conv_MOST)
    apply (elim MOST_rev_mp, rule MOST_I, clarify)
    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
    apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])
    apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
    apply (rule refl)
    done
qed

lemma FRESH_conj_iff:
  fixes P Q :: "'a::at \<Rightarrow> bool"
  assumes P: "finite (supp P)" and Q: "finite (supp Q)"
  shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"
using P Q by (rule FRESH_binop_iff)

lemma FRESH_disj_iff:
  fixes P Q :: "'a::at \<Rightarrow> bool"
  assumes P: "finite (supp P)" and Q: "finite (supp Q)"
  shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"
using P Q by (rule FRESH_binop_iff)


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

primrec
  nat_of :: "atom \<Rightarrow> nat"
where
  "nat_of (Atom s n) = n"

lemma atom_eq_iff:
  fixes a b :: atom
  shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
  by (induct a, induct b, simp)

lemma not_fresh_nat_of:
  shows "\<not> a \<sharp> nat_of"
unfolding fresh_def supp_def
proof (clarsimp)
  assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"
  hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"
    by simp
  then obtain b where
    b1: "b \<noteq> a" and
    b2: "sort_of b = sort_of a" and
    b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"
    by (rule obtain_atom) auto
  have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)
  also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)
  also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp
  also have "\<dots> = nat_of b" using b2 by simp
  finally have "nat_of a = nat_of b" by simp
  with b2 have "a = b" by (simp add: atom_eq_iff)
  with b1 show "False" by simp
qed

lemma supp_nat_of:
  shows "supp nat_of = UNIV"
  using not_fresh_nat_of [unfolded fresh_def] by auto


section {* Support for sets of atoms *}

lemma supp_finite_atom_set:
  fixes S::"atom set"
  assumes "finite S"
  shows "supp S = S"
  apply(rule finite_supp_unique)
  apply(simp add: supports_def)
  apply(simp add: swap_set_not_in)
  apply(rule assms)
  apply(simp add: swap_set_in)
done


(*
lemma supp_infinite:
  fixes S::"atom set"
  assumes asm: "finite (UNIV - S)"
  shows "(supp S) = (UNIV - S)"
apply(rule finite_supp_unique)
apply(auto simp add: supports_def permute_set_eq swap_atom)[1]
apply(rule asm)
apply(auto simp add: permute_set_eq swap_atom)[1]
done

lemma supp_infinite_coinfinite:
  fixes S::"atom set"
  assumes asm1: "infinite S"
  and     asm2: "infinite (UNIV-S)"
  shows "(supp S) = (UNIV::atom set)"
*)


end