tuned some proofs
authorChristian Urban <urbanc@in.tum.de>
Mon Dec 15 07:41:07 2008 +0000 (2008-12-15)
changeset 29103e2fdd4ce541b
parent 29102 2e1011dcd577
child 29104 a5ac0bc68e2b
tuned some proofs
src/HOL/Nominal/Examples/CR_Takahashi.thy
     1.1 --- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Sat Dec 13 17:46:13 2008 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Mon Dec 15 07:41:07 2008 +0000
     1.3 @@ -52,14 +52,16 @@
     1.4  lemma substitution_lemma:  
     1.5    assumes a: "x\<noteq>y" "x\<sharp>u"
     1.6    shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
     1.7 -using a by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
     1.8 -           (auto simp add: fresh_fact forget)
     1.9 +using a 
    1.10 +by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
    1.11 +   (auto simp add: fresh_fact forget)
    1.12  
    1.13  lemma subst_rename: 
    1.14    assumes a: "y\<sharp>t"
    1.15    shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]"
    1.16 -using a by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
    1.17 -           (auto simp add: calc_atm fresh_atm abs_fresh)
    1.18 +using a 
    1.19 +by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
    1.20 +   (auto simp add: swap_simps fresh_atm abs_fresh)
    1.21  
    1.22  section {* Beta-Reduction *}
    1.23  
    1.24 @@ -101,8 +103,9 @@
    1.25  lemma One_subst: 
    1.26    assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
    1.27    shows "t1[x::=s1] \<longrightarrow>\<^isub>1 t2[x::=s2]" 
    1.28 -using a by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
    1.29 -           (auto simp add: substitution_lemma fresh_atm fresh_fact)
    1.30 +using a 
    1.31 +by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
    1.32 +   (auto simp add: substitution_lemma fresh_atm fresh_fact)
    1.33  
    1.34  lemma better_o4_intro:
    1.35    assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
    1.36 @@ -200,35 +203,30 @@
    1.37  by (nominal_induct M rule: lam.strong_induct)
    1.38     (auto dest!: Dev_Lam intro: better_d4_intro)
    1.39  
    1.40 -(* needs fixing *)
    1.41  lemma Triangle:
    1.42    assumes a: "t \<longrightarrow>\<^isub>d t1" "t \<longrightarrow>\<^isub>1 t2"
    1.43    shows "t2 \<longrightarrow>\<^isub>1 t1"
    1.44  using a 
    1.45  proof(nominal_induct avoiding: t2 rule: Dev.strong_induct)
    1.46    case (d4 x s1 s2 t1 t1' t2) 
    1.47 -  have ih1: "\<And>t. t1 \<longrightarrow>\<^isub>1 t \<Longrightarrow>  t \<longrightarrow>\<^isub>1 t1'"
    1.48 -  and  ih2: "\<And>s. s1 \<longrightarrow>\<^isub>1 s \<Longrightarrow>  s \<longrightarrow>\<^isub>1 s2"
    1.49 -  and  fc: "x\<sharp>t2" "x\<sharp>s1" "x\<sharp>s2" by fact+ 
    1.50 +  have  fc: "x\<sharp>t2" "x\<sharp>s1" by fact+ 
    1.51    have "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2" by fact
    1.52 -  then obtain t' s' where "(t2 = App (Lam [x].t') s' \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s') \<or> 
    1.53 -                           (t2 = t'[x::=s'] \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s')"
    1.54 +  then obtain t' s' where reds: 
    1.55 +             "(t2 = App (Lam [x].t') s' \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s') \<or> 
    1.56 +              (t2 = t'[x::=s'] \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s')"
    1.57    using fc by (auto dest!: One_Redex)
    1.58 -  then show "t2 \<longrightarrow>\<^isub>1 t1'[x::=s2]"
    1.59 -    apply -
    1.60 -    apply(erule disjE)
    1.61 -    apply(erule conjE)+
    1.62 -    apply(simp)
    1.63 -    apply(rule o4)
    1.64 -    using fc apply(simp)
    1.65 -    using ih1 apply(simp)
    1.66 -    using ih2 apply(simp)
    1.67 -    apply(erule conjE)+
    1.68 -    apply(simp)
    1.69 -    apply(rule One_subst)
    1.70 -    using ih1 apply(simp)
    1.71 -    using ih2 apply(simp)    
    1.72 -    done
    1.73 +  have ih1: "t1 \<longrightarrow>\<^isub>1 t' \<Longrightarrow>  t' \<longrightarrow>\<^isub>1 t1'" by fact
    1.74 +  have ih2: "s1 \<longrightarrow>\<^isub>1 s' \<Longrightarrow>  s' \<longrightarrow>\<^isub>1 s2" by fact
    1.75 +  { assume "t1 \<longrightarrow>\<^isub>1 t'" "s1 \<longrightarrow>\<^isub>1 s'"
    1.76 +    then have "App (Lam [x].t') s' \<longrightarrow>\<^isub>1 t1'[x::=s2]" 
    1.77 +      using ih1 ih2 by (auto intro: better_o4_intro)
    1.78 +  }
    1.79 +  moreover
    1.80 +  { assume "t1 \<longrightarrow>\<^isub>1 t'" "s1 \<longrightarrow>\<^isub>1 s'"
    1.81 +    then have "t'[x::=s'] \<longrightarrow>\<^isub>1 t1'[x::=s2]" 
    1.82 +      using ih1 ih2 by (auto intro: One_subst)
    1.83 +  }
    1.84 +  ultimately show "t2 \<longrightarrow>\<^isub>1 t1'[x::=s2]" using reds by auto 
    1.85  qed (auto dest!: One_Lam One_Var One_App)
    1.86  
    1.87  lemma Diamond_for_One:
    1.88 @@ -308,4 +306,6 @@
    1.89    then show "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" by (simp add: Beta_star_equals_One_star)
    1.90  qed
    1.91  
    1.92 +
    1.93 +
    1.94  end