diff -r eed5d55ea9a6 -r 6b3be083229c FSet.thy
--- a/FSet.thy	Fri Dec 04 09:08:51 2009 +0100
+++ b/FSet.thy	Fri Dec 04 09:25:27 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)))"
@@ -180,7 +177,7 @@
   shows "(z memb x) = (z memb y)"
   using a by induct auto
 
-lemma ho_memb_rsp[quot_rsp]:
+lemma ho_memb_rsp[quotient_rsp]:
   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
   by (simp add: memb_rsp)
 
@@ -190,17 +187,17 @@
   shows "card1 a = card1 b"
   using e by induct (simp_all add:memb_rsp)
 
-lemma ho_card1_rsp[quot_rsp]: 
+lemma ho_card1_rsp[quotient_rsp]: 
   "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
-lemma cons_rsp[quot_rsp]:
+lemma cons_rsp[quotient_rsp]:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule list_eq.intros(5))
 
-lemma ho_cons_rsp[quot_rsp]:
+lemma ho_cons_rsp[quotient_rsp]:
   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
   by (simp add: cons_rsp)
 
@@ -257,7 +254,7 @@
   apply (rule append_sym_rsp)
   done
 
-lemma ho_append_rsp[quot_rsp]:
+lemma ho_append_rsp[quotient_rsp]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (simp add: append_rsp)
 
@@ -269,7 +266,7 @@
   apply(auto intro: list_eq.intros)
   done
 
-lemma ho_map_rsp[quot_rsp]:
+lemma ho_map_rsp[quotient_rsp]:
   "(op = ===> op \<approx> ===> op \<approx>) map map"
   by (simp add: map_rsp)
 
@@ -277,7 +274,7 @@
   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
-lemma ho_fold_rsp[quot_rsp]:
+lemma ho_fold_rsp[quotient_rsp]:
   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
   apply (auto simp add: FUN_REL_EQ)
   apply (case_tac "rsp_fold x")
@@ -297,13 +294,13 @@
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
-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 "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
-apply(tactic {* clean_tac @{context} [quot] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply(tactic {* clean_tac @{context} 1*})
 done
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
@@ -330,7 +327,7 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
@@ -348,7 +345,7 @@
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
@@ -404,6 +401,9 @@
   apply (assumption)
   done
 
+ML {* quot *}
+thm quotient_thm
+
 lemma "P (x :: 'a list) (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 *})
 done
@@ -431,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 *})
@@ -453,20 +453,20 @@
   "fset_case \<equiv> list_case"
 
 (* Probably not true without additional assumptions about the function *)
-lemma list_rec_rsp[quot_rsp]:
+lemma list_rec_rsp[quotient_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
   apply (auto simp add: FUN_REL_EQ)
   apply (erule_tac list_eq.induct)
   apply (simp_all)
   sorry
 
-lemma list_case_rsp[quot_rsp]:
+lemma list_case_rsp[quotient_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
   apply (auto simp add: FUN_REL_EQ)
   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 *})