# HG changeset patch
# User urbanc
# Date 1174828507 -7200
# Node ID 4dfa849069153d6ddde90da13371b8d315f3d812
# Parent  651777b8dc304dd7430b150003d3a7cec4464dda
moving lemmas into appropriate sections

diff -r 651777b8dc30 -r 4dfa84906915 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Mar 23 12:06:41 2007 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Sun Mar 25 15:15:07 2007 +0200
@@ -110,6 +110,22 @@
 apply(simp add: perm_fun_def)
 done
 
+lemma imp_eqvt:
+  shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
+  by (simp add: perm_bool)
+
+lemma conj_eqvt:
+  shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
+  by (simp add: perm_bool)
+
+lemma disj_eqvt:
+  shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))"
+  by (simp add: perm_bool)
+
+lemma neg_eqvt:
+  shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))"
+  by (simp add: perm_bool)
+
 (* permutation on options *)
 
 primrec (unchecked perm_option)
@@ -1678,7 +1694,6 @@
 qed
 
 section {* equivaraince for some connectives *}
-(* FIXME: maybe not really needed *)
 
 lemma pt_all_eqvt:
   fixes  pi :: "'x prm"
@@ -1696,32 +1711,12 @@
   and     x :: "'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and     at: "at TYPE('x)"
-  shows "pi\<bullet>(\<exists>(x::'a). P x) = (\<exists> (x::'a). (pi\<bullet>P) x)"
+  shows "pi\<bullet>(\<exists>(x::'a). P x) = (\<exists>(x::'a). (pi\<bullet>P) x)"
 apply(auto simp add: perm_bool perm_fun_def)
 apply(rule_tac x="pi\<bullet>x" in exI) 
 apply(simp add: pt_rev_pi[OF pt, OF at])
 done
 
-lemma imp_eqvt:
-  fixes pi::"'x prm"
-  shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
-  by (simp add: perm_bool)
-
-lemma conj_eqvt:
-  fixes pi::"'x prm"
-  shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
-  by (simp add: perm_bool)
-
-lemma disj_eqvt:
-  fixes pi::"'x prm"
-  shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))"
-  by (simp add: perm_bool)
-
-lemma neg_eqvt:
-  fixes pi::"'x prm"
-  shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))"
-  by (simp add: perm_bool)
-
 section {* facts about supports *}
 (*==============================*)