author urbanc Tue, 01 Nov 2005 23:55:53 +0100 changeset 18053 2719a6b7d95e parent 18052 004515accc10 child 18054 2493cb9f5ede
some minor tweaks in some proofs (nothing extraordinary)
```--- a/src/HOL/Nominal/Nominal.thy	Tue Nov 01 23:54:29 2005 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Tue Nov 01 23:55:53 2005 +0100
@@ -293,9 +293,9 @@
case Nil show ?case by (simp add: at1[OF at])
next
case (Cons x xs)
-  assume i: "(xs @ pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)"
-  have "(x#xs)@pi2 = x#(xs@pi2)" by simp
-  thus ?case using i by (cases "x", simp add:  at2[OF at])
+  have "(xs@pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)" by fact
+  also have "(x#xs)@pi2 = x#(xs@pi2)" by simp
+  ultimately show ?case by (cases "x", simp add:  at2[OF at])
qed

lemma at_swap:
@@ -551,7 +551,7 @@
apply(auto simp only: pt_def)
apply(simp only: at1[OF at])
apply(simp only: at_append[OF at])
+apply(simp only: prm_eq_def)
done

section {* finite support properties *}
@@ -895,7 +895,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and     at: "at TYPE('x)"
shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
-  by (simp add: perm_set_def pt_set_bij1[OF pt, OF at] pt_bij[OF pt, OF at])
+  by (simp add: perm_set_def pt_bij[OF pt, OF at])

lemma pt_set_bij2:
fixes pi :: "'x prm"
@@ -1266,7 +1266,7 @@
and   S1 :: "'x set"
and   S2 :: "'x set"
assumes  a: "S1 supports x"
-  and      b: "S1\<subseteq>S2"
+  and      b: "S1 \<subseteq> S2"
shows "S2 supports x"
using a b
by (force simp add: "op supports_def")```