# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267022357 -3600
# Node ID d1ab27c10049c3ae8e34567d47c428c0499955cc
# Parent  ea6a52a4f5bfb21d229fa28aba06a9ad264bdcb8
With permute_rsp we can lift the instance proofs :).

diff -r ea6a52a4f5bf -r d1ab27c10049 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 15:36:07 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 15:39:17 2010 +0100
@@ -135,25 +135,9 @@
 is
   "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
 
-lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
-
-lemma perm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z"
-apply (induct rule: kind_ty_trm_induct)
-apply (simp_all)
-done
-
-lemma perm_add_ok:
-  "((p + q) \<bullet> (x1 :: kind) = (p \<bullet> q \<bullet> x1))"
-  "((p + q) \<bullet> (x2 :: ty) = p \<bullet> q \<bullet> x2)"
-  "((p + q) \<bullet> (x3 :: trm) = p \<bullet> q \<bullet> x3)"
-apply (induct x1 and x2 and x3 rule: kind_ty_trm_inducts)
-apply (simp_all)
-done
-
-instance
-apply default
-apply (simp_all add: perm_zero_ok perm_add_ok)
-done
+instance by default (simp_all add:
+  permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted]
+  permute_rkind_permute_rty_permute_rtrm_append[quot_lifted])
 
 end
 
@@ -162,6 +146,8 @@
 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 *)
 
+lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
+
 lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
diff -r ea6a52a4f5bf -r d1ab27c10049 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 24 15:36:07 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 15:39:17 2010 +0100
@@ -158,18 +158,14 @@
 is
   "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
 
-lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
-
-instance
-apply default
-apply(induct_tac [!] x rule: trm1_bp_inducts(1))
-apply(simp_all)
-done
+instance by default 
+  (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted])
 
 end
 
 lemmas
-    fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
+    permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
+and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
@@ -181,7 +177,7 @@
   "{} supports BUnit"
   "(supp (atom x)) supports (BVr x)"
   "(supp a \<union> supp b) supports (BPr a b)"
-apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh)
+apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1)
 apply(rule_tac [!] allI)+
 apply(rule_tac [!] impI)
 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
@@ -223,14 +219,14 @@
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
 apply(simp add: supp_Abs fv_trm1)
-apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
+apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
 apply(simp add: alpha1_INJ)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen.simps)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
 apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
-apply(simp (no_asm) add: supp_def)
+apply(simp (no_asm) add: supp_def permute_trm1)
 apply(simp add: alpha1_INJ alpha_bp_eq)
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen)
@@ -579,35 +575,16 @@
 is
   "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
 
-lemma trm5_lts_zero:
-  "0 \<bullet> (x\<Colon>trm5) = x"
-  "0 \<bullet> (y\<Colon>lts) = y"
-  apply(induct x and y rule: trm5_lts_inducts)
-  apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
-  done
-
-lemma trm5_lts_plus:
-  "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
-  "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
-  apply(induct x and y rule: trm5_lts_inducts)
-  apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
-  done
-
-instance
-  apply default
-  apply (simp_all add: trm5_lts_zero trm5_lts_plus)
-  done
+instance by default
+  (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])
 
 end
 
-lemmas 
-  permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
-and
-  alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-and
-  bv5[simp] = rbv5.simps[quot_lifted]
-and
-  fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
+lemmas
+    permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
+and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+and bv5[simp] = rbv5.simps[quot_lifted]
+and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"