updated some of the definitions and proofs
authorurbanc
Mon Jul 30 10:39:12 2007 +0200 (2007-07-30)
changeset 24070ff4c715a11cd
parent 24069 8a15a04e36f6
child 24071 82873bc360c2
updated some of the definitions and proofs
src/HOL/Nominal/Examples/Crary.thy
     1.1 --- a/src/HOL/Nominal/Examples/Crary.thy	Sun Jul 29 23:27:40 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Crary.thy	Mon Jul 30 10:39:12 2007 +0200
     1.3 @@ -21,9 +21,9 @@
     1.4  
     1.5  nominal_datatype trm = 
     1.6      Unit
     1.7 -  | Var "name"
     1.8 +  | Var "name" ("Var _" [100] 100)
     1.9    | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
    1.10 -  | App "trm" "trm"
    1.11 +  | App "trm" "trm" ("App _ _" [110,110] 100)
    1.12    | Const "nat"
    1.13  
    1.14  types Ctxt  = "(name\<times>ty) list"
    1.15 @@ -42,6 +42,8 @@
    1.16    shows "x\<sharp>T"
    1.17    by (simp add: fresh_def supp_def)
    1.18  
    1.19 +
    1.20 +
    1.21  lemma ty_cases:
    1.22    fixes T::ty
    1.23    shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
    1.24 @@ -89,11 +91,11 @@
    1.25     (auto simp add: fresh_list_cons fresh_prod fresh_atm)
    1.26  
    1.27  consts
    1.28 -  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [60,100] 100)
    1.29 +  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
    1.30   
    1.31  nominal_primrec
    1.32    "\<theta><(Var x)> = (lookup \<theta> x)"
    1.33 -  "\<theta><(App t\<^isub>1 t\<^isub>2)> = App (\<theta><t\<^isub>1>) (\<theta><t\<^isub>2>)"
    1.34 +  "\<theta><(App t\<^isub>1 t\<^isub>2)> = App \<theta><t\<^isub>1> \<theta><t\<^isub>2>"
    1.35    "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
    1.36    "\<theta><(Const n)> = Const n"
    1.37    "\<theta><(Unit)> = Unit"
    1.38 @@ -164,19 +166,19 @@
    1.39  
    1.40  lemma fresh_psubst_simp:
    1.41    assumes "x\<sharp>t"
    1.42 -  shows "(x,u)#\<theta><t> = \<theta><t>" 
    1.43 +  shows "((x,u)#\<theta>)<t> = \<theta><t>" 
    1.44  using assms
    1.45  proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct)
    1.46    case (Lam y t x u)
    1.47 -  have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact+
    1.48 +  have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact
    1.49    moreover have "x\<sharp> Lam [y].t" by fact 
    1.50    ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm)
    1.51    moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact
    1.52 -  ultimately have "(x,u)#\<theta><t> = \<theta><t>" by auto
    1.53 -  moreover have "(x,u)#\<theta><Lam [y].t> = Lam [y]. ((x,u)#\<theta><t>)" using fs 
    1.54 +  ultimately have "((x,u)#\<theta>)<t> = \<theta><t>" by auto
    1.55 +  moreover have "((x,u)#\<theta>)<Lam [y].t> = Lam [y].(((x,u)#\<theta>)<t>)" using fs 
    1.56      by (simp add: fresh_list_cons fresh_prod)
    1.57    moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp
    1.58 -  ultimately show "(x,u)#\<theta><Lam [y].t> = \<theta><Lam [y].t>" by auto
    1.59 +  ultimately show "((x,u)#\<theta>)<Lam [y].t> = \<theta><Lam [y].t>" by auto
    1.60  qed (auto simp add: fresh_atm abs_fresh)
    1.61  
    1.62  lemma forget: 
    1.63 @@ -212,7 +214,7 @@
    1.64  
    1.65  lemma psubst_subst_psubst:
    1.66    assumes h:"c\<sharp>\<theta>"
    1.67 -  shows "\<theta><t>[c::=s] = (c,s)#\<theta><t>"
    1.68 +  shows "\<theta><t>[c::=s] = ((c,s)#\<theta>)<t>"
    1.69    using h
    1.70  by (nominal_induct t avoiding: \<theta> c s rule: trm.induct)
    1.71     (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
    1.72 @@ -244,7 +246,7 @@
    1.73    ultimately show ?case by auto  
    1.74  next
    1.75    case (Lam n t x u \<theta>)
    1.76 -  have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact+
    1.77 +  have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact
    1.78    have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact
    1.79    have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto
    1.80    then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto
    1.81 @@ -265,7 +267,7 @@
    1.82  
    1.83  equivariance valid 
    1.84  
    1.85 -inductive_cases  
    1.86 +inductive_cases
    1.87    valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
    1.88  
    1.89  abbreviation
    1.90 @@ -300,11 +302,11 @@
    1.91  inductive
    1.92    typing :: "Ctxt\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
    1.93  where
    1.94 -  t_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
    1.95 -| t_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2"
    1.96 -| t_Lam[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
    1.97 -| t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
    1.98 -| t_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
    1.99 +  T_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
   1.100 +| T_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> e\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2"
   1.101 +| T_Lam[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
   1.102 +| T_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
   1.103 +| T_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
   1.104  
   1.105  equivariance typing
   1.106  
   1.107 @@ -316,19 +318,20 @@
   1.108    shows "valid \<Gamma>"
   1.109    using a by (induct) (auto)
   1.110  
   1.111 +(*
   1.112  declare trm.inject [simp add]
   1.113  declare ty.inject  [simp add]
   1.114  
   1.115 -inductive_cases t_inv_auto[elim]: 
   1.116 -  "\<Gamma> \<turnstile> Lam [x].t : T"
   1.117 -  "\<Gamma> \<turnstile> Var x : T"
   1.118 -  "\<Gamma> \<turnstile> App x y : T"
   1.119 -  "\<Gamma> \<turnstile> Const n : T"
   1.120 -  "\<Gamma> \<turnstile> Unit : TUnit"
   1.121 -  "\<Gamma> \<turnstile> s : TUnit"
   1.122 +inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
   1.123 +inductive_cases2 t_Var_elim_auto[elim]: "\<Gamma> \<turnstile> Var x : T"
   1.124 +inductive_cases2 t_App_elim_auto[elim]: "\<Gamma> \<turnstile> App x y : T"
   1.125 +inductive_cases2 t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
   1.126 +inductive_cases2 t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit"
   1.127 +inductive_cases2 t_Unit_elim_auto'[elim]: "\<Gamma> \<turnstile> s : TUnit"
   1.128  
   1.129  declare trm.inject [simp del]
   1.130  declare ty.inject [simp del]
   1.131 +*)
   1.132  
   1.133  section {* Definitional Equivalence *}
   1.134  
   1.135 @@ -356,6 +359,126 @@
   1.136    shows "valid \<Gamma>"
   1.137  using a by (induct) (auto elim: typing_implies_valid)
   1.138  
   1.139 +lemma test30:
   1.140 +  fixes x::"name"
   1.141 +  assumes a: "(x,T) \<in> set \<Gamma>"
   1.142 +  shows "x\<in>supp \<Gamma>"
   1.143 +using a
   1.144 +apply(induct \<Gamma>)
   1.145 +apply(auto simp add: supp_list_cons supp_prod supp_atm)
   1.146 +done
   1.147 +
   1.148 +lemma supp_ty[simp]: 
   1.149 +  fixes T::"ty"
   1.150 +  shows "(supp T) = ({}::name set)"
   1.151 +apply(simp add: supp_def)
   1.152 +done
   1.153 +
   1.154 +lemma test3a:
   1.155 +  assumes a: "\<Gamma> \<turnstile> t : T"
   1.156 +  shows "(supp t) \<subseteq> ((supp \<Gamma>)::name set)"
   1.157 +using a
   1.158 +apply(induct)
   1.159 +apply(auto simp add: trm.supp supp_atm supp_list_cons abs_supp supp_prod)
   1.160 +apply(simp add: test30)
   1.161 +apply(simp add: supp_def perm_nat_def)
   1.162 +done
   1.163 +
   1.164 +lemma test3b:
   1.165 +  shows "supp (t\<^isub>1[x::=t\<^isub>2]) \<subseteq> ((supp ([x].t\<^isub>1,t\<^isub>2))::name set)"
   1.166 +apply(nominal_induct t\<^isub>1 avoiding: x t\<^isub>2 rule: trm.induct)
   1.167 +apply(auto simp add: trm.supp supp_prod abs_supp supp_atm)
   1.168 +apply(blast)
   1.169 +apply(blast)
   1.170 +apply(simp add: supp_def perm_nat_def)
   1.171 +done
   1.172 +
   1.173 +lemma test3:
   1.174 +  assumes a: "\<Gamma> \<turnstile> s \<equiv> t : T"
   1.175 +  shows "(supp (s,t)) \<subseteq> ((supp \<Gamma>)::name set)"
   1.176 +using a
   1.177 +apply(induct)
   1.178 +apply(auto simp add: supp_prod  supp_list_cons trm.supp abs_supp supp_atm)
   1.179 +apply(drule test3a)
   1.180 +apply(blast)
   1.181 +apply(subgoal_tac "supp (t\<^isub>1[x::=t\<^isub>2]) \<subseteq> ((supp ([x].t\<^isub>1,t\<^isub>2))::name set)")
   1.182 +apply(auto simp add: supp_prod abs_supp)[1]
   1.183 +apply(rule test3b)
   1.184 +apply(case_tac "x=xa")
   1.185 +apply(simp add: fresh_def supp_prod)
   1.186 +apply(blast)
   1.187 +apply(case_tac "x=xa")
   1.188 +apply(simp add: fresh_def supp_prod)
   1.189 +apply(blast)
   1.190 +apply(drule test3a)
   1.191 +apply(blast)
   1.192 +apply(drule test3a)+
   1.193 +apply(blast)
   1.194 +done
   1.195 +
   1.196 +lemma test0:
   1.197 +  assumes a: "(x,T\<^isub>1)#\<Gamma> \<turnstile> s\<^isub>1 \<equiv> t\<^isub>1 : T\<^isub>2" 
   1.198 +  and     b: "\<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1"
   1.199 +  shows "\<Gamma> \<turnstile> App (Lam [x]. s\<^isub>1) s\<^isub>2 \<equiv> t\<^isub>1[x::=t\<^isub>2] : T\<^isub>2"
   1.200 +using a b
   1.201 +apply(rule_tac Q_Beta)
   1.202 +apply(auto)
   1.203 +apply(drule def_equiv_implies_valid)
   1.204 +apply(drule valid.cases)
   1.205 +apply(auto)
   1.206 +apply(drule test3)
   1.207 +apply(auto simp add: fresh_def supp_prod)
   1.208 +done
   1.209 +
   1.210 +lemma test1:
   1.211 +  assumes a: "\<forall>x. x\<sharp>\<Gamma> \<longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
   1.212 +  shows "\<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
   1.213 +using a
   1.214 +apply -
   1.215 +apply(generate_fresh "name")
   1.216 +apply(rule_tac x="c" in Q_Ext)
   1.217 +apply(simp)
   1.218 +apply(simp add: fresh_prod)
   1.219 +done
   1.220 +
   1.221 +lemma test2:
   1.222 +  assumes a: "x\<sharp>(\<Gamma>,s,t) \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
   1.223 +  shows "\<forall>x. x\<sharp>(\<Gamma>,s,t) \<longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
   1.224 +using a
   1.225 +apply -
   1.226 +apply(rule allI)
   1.227 +apply(case_tac "xa=x")
   1.228 +apply(simp)
   1.229 +apply(rule impI)
   1.230 +apply(erule conjE)
   1.231 +apply(drule_tac pi="[(x,xa)]" in def_equiv.eqvt)
   1.232 +apply(simp add: eqvts)
   1.233 +apply(simp add: calc_atm)
   1.234 +apply(perm_simp)
   1.235 +done
   1.236 +
   1.237 +lemma test2:
   1.238 +  assumes a: "x\<sharp>(\<Gamma>,s,t) \<and> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
   1.239 +  shows "\<forall>x. x\<sharp>\<Gamma> \<longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2"
   1.240 +using a
   1.241 +apply -
   1.242 +apply(rule allI)
   1.243 +apply(case_tac "xa=x")
   1.244 +apply(simp)
   1.245 +apply(rule impI)
   1.246 +apply(erule conjE)
   1.247 +apply(frule test3)
   1.248 +apply(simp add: supp_prod supp_list_cons supp_atm trm.supp)
   1.249 +apply(subgoal_tac "xa\<sharp>(s,t)")
   1.250 +apply(drule_tac pi="[(x,xa)]" in def_equiv.eqvt)
   1.251 +apply(simp add: eqvts)
   1.252 +apply(simp add: calc_atm)
   1.253 +apply(perm_simp)
   1.254 +apply(simp add: fresh_def supp_prod)
   1.255 +apply(auto)
   1.256 +done
   1.257 +
   1.258 +
   1.259  section {* Weak Head Reduction *}
   1.260  
   1.261  inductive
   1.262 @@ -367,16 +490,15 @@
   1.263  declare trm.inject  [simp add]
   1.264  declare ty.inject  [simp add]
   1.265  
   1.266 -inductive_cases whr_inv_auto[elim]: 
   1.267 -  "t \<leadsto> t'"
   1.268 -  "Lam [x].t \<leadsto> t'"
   1.269 -  "App (Lam [x].t12) t2 \<leadsto> t"
   1.270 -  "Var x \<leadsto> t"
   1.271 -  "Const n \<leadsto> t"
   1.272 -  "App p q \<leadsto> t"
   1.273 -  "t \<leadsto> Const n"
   1.274 -  "t \<leadsto> Var x"
   1.275 -  "t \<leadsto> App p q"
   1.276 +inductive_cases whr_Gen[elim]: "t \<leadsto> t'"
   1.277 +inductive_cases whr_Lam[elim]: "Lam [x].t \<leadsto> t'"
   1.278 +inductive_cases whr_App_Lam[elim]: "App (Lam [x].t12) t2 \<leadsto> t"
   1.279 +inductive_cases whr_Var[elim]: "Var x \<leadsto> t"
   1.280 +inductive_cases whr_Const[elim]: "Const n \<leadsto> t"
   1.281 +inductive_cases whr_App[elim]: "App p q \<leadsto> t"
   1.282 +inductive_cases whr_Const_Right[elim]: "t \<leadsto> Const n"
   1.283 +inductive_cases whr_Var_Right[elim]: "t \<leadsto> Var x"
   1.284 +inductive_cases whr_App_Right[elim]: "t \<leadsto> App p q"
   1.285  
   1.286  declare trm.inject  [simp del]
   1.287  declare ty.inject  [simp del]
   1.288 @@ -423,12 +545,12 @@
   1.289    shows "a=b"
   1.290    using a b
   1.291  apply (induct arbitrary: b)
   1.292 -apply (erule whr_inv_auto(3))
   1.293 +apply (erule whr_App_Lam)
   1.294  apply (clarify)
   1.295  apply (rule subst_fun_eq)
   1.296  apply (simp)
   1.297  apply (force)
   1.298 -apply (erule whr_inv_auto(6))
   1.299 +apply (erule whr_App)
   1.300  apply (blast)+
   1.301  done
   1.302  
   1.303 @@ -438,7 +560,7 @@
   1.304    using assms 
   1.305  proof (induct arbitrary: b)
   1.306    case (QAN_Reduce x t a b)
   1.307 -  have h:"x \<leadsto> t" "t \<Down> a" by fact+
   1.308 +  have h:"x \<leadsto> t" "t \<Down> a" by fact
   1.309    have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact
   1.310    have "x \<Down> b" by fact
   1.311    then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto
   1.312 @@ -446,6 +568,20 @@
   1.313    then show "a=b" using ih hl by auto
   1.314  qed (auto)
   1.315  
   1.316 +lemma test4a:
   1.317 +  shows "s \<leadsto> t \<Longrightarrow> (supp t) \<subseteq> ((supp s)::name set)"
   1.318 +apply(induct s t rule: whr_def.induct)
   1.319 +apply(insert test3b)
   1.320 +apply(simp add: trm.supp supp_prod abs_supp)
   1.321 +apply(auto simp add: trm.supp)
   1.322 +done
   1.323 +
   1.324 +lemma test4b:
   1.325 +  shows "s \<Down> t \<Longrightarrow> (supp t) \<subseteq> ((supp s)::name set)"
   1.326 +apply(induct s t rule: whn_def.induct)
   1.327 +apply(auto dest: test4a)
   1.328 +done
   1.329 +
   1.330  section {* Algorithmic Term Equivalence and Algorithmic Path Equivalence *}
   1.331  
   1.332  inductive
   1.333 @@ -467,27 +603,27 @@
   1.334    avoids QAT_Arrow: x
   1.335    by simp_all
   1.336  
   1.337 +
   1.338  declare trm.inject [simp add]
   1.339  declare ty.inject  [simp add]
   1.340  
   1.341 -inductive_cases alg_equiv_inv_auto[elim]: 
   1.342 -  "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
   1.343 -  "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
   1.344 +inductive_cases alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
   1.345 +inductive_cases alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
   1.346 +
   1.347 +inductive_cases alg_path_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
   1.348 +inductive_cases alg_path_equiv_Unit_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
   1.349 +inductive_cases alg_path_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
   1.350  
   1.351 -inductive_cases alg_path_equiv_inv_auto[elim]: 
   1.352 -  "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
   1.353 -  "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
   1.354 -  "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
   1.355 -  "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
   1.356 -  "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
   1.357 -  "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
   1.358 -  "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
   1.359 -  "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
   1.360 -  "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
   1.361 -  "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
   1.362 -  "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
   1.363 -  "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
   1.364 -  "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
   1.365 +inductive_cases alg_path_equiv_Var_left_inv_auto[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
   1.366 +inductive_cases alg_path_equiv_Var_left_inv_auto'[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
   1.367 +inductive_cases alg_path_equiv_Var_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
   1.368 +inductive_cases alg_path_equiv_Var_right_inv_auto'[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
   1.369 +inductive_cases alg_path_equiv_Const_left_inv_auto[elim]: "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
   1.370 +inductive_cases alg_path_equiv_Const_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
   1.371 +inductive_cases alg_path_equiv_App_left_inv_auto[elim]: "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
   1.372 +inductive_cases alg_path_equiv_App_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
   1.373 +inductive_cases alg_path_equiv_Lam_left_inv_auto[elim]: "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
   1.374 +inductive_cases alg_path_equiv_Lam_right_inv_auto[elim]: "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
   1.375  
   1.376  declare trm.inject [simp del]
   1.377  declare ty.inject [simp del]
   1.378 @@ -522,14 +658,14 @@
   1.379    case (QAP_Var \<Gamma> x T u T')
   1.380    have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact
   1.381    then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto
   1.382 -  moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact+
   1.383 +  moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact
   1.384    ultimately show "T=T'" using type_unicity_in_context by auto
   1.385  next
   1.386    case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u T\<^isub>2')
   1.387 -  have ih: "\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
   1.388 +  have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
   1.389    have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2'" by fact
   1.390    then obtain r t T\<^isub>1' where "u = App r t"  "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
   1.391 -  with ih have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
   1.392 +  then have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
   1.393    then show "T\<^isub>2=T\<^isub>2'" using ty.inject by auto
   1.394  qed (auto)
   1.395  
   1.396 @@ -562,7 +698,7 @@
   1.397    case (QAT_Arrow  x \<Gamma> s t T\<^isub>1 T\<^isub>2 u)
   1.398    have ih:"(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2 
   1.399                                     \<Longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by fact
   1.400 -  have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact+
   1.401 +  have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact 
   1.402    have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
   1.403    then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" using fs 
   1.404      by (simp add: Q_Arrow_strong_inversion)
   1.405 @@ -595,7 +731,7 @@
   1.406    and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
   1.407  proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv.strong_inducts)
   1.408   case (QAT_Arrow x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
   1.409 -  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact+
   1.410 +  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact
   1.411    have h2:"\<Gamma> \<subseteq> \<Gamma>'" by fact
   1.412    have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
   1.413    have "valid \<Gamma>'" by fact
   1.414 @@ -643,8 +779,8 @@
   1.415  next
   1.416    case (3 \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>')
   1.417    have "\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" 
   1.418 -  and "\<Gamma> \<subseteq> \<Gamma>'" 
   1.419 -  and "valid \<Gamma>'" by fact+
   1.420 +  and  "\<Gamma> \<subseteq> \<Gamma>'" 
   1.421 +  and  "valid \<Gamma>'" by fact
   1.422    then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by simp
   1.423  qed (auto)
   1.424  
   1.425 @@ -781,10 +917,10 @@
   1.426  qed
   1.427  
   1.428  lemma logical_subst_monotonicity :
   1.429 -  assumes a: "\<Gamma>' \<turnstile> s is t over \<Gamma>" 
   1.430 +  assumes a: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   1.431    and     b: "\<Gamma>' \<subseteq> \<Gamma>''"
   1.432    and     c: "valid \<Gamma>''"
   1.433 -  shows "\<Gamma>'' \<turnstile> s is t over \<Gamma>"
   1.434 +  shows "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
   1.435  using a b c logical_monotonicity by blast
   1.436  
   1.437  lemma equiv_subst_ext :
   1.438 @@ -800,48 +936,54 @@
   1.439      moreover
   1.440      { 
   1.441        assume "(y,U) \<in> set [(x,T)]"
   1.442 -      with h2 have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
   1.443 +      then have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto 
   1.444      }
   1.445      moreover
   1.446      {
   1.447        assume hl:"(y,U) \<in> set \<Gamma>"
   1.448        then have "\<not> y\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_atm fresh_prod)
   1.449        then have hf:"x\<sharp> Var y" using fs by (auto simp add: fresh_atm)
   1.450 -      then have "(x,s)#\<theta><Var y> = \<theta><Var y>" "(x,t)#\<theta>'<Var y> = \<theta>'<Var y>" using fresh_psubst_simp by blast+ 
   1.451 +      then have "((x,s)#\<theta>)<Var y> = \<theta><Var y>" "((x,t)#\<theta>')<Var y> = \<theta>'<Var y>" 
   1.452 +	using fresh_psubst_simp by blast+ 
   1.453        moreover have  "\<Gamma>' \<turnstile> \<theta><Var y> is \<theta>'<Var y> : U" using h1 hl by auto
   1.454 -      ultimately have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
   1.455 +      ultimately have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto
   1.456      }
   1.457 -    ultimately have "\<Gamma>' \<turnstile> (x,s)#\<theta><Var y> is (x,t)#\<theta>'<Var y> : U" by auto
   1.458 +    ultimately have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto
   1.459    }
   1.460    then show "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>" by auto
   1.461  qed
   1.462  
   1.463  theorem fundamental_theorem_1:
   1.464 -  assumes h1: "\<Gamma> \<turnstile> t : T" 
   1.465 -  and     h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
   1.466 -  and     h3: "valid \<Gamma>'" 
   1.467 +  assumes a1: "\<Gamma> \<turnstile> t : T" 
   1.468 +  and     a2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
   1.469 +  and     a3: "valid \<Gamma>'" 
   1.470    shows "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T"   
   1.471 -using h1 h2 h3
   1.472 -proof (nominal_induct \<Gamma> t T avoiding: \<Gamma>' \<theta> \<theta>'  rule: typing.strong_induct)
   1.473 -  case (t_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
   1.474 -  have fs:"x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact+
   1.475 -  have h:"\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
   1.476 -  have ih:"\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
   1.477 -  {
   1.478 +using a1 a2 a3
   1.479 +proof (nominal_induct \<Gamma> t T avoiding: \<theta> \<theta>' arbitrary: \<Gamma>' rule: typing.strong_induct)
   1.480 +  case (T_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<theta> \<theta>' \<Gamma>')
   1.481 +  have vc: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact
   1.482 +  have asm1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
   1.483 +  have ih:"\<And>\<theta> \<theta>' \<Gamma>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
   1.484 +  show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using vc
   1.485 +  proof (simp, intro strip)
   1.486      fix \<Gamma>'' s' t'
   1.487 -    assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and v: "valid \<Gamma>''"
   1.488 -    then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity h by blast
   1.489 -    then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
   1.490 -    then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><t\<^isub>2> is (x,t')#\<theta>'<t\<^isub>2> : T\<^isub>2" using ih v by auto
   1.491 -    then have "\<Gamma>''\<turnstile>\<theta><t\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" using psubst_subst_psubst fs by simp
   1.492 -    moreover have "App (Lam [x].\<theta><t\<^isub>2>) s' \<leadsto> \<theta><t\<^isub>2>[x::=s']" by auto
   1.493 -    moreover have "App (Lam [x].\<theta>'<t\<^isub>2>) t' \<leadsto> \<theta>'<t\<^isub>2>[x::=t']" by auto
   1.494 -    ultimately have "\<Gamma>''\<turnstile> App (Lam [x].\<theta><t\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2" 
   1.495 +    assume sub: "\<Gamma>' \<subseteq> \<Gamma>''" 
   1.496 +    and    asm2: "\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" 
   1.497 +    and    val: "valid \<Gamma>''"
   1.498 +    from asm1 val sub have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity by blast
   1.499 +    with asm2 vc have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext by blast
   1.500 +    with ih val have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<t\<^isub>2> is ((x,t')#\<theta>')<t\<^isub>2> : T\<^isub>2" by auto
   1.501 +    with vc have "\<Gamma>''\<turnstile>\<theta><t\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" by (simp add: psubst_subst_psubst)
   1.502 +    moreover 
   1.503 +    have "App (Lam [x].\<theta><t\<^isub>2>) s' \<leadsto> \<theta><t\<^isub>2>[x::=s']" by auto
   1.504 +    moreover 
   1.505 +    have "App (Lam [x].\<theta>'<t\<^isub>2>) t' \<leadsto> \<theta>'<t\<^isub>2>[x::=t']" by auto
   1.506 +    ultimately show "\<Gamma>''\<turnstile> App (Lam [x].\<theta><t\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2" 
   1.507        using logical_weak_head_closure by auto
   1.508 -  }
   1.509 -  then show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by simp 
   1.510 +  qed
   1.511  qed (auto)
   1.512  
   1.513 +
   1.514  theorem fundamental_theorem_2:
   1.515    assumes h1: "\<Gamma> \<turnstile> s \<equiv> t : T" 
   1.516    and     h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
   1.517 @@ -851,14 +993,14 @@
   1.518  proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<theta> \<theta>' rule: def_equiv.strong_induct)
   1.519    case (Q_Refl \<Gamma> t T \<Gamma>' \<theta> \<theta>')
   1.520    have "\<Gamma> \<turnstile> t : T" 
   1.521 -  and  "valid \<Gamma>'" by fact+
   1.522 +  and  "valid \<Gamma>'" by fact
   1.523    moreover 
   1.524    have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
   1.525    ultimately show "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" using fundamental_theorem_1 by blast
   1.526  next
   1.527    case (Q_Symm \<Gamma> t s T \<Gamma>' \<theta> \<theta>')
   1.528    have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   1.529 -  and "valid \<Gamma>'" by fact+
   1.530 +  and "valid \<Gamma>'" by fact
   1.531    moreover 
   1.532    have ih: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<s> : T" by fact
   1.533    ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using logical_symmetry by blast
   1.534 @@ -867,7 +1009,7 @@
   1.535    have ih1: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" by fact
   1.536    have ih2: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<u> : T" by fact
   1.537    have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   1.538 -  and  v: "valid \<Gamma>'" by fact+
   1.539 +  and  v: "valid \<Gamma>'" by fact
   1.540    then have "\<Gamma>' \<turnstile> \<theta>' is \<theta>' over \<Gamma>" using logical_pseudo_reflexivity by auto
   1.541    then have "\<Gamma>' \<turnstile> \<theta>'<t> is \<theta>'<u> : T" using ih2 v by auto
   1.542    moreover have "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using ih1 h v by auto
   1.543 @@ -875,23 +1017,23 @@
   1.544  next
   1.545    case (Q_Abs x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
   1.546    have fs:"x\<sharp>\<Gamma>" by fact
   1.547 -  have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
   1.548 +  have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact 
   1.549    have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   1.550 -  and  h3: "valid \<Gamma>'" by fact+
   1.551 +  and  h3: "valid \<Gamma>'" by fact
   1.552    have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
   1.553    {
   1.554      fix \<Gamma>'' s' t'
   1.555      assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and hk: "valid \<Gamma>''"
   1.556      then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast
   1.557      then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
   1.558 -    then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><s\<^isub>2> is (x,t')#\<theta>'<t\<^isub>2> : T\<^isub>2" using ih hk by blast
   1.559 +    then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<s\<^isub>2> is ((x,t')#\<theta>')<t\<^isub>2> : T\<^isub>2" using ih hk by blast
   1.560      then have "\<Gamma>''\<turnstile> \<theta><s\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" using fs2 psubst_subst_psubst by auto
   1.561      moreover have "App (Lam [x]. \<theta><s\<^isub>2>) s' \<leadsto>  \<theta><s\<^isub>2>[x::=s']" 
   1.562                and "App (Lam [x].\<theta>'<t\<^isub>2>) t' \<leadsto> \<theta>'<t\<^isub>2>[x::=t']" by auto
   1.563      ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<theta><s\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2" 
   1.564        using logical_weak_head_closure by auto
   1.565    }
   1.566 -  moreover have "valid \<Gamma>'" using h3 by auto
   1.567 +  moreover have "valid \<Gamma>'" using h2 by auto
   1.568    ultimately have "\<Gamma>' \<turnstile> Lam [x].\<theta><s\<^isub>2> is Lam [x].\<theta>'<t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
   1.569    then show "\<Gamma>' \<turnstile> \<theta><Lam [x].s\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs2 by auto
   1.570  next
   1.571 @@ -900,14 +1042,14 @@
   1.572  next
   1.573    case (Q_Beta x \<Gamma> s\<^isub>2 t\<^isub>2 T\<^isub>1 s12 t12 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
   1.574    have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   1.575 -  and  h': "valid \<Gamma>'" by fact+
   1.576 +  and  h': "valid \<Gamma>'" by fact
   1.577    have fs: "x\<sharp>\<Gamma>" by fact
   1.578 -  have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
   1.579 +  have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact 
   1.580    have ih1: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" by fact
   1.581    have ih2: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s12> is \<theta>'<t12> : T\<^isub>2" by fact
   1.582    have "\<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" using ih1 h' h by auto
   1.583    then have "\<Gamma>' \<turnstile> (x,\<theta><s\<^isub>2>)#\<theta> is (x,\<theta>'<t\<^isub>2>)#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext h fs by blast
   1.584 -  then have "\<Gamma>' \<turnstile> (x,\<theta><s\<^isub>2>)#\<theta><s12> is (x,\<theta>'<t\<^isub>2>)#\<theta>'<t12> : T\<^isub>2" using ih2 h' by auto
   1.585 +  then have "\<Gamma>' \<turnstile> ((x,\<theta><s\<^isub>2>)#\<theta>)<s12> is ((x,\<theta>'<t\<^isub>2>)#\<theta>')<t12> : T\<^isub>2" using ih2 h' by auto
   1.586    then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^isub>2>] is \<theta>'<t12>[x::=\<theta>'<t\<^isub>2>] : T\<^isub>2" using fs2 psubst_subst_psubst by auto
   1.587    then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^isub>2>] is \<theta>'<t12[x::=t\<^isub>2]> : T\<^isub>2" using fs2 psubst_subst_propagate by auto
   1.588    moreover have "App (Lam [x].\<theta><s12>) (\<theta><s\<^isub>2>) \<leadsto> \<theta><s12>[x::=\<theta><s\<^isub>2>]" by auto 
   1.589 @@ -917,8 +1059,8 @@
   1.590  next
   1.591    case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
   1.592    have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   1.593 -  and  h2': "valid \<Gamma>'" by fact+
   1.594 -  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact+
   1.595 +  and  h2': "valid \<Gamma>'" by fact
   1.596 +  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
   1.597    have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> 
   1.598                            \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^isub>2" by fact
   1.599     {
   1.600 @@ -926,14 +1068,14 @@
   1.601      assume hsub: "\<Gamma>' \<subseteq> \<Gamma>''" and hl: "\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and hk: "valid \<Gamma>''"
   1.602      then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast
   1.603      then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
   1.604 -    then have "\<Gamma>'' \<turnstile> (x,s')#\<theta><App s (Var x)>  is (x,t')#\<theta>'<App t (Var x)> : T\<^isub>2" using ih hk by blast
   1.605 +    then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<App s (Var x)>  is ((x,t')#\<theta>')<App t (Var x)> : T\<^isub>2" using ih hk by blast
   1.606      then 
   1.607 -    have "\<Gamma>'' \<turnstile> App (((x,s')#\<theta>)<s>) (((x,s')#\<theta>)<(Var x)>) is App ((x,t')#\<theta>'<t>) ((x,t')#\<theta>'<(Var x)>) : T\<^isub>2"
   1.608 +    have "\<Gamma>'' \<turnstile> App (((x,s')#\<theta>)<s>) (((x,s')#\<theta>)<(Var x)>) is App (((x,t')#\<theta>')<t>) (((x,t')#\<theta>')<(Var x)>) : T\<^isub>2"
   1.609        by auto
   1.610 -    then have "\<Gamma>'' \<turnstile> App ((x,s')#\<theta><s>) s'  is App ((x,t')#\<theta>'<t>) t' : T\<^isub>2" by auto
   1.611 +    then have "\<Gamma>'' \<turnstile> App ((x,s')#\<theta>)<s> s'  is App ((x,t')#\<theta>')<t> t' : T\<^isub>2" by auto
   1.612      then have "\<Gamma>'' \<turnstile> App (\<theta><s>) s' is App (\<theta>'<t>) t' : T\<^isub>2" using fs fresh_psubst_simp by auto
   1.613    }
   1.614 -  moreover have "valid \<Gamma>'" using h2' by auto
   1.615 +  moreover have "valid \<Gamma>'" using h2 by auto
   1.616    ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
   1.617  next
   1.618    case (Q_Unit \<Gamma> s t \<Gamma>' \<theta> \<theta>')