--- /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
+