--- a/Nominal/Manual/Term4.thy	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Wed May 05 09:23:10 2010 +0200
@@ -18,76 +18,65 @@
   val {descr, sorts, ...} = dtinfo;
 *}
 setup {* snd o (define_raw_perms descr sorts @{thm rtrm4.induct} 1) *}
-print_theorems
-
-(* "repairing" of the permute function *)
-lemma repaired:
+lemmas perm = permute_rtrm4_permute_rtrm4_list.simps(1-3)
+lemma perm_fix:
   fixes ts::"rtrm4 list"
   shows "permute_rtrm4_list p ts = p \<bullet> ts"
-  apply(induct ts)
-  apply(simp_all)
-  done
-
-thm permute_rtrm4_permute_rtrm4_list.simps
-lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+  by (induct ts) simp_all
+lemmas perm_fixed = perm[simplified perm_fix]
 
 ML {* val bl = [[[BEmy 0], [BEmy 0, BEmy 1], [BSet ([(NONE, 0)], [1])]], [[], [BEmy 0, BEmy 1]]] *}
 
 local_setup {* fn ctxt => let val (_, _, ctxt') = define_raw_fv descr sorts [] bl ctxt in ctxt' end *}
-thm fv_rtrm4.simps fv_rtrm4_list.simps
+lemmas fv = fv_rtrm4.simps (*fv_rtrm4_list.simps*)
+
+lemma fv_fix: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
+  by (rule ext) (induct_tac x, simp_all)
+lemmas fv_fixed = fv[simplified fv_fix]
+
+(* TODO: check remove 2 *)
+local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms perm_fixed fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
+thm eqvts(1-2)
 
 local_setup {* snd o define_raw_alpha dtinfo [] bl [@{term fv_rtrm4}, @{term fv_rtrm4_list}] *}
-thm alpha_rtrm4_alpha_rtrm4_list.intros
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
+lemmas alpha_inj = alpha4_inj(1-3)
 
-lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"
-apply (rule ext)+
-apply (induct_tac x xa rule: list_induct2')
-apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)
-apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
-apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
-apply rule
-apply (erule alpha_rtrm4_list.cases)
-apply simp_all
-apply (rule alpha_rtrm4_alpha_rtrm4_list.intros)
-apply simp_all
-done
+lemma alpha_fix: "alpha_rtrm4_list = list_rel alpha_rtrm4"
+  apply (rule ext)+
+  apply (induct_tac x xa rule: list_induct2')
+  apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)
+  apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
+  apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
+  apply rule
+  apply (erule alpha_rtrm4_list.cases)
+  apply simp_all
+  apply (rule alpha_rtrm4_alpha_rtrm4_list.intros)
+  apply simp_all
+  done
 
-lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
-apply (rule ext)
-apply (induct_tac x)
-apply simp_all
-done
+lemmas alpha_inj_fixed = alpha_inj[simplified alpha_fix (*fv_fix*)]
 
 notation
-  alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
-  alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
-thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
-thm alpha4_inj
-
-lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3]
-
-local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4.simps fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
-thm eqvts(1-2)
+    alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100)
+and alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 
 local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
-  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt))
+  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms perm_fixed alpha4_inj} ctxt 1) ctxt) ctxt))
 *}
 thm alpha4_eqvt
-lemmas alpha4_eqvt_fixed = alpha4_eqvt[simplified fix2 fix3]
+lemmas alpha4_eqvt_fixed = alpha4_eqvt(1)[simplified alpha_fix (*fv_fix*)]
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
   build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}
 thm alpha4_reflp
-lemmas alpha4_reflp_fixed = alpha4_reflp[simplified fix2 fix3]
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
   (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
-lemmas alpha4_equivp_fixed = alpha4_equivp[simplified fix2 fix3]
+lemmas alpha4_equivp_fixed = alpha4_equivp[simplified alpha_fix fv_fix]
 
-quotient_type 
+quotient_type
   trm4 = rtrm4 / alpha_rtrm4
   by (simp_all add: alpha4_equivp)
 
@@ -119,7 +108,7 @@
 
 lemma [quot_respect]:
   "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
-  by (simp add: alpha4_inj_fixed)
+  by (simp add: alpha_inj_fixed)
 
 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
   [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
@@ -155,14 +144,14 @@
 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
 
 ML {*
-  map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fix3] fv_rtrm4_list.simps[simplified fix3]}
+  map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4.simps[simplified fv_fix] fv_rtrm4_list.simps[simplified fv_fix]}
 *}
 
 ML {*
 val liftd =
   map (Local_Defs.unfold @{context} @{thms id_simps}) (
     map (Local_Defs.fold @{context} @{thms alphas}) (
-      map (lift_thm [@{typ trm4}] @{context}) @{thms alpha4_inj_fixed[unfolded alphas]}
+      map (lift_thm [@{typ trm4}] @{context}) @{thms alpha_inj_fixed[unfolded alphas]}
     )
   )
 *}
@@ -173,7 +162,7 @@
 *}
 
 ML {*
-  map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fix3]}
+  map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fv_fix]}
 *}
 
 end