Abduction: bug fixed. add type cleaning and type checking to refutation.

Author: yutakang

Abduction/Abduction.thy

@@ -75,7 +75,7 @@ strategy Attack_On_Or_Node =
 
 setup\<open> Config.put_global Top_Down_Util.timeout_config (60.0 * 60.0 * 10.0) \<close>
 setup\<open> Config.put_global Top_Down_Util.limit_for_first_decrement 40 \<close>
-setup\<open> Config.put_global Top_Down_Util.limit_for_other_decrement 20 \<close>
+setup\<open> Config.put_global Top_Down_Util.limit_for_other_decrement 40 \<close>
 
 (* UI *)
 ML\<open> (*This part (the definitions of long_keyword, long_statement, and short_statement) are from

Abduction/Seed_Of_Or2And_Edge.ML

@@ -126,12 +126,6 @@ fun condition_to_filter_out_conjecture (parent_or(*parent_or*):term) (refutation
           not (SFTD.run_assertion pst parent_or SFTD.has_func_with_three_occs_in_a_row)
           andalso
           SFTD.run_assertion pst conjecture SFTD.has_func_with_three_occs_in_a_row;
-      fun has_counter_example_in_prems (pst:Proof.state) (term:term) =
-        let
-          val prems = Logic.strip_imp_prems term: terms;
-        in
-           SS.any_of_these_is_refuted refutation pst prems: bool
-        end;
       fun get_concl (term:term)       = try (snd o Logic.dest_implies) term
                                     <$> Top_Down_Util.standardize_vnames
                                     <$> Isabelle_Utils.strip_atyp
@@ -140,12 +134,19 @@ fun condition_to_filter_out_conjecture (parent_or(*parent_or*):term) (refutation
       val concl_of_meta_imp_in_conjec = get_concl conjecture: term option;
       fun concls_are_same _ = Utils.mk_option_pair (concl_of_meta_imp_in_parent, concl_of_meta_imp_in_conjec)
                           <$> (op =) |> Utils.is_some_true;
+      fun concl_of_conj_refuted_even_cncl_of_parent_is_not _ =
+          if is_none concl_of_meta_imp_in_parent orelse is_none concl_of_meta_imp_in_conjec
+          then false
+          else if SS.is_refuted refutation pst (the concl_of_meta_imp_in_parent)
+             then false
+             else  SS.is_refuted refutation pst (the concl_of_meta_imp_in_conjec);
     in
       too_large () orelse
       eq_to_final_goal () andalso from_tactic orelse
       concl_is_eq_to_final_goal () (*andalso seed_is_from_tactic seed*) orelse
       has_func_with_three_occs_in_a_row_even_though_the_parent_does_not_have_those () orelse
-      concls_are_same ()
+      concls_are_same () orelse
+      concl_of_conj_refuted_even_cncl_of_parent_is_not ()
 (*
       (*not from_tactic andalso not orig_prem_is_refuted andalso*) has_counter_example_in_prems pst conjecture(*TODO: This is BAD. We should also check if the conclusions are the same in the parent-node and the conjecture.*)
 *)

Abduction/Shared_State.ML

@@ -97,8 +97,11 @@ in
 fun refute (synched_table:synched_term2real_table) (pst:Proof.state) (cnjctr:term): real =
   let
     val cnjctr_prop       = if Top_Down_Util.is_prop cnjctr then cnjctr else HOLogic.mk_Trueprop cnjctr: term;
+    val cnjctr_prop_clean = Top_Down_Util.standardize_vnames cnjctr_prop
+                         |> Isabelle_Utils.strip_atyp
+                         |> Utils.try_with @{prop "False"} (Syntax.check_prop (Proof.context_of pst))  : term;
     val old_table         = Synchronized.value synched_table                                           : term2real_table;
-    val already_checked   = defined old_table cnjctr_prop                                              : bool;
+    val already_checked   = defined old_table cnjctr_prop_clean                                        : bool;
     fun quickcheck cnjctr = (cnjctr, TBC_Utils.term_has_counterexample_in_pst pst cnjctr)              : (term * real);
     val _                 =
       if   already_checked then ()
@@ -107,12 +110,12 @@ fun refute (synched_table:synched_term2real_table) (pst:Proof.state) (cnjctr:ter
           (* It is okay to spend some time to run quick-check before calling Synchronized.change:
            * Even if other threads find a counter-example for the same conjecture,
            * the result should be the same. *)
-          val pair = quickcheck cnjctr_prop
+          val pair = quickcheck cnjctr_prop_clean
         in
           Synchronized.change synched_table (insert_bool pair): unit
         end;
-    val new_table = Synchronized.value synched_table: term2real_table;
-    val result    = lookup new_table cnjctr_prop    : real;
+    val new_table = Synchronized.value synched_table  : term2real_table;
+    val result    = lookup new_table cnjctr_prop_clean: real;
   in
     result: real
   end;