tuned some proofs in CR and properly included CR_Takahashi
authorurbanc
Fri Apr 27 18:50:27 2007 +0200 (2007-04-27)
changeset 22823fa9ff469247f
parent 22822 c1a6a2159e69
child 22824 51bb2f6ecc4a
tuned some proofs in CR and properly included CR_Takahashi
src/HOL/Nominal/Examples/CR.thy
src/HOL/Nominal/Examples/ROOT.ML
     1.1 --- a/src/HOL/Nominal/Examples/CR.thy	Fri Apr 27 16:31:20 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/CR.thy	Fri Apr 27 18:50:27 2007 +0200
     1.3 @@ -247,6 +247,16 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma one_fresh_preserv_automatic:
     1.8 +  fixes a :: "name"
     1.9 +  assumes a: "t\<longrightarrow>\<^isub>1s"
    1.10 +  and     b: "a\<sharp>t"
    1.11 +  shows "a\<sharp>s"
    1.12 +using a b
    1.13 +apply(nominal_induct avoiding: a rule: One.strong_induct)
    1.14 +apply(auto simp add: abs_fresh fresh_atm fresh_fact)
    1.15 +done
    1.16 +
    1.17  lemma subst_rename: 
    1.18    assumes a: "c\<sharp>t1"
    1.19    shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
    1.20 @@ -263,20 +273,15 @@
    1.21    using a
    1.22    apply -
    1.23    apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
    1.24 -  apply(auto simp add: lam.distinct lam.inject alpha)
    1.25 +  apply(auto simp add: lam.inject alpha)
    1.26    apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
    1.27    apply(rule conjI)
    1.28 -  apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst, symmetric])
    1.29 -  apply(simp)
    1.30 -  apply(rule pt_name3)
    1.31 -  apply(rule at_ds5[OF at_name_inst])
    1.32 -  apply(frule_tac a="a" in one_fresh_preserv)
    1.33 -  apply(assumption)
    1.34 -  apply(rule conjI)
    1.35 -  apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst])
    1.36 -  apply(simp add: calc_atm)
    1.37 -  apply(force intro!: One.eqvt)
    1.38 -  done
    1.39 +  apply(perm_simp)
    1.40 +  apply(simp add: fresh_left calc_atm)
    1.41 +  apply(simp add: One.eqvt)
    1.42 +  apply(simp add: one_fresh_preserv)
    1.43 +done  
    1.44 +
    1.45  
    1.46  lemma one_app: 
    1.47    assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
     2.1 --- a/src/HOL/Nominal/Examples/ROOT.ML	Fri Apr 27 16:31:20 2007 +0200
     2.2 +++ b/src/HOL/Nominal/Examples/ROOT.ML	Fri Apr 27 18:50:27 2007 +0200
     2.3 @@ -6,6 +6,7 @@
     2.4  *)
     2.5  
     2.6  use_thy "CR";
     2.7 +use_thy "CR_Takahashi";
     2.8  use_thy "Class";
     2.9  use_thy "Compile";
    2.10  use_thy "Fsub";