--- a/Attic/Quot/Examples/FSet3.thy	Thu Apr 15 15:56:21 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy	Thu Apr 15 15:56:38 2010 +0200
@@ -72,9 +72,13 @@
   shows "[] \<approx> []"
 by simp
 
-lemma cons_rsp[quot_respect]: 
+lemma cons_rsp:
+  "xa \<approx> ya \<Longrightarrow> y # xa \<approx> y # ya"
+  by simp
+
+lemma [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
-by simp
+  by simp
 
 
 section {* Augmenting a set -- @{const finsert} *}
@@ -257,11 +261,11 @@
 
 lemma concat2:
   shows "concat (x # xs) \<approx> x @ concat xs"
-by (simp add: id_simps)
+by (simp)
 
 lemma concat_rsp[quot_respect]:
   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-sorry
+  sorry
 
 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
   apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
@@ -344,25 +348,31 @@
   apply (metis equivp_def fset_equivp)
   apply rule
   apply rule
-  apply(rule quotient_compose_list_pre)
+  apply (rule quotient_compose_list_pre)
   done
 
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
-apply(lifting concat1)
-apply(cleaning)
-apply(simp add: comp_def)
-apply(fold fempty_def[simplified id_simps])
-apply(rule refl)
-done
+  apply(lifting concat1)
+  apply(cleaning)
+  apply(simp add: comp_def)
+  apply(fold fempty_def[simplified id_simps])
+  apply(rule refl)
+  done
 
 (* Should be true *)
 
 lemma insert_rsp2[quot_respect]:
   "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
-apply auto
-apply (simp add: set_in_eq)
-sorry
+  apply auto
+  apply (simp add: set_in_eq)
+  apply (rule_tac b="x # b" in pred_compI)
+  apply auto
+  apply (rule_tac b="x # ba" in pred_compI)
+  apply (rule cons_rsp)
+  apply simp
+  apply (auto)[1]
+  done
 
 lemma append_rsp[quot_respect]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
@@ -370,11 +380,11 @@
 
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
-apply(lifting concat2)
-apply(cleaning)
-apply (simp add: finsert_def fconcat_def comp_def)
-apply cleaning
-done
+  apply(lifting concat2)
+  apply(cleaning)
+  apply (simp add: finsert_def fconcat_def comp_def)
+  apply cleaning
+  done
 
 text {* raw section *}
 

--- a/Nominal/Manual/Term4.thy	Thu Apr 15 15:56:21 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Thu Apr 15 15:56:38 2010 +0200
@@ -1,5 +1,5 @@
 theory Term4
-imports "../Abs" "../Perm" "../Fv" "../Rsp" "Quotient_List"
+imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List"
 begin
 
 atom_decl name
@@ -29,8 +29,8 @@
 thm permute_rtrm4_permute_rtrm4_list.simps
 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
-  [[[], [], [(NONE, 0,1)]], [[], []]  ] *}
+local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
+  [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *}
 print_theorems
 
 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"
@@ -54,34 +54,29 @@
   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_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)) *}
+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)) *}
 thm alpha4_inj
 
-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)) *}
+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
 
-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}
-*}
-print_theorems
+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}] [@{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))
+  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))
 *}
 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]
+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)) *}
+thm alpha4_reflp
+ML build_equivps
 
-(*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*)
-
+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]
 
 quotient_type 
   trm4 = rtrm4 / alpha_rtrm4
@@ -91,31 +86,84 @@
 
 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})))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4}))
+ |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4}))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4}))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4})))
 *}
 print_theorems
 
-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) *}
+
+
+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
+
+local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}]
+  (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *}
+print_theorems
+
+ML constr_rsp_tac
+
+local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}]
+  (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
+local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}]
+  (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
+
+lemma [quot_respect]:
+  "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
+  by (simp add: alpha4_inj)
+
+(* 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
 
-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)
+lemma list_rel_rsp:
+  "\<lbrakk>\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> S x a = T y b); list_rel R x y; list_rel R a b\<rbrakk>
+    \<Longrightarrow> list_rel S x a = list_rel T y b"
+  sorry
+
+lemma[quot_respect]:
+  "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel"
+  by (simp add: list_rel_rsp)
 
+lemma[quot_preserve]:
+  assumes a: "Quotient R abs1 rep1"
+  shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel"
+  apply (simp add: expand_fun_eq)
+  apply clarify
+  apply (induct_tac xa xb rule: list_induct2')
+  apply (simp_all add: Quotient_abs_rep[OF a])
+  done
 
-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) *}
+lemma[quot_preserve]:
+  assumes a: "Quotient R abs1 rep1"
+  shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
+  by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
+
+lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) =
+  (trm4 = trm4a \<and> list_rel (op =) list lista)"
+  by (lifting alpha4_inj(2))
+
+thm bla[simplified list_rel_eq]
 
-thm rtrm4.induct
-lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]
+lemma " (Lm4 name rtrm4 = Lm4 namea rtrm4a) =
+ (\<exists>pi\<Colon>perm.
+     fv_trm4 rtrm4 - {atom name} = fv_trm4 rtrm4a - {atom namea} \<and>
+     (fv_trm4 rtrm4 - {atom name}) \<sharp>* pi \<and>
+     pi \<bullet> rtrm4 = rtrm4a \<and> pi \<bullet> {atom name} = {atom namea})"
+
+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} *}
+.
+
+(*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*)
 
 end