# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264769225 -3600
# Node ID 5c0d9a507bcbac163e6afbe466200f398543a807
# Parent  74e9a580448cd57e8a2251e3f8499ea4529d8aad
Fixed the induction problem + some more proofs.

diff -r 74e9a580448c -r 5c0d9a507bcb Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Fri Jan 29 12:16:08 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Fri Jan 29 13:47:05 2010 +0100
@@ -150,26 +150,14 @@
 done
 
 (* TODO: ask Stefan why 'induct' goes wrong, commented out commands should work *)
-lemma rfv_eqvt_tmp:
-  "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1)) \<and>
-  ((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2)) \<and>
-  ((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
-thm kind_ty_trm.induct
-(*apply(induct t1 t2 t3 rule: kind_ty_trm.inducts)*)
-apply(rule kind_ty_trm.induct[of
-  "\<lambda>t1. ((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
-  "\<lambda>t2. ((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
-  "\<lambda>t3. ((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"])
-apply(simp_all add:  union_eqvt Diff_eqvt)
-apply(simp_all add: permute_set_eq atom_eqvt)
-done
 
 lemma rfv_eqvt[eqvt]:
   "((pi\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
   "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
   "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
-(*apply(induct t1 t2 t3 rule: kind_ty_trm.inducts)*)
-apply(simp_all only: rfv_eqvt_tmp)
+apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts)
+apply(simp_all add:  union_eqvt Diff_eqvt)
+apply(simp_all add: permute_set_eq atom_eqvt)
 done
 
 lemma alpha_eqvt:
@@ -350,13 +338,26 @@
 
 lemma kpi_rsp[quot_respect]: 
   "(aty ===> op = ===> akind ===> akind) KPi KPi"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
+  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
+  apply (rule a2) apply simp
+  apply (rule_tac x="0" in exI)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  done
+
 lemma tpi_rsp[quot_respect]: 
   "(aty ===> op = ===> aty ===> aty) TPi TPi"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
+  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
+  apply (rule a5) apply simp
+  apply (rule_tac x="0" in exI)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  done
 lemma lam_rsp[quot_respect]: 
   "(aty ===> op = ===> atrm ===> atrm) Lam Lam"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) sorry
+  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
+  apply (rule a9) apply simp
+  apply (rule_tac x="0" in exI)
+  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv)
+  done
 
 lemma rfv_ty_rsp[quot_respect]: 
   "(aty ===> op =) rfv_ty rfv_ty"
@@ -415,9 +416,11 @@
 done
 
 lemma perm_add_ok: "((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> (x1 :: KIND))) \<and> ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2) \<and> ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"
-apply(induct_tac [!] rule: KIND_TY_TRM_induct)
+apply(rule KIND_TY_TRM_induct[of 
+"\<lambda>x1. ((p1 + q1) \<bullet> (x1 :: KIND) = (p1 \<bullet> q1 \<bullet> x1))"
+"\<lambda>x2. ((p2 + q2) \<bullet> (x2 :: TY) = p2 \<bullet> q2 \<bullet> x2)"
+"\<lambda>x3. ((p3 + q3) \<bullet> (x3 :: TRM) = p3 \<bullet> q3 \<bullet> x3)"])
 apply (simp_all)
-(* Sth went wrong... *)
 sorry
 
 instance