# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265103828 -3600
# Node ID cc5830c452c47d365d18a8670ad05f763f607167
# Parent  bacf3584640ee1c4760127b72f150a1314399d92
With induct instead of induct_tac, just one induction is sufficient.

diff -r bacf3584640e -r cc5830c452c4 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Tue Feb 02 10:20:54 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Tue Feb 02 10:43:48 2010 +0100
@@ -51,21 +51,25 @@
 | "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)"
 | "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \<bullet> x) (permute_trm pi M)"
 
-lemma rperm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z"
-apply(induct_tac rule: kind_ty_trm.induct)
+lemma rperm_zero_ok:
+  "0 \<bullet> (x :: kind) = x"
+  "0 \<bullet> (y :: ty) = y"
+  "0 \<bullet> (z :: trm) = z"
+apply(induct x and y and z rule: kind_ty_trm.inducts)
 apply(simp_all)
 done
+
+lemma rperm_plus_ok:
+ "(p + q) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x"
+ "(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y"
+ "(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> z"
+apply(induct x and y and z rule: kind_ty_trm.inducts)
+apply(simp_all)
+done
+
 instance
 apply default
-apply (simp_all only:rperm_zero_ok)
-apply(induct_tac[!] x)
-apply(simp_all)
-apply(induct_tac ty)
-apply(simp_all)
-apply(induct_tac trm)
-apply(simp_all)
-apply(induct_tac trm)
-apply(simp_all)
+apply (simp_all only:rperm_zero_ok rperm_plus_ok)
 done
 
 end