--- a/src/HOL/Nominal/Nominal.thy Tue Apr 24 16:44:11 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Tue Apr 24 17:16:55 2007 +0200
@@ -1578,6 +1578,7 @@
(* the next two lemmas are needed in the proof *)
(* of the structural induction principle *)
+
lemma pt_fresh_aux:
fixes a::"'x"
and b::"'x"
@@ -1589,7 +1590,24 @@
shows "c\<sharp>([(a,b)]\<bullet>x)"
using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at])
-lemma pt_fresh_aux_ineq:
+lemma pt_fresh_perm_app:
+ fixes pi :: "'x prm"
+ and a :: "'x"
+ and x :: "'y"
+ assumes pt: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and h1: "a \<sharp> pi"
+ and h2: "a \<sharp> x"
+ shows "a \<sharp> (pi \<bullet> x)"
+using assms
+proof -
+ have "a \<sharp> rev pi"using h1 by (simp add: fresh_list_rev)
+ then have "(rev pi) \<bullet> a = a" by (simp add: at_prm_fresh[OF at])
+ then have "((rev pi) \<bullet> a) \<sharp> x" using h2 by simp
+ thus "a \<sharp> (pi \<bullet> x)" by (simp add: pt_fresh_right[OF pt, OF at])
+qed
+
+lemma pt_fresh_perm_app_ineq:
fixes pi::"'x prm"
and c::"'y"
and x::"'a"
@@ -3044,39 +3062,6 @@
shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)"
by (simp add: perm_fun_def)
-lemma pt_perm_fresh_app:
- fixes pi :: "'x prm"
- and a :: "'x"
- and x :: "'y"
- assumes at: "at TYPE('x)"
- and pt: "pt TYPE('y) TYPE('x)"
- and h1: "a \<sharp> pi"
- and h2: "a \<sharp> x"
- shows "a \<sharp> (pi \<bullet> x)"
-using assms
-proof -
- have "a \<sharp> rev pi"using h1 by (simp add: fresh_list_rev)
- then have "(rev pi) \<bullet> a = a" by (simp add: at_prm_fresh[OF at])
- then have "((rev pi) \<bullet> a) \<sharp> x" using h2 by simp
- thus "a \<sharp> (pi \<bullet> x)" by (simp add: pt_fresh_right[OF pt, OF at])
-qed
-
-lemma pt_perm_fresh_app_ineq:
- fixes pi :: "'x prm"
- and a :: "'y"
- and x :: "'z"
- assumes pta: "pt TYPE('z) TYPE('x)"
- and ptb: "pt TYPE('y) TYPE('x)"
- and at: "at TYPE('x)"
- and cp: "cp TYPE('z) TYPE('x) TYPE('y)"
- and dj: "disjoint TYPE('y) TYPE('x)"
- assumes h:"a \<sharp> x"
- shows "a \<sharp> pi \<bullet> x"
- apply -
- apply (rule pt_fresh_left_ineq[THEN iffD2],assumption+)
- apply (simp add: dj_perm_forget[OF dj],assumption)
-done
-
section {* test *}
lemma at_prm_eq_compose:
fixes pi1 :: "'x prm"
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Apr 24 16:44:11 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Apr 24 17:16:55 2007 +0200
@@ -703,8 +703,6 @@
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_aux_ineq = thm "Nominal.pt_fresh_aux_ineq";
- val fresh_aux = thm "Nominal.pt_fresh_aux";
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";
@@ -716,9 +714,10 @@
val pt_rev_pi = thm "Nominal.pt_rev_pi";
val at_exists_fresh = thm "Nominal.at_exists_fresh";
val at_exists_fresh' = thm "Nominal.at_exists_fresh'";
- val fresh_perm_app_ineq = thm "pt_fresh_perm_app_ineq";
- val fresh_perm_app = thm "pt_fresh_perm_app";
-
+ val fresh_perm_app_ineq = thm "Nominal.pt_fresh_perm_app_ineq";
+ val fresh_perm_app = thm "Nominal.pt_fresh_perm_app";
+ val fresh_aux = thm "Nominal.pt_fresh_aux";
+
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
(* types; this allows for example to use abs_perm (which is a *)
(* collection of theorems) instead of thm abs_fun_pi with explicit *)
@@ -858,12 +857,12 @@
in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [fresh_aux]
- and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]
- in [(("fresh_aux", thms1 @ thms2),[])] end
+ and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]
+ in [(("fresh_aux", thms1 @ thms2),[])] end
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [fresh_perm_app]
- and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]
- in [(("fresh_perm_app", thms1 @ thms2),[])] end
+ and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]
+ in [(("fresh_perm_app", thms1 @ thms2),[])] end
||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
end;