--- a/Nominal/Abs.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Abs.thy Mon Apr 26 10:01:13 2010 +0200
@@ -2,8 +2,8 @@
imports "../Nominal-General/Nominal2_Atoms"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Nominal2_Supp"
- "Nominal2_FSet"
"Quotient"
+ "Quotient_List"
"Quotient_Product"
begin
@@ -129,16 +129,22 @@
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
quotient_definition
+ Abs ("[_]set. _" [60, 60] 60)
+where
"Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
quotient_definition
+ Abs_res ("[_]res. _" [60, 60] 60)
+where
"Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
quotient_definition
+ Abs_lst ("[_]lst. _" [60, 60] 60)
+where
"Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
is
"Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
@@ -169,9 +175,8 @@
shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
- apply(simp_all add: alphas_abs)
- apply(lifting alphas_abs)
- done
+ unfolding alphas_abs
+ by (lifting alphas_abs)
instantiation abs_gen :: (pt) pt
begin
@@ -327,9 +332,8 @@
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
- apply(rule_tac [!] fresh_fun_eqvt_app)
- apply(simp_all add: eqvts_raw)
- done
+ by (rule_tac [!] fresh_fun_eqvt_app)
+ (simp_all add: eqvts_raw)
lemma supp_abs_subset1:
assumes a: "finite (supp x)"
@@ -337,36 +341,32 @@
and "(supp x) - as \<subseteq> supp (Abs_res as x)"
and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
unfolding supp_conv_fresh
- apply(auto dest!: aux_fresh)
- apply(simp_all add: fresh_def supp_finite_atom_set a)
- done
+ by (auto dest!: aux_fresh)
+ (simp_all add: fresh_def supp_finite_atom_set a)
lemma supp_abs_subset2:
assumes a: "finite (supp x)"
shows "supp (Abs as x) \<subseteq> (supp x) - as"
and "supp (Abs_res as x) \<subseteq> (supp x) - as"
and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
- apply(rule_tac [!] supp_is_subset)
- apply(simp_all add: abs_supports a)
- done
+ by (rule_tac [!] supp_is_subset)
+ (simp_all add: abs_supports a)
lemma abs_finite_supp:
assumes a: "finite (supp x)"
shows "supp (Abs as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
- apply(rule_tac [!] subset_antisym)
- apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
- done
+ by (rule_tac [!] subset_antisym)
+ (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
lemma supp_abs:
fixes x::"'a::fs"
shows "supp (Abs as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
- apply(rule_tac [!] abs_finite_supp)
- apply(simp_all add: finite_supp)
- done
+ by (rule_tac [!] abs_finite_supp)
+ (simp_all add: finite_supp)
instance abs_gen :: (fs) fs
apply(default)
@@ -397,101 +397,12 @@
section {* BELOW is stuff that may or may not be needed *}
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- shows "Abs as (t1, t2) = Abs as (s1, s2) \<longrightarrow> (Abs as t1 = Abs as s1 \<and> Abs as t2 = Abs as s2)"
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE)
-apply(simp add: supp_Pair)
-apply(simp add: Un_Diff)
-apply(simp add: fresh_star_union)
-apply(erule conjE)+
-apply(rule conjI)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-done
-
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and> Abs as t2 = Abs bs s2)"
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE)
-apply(simp add: supp_Pair)
-apply(simp add: Un_Diff)
-apply(simp add: fresh_star_union)
-apply(erule conjE)+
-apply(rule conjI)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-done
-
-lemma fresh_star_eq:
- assumes a: "as \<sharp>* p"
- shows "\<forall>a \<in> as. p \<bullet> a = a"
-using a by (simp add: fresh_star_def fresh_def supp_perm)
-
-lemma fresh_star_set_eq:
- assumes a: "as \<sharp>* p"
- shows "p \<bullet> as = as"
-using a
-apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)
-apply(auto)
-by (metis permute_atom_def)
-
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- assumes asm: "finite as"
- shows "(Abs as t1 = Abs bs s1 \<and> Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)"
-apply(subst abs_eq_iff)
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE | erule conjE)+
-apply(simp add: abs_eq_iff)
-apply(simp add: alphas_abs)
-apply(simp add: alphas)
-apply(rule conjI)
-apply(simp add: supp_Pair Un_Diff)
-oops
-
-
-
-(* support of concrete atom sets *)
-
lemma supp_atom_image:
fixes as::"'a::at_base set"
shows "supp (atom ` as) = supp as"
apply(simp add: supp_def)
apply(simp add: image_eqvt)
-apply(simp add: atom_eqvt_raw)
+apply(simp add: eqvts_raw)
apply(simp add: atom_image_cong)
done