(*  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_zero:

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

  unfolding fresh_star_def

  by (simp add: fresh_zero_perm)

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(1) 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

      by (intro subset_trans [OF supp_plus_perm])

         (auto simp add: supp_swap)

    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

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: "a \<sharp> x"

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

proof -

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

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

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

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

    unfolding fresh_star_def Ball_def 

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

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

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

qed

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

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_fun_app)

      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 {* @{const nat_of} is an example of a function 

  without finite support *}

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_components_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 {* Induction principle for permutations *}

lemma perm_struct_induct[consumes 1, case_names zero swap]:

  assumes S: "supp p \<subseteq> S"

  and zero: "P 0"

  and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"

  shows "P p"

proof -

  have "finite (supp p)" by (simp add: finite_supp)

  then show "P p" 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: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"

        using as by (auto simp add: supp_atom supp_perm swap_atom)

      let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"

      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 a2 by auto

      then have "P ?q" using ih by simp

      moreover

      have "supp ?q \<subseteq> S" using as a2 by simp

      ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 

      moreover 

      have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)

      ultimately have "P p" by simp

    }

    ultimately show "P p" by blast

  qed

qed

lemma perm_simple_struct_induct[case_names zero swap]:

  assumes zero: "P 0"

  and     swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"

  shows "P p"

by (rule_tac S="supp p" in perm_struct_induct)

   (auto intro: zero swap)

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"

using S

by (induct p rule: perm_struct_induct)

   (auto intro: zero plus swap simp add: supp_swap)

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_struct_induct)

    case zero

    show "0 \<bullet> x = x" by simp

  next

    case (swap p a b)

    then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all

    then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)

  qed

qed

lemma supp_perm_eq_test:

  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 {* Support of Finite Sets of Finitely Supported Elements *}

lemma Union_fresh:

  shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"

  unfolding Union_image_eq[symmetric]

  apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)

  apply(perm_simp)

  apply(rule refl)

  apply(assumption)

  done

lemma Union_supports_set:

  shows "(\<Union>x \<in> S. supp x) supports S"

proof -