--- a/src/HOL/Nominal/Examples/CR.thy Fri Jan 04 09:05:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy Fri Jan 04 09:34:11 2008 +0100
@@ -265,66 +265,29 @@
(auto simp add: calc_atm fresh_atm abs_fresh)
lemma one_abs:
- fixes t :: "lam"
- and t':: "lam"
- and a :: "name"
- assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'"
+ assumes a: "Lam [a].t\<longrightarrow>\<^isub>1t'"
shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
- using a
- apply -
- apply(ind_cases "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
- apply(auto simp add: lam.inject alpha)
- apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
- apply(rule conjI)
- apply(perm_simp)
- apply(simp add: fresh_left calc_atm)
- apply(simp add: One.eqvt)
- apply(simp add: one_fresh_preserv)
-done
-
+proof -
+ have "a\<sharp>Lam [a].t" by (simp add: abs_fresh)
+ with a have "a\<sharp>t'" by (simp add: one_fresh_preserv)
+ with a show ?thesis
+ by (cases rule: One.strong_cases[where a="a" and aa="a"])
+ (auto simp add: lam.inject abs_fresh alpha)
+qed
lemma one_app:
assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or>
- (\<exists>a s s1 s2. t1 = Lam [a].s \<and> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)"
- using a
- apply -
- apply(ind_cases "App t1 t2 \<longrightarrow>\<^isub>1 t'")
- apply(auto simp add: lam.distinct lam.inject)
- done
+ (\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2 \<and> a\<sharp>(t2,s2))"
+using a by (erule_tac One.cases) (auto simp add: lam.inject)
lemma one_red:
- assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M"
+ assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M" "a\<sharp>(t2,M)"
shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or>
(\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)"
- using a
- apply -
- apply(ind_cases "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
- apply(simp_all add: lam.inject)
- apply(force)
- apply(erule conjE)
- apply(drule sym[of "Lam [a].t1"])
- apply(simp)
- apply(drule one_abs)
- apply(erule exE)
- apply(simp)
- apply(force simp add: alpha)
- apply(erule conjE)
- apply(simp add: lam.inject alpha)
- apply(erule disjE)
- apply(simp)
- apply(force)
- apply(simp)
- apply(rule disjI2)
- apply(rule_tac x="[(a,aa)]\<bullet>t2a" in exI)
- apply(rule_tac x="s2" in exI)
- apply(auto)
- apply(subgoal_tac "a\<sharp>t2a")(*A*)
- apply(simp add: subst_rename)
- (*A*)
- apply(force intro: one_fresh_preserv)
- apply(force intro: One.eqvt)
- done
+using a
+by (cases rule: One.strong_cases [where a="a" and aa="a"])
+ (auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod)
text {* first case in Lemma 3.2.4*}
@@ -347,9 +310,8 @@
assumes a: "N\<longrightarrow>\<^isub>1N'"
shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
using a
-apply(nominal_induct M avoiding: x N N' rule: lam.induct)
-apply(auto simp add: fresh_prod fresh_atm)
-done
+by (nominal_induct M avoiding: x N N' rule: lam.induct)
+ (auto simp add: fresh_prod fresh_atm)
lemma one_subst:
assumes a: "M\<longrightarrow>\<^isub>1M'"
@@ -385,9 +347,8 @@
and b: "N\<longrightarrow>\<^isub>1N'"
shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']"
using a b
-apply(nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
-apply(auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
-done
+by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
+ (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
lemma diamond[rule_format]:
fixes M :: "lam"
@@ -401,12 +362,12 @@
thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
next
case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*)
- have vc: "x\<sharp>Q" "x\<sharp>Q'" by fact+
+ have vc: "x\<sharp>Q" "x\<sharp>Q'" "x\<sharp>M2" by fact+
have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
have "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2" by fact
hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q') \<or>
- (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" by (simp add: one_red)
+ (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" using vc by (simp add: one_red)
moreover (* subcase 2.1 *)
{ assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
then obtain P'' and Q'' where
@@ -446,7 +407,7 @@
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
assume "App P Q \<longrightarrow>\<^isub>1 M2"
hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q'') \<or>
- (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> x\<sharp>(Q,Q') \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q')"
+ (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q' \<and> x\<sharp>(Q,Q'))"
by (simp add: one_app[simplified])
moreover (* subcase 3.1 *)
{ assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
@@ -463,11 +424,11 @@
hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
}
moreover (* subcase 3.2 *)
- { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> x\<sharp>(Q,Q'') \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
+ { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q'' \<and> x\<sharp>(Q,Q'')"
then obtain x P1 P1'' Q'' where
b0: "P = Lam [x].P1" and b1: "M2 = P1''[x::=Q'']" and
b2: "P1\<longrightarrow>\<^isub>1P1''" and b3: "Q\<longrightarrow>\<^isub>1Q''" and vc: "x\<sharp>(Q,Q'')" by blast
- from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)
+ from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)
then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^isub>1P1'" by blast
from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^isub>1M3)" by simp
then obtain P1''' where
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy Fri Jan 04 09:05:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy Fri Jan 04 09:34:11 2008 +0100
@@ -63,6 +63,7 @@
using a by (nominal_induct t avoiding: x y s u rule: lam.induct)
(auto simp add: fresh_fact forget)
+
lemma subst_rename:
assumes a: "y\<sharp>t"
shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]"
@@ -124,48 +125,31 @@
finally show "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2[x::=s2]" by simp
qed
-lemma One_preserves_fresh:
- fixes x :: "name"
- assumes a: "t \<longrightarrow>\<^isub>1 s"
- shows "x\<sharp>t \<Longrightarrow> x\<sharp>s"
-using a by (nominal_induct t s avoiding: x rule: One.strong_induct)
- (auto simp add: abs_fresh fresh_atm fresh_fact)
-
lemma One_Var:
assumes a: "Var x \<longrightarrow>\<^isub>1 M"
shows "M = Var x"
using a by (erule_tac One.cases) (simp_all)
lemma One_Lam:
- assumes a: "Lam [x].t \<longrightarrow>\<^isub>1 s"
+ assumes a: "Lam [x].t \<longrightarrow>\<^isub>1 s" "x\<sharp>s"
shows "\<exists>t'. s = Lam [x].t' \<and> t \<longrightarrow>\<^isub>1 t'"
using a
- apply(erule_tac One.cases)
- apply(auto simp add: lam.inject alpha)
- apply(rule_tac x="[(x,xa)]\<bullet>t2" in exI)
- apply(perm_simp add: fresh_left calc_atm One.eqvt One_preserves_fresh)
-done
+by (cases rule: One.strong_cases[where x="x" and xa="x"])
+ (auto simp add: lam.inject abs_fresh alpha)
lemma One_App:
assumes a: "App t s \<longrightarrow>\<^isub>1 r"
shows "(\<exists>t' s'. r = App t' s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or>
(\<exists>x p p' s'. r = p'[x::=s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>\<^isub>1 p' \<and> s \<longrightarrow>\<^isub>1 s' \<and> x\<sharp>(s,s'))"
-using a by (erule_tac One.cases)
- (auto simp add: lam.inject)
+using a by (erule_tac One.cases) (auto simp add: lam.inject)
lemma One_Redex:
- assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r"
+ assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r" "x\<sharp>(s,r)"
shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or>
(\<exists>t' s'. r = t'[x::=s'] \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s')"
using a
-apply(erule_tac One.cases, simp_all)
-apply(auto dest: One_Lam simp add: lam.inject)[1]
-apply(rule disjI2)
-apply(auto simp add: lam.inject alpha)
-apply(rule_tac x="[(x,xa)]\<bullet>t2" in exI)
-apply(rule_tac x="s2" in exI)
-apply(simp add: subst_rename One_preserves_fresh One.eqvt)
-done
+by (cases rule: One.strong_cases [where x="x" and xa="x"])
+ (auto dest: One_Lam simp add: lam.inject abs_fresh alpha fresh_prod)
section {* Transitive Closure of One *}
@@ -186,11 +170,9 @@
| d3[intro]: "\<lbrakk>\<not>(\<exists>y t'. t1 = Lam [y].t'); t1 \<longrightarrow>\<^isub>d t2; s1 \<longrightarrow>\<^isub>d s2\<rbrakk> \<Longrightarrow> App t1 s1 \<longrightarrow>\<^isub>d App t2 s2"
| d4[intro]: "\<lbrakk>x\<sharp>(s1,s2); t1 \<longrightarrow>\<^isub>d t2; s1 \<longrightarrow>\<^isub>d s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) s1 \<longrightarrow>\<^isub>d t2[x::=s2]"
-(* FIXME: needs to be in nominal_inductive *)
-declare perm_pi_simp[eqvt_force]
-
equivariance Dev
-nominal_inductive Dev by (simp_all add: abs_fresh fresh_fact')
+nominal_inductive Dev
+ by (simp_all add: abs_fresh fresh_fact')
lemma better_d4_intro:
assumes a: "t1 \<longrightarrow>\<^isub>d t2" "s1 \<longrightarrow>\<^isub>d s2"
@@ -208,17 +190,19 @@
fixes x::"name"
assumes a: "M\<longrightarrow>\<^isub>d N"
shows "x\<sharp>M \<Longrightarrow> x\<sharp>N"
-using a by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
+using a
+by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
lemma Dev_Lam:
- assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N"
+ assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N"
shows "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>\<^isub>d N'"
-using a
-apply(erule_tac Dev.cases)
-apply(auto simp add: lam.inject alpha)
-apply(rule_tac x="[(x,xa)]\<bullet>s" in exI)
-apply(perm_simp add: fresh_left Dev.eqvt Dev_preserves_fresh)
-done
+proof -
+ from a have "x\<sharp>Lam [x].M" by (simp add: abs_fresh)
+ with a have "x\<sharp>N" by (simp add: Dev_preserves_fresh)
+ with a show ?thesis
+ by (cases rule: Dev.strong_cases [where x="x" and xa="x"])
+ (auto simp add: lam.inject abs_fresh alpha)
+qed
lemma Development_existence:
shows "\<exists>M'. M \<longrightarrow>\<^isub>d M'"
@@ -228,9 +212,13 @@
lemma Triangle:
assumes a: "t \<longrightarrow>\<^isub>d t1" "t \<longrightarrow>\<^isub>1 t2"
shows "t2 \<longrightarrow>\<^isub>1 t1"
-using a by (nominal_induct avoiding: t2 rule: Dev.strong_induct)
- (auto dest!: One_Var One_App One_Redex One_Lam intro: One_subst)
-(* Remark: we could here get away with a normal induction and appealing to One_preserves_fresh *)
+using a
+apply(nominal_induct avoiding: t2 rule: Dev.strong_induct)
+apply(auto dest!: One_Var)[1]
+apply(auto dest!: One_Lam)[1]
+apply(auto dest!: One_App)[1]
+apply(auto dest!: One_Redex intro: One_subst)[1]
+done
lemma Diamond_for_One:
assumes a: "t \<longrightarrow>\<^isub>1 t1" "t \<longrightarrow>\<^isub>1 t2"
--- a/src/HOL/Nominal/Examples/SN.thy Fri Jan 04 09:05:01 2008 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy Fri Jan 04 09:34:11 2008 +0100
@@ -71,33 +71,25 @@
nominal_inductive Beta
by (simp_all add: abs_fresh fresh_fact')
-lemma supp_beta:
+lemma beta_preserves_fresh:
+ fixes a::"name"
assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
- shows "(supp s)\<subseteq>((supp t)::name set)"
+ shows "a\<sharp>t \<Longrightarrow> a\<sharp>s"
using a
-by (induct)
- (auto intro!: simp add: abs_supp lam.supp subst_supp)
+apply(nominal_induct t s avoiding: a rule: Beta.strong_induct)
+apply(auto simp add: abs_fresh fresh_fact fresh_atm)
+done
lemma beta_abs:
- assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'"
+ assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'"
shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
-using a
-apply -
-apply(ind_cases "Lam [a].t \<longrightarrow>\<^isub>\<beta> t'")
-apply(auto simp add: lam.distinct lam.inject)
-apply(auto simp add: alpha)
-apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
-apply(rule conjI)
-apply(rule sym)
-apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
-apply(simp)
-apply(rule pt_name3)
-apply(simp add: at_ds5[OF at_name_inst])
-apply(rule conjI)
-apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
-apply(force dest!: supp_beta simp add: fresh_def)
-apply(force intro!: eqvts)
-done
+proof -
+ have "a\<sharp>Lam [a].t" by (simp add: abs_fresh)
+ with a have "a\<sharp>t'" by (simp add: beta_preserves_fresh)
+ with a show ?thesis
+ by (cases rule: Beta.strong_cases[where a="a" and aa="a"])
+ (auto simp add: lam.inject abs_fresh alpha)
+qed
lemma beta_subst:
assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"