tuned proofs
authorurbanc
Wed Jan 11 17:07:57 2006 +0100 (2006-01-11)
changeset 1865494782c7c4247
parent 18653 7a00c80400b1
child 18655 73cebafb9a89
tuned proofs
src/HOL/Nominal/Examples/SN.thy
src/HOL/Nominal/Examples/Weakening.thy
     1.1 --- a/src/HOL/Nominal/Examples/SN.thy	Wed Jan 11 14:00:11 2006 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Wed Jan 11 17:07:57 2006 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4    shows   "valid (pi\<bullet>\<Gamma>)"
     1.5  using a
     1.6  apply(induct)
     1.7 -apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
     1.8 +apply(auto simp add: fresh_eqvt)
     1.9  done
    1.10  
    1.11  (* typing judgements *)
    1.12 @@ -278,10 +278,10 @@
    1.13    moreover
    1.14    have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
    1.15    ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
    1.16 -    using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
    1.17 +    using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
    1.18  next 
    1.19    case (t3 \<Gamma> \<sigma> \<tau> a t)
    1.20 -  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
    1.21 +  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
    1.22    ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
    1.23  qed (auto)
    1.24  
     2.1 --- a/src/HOL/Nominal/Examples/Weakening.thy	Wed Jan 11 14:00:11 2006 +0100
     2.2 +++ b/src/HOL/Nominal/Examples/Weakening.thy	Wed Jan 11 17:07:57 2006 +0100
     2.3 @@ -76,7 +76,7 @@
     2.4      using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
     2.5  next 
     2.6    case (t3 \<Gamma> \<sigma> \<tau> a t)
     2.7 -  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
     2.8 +  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
     2.9    ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
    2.10  qed (auto)
    2.11