--- a/Nominal/Abs.thy Fri Mar 26 22:22:41 2010 +0100
+++ b/Nominal/Abs.thy Fri Mar 26 22:23:22 2010 +0100
@@ -117,33 +117,6 @@
apply(rule_tac [!] x="p \<bullet> pa" in exI)
by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
-lemma alphas_abs_swap1:
- assumes a1: "a \<notin> (supp x) - bs"
- and a2: "b \<notin> (supp x) - bs"
- shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
- and "(bs, x) \<approx>abs_res ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
- using a1 a2
- unfolding alphas_abs
- unfolding alphas
- unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
- unfolding fresh_star_def fresh_def
- unfolding swap_set_not_in[OF a1 a2]
- by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
- (auto simp add: supp_perm swap_atom)
-
-lemma alphas_abs_swap2:
- assumes a1: "a \<notin> (supp x) - (set bs)"
- and a2: "b \<notin> (supp x) - (set bs)"
- shows "(bs, x) \<approx>abs_lst ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
- using a1 a2
- unfolding alphas_abs
- unfolding alphas
- unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
- unfolding fresh_star_def fresh_def
- unfolding swap_set_not_in[OF a1 a2]
- by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
- (auto simp add: supp_perm swap_atom)
-
fun
aux_set
where
@@ -227,9 +200,16 @@
shows "(\<And>as (x::'a::pt). P1 (Abs as x)) \<Longrightarrow> P1 x1"
and "(\<And>as (x::'a::pt). P2 (Abs_res as x)) \<Longrightarrow> P2 x2"
and "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3"
- apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
- apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
- apply(lifting prod.induct[where 'a="atom list" and 'b="'a"])
+ 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_eq_iff:
+ 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)
+ apply(lifting alphas_abs)
done
instantiation abs_gen :: (pt) pt
@@ -297,6 +277,42 @@
lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
+lemma abs_swap1:
+ 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)"
+ and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ unfolding abs_eq_iff
+ unfolding alphas_abs
+ unfolding alphas
+ unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+ unfolding fresh_star_def fresh_def
+ unfolding swap_set_not_in[OF a1 a2]
+ using a1 a2
+ by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ (auto simp add: supp_perm swap_atom)
+
+lemma abs_swap2:
+ assumes a1: "a \<notin> (supp x) - (set bs)"
+ and a2: "b \<notin> (supp x) - (set bs)"
+ shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ unfolding abs_eq_iff
+ unfolding alphas_abs
+ unfolding alphas
+ unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+ unfolding fresh_star_def fresh_def
+ unfolding swap_set_not_in[OF a1 a2]
+ using a1 a2
+ by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ (auto simp add: supp_perm swap_atom)
+
+lemma abs_supports:
+ shows "((supp x) - as) supports (Abs as x)"
+ and "((supp x) - as) supports (Abs_res as x)"
+ and "((supp x) - (set bs)) supports (Abs_lst bs x)"
+ unfolding supports_def
+ unfolding permute_abs
+ by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
quotient_definition
"supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set"
@@ -317,10 +333,7 @@
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)"
- apply(lifting aux_set.simps)
- apply(lifting aux_set.simps)
- apply(lifting aux_list.simps)
- done
+ by (lifting aux_set.simps aux_set.simps aux_list.simps)
lemma aux_supp_eqvt[eqvt]:
shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
@@ -342,30 +355,6 @@
apply(simp_all add: eqvts_raw)
done
-lemma abs_swap1:
- 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)"
- and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
- using a1 a2
- apply(lifting alphas_abs_swap1(1))
- apply(lifting alphas_abs_swap1(2))
- done
-
-lemma abs_swap2:
- assumes a1: "a \<notin> (supp x) - (set bs)"
- and a2: "b \<notin> (supp x) - (set bs)"
- shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
- using a1 a2 by (lifting alphas_abs_swap2)
-
-lemma abs_supports:
- shows "((supp x) - as) supports (Abs as x)"
- and "((supp x) - as) supports (Abs_res as x)"
- and "((supp x) - (set bs)) supports (Abs_lst bs x)"
- unfolding supports_def
- unfolding permute_abs
- by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
-
lemma supp_abs_subset1:
assumes a: "finite (supp x)"
shows "(supp x) - as \<subseteq> supp (Abs as x)"
@@ -430,14 +419,6 @@
unfolding supp_abs
by auto
-lemma abs_eq_iff:
- 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)
- apply(lifting alphas_abs)
- done
-
section {* BELOW is stuff that may or may not be needed *}