diff -r b5d293e0b9bb -r 9cb8f9a59402 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 17 15:42:57 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 16:06:54 2009 +0200
@@ -1167,15 +1167,10 @@
 
 ML {* val thm = @{thm list_induct_r} OF [li] *}
 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
-thm APPLY_RSP
 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
-lemmas APPLY_RSP_I2 = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]
-
-thm REP_ABS_RSP(2)
 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
 
 prove trm
-thm UNION_def
 apply (atomize(full))
 apply (simp only: id_def[symmetric])
 
@@ -1186,8 +1181,11 @@
   val m = Thm.match (tc', gc')
   val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" }
  *}
+thm APPLY_RSP_I
 apply (tactic {* rtac t2 1 *})
-prefer 4
+prefer 2
+apply (rule IDENTITY_QUOTIENT)
+prefer 3
 (* ABS_REP_RSP_TAC *)
 ML_prf {*
   val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
@@ -1217,28 +1215,27 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP_TAC *)
-thm APPLY_RSP
 apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
-(* MINE *)
 apply (rule QUOTIENT_fset)
-prefer 3
+apply (rule IDENTITY_QUOTIENT)
+prefer 2
 (* ABS_REP_RSP *)
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
-(* MINE *)
 apply (rule QUOTIENT_fset)
 (* MINE *)
 apply (rule list_eq_refl )
-prefer 2
 (* ABS_REP_RSP *)
 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 prefer 2
 (* MINE *)
 apply (simp only: FUN_REL.simps)
-prefer 3
+prefer 2
 (* APPLY_RSP *)
 apply (rule_tac APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id" "Ball (Respects op \<approx>)" "Ball (Respects op \<approx>)"])
-(* 3: ho_respects *)
-prefer 4
+prefer 2
+apply (rule IDENTITY_QUOTIENT)
+(* 2: ho_respects *)
+prefer 3
 (* ABS_REP_RSP *)
 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 prefer 2
@@ -1255,17 +1252,18 @@
 apply (simp)
 (* APPLY_RSP *)
 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
-prefer 3
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 prefer 2
 (* MINE *)
 apply (simp only: FUN_REL.simps)
-prefer 4
+prefer 2
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
-prefer 2
+apply (rule QUOTIENT_fset)
 (* FIRST_ASSUM MATCH_ACCEPT_TAC *)
 apply (assumption)
-prefer 5
+prefer 2
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* REFL_TAC *)
@@ -1274,41 +1272,31 @@
 apply (rule ext)
 (* APPLY_RSP *)
 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
-prefer 3
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 prefer 2
 apply (simp only: FUN_REL.simps)
-prefer 4
+prefer 2
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
-prefer 2
+apply (rule QUOTIENT_fset)
 (* APPLY_RSP *)
 apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] )
-prefer 3
+apply (rule QUOTIENT_fset)
+apply (rule QUOTIENT_fset)
 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"])
-(* 3: CONS respects *)
-prefer 3
-apply (simp only: FUN_REL.simps)
+apply (rule IDENTITY_QUOTIENT)
+(* CONS respects *)
+prefer 2
+apply (simp add: FUN_REL.simps)
+apply (rule allI)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (simp)
-thm cons_preserves
 apply (rule cons_preserves)
 apply (assumption)
-prefer 3
+prefer 2
 apply (simp)
-(* Mine *)
-apply (simp only: id_def)
-apply (rule IDENTITY_QUOTIENT)
-prefer 2
-apply (rule QUOTIENT_fset)
-prefer 2
-apply (rule QUOTIENT_fset)
-prefer 3
-apply (rule QUOTIENT_fset)
 sorry
 
 thm list.recs(2)