# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260311447 -3600
# Node ID d8f07b5bcfaece75fdb7849815fb081d0ef306ea
# Parent  0b29650e3fd8bff03966535924b0a9ec06a9c786
implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges

diff -r 0b29650e3fd8 -r d8f07b5bcfae Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 22:26:01 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 23:30:47 2009 +0100
@@ -435,6 +435,9 @@
 apply(simp)
 apply(rule allI)
 apply(rule list_eq_refl)
+apply(cleaning)
+apply(simp add: fun_map.simps expand_fun_eq)
+apply(cleaning)
 done
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
@@ -462,4 +465,7 @@
 apply(tactic {* lambda_prs_tac @{context} 1 *})
 (* Until here is ok *)
 apply(cleaning)
+sorry
+
+
 end
diff -r 0b29650e3fd8 -r d8f07b5bcfae Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 22:26:01 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 23:30:47 2009 +0100
@@ -321,6 +321,7 @@
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
 apply(lifting lam_tst4)
-done
+apply(cleaning)
+sorry
 
 end
diff -r 0b29650e3fd8 -r d8f07b5bcfae Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 22:26:01 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 23:30:47 2009 +0100
@@ -1047,6 +1047,29 @@
 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps 
 (* 4. Test for refl *)
 
+thm fun_map.simps
+
+ML {* Conv.abs_conv; term_of *}
+
+thm fun_map.simps[THEN eq_reflection]
+
+ML {*
+fun fun_map_conv xs ctxt ctrm =
+  case (term_of ctrm) of
+    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
+        (Conv.binop_conv (fun_map_conv xs ctxt) then_conv
+        (if (member (op=) xs h) 
+         then Conv.all_conv 
+         else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]})) ctrm
+    | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm
+    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
+    | _ => Conv.all_conv ctrm
+*}
+
+ML {*
+fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
+*}
+
 ML {*
 fun clean_tac lthy =
   let
@@ -1059,9 +1082,9 @@
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [simp_tac (simps thms1),
+            fun_map_tac lthy,
             lambda_prs_tac lthy,
             simp_tac (simps thms2),
-            lambda_prs_tac lthy,
             TRY o rtac refl]
   end
 *}