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