--- a/Nominal/Abs.thy Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/Abs.thy Tue Jul 27 14:37:59 2010 +0200
@@ -43,7 +43,8 @@
alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100)
-(* monos *)
+section {* Mono *}
+
lemma [mono]:
shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
and "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
@@ -51,8 +52,9 @@
by (case_tac [!] bs, case_tac [!] cs)
(auto simp add: le_fun_def le_bool_def alphas)
-(* equivariance *)
-lemma alpha_gen_eqvt[eqvt]:
+section {* Equivariance *}
+
+lemma alpha_eqvt[eqvt]:
shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
@@ -63,8 +65,10 @@
unfolding Diff_eqvt[symmetric]
by (auto simp add: permute_bool_def fresh_star_permute_iff)
-(* equivalence *)
-lemma alpha_gen_refl:
+
+section {* Equivalence *}
+
+lemma alpha_refl:
assumes a: "R x x"
shows "(bs, x) \<approx>gen R f 0 (bs, x)"
and "(bs, x) \<approx>res R f 0 (bs, x)"
@@ -74,7 +78,7 @@
unfolding fresh_star_def
by (simp_all add: fresh_zero_perm)
-lemma alpha_gen_sym:
+lemma alpha_sym:
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
@@ -83,13 +87,22 @@
using a
by (auto simp add: fresh_minus_perm)
-lemma alpha_gen_sym_eqvt:
+lemma alpha_trans:
+ assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
+ shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+ and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
+ and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
+ using a
+ unfolding alphas fresh_star_def
+ by (simp_all add: fresh_plus_perm)
+
+lemma alpha_sym_eqvt:
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
and b: "p \<bullet> R = R"
shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
-apply(auto intro!: alpha_gen_sym)
+apply(auto intro!: alpha_sym)
apply(drule_tac [!] a)
apply(rule_tac [!] p="p" in permute_boolE)
apply(perm_simp add: permute_minus_cancel b)
@@ -100,23 +113,13 @@
apply(assumption)
done
-lemma alpha_gen_trans:
- assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
- shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
- and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
- and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
- using a
- unfolding alphas fresh_star_def
- by (simp_all add: fresh_plus_perm)
-
-
lemma alpha_gen_trans_eqvt:
assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
and a: "(bs, x) \<approx>gen R f p (cs, y)"
and d: "q \<bullet> R = R"
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
-apply(rule alpha_gen_trans)
+apply(rule alpha_trans)
defer
apply(rule a)
apply(rule b)
@@ -136,7 +139,7 @@
and d: "q \<bullet> R = R"
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
-apply(rule alpha_gen_trans)
+apply(rule alpha_trans)
defer
apply(rule a)
apply(rule b)
@@ -156,7 +159,7 @@
and d: "q \<bullet> R = R"
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
-apply(rule alpha_gen_trans)
+apply(rule alpha_trans)
defer
apply(rule a)
apply(rule b)
@@ -172,12 +175,6 @@
lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
-lemma test:
- shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
- and "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
- and "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
- by (simp_all add: alphas)
-
section {* General Abstractions *}
@@ -206,6 +203,7 @@
lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
+
lemma alphas_abs_refl:
shows "(bs, x) \<approx>abs (bs, x)"
and "(bs, x) \<approx>abs_res (bs, x)"
@@ -284,7 +282,7 @@
and "(op= ===> op= ===> alpha_abs_res) Pair Pair"
and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
unfolding fun_rel_def
- by (auto intro: alphas_abs_refl simp only:)
+ by (auto intro: alphas_abs_refl)
lemma [quot_respect]:
shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
@@ -305,8 +303,7 @@
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)"
- unfolding alphas_abs
- by (lifting alphas_abs)
+ unfolding alphas_abs by (lifting alphas_abs)
instantiation abs_gen :: (pt) pt
begin
@@ -373,6 +370,7 @@
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"
@@ -405,7 +403,7 @@
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)"
+ 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])
@@ -525,6 +523,54 @@
unfolding supp_abs
by auto
+fun
+ prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+where
+ "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y"
+
+definition
+ prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+where
+ "prod_alpha = prod_rel"
+
+
+lemma [quot_respect]:
+ shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+ by auto
+
+lemma [quot_preserve]:
+ assumes q1: "Quotient R1 abs1 rep1"
+ and q2: "Quotient R2 abs2 rep2"
+ shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
+ by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+lemma [mono]:
+ shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+ unfolding prod_alpha_def
+ by auto
+
+lemma [eqvt]:
+ shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+ unfolding prod_alpha_def
+ unfolding prod_rel.simps
+ by (perm_simp) (rule refl)
+
+lemma [eqvt]:
+ shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+ unfolding prod_fv.simps
+ by (perm_simp) (rule refl)
+
+
+
+
+
+
+
+
+
+
+
+
section {* BELOW is stuff that may or may not be needed *}
lemma supp_atom_image:
@@ -579,97 +625,6 @@
R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
by (simp add: alphas)
-lemma alpha_gen_simpler:
- assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
- and fin_fv: "finite (f x)"
- and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
- shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
- (f x - bs) \<sharp>* pi \<and>
- R (pi \<bullet> x) y \<and>
- pi \<bullet> bs = cs"
- apply rule
- unfolding alpha_gen
- apply clarify
- apply (erule conjE)+
- apply (simp)
- apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")
- apply (rule sym)
- apply simp
- apply (rule supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (rule finite_Diff)
- apply (rule fin_fv)
- apply (assumption)
- apply (simp add: eqvts fv_eqvt)
- apply (subst fv_rsp)
- apply assumption
- apply (simp)
- done
-
-lemma alpha_lst_simpler:
- assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
- and fin_fv: "finite (f x)"
- and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
- shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
- (f x - set bs) \<sharp>* pi \<and>
- R (pi \<bullet> x) y \<and>
- pi \<bullet> bs = cs"
- apply rule
- unfolding alpha_lst
- apply clarify
- apply (erule conjE)+
- apply (simp)
- apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")
- apply (rule sym)
- apply simp
- apply (rule supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (rule finite_Diff)
- apply (rule fin_fv)
- apply (assumption)
- apply (simp add: eqvts fv_eqvt)
- apply (subst fv_rsp)
- apply assumption
- apply (simp)
- done
-
-fun
- prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
-where
- "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
-
-definition
- prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
-where
- "prod_alpha = prod_rel"
-
-
-lemma [quot_respect]:
- shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
- by auto
-
-lemma [quot_preserve]:
- assumes q1: "Quotient R1 abs1 rep1"
- and q2: "Quotient R2 abs2 rep2"
- shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
- by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
-
-lemma [mono]:
- shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
- unfolding prod_alpha_def
- by auto
-
-lemma [eqvt]:
- shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
- unfolding prod_alpha_def
- unfolding prod_rel.simps
- by (perm_simp) (rule refl)
-
-lemma [eqvt]:
- shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
- unfolding prod_fv.simps
- by (perm_simp) (rule refl)
-
end