Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Nominal2_Eqvt.thy
changeset 2651 4aa72a88b2c1
parent 2642 f338b455314c
child 2658 b4472ebd7fad 
--- a/Nominal/Nominal2_Eqvt.thy	Fri Jan 07 02:30:00 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Fri Jan 07 05:06:25 2011 +0000
@@ -124,6 +124,18 @@
 
 lemma the_eqvt:
   assumes unique: "\<exists>!x. P x"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)"
+  apply(rule the1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule unique)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule theI'[OF unique])
+  done
+
+lemma the_eqvt2:
+  assumes unique: "\<exists>!x. P x"
   shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
   apply(rule the1_equality [symmetric])
   apply(simp add: ex1_eqvt2[symmetric])
nominal2