# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255788414 -7200
# Node ID 9cb8f9a59402d952e5abcf9e770a4ab0c4762659
# Parent  b5d293e0b9bbf5a60c7794d6da356ffcb2301f58
Partial simplification of the proof

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)
diff -r b5d293e0b9bb -r 9cb8f9a59402 QuotScript.thy
--- a/QuotScript.thy	Sat Oct 17 15:42:57 2009 +0200
+++ b/QuotScript.thy	Sat Oct 17 16:06:54 2009 +0200
@@ -81,8 +81,8 @@
 by auto
 
 lemma IDENTITY_QUOTIENT:
-  shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"
-unfolding QUOTIENT_def
+  shows "QUOTIENT (op =) id id"
+unfolding QUOTIENT_def id_def
 by blast
 
 lemma QUOTIENT_SYM:
@@ -114,8 +114,8 @@
   "f ---> g \<equiv> fun_map f g"
 
 lemma FUN_MAP_I:
-  shows "((\<lambda>x. x) ---> (\<lambda>x. x)) = (\<lambda>x. x)"
-by (simp add: expand_fun_eq)
+  shows "(id ---> id) = id"
+by (simp add: expand_fun_eq id_def)
 
 lemma IN_FUN:
   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
@@ -382,13 +382,13 @@
 
 lemma I_PRS:
   assumes q: "QUOTIENT R Abs Rep"
-  shows "(\<lambda>x. x) e = Abs ((\<lambda> x. x) (Rep e))"
+  shows "id e = Abs (id (Rep e))"
 using QUOTIENT_ABS_REP[OF q] by auto
 
 lemma I_RSP:
   assumes q: "QUOTIENT R Abs Rep"
   and     a: "R e1 e2"
-  shows "R ((\<lambda>x. x) e1) ((\<lambda> x. x) e2)"
+  shows "R (id e1) (id e2)"
 using a by auto
 
 lemma o_PRS: