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