# 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