# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264718198 -3600
# Node ID 98375dde48fc87f09e7ec41809932689635d2fd7
# Parent  8e2dd0b29466e71186bed631897182e8ae029da6
general abstraction operator and complete characterisation of its support and freshness

diff -r 8e2dd0b29466 -r 98375dde48fc Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Thu Jan 28 15:47:35 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Thu Jan 28 23:36:38 2010 +0100
@@ -2,7 +2,30 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" 
 begin
 
-datatype 'a ABS_raw = Abs_raw "atom list" "'a::pt"
+(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
+lemma in_permute_iff:
+  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
+apply(unfold mem_def permute_fun_def)[1]
+apply(simp add: permute_bool_def) 
+done
+
+lemma fresh_star_permute_iff:
+  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
+apply(simp add: fresh_star_def)
+apply(auto)
+apply(drule_tac x="p \<bullet> xa" in bspec)
+apply(unfold mem_def permute_fun_def)[1] 
+apply(simp add: eqvts)
+apply(simp add: fresh_permute_iff)
+apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
+apply(simp)
+apply(drule_tac x="- p \<bullet> xa" in bspec)
+apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
+apply(simp)
+apply(simp)
+done
+
+datatype 'a ABS_raw = Abs_raw "atom set" "'a::pt"
 
 primrec
   Abs_raw_map
@@ -35,55 +58,136 @@
 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> 
+  "\<lbrakk>\<exists>pi. (supp x) - as = (supp y) - bs \<and>  ((supp x) - as) \<sharp>* pi \<and> pi \<bullet> x = y\<rbrakk> 
    \<Longrightarrow> alpha_abs (Abs_raw as x) (Abs_raw bs y)"
 
+lemma alpha_reflp:
+  shows "alpha_abs ab ab"
+apply(induct ab)
+apply(rule alpha_abs.intros)
+apply(rule_tac x="0" in exI)
+apply(simp add: fresh_star_def fresh_zero_perm)
+done
 
-lemma Abs_raw_eq1:
-  assumes "alpha_abs (Abs_raw bs x) (Abs_raw bs y)"
-  shows "x = y"
-using assms
+lemma alpha_symp:
+  assumes a: "alpha_abs ab1 ab2"
+  shows "alpha_abs ab2 ab1"
+using a
+apply(erule_tac alpha_abs.cases)
+apply(clarify)
+apply(rule alpha_abs.intros)
+apply(rule_tac x="- pi" in exI)
+apply(auto)
+apply(auto simp add: fresh_star_def)
+apply(simp add: fresh_def supp_minus_perm)
+done
+
+lemma alpha_transp:
+  assumes a1: "alpha_abs ab1 ab2"
+  and     a2: "alpha_abs ab2 ab3"
+  shows "alpha_abs ab1 ab3"
+using a1 a2
+apply(erule_tac alpha_abs.cases)
+apply(erule_tac alpha_abs.cases)
+apply(clarify)
+apply(rule alpha_abs.intros)
+apply(rule_tac x="pia + pi" in exI)
+apply(simp)
+apply(auto simp add: fresh_star_def)
+using supp_plus_perm
+apply(simp add: fresh_def)
+apply(blast)
+done
+
+lemma alpha_eqvt:
+  assumes a: "alpha_abs ab1 ab2"
+  shows "alpha_abs (p \<bullet> ab1) (p \<bullet> ab2)"
+using a
 apply(erule_tac alpha_abs.cases)
-apply(auto)
-apply(drule sym)
+apply(clarify)
 apply(simp)
-sorry
+apply(rule alpha_abs.intros)
+apply(rule_tac x="p \<bullet> pi" in exI)
+apply(rule conjI)
+apply(simp add: supp_eqvt[symmetric])
+apply(simp add: Diff_eqvt[symmetric])
+apply(rule conjI)
+apply(simp add: supp_eqvt[symmetric])
+apply(simp add: Diff_eqvt[symmetric])
+apply(simp only: fresh_star_permute_iff)
+apply(simp add: permute_eqvt[symmetric])
+done
 
+lemma test1:
+  assumes a1: "a \<notin> (supp x) - bs"
+  and     a2: "b \<notin> (supp x) - bs"
+  shows "alpha_abs (Abs_raw bs x) (Abs_raw ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
+apply(rule alpha_abs.intros)
+apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
+apply(rule_tac conjI)
+apply(simp add: supp_eqvt[symmetric])
+apply(simp add: Diff_eqvt[symmetric])
+using a1 a2
+apply(simp add: swap_set_fresh)
+apply(rule conjI)
+prefer 2
+apply(simp)
+apply(simp add: fresh_star_def)
+apply(simp add: fresh_def)
+apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
+using a1 a2
+apply -
+apply(blast)
+apply(simp add: supp_swap)
+done
+
+fun
+  s_test
+where
+  "s_test (Abs_raw bs x) = (supp x) - bs"
+
+lemma s_test_lemma:
+  assumes a: "alpha_abs x y" 
+  shows "s_test x = s_test y"
+using a
+apply(induct)
+apply(simp)
+done
+  
 
 quotient_type 'a ABS = "('a::pt) ABS_raw" / "alpha_abs::('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
-  sorry
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto intro: alpha_reflp alpha_symp alpha_transp)
+  done
 
 quotient_definition
