nominal2: comparison Nominal/Nominal2

equal deleted inserted replaced

-:c9a1c6f50ff5
+:cf451e182bf0
 lemma [mono]:
 shows "R1 \<le> R2 \<Longrightarrow> alpha_set bs R1 \<le> alpha_set bs R2"
 and   "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
 and   "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
 by (case_tac [!] bs, case_tac [!] cs)
-(auto simp add: le_fun_def le_bool_def alphas)
+(auto simp: le_fun_def le_bool_def alphas)
 section {* Equivariance *}
 lemma alpha_eqvt[eqvt]:
 shows "(bs, x) \<approx>set R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>set (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
 shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set 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)"
 unfolding alphas fresh_star_def
 using a
-by (auto simp add: fresh_minus_perm)
+by (auto simp: fresh_minus_perm)
 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>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set 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   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
 unfolding alphas_abs
 unfolding alphas
 unfolding fresh_star_def
 by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
-(auto simp add: fresh_minus_perm)
+(auto simp: fresh_minus_perm)
 lemma alphas_abs_trans:
 shows "\<lbrakk>(bs, x) \<approx>abs_set (cs, y); (cs, y) \<approx>abs_set (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_set (ds, z)"
 and   "\<lbrakk>(bs, x) \<approx>abs_res (cs, y); (cs, y) \<approx>abs_res (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_res (ds, z)"
 and   "\<lbrakk>(es, x) \<approx>abs_lst (gs, y); (gs, y) \<approx>abs_lst (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>abs_lst (hs, z)"
 by (simp add: atom_set_perm_eq)
 obtain p where *: "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" and **: "supp p \<subseteq> supp x \<union> p' \<bullet> supp x"
 using set_renaming_perm2 by blast
 from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
 from 0 have 1: "(supp x - as) \<sharp>* p" using *
-by (auto simp add: fresh_star_def fresh_perm)
+by (auto simp: fresh_star_def fresh_perm)
 then have 2: "(supp x - as) \<inter> supp p = {}"
-by (auto simp add: fresh_star_def fresh_def)
+by (auto simp: fresh_star_def fresh_def)
 have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
 have "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" using ** by simp
 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as)))"
 using b by simp
 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> ((p' \<bullet> (supp x - as)) \<union> (p' \<bullet> (supp x \<inter> as)))"
 qed
 lemma alpha_abs_res_minimal:
 assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
 shows "(as \<inter> supp x, x) \<approx>res (op =) supp p (as' \<inter> supp x', x')"
-using asm unfolding alpha_res by (auto simp add: Diff_Int)
+using asm unfolding alpha_res by (auto simp: Diff_Int)
 lemma alpha_abs_res_abs_set:
 assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
 shows "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
 proof -
 qed
 lemma alpha_abs_set_abs_res:
 assumes asm: "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
 shows "(as, x) \<approx>res (op =) supp p (as', x')"
-using asm unfolding alphas by (auto simp add: Diff_Int)
+using asm unfolding alphas by (auto simp: Diff_Int)
 lemma alpha_abs_res_stronger1:
 assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
 shows "\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as'"
 using alpha_abs_res_stronger1_aux[OF asm] by auto
 using set_renaming_perm2 by blast
 from * have "\<forall>b \<in> supp x. p \<bullet> b = p' \<bullet> b" by blast
 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
 from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
 then have zb: "p \<bullet> as = p' \<bullet> as"
-apply(auto simp add: permute_set_def)
+apply(auto simp: permute_set_def)
 apply(rule_tac x="xa" in exI)
 apply(simp)
 done
 have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)
 from 0 have 1: "(supp x - as) \<sharp>* p" using *
-by (auto simp add: fresh_star_def fresh_perm)
+by (auto simp: fresh_star_def fresh_perm)
 then have 2: "(supp x - as) \<inter> supp p = {}"
-by (auto simp add: fresh_star_def fresh_def)
+by (auto simp: fresh_star_def fresh_def)
 have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
 have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast
 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as))) \<union> p' \<bullet> as"
 using b by simp
 also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union>
 then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
 from * have "\<forall>b \<in> set as. p \<bullet> b = p' \<bullet> b" by blast
 then have zb: "p \<bullet> as = p' \<bullet> as" by (induct as) (auto)
 have zc: "p' \<bullet> set as = set as'" using asm by (simp add: alphas set_eqvt)
 from 0 have 1: "(supp x - set as) \<sharp>* p" using *
-by (auto simp add: fresh_star_def fresh_perm)
+by (auto simp: fresh_star_def fresh_perm)
 then have 2: "(supp x - set as) \<inter> supp p = {}"
