replaced exists_fresh lemma with a version formulated with obtains;
old lemma is available as exists_fresh' (still needed in apply-scripts)
--- a/src/HOL/Nominal/Examples/CR.thy Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy Wed Nov 15 16:23:55 2006 +0100
@@ -225,7 +225,7 @@
show ?case
proof (simp)
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
by (force simp add: fresh_prod fresh_atm)
@@ -243,7 +243,7 @@
show ?case
proof (simp add: subst_eqvt)
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
by (force simp add: fresh_prod fresh_atm)
@@ -320,7 +320,7 @@
show ?case
proof (simp)
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
by (force simp add: fresh_prod fresh_atm)
@@ -342,7 +342,7 @@
show ?case
proof (simp)
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,pi\<bullet>s1,pi\<bullet>s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)"
by (force simp add: fresh_prod at_fresh[OF at_name_inst])
--- a/src/HOL/Nominal/Examples/Fsub.thy Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Nov 15 16:23:55 2006 +0100
@@ -535,7 +535,7 @@
have b3: "X\<sharp>\<Gamma>" by fact
have b3': "X\<sharp>T1" "X\<sharp>S1" using b1 b3 by (simp_all add: subtype_implies_fresh)
have "\<exists>C::tyvrs. C\<sharp>(pi\<bullet>X,pi\<bullet>S2,pi\<bullet>T2,pi\<bullet>S1,pi\<bullet>T1,pi\<bullet>\<Gamma>,x)"
- by (rule at_exists_fresh[OF at_tyvrs_inst], simp add: fs_tyvrs1)
+ by (rule exists_fresh', simp add: fs_tyvrs1)
then obtain C::"tyvrs" where f1: "C\<noteq>(pi\<bullet>X)" and f2: "C\<sharp>(pi\<bullet>S1)" and f3: "C\<sharp>(pi\<bullet>T1)"
and f4: "C\<sharp>(pi\<bullet>S2)" and f5: "C\<sharp>(pi\<bullet>T2)" and f6: "C\<sharp>(pi\<bullet>\<Gamma>)" and f7: "C\<sharp>x"
by (auto simp add: fresh_prod fresh_atm)
--- a/src/HOL/Nominal/Examples/SN.thy Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy Wed Nov 15 16:23:55 2006 +0100
@@ -92,7 +92,7 @@
show ?case
proof (simp)
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
by (force simp add: fresh_prod fresh_atm)
@@ -110,7 +110,7 @@
show ?case
proof (simp add: subst_eqvt)
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
by (force simp add: fresh_prod fresh_atm)
@@ -318,7 +318,7 @@
have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"
by (force simp add: fresh_prod at_fresh[OF at_name_inst])
--- a/src/HOL/Nominal/Examples/Weakening.thy Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy Wed Nov 15 16:23:55 2006 +0100
@@ -102,7 +102,7 @@
have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
- by (rule exists_fresh, simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"
by (force simp add: fresh_prod fresh_atm)
@@ -159,7 +159,7 @@
have f: "a\<sharp>\<Gamma>" by fact
then have f': "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
have "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
- by (rule exists_fresh, simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where fs: "c\<noteq>(pi\<bullet>a)" "c\<sharp>x" "c\<sharp>(pi\<bullet>t)" "c\<sharp>(pi\<bullet>\<Gamma>)"
by (force simp add: fresh_prod fresh_atm)
--- a/src/HOL/Nominal/Nominal.thy Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy Wed Nov 15 16:23:55 2006 +0100
@@ -338,19 +338,23 @@
text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
-lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"
+lemma fresh_unit_elim:
+ shows "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"
by (simp add: fresh_def supp_unit)
-lemma fresh_prod_elim: "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
+lemma fresh_prod_elim:
+ shows "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
by rule (simp_all add: fresh_prod)
lemma fresh_prodD:
- "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> x"
- "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y"
+ shows "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>x"
+ and "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y"
by (simp_all add: fresh_prod)
+(* setup for the simplifier to automatically unsplit freshness in products *)
+
ML_setup {*
- val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD") :: mksimps_pairs;
+ val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD")::mksimps_pairs;
change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
*}
@@ -717,29 +721,38 @@
apply(rule at_prm_eq_refl)
done
---"there always exists an atom not being in a finite set"
+--"there always exists an atom that is not being in a finite set"
lemma ex_in_inf:
fixes A::"'x set"
assumes at: "at TYPE('x)"
and fs: "finite A"
- shows "\<exists>c::'x. c\<notin>A"
+ obtains c::"'x" where "c\<notin>A"
proof -
from fs at4[OF at] have "infinite ((UNIV::'x set) - A)"
by (simp add: Diff_infinite_finite)
hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
- hence "\<exists>c::'x. c\<in>((UNIV::'x set) - A)" by force
- thus "\<exists>c::'x. c\<notin>A" by force
+ then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force
+ then have "c\<notin>A" by simp
+ then show ?thesis using prems by simp
qed
---"there always exists a fresh name for an object with finite support"
+text {* there always exists a fresh name for an object with finite support *}
+lemma at_exists_fresh':
+ fixes x :: "'a"
+ assumes at: "at TYPE('x)"
+ and fs: "finite ((supp x)::'x set)"
+ shows "\<exists>c::'x. c\<sharp>x"
+ by (auto simp add: fresh_def intro: ex_in_inf[OF at, OF fs])
+
lemma at_exists_fresh:
fixes x :: "'a"
assumes at: "at TYPE('x)"
and fs: "finite ((supp x)::'x set)"
- shows "\<exists>c::'x. c\<sharp>x"
- by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs])
+ obtains c::"'x" where "c\<sharp>x"
+ by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def)
-lemma at_finite_select: "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S"
+lemma at_finite_select:
+ shows "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S"
apply (drule Diff_infinite_finite)
apply (simp add: at_def)
apply blast
@@ -1635,6 +1648,7 @@
qed
section {* equivaraince for some connectives *}
+(* FIXME: maybe not really needed *)
lemma pt_all_eqvt:
fixes pi :: "'x prm"
@@ -2776,7 +2790,7 @@
shows "b\<sharp>([a].x)"
proof -
have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)"
- proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
+ proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
show "finite ((supp ([a].x))::'x set)" using f
by (simp add: abs_fun_finite_supp[OF pt, OF at])
qed
@@ -2807,7 +2821,7 @@
shows "b\<sharp>x"
proof -
have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)"
- proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
+ proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
show "finite ((supp ([a].x))::'x set)" using f
by (simp add: abs_fun_finite_supp[OF pt, OF at])
qed
@@ -2834,7 +2848,7 @@
shows "a\<sharp>([a].x)"
proof -
have "\<exists>c::'x. c\<sharp>(a,x)"
- by (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
+ by (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
then obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a"
and fr2: "c\<sharp>x" by (force simp add: fresh_prod at_fresh[OF at])
have "c\<sharp>([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at])
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Nov 15 16:23:55 2006 +0100
@@ -684,6 +684,7 @@
val pt_pi_rev = thm "Nominal.pt_pi_rev";
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'";
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
@@ -764,6 +765,7 @@
||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
+ ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[])]
||>> PureThy.add_thmss
let val thms1 = inst_at [at_fresh]
--- a/src/HOL/Nominal/nominal_package.ML Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Wed Nov 15 16:23:55 2006 +0100
@@ -1595,7 +1595,7 @@
(** uniqueness **)
- val exists_fresh = PureThy.get_thms thy11 (Name "exists_fresh");
+ val exists_fresh' = PureThy.get_thms thy11 (Name "exists_fresh'");
val fs_atoms = map (fn Type (s, _) => PureThy.get_thm thy11
(Name ("fs_" ^ Sign.base_name s ^ "1"))) dt_atomTs;
val fresh_atm = PureThy.get_thms thy11 (Name "fresh_atm");
@@ -1636,7 +1636,7 @@
(fn _ => EVERY
[cut_facts_tac ths 1,
REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
- resolve_tac exists_fresh 1,
+ resolve_tac exists_fresh' 1,
asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
val (([cx], ths), ctxt') = Obtain.result
(fn _ => EVERY