# 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