--- a/Nominal/Term4.thy	Tue Mar 02 17:48:56 2010 +0100
+++ b/Nominal/Term4.thy	Tue Mar 02 19:48:44 2010 +0100
@@ -1,5 +1,5 @@
 theory Term4
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List"
 begin
 
 atom_decl name
@@ -33,14 +33,32 @@
   [[[], [], [(NONE, 0,1)]], [[], []]  ] *}
 print_theorems
 
+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
+
+(* We need sth like:
+lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *)
+
 notation
   alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
   alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
-thm alpha_rtrm4_alpha_rtrm4_list.intros
+thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_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)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_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)) *}
 thm alpha4_inj
-thm alpha_rtrm4_alpha_rtrm4_list.induct
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_alpha_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
 
 local_setup {*
 snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}
@@ -48,18 +66,56 @@
 print_theorems
 
 local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
-  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
+  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
+*}
+lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
+  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{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]
+
+(*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"
+  apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts)
+  apply (simp_all add: alpha_gen)
+done*)
+
+
+quotient_type 
+  trm4 = rtrm4 / alpha_rtrm4
+(*and
+  trm4list = "rtrm4 list" / alpha_rtrm4_list*)
+  by (simp_all add: alpha4_equivp)
+
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4})))
 *}
 print_theorems
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
-  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{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)) *}
-thm alpha4_equivp
+local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}]
+  (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *}
+print_theorems
 
-quotient_type 
-  qrtrm4 = rtrm4 / alpha_rtrm4 and
-  qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
-  by (simp_all add: alpha4_equivp)
+local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}]
+  (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *}
+lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
+apply simp
+apply clarify
+apply (simp add: alpha4_inj)
+
+
+local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}]
+  (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *}
+local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp}
+  [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}, @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] 
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
+
+thm rtrm4.induct
+lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]
 
 end