# HG changeset patch
# User urbanc
# Date 1136995950 -3600
# Node ID 32722023ff90f85e24069e823fc12537e93f2631
# Parent  73cebafb9a8981649fb19cd43bc3815dcfd0e9b5
added lemmas perm_empty, perm_insert to do with
permutations on sets

diff -r 73cebafb9a89 -r 32722023ff90 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Jan 11 17:10:11 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Jan 11 17:12:30 2006 +0100
@@ -26,10 +26,18 @@
 defs (overloaded)
   perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
 
+lemma perm_empty:
+  shows "pi\<bullet>{} = {}"
+  by (simp add: perm_set_def)
+
 lemma perm_union:
   shows "pi \<bullet> (X \<union> Y) = (pi \<bullet> X) \<union> (pi \<bullet> Y)"
   by (auto simp add: perm_set_def)
 
+lemma perm_insert:
+  shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)"
+  by (auto simp add: perm_set_def)
+
 (* permutation on units and products *)
 primrec (perm_unit)
   "pi\<bullet>()    = ()"
@@ -77,6 +85,7 @@
   by (cases "b", auto)
 
 (* permutation on options *)
+
 primrec (perm_option)
   perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
   perm_none_def:  "pi\<bullet>None    = None"
@@ -271,10 +280,10 @@
 
 text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
 
-lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) == PROP C"
+lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_def supp_unit)
 
-lemma fresh_prod_elim: "(a\<sharp>(x,y) \<Longrightarrow> PROP C) == (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
+lemma fresh_prod_elim: "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
   by rule (simp_all add: fresh_prod)
 
 
@@ -991,8 +1000,6 @@
   fixes pi :: "'x prm"
   and   x  :: "'a"
   and   X  :: "'a set"
-  assumes pt: "pt TYPE('a) TYPE('x)"
-  and     at: "at TYPE('x)"
   shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
 apply(case_tac "x\<in>X = True")
 apply(auto)