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.
Stronger tactic, simpler proof.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 23 Oct 2009 18:20:06 +0200
changeset 164 4f00ca4f5ef4
parent 163 3da18bf6886c
child 165 2c83d04262f9
child 166 3300260b63a1
Stronger tactic, simpler proof.
FSet.thy file | annotate | diff | comparison | revisions 
--- a/FSet.thy	Fri Oct 23 16:34:20 2009 +0200
+++ b/FSet.thy	Fri Oct 23 18:20:06 2009 +0200
@@ -172,26 +172,38 @@
 thm fun_map.simps
 text {* Respectfullness *}
 
-lemma mem_respects:
+lemma memb_rsp:
   fixes z
   assumes a: "list_eq x y"
   shows "(z memb x) = (z memb y)"
   using a by induct auto
 
+lemma ho_memb_rsp:
+  "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
+  apply (simp add: FUN_REL.simps)
+  apply (metis memb_rsp)
+  done
+
 lemma card1_rsp:
   fixes a b :: "'a list"
   assumes e: "a \<approx> b"
   shows "card1 a = card1 b"
   using e apply induct
-  apply (simp_all add:mem_respects)
+  apply (simp_all add:memb_rsp)
   done
 
-lemma cons_preserves:
+lemma cons_rsp:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule list_eq.intros(5))
 
+lemma ho_cons_rsp:
+  "op = ===> op \<approx> ===> op \<approx> op # op #"
+  apply (simp add: FUN_REL.simps)
+  apply (metis cons_rsp)
+  done
+
 lemma append_respects_fst:
   assumes a : "list_eq l1 l2"
   shows "list_eq (l1 @ s) (l2 @ s)"
@@ -251,6 +263,16 @@
 *}
 
 ML {*
+fun LAMBDA_RES_TAC ctxt =
+  case (term_of o #concl o fst) (Subgoal.focus ctxt 1 (Isar.goal ())) of
+    (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | _ => fn _ => no_tac
+*}
+
+
+ML {*
 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm =
   (FIRST' [
     rtac @{thm FUN_QUOTIENT},
@@ -258,10 +280,12 @@
     rtac @{thm IDENTITY_QUOTIENT},
     rtac @{thm ext},
     rtac trans_thm,
+    LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+    rtac refl,
     (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
-    rtac reflex_thm,
+    rtac reflex_thm, 
     atac,
     (
      (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))
@@ -280,15 +304,13 @@
 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
+
 prove list_induct_tr: trm_r
 apply (atomize(full))
 (* APPLY_RSP_TAC *)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RES_TAC *)
-apply (simp only: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* MK_COMB_TAC *)
@@ -300,14 +322,11 @@
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* REFL_TAC *)
-apply (simp)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* APPLY_RSP_TAC *)
 apply (tactic {* REPEAT_ALL_NEW (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 (rule allI)
-apply (rule allI)
-apply (rule impI)
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* MK_COMB_TAC *)
@@ -319,19 +338,14 @@
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* REFL_TAC *)
-apply (simp)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* W(C (curry op THEN) (G... *)
+apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* CONS respects *)
-apply (simp add: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (rule cons_preserves)
-apply (assumption)
+apply (rule ho_cons_rsp)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp only: FUN_REL.simps)
+apply (subst FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
@@ -360,48 +374,26 @@
 prove m2_t_p: m2_t_g
 apply (atomize(full))
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp add: FUN_REL.simps)
 prefer 2
-apply (simp only: FUN_REL.simps)
+apply (subst FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 prefer 2
-apply (simp only: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp only: FUN_REL.simps)
+apply (subst FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (simp only: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (simp add:mem_respects)
-apply (simp only: FUN_REL.simps)
+apply (subst FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (simp add:cons_preserves)
-apply (simp only: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (simp add:mem_respects)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (rule ho_memb_rsp)
+apply (rule ho_cons_rsp)
+apply (rule ho_memb_rsp)
 apply (auto)
 done
 
@@ -413,7 +405,6 @@
 lemma id_apply2 [simp]: "id x \<equiv> x"
   by (simp add: id_def)
 
-
 thm LAMBDA_PRS
 ML {*
  val t = prop_of @{thm LAMBDA_PRS}
@@ -443,9 +434,9 @@
 ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *}
 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *}
 ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *}
-ML {* rwrs; m2_t' *}
-ML {* eqsubst_thm @{context} [rwrs] m2_t' *}
-thm INSERT_def
+ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *}
+ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *}
+ML {* ObjectLogic.rulify rthm *}
 
 
 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
@@ -474,7 +465,7 @@
   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
 unfolding IN_def EMPTY_def
 apply(rule_tac f="(op =) False" in arg_cong)
-apply(rule mem_respects)
+apply(rule memb_rsp)
 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply(rule list_eq.intros)
 done
@@ -493,7 +484,7 @@
 unfolding IN_def INSERT_def
 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
-apply(rule mem_respects)
+apply(rule memb_rsp)
 apply(rule list_eq.intros(3))
 apply(unfold REP_fset_def ABS_fset_def)
 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
@@ -554,7 +545,7 @@
     REPEAT_ALL_NEW (FIRST' [
       rtac @{thm list_eq_refl},
       rtac @{thm cons_preserves},
-      rtac @{thm mem_respects},
+      rtac @{thm memb_rsp},
       rtac @{thm card1_rsp},
       rtac @{thm QUOT_TYPE_I_fset.R_trans2},
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
nominal2