author Christian Urban Mon Dec 15 07:41:07 2008 +0000 (2008-12-15) changeset 29103 e2fdd4ce541b parent 29102 2e1011dcd577 child 29104 a5ac0bc68e2b
tuned some proofs
```     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
```