src/HOL/Nominal/Examples/SN.thy
changeset 18345 d37fb71754fe
parent 18313 e61d2424863d
child 18348 b5d7649f8aca
equal deleted inserted replaced
18344:95083a68cbbb 18345:d37fb71754fe
   834 lemma fresh_at[rule_format]: "a\<in>set(domain \<theta>) \<longrightarrow> c\<sharp>\<theta>\<longrightarrow>c\<sharp>(\<theta><a>)"
   834 lemma fresh_at[rule_format]: "a\<in>set(domain \<theta>) \<longrightarrow> c\<sharp>\<theta>\<longrightarrow>c\<sharp>(\<theta><a>)"
   835 apply(induct_tac \<theta>)   
   835 apply(induct_tac \<theta>)   
   836 apply(auto simp add: fresh_prod fresh_list_cons)
   836 apply(auto simp add: fresh_prod fresh_list_cons)
   837 done
   837 done
   838 
   838 
   839 lemma psubs_subs[rule_format]: "c\<sharp>\<theta>\<longrightarrow> (t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]"
   839 lemma psubst_subst[rule_format]: "c\<sharp>\<theta>\<longrightarrow> (t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]"
   840 apply(nominal_induct t avoiding: \<theta> c s rule: lam_induct)
   840 apply(nominal_induct t avoiding: \<theta> c s rule: lam_induct)
   841 apply(auto dest: fresh_domain)
   841 apply(auto dest: fresh_domain)
   842 apply(drule fresh_at)
   842 apply(drule fresh_at)
   843 apply(assumption)
   843 apply(assumption)
   844 apply(rule forget)
   844 apply(rule forget)
   847 apply(simp)
   847 apply(simp)
   848 (*A*)
   848 (*A*)
   849 apply(simp add: fresh_list_cons fresh_prod)
   849 apply(simp add: fresh_list_cons fresh_prod)
   850 done
   850 done
   851 
   851 
       
   852 thm fresh_context
       
   853 
   852 lemma all_RED: 
   854 lemma all_RED: 
   853  "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow>  (t[<\<theta>>]\<in>RED \<tau>)"
   855   assumes a: "\<Gamma>\<turnstile>t:\<tau>"
       
   856   and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
       
   857   shows "t[<\<theta>>]\<in>RED \<tau>"
       
   858 using a b
       
   859 proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct)
       
   860   case (Lam a t) --"lambda case"
       
   861   have ih: "\<And>\<Gamma> \<tau> \<theta>. \<Gamma> \<turnstile> t:\<tau> \<Longrightarrow> 
       
   862                     (\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>) 
       
   863                     \<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>" 
       
   864   and  \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>" 
       
   865   and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" 
       
   866   and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact
       
   867   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
       
   868   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
       
   869   from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond
       
   870     by (force dest: fresh_context simp add: psubst_subst)
       
   871   hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED)
       
   872   thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
       
   873 qed (force dest!: t1_elim t2_elim)+
       
   874 
       
   875 lemma all_RED:
       
   876   assumes a: "\<Gamma>\<turnstile>t:\<tau>"
       
   877   and     b: "\<And>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<Longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
       
   878   shows "t[<\<theta>>]\<in>RED \<tau>"
       
   879 using a b
   854 apply(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct)
   880 apply(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct)
   855 (* Variables *)
   881 (* Variables *)
   856 apply(force dest: t1_elim)
   882 apply(force dest: t1_elim)
   857 (* Applications *)
   883 (* Applications *)
   858 apply(atomize)
   884 apply(atomize)
   859 apply(force dest!: t2_elim)
   885 apply(force dest!: t2_elim)
   860 (* Abstractions *)
   886 (* Abstractions  *)
   861 apply(auto dest!: t3_elim simp only:)
   887 apply(auto dest!: t3_elim simp only: psubst_Lam)
   862 apply(simp only: fresh_prod psubst_Lam)
       
   863 apply(rule abs_RED[THEN mp])
   888 apply(rule abs_RED[THEN mp])
   864 apply(force dest: fresh_context simp add: psubs_subs)
   889 apply(force dest: fresh_context simp add: psubs_subs)
   865 done
   890 done
   866 
       
   867 lemma all_RED: 
       
   868   "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow>  (t[<\<theta>>]\<in>RED \<tau>)"
       
   869 apply(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct)
       
   870 (* Variables *)
       
   871 apply(force dest: t1_elim)
       
   872 (* Applications *)
       
   873 apply(atomize)
       
   874 apply(clarify)
       
   875 apply(drule t2_elim)
       
   876 apply(erule exE, erule conjE)
       
   877 apply(drule_tac x="\<Gamma>" in spec)
       
   878 apply(drule_tac x="\<Gamma>" in spec)
       
   879 apply(drule_tac x="\<tau>'\<rightarrow>\<tau>" in spec)
       
   880 apply(drule_tac x="\<tau>'" in spec)
       
   881 apply(drule_tac x="\<theta>" in spec)
       
   882 apply(drule_tac x="\<theta>" in spec)
       
   883 apply(force)
       
   884 (* Abstractions *)
       
   885 apply(clarify)
       
   886 apply(drule t3_elim)
       
   887 apply(simp add: fresh_prod)
       
   888 apply(erule exE)+
       
   889 apply(erule conjE)
       
   890 apply(simp only: fresh_prod psubst_Lam)
       
   891 apply(rule abs_RED[THEN mp])
       
   892 apply(clarify)
       
   893 apply(atomize)
       
   894 apply(force dest: fresh_context simp add: psubs_subs)
       
   895 done
       
   896 
       
   897 
       
   898 lemma all_RED: 
       
   899  "\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow>  (t[<\<theta>>]\<in>RED \<tau>)"
       
   900 proof(nominal_induct t rule: lam_induct)
       
   901   case Var 
       
   902   show ?case by (force dest: t1_elim)
       
   903 next
       
   904   case App
       
   905   thus ?case by (force dest!: t2_elim)
       
   906 (* HERE *)
       
   907 next
       
   908   case (Lam \<Gamma> \<tau> \<theta> a t)
       
   909   have ih: 
       
   910     "\<forall>\<Gamma> \<tau> \<theta>. (\<forall>\<sigma> c. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>) \<and> \<Gamma> \<turnstile> t : \<tau> \<longrightarrow> t[<\<theta>>]\<in>RED \<tau>"
       
   911     by fact
       
   912   have "a\<sharp>(\<Gamma>,\<tau>,\<theta>)" by fact
       
   913   hence b1: "a\<sharp>\<Gamma>" and b2: "a\<sharp>\<tau>" and b3: "a\<sharp>\<theta>" by (simp_all add: fresh_prod)
       
   914   from b1 have c1: "\<not>(\<exists>\<tau>. (a,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context) 
       
   915   show ?case using b1 
       
   916   proof (auto dest!: t3_elim simp only: psubst_Lam)
       
   917     fix \<sigma>1::"ty" and \<sigma>2::"ty"
       
   918     assume a1: "((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2"
       
   919     and    a3: "\<forall>(\<sigma>\<Colon>ty) (c\<Colon>name). (c,\<sigma>) \<in> set \<Gamma> \<longrightarrow> c \<in> set (domain \<theta>) \<and>  \<theta> <c> \<in> RED \<sigma>"
       
   920     have "\<forall>s\<in>RED \<sigma>1. (t[<\<theta>>])[a::=s]\<in>RED \<sigma>2" 
       
   921     proof
       
   922 (* HERE *)
       
   923 
       
   924       fix s::"lam"
       
   925       assume a4: "s \<in> RED \<sigma>1"
       
   926       from ih have "\<forall>\<sigma> c. (c,\<sigma>)\<in>set ((a,\<sigma>1)#\<Gamma>) \<longrightarrow> c\<in>set (domain ((c,s)#\<theta>)) \<and> (((c,s)#\<theta>)<c>)\<in>RED \<sigma>"
       
   927 	using c1 a4 proof (auto)
       
   928 apply(simp)
       
   929 	apply(rule allI)+
       
   930 	apply(rule conjI)
       
   931 
       
   932       proof (auto) *)
       
   933       have "(((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2) \<longrightarrow> t[<((a,s)#\<theta>)>] \<in> RED \<sigma>2" using Lam a3 b3 
       
   934 	proof(blast dest: fresh_context)
       
   935 
       
   936       show "(t[<\<theta>>])[a::=s] \<in> RED \<sigma>2"
       
   937 	
       
   938     qed
       
   939     thus "Lam [a].(t[<\<theta>>]) \<in> RED (\<sigma>1\<rightarrow>\<sigma>2)" by (simp only: abs_RED)
       
   940   qed
       
   941 qed
       
   942 
       
   943 
       
   944 
       
   945 
       
   946 
       
   947     have "(((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2) \<longrightarrow> t[<((a,u)#\<theta>)>] \<in> RED \<sigma>2" using Lam a3 sorry
       
   948     hence "t[<((a,u)#\<theta>)>] \<in> RED \<sigma>2" using a1 by simp
       
   949     hence "t[<\<theta>>][a::=u] \<in> RED \<sigma>2" using b3 by (simp add: psubs_subs)
       
   950     show "Lam [a].(t[<\<theta>>]) \<in> RED (\<sigma>1\<rightarrow>\<sigma>2)" 
       
   951     hence "Lam [a].(t[<\<theta>>]) \<in> RED (\<tau>\<rightarrow>\<sigma>)" using a2 abs_RED by force
       
   952     show "App (Lam [a].(t[<\<theta>>])) u \<in> RED \<sigma>2"
       
   953 
       
   954     
       
   955 
       
   956   thus ?case using t2_elim 
       
   957     proof(auto, blast)
       
   958 
       
   959 qed
       
   960 
       
   961 (* Variables *)
       
   962 apply(force dest: t1_elim)
       
   963 (* Applications *)
       
   964 apply(clarify)
       
   965 apply(drule t2_elim)
       
   966 apply(erule exE, erule conjE)
       
   967 apply(drule_tac x="a" in spec)
       
   968 apply(drule_tac x="a" in spec)
       
   969 apply(drule_tac x="\<tau>\<rightarrow>aa" in spec)
       
   970 apply(drule_tac x="\<tau>" in spec)
       
   971 apply(drule_tac x="b" in spec)
       
   972 apply(drule_tac x="b" in spec)
       
   973 apply(force)
       
   974 (* Abstractions *)
       
   975 apply(clarify)
       
   976 apply(drule t3_elim)
       
   977 apply(simp add: fresh_prod)
       
   978 apply(erule exE)+
       
   979 apply(erule conjE)
       
   980 apply(simp only: fresh_prod psubst_Lam)
       
   981 apply(rule abs_RED)
       
   982 apply(auto)
       
   983 apply(drule_tac x="(ab,\<tau>)#a" in spec)
       
   984 apply(drule_tac x="\<tau>'" in spec)
       
   985 apply(drule_tac x="(ab,s)#b" in spec)
       
   986 apply(simp)
       
   987 apply(auto)
       
   988 apply(drule fresh_context)
       
   989 apply(simp)
       
   990 apply(simp add: psubs_subs)
       
   991 done
       
   992 
       
   993 
       
   994 
       
   995 done
       
   996