# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260205053 -3600
# Node ID 120e479ed3670001e3e9fd86eeecb7ba71ad5ebf
# Parent  0cf166548856c69c8fc6e5042f316228a89267c7
first attempt to deal with Babs in regularise and cleaning (not yet working)

diff -r 0cf166548856 -r 120e479ed367 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Mon Dec 07 15:21:51 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 17:57:33 2009 +0100
@@ -255,12 +255,59 @@
 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
 by simp
 
+(* test about lifting identity equations *)
 
-lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
-apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})
-defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* clean_tac  @{context} 1 *})
+ML {*
+(* helper code from QuotMain *)
+val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
+val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
+val simproc = Simplifier.simproc_i @{theory} "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
+val simpset = (mk_minimal_ss @{context}) 
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
+                       addsimprocs [simproc] addSolver equiv_solver
+*}
+
+(* What regularising does *)
+(*========================*)
+
+(* 0. preliminary simplification step *)
+thm ball_reg_eqv bex_reg_eqv babs_reg_eqv
+    ball_reg_eqv_range bex_reg_eqv_range
+(* 1. first two rtacs *)
+thm ball_reg_right bex_reg_left
+(* 2. monos *)
+(* 3. commutation rules *)
+thm ball_all_comm bex_ex_comm
+(* 4. then rel-equality *)
+thm eq_imp_rel
+(* 5. then simplification like 0 *)
+(* finally jump to 1 *)
+
+
+(* What cleaning does *)
+(*====================*)
+
+(* 1. conversion *)
+thm lambda_prs
+(* 2. simplification with *)
+thm all_prs ex_prs
+(* 3. Simplification with *)
+thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep
+(* 4. Test for refl *)
+
+lemma
+  shows "equivp (op \<approx>)"
+  and   "equivp ((op \<approx>) ===> (op \<approx>))"
+apply -
+apply(tactic {* equiv_tac @{context} 1 *})
+apply(tactic {* equiv_tac @{context} 1 *})?
+oops
+
+
+lemma
+  "(\<lambda>y. y) = (\<lambda>x. x) \<longrightarrow>
+    (op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))"
+apply(tactic {* simp_tac simpset  1 *})
 sorry
 
 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
@@ -268,6 +315,7 @@
 
 lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *})
+apply(tactic {* regularize_tac @{context} 1*})?
 defer
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
diff -r 0cf166548856 -r 120e479ed367 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 15:21:51 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 17:57:33 2009 +0100
@@ -183,6 +183,11 @@
     setmksimps (mksimps [])
 *}
 
+ML {*
+(* TODO/FIXME not needed anymore? *)
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
 section {* atomize *}
 
 lemma atomize_eqv[atomize]:
@@ -486,8 +491,8 @@
 
 ML {*
 fun equiv_tac ctxt =
-  REPEAT_ALL_NEW (FIRST' 
-    [resolve_tac (equiv_rules_get ctxt)])
+  (K (print_tac "equiv tac")) THEN'
+  REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
 *}
 
 ML {*
@@ -577,20 +582,23 @@
   val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
   val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
   val simpset = (mk_minimal_ss ctxt) 
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv}
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv}
                        addsimprocs [simproc] addSolver equiv_solver
   (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
+  (* can this cause loops in equiv_tac ? *)
   val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 in
   ObjectLogic.full_atomize_tac THEN'
   simp_tac simpset THEN'
-  REPEAT_ALL_NEW (FIRST' [
+  REPEAT_ALL_NEW (CHANGED o FIRST' [
     rtac @{thm ball_reg_right},
     rtac @{thm bex_reg_left},
     resolve_tac (Inductive.get_monos ctxt),
     rtac @{thm ball_all_comm},
     rtac @{thm bex_ex_comm},
-    resolve_tac eq_eqvs,
+    resolve_tac eq_eqvs,  
+    (* should be equivalent to the above, but causes loops: *) 
+    (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *)
     simp_tac simpset])
 end
 *}
@@ -848,9 +856,6 @@
         handle ERROR "find_qt_asm: no pair" => no_tac)
     | _ => no_tac)
 *}
-ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
 
 ML {*
 fun rep_abs_rsp_tac ctxt =
diff -r 0cf166548856 -r 120e479ed367 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Mon Dec 07 15:21:51 2009 +0100
+++ b/Quot/QuotScript.thy	Mon Dec 07 17:57:33 2009 +0100
@@ -256,7 +256,7 @@
   apply(rule iffI)
   apply(rule allI)
   apply(drule_tac x="\<lambda>y. f x" in bspec)
-  apply(simp add: Respects_def in_respects)
+  apply(simp add: in_respects)
   apply(rule impI)
   using a equivp_reflp_symp_transp[of "R2"]
   apply(simp add: reflp_def)
@@ -338,6 +338,12 @@
   using Quotient_rel[OF q]
   by metis
 
+(* needed for regularising? *)
+lemma babs_reg_eqv:
+  shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
+by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
+
+
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"