32 "_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5) |
32 "_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5) |
33 "_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) |
33 "_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) |
34 "_PromAux" :: "three_seqe" ("promaux {_||_||_}") |
34 "_PromAux" :: "three_seqe" ("promaux {_||_||_}") |
35 |
35 |
36 parse_translation \<open> |
36 parse_translation \<open> |
37 [(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})), |
37 [(\<^syntax_const>\<open>_Trueprop\<close>, K (single_tr \<^const_syntax>\<open>Trueprop\<close>)), |
38 (@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})), |
38 (\<^syntax_const>\<open>_Context\<close>, K (two_seq_tr \<^const_syntax>\<open>Context\<close>)), |
39 (@{syntax_const "_PromAux"}, K (three_seq_tr @{const_syntax PromAux}))] |
39 (\<^syntax_const>\<open>_PromAux\<close>, K (three_seq_tr \<^const_syntax>\<open>PromAux\<close>))] |
40 \<close> |
40 \<close> |
41 |
41 |
42 print_translation \<open> |
42 print_translation \<open> |
43 [(@{const_syntax Trueprop}, K (single_tr' @{syntax_const "_Trueprop"})), |
43 [(\<^const_syntax>\<open>Trueprop\<close>, K (single_tr' \<^syntax_const>\<open>_Trueprop\<close>)), |
44 (@{const_syntax Context}, K (two_seq_tr' @{syntax_const "_Context"})), |
44 (\<^const_syntax>\<open>Context\<close>, K (two_seq_tr' \<^syntax_const>\<open>_Context\<close>)), |
45 (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))] |
45 (\<^const_syntax>\<open>PromAux\<close>, K (three_seq_tr' \<^syntax_const>\<open>_PromAux\<close>))] |
46 \<close> |
46 \<close> |
47 |
47 |
48 definition liff :: "[o, o] \<Rightarrow> o" (infixr "o-o" 45) |
48 definition liff :: "[o, o] \<Rightarrow> o" (infixr "o-o" 45) |
49 where "P o-o Q == (P -o Q) >< (Q -o P)" |
49 where "P o-o Q == (P -o Q) >< (Q -o P)" |
50 |
50 |
269 apply best |
269 apply best |
270 done |
270 done |
271 |
271 |
272 ML \<open> |
272 ML \<open> |
273 val safe_pack = |
273 val safe_pack = |
274 @{context} |
274 \<^context> |
275 |> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1 |
275 |> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1 |
276 contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule} |
276 contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule} |
277 |> Cla.add_unsafe @{thm aux_impl} |
277 |> Cla.add_unsafe @{thm aux_impl} |
278 |> Cla.get_pack; |
278 |> Cla.get_pack; |
279 |
279 |
280 val power_pack = |
280 val power_pack = |
281 Cla.put_pack safe_pack @{context} |
281 Cla.put_pack safe_pack \<^context> |
282 |> Cla.add_unsafe @{thm impr_contr_der} |
282 |> Cla.add_unsafe @{thm impr_contr_der} |
283 |> Cla.get_pack; |
283 |> Cla.get_pack; |
284 \<close> |
284 \<close> |
285 |
285 |
286 method_setup best_safe = |
286 method_setup best_safe = |