# HG changeset patch
# User urbanc
# Date 1160744494 -7200
# Node ID 7fe928722821491454cd5cc9a1f2e50658f4e025
# Parent  0eae3fb489361be11647539e5475b50087319873
added the missing freshness-lemmas for nat, int, char and string and
also the lemma for permutation acting on if's

diff -r 0eae3fb48936 -r 7fe928722821 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Oct 13 12:32:44 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Fri Oct 13 15:01:34 2006 +0200
@@ -97,7 +97,15 @@
   shows "P"
   using a by (simp add: perm_bool)
 
+lemma perm_if:
+  fixes pi::"'a prm"
+  shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))"
+apply(simp add: perm_fun_def)
+done
+
+
 (* permutation on options *)
+
 primrec (unchecked perm_option)
   perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
   perm_none_def:  "pi\<bullet>None    = None"
@@ -300,6 +308,34 @@
   apply(simp add: fresh_def supp_some)
   done
 
+lemma fresh_int:
+  fixes a :: "'x"
+  and   i :: "int"
+  shows "a\<sharp>i"
+  apply(simp add: fresh_def supp_int)
+  done
+
+lemma fresh_nat:
+  fixes a :: "'x"
+  and   n :: "nat"
+  shows "a\<sharp>n"
+  apply(simp add: fresh_def supp_nat)
+  done
+
+lemma fresh_char:
+  fixes a :: "'x"
+  and   c :: "char"
+  shows "a\<sharp>c"
+  apply(simp add: fresh_def supp_char)
+  done
+
+lemma fresh_string:
+  fixes a :: "'x"
+  and   s :: "string"
+  shows "a\<sharp>s"
+  apply(simp add: fresh_def supp_string)
+  done
+
 text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
 
 lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"