equal
deleted
inserted
replaced
53 apply blast |
53 apply blast |
54 done |
54 done |
55 |
55 |
56 ML {* |
56 ML {* |
57 fun wfd_strengthen_tac ctxt s i = |
57 fun wfd_strengthen_tac ctxt s i = |
58 RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1) |
58 res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1) |
59 *} |
59 *} |
60 |
60 |
61 lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P" |
61 lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P" |
62 apply (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P") |
62 apply (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P") |
63 apply blast |
63 apply blast |
454 (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => (term_vars a = []) |
454 (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => (term_vars a = []) |
455 | _ => false |
455 | _ => false |
456 in |
456 in |
457 |
457 |
458 fun rcall_tac ctxt i = |
458 fun rcall_tac ctxt i = |
459 let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i |
459 let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i |
460 in IHinst tac @{thms rcallTs} i end |
460 in IHinst tac @{thms rcallTs} i end |
461 THEN eresolve_tac @{thms rcall_lemmas} i |
461 THEN eresolve_tac @{thms rcall_lemmas} i |
462 |
462 |
463 fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE |
463 fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE |
464 rcall_tac ctxt i ORELSE |
464 rcall_tac ctxt i ORELSE |
476 |
476 |
477 val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' |
477 val clean_ccs_tac = REPEAT_FIRST (eresolve_tac ([@{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' |
478 hyp_subst_tac) |
478 hyp_subst_tac) |
479 |
479 |
480 fun clean_ccs_tac ctxt = |
480 fun clean_ccs_tac ctxt = |
481 let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in |
481 let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in |
482 TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' |
482 TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' |
483 eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' |
483 eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' |
484 hyp_subst_tac)) |
484 hyp_subst_tac)) |
485 end |
485 end |
486 |
486 |