alternative and much simpler proof for Church-Rosser of Beta-Reduction
authorurbanc
Fri Apr 27 14:21:23 2007 +0200 (2007-04-27)
changeset 2282115b2e7ec1f3b
parent 22820 e6803064a469
child 22822 c1a6a2159e69
alternative and much simpler proof for Church-Rosser of Beta-Reduction
src/HOL/IsaMakefile
src/HOL/Nominal/Examples/CR_Takahashi.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 27 05:53:37 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 27 14:21:23 2007 +0200
     1.3 @@ -748,6 +748,7 @@
     1.4  $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
     1.5    Nominal/Examples/ROOT.ML \
     1.6    Nominal/Examples/CR.thy \
     1.7 +  Nominal/Examples/CR_Takahashi.thy \
     1.8    Nominal/Examples/Class.thy \
     1.9    Nominal/Examples/Compile.thy \
    1.10    Nominal/Examples/Fsub.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Fri Apr 27 14:21:23 2007 +0200
     2.3 @@ -0,0 +1,454 @@
     2.4 +(* $Id$ *)
     2.5 +
     2.6 +theory CR_Takahashi
     2.7 +imports Lam_Funs
     2.8 +begin
     2.9 +
    2.10 +text {* The Church-Rosser proof from a paper by Masako Takahashi;
    2.11 +        our formalisation follows with some slight exceptions the one 
    2.12 +        done by Randy Pollack and James McKinna from their 1993 
    2.13 +        TLCA-paper; the proof is simpler by using an auxiliary
    2.14 +        reduction relation called complete development reduction.
    2.15 +      
    2.16 +        Authors: Mathilde Arnaud and Christian Urban
    2.17 +     *}
    2.18 +
    2.19 +lemma forget:
    2.20 +  assumes asm: "x\<sharp>L"
    2.21 +  shows "L[x::=P] = L"
    2.22 +  using asm 
    2.23 +by (nominal_induct L avoiding: x P rule: lam.induct)
    2.24 +   (auto simp add: abs_fresh fresh_atm)
    2.25 +
    2.26 +lemma fresh_fact:
    2.27 +  fixes z::"name"
    2.28 +  assumes asms: "z\<sharp>N" "z\<sharp>L"
    2.29 +  shows "z\<sharp>(N[y::=L])"
    2.30 +  using asms 
    2.31 +by (nominal_induct N avoiding: z y L rule: lam.induct)
    2.32 +   (auto simp add: abs_fresh fresh_atm)
    2.33 +
    2.34 +lemma fresh_fact': 
    2.35 +  fixes a::"name"
    2.36 +  assumes a: "a\<sharp>t2"
    2.37 +  shows "a\<sharp>t1[a::=t2]"
    2.38 +using a 
    2.39 +by (nominal_induct t1 avoiding: a t2 rule: lam.induct)
    2.40 +   (auto simp add: abs_fresh fresh_atm)
    2.41 +
    2.42 +lemma substitution_lemma:  
    2.43 +  assumes asm: "x\<noteq>y" "x\<sharp>L"
    2.44 +  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
    2.45 +  using asm 
    2.46 +by (nominal_induct M avoiding: x y N L rule: lam.induct)
    2.47 +   (auto simp add: fresh_fact forget)
    2.48 +
    2.49 +section {* Beta Reduction *}
    2.50 +
    2.51 +inductive2
    2.52 +  "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
    2.53 +where
    2.54 +    b1[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
    2.55 +  | b2[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
    2.56 +  | b3[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"
    2.57 +  | b4[intro]: "a\<sharp>s2 \<Longrightarrow> (App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
    2.58 +
    2.59 +equivariance Beta
    2.60 +
    2.61 +nominal_inductive Beta
    2.62 +  by (simp_all add: abs_fresh fresh_fact')
    2.63 +
    2.64 +inductive2
    2.65 +  "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
    2.66 +where
    2.67 +    bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
    2.68 +  | bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
    2.69 +
    2.70 +equivariance Beta_star
    2.71 +
    2.72 +lemma beta_star_trans:
    2.73 +  assumes a1: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
    2.74 +  and     a2: "M2\<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
    2.75 +  shows "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
    2.76 +using a2 a1
    2.77 +by (induct) (auto)
    2.78 +
    2.79 +section {* One-Reduction *}
    2.80 +
    2.81 +inductive2
    2.82 +  One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
    2.83 +where
    2.84 +    o1[intro!]:      "M\<longrightarrow>\<^isub>1M"
    2.85 +  | o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2;s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^isub>1(App t2 s2)"
    2.86 +  | o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)"
    2.87 +  | o4[simp,intro!]: "\<lbrakk>a\<sharp>(s1,s2); s1\<longrightarrow>\<^isub>1s2;t1\<longrightarrow>\<^isub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^isub>1(t2[a::=s2])"
    2.88 +
    2.89 +equivariance One
    2.90 +
    2.91 +nominal_inductive One
    2.92 +  by (simp_all add: abs_fresh fresh_fact')
    2.93 +
    2.94 +lemma one_subst_aux:
    2.95 +  assumes a: "N\<longrightarrow>\<^isub>1N'"
    2.96 +  shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
    2.97 +using a
    2.98 +by (nominal_induct M avoiding: x N N' rule: lam.induct)
    2.99 +   (auto simp add: fresh_prod fresh_atm)
   2.100 +
   2.101 +lemma one_subst: 
   2.102 +  assumes a: "M\<longrightarrow>\<^isub>1M'" 
   2.103 +  and     b: "N\<longrightarrow>\<^isub>1N'"
   2.104 +  shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
   2.105 +using a b
   2.106 +by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
   2.107 +   (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
   2.108 +
   2.109 +inductive2
   2.110 +  "One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
   2.111 +where
   2.112 +    os1[intro, simp]: "M \<longrightarrow>\<^isub>1\<^sup>* M"
   2.113 +  | os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>1\<^sup>* M2; M2 \<longrightarrow>\<^isub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>1\<^sup>* M3"
   2.114 +
   2.115 +equivariance One_star 
   2.116 +
   2.117 +lemma one_star_trans:
   2.118 +  assumes a1: "M1\<longrightarrow>\<^isub>1\<^sup>* M2" 
   2.119 +  and     a2: "M2\<longrightarrow>\<^isub>1\<^sup>* M3"
   2.120 +  shows "M1\<longrightarrow>\<^isub>1\<^sup>* M3"
   2.121 +using a2 a1
   2.122 +by (induct) (auto)
   2.123 +
   2.124 +lemma one_fresh_preserv:
   2.125 +  fixes a :: "name"
   2.126 +  assumes a: "t\<longrightarrow>\<^isub>1s"
   2.127 +  and     b: "a\<sharp>t"
   2.128 +  shows "a\<sharp>s"
   2.129 +using a b
   2.130 +by (nominal_induct avoiding: a rule: One.strong_induct)
   2.131 +   (auto simp add: abs_fresh fresh_atm fresh_fact)
   2.132 +
   2.133 +lemma subst_rename: 
   2.134 +  assumes a: "c\<sharp>t1"
   2.135 +  shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
   2.136 +using a
   2.137 +by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
   2.138 +   (auto simp add: calc_atm fresh_atm abs_fresh)
   2.139 +
   2.140 +lemma one_var:
   2.141 +  assumes a: "Var x \<longrightarrow>\<^isub>1 t"
   2.142 +  shows "t = Var x"
   2.143 +using a
   2.144 +by - (ind_cases2 "Var x \<longrightarrow>\<^isub>1 t", simp)
   2.145 +
   2.146 +lemma one_abs: 
   2.147 +  fixes    t :: "lam"
   2.148 +  and      t':: "lam"
   2.149 +  and      a :: "name"
   2.150 +  assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'"
   2.151 +  shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
   2.152 +  using a
   2.153 +  apply -
   2.154 +  apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
   2.155 +  apply(auto simp add: lam.inject alpha)
   2.156 +  apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   2.157 +  apply(rule conjI)
   2.158 +  apply(perm_simp)
   2.159 +  apply(simp add: fresh_left calc_atm)
   2.160 +  apply(simp add: One.eqvt)
   2.161 +  apply(simp add: one_fresh_preserv)
   2.162 +done  
   2.163 +
   2.164 +lemma one_app: 
   2.165 +  assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
   2.166 +  shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
   2.167 +         (\<exists>a s s1 s2. t1 = Lam [a].s \<and> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
   2.168 +  using a
   2.169 +  apply -
   2.170 +  apply(ind_cases2 "App t1 t2 \<longrightarrow>\<^isub>1 t'")
   2.171 +  apply(auto simp add: lam.distinct lam.inject)
   2.172 +  done
   2.173 +
   2.174 +lemma one_red: 
   2.175 +  assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M"
   2.176 +  shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
   2.177 +         (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
   2.178 +  using a
   2.179 +  apply -
   2.180 +  apply(ind_cases2 "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
   2.181 +  apply(simp_all add: lam.inject)
   2.182 +  apply(force)
   2.183 +  apply(erule conjE)
   2.184 +  apply(drule sym[of "Lam [a].t1"])
   2.185 +  apply(simp)
   2.186 +  apply(drule one_abs)
   2.187 +  apply(erule exE)
   2.188 +  apply(simp)
   2.189 +  apply(force simp add: alpha)
   2.190 +  apply(erule conjE)
   2.191 +  apply(simp add: lam.inject alpha)
   2.192 +  apply(erule disjE)
   2.193 +  apply(simp)
   2.194 +  apply(force)
   2.195 +  apply(simp)
   2.196 +  apply(rule disjI2)
   2.197 +  apply(rule_tac x="[(a,aa)]\<bullet>t2a" in exI)
   2.198 +  apply(rule_tac x="s2" in exI)
   2.199 +  apply(auto)
   2.200 +  apply(subgoal_tac "a\<sharp>t2a")(*A*)
   2.201 +  apply(simp add: subst_rename)
   2.202 +  (*A*)
   2.203 +  apply(force intro: one_fresh_preserv)
   2.204 +  apply(simp add: One.eqvt)
   2.205 +  done
   2.206 +
   2.207 +text {* complete development reduction *}
   2.208 +
   2.209 +inductive2
   2.210 +  cd1 :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ >c _" [80,80]80)
   2.211 +where
   2.212 +  cd1v[intro!]:      "Var x >c Var x"
   2.213 +  | cd1l[simp,intro!]: "s1 >c s2 \<Longrightarrow> Lam [a].s1 >c Lam[a].s2"
   2.214 +  | cd1a[simp,intro!]: "\<lbrakk>\<not>(\<exists> a s. s1 = Lam [a].s); s1 >c s2; t1 >c t2\<rbrakk> \<Longrightarrow> App s1 t1 >c App s2 t2"
   2.215 +  | cd1r[simp,intro!]: "\<lbrakk>a\<sharp>(s1,s2); s1 >c s2; t1 >c t2\<rbrakk> \<Longrightarrow> App (Lam [a].t1) s1 >c (t2[a::=s2])"
   2.216 +
   2.217 +(* FIXME: needs to be in nominal_inductive *)
   2.218 +declare perm_pi_simp[eqvt_force]
   2.219 +
   2.220 +equivariance cd1
   2.221 +
   2.222 +nominal_inductive cd1
   2.223 +  by (simp_all add: abs_fresh fresh_fact')
   2.224 +
   2.225 +lemma better_cd1r_intro[intro]:
   2.226 +  assumes a: "s1 >c s2"
   2.227 +  and     b: "t1 >c t2"
   2.228 +  shows "App (Lam [a].t1) s1 >c (t2[a::=s2])"
   2.229 +proof -
   2.230 +  obtain c::"name" where fs: "c\<sharp>(a,t1,s1,t2,s2)" by (rule exists_fresh, rule fin_supp,blast)
   2.231 +  have eq1: "Lam [a].t1 = Lam [c].([(c,a)]\<bullet>t1)" using fs
   2.232 +    by (rule_tac sym, auto simp add: lam.inject alpha fresh_prod fresh_atm)
   2.233 +  have "App (Lam [a].t1) s1 = App (Lam [c].([(c,a)]\<bullet>t1)) s1"
   2.234 +    using eq1 by simp
   2.235 +  also have "\<dots> >c  ([(c,a)]\<bullet>t2)[c::=s2]" using fs a b
   2.236 +    by (rule_tac cd1r, simp_all add: cd1.eqvt)
   2.237 +  also have "\<dots> = t2[a::=s2]" using fs 
   2.238 +    by (rule_tac subst_rename[symmetric], simp)
   2.239 +  finally show "App (Lam [a].t1) s1 >c (t2[a::=s2])" by simp
   2.240 +qed
   2.241 +
   2.242 +lemma cd1_fresh_preserve:
   2.243 +  fixes a::"name"
   2.244 +  assumes a: "a\<sharp>s1" 
   2.245 +  and     b: "s1 >c s2"
   2.246 +  shows "a\<sharp>s2"
   2.247 +using b a
   2.248 +by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
   2.249 +
   2.250 +  
   2.251 +lemma cd1_lam:
   2.252 +  fixes c::"'a::fs_name"
   2.253 +  assumes a: "Lam [a].t >c t'"
   2.254 +  shows "\<exists>s. t'=Lam [a].s \<and> t >c s"
   2.255 +using a
   2.256 +apply -
   2.257 +apply(erule cd1.cases)
   2.258 +apply(simp_all)
   2.259 +apply(simp add: lam.inject)
   2.260 +apply(simp add: alpha)
   2.261 +apply(auto)
   2.262 +apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   2.263 +apply(perm_simp add: fresh_left cd1.eqvt cd1_fresh_preserve)
   2.264 +done
   2.265 +
   2.266 +lemma develop_existence:
   2.267 +  shows "\<exists>M'. M >c M'"
   2.268 +by (nominal_induct M rule: lam.induct)
   2.269 +   (auto dest!: cd1_lam)
   2.270 +
   2.271 +lemma triangle:
   2.272 +  assumes a: "M >c M'"
   2.273 +  and     b: "M \<longrightarrow>\<^isub>1 M''"
   2.274 +  shows "M'' \<longrightarrow>\<^isub>1 M'"
   2.275 +using a b
   2.276 +by (nominal_induct avoiding: M'' rule: cd1.strong_induct)
   2.277 +   (auto dest!: one_var one_app one_abs one_red intro: one_subst)
   2.278 +
   2.279 +lemma diamond:
   2.280 +  assumes a: "M1 \<longrightarrow>\<^isub>1 M2"
   2.281 +  and     b: "M1 \<longrightarrow>\<^isub>1 M3"
   2.282 +  shows "\<exists>M4. M2 \<longrightarrow>\<^isub>1 M4 \<and> M3 \<longrightarrow>\<^isub>1 M4"
   2.283 +proof -
   2.284 +  obtain Mc where c: "M1 >c Mc" using develop_existence by blast
   2.285 +  have "M2 \<longrightarrow>\<^isub>1 Mc" using a c by (simp add: triangle)
   2.286 +  moreover
   2.287 +  have "M3 \<longrightarrow>\<^isub>1 Mc" using b c by (simp add: triangle)
   2.288 +  ultimately show "\<exists>M4. M2 \<longrightarrow>\<^isub>1 M4 \<and> M3 \<longrightarrow>\<^isub>1 M4" by blast
   2.289 +qed
   2.290 +  
   2.291 +lemma one_lam_cong: 
   2.292 +  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   2.293 +  shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)"
   2.294 +  using a
   2.295 +proof induct
   2.296 +  case bs1 thus ?case by simp
   2.297 +next
   2.298 +  case (bs2 y z) 
   2.299 +  thus ?case by (blast dest: b3)
   2.300 +qed
   2.301 +
   2.302 +lemma one_app_congL: 
   2.303 +  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   2.304 +  shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
   2.305 +  using a
   2.306 +proof induct
   2.307 +  case bs1 thus ?case by simp
   2.308 +next
   2.309 +  case bs2 thus ?case by (blast dest: b1)
   2.310 +qed
   2.311 +  
   2.312 +lemma one_app_congR: 
   2.313 +  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   2.314 +  shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
   2.315 +using a
   2.316 +proof induct
   2.317 +  case bs1 thus ?case by simp
   2.318 +next 
   2.319 +  case bs2 thus ?case by (blast dest: b2)
   2.320 +qed
   2.321 +
   2.322 +lemma one_app_cong: 
   2.323 +  assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   2.324 +  and     a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" 
   2.325 +  shows "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
   2.326 +proof -
   2.327 +  have "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL)
   2.328 +  moreover
   2.329 +  have "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR)
   2.330 +  ultimately show ?thesis by (rule beta_star_trans)
   2.331 +qed
   2.332 +
   2.333 +lemma one_beta_star: 
   2.334 +  assumes a: "(t1\<longrightarrow>\<^isub>1t2)" 
   2.335 +  shows "(t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)"
   2.336 +  using a
   2.337 +proof(nominal_induct rule: One.strong_induct)
   2.338 +  case (o4 a s1 s2 t1 t2)
   2.339 +  have vc: "a\<sharp>s1" "a\<sharp>s2" by fact
   2.340 +  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact
   2.341 +  have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" using vc by (simp add: b4)
   2.342 +  from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" 
   2.343 +    by (blast intro!: one_app_cong one_lam_cong)
   2.344 +  show ?case using c2 c1 by (blast intro: beta_star_trans)
   2.345 +qed (auto intro!: one_app_cong one_lam_cong)
   2.346 +
   2.347 +lemma one_star_lam_cong: 
   2.348 +  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
   2.349 +  shows "(Lam  [a].t1)\<longrightarrow>\<^isub>1\<^sup>* (Lam [a].t2)"
   2.350 +  using a
   2.351 +by (induct) (auto intro: one_star_trans)
   2.352 +
   2.353 +lemma one_star_app_congL: 
   2.354 +  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
   2.355 +  shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
   2.356 +  using a
   2.357 +by (induct) (auto intro: one_star_trans)
   2.358 +
   2.359 +lemma one_star_app_congR: 
   2.360 +  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
   2.361 +  shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
   2.362 +  using a
   2.363 +by (induct) (auto intro: one_star_trans)
   2.364 +
   2.365 +lemma beta_one_star: 
   2.366 +  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2" 
   2.367 +  shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
   2.368 +  using a
   2.369 +by (induct)
   2.370 +   (auto intro!: one_star_app_congL one_star_app_congR one_star_lam_cong)
   2.371 +
   2.372 +lemma rectangle_for_one:
   2.373 +  assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t1" 
   2.374 +  and     b: "t\<longrightarrow>\<^isub>1t2"
   2.375 +  shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3"
   2.376 +  using a b
   2.377 +proof (induct arbitrary: t2)
   2.378 +  case os1 thus ?case by force
   2.379 +next
   2.380 +  case (os2 t s1 s2 t2)  
   2.381 +  have b: "s1 \<longrightarrow>\<^isub>1 s2" by fact
   2.382 +  have h: "\<And>t2. t \<longrightarrow>\<^isub>1 t2 \<Longrightarrow> (\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" by fact
   2.383 +  have c: "t \<longrightarrow>\<^isub>1 t2" by fact
   2.384 +  show "\<exists>t3. s2 \<longrightarrow>\<^isub>1 t3 \<and>  t2 \<longrightarrow>\<^isub>1\<^sup>* t3" 
   2.385 +  proof -
   2.386 +    from c h have "\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
   2.387 +    then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3" and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
   2.388 +    have "\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4" using b c1 by (blast intro: diamond)
   2.389 +    thus ?thesis using c2 by (blast intro: one_star_trans)
   2.390 +  qed
   2.391 +qed
   2.392 +
   2.393 +lemma cr_for_one_star: 
   2.394 +  assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t2"
   2.395 +      and b: "t\<longrightarrow>\<^isub>1\<^sup>*t1"
   2.396 +    shows "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3"
   2.397 +using a b
   2.398 +proof (induct arbitrary: t1)
   2.399 +  case (os1 t) then show ?case by force
   2.400 +next 
   2.401 +  case (os2 t s1 s2 t1)
   2.402 +  have c: "t \<longrightarrow>\<^isub>1\<^sup>* s1" by fact
   2.403 +  have c': "t \<longrightarrow>\<^isub>1\<^sup>* t1" by fact
   2.404 +  have d: "s1 \<longrightarrow>\<^isub>1 s2" by fact
   2.405 +  have "t \<longrightarrow>\<^isub>1\<^sup>* t1 \<Longrightarrow> (\<exists>t3.  t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> s1 \<longrightarrow>\<^isub>1\<^sup>* t3)" by fact
   2.406 +  then obtain t3 where f1: "t1 \<longrightarrow>\<^isub>1\<^sup>* t3"
   2.407 +                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" using c' by blast
   2.408 +  from rectangle_for_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast
   2.409 +  then obtain t4 where g1: "t3\<longrightarrow>\<^isub>1t4"
   2.410 +                   and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast
   2.411 +  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (blast intro: one_star_trans)
   2.412 +  thus ?case using g2 by blast
   2.413 +qed
   2.414 +
   2.415 +lemma beta_star_and_one_star: 
   2.416 +  shows "(M1\<longrightarrow>\<^isub>1\<^sup>*M2) = (M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2)"
   2.417 +proof
   2.418 +  assume "M1 \<longrightarrow>\<^isub>1\<^sup>* M2"
   2.419 +  then show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2"
   2.420 +  proof induct
   2.421 +    case (os1 M1) thus "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M1" by simp
   2.422 +  next
   2.423 +    case (os2 M1 M2 M3)
   2.424 +    have "M2\<longrightarrow>\<^isub>1M3" by fact
   2.425 +    then have "M2\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (rule one_beta_star)
   2.426 +    moreover have "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" by fact
   2.427 +    ultimately show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (auto intro: beta_star_trans)
   2.428 +  qed
   2.429 +next
   2.430 +  assume "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2" 
   2.431 +  then show "M1\<longrightarrow>\<^isub>1\<^sup>*M2"
   2.432 +  proof induct
   2.433 +    case (bs1 M1) thus  "M1\<longrightarrow>\<^isub>1\<^sup>*M1" by simp
   2.434 +  next
   2.435 +    case (bs2 M1 M2 M3) 
   2.436 +    have "M2\<longrightarrow>\<^isub>\<beta>M3" by fact
   2.437 +    then have "M2\<longrightarrow>\<^isub>1\<^sup>*M3" by (rule beta_one_star)
   2.438 +    moreover have "M1\<longrightarrow>\<^isub>1\<^sup>*M2" by fact
   2.439 +    ultimately show "M1\<longrightarrow>\<^isub>1\<^sup>*M3" by (auto intro: one_star_trans)
   2.440 +  qed
   2.441 +qed
   2.442 +
   2.443 +lemma cr_for_beta_star: 
   2.444 +  assumes a1: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t1" 
   2.445 +  and     a2: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
   2.446 +  shows "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3"
   2.447 +proof -
   2.448 +  from a1 have "t\<longrightarrow>\<^isub>1\<^sup>*t1" by (simp only: beta_star_and_one_star)
   2.449 +  moreover
   2.450 +  from a2 have "t\<longrightarrow>\<^isub>1\<^sup>*t2" by (simp only: beta_star_and_one_star)
   2.451 +  ultimately have "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3" by (blast intro: cr_for_one_star) 
   2.452 +  then obtain t3 where "t1\<longrightarrow>\<^isub>1\<^sup>*t3" and "t2\<longrightarrow>\<^isub>1\<^sup>*t3" by (blast intro: cr_for_one_star)
   2.453 +  hence "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" and "t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp_all only: beta_star_and_one_star)
   2.454 +  then show "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by blast
   2.455 +qed
   2.456 +
   2.457 +end