diff -r e8cf0520c820 -r 7b3dd407f6b3 Nominal/Abs.thy --- a/Nominal/Abs.thy Sat Mar 27 08:42:07 2010 +0100 +++ b/Nominal/Abs.thy Sun Mar 28 22:54:38 2010 +0200 @@ -120,37 +120,6 @@ apply(rule_tac [!] x="p \ pa" in exI) by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) -fun - aux_set -where - "aux_set (bs, x) = (supp x) - bs" - -fun - aux_list -where - "aux_list (cs, x) = (supp x) - (set cs)" - -lemma aux_abs_lemma: - assumes a: "(bs, x) \abs (cs, y)" - shows "aux_set (bs, x) = aux_set (cs, y)" - using a - by (induct rule: alpha_abs.induct) - (simp add: alphas_abs alphas) - -lemma aux_abs_res_lemma: - assumes a: "(bs, x) \abs_res (cs, y)" - shows "aux_set (bs, x) = aux_set (cs, y)" - using a - by (induct rule: alpha_abs_res.induct) - (simp add: alphas_abs alphas) - -lemma aux_abs_list_lemma: - assumes a: "(bs, x) \abs_lst (cs, y)" - shows "aux_list (bs, x) = aux_list (cs, y)" - using a - by (induct rule: alpha_abs_lst.induct) - (simp add: alphas_abs alphas) - quotient_type 'a abs_gen = "(atom set \ 'a::pt)" / "alpha_abs" and 'b abs_res = "(atom set \ 'b::pt)" / "alpha_abs_res" @@ -188,24 +157,13 @@ unfolding fun_rel_def by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) -lemma [quot_respect]: - shows "(alpha_abs ===> op=) aux_set aux_set" - and "(alpha_abs_res ===> op=) aux_set aux_set" - and "(alpha_abs_lst ===> op=) aux_list aux_list" - unfolding fun_rel_def - apply(rule_tac [!] allI) - apply(rule_tac [!] allI) - apply(case_tac [!] x, case_tac [!] y) - apply(rule_tac [!] impI) - by (simp_all only: aux_abs_lemma aux_abs_res_lemma aux_abs_list_lemma) - -lemma abs_inducts: - shows "(\as (x::'a::pt). P1 (Abs as x)) \ P1 x1" - and "(\as (x::'a::pt). P2 (Abs_res as x)) \ P2 x2" - and "(\as (x::'a::pt). P3 (Abs_lst as x)) \ P3 x3" - by (lifting prod.induct[where 'a="atom set" and 'b="'a"] - prod.induct[where 'a="atom set" and 'b="'a"] - prod.induct[where 'a="atom list" and 'b="'a"]) +lemma abs_exhausts: + shows "(\as (x::'a::pt). y1 = Abs as x \ P1) \ P1" + and "(\as (x::'a::pt). y2 = Abs_res as x \ P2) \ P2" + and "(\as (x::'a::pt). y3 = Abs_lst as x \ P3) \ P3" + by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] + prod.exhaust[where 'a="atom set" and 'b="'a"] + prod.exhaust[where 'a="atom list" and 'b="'a"]) lemma abs_eq_iff: shows "Abs bs x = Abs cs y \ (bs, x) \abs (cs, y)" @@ -230,7 +188,7 @@ instance apply(default) - apply(induct_tac [!] x rule: abs_inducts(1)) + apply(case_tac [!] x rule: abs_exhausts(1)) apply(simp_all) done @@ -251,7 +209,7 @@ instance apply(default) - apply(induct_tac [!] x rule: abs_inducts(2)) + apply(case_tac [!] x rule: abs_exhausts(2)) apply(simp_all) done @@ -272,7 +230,7 @@ instance apply(default) - apply(induct_tac [!] x rule: abs_inducts(3)) + apply(case_tac [!] x rule: abs_exhausts(3)) apply(simp_all) done @@ -317,37 +275,52 @@ unfolding permute_abs by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric]) -quotient_definition - "supp_gen :: ('a::pt) abs_gen \ atom set" -is - "aux_set" +function + supp_gen :: "('a::pt) abs_gen \ atom set" +where + "supp_gen (Abs as x) = supp x - as" +apply(case_tac x rule: abs_exhausts(1)) +apply(simp) +apply(simp add: abs_eq_iff alphas_abs alphas) +done -quotient_definition - "supp_res :: ('a::pt) abs_res \ atom set" -is - "aux_set" +termination supp_gen + by (auto intro!: local.termination) -quotient_definition - "supp_lst :: ('a::pt) abs_lst \ atom set" -is - "aux_list" +function + supp_res :: "('a::pt) abs_res \ atom set" +where + "supp_res (Abs_res as x) = supp x - as" +apply(case_tac x rule: abs_exhausts(2)) +apply(simp) +apply(simp add: abs_eq_iff alphas_abs alphas) +done + +termination supp_res + by (auto intro!: local.termination) -lemma aux_supps: - shows "supp_gen (Abs bs x) = (supp x) - bs" - and "supp_res (Abs_res bs x) = (supp x) - bs" - and "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" - by (lifting aux_set.simps aux_set.simps aux_list.simps) +function + supp_lst :: "('a::pt) abs_lst \ atom set" +where + "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" +apply(case_tac x rule: abs_exhausts(3)) +apply(simp) +apply(simp add: abs_eq_iff alphas_abs alphas) +done -lemma aux_supp_eqvt[eqvt]: +termination supp_lst + by (auto intro!: local.termination) + +lemma [eqvt]: shows "(p \ supp_gen x) = supp_gen (p \ x)" and "(p \ supp_res y) = supp_res (p \ y)" and "(p \ supp_lst z) = supp_lst (p \ z)" - apply(induct_tac x rule: abs_inducts(1)) - apply(simp add: aux_supps supp_eqvt Diff_eqvt) - apply(induct_tac y rule: abs_inducts(2)) - apply(simp add: aux_supps supp_eqvt Diff_eqvt) - apply(induct_tac z rule: abs_inducts(3)) - apply(simp add: aux_supps supp_eqvt Diff_eqvt set_eqvt) + apply(case_tac x rule: abs_exhausts(1)) + apply(simp add: supp_eqvt Diff_eqvt) + apply(case_tac y rule: abs_exhausts(2)) + apply(simp add: supp_eqvt Diff_eqvt) + apply(case_tac z rule: abs_exhausts(3)) + apply(simp add: supp_eqvt Diff_eqvt set_eqvt) done lemma aux_fresh: @@ -364,7 +337,7 @@ and "(supp x) - as \ supp (Abs_res as x)" and "(supp x) - (set bs) \ supp (Abs_lst bs x)" unfolding supp_conv_fresh - apply(auto dest!: aux_fresh simp add: aux_supps) + apply(auto dest!: aux_fresh) apply(simp_all add: fresh_def supp_finite_atom_set a) done @@ -397,19 +370,19 @@ instance abs_gen :: (fs) fs apply(default) - apply(induct_tac x rule: abs_inducts(1)) + apply(case_tac x rule: abs_exhausts(1)) apply(simp add: supp_abs finite_supp) done instance abs_res :: (fs) fs apply(default) - apply(induct_tac x rule: abs_inducts(2)) + apply(case_tac x rule: abs_exhausts(2)) apply(simp add: supp_abs finite_supp) done instance abs_lst :: (fs) fs apply(default) - apply(induct_tac x rule: abs_inducts(3)) + apply(case_tac x rule: abs_exhausts(3)) apply(simp add: supp_abs finite_supp) done @@ -422,7 +395,6 @@ unfolding supp_abs by auto - section {* BELOW is stuff that may or may not be needed *} (* support of concrete atom sets *)