diff -r 31b4ac97cfea -r 8e2dd0b29466 Quot/Nominal/Abs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/Abs.thy	Thu Jan 28 15:47:35 2010 +0100
@@ -0,0 +1,191 @@
+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
+