Abduction: critical change. conditino to filter out changed.

Also, higher importance for template-based conjectures.

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 15 \<close>
+setup\<open> Config.put_global Top_Down_Util.limit_for_other_decrement 20 \<close>
 
 (* UI *)
 ML\<open> (*This part (the definitions of long_keyword, long_statement, and short_statement) are from

Abduction/Abduction_Graph.ML

@@ -54,6 +54,7 @@ val lemma_name_of                                : abduction_graph -> key -> str
 val print_orkey                                  : Proof.context -> abduction_graph -> key -> unit;
 val proof_of                                     : abduction_graph -> key -> strings;
 val proof_id_of                                  : abduction_graph -> key -> int option;
+val is_template_based                            : abduction_graph -> key -> bool;
 val compute_importance_of_ornode                 : abduction_graph -> key -> real;
 val sort_orkeys_based_on_importance              : abduction_graph -> keys -> keys;
 
@@ -309,14 +310,26 @@ fun is_worth_proving (ctxt:Proof.context) (graph:abduction_graph) (key:key)  =
 (* proof_id_of *)
 fun proof_id_of (graph:abduction_graph) (key:key) = PGraph.get_node graph key |> Abduction_Node.proof_id_of: int option;
 
+(* is_template_based *)
+fun is_template_based (ag:abduction_graph) (key:key) =
+  let
+    val node   = PGraph.get_node ag key: abduction_node;
+    val result = Abduction_Node.is_template_based node;
+  in
+    result
+  end;
+
 (* compute_importance_of_ornode *)
 fun compute_importance_of_ornode (ag:abduction_graph) (orkey as (Or_N, _)) =
     let
       val parent_andkeys         = PGraph.immediate_preds ag orkey: keys;
       val importances_of_parents = map (importance ag) parent_andkeys: real list;
-      val importance             = case Utils.reals_to_max_option importances_of_parents of
+      val importance_from_parent = case Utils.reals_to_max_option importances_of_parents of
                                      NONE     => error "compute_importance_of_ornode. No ancestral andnode."
                                    | SOME max => max: real;
+      val importance = if is_template_based ag orkey
+                       then (1.0 + importance_from_parent) / 2.0
+                       else importance_from_parent: real; (*TODO: magic number & magic formula*)
     in
       importance
     end

Abduction/Abduction_Node.ML

@@ -34,6 +34,7 @@ val proof_of                                     : abduction_node -> strings opt
 val is_branch                                    : abduction_node -> bool;
 val is_final_goal                                : abduction_node -> bool;
 val lemma_name_of                                : abduction_node -> string;
+val is_template_based                            : abduction_node -> bool;
 val is_worth_proving                             : Proof.context -> abduction_node -> bool;
 
 (* query on abduction_node for or2and_edge *)
@@ -119,6 +120,10 @@ fun or2and_edge_to_proof (Or_To_And or2and_edge:abduction_node) = Or2And_Edge.or
 fun lemma_name_of (Or_Node or_nd) = #lemma_name or_nd
   | lemma_name_of _ = error "lemma_name_of failed. Not an Or_Node."
 
+(* is_template_based *)
+fun is_template_based (Or_Node ornode) = Or_Node.is_template_based ornode
+  | is_template_based _ = error "is_template_based in Abduction_Node.ML failed";
+
 (** destructors on abduction_node **)
 (* dest_Or_Node *)
 fun dest_Or_Node (Or_Node or_b) = or_b

Abduction/Or_Node.ML

@@ -21,6 +21,8 @@ val is_worth_proving    : Proof.context -> ornode -> bool;
 type is_final_goal = bool;
 val mk_ornode: Proof.context -> is_final_goal -> string -> term -> ornode;
 
+val is_template_based: ornode -> bool;
+
 (* update of ornode *)
 val update_gg_parent_not_finished: ornode -> bool -> ornode;
 val update_proved_completely     : ornode -> ornode;
@@ -68,6 +70,7 @@ fun is_worth_proving (ctxt:Proof.context) (ornode:ornode) =
 
 (* creation of ornode *)
 type is_final_goal = bool;
+
 fun mk_ornode (ctxt:Proof.context) (is_final_goal:is_final_goal) (lemma_name:string) (goal:term) =
   let
     val name = if   is_final_goal
@@ -87,6 +90,9 @@ fun mk_ornode (ctxt:Proof.context) (is_final_goal:is_final_goal) (lemma_name:str
    }: ornode
   end;
 
+fun is_template_based ({lemma_name, ...}: ornode) =
+  Top_Down_Util.is_template_based lemma_name;
+
 (** update of ornode **)
 (* update_gg_parent_not_finished *)
 (*