247 |
246 |
248 *} |
247 *} |
249 |
248 |
250 ML {* |
249 ML {* |
251 |
250 |
252 val caseB_lemmas = mk_lemmas (thms "caseBs") |
251 val caseB_lemmas = mk_lemmas @{thms caseBs} |
253 |
252 |
254 val ccl_dstncts = |
253 val ccl_dstncts = |
255 let fun mk_raw_dstnct_thm rls s = |
254 let fun mk_raw_dstnct_thm rls s = |
256 prove_goal (the_context ()) s (fn _=> [rtac notI 1,eresolve_tac rls 1]) |
255 prove_goal @{theory} s (fn _=> [rtac notI 1,eresolve_tac rls 1]) |
257 in map (mk_raw_dstnct_thm caseB_lemmas) |
256 in map (mk_raw_dstnct_thm caseB_lemmas) |
258 (mk_dstnct_rls (the_context ()) ["bot","true","false","pair","lambda"]) end |
257 (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end |
259 |
258 |
260 fun mk_dstnct_thms thy defs inj_rls xs = |
259 fun mk_dstnct_thms thy defs inj_rls xs = |
261 let fun mk_dstnct_thm rls s = prove_goalw thy defs s |
260 let fun mk_dstnct_thm rls s = prove_goalw thy defs s |
262 (fn _ => [simp_tac (simpset_of thy addsimps (rls@inj_rls)) 1]) |
261 (fn _ => [simp_tac (simpset_of thy addsimps (rls@inj_rls)) 1]) |
263 in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end |
262 in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end |
271 val XH_to_E = make_elim o XH_to_D |
270 val XH_to_E = make_elim o XH_to_D |
272 val XH_to_Is = map XH_to_I |
271 val XH_to_Is = map XH_to_I |
273 val XH_to_Ds = map XH_to_D |
272 val XH_to_Ds = map XH_to_D |
274 val XH_to_Es = map XH_to_E; |
273 val XH_to_Es = map XH_to_E; |
275 |
274 |
276 bind_thms ("ccl_rews", thms "caseBs" @ ccl_injs @ ccl_dstncts); |
275 bind_thms ("ccl_rews", @{thms caseBs} @ ccl_injs @ ccl_dstncts); |
277 bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [notE]); |
276 bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [notE]); |
278 bind_thms ("ccl_injDs", XH_to_Ds (thms "ccl_injs")); |
277 bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs}); |
279 *} |
278 *} |
280 |
279 |
281 lemmas [simp] = ccl_rews |
280 lemmas [simp] = ccl_rews |
282 and [elim!] = pair_inject ccl_dstnctsEs |
281 and [elim!] = pair_inject ccl_dstnctsEs |
283 and [dest!] = ccl_injDs |
282 and [dest!] = ccl_injDs |
386 done |
385 done |
387 |
386 |
388 ML {* |
387 ML {* |
389 |
388 |
390 local |
389 local |
391 fun mk_thm s = prove_goal (the_context ()) s (fn _ => |
390 fun mk_thm s = prove_goal @{theory} s (fn _ => |
392 [rtac notI 1,dtac (thm "case_pocong") 1,etac rev_mp 5, |
391 [rtac notI 1, dtac @{thm case_pocong} 1, etac rev_mp 5, |
393 ALLGOALS (simp_tac @{simpset}), |
392 ALLGOALS (simp_tac @{simpset}), |
394 REPEAT (resolve_tac [thm "po_refl", thm "npo_lam_bot"] 1)]) |
393 REPEAT (resolve_tac [@{thm po_refl}, @{thm npo_lam_bot}] 1)]) |
395 in |
394 in |
396 |
395 |
397 val npo_rls = [thm "npo_pair_lam", thm "npo_lam_pair"] @ map mk_thm |
396 val npo_rls = [@{thm npo_pair_lam}, @{thm npo_lam_pair}] @ map mk_thm |
398 ["~ true [= false", "~ false [= true", |
397 ["~ true [= false", "~ false [= true", |
399 "~ true [= <a,b>", "~ <a,b> [= true", |
398 "~ true [= <a,b>", "~ <a,b> [= true", |
400 "~ true [= lam x. f(x)","~ lam x. f(x) [= true", |
399 "~ true [= lam x. f(x)","~ lam x. f(x) [= true", |
401 "~ false [= <a,b>", "~ <a,b> [= false", |
400 "~ false [= <a,b>", "~ <a,b> [= false", |
402 "~ false [= lam x. f(x)","~ lam x. f(x) [= false"] |
401 "~ false [= lam x. f(x)","~ lam x. f(x) [= false"] |