src/HOL/Tools/ATP/atp_problem_generate.ML
 changeset 46377 dce6c3a460a9 parent 46375 d724066ff3d0 child 46379 de5dd84717c1
equal inserted replaced
46376:110ba6344446 46377:dce6c3a460a9
`  1234                          name stature Axiom of`
`  1234                          name stature Axiom of`
`  1235     formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>`
`  1235     formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>`
`  1236     if s = tptp_true then NONE else SOME formula`
`  1236     if s = tptp_true then NONE else SOME formula`
`  1237   | formula => SOME formula`
`  1237   | formula => SOME formula`
`  1238 `
`  1238 `
`  1239 fun s_not_trueprop (@{const Trueprop} \$ t) = @{const Trueprop} \$ s_not t`
`  1239 fun not_trueprop (@{const Trueprop} \$ t) =`
`  1240   | s_not_trueprop t =`
`  1240     @{const Trueprop} \$ (@{const Not} \$ t)`
`  1241     if fastype_of t = @{typ bool} then s_not t else @{prop False} (* too meta *)`
`  1241   | not_trueprop t =`
`       `
`  1242     if fastype_of t = @{typ bool} then @{const Not} \$ t`
`       `
`  1243     else @{prop False} (* "t" is too meta *)`
`  1242 `
`  1244 `
`  1243 fun make_conjecture ctxt format type_enc =`
`  1245 fun make_conjecture ctxt format type_enc =`
`  1244   map (fn ((name, stature), (kind, t)) =>`
`  1246   map (fn ((name, stature), (kind, t)) =>`
`  1245           t |> kind = Conjecture ? s_not_trueprop`
`  1247           t |> kind = Conjecture ? not_trueprop`
`  1246             |> make_formula ctxt format type_enc (format <> CNF) name stature`
`  1248             |> make_formula ctxt format type_enc (format <> CNF) name stature`
`  1247                             kind)`
`  1249                             kind)`
`  1248 `
`  1250 `
`  1249 (** Finite and infinite type inference **)`
`  1251 (** Finite and infinite type inference **)`
`  1250 `
`  1252 `
`  1727     val hyp_ts =`
`  1729     val hyp_ts =`
`  1728       hyp_ts`
`  1730       hyp_ts`
`  1729       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)`
`  1731       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)`
`  1730     val facts = facts |> map (apsnd (pair Axiom))`
`  1732     val facts = facts |> map (apsnd (pair Axiom))`
`  1731     val conjs =`
`  1733     val conjs =`
`  1732       map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]`
`  1734       map (pair prem_kind) hyp_ts @ [(Conjecture, not_trueprop concl_t)]`
`  1733       |> map (apsnd freeze_term)`
`  1735       |> map (apsnd freeze_term)`
`  1734       |> map2 (pair o rpair (Local, General) o string_of_int)`
`  1736       |> map2 (pair o rpair (Local, General) o string_of_int)`
`  1735               (0 upto length hyp_ts)`
`  1737               (0 upto length hyp_ts)`
`  1736     val ((conjs, facts), lam_facts) =`
`  1738     val ((conjs, facts), lam_facts) =`
`  1737       (conjs, facts)`
`  1739       (conjs, facts)`