# HG changeset patch # User blanchet # Date 1282458619 -7200 # Node ID 2479d541bc6101b69694cf3d4c154adcafcdb72c # Parent 0170e0dc5f9607c4557cbdaf8793dda4e47eeda3# Parent 3387432c18af5ab2a53e98d395aff16c385053c2 merged diff -r 0170e0dc5f96 -r 2479d541bc61 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Sun Aug 22 14:01:25 2010 +0800 +++ b/src/HOL/Auth/NS_Shared.thy Sun Aug 22 08:30:19 2010 +0200 @@ -5,7 +5,7 @@ header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*} -theory NS_Shared imports Sledgehammer2d(*###*) Public begin +theory NS_Shared imports Public begin text{* From page 247 of @@ -311,8 +311,6 @@ Crypt K (Nonce NB) \ parts (spies evs) \ Says B A (Crypt K (Nonce NB)) \ set evs" apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) -sledgehammer [atp = e, overlord] (Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E) -apply (metis Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E) apply (analz_mono_contra, simp_all, blast) txt{*NS2: contradiction from the assumptions @{term "Key K \ used evs2"} and @{term "Crypt K (Nonce NB) \ parts (spies evs2)"} *} diff -r 0170e0dc5f96 -r 2479d541bc61 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Aug 22 14:01:25 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Aug 22 08:30:19 2010 +0200 @@ -43,7 +43,7 @@ val name = Facts.string_of_ref xref |> forall (member Thm.eq_thm chained_ths) ths ? prefix chained_prefix - in (name, ths) end + in (name, ths |> map Clausifier.transform_elim_theorem) end (***************************************************************) @@ -433,13 +433,73 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) -fun is_theorem_bad_for_atps thm = +(**** Predicates to detect unwanted facts (prolific or likely to cause + unsoundness) ****) + +(* Too general means, positive equality literal with a variable X as one + operand, when X does not occur properly in the other operand. This rules out + clearly inconsistent facts such as X = a | X = b, though it by no means + guarantees soundness. *) + +(* Unwanted equalities are those between a (bound or schematic) variable that + does not properly occur in the second operand. *) +val is_exhaustive_finite = + let + fun is_bad_equal (Var z) t = + not (exists_subterm (fn Var z' => z = z' | _ => false) t) + | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) + | is_bad_equal _ _ = false + fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 + fun do_formula pos t = + case (pos, t) of + (_, @{const Trueprop} $ t1) => do_formula pos t1 + | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => + do_formula pos t' + | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => + do_formula pos t' + | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => + do_formula pos t' + | (_, @{const "==>"} $ t1 $ t2) => + do_formula (not pos) t1 andalso + (t2 = @{prop False} orelse do_formula pos t2) + | (_, @{const "op -->"} $ t1 $ t2) => + do_formula (not pos) t1 andalso + (t2 = @{const False} orelse do_formula pos t2) + | (_, @{const Not} $ t1) => do_formula (not pos) t1 + | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2] + | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2] + | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2 + | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 + | _ => false + in do_formula true end + +fun has_bound_or_var_of_type tycons = + exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s + | Abs (_, Type (s, _), _) => member (op =) tycons s + | _ => false) + +(* Facts are forbidden to contain variables of these types. The typical reason + is that they lead to unsoundness. Note that "unit" satisfies numerous + equations like "?x = ()". The resulting clauses will have no type constraint, + yielding false proofs. Even "bool" leads to many unsound proofs, though only + for higher-order problems. *) +val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}]; + +(* Facts containing variables of type "unit" or "bool" or of the form + "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types + are omitted. *) +fun is_dangerous_term full_types t = + not full_types andalso + (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t) + +fun is_theorem_bad_for_atps full_types thm = let val t = prop_of thm in is_formula_too_complex t orelse exists_type type_has_top_sort t orelse - exists_sledgehammer_const t orelse is_strange_thm thm + is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse + is_strange_thm thm end -fun all_name_thms_pairs ctxt add_thms chained_ths = +fun all_name_thms_pairs ctxt full_types add_thms chained_ths = let val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); val local_facts = ProofContext.facts_of ctxt; @@ -462,8 +522,10 @@ | SOME ths1 => Thm.eq_thms (ths0, ths1)) val name1 = Facts.extern facts name; val name2 = Name_Space.extern full_space name; - val ths = filter (fn th => not (is_theorem_bad_for_atps th) orelse - member Thm.eq_thm add_thms th) ths0 + val ths = + ths0 |> map Clausifier.transform_elim_theorem + |> filter ((not o is_theorem_bad_for_atps full_types) orf + member Thm.eq_thm add_thms) in case find_first check_thms [name1, name2, name] of NONE => I @@ -505,68 +567,6 @@ (* ATP invocation methods setup *) (***************************************************************) -(**** Predicates to detect unwanted facts (prolific or likely to cause - unsoundness) ****) - -(* Too general means, positive equality literal with a variable X as one - operand, when X does not occur properly in the other operand. This rules out - clearly inconsistent facts such as X = a | X = b, though it by no means - guarantees soundness. *) - -(* Unwanted equalities are those between a (bound or schematic) variable that - does not properly occur in the second operand. *) -fun too_general_eqterms (Var z) t = - not (exists_subterm (fn Var z' => z = z' | _ => false) t) - | too_general_eqterms (Bound j) t = not (loose_bvar1 (t, j)) - | too_general_eqterms _ _ = false - -val is_exhaustive_finite = - let - fun do_equals t1 t2 = - too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1 - fun do_formula pos t = - case (pos, t) of - (_, @{const Trueprop} $ t1) => do_formula pos t1 - | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => - do_formula pos t' - | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => - do_formula pos t' - | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => - do_formula pos t' - | (_, @{const "==>"} $ t1 $ t2) => - do_formula (not pos) t1 andalso do_formula pos t2 - | (_, @{const "op -->"} $ t1 $ t2) => - do_formula (not pos) t1 andalso do_formula pos t2 - | (_, @{const Not} $ t1) => do_formula (not pos) t1 - | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2] - | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2] - | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2 - | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2 - | (_, @{const False}) => true - | (_, @{const True}) => true - | _ => false - in do_formula true end - - -fun has_bound_or_var_of_type tycons = - exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s - | Abs (_, Type (s, _), _) => member (op =) tycons s - | _ => false) - -(* Facts are forbidden to contain variables of these types. The typical reason - is that they lead to unsoundness. Note that "unit" satisfies numerous - equations like "?x = ()". The resulting clauses will have no type constraint, - yielding false proofs. Even "bool" leads to many unsound proofs, though only - for higher-order problems. *) -val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}]; - -(* Facts containing variables of type "unit" or "bool" or of the form - "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types - are omitted. *) -fun is_dangerous_term full_types t = - not full_types andalso - (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t) - fun relevant_facts full_types relevance_threshold relevance_convergence defs_relevant max_new theory_relevant (relevance_override as {add, del, only}) @@ -576,11 +576,8 @@ val axioms = checked_name_thm_pairs (respect_no_atp andalso not only) ctxt (if only then map (name_thms_pair_from_ref ctxt chained_ths) add - else all_name_thms_pairs ctxt add_thms chained_ths) + else all_name_thms_pairs ctxt full_types add_thms chained_ths) |> make_unique - |> map (apsnd Clausifier.transform_elim_theorem) - |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse - not (is_dangerous_term full_types (prop_of th))) in relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override