# HG changeset patch
# User urbanc
# Date 1177692627 -7200
# Node ID fa9ff469247feb2408f3bbb83d144b1e14f70211
# Parent  c1a6a2159e69123e520c26dc093c9683c2b3dc53
tuned some proofs in CR and properly included CR_Takahashi

diff -r c1a6a2159e69 -r fa9ff469247f src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Fri Apr 27 16:31:20 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Fri Apr 27 18:50:27 2007 +0200
@@ -247,6 +247,16 @@
   qed
 qed
 
+lemma one_fresh_preserv_automatic:
+  fixes a :: "name"
+  assumes a: "t\<longrightarrow>\<^isub>1s"
+  and     b: "a\<sharp>t"
+  shows "a\<sharp>s"
+using a b
+apply(nominal_induct avoiding: a rule: One.strong_induct)
+apply(auto simp add: abs_fresh fresh_atm fresh_fact)
+done
+
 lemma subst_rename: 
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
@@ -263,20 +273,15 @@
   using a
   apply -
   apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
-  apply(auto simp add: lam.distinct lam.inject alpha)
+  apply(auto simp add: lam.inject alpha)
   apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   apply(rule conjI)
-  apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst, symmetric])
-  apply(simp)
-  apply(rule pt_name3)
-  apply(rule at_ds5[OF at_name_inst])
-  apply(frule_tac a="a" in one_fresh_preserv)
-  apply(assumption)
-  apply(rule conjI)
-  apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst])
-  apply(simp add: calc_atm)
-  apply(force intro!: One.eqvt)
-  done
+  apply(perm_simp)
+  apply(simp add: fresh_left calc_atm)
+  apply(simp add: One.eqvt)
+  apply(simp add: one_fresh_preserv)
+done  
+
 
 lemma one_app: 
   assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
diff -r c1a6a2159e69 -r fa9ff469247f src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Fri Apr 27 16:31:20 2007 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Fri Apr 27 18:50:27 2007 +0200
@@ -6,6 +6,7 @@
 *)
 
 use_thy "CR";
+use_thy "CR_Takahashi";
 use_thy "Class";
 use_thy "Compile";
 use_thy "Fsub";