# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259302576 -3600
# Node ID 5a9bdf81672d625cd6a50281cc11ee74c29e76d8
# Parent  4dad34ca50db14be802006c246f5d8bb43181ae6
More cleaning in QuotMain, identity handling.

diff -r 4dad34ca50db -r 5a9bdf81672d QuotMain.thy
--- a/QuotMain.thy	Fri Nov 27 07:00:14 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 07:16:16 2009 +0100
@@ -201,28 +201,21 @@
 
 section {* infrastructure about id *}
 
-(* Need to have a meta-equality *)
-
-lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
-by (simp add: id_def)
-
-(* TODO: can be also obtained with: *)
-ML {* symmetric (eq_reflection OF @{thms id_def}) *}
-
 lemma prod_fun_id: "prod_fun id id \<equiv> id"
-by (rule eq_reflection) (simp add: prod_fun_def)
+  by (rule eq_reflection) (simp add: prod_fun_def)
 
 lemma map_id: "map id \<equiv> id"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (rule_tac list="x" in list.induct)
-apply (simp_all)
-done
+  apply (rule eq_reflection)
+  apply (rule ext)
+  apply (rule_tac list="x" in list.induct)
+  apply (simp_all)
+  done
 
 lemmas id_simps =
   FUN_MAP_I[THEN eq_reflection]
   id_apply[THEN eq_reflection]
-  id_def_sym prod_fun_id map_id
+  id_def[THEN eq_reflection,symmetric]
+  prod_fun_id map_id
 
 ML {*
 fun simp_ids thm =
@@ -905,29 +898,15 @@
     val llhs = Syntax.check_term lthy lhs;
     val eq = Logic.mk_equals (llhs, rhs);
     val ceq = cterm_of (ProofContext.theory_of lthy') eq;
-    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply});
+    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps id_simps});
     val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
-    val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t;
-                                              (* FIXME/TODO: should that be id_simps? *)
+    val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
   in
     singleton (ProofContext.export lthy' lthy) t_id
   end
 *}
 
 ML {*
-fun findaps_all rty tm =
-  case tm of
-    Abs(_, T, b) =>
-      findaps_all rty (subst_bound ((Free ("x", T)), b))
-  | (f $ a) => (findaps_all rty f @ findaps_all rty a)
-  | Free (_, (T as (Type ("fun", (_ :: _))))) =>
-      (if needs_lift rty T then [T] else [])
-  | _ => [];
-fun findaps rty tm = distinct (op =) (findaps_all rty tm)
-*}
-
-
-ML {*
 fun find_aps_all rtm qtm =
   case (rtm, qtm) of
     (Abs(_, T1, s1), Abs(_, T2, s2)) =>
@@ -945,7 +924,6 @@
 *}
 
 ML {*
-(* FIXME: allex_prs and lambda_prs can be one function *)
 fun allex_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
   THEN' (quotient_tac quot);
@@ -988,7 +966,7 @@
     val gc = Drule.strip_imp_concl (cprop_of lpi);
     val t = Goal.prove_internal [] gc (fn _ => tac 1)
     val te = @{thm eq_reflection} OF [t]
-    val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
+    val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
     val tl = Thm.lhs_of ts
 (*    val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
 (*    val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)