# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260045956 -3600
# Node ID e67961288b1264c6b84ecddef6a511880ae333d9
# Parent  287ea842a7d43a5f6c445f8d6b8821bf05409fca# Parent  8395fc6a694596b125ee077c1f166b3df2578a22
merged

diff -r 287ea842a7d4 -r e67961288b12 IntEx.thy
--- a/IntEx.thy	Sat Dec 05 21:44:01 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 21:45:56 2009 +0100
@@ -149,8 +149,6 @@
 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
 
-lemma cheat: "P" sorry
-
 lemma test1: "my_plus a b = my_plus a b"
 apply(rule refl)
 done
@@ -162,12 +160,10 @@
 abbreviation 
   "Resp \<equiv> Respects"
 
-
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* lambda_allex_prs_tac @{context} 1 *})
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 
@@ -177,9 +173,32 @@
 
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
-apply(rule cheat)
-apply(rule cheat)
+apply(rule ballI)
+apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp])
+apply(simp only: in_respects)
+
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(rule quot_rel_rsp)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(fold PLUS_def)
 apply(tactic {* clean_tac @{context} 1 *})
+thm Quotient_rel_rep
+thm Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]
+apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 done
 
 lemma test3: "my_plus = my_plus"
@@ -188,9 +207,17 @@
 
 lemma "PLUS = PLUS"
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
-apply(rule cheat)
-apply(rule cheat)
+apply(rule ho_plus_rsp)
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(rule quot_rel_rsp)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
+apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
 done
 
 
diff -r 287ea842a7d4 -r e67961288b12 QuotMain.thy
--- a/QuotMain.thy	Sat Dec 05 21:44:01 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 21:45:56 2009 +0100
@@ -964,12 +964,6 @@
     | _ => no_tac)
 *}
 
-lemma fun_rel_id:
-  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
-  shows "(R1 ===> R2) f g"
-using a by simp
-
-
 ML {*
 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case (bare_concl goal) of
diff -r 287ea842a7d4 -r e67961288b12 QuotScript.thy
--- a/QuotScript.thy	Sat Dec 05 21:44:01 2009 +0100
+++ b/QuotScript.thy	Sat Dec 05 21:45:56 2009 +0100
@@ -335,6 +335,19 @@
   using a unfolding Quotient_def
   by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply)
 
+lemma fun_rel_id:
+  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+  shows "(R1 ===> R2) f g"
+using a by simp
+
+lemma quot_rel_rsp:
+  assumes a: "Quotient R Abs Rep"
+  shows "(R ===> R ===> op =) R R"
+  apply(rule fun_rel_id)+
+  apply(rule equals_rsp[OF a])
+  apply(assumption)+
+  done
+