402 end |
402 end |
403 |
403 |
404 (* These are ignored anyway by the relevance filter (unless they appear in |
404 (* These are ignored anyway by the relevance filter (unless they appear in |
405 higher-order places) but not by the monomorphizer. *) |
405 higher-order places) but not by the monomorphizer. *) |
406 val atp_logical_consts = |
406 val atp_logical_consts = |
407 [@{const_name Pure.prop}, @{const_name Pure.conjunction}, @{const_name all}, @{const_name "==>"}, |
407 [@{const_name Pure.prop}, @{const_name Pure.conjunction}, |
408 @{const_name "=="}, @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, |
408 @{const_name Pure.all}, @{const_name Pure.imp}, @{const_name Pure.eq}, |
|
409 @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, |
409 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] |
410 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] |
410 |
411 |
411 (* These are either simplified away by "Meson.presimplify" (most of the time) or |
412 (* These are either simplified away by "Meson.presimplify" (most of the time) or |
412 handled specially via "fFalse", "fTrue", ..., "fequal". *) |
413 handled specially via "fFalse", "fTrue", ..., "fequal". *) |
413 val atp_irrelevant_consts = |
414 val atp_irrelevant_consts = |
1877 fact :: reorder [] (facts @ skipped) |
1878 fact :: reorder [] (facts @ skipped) |
1878 end |
1879 end |
1879 in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end |
1880 in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end |
1880 |
1881 |
1881 fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t |
1882 fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t |
1882 | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t |
1883 | s_not_prop (@{const Pure.imp} $ t $ @{prop False}) = t |
1883 | s_not_prop t = @{const "==>"} $ t $ @{prop False} |
1884 | s_not_prop t = @{const Pure.imp} $ t $ @{prop False} |
1884 |
1885 |
1885 fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts |
1886 fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts |
1886 concl_t facts = |
1887 concl_t facts = |
1887 let |
1888 let |
1888 val thy = Proof_Context.theory_of ctxt |
1889 val thy = Proof_Context.theory_of ctxt |