src/HOL/Nominal/Examples/SN.thy
changeset 19218 47b05ebe106b
parent 18659 2ff0ae57431d
child 19496 79dbe35c6cba
     1.1 --- a/src/HOL/Nominal/Examples/SN.thy	Wed Mar 08 17:55:51 2006 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Wed Mar 08 18:00:00 2006 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4    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)"
     1.5    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)"
     1.6    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)"
     1.7 -  and a4:    "\<And>a t1 s1 x. a\<sharp>(s1,x) \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
     1.8 +  and a4:    "\<And>a t1 s1 x. a\<sharp>x \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
     1.9    shows "P x t s"
    1.10  proof -
    1.11    from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
    1.12 @@ -112,7 +112,7 @@
    1.13        have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
    1.14  	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
    1.15        then obtain c::"name" 
    1.16 -	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)"
    1.17 +	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)"
    1.18  	by (force simp add: fresh_prod fresh_atm)
    1.19        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)])"
    1.20  	using a4 f2 by (blast intro!: eqvt_beta)
    1.21 @@ -857,7 +857,6 @@
    1.22  (*A*)
    1.23  apply(simp add: fresh_list_cons fresh_prod)
    1.24  done
    1.25 -
    1.26  lemma all_RED: 
    1.27    assumes a: "\<Gamma>\<turnstile>t:\<tau>"
    1.28    and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
    1.29 @@ -879,6 +878,27 @@
    1.30    thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
    1.31  qed (force dest!: t1_elim t2_elim)+
    1.32  
    1.33 +
    1.34 +lemma all_RED: 
    1.35 +  assumes a: "\<Gamma>\<turnstile>t:\<tau>"
    1.36 +  and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
    1.37 +  shows "t[<\<theta>>]\<in>RED \<tau>"
    1.38 +using a b
    1.39 +proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam.induct)
    1.40 +  case (Lam a t) --"lambda case"
    1.41 +  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> 
    1.42 +                    \<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>" 
    1.43 +  and  \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>" 
    1.44 +  and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" 
    1.45 +  and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact
    1.46 +  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
    1.47 +  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
    1.48 +  from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond
    1.49 +    by (force dest: fresh_context simp add: psubst_subst)
    1.50 +  hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED)
    1.51 +  thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
    1.52 +qed (force dest!: t1_elim t2_elim)+
    1.53 +
    1.54  (* identity substitution generated from a context \<Gamma> *)
    1.55  consts
    1.56    "id" :: "(name\<times>ty) list \<Rightarrow> (name\<times>lam) list"