Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Minor cleaning
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 27 Nov 2009 07:00:14 +0100
changeset 414 4dad34ca50db
parent 413 f79dd5500838
child 415 5a9bdf81672d
Minor cleaning
FSet.thy file | annotate | diff | comparison | revisions
IntEx.thy file | annotate | diff | comparison | revisions
LFex.thy file | annotate | diff | comparison | revisions 
--- 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"
--- 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
 
 (*
--- 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 =
nominal2