diff --git a/Abduction/Abduction.thy b/Abduction/Abduction.thy index 8e31c38c..8768f762 100644 --- a/Abduction/Abduction.thy +++ b/Abduction/Abduction.thy @@ -115,5 +115,7 @@ val _ = theorem \<^command_keyword>\prove\ "prove"; end; \ +ML\ +\ end \ No newline at end of file diff --git a/Abduction/Abduction_Graph.ML b/Abduction/Abduction_Graph.ML index 70cf9b7c..55546fe0 100644 --- a/Abduction/Abduction_Graph.ML +++ b/Abduction/Abduction_Graph.ML @@ -359,7 +359,7 @@ fun print_lemma_and_proof_of_key (ctxt:Proof.context) (graph:abduction_graph) (k (* print_proof_of_graph *) fun print_proof_of_graph (pst:Proof.state) (graph:abduction_graph) = let - val keys = PGraph.keys graph |> filter is_ornode |> rev : keys; + val keys = keys graph |> filter is_ornode |> rev : keys; val key_prf_id_pairs = map (fn key => (key, proof_id_of graph key)) keys : (key * int option) list; val key_prf_id_pairs_solved_only = filter (fn (_, id) => is_some id) key_prf_id_pairs : (key * int option) list; val key_prf_id_pairs_wo_opt = map (apsnd the) key_prf_id_pairs_solved_only : (key * int) list; diff --git a/Abduction/All_Top_Down_Conjecturing.ML b/Abduction/All_Top_Down_Conjecturing.ML index f4fa3275..22a82e30 100644 --- a/Abduction/All_Top_Down_Conjecturing.ML +++ b/Abduction/All_Top_Down_Conjecturing.ML @@ -6,7 +6,7 @@ * Huawei Technologies Research & Development (UK) Limited. *) (*** structure All_Top_Down_Conjecturing ***) -structure All_Top_Down_Conjecturing: TOP_DOWN_CONJECTURING = +structure All_Top_Down_Conjecturing(*: TOP_DOWN_CONJECTURING*) = struct fun is_composite trm = Isabelle_Utils.is_Abs trm orelse Isabelle_Utils.is_App trm: bool; @@ -62,8 +62,10 @@ fun template_conjectures (ctxt:Proof.context) (trm:term): (string * term) list = structure S4TD = SeLFiE_For_Top_Down; structure SS = Shared_State; +structure AG = Abduction_Graph; -fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.state) trm = +fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.state) + (agraph:AG.abduction_graph) (trm:term) = let val ctxt = Proof.context_of pst: Proof.context; fun tracing' mssg = ()(*tracing mssg*); @@ -91,6 +93,7 @@ fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.st |> parallel_filter (fn (_, trm) => S4TD.run_assertion pst trm S4TD.does_not_have_trivial_equality) |> parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.nested_eq) |> parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.var_appears_many_times_but_always_in_the_same_subtrm) + |> map (fn (_, term) => (SS.get_lemma_name term2name ctxt term, term)); val _ = tracing' "[[[[[[[[[[[top_down_conjecture ends]]]]]]]]]]": unit; in diff --git a/Abduction/Proof_By_Abduction.ML b/Abduction/Proof_By_Abduction.ML index 9c412b36..62c29830 100644 --- a/Abduction/Proof_By_Abduction.ML +++ b/Abduction/Proof_By_Abduction.ML @@ -23,6 +23,8 @@ open Abduction_Graph; structure SOOE = Seed_Of_Or2And_Edge; structure SS = Shared_State; +structure AG = Abduction_Graph; +structure TDU = Top_Down_Util; (** functions to expand ornode leaves **) @@ -59,9 +61,62 @@ fun expand_ornode_if_original_goral_is_unproved let val _ = tracing' "We did NOT prove the or-node."; (*top-down explicit conjecturing*) - val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures term2name pst lemma_term : (string * term) list; + val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures term2name pst graph lemma_term : (string * term) list; val filtered_explicit = filter_out (SOOE.condition_to_filter_out_cnjctr lemma_term refutation pst graph false o snd) explicit_conjectures: (string * term) list; val explicit_wo_counterexample = filter_out (Shared_State.is_refuted refutation pst o snd) filtered_explicit : (string * term) list; + +(*TODO: I should apply simplification using proved lemmas here not in top_down_conjectures.*) +(* + val agraph = Synchronized.value synched_agraph; + val ctxt = Proof.context_of pst + fun is_already_in_graph (simplified:term) = + let + val orkey = (Abduction_Graph.Or_N, [simplified]): AG.key; + val already_exists = try (Abduction_Graph.PGraph.get_node agraph) orkey |> is_some; + val is_True = simplified = @{term True}; + val _ = if already_exists then tracing ("already_exists: " ^ Isabelle_Utils.trm_to_string ctxt simplified) else (); + in + already_exists orelse is_True + end: bool; + val keys = AG.keys agraph: AG.keys; + val orkeys = filter AG.is_ornode keys: AG.keys; + val completely_proved_orkeys = filter (AG.is_proved_completely agraph) orkeys: AG.keys; + val completely_proved_terms:terms = map AG.orkey_to_term completely_proved_orkeys: terms; + val completely_proved_lemmas:thms = map (TDU.term_to_thm ctxt) completely_proved_terms: thms; + fun mk_simplifier (added:thm) (tobe_simplified:thm) = (added, Basic_Simplifier.asm_full_simplify (Simplifier.add_simp added ctxt) tobe_simplified): (thm * thm); + val simplifiers = map (mk_simplifier) completely_proved_lemmas: (thm -> (thm *thm)) list; + fun simplify_cnjctr_using_proved_lemma (cnjctr:term) = + let +val _ = tracing "Conjecture is:" +val _ = tracing (Isabelle_Utils.trm_to_string ctxt cnjctr); + val cnjctr_as_thm = TDU.term_to_thm ctxt cnjctr; + val thm_pairs = Utils.map_arg cnjctr_as_thm simplifiers: (thm * thm) list;(*(used_proved_lemma * simplified_result) list*) + val term_pairs = map (apply2 Thm.full_prop_of) thm_pairs: (term * term) list; +val _ = tracing ("The length of term_pairs is: " ^ Int.toString (length term_pairs)) +val _ = tracing "They are:" +val _ = map (fn (_, trm) => tracing (Isabelle_Utils.trm_to_string ctxt trm)) term_pairs +(*We only care if we can simplify the conjecture using already proved lemmas.*) + val filtered = filter_out (fn (_, simplified:term) => cnjctr = simplified) term_pairs: (term * term) list; +val _ = tracing ("The length of filtered is: " ^ Int.toString (length filtered)) + val used_lemmas = map fst filtered: terms; + val distinct_pairs = distinct (op =) filtered: (term * term) list; + in + distinct_pairs (*already completely proved lemmas that are used to reduce the conjecture to an or-term in the abduction graph.*) + end; + + fun replace_cnjctr_if_we_can_simplify_it_to_term_in_graph (string:string, cnjctr:term) = + let + val used_and_existing_lemma_pairs = simplify_cnjctr_using_proved_lemma cnjctr; + val used_and_existing_lemmas = map Utils.pair_to_list used_and_existing_lemma_pairs |> flat |> distinct (op =): terms; + val result_terms = if null used_and_existing_lemmas then [cnjctr] else used_and_existing_lemmas; +val _ = if null used_and_existing_lemmas then () else tracing "NOT NULL"; + val w_string = map (pair string) result_terms: (string * term) list; + in + w_string: (string * term) list + end; + + val explicit_wo_counterexample = explicit_wo_counterexample |> Par_List.map replace_cnjctr_if_we_can_simplify_it_to_term_in_graph |> flat |> distinct (op =) +*) val seed_from_explicit = SOOE.conjectures_to_seed_of_or2and_edge term2name pst explicit_wo_counterexample : seed_of_or2and_edge; val _ = SOOE.decremental_abduction pst or_key seed_from_explicit term2name synched_agraph : unit; (*tactic application as conjecturing. A little expensive*) diff --git a/Abduction/Seed_Of_Or2And_Edge.ML b/Abduction/Seed_Of_Or2And_Edge.ML index cb75f9fa..7817bc52 100644 --- a/Abduction/Seed_Of_Or2And_Edge.ML +++ b/Abduction/Seed_Of_Or2And_Edge.ML @@ -80,18 +80,12 @@ fun apply_PSL_to_get_seeds_of_or2and_edges (synched_term2string:SS.synched_term2 val _ = map (tracing' o (Isabelle_Utils.trm_to_string ctxt)) standardized_props: unit list; fun check_print_read ctxt term = term - |> (fn x => (tracing' ("checking " ^ Isabelle_Utils.trm_to_string ctxt term); x)) |> Isabelle_Utils.trm_to_string ctxt - |> (fn x => (tracing' "STEP 1"; x)) |> Syntax.read_term ctxt - |> (fn x => (tracing' "STEP 2"; x)) |> Isabelle_Utils.strip_atyp - |> (fn x => (tracing' "STEP 3"; x)) |> Syntax.check_term ctxt - |> (fn x => (tracing' "STEP 4"; x)) |> Top_Down_Util.standardize_vnames; - fun check_print_read_terms ctxt terms = map (check_print_read ctxt) terms: terms; fun pass_check_print_read_terms ctxt terms = try (check_print_read_terms ctxt) terms |> is_some; val mk_lemma_name = SS.get_lemma_name synched_term2string: Proof.context -> term -> string; @@ -180,10 +174,6 @@ fun conjectures_to_seed_of_or2and_edge (term2name:SS.synched_term2string_table) val cnjctrs = map snd cnjctrs_w_name : terms; val cnjctrs_as_props = map mk_prop cnjctrs : terms; val checked_cnjctrs = List.mapPartial check_prop cnjctrs_as_props : terms; -(* -val _ = tracing "++ 2: conjectures_to_seed_of_or2and_edge ++" -val _ = checked_cnjctrs |> map (tracing o Isabelle_Utils.trm_to_string (Proof.context_of pst)); -*) val ctxt = Proof.context_of pst : Proof.context; val name_cnjctr_pairs = map (fn cnjctr => (SS.get_lemma_name term2name ctxt cnjctr, cnjctr)) checked_cnjctrs: (string * term) list; val result = conjecture_to_seed_of_or2and_edge name_cnjctr_pairs : seed_of_or2and_edge; @@ -219,22 +209,13 @@ fun add_or2and_edge_and_connect_it_to_parental_ornode then tracing' ("--------- because they are the result of applying this induction: " ^ space_implode " " (Or2And_Edge.how_to_get_andnodes_from_ornode_of proof)) else tracing' "--------- because they are the result of explicit conjecturing"; - fun cnjctr_to_thm (ctxt:Proof.context) (cnjctr:term) = - let - val prop = if Top_Down_Util.is_prop cnjctr then cnjctr else HOLogic.mk_Trueprop cnjctr; - val fvar_names = Isabelle_Utils.get_free_var_names_in_trm prop |> distinct (op =): strings; - val thm = Goal.prove ctxt fvar_names [] cnjctr (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)): thm; - in - thm - end; - fun register_proved_thm_in_lthy (name:string) (thm:thm) (lthy:local_theory): local_theory = Local_Theory.note ((Binding.name name, []), [thm]) lthy |> snd: local_theory; fun assm_cnjctr_in_pst (name:string, cnjctr:term) (pst:Proof.state) = let - val ctxt = Proof.context_of pst : Proof.context; - val cnjctr_as_thm = cnjctr_to_thm ctxt cnjctr : thm; + val ctxt = Proof.context_of pst : Proof.context; + val cnjctr_as_thm = Top_Down_Util.term_to_thm ctxt cnjctr : thm; val pst_w_cnjctr_opt = try (Proof.map_context (register_proved_thm_in_lthy name cnjctr_as_thm)) pst: Proof.state option; val pst_w_cnjctr = case pst_w_cnjctr_opt of SOME no_dup_pst => no_dup_pst | _ => pst in diff --git a/Abduction/Top_Down_Util.ML b/Abduction/Top_Down_Util.ML index 949543d7..d46d64a5 100644 --- a/Abduction/Top_Down_Util.ML +++ b/Abduction/Top_Down_Util.ML @@ -32,6 +32,7 @@ val get_lemma_names_from_sh_output : theory -> string -> strings; val is_thm_name_registered : Proof.context -> string -> bool; val mk_new_lemma_name : Proof.context -> bool(*is_final_goal*) -> string; val term_compare : term * term -> order; +val term_to_thm : Proof.context -> term -> thm; end; @@ -217,6 +218,15 @@ fun mk_new_lemma_name (ctxt:Proof.context) (is_final_goal:bool): string = fun term_compare (trm1, trm2) = Term_Ord.term_ord (standardize_vnames trm1, standardize_vnames trm2); +fun term_to_thm (ctxt:Proof.context) (cnjctr:term) = + let + val prop = if is_prop cnjctr then cnjctr else HOLogic.mk_Trueprop cnjctr; + val fvar_names = Isabelle_Utils.get_free_var_names_in_trm prop |> distinct (op =): strings; + val thm = Goal.prove ctxt fvar_names [] cnjctr (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)): thm; + in + thm + end; + end; @@ -243,7 +253,7 @@ fun non_prop_trm_to_dummy_eq (ctxt:Proof.context) (lhs:term) = fun simp_non_prop_term (ctxt:Proof.context) (trm:term) = let val dummy_thm = non_prop_trm_to_dummy_eq ctxt trm: thm option; - val simplifier = Basic_Simplifier.simplify ctxt + val simplifier = Basic_Simplifier.asm_full_simplify ctxt val simped_dummy_thm = Option.mapPartial (try (Isabelle_Utils.timeout_apply (Time.fromSeconds 1) simplifier)) dummy_thm: thm option; val simped_fst_goal = Option.map Thm.concl_of simped_dummy_thm: term option; val simped_fst_pair = Option.mapPartial (try (HOLogic.dest_eq o HOLogic.dest_Trueprop)) simped_fst_goal: (term * term) option; diff --git a/SeLFiE/Assertion_Generalization.ML b/SeLFiE/Assertion_Generalization.ML index d3cd8a20..e7a59b66 100644 --- a/SeLFiE/Assertion_Generalization.ML +++ b/SeLFiE/Assertion_Generalization.ML @@ -256,7 +256,7 @@ Imply ( All ("recursive_on_nth_param", QOuter_Number, Imply ( Ands [ - Node_Takes_Less_Than_N_Arguments (Variable "func_occ", Variable "recursive_on_nth_param"), + Node_Takes_More_Than_N_Arguments (Variable "func_occ", Variable "recursive_on_nth_param"), In_Some_Definitions ( Variable "func", is_defined_recursively_on_nth, @@ -266,7 +266,7 @@ Imply ( All ("used_to_update_mth_arg", QOuter_Number, Imply ( Ands [ - Node_Takes_Less_Than_N_Arguments (Variable "func_occ", Variable "used_to_update_mth_arg"), + Node_Takes_More_Than_N_Arguments (Variable "func_occ", Variable "used_to_update_mth_arg"), Not (Are_Same_Number (Variable "recursive_on_nth_param", Variable "used_to_update_mth_arg")), In_Some_Definitions ( Variable "func", @@ -342,12 +342,12 @@ Imply ( Ands [ Some ("func_is_recurse_on_nth", QOuter_Number, Ands [ - Node_Takes_Less_Than_N_Arguments (Variable "func_trm_occ", Variable "func_is_recurse_on_nth"), (*Does this actually harm us?*) + Node_Takes_More_Than_N_Arguments (Variable "func_trm_occ", Variable "func_is_recurse_on_nth"), (*Does this actually harm us?*) Is_Nth_Argument_Or_Below_Nth_Argument_Of (Variable "ind_occ", Variable "func_is_recurse_on_nth", Variable "func_trm_occ"),(*Does this actually harm us?*) Some_Of ("arb_trm_occ", Variable "arb_trm", Some ("mth_arg_of_func_occ_has_arb", QOuter_Number, Ands [ - Node_Takes_Less_Than_N_Arguments (Variable "func_trm_occ", Variable "mth_arg_of_func_occ_has_arb"), + Node_Takes_More_Than_N_Arguments (Variable "func_trm_occ", Variable "mth_arg_of_func_occ_has_arb"), Some_Of ("func_trm_occ2", Variable "func_trm", (*we do not always talk about the same occurrence of the function. See addO_exp\_inj in Goodstein_Lambda.thy where we have to deal with two different occurrences of add0.*) Ands [ Is_Nth_Argument_Or_Below_Nth_Argument_Of (Variable "arb_trm_occ", Variable "mth_arg_of_func_occ_has_arb", Variable "func_trm_occ2"), @@ -488,7 +488,7 @@ Ors [ Ands [ All ("used_to_update_mth_arg", QOuter_Number, Ands [ - Node_Takes_Less_Than_N_Arguments (Variable "func_occ", Variable "used_to_update_mth_arg"), + Node_Takes_More_Than_N_Arguments (Variable "func_occ", Variable "used_to_update_mth_arg"), In_Some_Definitions ( Variable "func", mth_arg_of_func_occ_has_different_print_straw,