# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259261491 -3600
# Node ID fafcc54e531d030ba4a1f50b6d2ae7d20a9d9005
# Parent  559c01f40beeeed3bb6e732d0efc400614dacf9e
some diagnostic code for r_mk_comb

diff -r 559c01f40bee -r fafcc54e531d FSet.thy
--- a/FSet.thy	Thu Nov 26 16:23:24 2009 +0100
+++ b/FSet.thy	Thu Nov 26 19:51:31 2009 +0100
@@ -346,78 +346,12 @@
 
 lemma cheat: "P" sorry
 
-lemma imp_refl: "P \<longrightarrow> P" by simp
-
-lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
-apply(auto)
-done
-
-thm Set.conj_mono
-thm Set.imp_mono
-ML {* Inductive.get_monos @{context} *}
-thm LEFT_RES_FORALL_REGULAR
-
-lemma test: 
-  fixes P Q::"'a \<Rightarrow> bool"  
-  and x::"'a"
-  assumes a: "REFL R2"
-  and     b: "\<And>f. Q (f x) \<Longrightarrow> P (f x)"
-  shows "(\<forall>f\<in>(Respects (R1 ===> R2)). Q (f x)) \<longrightarrow> (\<forall>f. P (f x))"
-apply(rule impI)
-apply(rule allI)
-apply(drule_tac x="\<lambda>y. f x" in bspec)
-apply(simp add: Respects_def IN_RESPECTS)
-apply(rule impI)
-using a
-apply(simp add: REFL_def)
-using b
-apply -
-apply(simp)
-done
-
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-defer
-apply(rule cheat)
 apply(rule cheat)
-apply(atomize (full))
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule LEFT_RES_FORALL_REGULAR)
-apply(rule conjI)
-using list_eq_refl
-thm Ball_def IN_RESPECTS FUN_REL.simps
-
-apply -
-apply(simp (no_asm) add: Respects_def)
-apply(blast)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule LEFT_RES_FORALL_REGULAR)
-apply(rule conjI)
-defer
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(unfold Respects_def)
-sorry
-
-lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
-apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-defer
+prefer 2
 apply(rule cheat)
-apply(rule cheat)
-apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
-done
+apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
diff -r 559c01f40bee -r fafcc54e531d QuotMain.thy
--- a/QuotMain.thy	Thu Nov 26 16:23:24 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 19:51:31 2009 +0100
@@ -685,7 +685,6 @@
 
 section {* RepAbs injection tactic *}
 (*
-
 To prove that the regularised theorem implies the abs/rep injected, we first
 atomize it and then try:
 
@@ -835,6 +834,56 @@
     ])
 *}
 
+(*
+To prove that the regularised theorem implies the abs/rep injected, 
+we try:
+
+ 1) theorems 'trans2' from the appropriate QUOT_TYPE
+ 2) remove lambdas from both sides (LAMBDA_RES_TAC)
+ 3) remove Ball/Bex from the right hand side
+ 4) use user-supplied RSP theorems
+ 5) remove rep_abs from the right side
+ 6) reflexivity of equality
+ 7) split applications of lifted type (apply_rsp)
+ 8) split applications of non-lifted type (cong_tac)
+ 9) apply extentionality
+10) reflexivity of the relation
+11) assumption
+    (Lambdas under respects may have left us some assumptions)
+12) proving obvious higher order equalities by simplifying fun_rel
+    (not sure if it is still needed?)
+13) unfolding lambda on one side
+14) simplifying (= ===> =) for simpler respectfulness
+
+*)
+
+ML {*
+fun r_mk_comb_tac' ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+  REPEAT_ALL_NEW (FIRST' [
+    (K (print_tac "start")) THEN' (K no_tac), 
+    DT ctxt "1" (rtac trans_thm),
+    DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+    DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+    DT ctxt "4" (ball_rsp_tac ctxt),
+    DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+    DT ctxt "6" (bex_rsp_tac ctxt),
+    DT ctxt "7" (FIRST' (map rtac rsp_thms)),
+    DT ctxt "8" (rtac refl),
+    DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
+                  THEN' (RANGE [SOLVES' (quotient_tac quot_thm)]))),
+    DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
+                (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)]))),
+    DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+    DT ctxt "C" (rtac @{thm ext}),
+    DT ctxt "D" (rtac reflex_thm),
+    DT ctxt "E" (atac),
+    DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
+    DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
+    DT ctxt "H" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
+    ])
+*}
+
+
 
 (****************************************)
 (* cleaning of the theorem              *)