# HG changeset patch
# User urbanc
# Date 1179661186 -7200
# Node ID 722f583795384f96fdfe118ef9ba81def05ee549
# Parent  11607c283074d278ade249c8bec1f12af7fc078e
added lemma for permutations on strings

diff -r 11607c283074 -r 722f58379538 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sun May 20 10:13:06 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Sun May 20 13:39:46 2007 +0200
@@ -150,7 +150,12 @@
 
 (* permutation on characters (used in strings) *)
 defs (unchecked overloaded)
-  perm_char_def: "pi\<bullet>(s::char) \<equiv> s"
+  perm_char_def: "pi\<bullet>(c::char) \<equiv> c"
+
+lemma perm_string:
+  fixes s::"string"
+  shows "pi\<bullet>s = s"
+by (induct s)(auto simp add: perm_char_def)
 
 (* permutation on ints *)
 defs (unchecked overloaded)
@@ -272,8 +277,7 @@
 lemma supp_string:
   fixes s::"string"
   shows "supp (s) = {}"
-apply(induct s)
-apply(auto simp add: supp_char supp_list_nil supp_list_cons)
+apply(simp add: supp_def perm_string)
 done
 
 lemma fresh_set_empty: