# HG changeset patch
# User urbanc
# Date 1189088922 -7200
# Node ID da7de38392df7f755e296f53467a7280cdb7bf57
# Parent  e2332d1ff6c77e706312551e5fde137bdaab80a6
trivial cleaning up

diff -r e2332d1ff6c7 -r da7de38392df src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Sep 06 12:30:41 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 06 16:28:42 2007 +0200
@@ -24,8 +24,8 @@
   perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
   swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
 
-(* for the decision procedure involving permutations *)
-(* (to make the perm-composition to be terminating   *)
+(* an auxiliary constant for the decision procedure involving *) 
+(* permutations (to avoid loops when using perm-composition)  *)
 constdefs
   "perm_aux pi x \<equiv> pi\<bullet>x"
 
@@ -1107,6 +1107,10 @@
 apply(simp_all add: pt3[OF pta])
 done
 
+lemma pt_bool_inst:
+  shows  "pt TYPE(bool) TYPE('x)"
+  by (simp add: pt_def perm_bool)
+
 section {* further lemmas for permutation types *}
 (*==============================================*)
 
@@ -1993,17 +1997,15 @@
   and     a: "\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y"
   shows "pi\<bullet>y = y"
 proof(induct pi)
-    case Nil show ?case by (simp add: pt1[OF pt])
-  next
-    case (Cons x xs)
-    have "\<exists>a b. x=(a,b)" by force
-    then obtain a b where p: "x=(a,b)" by force
-    assume i: "xs\<bullet>y = y"
-    have "x#xs = [x]@xs" by simp
-    hence "(x#xs)\<bullet>y = ([x]@xs)\<bullet>y" by simp
-    hence "(x#xs)\<bullet>y = [x]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
-    thus ?case using a i p by force
-  qed
+  case Nil show ?case by (simp add: pt1[OF pt])
+next
+  case (Cons x xs)
+  have ih: "xs\<bullet>y = y" by fact
+  obtain a b where p: "x=(a,b)" by force
+  have "((a,b)#xs)\<bullet>y = ([(a,b)]@xs)\<bullet>y" by simp
+  also have "\<dots> = [(a,b)]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
+  finally show ?case using a ih p by simp
+qed
 
 lemma pt_swap_eq:
   fixes   y :: "'a"