src/HOL/Tools/ATP/atp_problem_generate.ML
 changeset 46818 2a28e66e2e4c parent 46711 f745bcc4a1e5 child 47030 7e80e14247fc
```     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Mar 04 23:04:40 2012 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Mar 04 23:20:43 2012 +0100
1.3 @@ -693,6 +693,79 @@
1.4      (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
1.5    | adjust_type_enc _ type_enc = type_enc
1.6
1.7 +fun is_fol_term t =
1.8 +  case t of
1.9 +    @{const Not} \$ t1 => is_fol_term t1
1.10 +  | Const (@{const_name All}, _) \$ Abs (_, _, t') => is_fol_term t'
1.11 +  | Const (@{const_name All}, _) \$ t1 => is_fol_term t1
1.12 +  | Const (@{const_name Ex}, _) \$ Abs (_, _, t') => is_fol_term t'
1.13 +  | Const (@{const_name Ex}, _) \$ t1 => is_fol_term t1
1.14 +  | @{const HOL.conj} \$ t1 \$ t2 => is_fol_term t1 andalso is_fol_term t2
1.15 +  | @{const HOL.disj} \$ t1 \$ t2 => is_fol_term t1 andalso is_fol_term t2
1.16 +  | @{const HOL.implies} \$ t1 \$ t2 => is_fol_term t1 andalso is_fol_term t2
1.17 +  | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) \$ t1 \$ t2 =>
1.18 +    is_fol_term t1 andalso is_fol_term t2
1.19 +  | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)
1.20 +
1.21 +fun simple_translate_lambdas do_lambdas ctxt t =
1.22 +  if is_fol_term t then
1.23 +    t
1.24 +  else
1.25 +    let
1.26 +      fun trans Ts t =
1.27 +        case t of
1.28 +          @{const Not} \$ t1 => @{const Not} \$ trans Ts t1
1.29 +        | (t0 as Const (@{const_name All}, _)) \$ Abs (s, T, t') =>
1.30 +          t0 \$ Abs (s, T, trans (T :: Ts) t')
1.31 +        | (t0 as Const (@{const_name All}, _)) \$ t1 =>
1.32 +          trans Ts (t0 \$ eta_expand Ts t1 1)
1.33 +        | (t0 as Const (@{const_name Ex}, _)) \$ Abs (s, T, t') =>
1.34 +          t0 \$ Abs (s, T, trans (T :: Ts) t')
1.35 +        | (t0 as Const (@{const_name Ex}, _)) \$ t1 =>
1.36 +          trans Ts (t0 \$ eta_expand Ts t1 1)
1.37 +        | (t0 as @{const HOL.conj}) \$ t1 \$ t2 =>
1.38 +          t0 \$ trans Ts t1 \$ trans Ts t2
1.39 +        | (t0 as @{const HOL.disj}) \$ t1 \$ t2 =>
1.40 +          t0 \$ trans Ts t1 \$ trans Ts t2
1.41 +        | (t0 as @{const HOL.implies}) \$ t1 \$ t2 =>
1.42 +          t0 \$ trans Ts t1 \$ trans Ts t2
1.43 +        | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1.44 +            \$ t1 \$ t2 =>
1.45 +          t0 \$ trans Ts t1 \$ trans Ts t2
1.46 +        | _ =>
1.47 +          if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1.48 +          else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1.49 +      val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1.50 +    in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
1.51 +
1.52 +fun do_cheaply_conceal_lambdas Ts (t1 \$ t2) =
1.53 +    do_cheaply_conceal_lambdas Ts t1
1.54 +    \$ do_cheaply_conceal_lambdas Ts t2
1.55 +  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
1.56 +    Const (lam_lifted_poly_prefix ^ serial_string (),
1.57 +           T --> fastype_of1 (T :: Ts, t))
1.58 +  | do_cheaply_conceal_lambdas _ t = t
1.59 +
1.60 +fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
1.61 +fun conceal_bounds Ts t =
1.62 +  subst_bounds (map (Free o apfst concealed_bound_name)
1.63 +                    (0 upto length Ts - 1 ~~ Ts), t)
1.64 +fun reveal_bounds Ts =
1.65 +  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
1.66 +                    (0 upto length Ts - 1 ~~ Ts))
1.67 +
1.68 +fun do_introduce_combinators ctxt Ts t =
1.69 +  let val thy = Proof_Context.theory_of ctxt in
1.70 +    t |> conceal_bounds Ts
1.71 +      |> cterm_of thy
1.72 +      |> Meson_Clausify.introduce_combinators_in_cterm
1.73 +      |> prop_of |> Logic.dest_equals |> snd
1.74 +      |> reveal_bounds Ts
1.75 +  end
1.76 +  (* A type variable of sort "{}" will make abstraction fail. *)
1.77 +  handle THM _ => t |> do_cheaply_conceal_lambdas Ts
1.78 +val introduce_combinators = simple_translate_lambdas do_introduce_combinators
1.79 +
1.80  fun constify_lifted (t \$ u) = constify_lifted t \$ constify_lifted u
1.81    | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
1.82    | constify_lifted (Free (x as (s, _))) =
1.83 @@ -720,10 +793,17 @@
1.84                      lam_lifted_mono_prefix) ^ "_a"))
1.85            Lambda_Lifting.is_quantifier
1.86    #> fst
1.87 -fun lift_lams_part_2 (facts, lifted) =
1.88 -  (map (open_form (unprefix close_form_prefix) o constify_lifted) facts,
1.89 -   map (open_form I o constify_lifted) lifted)
1.90 -val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
1.91 +
1.92 +fun lift_lams_part_2 ctxt (facts, lifted) =
1.93 +  (facts, lifted)
1.94 +  (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid
1.95 +     of them *)
1.96 +  |> pairself (map (introduce_combinators ctxt))
1.97 +  |> pairself (map constify_lifted)
1.98 +  |>> map (open_form (unprefix close_form_prefix))
1.99 +  ||> map (open_form I)
1.100 +
1.101 +fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
1.102
1.103  fun intentionalize_def (Const (@{const_name All}, _) \$ Abs (_, _, t)) =
1.104      intentionalize_def t
1.105 @@ -1133,14 +1213,6 @@
1.106            #> Meson.presimplify
1.107            #> prop_of)
1.108
1.109 -fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
1.110 -fun conceal_bounds Ts t =
1.111 -  subst_bounds (map (Free o apfst concealed_bound_name)
1.112 -                    (0 upto length Ts - 1 ~~ Ts), t)
1.113 -fun reveal_bounds Ts =
1.114 -  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
1.115 -                    (0 upto length Ts - 1 ~~ Ts))
1.116 -
1.117  fun is_fun_equality (@{const_name HOL.eq},
1.118                       Type (_, [Type (@{type_name fun}, _), _])) = true
1.119    | is_fun_equality _ = false
1.120 @@ -1154,59 +1226,6 @@
1.121    else
1.122      t
1.123
1.124 -fun simple_translate_lambdas do_lambdas ctxt t =
1.125 -  let val thy = Proof_Context.theory_of ctxt in
1.126 -    if Meson.is_fol_term thy t then
1.127 -      t
1.128 -    else
1.129 -      let
1.130 -        fun trans Ts t =
1.131 -          case t of
1.132 -            @{const Not} \$ t1 => @{const Not} \$ trans Ts t1
1.133 -          | (t0 as Const (@{const_name All}, _)) \$ Abs (s, T, t') =>
1.134 -            t0 \$ Abs (s, T, trans (T :: Ts) t')
1.135 -          | (t0 as Const (@{const_name All}, _)) \$ t1 =>
1.136 -            trans Ts (t0 \$ eta_expand Ts t1 1)
1.137 -          | (t0 as Const (@{const_name Ex}, _)) \$ Abs (s, T, t') =>
1.138 -            t0 \$ Abs (s, T, trans (T :: Ts) t')
1.139 -          | (t0 as Const (@{const_name Ex}, _)) \$ t1 =>
1.140 -            trans Ts (t0 \$ eta_expand Ts t1 1)
1.141 -          | (t0 as @{const HOL.conj}) \$ t1 \$ t2 =>
1.142 -            t0 \$ trans Ts t1 \$ trans Ts t2
1.143 -          | (t0 as @{const HOL.disj}) \$ t1 \$ t2 =>
1.144 -            t0 \$ trans Ts t1 \$ trans Ts t2
1.145 -          | (t0 as @{const HOL.implies}) \$ t1 \$ t2 =>
1.146 -            t0 \$ trans Ts t1 \$ trans Ts t2
1.147 -          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1.148 -              \$ t1 \$ t2 =>
1.149 -            t0 \$ trans Ts t1 \$ trans Ts t2
1.150 -          | _ =>
1.151 -            if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1.152 -            else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1.153 -        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1.154 -      in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
1.155 -  end
1.156 -
1.157 -fun do_cheaply_conceal_lambdas Ts (t1 \$ t2) =
1.158 -    do_cheaply_conceal_lambdas Ts t1
1.159 -    \$ do_cheaply_conceal_lambdas Ts t2
1.160 -  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
1.161 -    Const (lam_lifted_poly_prefix ^ serial_string (),
1.162 -           T --> fastype_of1 (T :: Ts, t))
1.163 -  | do_cheaply_conceal_lambdas _ t = t
1.164 -
1.165 -fun do_introduce_combinators ctxt Ts t =
1.166 -  let val thy = Proof_Context.theory_of ctxt in
1.167 -    t |> conceal_bounds Ts
1.168 -      |> cterm_of thy
1.169 -      |> Meson_Clausify.introduce_combinators_in_cterm
1.170 -      |> prop_of |> Logic.dest_equals |> snd
1.171 -      |> reveal_bounds Ts
1.172 -  end
1.173 -  (* A type variable of sort "{}" will make abstraction fail. *)
1.174 -  handle THM _ => t |> do_cheaply_conceal_lambdas Ts
1.175 -val introduce_combinators = simple_translate_lambdas do_introduce_combinators
1.176 -
1.177  fun preprocess_abstractions_in_terms trans_lams facts =
1.178    let
1.179      val (facts, lambda_ts) =
1.180 @@ -1230,6 +1249,8 @@
1.181        | freeze t = t
1.182    in t |> exists_subterm is_Var t ? freeze end
1.183
1.184 +fun default_formula role = if role = Conjecture then @{term False} else @{term True}
1.185 +
1.186  fun presimp_prop ctxt role t =
1.187    (let
1.188       val thy = Proof_Context.theory_of ctxt
1.189 @@ -1243,7 +1264,7 @@
1.190         |> presimplify_term ctxt
1.191         |> HOLogic.dest_Trueprop
1.192     end
1.193 -   handle TERM _ => if role = Conjecture then @{term False} else @{term True})
1.194 +   handle TERM _ => default_formula role)
1.195    |> pair role
1.196
1.197  fun make_formula ctxt format type_enc eq_as_iff name stature kind t =
1.198 @@ -1765,13 +1786,13 @@
1.199    else if lam_trans = combs_and_liftingN then
1.200      lift_lams_part_1 ctxt type_enc
1.201      ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
1.202 -    #> lift_lams_part_2
1.203 +    #> lift_lams_part_2 ctxt
1.204    else if lam_trans = combs_or_liftingN then
1.205      lift_lams_part_1 ctxt type_enc
1.206      ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
1.207                         @{term "op =::bool => bool => bool"} => t
1.208                       | _ => introduce_combinators ctxt (intentionalize_def t))
1.209 -    #> lift_lams_part_2
1.210 +    #> lift_lams_part_2 ctxt
1.211    else if lam_trans = keep_lamsN then
1.212      map (Envir.eta_contract) #> rpair []
1.213    else
1.214 @@ -1867,8 +1888,8 @@
1.215       | Positively_Naked_Vars =>
1.216         formula_fold pos (is_var_positively_naked_in_term name) phi false
1.217       | Ghost_Type_Arg_Vars =>
1.218 -       formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name)
1.219 -                    phi false)
1.220 +       formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name) phi
1.221 +                    false)
1.222    | should_guard_var_in_formula _ _ _ _ _ _ _ = true
1.223
1.224  fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
1.225 @@ -1908,16 +1929,20 @@
1.226          val t =
1.228              IConst (name as (s, _), _, T_args) =>
1.229 -            let
1.230 -              val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1.231 -            in
1.232 +            let val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere in
1.233                map (term arg_site) args |> mk_aterm format type_enc name T_args
1.234              end
1.235            | IVar (name, _) =>
1.236              map (term Elsewhere) args |> mk_aterm format type_enc name []
1.237            | IAbs ((name, T), tm) =>
1.238 -            AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1.239 -                  term Elsewhere tm)
1.240 +            if is_type_enc_higher_order type_enc then
1.241 +              AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1.242 +                    term Elsewhere tm)
1.243 +            else
1.244 +              ATerm (("LAMBDA", "LAMBDA"), []) (*###*)
1.245 +(*###
1.246 +              raise Fail "unexpected lambda-abstraction"
1.247 +*)
1.248            | IApp _ => raise Fail "impossible \"IApp\""
1.249          val T = ityp_of u
1.250        in
```