--- a/Nominal/Manual/Term4.thy	Tue Apr 20 15:59:57 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Tue Apr 20 17:25:31 2010 +0200
@@ -1,5 +1,5 @@
 theory Term4
-imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List"
+imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove"
 begin
 
 atom_decl name
@@ -28,7 +28,7 @@
   done
 
 thm permute_rtrm4_permute_rtrm4_list.simps
-lemmas rawperm=permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
 
 local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
@@ -48,42 +48,45 @@
 apply simp_all
 done
 
-(* We need sth like:
-lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *)
+ML {* @{term "\<Union>a"} *}
+
+lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
+apply (rule ext)
+apply (induct_tac x)
+apply simp_all
+done
 
 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[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
+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
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (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_no
+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_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
 thm eqvts(1-2)
 
 local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
-  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_no} ctxt 1) ctxt) ctxt))
+(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))
 *}
-lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
+thm alpha4_eqvt
+lemmas alpha4_eqvt_fixed = alpha4_eqvt[simplified fix2 fix3]
 
 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_no} ctxt) ctxt)) *}
+  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
-ML build_equivps
+lemmas alpha4_reflp_fixed = alpha4_reflp[simplified fix2 fix3]
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
-  (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_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
-lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
+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]
 
 quotient_type 
   trm4 = rtrm4 / alpha_rtrm4
-(*and
-  trm4list = "rtrm4 list" / alpha_rtrm4_list*)
   by (simp_all add: alpha4_equivp)
 
 local_setup {*
@@ -96,7 +99,6 @@
 print_theorems
 
 
-
 lemma fv_rtrm4_rsp:
   "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"
   "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"
@@ -115,31 +117,61 @@
 
 lemma [quot_respect]:
   "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
-  by (simp add: alpha4_inj)
+  by (simp add: alpha4_inj_fixed)
 
-(* Maybe also need: @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"} *)
 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
   [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
-print_theorems
 
-setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_append} *}
+setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_plus} *}
 print_theorems
 
-
+(* Instead of permute for trm4_list we may need the following 2 lemmas: *)
+lemma [quot_preserve]: "(id ---> map rep_trm4 ---> map abs_trm4) permute = permute"
+  apply (simp add: expand_fun_eq)
+  apply clarify
+  apply (rename_tac "pi" x)
+  apply (induct_tac x)
+  apply simp
+  apply simp
+  apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified])
+  done
 
-lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) =
-  (trm4 = trm4a \<and> list_rel (op =) list lista)"
-  by (lifting alpha4_inj(2))
+lemma [quot_respect]: "(op = ===> list_rel alpha_rtrm4 ===> list_rel alpha_rtrm4) permute permute"
+  apply simp
+  apply (rule allI)+
+  apply (induct_tac xa y rule: list_induct2')
+  apply simp_all
+  apply clarify
+  apply (erule alpha4_eqvt)
+  done
 
-thm bla[simplified list_rel_eq]
+ML {*
+  map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed}
+*}
 
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *}
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *}
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *}
 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
-.
+
+ML {*
+  map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4_fv_rtrm4_list.simps[simplified fix3]}
+*}
 
-(*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*)
+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]}
+    )
+  )
+*}
+
+ML {*
+  map (lift_thm [@{typ trm4}] @{context})
+  (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
+*}
+
+ML {*
+  map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fix3]}
+*}
 
 end