equal
deleted
inserted
replaced
3052 definition |
3052 definition |
3053 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
3053 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
3054 where |
3054 where |
3055 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
3055 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
3056 |
3056 |
|
3057 lemma flip_fresh_fresh: |
|
3058 assumes "atom a \<sharp> x" "atom b \<sharp> x" |
|
3059 shows "(a \<leftrightarrow> b) \<bullet> x = x" |
|
3060 using assms |
|
3061 by (simp add: flip_def swap_fresh_fresh) |
|
3062 |
3057 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0" |
3063 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0" |
3058 unfolding flip_def by (rule swap_self) |
3064 unfolding flip_def by (rule swap_self) |
3059 |
3065 |
3060 lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)" |
3066 lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)" |
3061 unfolding flip_def by (rule swap_commute) |
3067 unfolding flip_def by (rule swap_commute) |
3071 |
3077 |
3072 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x" |
3078 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x" |
3073 by (simp add: flip_commute) |
3079 by (simp add: flip_commute) |
3074 |
3080 |
3075 lemma flip_eqvt [eqvt]: |
3081 lemma flip_eqvt [eqvt]: |
3076 fixes a b c::"'a::at_base" |
|
3077 shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)" |
3082 shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)" |
3078 unfolding flip_def |
3083 unfolding flip_def |
3079 by (simp add: swap_eqvt atom_eqvt) |
3084 by (simp add: swap_eqvt atom_eqvt) |
3080 |
3085 |
3081 lemma flip_at_base_simps [simp]: |
3086 lemma flip_at_base_simps [simp]: |
3089 by simp_all |
3094 by simp_all |
3090 |
3095 |
3091 text {* the following two lemmas do not hold for at_base, |
3096 text {* the following two lemmas do not hold for at_base, |
3092 only for single sort atoms from at *} |
3097 only for single sort atoms from at *} |
3093 |
3098 |
|
3099 lemma flip_triple: |
|
3100 fixes a b c::"'a::at" |
|
3101 assumes "a \<noteq> b" and "c \<noteq> b" |
|
3102 shows "(a \<leftrightarrow> c) + (b \<leftrightarrow> c) + (a \<leftrightarrow> c) = (a \<leftrightarrow> b)" |
|
3103 unfolding flip_def |
|
3104 by (rule swap_triple) (simp_all add: assms) |
|
3105 |
3094 lemma permute_flip_at: |
3106 lemma permute_flip_at: |
3095 fixes a b c::"'a::at" |
3107 fixes a b c::"'a::at" |
3096 shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)" |
3108 shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)" |
3097 unfolding flip_def |
3109 unfolding flip_def |
3098 apply (rule atom_eq_iff [THEN iffD1]) |
3110 apply (rule atom_eq_iff [THEN iffD1]) |
3103 lemma flip_at_simps [simp]: |
3115 lemma flip_at_simps [simp]: |
3104 fixes a b::"'a::at" |
3116 fixes a b::"'a::at" |
3105 shows "(a \<leftrightarrow> b) \<bullet> a = b" |
3117 shows "(a \<leftrightarrow> b) \<bullet> a = b" |
3106 and "(a \<leftrightarrow> b) \<bullet> b = a" |
3118 and "(a \<leftrightarrow> b) \<bullet> b = a" |
3107 unfolding permute_flip_at by simp_all |
3119 unfolding permute_flip_at by simp_all |
3108 |
|
3109 lemma flip_fresh_fresh: |
|
3110 fixes a b::"'a::at_base" |
|
3111 assumes "atom a \<sharp> x" "atom b \<sharp> x" |
|
3112 shows "(a \<leftrightarrow> b) \<bullet> x = x" |
|
3113 using assms |
|
3114 by (simp add: flip_def swap_fresh_fresh) |
|
3115 |
|
3116 |
3120 |
3117 |
3121 |
3118 subsection {* Syntax for coercing at-elements to the atom-type *} |
3122 subsection {* Syntax for coercing at-elements to the atom-type *} |
3119 |
3123 |
3120 syntax |
3124 syntax |