# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260047109 -3600
# Node ID 41500cd131dcf09191e4de9fefda0b19034d7b5b
# Parent  d641c32855f0e4dcf639ad9bddeb467cd1b9aca7
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.

diff -r d641c32855f0 -r 41500cd131dc IntEx.thy
--- a/IntEx.thy	Sat Dec 05 21:50:31 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 22:05:09 2009 +0100
@@ -130,17 +130,11 @@
   apply(auto)
   done
 
-lemma list_equiv_rsp[quotient_rsp]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
-by auto
-
-lemma ho_plus_rsp[quotient_rsp]:
+lemma plus_rsp[quotient_rsp]:
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
 ML {* val qty = @{typ "my_int"} *}
-ML {* val ty_name = "my_int" *}
-ML {* val rsp_thms = @{thms ho_plus_rsp} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 
@@ -174,7 +168,7 @@
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
 apply(rule ballI)
-apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp])
+apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
 apply(simp only: in_respects)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
@@ -186,7 +180,7 @@
 
 lemma "PLUS = PLUS"
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
-apply(rule ho_plus_rsp)
+apply(rule plus_rsp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
@@ -238,14 +232,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(rule nil_rsp)
-apply(tactic {* quotient_tac @{context} 1*})
-apply(simp only: fun_map.simps id_simps)
-apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
-apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
-apply(simp) (* FIXME: why is this needed *)
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
@@ -255,13 +243,7 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(rule cons_rsp)
-apply(tactic {* quotient_tac @{context} 1 *})
-apply(simp only: fun_map.simps id_simps)
-apply(simp only: Quotient_abs_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
-apply(simp only: Quotient_abs_rep[OF list_quotient[OF Quotient_my_int]])
-apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
-apply(simp only: cons_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 done
 
diff -r d641c32855f0 -r 41500cd131dc QuotMain.thy
--- a/QuotMain.thy	Sat Dec 05 21:50:31 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 22:05:09 2009 +0100
@@ -149,7 +149,7 @@
   fun_quotient list_quotient
 
 lemmas [quotient_rsp] =
-  quot_rel_rsp
+  quot_rel_rsp nil_rsp cons_rsp
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
@@ -984,13 +984,6 @@
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const (@{const_name fun_rel}, _) $ _ $ _)
-    => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Const _) $ (Const _) =>
-    (* respectfulness of constants; in particular of a simple relation *)
-    resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
 | Const (@{const_name "op ="},_) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
@@ -1005,6 +998,13 @@
     rtac @{thm refl} ORELSE'
     (resolve_tac trans2 THEN' RANGE [
       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+    (Const (@{const_name fun_rel}, _) $ _ $ _) $
+    (Const (@{const_name fun_rel}, _) $ _ $ _)
+    => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
+| _ $ (Const _) $ (Const _) => (* fun_rel, list_rel, etc but not equality *)
+    (* respectfulness of constants; in particular of a simple relation *)
+    resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
 | _ $ _ $ _ =>
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *)