--- a/src/HOL/Nominal/Examples/Fsub.thy Fri Jun 30 18:26:36 2006 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Sun Jul 02 17:27:10 2006 +0200
@@ -178,7 +178,7 @@
have "\<turnstile> (pi\<bullet>\<Gamma>) ok" by fact
moreover
have "X\<sharp>(domain \<Gamma>)" by fact
- hence "(pi\<bullet>X)\<sharp>(domain (pi\<bullet>\<Gamma>))" by (simp add: fresh_eqvt domain_eqvt[symmetric])
+ hence "(pi\<bullet>X)\<sharp>(domain (pi\<bullet>\<Gamma>))" by (simp add: fresh_bij domain_eqvt[symmetric])
moreover
have "T closed_in \<Gamma>" by fact
hence "(pi\<bullet>T) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_eqvt)
@@ -341,7 +341,7 @@
dest: pt_set_bij2[OF pt_tyvrs_inst, OF at_tyvrs_inst]
simp add: domain_eqvt)
apply(force)
-apply(force intro!: S_Forall simp add: fresh_prod fresh_eqvt)
+apply(force intro!: S_Forall simp add: fresh_prod fresh_bij)
done
text {* The most painful part of the subtyping definition is the strengthening of the
--- a/src/HOL/Nominal/Examples/Iteration.thy Fri Jun 30 18:26:36 2006 +0200
+++ b/src/HOL/Nominal/Examples/Iteration.thy Sun Jul 02 17:27:10 2006 +0200
@@ -104,15 +104,11 @@
done
have fs1: "a1\<sharp>f3 a1 r1" using b f1
apply(auto)
- apply(case_tac "a=a1")
- apply(simp)
apply(rule_tac pi="[(a1,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: calc_atm fresh_prod)
done
have fs2: "a2\<sharp>f3 a2 r2" using b f2
apply(auto)
- apply(case_tac "a=a2")
- apply(simp)
apply(rule_tac pi="[(a2,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
apply(perm_simp add: calc_atm fresh_prod)
done
@@ -155,7 +151,7 @@
have fs_pi: "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)"
proof -
from c obtain a where fs1: "a\<sharp>f3" and fs2: "\<forall>(r::'a::pt_name). a\<sharp>f3 a r" by force
- have "(pi\<bullet>a)\<sharp>(pi\<bullet>f3)" using fs1 by (simp add: fresh_eqvt)
+ have "(pi\<bullet>a)\<sharp>(pi\<bullet>f3)" using fs1 by (simp add: fresh_bij)
moreover
have "\<forall>(r::'a::pt_name). (pi\<bullet>a)\<sharp>((pi\<bullet>f3) (pi\<bullet>a) r)" using fs2 by (perm_simp add: fresh_right)
ultimately show "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)" by blast
--- a/src/HOL/Nominal/Examples/SN.thy Fri Jun 30 18:26:36 2006 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy Sun Jul 02 17:27:10 2006 +0200
@@ -217,7 +217,7 @@
shows "valid (pi\<bullet>\<Gamma>)"
using a
apply(induct)
-apply(auto simp add: fresh_eqvt)
+apply(auto simp add: fresh_bij)
done
(* typing judgements *)
@@ -281,7 +281,7 @@
using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
next
case (t3 \<Gamma> \<sigma> \<tau> a t)
- moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
+ moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force
qed (auto)
--- a/src/HOL/Nominal/Examples/Weakening.thy Fri Jun 30 18:26:36 2006 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy Sun Jul 02 17:27:10 2006 +0200
@@ -42,7 +42,7 @@
shows "valid (pi\<bullet>\<Gamma>)"
using a
apply(induct)
-apply(auto simp add: fresh_eqvt)
+apply(auto simp add: fresh_bij)
done
(* typing judgements *)
@@ -76,7 +76,7 @@
using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
next
case (t3 \<Gamma> \<sigma> \<tau> a t)
- moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
+ moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force
qed (auto)
--- a/src/HOL/Nominal/Nominal.thy Fri Jun 30 18:26:36 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy Sun Jul 02 17:27:10 2006 +0200
@@ -87,6 +87,16 @@
shows "pi\<bullet>(b::bool) = b"
by (cases b) auto
+lemma perm_boolI:
+ assumes a: "P"
+ shows "pi\<bullet>P"
+ using a by (simp add: perm_bool)
+
+lemma perm_boolE:
+ assumes a: "pi\<bullet>P"
+ shows "P"
+ using a by (simp add: perm_bool)
+
(* permutation on options *)
primrec (unchecked perm_option)
perm_some_def: "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
@@ -865,6 +875,13 @@
apply(simp add: supp_def dj_perm_forget[OF dj])
done
+lemma at_fresh_ineq:
+ fixes a :: "'x"
+ and b :: "'y"
+ assumes dj: "disjoint TYPE('y) TYPE('x)"
+ shows "a\<sharp>b"
+ by (simp add: fresh_def dj_supp[OF dj])
+
section {* permutation type instances *}
(* ===================================*)
@@ -1406,6 +1423,15 @@
shows "a\<sharp>x"
using a by (simp add: pt_fresh_bij[OF pt, OF at])
+lemma pt_fresh_eqvt:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>(a\<sharp>x) = (pi\<bullet>a)\<sharp>(pi\<bullet>x)"
+ by (simp add: perm_bool pt_fresh_bij[OF pt, OF at])
+
lemma pt_perm_fresh1:
fixes a :: "'x"
and b :: "'x"
@@ -1556,6 +1582,29 @@
thus ?thesis by (simp add: pt2[OF pt])
qed
+section {* equivaraince for some connectives *}
+
+lemma pt_all_eqvt:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). (pi\<bullet>P) x)"
+apply(auto simp add: perm_bool perm_fun_def)
+apply(drule_tac x="pi\<bullet>x" in spec)
+apply(simp add: pt_rev_pi[OF pt, OF at])
+done
+
+lemma imp_eqvt:
+ fixes pi::"'x prm"
+ shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
+ by (simp add: perm_bool)
+
+lemma conj_eqvt:
+ fixes pi::"'x prm"
+ shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
+ by (simp add: perm_bool)
+
section {* facts about supports *}
(*==============================*)
--- a/src/HOL/Nominal/nominal_atoms.ML Fri Jun 30 18:26:36 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sun Jul 02 17:27:10 2006 +0200
@@ -668,6 +668,7 @@
val pt_perm_compose' = thm "Nominal.pt_perm_compose'";
val perm_app = thm "Nominal.pt_fun_app_eq";
val at_fresh = thm "Nominal.at_fresh";
+ val at_fresh_ineq = thm "Nominal.at_fresh_ineq";
val at_calc = thms "Nominal.at_calc";
val at_supp = thm "Nominal.at_supp";
val dj_supp = thm "Nominal.dj_supp";
@@ -679,8 +680,11 @@
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 all_eqvt = thm "Nominal.pt_all_eqvt";
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";
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
@@ -761,7 +765,12 @@
||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])]
||>> 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 [(("fresh_atm", inst_at [at_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]
+ val thms2 = inst_dj [at_fresh_ineq]
+ in [(("fresh_atm", thms1 @ thms2),[])] end
||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [abs_fun_pi]
@@ -792,7 +801,10 @@
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [fresh_bij]
and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
- in [(("fresh_eqvt", thms1 @ thms2),[])] end
+ in [(("fresh_bij", thms1 @ thms2),[])] end
+ ||>> PureThy.add_thmss
+ let val thms1 = inst_pt_at [fresh_eqvt]
+ in [(("fresh_eqvt", thms1),[])] end
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [fresh_aux]
and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq]