author urbanc Sun, 25 Mar 2007 15:15:07 +0200 changeset 22514 4dfa84906915 parent 22513 651777b8dc30 child 22515 f4061faa5fda
moving lemmas into appropriate sections
```--- 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 @@
done

+lemma imp_eqvt:
+  shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
+
+lemma conj_eqvt:
+  shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
+
+lemma disj_eqvt:
+  shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))"
+
+lemma neg_eqvt:
+  shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))"
+
(* 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(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))"
-
-lemma conj_eqvt:
-  fixes pi::"'x prm"
-  shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
-
-lemma disj_eqvt:
-  fixes pi::"'x prm"
-  shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))"