equal
deleted
inserted
replaced
122 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))" |
122 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))" |
123 by (perm_simp add: permute_minus_cancel) (rule refl) |
123 by (perm_simp add: permute_minus_cancel) (rule refl) |
124 |
124 |
125 lemma the_eqvt: |
125 lemma the_eqvt: |
126 assumes unique: "\<exists>!x. P x" |
126 assumes unique: "\<exists>!x. P x" |
|
127 shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)" |
|
128 apply(rule the1_equality [symmetric]) |
|
129 apply(rule_tac p="-p" in permute_boolE) |
|
130 apply(perm_simp add: permute_minus_cancel) |
|
131 apply(rule unique) |
|
132 apply(rule_tac p="-p" in permute_boolE) |
|
133 apply(perm_simp add: permute_minus_cancel) |
|
134 apply(rule theI'[OF unique]) |
|
135 done |
|
136 |
|
137 lemma the_eqvt2: |
|
138 assumes unique: "\<exists>!x. P x" |
127 shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))" |
139 shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))" |
128 apply(rule the1_equality [symmetric]) |
140 apply(rule the1_equality [symmetric]) |
129 apply(simp add: ex1_eqvt2[symmetric]) |
141 apply(simp add: ex1_eqvt2[symmetric]) |
130 apply(simp add: permute_bool_def unique) |
142 apply(simp add: permute_bool_def unique) |
131 apply(simp add: permute_bool_def) |
143 apply(simp add: permute_bool_def) |