src/Sequents/ILL.thy
changeset 30510 4120fc59dd85
parent 22894 619b270607ac
child 30549 d2d7874648bd
equal deleted inserted replaced
30509:e19d5b459a61 30510:4120fc59dd85
   144 
   144 
   145 end
   145 end
   146 *}
   146 *}
   147 
   147 
   148 method_setup best_lazy =
   148 method_setup best_lazy =
   149   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *}
   149   {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
   150   "lazy classical reasoning"
   150   "lazy classical reasoning"
   151 
   151 
   152 lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
   152 lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
   153   apply (rule derelict)
   153   apply (rule derelict)
   154   apply (rule impl)
   154   apply (rule impl)
   280 val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
   280 val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
   281 *}
   281 *}
   282 
   282 
   283 
   283 
   284 method_setup best_safe =
   284 method_setup best_safe =
   285   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} ""
   285   {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
   286 
   286 
   287 method_setup best_power =
   287 method_setup best_power =
   288   {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} ""
   288   {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
   289 
   289 
   290 
   290 
   291 (* Some examples from Troelstra and van Dalen *)
   291 (* Some examples from Troelstra and van Dalen *)
   292 
   292 
   293 lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
   293 lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"