author urbanc Wed, 08 Mar 2006 18:00:00 +0100 changeset 19218 47b05ebe106b parent 19217 5caacd449ea4 child 19219 8c0b056a18ed
deleted some proofs "on comment"
```--- a/src/HOL/Nominal/Examples/SN.thy	Wed Mar 08 17:55:51 2006 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Mar 08 18:00:00 2006 +0100
@@ -77,7 +77,7 @@
and a1:    "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App s1 t) (App s2 t)"
and a2:    "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App t s1) (App t s2)"
and a3:    "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
-  and a4:    "\<And>a t1 s1 x. a\<sharp>(s1,x) \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
+  and a4:    "\<And>a t1 s1 x. a\<sharp>x \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
shows "P x t s"
proof -
from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
@@ -112,7 +112,7 @@
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)
then obtain c::"name"
-	where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
+	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)
have x: "P x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)])"
using a4 f2 by (blast intro!: eqvt_beta)
@@ -857,7 +857,6 @@
(*A*)
done
-
lemma all_RED:
assumes a: "\<Gamma>\<turnstile>t:\<tau>"
and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)"
@@ -879,6 +878,27 @@
thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
qed (force dest!: t1_elim t2_elim)+

+
+lemma all_RED:
+  assumes a: "\<Gamma>\<turnstile>t:\<tau>"
+  and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)"
+  shows "t[<\<theta>>]\<in>RED \<tau>"
+using a b
+proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam.induct)
+  case (Lam a t) --"lambda case"
+  have ih: "\<And>\<Gamma> \<tau> \<theta>. \<lbrakk>\<Gamma> \<turnstile> t:\<tau>; \<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>\<rbrakk>
+                    \<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>"
+  and  \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>"
+  and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>"
+  and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact
+  hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" using t3_elim fresh by simp
+  then obtain \<tau>1 \<tau>2 where \<tau>_inst: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and typing: "((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" by blast
+  from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond
+    by (force dest: fresh_context simp add: psubst_subst)
+  hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED)
+  thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
+qed (force dest!: t1_elim t2_elim)+
+
(* identity substitution generated from a context \<Gamma> *)
consts
"id" :: "(name\<times>ty) list \<Rightarrow> (name\<times>lam) list"```