# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266598243 -3600
# Node ID a94c04c4a7203f952418836ca231c5136e7849c2
# Parent  5770c73f24153ae736cc790d937f1b44273b0d7e
proof cleaning and standardizing.

diff -r 5770c73f2415 -r a94c04c4a720 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Fri Feb 19 16:45:24 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Fri Feb 19 17:50:43 2010 +0100
@@ -134,7 +134,7 @@
 lemma alpha_rfv1:
   shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
   apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))
-  apply(simp_all add: alpha_gen.simps)
+  apply(simp_all add: fv_rtrm1_fv_bp.simps alpha_gen.simps)
   done
 
 lemma [quot_respect]:
@@ -143,12 +143,8 @@
  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"
  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"
 apply (auto simp add: alpha1_inj)
-apply (rule_tac x="0" in exI)
-apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
-apply (rule_tac x="0" in exI)
-apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq)
-apply (rule_tac x="0" in exI)
-apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1)
+apply (rule_tac [!] x="0" in exI)
+apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq)
 done
 
 lemma [quot_respect]:
@@ -541,7 +537,6 @@
   "(op = ===> alpha_rtrm5) rVr5 rVr5"
   "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"
   "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
-  "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"
   "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"
   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"
   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"
@@ -549,9 +544,6 @@
   apply (clarify) apply (rule conjI)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
-  apply (clarify) apply (rule conjI)
-  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
-  apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   done
 
 lemma
@@ -631,14 +623,8 @@
 lemma lets_not_ok1:
   "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
              (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ(3))
-apply(clarify)
-apply (simp add: alpha_gen)
-apply (simp add: permute_trm5_lts fresh_star_def)
-apply (simp add: alpha5_INJ(5))
-apply(clarify)
-apply (simp add: alpha5_INJ(2))
-apply (simp add: alpha5_INJ(1))
+apply (simp add: alpha5_INJ(3) alpha_gen)
+apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1))
 done
 
 lemma distinct_helper:
@@ -656,10 +642,7 @@
   "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
    (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>
    (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"
-apply (subst alpha5_INJ)
-apply (simp only: alpha_gen permute_trm5_lts fresh_star_def)
-apply (subst alpha5_INJ(5))
-apply (subst alpha5_INJ(5))
+apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)
 apply (simp add: distinct_helper2)
 done