# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259911118 -3600
# Node ID fac6069d8e80215ebc2d4eab0c63a1eb9d605af4
# Parent  91c374abde06ff9c9afdef7946a630190fec8172
Made your version work again with LIST_REL_EQ.

diff -r 91c374abde06 -r fac6069d8e80 FSet.thy
--- a/FSet.thy	Thu Dec 03 15:03:31 2009 +0100
+++ b/FSet.thy	Fri Dec 04 08:18:38 2009 +0100
@@ -135,9 +135,6 @@
        if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
      ) else z)"
 
-(* fold1_def is not usable, but: *)
-thm fold1.simps
-
 lemma fs1_strong_cases:
   fixes X :: "'a list"
   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
@@ -434,8 +431,8 @@
   "INSERT2 \<equiv> op #"
 
 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
@@ -469,7 +466,7 @@
   sorry
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
 
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
diff -r 91c374abde06 -r fac6069d8e80 LamEx.thy
--- a/LamEx.thy	Thu Dec 03 15:03:31 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 08:18:38 2009 +0100
@@ -128,7 +128,7 @@
 unfolding fresh_def supp_def
 sorry
 
-lemma perm_rsp[quot_rsp]:
+lemma perm_rsp[quotient_rsp]:
   "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
@@ -140,14 +140,14 @@
   (* this is probably only true if some type conditions are imposed *)
   sorry
 
-lemma rVar_rsp[quot_rsp]:
+lemma rVar_rsp[quotient_rsp]:
   "(op = ===> alpha) rVar rVar"
 by (auto intro:a1)
 
-lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
+lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
 by (auto intro:a2)
 
-lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
+lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
   apply(rule a3)
   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -160,7 +160,7 @@
   apply(simp add: abs_fresh)
   done
 
-lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv"
   sorry
 
 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
@@ -174,7 +174,7 @@
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] [quot] *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
diff -r 91c374abde06 -r fac6069d8e80 QuotMain.thy
--- a/QuotMain.thy	Thu Dec 03 15:03:31 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 08:18:38 2009 +0100
@@ -957,7 +957,7 @@
 
     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
     (* global simplification *)
-    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))])
 *}
 
 ML {*