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.
Further developing the tactic and simplifying the proof
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 22 Oct 2009 17:35:40 +0200
changeset 159 7cefc03224df
parent 158 c0d13b337c66
child 160 6b475324cef7
Further developing the tactic and simplifying the proof
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/QuotMain.thy	Thu Oct 22 16:24:02 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 17:35:40 2009 +0200
@@ -1031,6 +1031,12 @@
   (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
 *}
 
+ML {* 
+
+((simp_tac ((Simplifier.context @{context}  HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' (fn _ => no_tac))
+*}
+
+ML {* ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))  THEN_ALL_NEW (fn _ => no_tac)) *}
 
 ML {*
 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm =
@@ -1045,7 +1051,8 @@
       instantiate_tac @{thm APPLY_RSP} ctxt,
       rtac reflex_thm,
 (*      Cong_Tac.cong_tac @{thm cong},*)
-      atac
+      atac,
+      ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))  THEN_ALL_NEW (fn _ => no_tac))
     ])
 *}
 
@@ -1091,7 +1098,6 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp only: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
@@ -1115,8 +1121,6 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-(* MINE *)
-apply (simp only: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
@@ -1128,7 +1132,6 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp only: FUN_REL.simps)
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
@@ -1160,7 +1163,6 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp add: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done
nominal2