# HG changeset patch # User Christian Urban # Date 1264718218 -3600 # Node ID 542b36e1c390c9df3e4a0a28c1ff06b3cb3fe1d0 # Parent 98375dde48fc87f09e7ec41809932689635d2fd7# Parent ef8a2b0b237aef8961cd308e3d5fd3b566097340 merged diff -r ef8a2b0b237a -r 542b36e1c390 Quot/Nominal/Abs.thy --- a/Quot/Nominal/Abs.thy Thu Jan 28 19:23:55 2010 +0100 +++ b/Quot/Nominal/Abs.thy Thu Jan 28 23:36:58 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 \\must be cleaned *) +lemma in_permute_iff: + shows "(p \ x) \ (p \ X) \ x \ X" +apply(unfold mem_def permute_fun_def)[1] +apply(simp add: permute_bool_def) +done + +lemma fresh_star_permute_iff: + shows "(p \ a) \* (p \ x) \ a \* x" +apply(simp add: fresh_star_def) +apply(auto) +apply(drule_tac x="p \ 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 \ 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 \ 'a ABS_raw \ bool" where - "\\pi. (supp x) - (set as) = (supp y) - (set bs) \ ((supp x) - (set as)) \* pi \ pi \ x = y\ + "\\pi. (supp x) - as = (supp y) - bs \ ((supp x) - as) \* pi \ pi \ x = y\ \ 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 \ ab1) (p \ 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 \ 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 \ (supp x) - bs" + and a2: "b \ (supp x) - bs" + shows "alpha_abs (Abs_raw bs x) (Abs_raw ((a \ b) \ bs) ((a \ b) \ x))" +apply(rule alpha_abs.intros) +apply(rule_tac x="(a \ 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 \ b) \ {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 \ 'a ABS_raw \ 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 \ ('a::pt) \ 'a ABS" + "Abs::atom set \ ('a::pt) \ '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: "\\as (x::'a::pt). P (Abs as x)\ \ 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 \ (supp x) - bs" + and a2: "b \ (supp x) - bs" + shows "(Abs bs x) = (Abs ((a \ b) \ bs) ((a \ b) \ 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 \ atom \ bool" +as + "s_test::('a::pt) ABS_raw \ atom \ 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 \ (s_test_lifted ab)) = s_test_lifted (p \ 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: "\p. p \ f = f" + shows "a \ x \ a \ (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 \ Abs bs x) \ (a \ 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) \ (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 \ bs" - and a2: "a \ x" - shows "a \ Abs bs x" -proof - - obtain c where - fr: "c \ bs" "c \ x" "c \ 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 \ a) \ (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 \ a) \ c) \ ((c \ a) \(Abs bs x))" - by (simp only: fresh_permute_iff) - ultimately show "a \ Abs bs x" using fr(4) - by simp -qed - -lemma Abs_fresh2: - fixes x :: "'a::fs" - assumes a1: "a \ Abs bs x" - and a2: "a \ bs" - shows "a \ x" -proof - - obtain c where - fr: "c \ bs" "c \ x" "c \ 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 \ a) \ (Abs bs x)" using a1 fr(3) - by (simp only: swap_fresh_fresh) - also have "\ = Abs bs ((c \ a) \ x)" using a2 fr(1) - by (simp add: swap_fresh_fresh) - ultimately have "Abs bs x = Abs bs ((c \ a) \ x)" by simp - then have "x = (c \ a) \ x" by (rule Abs_eq1) - moreover from fr(2) - have "((c \ a) \ c) \ ((c \ a) \ x)" - by (simp only: fresh_permute_iff) - ultimately show "a \ x" using fr(4) - by simp -qed - -lemma Abs_fresh3: - fixes x :: "'a::fs" - assumes "a \ set bs" - shows "a \ Abs bs x" -proof - - obtain c where - fr: "c \ a" "c \ x" "c \ 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 \ a) \ c) \ ((c \ a) \ Abs bs x)" - by (simp only: fresh_permute_iff) - moreover - have "((c \ a) \ Abs bs x) = Abs bs x" using assms fr(1) fr(2) sorry - ultimately - show "a \ Abs bs x" using fr(4) by simp -qed + shows "a \ Abs bs x = (a \ bs \ (a \ bs \ a \ x))" +apply(simp add: fresh_def) +apply(simp add: supp_Abs) +apply(auto) +done done