# HG changeset patch # User Christian Urban # Date 1268998315 -3600 # Node ID dbdce626c9254551d26ed29e836c48e7f0e9bce7 # Parent f329811050891f1a712a43cf82887a69c9648e1e# Parent c6849a634582a89da00e6217a12852d74bf2bd9b merged diff -r f32981105089 -r dbdce626c925 Nominal/Abs.thy --- a/Nominal/Abs.thy Fri Mar 19 12:31:17 2010 +0100 +++ b/Nominal/Abs.thy Fri Mar 19 12:31:55 2010 +0100 @@ -1,5 +1,5 @@ theory Abs -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" "Nominal2_FSet" begin lemma permute_boolI: @@ -749,17 +749,6 @@ (* support of concrete atom sets *) -lemma atom_eqvt_raw: - fixes p::"perm" - shows "(p \ atom) = atom" -by (simp add: expand_fun_eq permute_fun_def atom_eqvt) - -lemma atom_image_cong: - shows "(atom ` X = atom ` Y) = (X = Y)" -apply(rule inj_image_eq_iff) -apply(simp add: inj_on_def) -done - lemma supp_atom_image: fixes as::"'a::at_base set" shows "supp (atom ` as) = supp as" @@ -793,5 +782,10 @@ \ pi \ bs = cs)" by (simp add: alpha_gen) +(* maybe should be added to Infinite.thy *) +lemma infinite_Un: + shows "infinite (S \ T) \ infinite S \ infinite T" + by simp + end diff -r f32981105089 -r dbdce626c925 Nominal/LamEx.thy --- a/Nominal/LamEx.thy Fri Mar 19 12:31:17 2010 +0100 +++ b/Nominal/LamEx.thy Fri Mar 19 12:31:55 2010 +0100 @@ -41,10 +41,6 @@ "\(P \ Q) \ (\P) \ (\Q)" by simp -lemma infinite_Un: - "infinite (S \ T) \ infinite S \ infinite T" - by simp - instance apply default apply(induct_tac x) diff -r f32981105089 -r dbdce626c925 Nominal/LamEx2.thy --- a/Nominal/LamEx2.thy Fri Mar 19 12:31:17 2010 +0100 +++ b/Nominal/LamEx2.thy Fri Mar 19 12:31:55 2010 +0100 @@ -41,10 +41,6 @@ "\(P \ Q) \ (\P) \ (\Q)" by simp -lemma infinite_Un: - "infinite (S \ T) \ infinite S \ infinite T" - by simp - instance apply default apply(induct_tac x) diff -r f32981105089 -r dbdce626c925 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Fri Mar 19 12:31:17 2010 +0100 +++ b/Nominal/Nominal2_FSet.thy Fri Mar 19 12:31:55 2010 +0100 @@ -61,6 +61,10 @@ lemma fset_to_set_eqvt[eqvt]: "pi \ (fset_to_set x) = fset_to_set (pi \ x)" by (lifting set_eqvt) +lemma fin_fset_to_set: + "finite (fset_to_set x)" + by (induct x) (simp_all) + lemma supp_fset_to_set: "supp (fset_to_set x) = supp x" apply (simp add: supp_def) @@ -80,28 +84,75 @@ apply (simp add: eqvts eqvts_raw atom_fmap_cong) done -(*lemma "\ (memb x S) \ \ (memb y T) \ ((x # S) \ (y # T)) = (x = y \ S \ T)"*) +lemma supp_atom_insert: + "finite (xs :: atom set) \ supp (insert x xs) = supp x \ supp xs" + apply (simp add: supp_finite_atom_set) + apply (simp add: supp_atom) + done -lemma infinite_Un: - shows "infinite (S \ T) \ infinite S \ infinite T" - by simp +lemma atom_image_cong: + shows "(atom ` X = atom ` Y) = (X = Y)" + apply(rule inj_image_eq_iff) + apply(simp add: inj_on_def) + done -lemma supp_insert: "supp (insert (x :: 'a :: fs) xs) = supp x \ supp xs" - oops +lemma atom_eqvt_raw: + fixes p::"perm" + shows "(p \ atom) = atom" + by (simp add: expand_fun_eq permute_fun_def atom_eqvt) -lemma supp_finsert: - "supp (finsert (x :: 'a :: fs) S) = supp x \ supp S" +lemma supp_finite_at_set: + fixes S::"('a :: at) set" + assumes a: "finite S" + shows "supp S = atom ` S" + apply(rule finite_supp_unique) + apply(simp add: supports_def) + apply (rule finite_induct[OF a]) + apply (simp add: eqvts) + apply (simp) + apply clarify + apply (subst atom_image_cong[symmetric]) + apply (subst atom_eqvt_raw[symmetric]) + apply (subst eqvts[symmetric]) + apply (rule swap_set_not_in) + apply simp_all + apply(rule finite_imageI) + apply(rule a) + apply (subst atom_image_cong[symmetric]) + apply (subst atom_eqvt_raw[symmetric]) + apply (subst eqvts[symmetric]) + apply (rule swap_set_in) + apply simp_all + done + +lemma supp_at_insert: + "finite (xs :: ('a :: at) set) \ supp (insert x xs) = supp x \ supp xs" + apply (simp add: supp_finite_at_set) + apply (simp add: supp_at_base) + done + +lemma supp_atom_finsert: + "supp (finsert (x :: atom) S) = supp x \ supp S" apply (subst supp_fset_to_set[symmetric]) - apply simp - (* apply (simp add: supp_insert supp_fset_to_set) *) - oops + apply (simp add: supp_finite_atom_set) + apply (simp add: supp_atom_insert[OF fin_fset_to_set]) + apply (simp add: supp_fset_to_set) + done -instance fset :: (fs) fs +lemma supp_at_finsert: + "supp (finsert (x :: 'a :: at) S) = supp x \ supp S" + apply (subst supp_fset_to_set[symmetric]) + apply (simp add: supp_finite_atom_set) + apply (simp add: supp_at_insert[OF fin_fset_to_set]) + apply (simp add: supp_fset_to_set) + done + +instance fset :: (at) fs apply (default) apply (induct_tac x rule: fset_induct) apply (simp add: supp_def eqvts) - (* apply (simp add: supp_finsert) *) - (* apply default ? *) - oops + apply (simp add: supp_at_finsert) + apply (simp add: supp_at_base) + done end diff -r f32981105089 -r dbdce626c925 Nominal/Term1.thy --- a/Nominal/Term1.thy Fri Mar 19 12:31:17 2010 +0100 +++ b/Nominal/Term1.thy Fri Mar 19 12:31:55 2010 +0100 @@ -195,9 +195,6 @@ lemma Collect_neg_conj: "{x. \(P x \ Q x)} = {x. \(P x)} \ {x. \(Q x)}" by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) -lemma inf_or: "(infinite x \ infinite y) = infinite (x \ y)" -by (simp add: finite_Un) - lemma supp_fv_let: assumes sa : "fv_bp bp = supp bp" shows "\fv_trm1 ta = supp ta; fv_trm1 tb = supp tb; fv_bp bp = supp bp\ @@ -212,7 +209,7 @@ apply(simp only: permute_ABS) apply(simp only: Abs_eq_iff) apply(simp only: alpha_gen supp_Pair split_conv eqvts) -apply(simp only: inf_or[symmetric]) +apply(simp only: infinite_Un) apply(simp only: Collect_disj_eq) apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) apply (simp only: eqvts[symmetric] fv_trm1_eqvt[symmetric])