diff -r 75af61f32ece -r f1c0a66284d3 FSet.thy
--- a/FSet.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/FSet.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -328,7 +328,7 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 lemma "FOLD f g (z::'b) (INSERT a x) =
   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
@@ -350,52 +350,52 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 apply(rule cheat)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+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 = (===>) *) 
+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 = (===>) *) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+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*}) (* E *) (* R x y assumptions *)
+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*}) (* D *) (* reflexivity of basic relations *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
+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 = (===>) *) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+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*}) (* E *) (* R x y assumptions *)
+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*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+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*}) (* E *) (* R x y assumptions *)
+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*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+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*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+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*}) (* E *) (* R x y assumptions *)
+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*}) (* E *) (* R x y assumptions *)
 done
 
 
@@ -444,8 +444,8 @@
   apply (assumption)
   done
 
-ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-ML {* fun r_mk_comb_tac_fset' lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 (* Construction site starts here *)
 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"
@@ -460,65 +460,65 @@
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule FUN_QUOTIENT)
 apply (rule QUOTIENT_fset)
 apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply assumption
 apply (rule refl)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 done