-by (auto simp add: fresh_star_def fresh_def)
+by (auto simp: fresh_star_def fresh_def)
 have b: "supp x = (supp x - set as) \<union> (supp x \<inter> set as)" by auto
 have "supp p \<subseteq> supp x \<union> set as \<union> p' \<bullet> supp x \<union> p' \<bullet> set as" using ** using union_eqvt by blast
 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union>
 (p' \<bullet> ((supp x - set as) \<union> (supp x \<inter> set as))) \<union> p' \<bullet> set as" using b by simp
 also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union>
 shows "(as, x) \<approx>abs_set (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>set (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')"
 and   "(as, x) \<approx>abs_res (as', x') \<longleftrightarrow> (\<exists>p. (as, x) \<approx>res (op =) supp p (as', x') \<and> supp p \<subseteq> as \<union> as')"
 and   "(bs, x) \<approx>abs_lst (bs', x') \<longleftrightarrow>
 (\<exists>p. (bs, x) \<approx>lst (op =) supp p (bs', x') \<and> supp p \<subseteq> set bs \<union> set bs')"
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_set_stronger1)[1]
+apply(auto simp: alphas_abs alpha_abs_set_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs)[1]
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_res_stronger1)[1]
+apply(auto simp: alphas_abs alpha_abs_res_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs)[1]
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1]
+apply(auto simp: alphas_abs alpha_abs_lst_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs)[1]
 done
 lemma alpha_res_alpha_set:
 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
 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)
+(auto simp: supp_perm swap_atom)
 lemma Abs_swap2:
 assumes a1: "a \<notin> (supp x) - (set bs)"
 and     a2: "b \<notin> (supp x) - (set bs)"
 shows "[bs]lst. x = [(a \<rightleftharpoons> b) \<bullet> bs]lst. ((a \<rightleftharpoons> b) \<bullet> x)"
 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)
+(auto simp: supp_perm swap_atom)
 lemma Abs_supports:
 shows "((supp x) - as) supports ([as]set. x)"
 and   "((supp x) - as) supports ([as]res. x)"
 and   "((supp x) - set bs) supports ([bs]lst. x)"
 fixes x::"'a::fs"
 shows "as \<sharp>* ([bs]set. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
 and   "as \<sharp>* ([bs]res. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
 and   "as \<sharp>* ([cs]lst. x) \<longleftrightarrow> (as - set cs) \<sharp>* x"
 unfolding fresh_star_def
-by (auto simp add: Abs_fresh_iff)
+by (auto simp: Abs_fresh_iff)
 lemma Abs_fresh_star:
 fixes x::"'a::fs"
 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']set. x)"
 and   "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']res. x)"
 and   "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* ([bs']lst. x)"
 unfolding fresh_star_def
-by(auto simp add: Abs_fresh_iff)
+by(auto simp: Abs_fresh_iff)
 lemma Abs_fresh_star2:
 fixes x::"'a::fs"
 shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]set. x) \<longleftrightarrow> as \<sharp>* x"
 and   "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]res. x) \<longleftrightarrow> as \<sharp>* x"
 fixes x y::"'a::fs"
 shows "[{atom a}]set. x = [{atom a}]set. y \<longleftrightarrow> x = y"
 and   "[{atom a}]res. x = [{atom a}]res. y \<longleftrightarrow> x = y"
 and   "[[atom a]]lst. x = [[atom a]]lst. y \<longleftrightarrow> x = y"
 unfolding Abs_eq_iff2 alphas
-by (auto simp add: supp_perm_singleton fresh_star_def fresh_zero_perm)
+by (auto simp: supp_perm_singleton fresh_star_def fresh_zero_perm)
 lemma Abs1_eq_iff_fresh:
 fixes x y::"'a::fs"
 and a b c::"'b::at"
 assumes "atom c \<sharp> (a, b, x, y)"
 lemma Abs1_eq_iff_all:
 fixes x y::"'a::fs"
 and z::"'c::fs"
 and a b::"'b::at"
-shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
-and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
-and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
 apply(auto)
 apply(simp add: Abs1_eq_iff_fresh(1)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(1))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 apply(simp add: Abs1_eq_iff_fresh(2)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(2))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 apply(simp add: Abs1_eq_iff_fresh(3)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(3))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 done
 lemma Abs1_eq_iff:
 fixes x y::"'a::fs"
 and a b::"'b::at"
 fixes x::"'a::fs"
 and a b::"'b::at"
 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
 and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
 and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
-using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
+using assms by (auto simp: Abs1_eq_iff fresh_permute_left)
 ML {*
 fun alpha_single_simproc thm _ ctxt ctrm =
 let
 by (perm_simp) (rule refl)
 lemma prod_fv_supp:
 shows "prod_fv supp supp = supp"
 by (rule ext)
-(auto simp add: supp_Pair)
+(auto simp: supp_Pair)
 lemma prod_alpha_eq:
 shows "prod_alpha (op=) (op=) = (op=)"
 unfolding prod_alpha_def
 by (auto intro!: ext)

changeset 3224	cf451e182bf0
parent 3218	89158f401b07
child 3229	b52e8651591f