ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
authorblanchet
Sun Mar 04 23:20:43 2012 +0100 (2012-03-04)
changeset 468182a28e66e2e4c
parent 46817 90c8620852cf
child 46819 9b38f8527510
ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/Meson/meson.ML
     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.227            case head of
   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
     2.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Mar 04 23:04:40 2012 +0100
     2.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Mar 04 23:20:43 2012 +0100
     2.3 @@ -26,7 +26,6 @@
     2.4    val skolemize : Proof.context -> thm -> thm
     2.5    val extensionalize_conv : Proof.context -> conv
     2.6    val extensionalize_theorem : Proof.context -> thm -> thm
     2.7 -  val is_fol_term: theory -> term -> bool
     2.8    val make_clauses_unsorted: Proof.context -> thm list -> thm list
     2.9    val make_clauses: Proof.context -> thm list -> thm list
    2.10    val make_horns: thm list -> thm list
    2.11 @@ -457,17 +456,6 @@
    2.12        [] => false (*not a function type, OK*)
    2.13      | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
    2.14  
    2.15 -(* Returns false if any Vars in the theorem mention type bool.
    2.16 -   Also rejects functions whose arguments are Booleans or other functions. *)
    2.17 -fun is_fol_term thy t =
    2.18 -    Term.is_first_order [@{const_name all}, @{const_name All},
    2.19 -                         @{const_name Ex}] t andalso
    2.20 -    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
    2.21 -                          | _ => false) t orelse
    2.22 -         has_bool_arg_const t orelse
    2.23 -         exists_Const (higher_inst_const thy) t orelse
    2.24 -         has_meta_conn t);
    2.25 -
    2.26  fun rigid t = not (is_Var (head_of t));
    2.27  
    2.28  fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t