# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264690055 -3600
# Node ID 8e2dd0b29466e71186bed631897182e8ae029da6
# Parent  31b4ac97cfea3ac03d037aad0b9b859922264b38
attempt of a general abstraction operator

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
+
diff -r 31b4ac97cfea -r 8e2dd0b29466 Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Thu Jan 28 14:20:26 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Thu Jan 28 15:47:35 2010 +0100
@@ -47,7 +47,18 @@
 unfolding fresh_star_def
 by (simp add: fresh_plus)
 
-
+lemma supp_finite_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "supp S = S"
+  apply(rule finite_supp_unique)
+  apply(simp add: supports_def)
+  apply(auto simp add: permute_set_eq swap_atom)[1]
+  apply(metis)
+  apply(rule assms)
+  apply(auto simp add: permute_set_eq swap_atom)[1]
+done
+  
 
 atom_decl name
 
@@ -244,9 +255,30 @@
 inductive
     alpha2 :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
 where
-  a1: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"
-| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"
-| a3: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s"
+  a21: "a = b \<Longrightarrow> (rVar a) \<approx>2 (rVar b)"
+| a22: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>2 rApp t2 s2"
+| a23: "(a = b \<and> t \<approx>2 s) \<or> (a \<noteq> b \<and> ((a \<leftrightarrow> b) \<bullet> t) \<approx>2 s \<and> atom b \<notin> rfv t)\<Longrightarrow> rLam a t \<approx>2 rLam b s"
+
+lemma fv_vars:
+  fixes a::name
+  assumes a1: "\<forall>x \<in> rfv t - {atom a}. pi \<bullet> x = x"
+  shows "(pi \<bullet> t) \<approx>2 ((a \<leftrightarrow> (pi \<bullet> a)) \<bullet> t)"
+using a1
+apply(induct t)
+apply(auto)
+apply(rule a21)
+apply(case_tac "name = a")
+apply(simp)
+apply(simp)
+defer
+apply(rule a22)
+apply(simp)
+apply(simp)
+apply(rule a23)
+apply(case_tac "a = name")
+apply(simp)
+oops
+
 
 lemma 
   assumes a1: "t \<approx>2 s"
@@ -272,9 +304,11 @@
 apply(drule alpha_rfv)
 apply(drule sym)
 apply(simp)
+apply(simp add: rfv_eqvt[symmetric])
 defer
 apply(subgoal_tac "atom a \<sharp> (rfv t - {atom a})")
 apply(subgoal_tac "atom b \<sharp> (rfv t - {atom a})")
+
 defer
 sorry
 
@@ -300,6 +334,7 @@
 apply(simp)
 defer
 apply(simp)
+apply(simp add: fresh_star_def)
 sorry
 
 quotient_type lam = rlam / alpha