(*  Title:      Nominal2_Supp

    Authors:    Brian Huffman, Christian Urban

    Supplementary Lemmas and Definitions for 

    Nominal Isabelle. 

*)

theory Nominal2_Supp

imports Nominal2_Base Nominal2_Eqvt 

begin

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

end