--- a/src/HOL/Nominal/Nominal.thy Fri May 02 18:42:17 2008 +0200
+++ b/src/HOL/Nominal/Nominal.thy Fri May 02 22:43:14 2008 +0200
@@ -1327,14 +1327,13 @@
shows "(pi\<bullet>x)\<in>X"
using a by (simp add: pt_set_bij1[OF pt, OF at])
+(* FIXME: is this lemma needed anywhere? *)
lemma pt_set_bij3:
fixes pi :: "'x prm"
and x :: "'a"
and X :: "'a set"
shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
-apply(case_tac "x\<in>X = True")
-apply(auto)
-done
+by (simp add: perm_bool)
lemma pt_subseteq_eqvt:
fixes pi :: "'x prm"
@@ -1529,6 +1528,35 @@
apply(simp add: pt_rev_pi[OF ptb, OF at])
done
+lemma pt_fresh_star_bij_ineq:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'y set"
+ and b :: "'y list"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
+ and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
+apply(unfold fresh_star_def)
+apply(auto)
+apply(drule_tac x="pi\<bullet>xa" in bspec)
+apply(rule pt_set_bij2[OF ptb, OF at])
+apply(assumption)
+apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="pi\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at])
+apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
+apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
+apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt)
+apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
+done
+
lemma pt_fresh_left:
fixes pi :: "'x prm"
and x :: "'a"
@@ -1577,6 +1605,31 @@
apply(rule at)
done
+lemma pt_fresh_star_bij:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x set"
+ and b :: "'x list"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
+ and "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
+apply(rule pt_fresh_star_bij_ineq(1))
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+apply(rule pt_fresh_star_bij_ineq(2))
+apply(rule pt)
+apply(rule at_pt_inst)
+apply(rule at)+
+apply(rule cp_pt_inst)
+apply(rule pt)
+apply(rule at)
+done
+
lemma pt_fresh_bij1:
fixes pi :: "'x prm"
and x :: "'a"
@@ -1745,6 +1798,30 @@
thus ?thesis using eq3 by simp
qed
+lemma pt_pi_fresh_fresh:
+ fixes x :: "'a"
+ and pi :: "'x prm"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE ('x)"
+ and a: "\<forall>(a,b)\<in>set pi. a\<sharp>x \<and> b\<sharp>x"
+ shows "pi\<bullet>x=x"
+using a
+proof (induct pi)
+ case Nil
+ show "([]::'x prm)\<bullet>x = x" by (rule pt1[OF pt])
+next
+ case (Cons ab pi)
+ have a: "\<forall>(a,b)\<in>set (ab#pi). a\<sharp>x \<and> b\<sharp>x" by fact
+ have ih: "(\<forall>(a,b)\<in>set pi. a\<sharp>x \<and> b\<sharp>x) \<Longrightarrow> pi\<bullet>x=x" by fact
+ obtain a b where e: "ab=(a,b)" by (cases ab) (auto)
+ from a have a': "a\<sharp>x" "b\<sharp>x" using e by auto
+ have "(ab#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x" using e by simp
+ also have "\<dots> = [(a,b)]\<bullet>(pi\<bullet>x)" by (simp only: pt2[OF pt])
+ also have "\<dots> = [(a,b)]\<bullet>x" using ih a by simp
+ also have "\<dots> = x" using a' by (simp add: pt_fresh_fresh[OF pt, OF at])
+ finally show "(ab#pi)\<bullet>x = x" by simp
+qed
+
lemma pt_perm_compose:
fixes pi1 :: "'x prm"
and pi2 :: "'x prm"
--- a/src/HOL/Nominal/nominal_atoms.ML Fri May 02 18:42:17 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Fri May 02 22:43:14 2008 +0200
@@ -746,6 +746,8 @@
val fresh_right = @{thm "Nominal.pt_fresh_right"};
val fresh_bij_ineq = @{thm "Nominal.pt_fresh_bij_ineq"};
val fresh_bij = @{thm "Nominal.pt_fresh_bij"};
+ val fresh_star_bij_ineq = @{thms "Nominal.pt_fresh_star_bij_ineq"};
+ val fresh_star_bij = @{thms "Nominal.pt_fresh_star_bij"};
val fresh_eqvt = @{thm "Nominal.pt_fresh_eqvt"};
val fresh_eqvt_ineq = @{thm "Nominal.pt_fresh_eqvt_ineq"};
val set_diff_eqvt = @{thm "Nominal.pt_set_diff_eqvt"};
@@ -775,6 +777,10 @@
(* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *)
fun instR thm thms = map (fn ti => ti RS thm) thms;
+ (* takes a theorem thm and a list of theorems [(t1,m1),..,(tn,mn)] *)
+ (* produces a list of theorems of the form [[t1,m1] MRS thm,..,[tn,mn] MRS thm] *)
+ fun instRR thm thms = map (fn (ti,mi) => [ti,mi] MRS thm) thms;
+
(* takes two theorem lists (hopefully of the same length ;o) *)
(* produces a list of theorems of the form *)
(* [t1 RS m1,..,tn RS mn] where [t1,..,tn] is thms1 and [m1,..,mn] is thms2 *)
@@ -817,7 +823,7 @@
fun inst_at thms = maps (fn ti => instR ti ats) thms;
fun inst_fs thms = maps (fn ti => instR ti fss) thms;
fun inst_cp thms cps = flat (inst_mult thms cps);
- fun inst_pt_at thms = inst_zip ats (inst_pt thms);
+ fun inst_pt_at thms = maps (fn ti => instRR ti (pts ~~ ats)) thms;
fun inst_dj thms = maps (fn ti => instR ti djs) thms;
fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps;
fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms));
@@ -897,6 +903,10 @@
and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
in [(("fresh_bij", thms1 @ thms2),[])] end
||>> PureThy.add_thmss
+ let val thms1 = inst_pt_at fresh_star_bij
+ and thms2 = flat (map (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq);
+ in [(("fresh_star_bij", thms1 @ thms2),[])] end
+ ||>> PureThy.add_thmss
let val thms1 = inst_pt_at [fresh_eqvt]
and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end