theory LamEx
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" 
begin

datatype 'a ABS_raw = Abs_raw "atom list" "'a::pt"

primrec
  Abs_raw_map
where
  "Abs_raw_map f (Abs_raw as x) = Abs_raw as (f x)"

fun
  Abs_raw_rel
where
  "Abs_raw_rel R (Abs_raw as x) (Abs_raw bs y) = R x y"

declare [[map "ABS_raw" = (Abs_raw_map, Abs_raw_rel)]]

instantiation ABS_raw :: (pt) pt
begin

primrec
  permute_ABS_raw
where
  "permute_ABS_raw p (Abs_raw as x) = Abs_raw (p \<bullet> as) (p \<bullet> x)"

instance
apply(default)
apply(case_tac [!] x)
apply(simp_all)
done

end  

inductive
  alpha_abs :: "('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
where
  "\<lbrakk>\<exists>pi. (supp x) - (set as) = (supp y) - (set bs) \<and>  ((supp x) - (set as)) \<sharp>* pi \<and> pi \<bullet> x = y\<rbrakk> 
   \<Longrightarrow> alpha_abs (Abs_raw as x) (Abs_raw bs y)"


lemma Abs_raw_eq1:
  assumes "alpha_abs (Abs_raw bs x) (Abs_raw bs y)"
  shows "x = y"
using assms
apply(erule_tac alpha_abs.cases)
apply(auto)
apply(drule sym)
apply(simp)
sorry


quotient_type 'a ABS = "('a::pt) ABS_raw" / "alpha_abs::('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
  sorry

quotient_definition
   "Abs::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a ABS"
as
   "Abs_raw"

lemma [quot_respect]:
  shows "((op =) ===> (op =) ===> alpha_abs) Abs_raw Abs_raw"
apply(auto)
apply(rule alpha_abs.intros)
apply(rule_tac x="0" in exI)
apply(simp add: fresh_star_def fresh_zero_perm)
done

lemma [quot_respect]:
  shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
apply(auto)
sorry

lemma ABS_induct:
  "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"
apply(lifting ABS_raw.induct)
done

lemma Abs_eq1:
  assumes "(Abs bs x) = (Abs bs y)"
  shows "x = y"
using assms
apply(lifting Abs_raw_eq1)
done


instantiation ABS :: (pt) pt
begin

quotient_definition
  "permute_ABS::perm \<Rightarrow> ('a::pt ABS) \<Rightarrow> 'a ABS"
as
  "permute::perm \<Rightarrow> ('a::pt ABS_raw) \<Rightarrow> 'a ABS_raw"

lemma permute_ABS [simp]:
  fixes x::"'b::pt"  (* ??? has to be 'b \<dots> 'a doe not work *)
  shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
apply(lifting permute_ABS_raw.simps(1))
done

instance
  apply(default)
  apply(induct_tac [!] x rule: ABS_induct)
  apply(simp_all)
  done

end
  
lemma Abs_supports:
  shows "(supp (as, x)) supports (Abs as x) "
unfolding supports_def
unfolding fresh_def[symmetric]
apply(simp add: fresh_Pair swap_fresh_fresh)
done

instance ABS :: (fs) fs
apply(default)
apply(induct_tac x rule: ABS_induct)
thm supports_finite
apply(rule supports_finite)
apply(rule Abs_supports)
apply(simp add: supp_Pair finite_supp)
done

lemma Abs_fresh1:
  fixes x::"'a::fs"
  assumes a1: "a \<sharp> bs" 
  and     a2: "a \<sharp> x"
  shows "a \<sharp> Abs bs x"
proof -
  obtain c where 
    fr: "c \<sharp> bs" "c \<sharp> x" "c \<sharp> Abs bs x" "sort_of c = sort_of a"
    apply(rule_tac X="supp (bs, x, Abs bs x)" in obtain_atom)
    unfolding fresh_def[symmetric] 
    apply(auto simp add: supp_Pair finite_supp fresh_Pair fresh_atom)
    done
  have "(c \<rightleftharpoons> a) \<bullet> (Abs bs x) = Abs bs x" using a1 a2 fr(1) fr(2) 
    by (simp add: swap_fresh_fresh)
  moreover from fr(3) 
  have "((c \<rightleftharpoons> a) \<bullet> c) \<sharp> ((c \<rightleftharpoons> a) \<bullet>(Abs bs x))"
    by (simp only: fresh_permute_iff)
  ultimately show  "a \<sharp> Abs bs x" using fr(4) 
    by simp
qed

lemma Abs_fresh2:
  fixes x :: "'a::fs"
  assumes a1: "a \<sharp> Abs bs x" 
  and     a2: "a \<sharp> bs" 
  shows "a \<sharp> x"
proof -
  obtain c where 
    fr: "c \<sharp> bs" "c \<sharp> x" "c \<sharp> Abs bs x" "sort_of c = sort_of a"
    apply(rule_tac X="supp (bs, x, Abs bs x)" in obtain_atom)
    unfolding fresh_def[symmetric] 
    apply(auto simp add: supp_Pair finite_supp fresh_Pair fresh_atom)
    done
  have "Abs bs x = (c \<rightleftharpoons> a) \<bullet> (Abs bs x)" using a1 fr(3) 
    by (simp only: swap_fresh_fresh)
  also have "\<dots> = Abs bs ((c \<rightleftharpoons> a) \<bullet> x)" using a2 fr(1) 
    by (simp add: swap_fresh_fresh)
  ultimately have "Abs bs x = Abs bs ((c \<rightleftharpoons> a) \<bullet> x)" by simp
  then have "x = (c \<rightleftharpoons> a) \<bullet> x" by (rule Abs_eq1)
  moreover from fr(2) 
  have "((c \<rightleftharpoons> a) \<bullet> c) \<sharp> ((c \<rightleftharpoons> a) \<bullet> x)"
    by (simp only: fresh_permute_iff)
  ultimately show  "a \<sharp> x" using fr(4) 
    by simp
qed

lemma Abs_fresh3:
  fixes x :: "'a::fs"
  assumes "a \<in> set bs"
  shows "a \<sharp> Abs bs x"
proof -
  obtain c where 
    fr: "c \<sharp> a" "c \<sharp> x" "c \<sharp> Abs bs x" "sort_of c = sort_of a"
    apply(rule_tac X="supp (a, x, Abs bs x)" in obtain_atom)
    unfolding fresh_def[symmetric] 
    apply(auto simp add: supp_Pair finite_supp fresh_Pair fresh_atom)
    done
  from fr(3) have "((c \<rightleftharpoons> a) \<bullet> c) \<sharp> ((c \<rightleftharpoons> a) \<bullet> Abs bs x)"
    by (simp only: fresh_permute_iff)
  moreover
  have "((c \<rightleftharpoons> a) \<bullet> Abs bs x) = Abs bs x" using assms fr(1) fr(2) sorry
  ultimately
  show "a \<sharp> Abs bs x" using fr(4) by simp
qed

done