author urbanc Sun, 19 Feb 2006 17:18:39 +0100 changeset 19107 b16a45c53884 parent 19106 6e6b5b1fdc06 child 19108 6f8c1343341b
added a few lemmas to do with permutation-equivalence for the recursion combinator
```--- a/src/HOL/Nominal/Nominal.thy	Sun Feb 19 13:21:32 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Sun Feb 19 17:18:39 2006 +0100
@@ -453,11 +453,13 @@
shows "(a\<sharp>b) = (a\<noteq>b)"
by (simp add: at_supp[OF at] fresh_def)

-lemma at_prm_fresh[rule_format]:
+lemma at_prm_fresh:
fixes c :: "'x"
and   pi:: "'x prm"
assumes at: "at TYPE('x)"
-  shows "c\<sharp>pi \<longrightarrow> pi\<bullet>c = c"
+  and     a: "c\<sharp>pi"
+  shows "pi\<bullet>c = c"
+using a
apply(induct pi)
apply(force simp add: fresh_list_cons at2[OF at] fresh_prod at_fresh[OF at] at3[OF at])
@@ -467,7 +469,7 @@
fixes pi1 :: "'x prm"
and   pi2 :: "'x prm"
assumes at: "at TYPE('x)"
-  shows a: "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)"
+  shows "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)"
fix x
assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
@@ -483,7 +485,30 @@
hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at])
thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp
qed
+
+lemma at_prm_eq_append:
+  fixes pi1 :: "'x prm"
+  and   pi2 :: "'x prm"
+  and   pi3 :: "'x prm"
+  assumes at: "at TYPE('x)"
+  and     a: "pi1 \<triangleq> pi2"
+  shows "(pi3@pi1) \<triangleq> (pi3@pi2)"
+using a by (simp add: prm_eq_def at_append[OF at] at_bij[OF at])
+
+lemma at_prm_eq_trans:
+  fixes pi1 :: "'x prm"
+  and   pi2 :: "'x prm"
+  and   pi3 :: "'x prm"
+  assumes a1: "pi1 \<triangleq> pi2"
+  and     a2: "pi2 \<triangleq> pi3"
+  shows "pi1 \<triangleq> pi3"
+using a1 a2 by (auto simp add: prm_eq_def)

+lemma at_prm_eq_refl:
+  fixes pi :: "'x prm"
+  shows "pi \<triangleq> pi"
+
lemma at_prm_rev_eq1:
fixes pi1 :: "'x prm"
and   pi2 :: "'x prm"
@@ -502,7 +527,7 @@
and   a  :: "'x"
and   b  :: "'x"
assumes at: "at TYPE('x)"
-  shows "(pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)]) \<triangleq> ([(a,b)]@pi)"
+  shows "([(a,b)]@pi) \<triangleq> (pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)])"
by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at]
at_rev_pi[OF at] at_calc[OF at])

@@ -593,6 +618,23 @@
done

+lemma at_ds10:
+  fixes pi1 :: "'x prm"
+  and   pi2 :: "'x prm"
+  and   a  :: "'x"
+  and   b  :: "'x"
+  assumes at: "at TYPE('x)"
+  and     a:  "b\<sharp>(rev pi1)"
+  shows "(pi2@([(pi1\<bullet>a,b)]@pi1)) \<triangleq> (pi2@(pi1@[(a,b)]))"
+using a
+apply -
+apply(rule at_prm_eq_append[OF at])
+apply(rule at_prm_eq_trans)
+apply(rule at_ds2[OF at])
+apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at])
+apply(rule at_prm_eq_refl)
+done
+
--"there always exists an atom not being in a finite set"
lemma ex_in_inf:
fixes   A::"'x set"```