# HG changeset patch # User blanchet # Date 1314018165 -7200 # Node ID 15160cdc46885ba90502806651118c1944ced9d7 # Parent f0bc74b9161e609fe93677a1191b6fff2c91c41a precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis diff -r f0bc74b9161e -r 15160cdc4688 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 @@ -42,7 +42,6 @@ val hybridN : string val lambdasN : string val smartN : string - val bound_var_prefix : string val schematic_var_prefix : string val fixed_var_prefix : string val tvar_prefix : string @@ -134,6 +133,8 @@ val simpN = "simp" val bound_var_prefix = "B_" +val all_bound_var_prefix = "BA_" +val exist_bound_var_prefix = "BE_" val schematic_var_prefix = "V_" val fixed_var_prefix = "v_" val tvar_prefix = "T_" @@ -297,6 +298,8 @@ | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i fun make_bound_var x = bound_var_prefix ^ ascii_of x +fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x +fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v fun make_fixed_var x = fixed_var_prefix ^ ascii_of x @@ -505,16 +508,14 @@ else IVar ((make_schematic_var v, s), T), atyps_of T) | iterm_from_term _ bs (Bound j) = - nth bs j |> (fn (s, T) => (IConst (`make_bound_var s, T, []), atyps_of T)) + nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T)) | iterm_from_term thy bs (Abs (s, T, t)) = let fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string val s = vary s - val (tm, atomic_Ts) = iterm_from_term thy ((s, T) :: bs) t - in - (IAbs ((`make_bound_var s, T), tm), - union (op =) atomic_Ts (atyps_of T)) - end + val name = `make_bound_var s + val (tm, atomic_Ts) = iterm_from_term thy ((s, (name, T)) :: bs) t + in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end datatype locality = General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | @@ -901,26 +902,35 @@ iterm_from_term thy bs (Envir.eta_contract t) |>> (introduce_proxies type_enc #> AAtom) ||> union (op =) atomic_types - fun do_quant bs q s T t' = - let val s = singleton (Name.variant_list (map fst bs)) s in - do_formula ((s, T) :: bs) t' - #>> mk_aquant q [(`make_bound_var s, SOME T)] + fun do_quant bs q pos s T t' = + let + val s = singleton (Name.variant_list (map fst bs)) s + val universal = Option.map (q = AExists ? not) pos + val name = + s |> `(case universal of + SOME true => make_all_bound_var + | SOME false => make_exist_bound_var + | NONE => make_bound_var) + in + do_formula ((s, (name, T)) :: bs) pos t' + #>> mk_aquant q [(name, SOME T)] end - and do_conn bs c t1 t2 = - do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c) - and do_formula bs t = + and do_conn bs c pos1 t1 pos2 t2 = + do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c) + and do_formula bs pos t = case t of - @{const Trueprop} $ t1 => do_formula bs t1 - | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot + @{const Trueprop} $ t1 => do_formula bs pos t1 + | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot | Const (@{const_name All}, _) $ Abs (s, T, t') => - do_quant bs AForall s T t' + do_quant bs AForall pos s T t' | Const (@{const_name Ex}, _) $ Abs (s, T, t') => - do_quant bs AExists s T t' - | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 - | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 - | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 + do_quant bs AExists pos s T t' + | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2 + | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2 + | @{const HOL.implies} $ t1 $ t2 => + do_conn bs AImplies (Option.map not pos) t1 pos t2 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => - if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t + if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t | _ => do_term bs t in do_formula [] end @@ -1043,7 +1053,7 @@ fun make_formula thy type_enc eq_as_iff name loc kind t = let val (iformula, atomic_types) = - iformula_from_prop thy type_enc eq_as_iff t [] + iformula_from_prop thy type_enc eq_as_iff (SOME (kind <> Conjecture)) t [] in {name = name, locality = loc, kind = kind, iformula = iformula, atomic_types = atomic_types} @@ -1118,10 +1128,11 @@ should_encode_type ctxt mono level T | should_guard_type _ _ _ _ _ = false -fun is_var_or_bound_var (IConst ((s, _), _, _)) = - String.isPrefix bound_var_prefix s - | is_var_or_bound_var (IVar _) = true - | is_var_or_bound_var _ = false +fun is_maybe_universal_var (IConst ((s, _), _, _)) = + String.isPrefix bound_var_prefix s orelse + String.isPrefix all_bound_var_prefix s + | is_maybe_universal_var (IVar _) = true + | is_maybe_universal_var _ = false datatype tag_site = Top_Level of bool option | @@ -1133,7 +1144,7 @@ (case uniformity of Uniform => should_encode_type ctxt mono level T | Nonuniform => - case (site, is_var_or_bound_var u) of + case (site, is_maybe_universal_var u) of (Eq_Arg _, true) => should_encode_type ctxt mono level T | _ => false) | should_tag_with_type _ _ _ _ _ _ = false @@ -1163,7 +1174,7 @@ else iter (ary + 1) (range_type T) in iter 0 const_T end - fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) = + fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) = if explicit_apply = NONE andalso (can dest_funT T orelse T = @{typ bool}) then let @@ -1187,8 +1198,9 @@ let val (head, args) = strip_iterm_comb tm in (case head of IConst ((s, _), T, _) => - if String.isPrefix bound_var_prefix s then - add_var_or_bound_var T accum + if String.isPrefix bound_var_prefix s orelse + String.isPrefix all_bound_var_prefix s then + add_universal_var T accum else let val ary = length args in ((bool_vars, fun_var_Ts), @@ -1226,8 +1238,8 @@ sym_tab end) end - | IVar (_, T) => add_var_or_bound_var T accum - | IAbs ((_, T), tm) => accum |> add_var_or_bound_var T |> add false tm + | IVar (_, T) => add_universal_var T accum + | IAbs ((_, T), tm) => accum |> add_universal_var T |> add false tm | _ => accum) |> fold (add false) args end @@ -1574,9 +1586,10 @@ | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) | is_var_positively_naked_in_term _ _ _ _ = true -fun should_guard_var_in_formula pos phi (SOME true) name = + +fun should_guard_var_in_formula _ _ (SOME false) _ = false + | should_guard_var_in_formula pos phi _ name = formula_fold pos (is_var_positively_naked_in_term name) phi false - | should_guard_var_in_formula _ _ _ _ = true fun mk_aterm format type_enc name T_args args = ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args) @@ -1728,10 +1741,12 @@ (** Symbol declarations **) fun should_declare_sym type_enc pred_sym s = - is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso (case type_enc of Guards _ => not pred_sym - | _ => true) + | _ => true) andalso + is_tptp_user_symbol s andalso + forall (fn prefix => not (String.isPrefix prefix s)) + [bound_var_prefix, all_bound_var_prefix, exist_bound_var_prefix] fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab (conjs, facts) = @@ -1799,7 +1814,7 @@ (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) = - if is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] then + if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then case level of Noninf_Nonmono_Types soundness => if exists (type_instance ctxt T) surely_infinite_Ts orelse @@ -1849,7 +1864,6 @@ ? fold (add_fact_mononotonicity_info ctxt level) facts end -(* FIXME: do the right thing for existentials! *) fun formula_line_for_guards_mono_type ctxt format mono type_enc T = Formula (guards_sym_formula_prefix ^ ascii_of (mangled_type format type_enc T),