(*  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 
  "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"

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

lemma fresh_star_union:
  shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
  by (auto simp add: fresh_star_def)

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

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

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

lemma fresh_star_empty_elim:
  "({} \<sharp>* x \<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[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

text {* Induction principle for permutations *}

lemma perm_subset_induct_aux [consumes 1, case_names zero swap plus]:
  assumes S: "supp p \<subseteq> S"
  assumes zero: "P 0"
  assumes swap: "\<And>a b. supp (a \<rightleftharpoons> b) \<subseteq> S \<Longrightarrow> P (a \<rightleftharpoons> b)"
  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
  shows "P p"
proof -
  have "finite (supp p)" by (simp add: finite_supp)
  then show ?thesis using S
  proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
    case (psubset p)
    then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
    have as: "supp p \<subseteq> S" by fact
    { assume "supp p = {}"
      then have "p = 0" by (simp add: supp_perm expand_perm_eq)
      then have "P p" using zero by simp
    }
    moreover
    { assume "supp p \<noteq> {}"
      then obtain a where a0: "a \<in> supp p" by blast
      then have a1: "supp (- p \<bullet> a \<rightleftharpoons> a) \<subseteq> S" using as
	by (auto simp add: supp_atom supp_perm swap_atom)
      let ?q = "p + (- p \<bullet> a \<rightleftharpoons> a)"
      have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
      moreover
      have "a \<notin> supp ?q" by (simp add: supp_perm)
      then have "supp ?q \<noteq> supp p" using a0 by auto
      ultimately have "supp ?q \<subset> supp p" using as by auto
      then have "P ?q" using ih by simp
      moreover
      have "supp ?q \<subseteq> S" using as a2 by simp
      moreover
      have "P (- p \<bullet> a \<rightleftharpoons> a)" using a1 swap by simp
      ultimately 
      have "P (?q + (- p \<bullet> a \<rightleftharpoons> a))" using a1 plus by simp
      moreover 
      have "p = ?q + (- p \<bullet> a \<rightleftharpoons> a)" by (simp add: expand_perm_eq)
      ultimately have "P p" by simp
    }
    ultimately show "P p" by blast
  qed
qed

lemma perm_subset_induct [consumes 1, case_names zero swap plus]:
  assumes S: "supp p \<subseteq> S"
  assumes zero: "P 0"
  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
  shows "P p"
apply(rule perm_subset_induct_aux[OF S])
apply(auto simp add: zero swap plus supp_swap split: if_splits)
done

lemma supp_perm_eq:
  assumes "(supp x) \<sharp>* p"
  shows "p \<bullet> x = x"
proof -
  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
    unfolding supp_perm fresh_star_def fresh_def by auto
  then show "p \<bullet> x = x"
  proof (induct p rule: perm_subset_induct)
    case zero
    show "0 \<bullet> x = x" by simp
  next
    case (swap a b)
    then have "a \<sharp> x" "b \<sharp> x" by simp_all
    then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
  next
    case (plus p1 p2)
    have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
    then show "(p1 + p2) \<bullet> x = x" by simp
  qed
qed

section {* at_set_avoiding2 *}

lemma at_set_avoiding2:
  assumes "finite xs"
  and     "finite (supp c)" "finite (supp x)"
  and     "xs \<sharp>* x"
  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
using assms
apply(erule_tac c="(c, x)" in at_set_avoiding)
apply(simp add: supp_Pair)
apply(rule_tac x="p" in exI)
apply(simp add: fresh_star_prod)
apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
apply(auto simp add: fresh_star_def fresh_def)
done

lemma at_set_avoiding2_atom:
  assumes "finite (supp c)" "finite (supp x)"
  and     b: "xa \<sharp> x"
  shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
proof -
  have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
  obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
    using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
  have c: "(p \<bullet> xa) \<sharp> c" using p1
    unfolding fresh_star_def Ball_def 
    by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
  hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
  then show ?thesis by blast
qed

end