src/HOL/Nominal/Examples/Weakening.thy
 changeset 18346 c9be8266325f parent 18311 b83b00cbaecf child 18352 b9d0bd76286c
equal inserted replaced
18345:d37fb71754fe 18346:c9be8266325f
`   213   have a1: "\<Gamma>1 \<lless> \<Gamma>2" by fact`
`   213   have a1: "\<Gamma>1 \<lless> \<Gamma>2" by fact`
`   214   have a2: "valid \<Gamma>2" by fact`
`   214   have a2: "valid \<Gamma>2" by fact`
`   215   have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 sub_def by simp `
`   215   have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 sub_def by simp `
`   216   moreover`
`   216   moreover`
`   217   have "valid ((a,\<tau>)#\<Gamma>2)" using a2 fc by force`
`   217   have "valid ((a,\<tau>)#\<Gamma>2)" using a2 fc by force`
`   218   ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by force`
`   218   ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by simp `
`   219   with fc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force`
`   219   with fc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force`
`   220 qed (auto simp add: sub_def) (* app and var case *)`
`   220 qed (auto simp add: sub_def) (* app and var case *)`
`   221 `
`   221 `
`   222 text{* The original induction principle for typing `
`   222 text{* The original induction principle for typing `
`   223        is not strong enough - so the simple proof fails *}`
`   223        is not strong enough - so the simple proof fails *}`