Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LamEx.thy
changeset 258 93ea455b29f1
parent 257 68bd5c2a1b96
child 259 22c199522bef
equal deleted inserted replaced
257:68bd5c2a1b96 258:93ea455b29f1 
   238       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
 
   238       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
 
   239      ]);
 
   239      ]);
 
   240  *}
 
   240  *}
 
   241   apply (tactic {* tac @{context} 1 *}) *)
 
   241   apply (tactic {* tac @{context} 1 *}) *)
 
   242 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 
   242 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 
   243 ML {*
 
   243 (*ML {*
 
   244   val rt = build_repabs_term @{context} t_r consts rty qty
 
   244   val rt = build_repabs_term @{context} t_r consts rty qty
 
   245   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 
   245   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 
   246 *}
 
   246 *}
 
   247 prove rg
 
   247 prove rg
 
   248 apply(atomize(full))
 
   248 apply(atomize(full))
 
   257      (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
 
   257      (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
 
   258      THEN_ALL_NEW (fn _ => no_tac)
 
   258      THEN_ALL_NEW (fn _ => no_tac)
 
   259     ),
 
   259     ),
 
   260     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
 
   260     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
 
   261     rtac refl,
 
   261     rtac refl,
 
   262 (*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
 
       
   263     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
 
   262     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
 
   264     Cong_Tac.cong_tac @{thm cong},
 
   263     Cong_Tac.cong_tac @{thm cong},
 
   265     rtac @{thm ext},
 
   264     rtac @{thm ext},
 
   266     rtac reflex_thm,
 
   265     rtac reflex_thm,
 
   267     atac,
 
   266     atac,
 
   272     WEAK_LAMBDA_RES_TAC ctxt
 
   271     WEAK_LAMBDA_RES_TAC ctxt
 
   273     ]);
 
   272     ]);
 
   274   fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
 
   273   fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
 
   275 *}
 
   274 *}
 
   276 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
   275 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
   277 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
   276 *)
 
   278 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   279 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   280 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   281 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   282 prefer 2
 
       
   283 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   284 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   285 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   286 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   287 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   288 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   289 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   290 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   291 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   292 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   293 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   294 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   295 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   296 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   297 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   298 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   299 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   300 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   301 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   302 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   303 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   304 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   305 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   306 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   307 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
 
       
   308 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   309 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
 
       
   310 
       
   311 
   277 
   312 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 
   278 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 
   313 
   279 
   314 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}
 
   280 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}
 
   315 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
 
   281 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
 
       
   282 
       
   283 ML {*
 
       
   284 
       
   285 
       
   286 *}
 
       
   287 
   316 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *}
 
   288 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *}
 
   317 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
 
   289 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
 
   318 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 
   290 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 
   319 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_t *}
 
   291 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_t *}
 
   320 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
 
   292 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
nominal2