-   "Abs::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a ABS"
+   "Abs::atom set \<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)
+apply(rule alpha_reflp)
 done
 
 lemma [quot_respect]:
   shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"
 apply(auto)
-sorry
+apply(simp add: alpha_eqvt)
+done
+
+lemma [quot_respect]:
+  shows "(alpha_abs ===> (op =)) s_test s_test"
+apply(simp add: s_test_lemma)
+done
 
 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
 
@@ -105,87 +209,114 @@
   done
 
 end
-  
+
+lemma test1_lifted:
+  assumes a1: "a \<notin> (supp x) - bs"
+  and     a2: "b \<notin> (supp x) - bs"
+  shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
+using a1 a2
+apply(lifting test1)
+done
+
 lemma Abs_supports:
-  shows "(supp (as, x)) supports (Abs as x) "
+  shows "((supp x) - as) supports (Abs as x) "
 unfolding supports_def
+apply(clarify)
+apply(simp (no_asm))
+apply(subst test1_lifted[symmetric])
+apply(simp_all)
+done
+
+quotient_definition
+  "s_test_lifted :: ('a::pt) ABS \<Rightarrow> atom \<Rightarrow> bool"
+as
+  "s_test::('a::pt) ABS_raw \<Rightarrow> atom \<Rightarrow> bool"
+
+lemma s_test_lifted_simp:
+  shows "s_test_lifted (Abs bs x) = (supp x) - bs"
+apply(lifting s_test.simps(1))
+done
+
+lemma s_test_lifted_eqvt:
+  shows "(p \<bullet> (s_test_lifted ab)) = s_test_lifted (p \<bullet> ab)"
+apply(induct ab rule: ABS_induct)
+apply(simp add: s_test_lifted_simp supp_eqvt Diff_eqvt)
+done
+
+lemma fresh_f_empty_supp:
+  assumes a: "\<forall>p. p \<bullet> f = f"
+  shows "a \<sharp> x \<Longrightarrow> a \<sharp> (f x)"
+apply(simp add: fresh_def)
+apply(simp add: supp_def)
+apply(simp add: permute_fun_app_eq)
+apply(simp add: a)
+apply(rule finite_subset)
+prefer 2
+apply(assumption)
+apply(auto)
+done
+
+
+lemma s_test_fresh_lemma:
+  shows "(a \<sharp> Abs bs x) \<Longrightarrow> (a \<sharp> s_test_lifted (Abs bs x))"
+apply(rule fresh_f_empty_supp)
+apply(rule allI)
+apply(subst permute_fun_def)
+apply(simp add: s_test_lifted_eqvt)
+apply(simp)
+done
+
+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
+
+lemma s_test_subset:
+  fixes x::"'a::fs"
+  shows "((supp x) - as) \<subseteq> (supp (Abs as x))"
+apply(rule subsetI)
+apply(rule contrapos_pp)
+apply(assumption)
 unfolding fresh_def[symmetric]
-apply(simp add: fresh_Pair swap_fresh_fresh)
+apply(drule_tac s_test_fresh_lemma)
+apply(simp only: s_test_lifted_simp)
+apply(simp add: fresh_def)
+apply(subgoal_tac "finite (supp x - as)")
+apply(simp add: supp_finite_set)
+apply(simp add: finite_supp)
+done
+
+lemma supp_Abs:
+  fixes x::"'a::fs"
+  shows "supp (Abs as x) = (supp x) - as"
+apply(rule subset_antisym)
+apply(rule supp_is_subset)
+apply(rule Abs_supports)
+apply(simp add: finite_supp)
+apply(rule s_test_subset)
 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)
+apply(simp add: supp_Abs)
+apply(simp add: finite_supp)
 done
 
-lemma Abs_fresh1:
+lemma fresh_abs1:
   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
+  shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
+apply(simp add: fresh_def)
+apply(simp add: supp_Abs)
+apply(auto)
+done
 
 done