# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259301614 -3600
# Node ID 4dad34ca50db14be802006c246f5d8bb43181ae6
# Parent  f79dd55008386d4d1000673215ac85d3ce7d5094
Minor cleaning

diff -r f79dd5500838 -r 4dad34ca50db FSet.thy
--- a/FSet.thy	Fri Nov 27 04:02:20 2009 +0100
+++ b/FSet.thy	Fri Nov 27 07:00:14 2009 +0100
@@ -345,58 +345,11 @@
 
 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 *})
-apply(rule cheat)
+apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *})
 prefer 2
-apply(rule cheat)
+apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
 apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*})
-thm RES_FORALL_RSP
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-sorry
+done
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
diff -r f79dd5500838 -r 4dad34ca50db IntEx.thy
--- a/IntEx.thy	Fri Nov 27 04:02:20 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 07:00:14 2009 +0100
@@ -164,8 +164,12 @@
 apply simp
 done
 
+lemma map_prs: "map REP_my_int (map ABS_my_int x) = x"
+sorry
+
 lemma "foldl PLUS x [] = x"
 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
+apply (simp_all only: map_prs)
 sorry
 
 (*
diff -r f79dd5500838 -r 4dad34ca50db LFex.thy
--- a/LFex.thy	Fri Nov 27 04:02:20 2009 +0100
+++ b/LFex.thy	Fri Nov 27 07:00:14 2009 +0100
@@ -263,8 +263,7 @@
     val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs))
   in
   (ObjectLogic.full_atomize_tac) THEN'
-  (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) 
-  THEN'
+  (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) THEN'
   REPEAT_ALL_NEW (FIRST' [
     (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
     (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
@@ -274,7 +273,8 @@
     (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
     (resolve_tac (Inductive.get_monos ctxt)),
     rtac @{thm move_forall},
-    rtac @{thm move_exists}
+    rtac @{thm move_exists},
+    (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc]))
   ])
   end
 *}
@@ -300,95 +300,9 @@
    ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-
-apply(rule LEFT_RES_FORALL_REGULAR)
-apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *})
-apply(atomize (full))
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(rule test)
-defer
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule test)
-defer
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(rule test)
-defer
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-
-
-thm test[OF mp]
-
-
 prefer 2
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-apply(thin_tac "Respects (akind ===> akind ===> op =) x") 
-apply(thin_tac "Respects (aty ===> aty ===> op =) xa")
-apply(thin_tac "Respects (atrm ===> atrm ===> op =) xb")
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-
-apply(rule LEFT_RES_FORALL_REGULAR)
-apply(rule conjI)
-prefer 2
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
-using al_refl
-apply(simp add: Respects_def)
-
-
-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(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(rule impI) apply(assumption)
-apply(rule Set.imp_mono)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-apply(rule Set.imp_mono)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-apply(rule Set.imp_mono)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply(rule move_quant)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-apply(rule impI) apply(assumption)
+apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*})
+apply (tactic {* clean_tac @{context} quot defs reps_same absrep 1 *})
 
 ML {*
 val rty_qty_rel =