src/HOL/Nominal/Examples/SN.thy
changeset 18382 44578c918349
parent 18378 35fba71ec6ef
child 18383 5f40a59a798b
     1.1 --- a/src/HOL/Nominal/Examples/SN.thy	Sat Dec 10 00:11:35 2005 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Sun Dec 11 01:21:26 2005 +0100
     1.3 @@ -853,8 +853,6 @@
     1.4  apply(simp add: fresh_list_cons fresh_prod)
     1.5  done
     1.6  
     1.7 -thm fresh_context
     1.8 -
     1.9  lemma all_RED: 
    1.10    assumes a: "\<Gamma>\<turnstile>t:\<tau>"
    1.11    and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
    1.12 @@ -891,4 +889,73 @@
    1.13  apply(auto dest!: t3_elim simp only: psubst_Lam)
    1.14  apply(rule abs_RED[THEN mp])
    1.15  apply(force dest: fresh_context simp add: psubst_subst)
    1.16 -done
    1.17 \ No newline at end of file
    1.18 +done
    1.19 +
    1.20 +(* identity substitution generated from a \<Gamma> *)
    1.21 +consts
    1.22 +  "id" :: "(name\<times>ty) list \<Rightarrow> (name\<times>lam) list"
    1.23 +primrec
    1.24 +  "id []    = []"
    1.25 +  "id (x#\<Gamma>) = ((fst x),Var (fst x))#(id \<Gamma>)"
    1.26 +
    1.27 +lemma id_var:
    1.28 +  assumes a: "a \<in> set (domain (id \<Gamma>))"
    1.29 +  shows "(id \<Gamma>)<a> = Var a"
    1.30 +using a
    1.31 +apply(induct \<Gamma>, auto)
    1.32 +done
    1.33 +
    1.34 +lemma id_fresh:
    1.35 +  fixes a::"name"
    1.36 +  assumes a: "a\<sharp>\<Gamma>"
    1.37 +  shows "a\<sharp>(id \<Gamma>)"
    1.38 +using a
    1.39 +apply(induct \<Gamma>)
    1.40 +apply(auto simp add: fresh_list_nil fresh_list_cons fresh_prod)
    1.41 +done
    1.42 +
    1.43 +lemma id_apply:  
    1.44 +  assumes a: "valid \<Gamma>"
    1.45 +  shows "t[<(id \<Gamma>)>] = t"
    1.46 +using a
    1.47 +apply(nominal_induct t avoiding: \<Gamma> rule: lam_induct)
    1.48 +apply(auto)
    1.49 +apply(simp add: id_var)
    1.50 +apply(drule id_fresh)+
    1.51 +apply(simp)
    1.52 +done
    1.53 +
    1.54 +lemma id_mem:
    1.55 +  assumes a: "(a,\<tau>)\<in>set \<Gamma>"
    1.56 +  shows "a \<in> set (domain (id \<Gamma>))"
    1.57 +using a
    1.58 +apply(induct \<Gamma>, auto)
    1.59 +done
    1.60 +
    1.61 +lemma ty_in_RED:  
    1.62 +  shows "\<Gamma>\<turnstile>t:\<tau>\<Longrightarrow>t\<in>RED \<tau>"
    1.63 +apply(frule typing_valid)
    1.64 +apply(drule_tac \<theta>="id \<Gamma>" in all_RED)
    1.65 +apply(simp add: id_mem)
    1.66 +apply(frule id_mem)
    1.67 +apply(simp add: id_var)
    1.68 +apply(subgoal_tac "CR3 \<sigma>")
    1.69 +apply(drule CR3_CR4)
    1.70 +apply(simp add: CR4_def)
    1.71 +apply(drule_tac x="Var a" in spec)
    1.72 +apply(drule mp)
    1.73 +apply(auto simp add: NEUT_def NORMAL_def)
    1.74 +apply(ind_cases "(Var a) \<longrightarrow>\<^isub>\<beta> t'")
    1.75 +apply(rule RED_props[THEN conjunct2, THEN conjunct2])
    1.76 +apply(simp add: id_apply)
    1.77 +done
    1.78 +
    1.79 +lemma ty_SN: "\<Gamma>\<turnstile>t:\<tau>\<Longrightarrow>SN(t)"
    1.80 +apply(drule ty_in_RED)
    1.81 +apply(subgoal_tac "CR1 \<tau>")(*A*)
    1.82 +apply(simp add: CR1_def)
    1.83 +(*A*)
    1.84 +apply(rule RED_props[THEN conjunct1])
    1.85 +done
    1.86 +
    1.87 +end
    1.88 \ No newline at end of file